From c27098ecc491d75c07dc4053ca6c5e46e8284387 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Fri, 1 Dec 2023 16:13:08 +0100 Subject: [PATCH] First version of full incremental solving loop --- src/bin/common/solving_loop.ml | 563 ++++++++++++++---- src/lib/frontend/d_cnf.ml | 465 ++++----------- src/lib/frontend/d_cnf.mli | 69 ++- src/lib/frontend/d_state_option.ml | 91 ++- src/lib/frontend/d_state_option.mli | 30 +- src/lib/frontend/frontend.ml | 21 +- src/lib/reasoners/fun_sat.ml | 36 +- src/lib/reasoners/fun_sat_frontend.ml | 35 +- src/lib/reasoners/satml.ml | 20 +- src/lib/reasoners/satml_frontend.ml | 4 +- tests/cram.t/postlude.smt2 | 4 +- tests/cram.t/prelude.ae | 2 +- tests/issues/926.models.smt2 | 2 +- .../smtlib/testfile-get-info1.dolmen.expected | 2 +- 14 files changed, 811 insertions(+), 533 deletions(-) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 746e17dcc1..e0daa120a0 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -52,7 +52,7 @@ type any_sat_module = (module Sat_solver_sig.S) (* Internal state while iterating over input statements *) type 'a state = { env : 'a; - solver_ctx: solver_ctx; + solver_ctx : solver_ctx; sat_solver : any_sat_module; } @@ -104,14 +104,14 @@ let cmd_on_modes st modes cmd = Errors.forbidden_command curr_mode cmd end -(* Dolmen util *) +(* Dolmen helpers *) (** Adds the named terms of the statement [stmt] to the map accumulator [acc] *) let add_if_named ~(acc : DStd.Expr.term Util.MS.t) - (stmt : Typer_Pipe.typechecked D_loop.Typer_Pipe.stmt) = + (stmt : 'a D_loop.Typer_Pipe.stmt) = match stmt.contents with - | `Defs [`Term_def ({name = Simple n; _}, id, _, _, t)] -> + | `Defs [`Term_def (DStd.Id.{name = Simple n; _}, id, _, _, t)] -> begin match DStd.Expr.Id.get_tag id DStd.Expr.Tags.named with | None -> acc @@ -121,13 +121,62 @@ let add_if_named names. *) acc +(** Translates dolmen locs to Alt-Ergo's locs *) +let dl_to_ael dloc_file (compact_loc: DStd.Loc.t) = + DStd.Loc.(lexing_positions (loc dloc_file compact_loc)) + (* We currently use the full state of the solver as model. *) type model = Model : 'a sat_module * 'a -> model type solve_res = | Sat of model | Unknown of model option - | Unsat + | Unsat of Explanation.t + +let check_status_consistency s = + let known_status = Options.get_status () in + match s with + | Unsat _ -> + if known_status == Status_Sat then begin + Printer.print_wrn + "This file is known to be Sat but Alt-Ergo return Unsat"; + Errors.warning_as_error () + end + | Sat _ -> + if known_status == Status_Unsat then begin + Printer.print_wrn + "This file is known to be Unsat but Alt-Ergo return Sat"; + Errors.warning_as_error () + end + | Unknown _ -> assert false + +let print_solve_res loc goal_name r = + let validity_mode = + match Options.get_output_format () with + | Smtlib2 -> false + | Native | Why3 | Unknown _ -> true + in + let time = O.Time.value () in + let steps = Steps.get_steps () in + match r with + | Sat _ -> + Printer.print_status_sat ~validity_mode + (Some loc) (Some time) (Some steps) (Some goal_name); + check_status_consistency r; + | Unsat dep -> + Printer.print_status_unsat ~validity_mode + (Some loc) (Some time) (Some steps) (Some goal_name); + if O.get_unsat_core() && + not (O.get_debug_unsat_core()) && + not (O.get_save_used_context()) + then + Printer.print_fmt (Options.Output.get_fmt_regular ()) + "unsat-core:@,%a@." + (Explanation.print_unsat_core ~tab:true) dep; + check_status_consistency r + | Unknown _ -> + Printer.print_status_unknown ~validity_mode + (Some loc) (Some time) (Some steps) (Some goal_name); exception StopProcessDecl @@ -197,7 +246,7 @@ let main () = end; Unknown (Some mdl) end - | `Unsat -> Unsat + | `Unsat -> Unsat ftdn_env.expl with Util.Timeout -> (* It is still necessary to leave this catch here, because we may trigger this exception in between calls of the sat solver. *) @@ -219,24 +268,28 @@ let main () = begin match kind with | Ty.Check | Ty.Cut -> - { state with solver_ctx = - { state.solver_ctx with local = []}} + { state with solver_ctx = {state.solver_ctx with local = []}} | Ty.Thm | Ty.Sat -> - { state with solver_ctx = { - state.solver_ctx with global = []; local = []}} + { state with solver_ctx = + {state.solver_ctx with global = []; local = []}} end | Typed.TAxiom (_, s, _, _) when Ty.is_global_hyp s -> let cnf = Cnf.make state.solver_ctx.global td in - { state with solver_ctx = { state.solver_ctx with global = cnf; }} + { state with solver_ctx = + { state.solver_ctx with global = cnf } + } | Typed.TAxiom (_, s, _, _) when Ty.is_local_hyp s -> let cnf = Cnf.make state.solver_ctx.local td in - { state with solver_ctx = { state.solver_ctx with local = cnf; }} - | Typed.TReset _ -> - { state with solver_ctx = {ctx = []; local = []; global = []}} + { state with solver_ctx = + { state.solver_ctx with local = cnf; } + } + | Typed.TReset _ -> {state with solver_ctx = empty_solver_ctx} | Typed.TExit _ -> raise Exit | _ -> let cnf = Cnf.make state.solver_ctx.ctx td in - { state with solver_ctx = { state.solver_ctx with ctx = cnf; }} + { state with solver_ctx = + { state.solver_ctx with ctx = cnf } + } end in @@ -304,7 +357,8 @@ let main () = if O.get_parse_only () then state else begin try let l, env = I.type_parsed state.env assertion_stack p in - List.fold_left (typed_loop all_used_context) { state with env; } l + let state = {state with env} in + List.fold_left (typed_loop all_used_context) state l with | Errors.Error e -> let () = @@ -331,7 +385,12 @@ let main () = } in try let parsed_seq = parsed () in - let _ : _ state = Seq.fold_left typing_loop state parsed_seq in + let _ : _ state = + Seq.fold_left + typing_loop + state + parsed_seq + in Options.Time.unset_timeout (); with Util.Timeout -> Frontend.print_status (Timeout None) 0; @@ -354,6 +413,23 @@ let main () = State.create_key ~pipe:"" "is_incremental" in + (* Before each query, we push the current environment. This allows to keep a + fresh one for the next assertions. *) + let internal_push st = + let module Api = (val (DO.SatSolverModule.get st)) in + Steps.apply_without_step_limit (fun _ -> Api.FE.push 1 Api.env); + st + in + + (* The pop corresponding to the previous push. It is applied everytime the + mode goes from Sat/Unsat to Assert. *) + let internal_pop st = + assert (List.mem (DO.Mode.get st) [Sat; Unsat]); + let module Api = (val (DO.SatSolverModule.get st)) in + Steps.apply_without_step_limit (fun _ -> Api.FE.pop 1 Api.env); + st + in + let set_steps_bound i st = try DO.Steps.set i st with Invalid_argument _ -> (* Raised by Steps.set_steps_bound *) @@ -415,7 +491,7 @@ let main () = in let set_partial_model_and_mode solve_res st = match solve_res with - | Unsat -> + | Unsat _ -> st |> DO.Mode.set Util.Unsat |> State.set partial_model_key None @@ -524,6 +600,20 @@ let main () = |> Typer_Pipe.init ~type_check in + (* Initializing hooks in the mode handler. + When we perform a check-sat, the environment we are working on is specific + to the Sat or Unsat mode we end up in. If we start asserting again, we must + do it in the previous environment. + *) + let () = + DO.Mode.reset_hooks (); + DO.Mode.add_hook + (fun _ ~old ~new_ st -> + match old, new_ with + | (Sat | Unsat), Assert -> internal_pop st + | _ -> st + ) + in let print_wrn_opt ~name loc ty value = warning "%a The option %s expects a %s, got %a" @@ -682,61 +772,79 @@ let main () = unsupported_opt name; st in - let handle_optimize_stmt ~is_max loc id (term : DStd.Expr.Term.t) st = - let contents = `Optimize (term, is_max) in - let stmt = { Typer_Pipe.id; contents; loc; attrs = []; implicit = false } in - let cnf = - D_cnf.make (State.get State.logic_file st).loc - (State.get solver_ctx_key st).ctx stmt - in - (* Using both optimization and incremental mode may be wrong if - some optimization constraints aren't at the toplevel. - See issue: https://github.com/OCamlPro/alt-ergo/issues/993. *) + let handle_optimize_stmt ~is_max loc expr st = + let st = DO.Mode.set Assert st in + let module Api = (val (DO.SatSolverModule.get st)) in if State.get incremental_depth st > 0 then warning "Optimization constraints in presence of push \ and pop statements are not correctly processed."; - State.set solver_ctx_key ( - let solver_ctx = State.get solver_ctx_key st in - { solver_ctx with ctx = cnf } - ) st + let () = + if not @@ D_cnf.is_pure_term expr then + begin + recoverable_error + "the expression %a is not a valid objective function. \ + Only terms without let bindings or ite subterms can be optimized." + Expr.print expr + end + else + Api.FE.optimize ~loc (expr, is_max) Api.env + in st in let handle_get_objectives (_args : DStd.Expr.Term.t list) st = - let () = - if Options.get_interpretation () then - match State.get partial_model_key st with - | Some Model ((module SAT), partial_model) -> - let objectives = SAT.get_objectives partial_model in - begin - match objectives with - | Some o -> - if not @@ Objective.Model.has_no_limit o then - warning "Some objectives cannot be fulfilled"; - Objective.Model.pp (Options.Output.get_fmt_regular ()) o - | None -> - recoverable_error "No objective generated" - end - | None -> - recoverable_error - "Model generation is disabled (try --produce-models)" - in - st + if Options.get_interpretation () then + match State.get partial_model_key st with + | Some Model ((module SAT), partial_model) -> + let objectives = SAT.get_objectives partial_model in + begin + match objectives with + | Some o -> + if not @@ Objective.Model.has_no_limit o then + warning "Some objectives cannot be fulfilled"; + Objective.Model.pp (Options.Output.get_fmt_regular ()) o + | None -> + recoverable_error "No objective generated" + end + | None -> + recoverable_error + "Model generation is disabled (try --produce-models)" in let handle_custom_statement loc id args st = let args = List.map Dolmen_type.Core.Smtlib2.sexpr_as_term args in let logic_file = State.get State.logic_file st in let st, terms = Typer.terms st ~input:(`Logic logic_file) ~loc args in + let loc = + let dloc_file = (State.get State.logic_file st).loc in + dl_to_ael dloc_file loc + in match id, terms.ret with - | Dolmen.Std.Id.{name = Simple "minimize"; _}, [term] -> + | Dolmen.Std.Id.{name = Simple ("minimize" as name_base); _}, [term] -> cmd_on_modes st [Assert] "minimize"; - handle_optimize_stmt ~is_max:false loc id term st - | Dolmen.Std.Id.{name = Simple "maximize"; _}, [term] -> + let expr = + D_cnf.make_expr + ~loc + ~name_base + ~toplevel:true + ~decl_kind:Expr.Dobjective + term + in + handle_optimize_stmt ~is_max:false loc expr st + | Dolmen.Std.Id.{name = Simple ("maximize" as name_base); _}, [term] -> cmd_on_modes st [Assert] "maximize"; - handle_optimize_stmt ~is_max:true loc id term st + let expr = + D_cnf.make_expr + ~loc + ~name_base + ~toplevel:true + ~decl_kind:Expr.Dobjective + term + in + handle_optimize_stmt ~is_max:true loc expr st | Dolmen.Std.Id.{name = Simple "get-objectives"; _}, terms -> cmd_on_modes st [Sat] "get-objectives"; - handle_get_objectives terms st + handle_get_objectives terms st; + st | Dolmen.Std.Id.{name = Simple (("minimize" | "maximize") as ext); _}, _ -> recoverable_error "Statement %s only expects 1 argument (%i given)" @@ -834,26 +942,279 @@ let main () = assignments in + (* Copied from D_cnf, this treats the `Hyp case. *) + let assume_axiom st name t loc attrs : unit = + let module Api = (val (DO.SatSolverModule.get st)) in + let dloc_file = (State.get State.logic_file st).loc in + let dloc = DStd.Loc.loc dloc_file loc in + let aloc = DStd.Loc.lexing_positions dloc in + (* Dolmen adds information about theory extensions and case splits in the + [attrs] field of the parsed statements. [attrs] can be arbitrary terms, + where the information we care about is encoded as a [Colon]-list of + symbols. + + The few helper functions below are used to extract the information from + the [attrs]. More specifically: + + - "case split" statements have the [DStd.Id.case_split] symbol as an + attribute + + - Theory elements have a 3-length list of symbols as an attribute, of + the form [theory_decl; name; extends], where [theory_decl] is the + symbol [DStd.Id.theory_decl] and [name] and [extends] are the theory + extension name and the base theory name, respectively. + *) + let rec symbols = function + | DStd.Term. { term = Colon ({ term = Symbol sy; _ }, xs); _ } -> + Option.bind (symbols xs) @@ fun sys -> + Some (sy :: sys) + | { term = Symbol sy; _ } -> Some [sy] + | _ -> None + in + let sy_attrs = List.filter_map symbols attrs in + let is_case_split = + let is_case_split = function + | [ sy ] when DStd.Id.(equal sy case_split) -> true + | _ -> false + in + List.exists is_case_split sy_attrs + in + let theory = + let theory = + let open DStd.Id in + function + | [ td; name; extends] when DStd.Id.(equal td theory_decl) -> + let name = match name.name with + | Simple name -> name + | _ -> + Fmt.failwith + "Internal error: invalid theory extension: %a" + print name + in + let extends = match extends.name with + | Simple name -> + begin match Util.th_ext_of_string name with + | Some extends -> extends + | None -> + Errors.typing_error (ThExtError name) aloc + end + | _ -> + Fmt.failwith + "Internal error: invalid base theory name: %a" + print extends + in + Some (name, extends) + | _ -> None + in + match List.filter_map theory sy_attrs with + | [] -> None + | [name, extends] -> Some (name, extends) + | _ -> + Fmt.failwith + "%a: Internal error: multiple theories." + DStd.Loc.fmt dloc + in + let st_loc = dl_to_ael dloc_file loc in + match theory with + | Some (th_name, extends) -> + let axiom_kind = + if is_case_split then Util.Default else Util.Propagator + in + let e = D_cnf.make_form name t st_loc ~decl_kind:Expr.Dtheory in + let th_elt = { + Expr.th_name; + axiom_kind; + extends; + ax_form = e; + ax_name = name; + } in + Api.FE.th_assume ~loc:st_loc th_elt Api.env + | None -> + let e = D_cnf.make_form name t st_loc ~decl_kind:Expr.Daxiom in + Api.FE.assume ~loc:st_loc (name, e, true) Api.env + in + + (* Push the current environment and performs the query. + If an assertion is performed, we have to pop it back. This is handled by + the hook on D_state_option.Mode. *) + let handle_query st id loc attrs contents = + let module Api = (val (DO.SatSolverModule.get st)) in + (* Setting the current mode. We must go back to Assert mode in case we + want to trigger the pop registered as a mode hook. *) + let st = DO.Mode.set Assert st in + (* Pushing the environment once. This allows to keep a trace of the old + environment in case we want to assert afterwards. + The `pop` instruction is handled by the hook on the mode: when we assert + anything, we must make sure to go back to `Assert` mode. *) + let st = internal_push st in + let st_loc = + let file_loc = (State.get State.logic_file st).loc in + dl_to_ael file_loc loc + in + let name = + match id.DStd.Id.name with + | Simple name -> name + | Indexed _ | Qualified _ -> assert false + in + (* First, we check the environment if it already concluded. *) + let solve_res = + match Api.env.res with + | `Unsat -> Unsat Api.env.expl + | `Sat -> + begin + let mdl = Model ((module Api.SAT), Api.env.sat_env) in + let () = + if Options.(get_interpretation () && get_dump_models ()) then + Api.FE.print_model + (Options.Output.get_fmt_models ()) + Api.env.sat_env + in + Sat mdl + end + | `Unknown -> + (* The environment did not conclude yet. *) + begin + (* Preprocessing query. *) + let goal_sort = + match contents with + | `Goal _ -> Ty.Thm + | `Check _ -> Ty.Sat + in + let hyps, t = + match contents with + | `Goal t -> + D_cnf.pp_query t + | `Check hyps -> + D_cnf.pp_query ~hyps (DStd.Expr.Term.(of_cst Const._false)) + in + let () = + List.iter ( + fun t -> + let name = Ty.fresh_hypothesis_name goal_sort in + assume_axiom st name t loc attrs + ) hyps + in + let e = D_cnf.make_form "" t st_loc ~decl_kind:Expr.Dgoal in + (* Performing the query. *) + Api.FE.query ~loc:st_loc (name, e, goal_sort) Api.env; + (* Treatment of the result. *) + let partial_model = Api.env.sat_env in + (* If the status of the SAT environment is inconsistent, + we have to drop the partial model in order to prevent + printing wrong model. *) + match Api.env.res with + | `Sat -> + begin + let mdl = Model ((module Api.SAT), partial_model) in + let () = + if Options.(get_interpretation () && get_dump_models ()) then + Api.FE.print_model + (Options.Output.get_fmt_models ()) + partial_model + in + Sat mdl + end + | `Unknown -> + begin + let mdl = Model ((module Api.SAT), partial_model) in + if Options.(get_interpretation () && get_dump_models ()) then begin + let ur = Api.SAT.get_unknown_reason partial_model in + Printer.print_fmt (Options.Output.get_fmt_diagnostic ()) + "@[Returned unknown reason = %a@]" + Sat_solver_sig.pp_ae_unknown_reason_opt ur; + Api.FE.print_model + (Options.Output.get_fmt_models ()) + partial_model + end; + Unknown (Some mdl) + end + | `Unsat -> Unsat Api.env.expl + end + in + (* Prints the result. *) + print_solve_res st_loc name solve_res; + (* Updates the dolmen state. *) + set_partial_model_and_mode solve_res st + in + let handle_stmt : - Frontend.used_context -> State.t -> - 'a D_loop.Typer_Pipe.stmt -> State.t = + Frontend.used_context -> + State.t -> + [< Typer_Pipe.typechecked | `Check of 'a ] D_loop.Typer_Pipe.stmt -> + State.t = let goal_cnt = ref 0 in - fun all_context st td -> + fun + _all_context + st + td -> let file_loc = (State.get State.logic_file st).loc in - let solver_ctx = State.get solver_ctx_key st in match td with + (* Set logic *) | { contents = `Set_logic _; _} -> cmd_on_modes st [Start] "set-logic"; DO.Mode.set Util.Assert st + + (* Push and Pop commands *) + | { contents = `Pop n; loc; _ } -> + let module Api = (val (DO.SatSolverModule.get st)) in + let st = DO.Mode.set Util.Assert st in + Api.FE.pop + ~loc:(dl_to_ael file_loc loc) + n + Api.env; + st + | { contents = `Push n; loc; _ } -> + let module Api = (val (DO.SatSolverModule.get st)) in + let st = DO.Mode.set Util.Assert st in + Api.FE.push + ~loc:(dl_to_ael file_loc loc) + n + Api.env; + st + + (* Goal definition *) + | { + id; loc; attrs; + contents = (`Goal _) as contents; + implicit = _; + } -> + cmd_on_modes st [Assert; Sat; Unsat] "goal"; + (* Setting the mode is done by handle_query. *) + handle_query st id loc attrs contents + + (* Axiom definitions *) + | { id = DStd.Id.{name = Simple name; _}; contents = `Hyp t; loc; attrs; + implicit=_ } -> + let st = DO.Mode.set Util.Assert st in + assume_axiom st name t loc attrs; + st + + | { contents = `Defs defs; loc; _ } -> + let module Api = (val (DO.SatSolverModule.get st)) in + let st = DO.Mode.set Util.Assert st in + let loc = dl_to_ael file_loc loc in + let defs = D_cnf.make_defs defs loc in + let () = + List.iter + (function + | `Assume (name, e) -> Api.FE.assume ~loc (name, e, true) Api.env + | `PredDef (e, name) -> Api.FE.pred_def ~loc (name, e) Api.env + ) + defs + in + st + + | {contents = `Decls l; _} -> + let st = DO.Mode.set Util.Assert st in + D_cnf.cache_decls l; + st + (* When the next statement is a goal, the solver is called and provided the goal and the current context *) - | { id; contents = (`Solve _ as contents); loc ; attrs; implicit } -> - cmd_on_modes st [Assert; Sat; Unsat] "solve"; - let l = - solver_ctx.local @ - solver_ctx.global @ - solver_ctx.ctx - in + | { id; contents = (`Solve _ as contents); loc ; attrs; implicit=_ } -> + cmd_on_modes st [Assert; Unsat; Sat] "check-sat"; + (* Setting the mode is done by handle_query. *) + let module Api = (val DO.SatSolverModule.get st) in let id = match (State.get State.logic_file st).lang with | Some (Smtlib2 _) -> @@ -861,52 +1222,17 @@ let main () = "g_" ^ string_of_int (incr goal_cnt; !goal_cnt) | _ -> id in - let name = - match id.name with - | Simple name -> name - | _ -> - let loc = DStd.Loc.loc file_loc loc in - Fmt.failwith "%a: internal error: goal name should be simple" - DStd.Loc.fmt loc - in let contents = match contents with | `Solve (hyps, []) -> `Check hyps | `Solve ([], [t]) -> `Goal t | _ -> let loc = DStd.Loc.loc file_loc loc in - Fmt.failwith "%a: internal error: unknown statement" + fatal_error "%a: internal error: unknown statement" DStd.Loc.fmt loc in - let stmt = { Typer_Pipe.id; contents; loc ; attrs; implicit } in - let cnf, is_thm = - match D_cnf.make (State.get State.logic_file st).loc l stmt with - | { Commands.st_decl = Query (_, _, kind); _ } as cnf :: hyps -> - let is_thm = - match kind with Ty.Thm | Sat -> true | _ -> false - in - List.rev (cnf :: hyps), is_thm - | _ -> assert false - in - let solve_res = - solve - (DO.SatSolverModule.get st) - all_context - (cnf, name) - in - if is_thm - then - State.set solver_ctx_key ( - let solver_ctx = State.get solver_ctx_key st in - { solver_ctx with global = []; local = [] } - ) st - |> set_partial_model_and_mode solve_res - else - State.set solver_ctx_key ( - let solver_ctx = State.get solver_ctx_key st in - { solver_ctx with local = [] } - ) st - |> set_partial_model_and_mode solve_res + (* Performing the query *) + handle_query st id loc attrs contents; | {contents = `Set_option { DStd.Term.term = @@ -942,6 +1268,7 @@ let main () = end | {contents = `Reset; _} -> + let () = Steps.reset_steps () in st |> State.set partial_model_key None |> State.set solver_ctx_key empty_solver_ctx @@ -989,28 +1316,10 @@ let main () = | {contents = `Other (custom, args); loc; _} -> handle_custom_statement loc custom args st - | td -> - let st = - match td.contents with - | `Pop n -> - State.set incremental_depth (State.get incremental_depth st - n) st - | `Push n -> - State.set incremental_depth (State.get incremental_depth st + n) st - | _ -> st - in - (* TODO: - - Separate statements that should be ignored from unsupported - statements and throw exception or print a warning when an - unsupported statement is encountered. - *) - let cnf = - D_cnf.make (State.get State.logic_file st).loc - (State.get solver_ctx_key st).ctx td - in - State.set solver_ctx_key ( - let solver_ctx = State.get solver_ctx_key st in - { solver_ctx with ctx = cnf } - ) st + | _ -> + Printer.print_dbg ~header:true + "Ignoring statement: %a" Typer_Pipe.print td; + st in let handle_stmts all_context st l = let rec aux named_map st = function diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml index e88b949671..5d47663f42 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/src/lib/frontend/d_cnf.ml @@ -507,10 +507,6 @@ let builtins = | `Logic (Smtlib2 _) -> bv_builtins ++ smt_fpa_builtins | _ -> fun _ _ -> `Not_found -(** Translates dolmen locs to Alt-Ergo's locs *) -let dl_to_ael dloc_file (compact_loc: DStd.Loc.t) = - DStd.Loc.(lexing_positions (loc dloc_file compact_loc)) - (** clears the cache in the [Cache] module. *) let clear_cache () = Cache.clear () @@ -1014,11 +1010,7 @@ let mk_rounding fpar = Sy.Op (Sy.Constr (Hstring.make name)) in E.mk_term sy [] ty -(** [mk_expr ~loc ~name_base ~toplevel ~decl_kind term] - - Builds an Alt-Ergo hashconsed expression from a dolmen term -*) -let rec mk_expr +let rec make_expr ?(loc = Loc.dummy) ?(name_base = "") ?(toplevel = false) ~decl_kind dt = let name_tag = ref 0 in @@ -1700,7 +1692,7 @@ and make_trigger ?(loc = Loc.dummy) ~name_base ~decl_kind | e -> [e] in let mk_expr = - mk_expr ~loc ~name_base ~decl_kind + make_expr ~loc ~name_base ~decl_kind in let content = List.map mk_expr e in let t_depth = @@ -1794,9 +1786,101 @@ let pp_query ?(hyps =[]) t = let axioms, goal = intro_hypothesis t in List.rev_append (List.rev_map (elim_toplevel_forall false) hyps) axioms, goal +let make_defs defs loc = + (* For a mutually recursive definition, we have to add all the function + names in a row. *) + List.iter (fun (def : Typer_Pipe.def) -> + match def with + | `Term_def (_, ({ path; _ } as tcst), _, _, _) -> + let name_base = get_basename path in + let sy = Sy.name ~defined:true name_base in + Cache.store_sy tcst sy + | `Type_alias _ -> () + | `Instanceof _ -> + (* These statements are only used in models when completing a + polymorphic partially-defined bulitin and should not end up + here. *) + assert false + ) defs; + List.filter_map (fun (def : Typer_Pipe.def) -> + match def with + | `Term_def ( _, ({ path; tags; _ } as tcst), tyvars, terml, body) -> + Cache.store_tyvl tyvars; + let name_base = get_basename path in + let binders_set, defn = + let rty = dty_to_ty body.term_ty in + let binders_set, rev_args = + List.fold_left ( + fun (binders_set, acc) (DE.{ path; id_ty; _ } as tv) -> + let ty = dty_to_ty id_ty in + let sy = Sy.var (Var.of_string (get_basename path)) in + Cache.store_sy tv sy; + let e = E.mk_term sy [] ty in + SE.add e binders_set, e :: acc + ) (SE.empty, []) terml + in + let sy = Cache.find_sy tcst in + let e = E.mk_term sy (List.rev rev_args) rty in + binders_set, e + in + begin match DStd.Tag.get tags DE.Tags.predicate with + | Some () -> + let decl_kind = E.Dpredicate defn in + let ff = + make_expr ~loc ~name_base + ~toplevel:false ~decl_kind body + in + let qb = E.mk_eq ~iff:true defn ff in + let binders = E.mk_binders binders_set in + let ff = + E.mk_forall name_base Loc.dummy binders [] qb ~toplevel:true + ~decl_kind + in + assert (Var.Map.is_empty (E.free_vars ff Var.Map.empty)); + let ff = E.purify_form ff in + let e = + if Ty.Svty.is_empty (E.free_type_vars ff) then ff + else + E.mk_forall name_base loc + Var.Map.empty [] ff ~toplevel:true ~decl_kind + in + Some (`PredDef (e, name_base)) + | None -> + let decl_kind = E.Dfunction defn in + let ff = + make_expr ~loc ~name_base + ~toplevel:false ~decl_kind body + in + let iff = Ty.equal (Expr.type_info defn) (Ty.Tbool) in + let qb = E.mk_eq ~iff defn ff in + let binders = E.mk_binders binders_set in + let ff = + E.mk_forall name_base Loc.dummy binders [] qb ~toplevel:true + ~decl_kind + in + assert (Var.Map.is_empty (E.free_vars ff Var.Map.empty)); + let ff = E.purify_form ff in + let e = + if Ty.Svty.is_empty (E.free_type_vars ff) then ff + else + E.mk_forall name_base loc + Var.Map.empty [] ff ~toplevel:true ~decl_kind + in + if Options.get_verbose () then + Format.eprintf "defining term of %a@." DE.Term.print body; + Some (`Assume (name_base, e)) + end + | `Type_alias _ -> None + | `Instanceof _ -> + (* These statements are only used in models when completing a + polymorphic partially-defined bulitin and should not end up + here. *) + assert false + ) defs + let make_form name_base f loc ~decl_kind = let ff = - mk_expr ~loc ~name_base ~toplevel:true ~decl_kind f + make_expr ~loc ~name_base ~toplevel:true ~decl_kind f in assert (Var.Map.is_empty (E.free_vars ff Var.Map.empty)); let ff = E.purify_form ff in @@ -1804,6 +1888,42 @@ let make_form name_base f loc ~decl_kind = else E.mk_forall name_base loc Var.Map.empty [] ff ~toplevel:true ~decl_kind +let cache_decls = function + | [] -> assert false (* We could probably just return (). *) + | [td] -> + begin + match td with + | `Type_decl (td, _def) -> mk_ty_decl td + | `Term_decl td -> mk_term_decl td + end + | dcl -> + let rec aux acc tdl = + (* for now, when acc has more than one element it is assumed that the + types are mutually recursive. Which is not necessarily the case. + But it doesn't affect the execution. + *) + match tdl with + | `Term_decl td :: tl -> + begin match acc with + | [] -> () + | [otd] -> mk_ty_decl otd + | _ -> mk_mr_ty_decls (List.rev acc) + end; + mk_term_decl td; + aux [] tl + + | `Type_decl (td, _def) :: tl -> + aux (td :: acc) tl + + | [] -> + begin match acc with + | [] -> () + | [otd] -> mk_ty_decl otd + | _ -> mk_mr_ty_decls (List.rev acc) + end + in + aux [] dcl + (* Helper function used to check if the expression defining an objective function is a pure term. *) let rec is_pure_term t = @@ -1812,326 +1932,3 @@ let rec is_pure_term t = | (Sy.Let | Lit _ | Form _) -> false | Sy.Op Tite -> false | _ -> List.for_all is_pure_term xs - -let make dloc_file acc stmt = - let rec aux acc (stmt: _ Typer_Pipe.stmt) = - match stmt with - (* Optimize terms *) - | { contents = `Optimize (t, is_max); loc; _ } -> - let st_loc = dl_to_ael dloc_file loc in - let e = - mk_expr ~loc:st_loc ~toplevel:true ~decl_kind:Dobjective t - in - if not @@ is_pure_term e then - begin - Printer.print_wrn - "the expression %a is not a valid objective function. \ - Only terms without let bindings or ite subterms can be optimized." - E.print e; - acc - end - else - let st_decl = C.Optimize (e, is_max) in - C.{ st_decl; st_loc } :: acc - - (* Push and Pop commands *) - | { contents = `Pop n; loc; _ } -> - let st_loc = dl_to_ael dloc_file loc in - let st_decl = C.Pop n in - C.{ st_decl; st_loc } :: acc - - | { contents = `Push n; loc; _ } -> - let st_loc = dl_to_ael dloc_file loc in - let st_decl = C.Push n in - C.{ st_decl; st_loc } :: acc - - (* Goal and check-sat definitions *) - | { - id; loc; attrs; - contents = (`Goal _ | `Check _) as contents; - implicit; - } -> - let name = - match id.name with - | Simple name -> name - | Indexed _ | Qualified _ -> assert false - in - let goal_sort = - match contents with - | `Goal _ -> Ty.Thm - | `Check _ -> Ty.Sat - in - let st_loc = dl_to_ael dloc_file loc in - let _hyps, t = - match contents with - | `Goal t -> - pp_query t - | `Check hyps -> - pp_query ~hyps (DStd.Expr.Term.(of_cst Const._false)) - in - let rev_hyps_c = - List.fold_left ( - fun acc t -> - let ns = DStd.Namespace.Decl in - let name = Ty.fresh_hypothesis_name goal_sort in - let decl: _ Typer_Pipe.stmt = { - id = Id.mk ns name; - contents = `Hyp t; loc; attrs; implicit - } - in - aux acc decl - ) [] _hyps - in - let e = make_form "" t st_loc ~decl_kind:E.Dgoal in - let st_decl = C.Query (name, e, goal_sort) in - C.{st_decl; st_loc} :: List.rev_append (List.rev rev_hyps_c) acc - - | { contents = `Solve _; _ } -> - (* Filtered out by the solving_loop *) - (* TODO: Remove them from the types *) - assert false - - (* Axiom definitions *) - | { id = Id.{name = Simple name; _}; contents = `Hyp t; loc; attrs; - implicit=_ } -> - let dloc = DStd.Loc.(loc dloc_file stmt.loc) in - let aloc = DStd.Loc.lexing_positions dloc in - (* Dolmen adds information about theory extensions and case splits in the - [attrs] field of the parsed statements. [attrs] can be arbitrary terms, - where the information we care about is encoded as a [Colon]-list of - symbols. - - The few helper functions below are used to extract the information from - the [attrs]. More specifically: - - - "case split" statements have the [DStd.Id.case_split] symbol as an - attribute - - - Theory elements have a 3-length list of symbols as an attribute, of - the form [theory_decl; name; extends], where [theory_decl] is the - symbol [DStd.Id.theory_decl] and [name] and [extends] are the theory - extension name and the base theory name, respectively. - *) - let rec symbols = function - | DStd.Term. { term = Colon ({ term = Symbol sy; _ }, xs); _ } -> - Option.bind (symbols xs) @@ fun sys -> - Some (sy :: sys) - | { term = Symbol sy; _ } -> Some [sy] - | _ -> None - in - let sy_attrs = List.filter_map symbols attrs in - let is_case_split = - let is_case_split = function - | [ sy ] when DStd.Id.(equal sy case_split) -> true - | _ -> false - in - List.exists is_case_split sy_attrs - in - let theory = - let theory = - let open DStd.Id in - function - | [ td; name; extends] when DStd.Id.(equal td theory_decl) -> - let name = match name.name with - | Simple name -> name - | _ -> - Fmt.failwith - "Internal error: invalid theory extension: %a" - print name - in - let extends = match extends.name with - | Simple name -> - begin match Util.th_ext_of_string name with - | Some extends -> extends - | None -> - Errors.typing_error (ThExtError name) aloc - end - | _ -> - Fmt.failwith - "Internal error: invalid base theory name: %a" - print extends - in - Some (name, extends) - | _ -> None - in - match List.filter_map theory sy_attrs with - | [] -> None - | [name, extends] -> Some (name, extends) - | _ -> - Fmt.failwith - "%a: Internal error: multiple theories." - DStd.Loc.fmt dloc - in - let decl_kind, assume = - match theory with - | Some (th_name, extends) -> - let axiom_kind = - if is_case_split then Util.Default else Util.Propagator - in - let th_assume name e = - let th_elt = { - Expr.th_name; - axiom_kind; - extends; - ax_form = e; - ax_name = name; - } in - C.ThAssume th_elt - in - E.Dtheory, th_assume - | None -> E.Daxiom, fun name e -> C.Assume (name, e, true) - in - let st_loc = dl_to_ael dloc_file loc in - let e = make_form name t st_loc ~decl_kind in - let st_decl = assume name e in - C.{ st_decl; st_loc } :: acc - - (* Function and predicate definitions *) - | { contents = `Defs defs; loc; _ } -> - (* For a mutually recursive definition, we have to add all the function - names in a row. *) - List.iter (fun (def : Typer_Pipe.def) -> - match def with - | `Term_def (_, ({ path; _ } as tcst), _, _, _) -> - let name_base = get_basename path in - let sy = Sy.name ~defined:true name_base in - Cache.store_sy tcst sy - | `Type_alias _ -> () - | `Instanceof _ -> - (* These statements are only used in models when completing a - polymorphic partially-defined bulitin and should not end up - here. *) - assert false - ) defs; - let append xs = List.append xs acc in - append @@ - List.filter_map (fun (def : Typer_Pipe.def) -> - match def with - | `Term_def ( _, ({ path; tags; _ } as tcst), tyvars, terml, body) -> - Cache.store_tyvl tyvars; - let st_loc = dl_to_ael dloc_file loc in - let name_base = get_basename path in - - let binders_set, defn = - let rty = dty_to_ty body.term_ty in - let binders_set, rev_args = - List.fold_left ( - fun (binders_set, acc) (DE.{ path; id_ty; _ } as tv) -> - let ty = dty_to_ty id_ty in - let sy = Sy.var (Var.of_string (get_basename path)) in - Cache.store_sy tv sy; - let e = E.mk_term sy [] ty in - SE.add e binders_set, e :: acc - ) (SE.empty, []) terml - in - let sy = Cache.find_sy tcst in - let e = E.mk_term sy (List.rev rev_args) rty in - binders_set, e - in - - let loc = st_loc in - - begin match DStd.Tag.get tags DE.Tags.predicate with - | Some () -> - let decl_kind = E.Dpredicate defn in - let ff = - mk_expr ~loc ~name_base - ~toplevel:false ~decl_kind body - in - let qb = E.mk_eq ~iff:true defn ff in - let binders = E.mk_binders binders_set in - let ff = - E.mk_forall name_base Loc.dummy binders [] qb ~toplevel:true - ~decl_kind - in - assert (Var.Map.is_empty (E.free_vars ff Var.Map.empty)); - let ff = E.purify_form ff in - let e = - if Ty.Svty.is_empty (E.free_type_vars ff) then ff - else - E.mk_forall name_base loc - Var.Map.empty [] ff ~toplevel:true ~decl_kind - in - Some C.{ st_decl = C.PredDef (e, name_base); st_loc } - | None -> - let decl_kind = E.Dfunction defn in - let ff = - mk_expr ~loc ~name_base - ~toplevel:false ~decl_kind body - in - let iff = Ty.equal (Expr.type_info defn) (Ty.Tbool) in - let qb = E.mk_eq ~iff defn ff in - let binders = E.mk_binders binders_set in - let ff = - E.mk_forall name_base Loc.dummy binders [] qb ~toplevel:true - ~decl_kind - in - assert (Var.Map.is_empty (E.free_vars ff Var.Map.empty)); - let ff = E.purify_form ff in - let e = - if Ty.Svty.is_empty (E.free_type_vars ff) then ff - else - E.mk_forall name_base loc - Var.Map.empty [] ff ~toplevel:true ~decl_kind - in - if Options.get_verbose () then - Format.eprintf "defining term of %a@." DE.Term.print body; - Some C.{ st_decl = C.Assume (name_base, e, true); st_loc } - end - | `Type_alias _ -> None - | `Instanceof _ -> - (* These statements are only used in models when completing a - polymorphic partially-defined bulitin and should not end up - here. *) - assert false - ) defs - - | {contents = `Decls [td]; _ } -> - begin match td with - | `Type_decl (td, _def) -> mk_ty_decl td - | `Term_decl td -> mk_term_decl td - end; - acc - - | {contents = `Decls dcl; _ } -> - let rec aux acc tdl = - (* for now, when acc has more than one element it is assumed that the - types are mutually recursive. Which is not necessarily the case. - But it doesn't affect the execution. - *) - match tdl with - | `Term_decl td :: tl -> - begin match acc with - | [] -> () - | [otd] -> mk_ty_decl otd - | _ -> mk_mr_ty_decls (List.rev acc) - end; - mk_term_decl td; - aux [] tl - - | `Type_decl (td, _def) :: tl -> - aux (td :: acc) tl - - | [] -> - begin match acc with - | [] -> () - | [otd] -> mk_ty_decl otd - | _ -> mk_mr_ty_decls (List.rev acc) - end - in - aux [] dcl; - acc - - | { contents = `Set_logic _ | `Set_info _ | `Get_info _ ; _ } -> acc - - | { contents = #Typer_Pipe.typechecked; _ } as stmt -> - (* TODO: - - Separate statements that should be ignored from unsupported - statements and throw exception or print a warning when an unsupported - statement is encountered. - *) - Printer.print_dbg ~header:true - "Ignoring statement: %a" Typer_Pipe.print stmt; - acc - in - aux acc stmt diff --git a/src/lib/frontend/d_cnf.mli b/src/lib/frontend/d_cnf.mli index cdb65f51f5..435a182ffd 100644 --- a/src/lib/frontend/d_cnf.mli +++ b/src/lib/frontend/d_cnf.mli @@ -44,6 +44,32 @@ val dty_to_ty : ?update:bool -> ?is_var:bool -> D_loop.DStd.Expr.ty -> Ty.t individually. *) +(** [ make_defs dlist loc ] + Transforms the dolmen definition list [dlist] into an Alt-Ergo definition. + Dolmen definitions can be: + - Definitions, that either are predicates (transformed in `PredDef) or + simple definitions (transformed in `Assume); + - Type aliases (filtered out); + - Statements used in models (they must not be in the input list, otherwise + this function fails). *) +val make_defs : + D_loop.Typer_Pipe.def list -> + Loc.t -> + [> `Assume of string * Expr.t | `PredDef of Expr.t * string ] list + +(** [mk_expr ~loc ~name_base ~toplevel ~decl_kind term] + + Builds an Alt-Ergo hashconsed expression from a dolmen term +*) +val make_expr : + ?loc:Loc.t -> + ?name_base:string -> + ?toplevel:bool -> + decl_kind:Expr.decl_kind -> D_loop.DStd.Expr.term -> Expr.t + +(** [make_form name term loc decl_kind] + Same as `make_expr`, but for formulas. It applies a purification step and + processes free variables by adding a forall quantifier. *) val make_form : string -> D_loop.DStd.Expr.term -> @@ -51,15 +77,38 @@ val make_form : decl_kind:Expr.decl_kind -> Expr.t -val make : - D_loop.DStd.Loc.file -> - Commands.sat_tdecl list -> - [< D_loop.Typer_Pipe.typechecked - | `Optimize of Dolmen.Std.Expr.term * bool - | `Goal of Dolmen.Std.Expr.term - | `Check of Dolmen.Std.Expr.term list - > `Hyp ] D_loop.Typer_Pipe.stmt -> - Commands.sat_tdecl list +(** Preprocesses the body of a goal by: + - removing the top-level universal quantifiers and considering their + quantified variables as uninsterpreted symbols. + - transforming a given formula: [a[1] -> a[2] -> ... -> a[n]] in which + the [a[i]]s are subformulas and [->] is a logical implication, to a set of + hypotheses [{a[1]; ...; a[n-1]}], and a goal [a[n]] whose validity is + verified by the solver. + If additional hypotheses are provided in [hyps], they are preprocessed and + added to the set of hypotheses in the same way as the left-hand side of + implications. In other words, [pp_query ~hyps:[h1; ...; hn] t] is the same + as [pp_query (h1 -> ... -> hn t)], but more convenient if the some + hypotheses are already separated from the goal. + Returns a list of hypotheses and the new goal body +*) +val pp_query : + ?hyps:D_loop.DStd.Expr.term list -> + D_loop.DStd.Expr.term -> + D_loop.DStd.Expr.term list * D_loop.DStd.Expr.term + +(** Registers the declarations in the cache. If there are more than one element + in the list, it is assumed they are mutually recursive (but if it is not the + case, it still work). *) +val cache_decls : D_loop.Typer_Pipe.decl list -> unit + +(* val make : + * D_loop.DStd.Loc.file -> + * Commands.sat_tdecl list -> + * [< D_loop.Typer_Pipe.typechecked + * | `Goal of Dolmen.Std.Expr.term + * | `Check of Dolmen.Std.Expr.term list + * > `Hyp ] D_loop.Typer_Pipe.stmt -> + * Commands.sat_tdecl list *) (** [make acc stmt] Makes one or more [Commands.sat_tdecl] from the type-checked statement [stmt] and appends them to [acc]. *) @@ -68,3 +117,5 @@ val builtins : Dolmen_loop.State.t -> D_loop.Typer.lang -> Dolmen_loop.Typer.T.builtin_symbols + +val is_pure_term : Expr.t -> bool diff --git a/src/lib/frontend/d_state_option.ml b/src/lib/frontend/d_state_option.ml index 3c5d807c7d..262e55a78a 100644 --- a/src/lib/frontend/d_state_option.ml +++ b/src/lib/frontend/d_state_option.ml @@ -32,6 +32,13 @@ module O = Options module State = D_loop.State module Typer = D_loop.Typer +type 'a hook = + 'a D_loop.State.key -> + old:'a -> + new_:'a -> + D_loop.Typer.state -> + D_loop.Typer.state + module type Accessor = sig (** The data saved in the state. *) type t @@ -45,34 +52,64 @@ module type S = sig include Accessor (** Sets the option on the dolmen state. *) - val set : t -> D_loop.Typer.state -> D_loop.Typer.state + val set : t -> Typer.state -> Typer.state (** Clears the option from the state. *) - val clear : D_loop.Typer.state -> D_loop.Typer.state + val clear : Typer.state -> Typer.state +end + +module type S_with_hooks = sig + include S + + val reset_hooks : unit -> unit + + val add_hook : t hook -> unit end let create_opt (type t) - ?(on_update=(fun _ _ -> Fun.id)) + ?on_update (key : string) - (get : unit -> t) : (module S with type t = t) = + (default_get : unit -> t) : (module S_with_hooks with type t = t) = (module struct type nonrec t = t + let on_update_base = + match on_update with + | None -> [] + | Some f -> [f] + + let on_update_list = ref on_update_base + let key = State.create_key ~pipe:"" key - let set opt st = - st - |> on_update key opt - |> State.set key opt + let apply_hooks ~old ~new_ st = + List.fold_left + (fun acc f -> f key ~old ~new_ acc) + st + !on_update_list let unsafe_get st = State.get key st - let clear st = State.update_opt key (fun _ -> None) st - let get st = try unsafe_get st with - | State.Key_not_found _ -> get () + | State.Key_not_found _ -> default_get () + + let set new_ st = + let old = get st in + let st = apply_hooks ~old ~new_ st in + State.set key new_ st + + let clear st = + let old = get st in + let new_ = default_get () in + st + |> apply_hooks ~old ~new_ + |> State.update_opt key (fun _ -> None) + + let reset_hooks () = on_update_list := on_update_base + + let add_hook h = on_update_list := h :: !on_update_list end) (* The current mode of the sat solver. Serves as a flag for some options that @@ -83,12 +120,12 @@ module Mode = (val (create_opt "start_mode") (fun _ -> Util.Start)) in start mode. *) let create_opt_only_start_mode (type t) - ?(on_update=(fun _ _ -> Fun.id)) + ?(on_update=(fun _ ~old:_ ~new_:_ -> Fun.id)) (key : string) - (get : unit -> t) : (module S with type t = t) = - let on_update k opt st = + (get : unit -> t) : (module S_with_hooks with type t = t) = + let on_update k ~old ~new_ st = match Mode.get st with - | Util.Start -> on_update k opt st + | Util.Start -> on_update k ~old ~new_ st | curr_mode -> Errors.invalid_set_option curr_mode key in create_opt ~on_update key get @@ -103,14 +140,28 @@ module Optimize = module ProduceAssignment = (val (create_opt_only_start_mode "produce_assignment" (fun _ -> false))) +module type Sat_solver_api = sig + module SAT : Sat_solver_sig.S + module FE : Frontend.S with type sat_env = SAT.t + + val env : FE.env +end + let get_sat_solver ?(sat = O.get_sat_solver ()) ?(no_th = O.get_no_theory ()) - () = + () : (module Sat_solver_api) = let module SatCont = (val (Sat_solver.get sat) : Sat_solver_sig.SatContainer) in let module TH = (val Sat_solver.get_theory ~no_th) in - (module SatCont.Make(TH) : Sat_solver_sig.S) + let module SAT : Sat_solver_sig.S = SatCont.Make(TH) in + let module FE : Frontend.S with type sat_env = SAT.t = Frontend.Make (SAT) in + (module struct + module SAT = SAT + module FE = FE + + let env = FE.init_env (Frontend.init_all_used_context ()) + end) module SatSolverModule = (val ( @@ -119,15 +170,15 @@ module SatSolverModule = (fun _ -> get_sat_solver ()))) let msatsolver = - let on_update _ sat st = - SatSolverModule.set (get_sat_solver ~sat ()) st + let on_update _ ~old:_ ~new_ st = + SatSolverModule.set (get_sat_solver ~sat:new_ ()) st in (create_opt_only_start_mode ~on_update "sat_solver" O.get_sat_solver) module SatSolver = (val msatsolver) let msteps = - let on_update _ sat st = Steps.set_steps_bound sat; st in + let on_update _ ~old:_ ~new_ st = Steps.set_steps_bound new_; st in (create_opt_only_start_mode ~on_update "steps_bound" O.get_steps_bound) module Steps = (val msteps) diff --git a/src/lib/frontend/d_state_option.mli b/src/lib/frontend/d_state_option.mli index 0d373c3c09..d0db1bd3de 100644 --- a/src/lib/frontend/d_state_option.mli +++ b/src/lib/frontend/d_state_option.mli @@ -32,6 +32,14 @@ an option that can be set, fetched et reset independently from the Options module, which is used as a static reference. *) +(** A hook which is called when an option is updated. *) +type 'a hook = + 'a D_loop.State.key -> + old:'a -> + new_:'a -> + D_loop.Typer.state -> + D_loop.Typer.state + module type Accessor = sig (** The data saved in the state. *) type t @@ -51,8 +59,18 @@ module type S = sig val clear : D_loop.Typer.state -> D_loop.Typer.state end +module type S_with_hooks = sig + include S + + (** Resets all hooks, except the one registered at initialization. *) + val reset_hooks : unit -> unit + + (** Adds a hook which is called during the update of the value. *) + val add_hook : t hook -> unit +end + (** The current mode of the solver. *) -module Mode : S with type t = Util.mode +module Mode : S_with_hooks with type t = Util.mode (** Options are divided in two categories: 1. options that can be updated anytime; @@ -71,9 +89,17 @@ module ProduceAssignment : S with type t = bool (** The Sat solver used. When set, updates the SatSolverModule defined below. *) module SatSolver : S with type t = Util.sat_solver +module type Sat_solver_api = sig + module SAT : Sat_solver_sig.S + + module FE : Frontend.S with type sat_env = SAT.t + + val env : FE.env +end + (** The Sat solver module used for the calculation. This option's value depends on SatSolver: when SatSolver is updated, this one also is. *) -module SatSolverModule : Accessor with type t = (module Sat_solver_sig.S) +module SatSolverModule : Accessor with type t = (module Sat_solver_api) (** Option for setting the max number of steps. Interfaces with the toplevel Steps module. diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index c18df4c219..bf2f374101 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -239,6 +239,8 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct expl = Explanation.empty } + let set_result env res = env.res <- res + let output_used_context g_name dep = if not (Options.get_js_mode ()) then begin let f = Options.get_used_context_file () in @@ -315,7 +317,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct ~max:n ~elt:() ~init:(env.res, env.expl) in SAT.pop env.sat_env n; - env.res <- res; + set_result env res; env.expl <- expl let internal_assume @@ -382,7 +384,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct in if get_debug_unsat_core () then check_produced_unsat_core expl; if get_save_used_context () then output_used_context n expl; - env.res <- `Unsat; + set_result env `Unsat; env.expl <- expl let internal_th_assume @@ -413,12 +415,13 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct let handle_sat_exn f ?loc x env = try f ?loc x env with - | SAT.Sat -> env.res <- `Sat + | SAT.Sat -> set_result env `Sat | SAT.Unsat expl -> - env.res <- `Unsat; + set_result env `Unsat; env.expl <- Ex.union expl env.expl - | SAT.I_dont_know -> - env.res <- `Unknown + | SAT.I_dont_know -> set_result env `Unknown + | Util.Step_limit_reached _ -> set_result env `Unknown + (* The SAT.Timeout exception is not catched. *) (* Wraps the function f to check if the step limit is reached (in which case, don't do anything), and then calls the function & catches the @@ -477,7 +480,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct (* This case should mainly occur when a query has a non-unsat result, so we want to print the status in this case. *) hook_on_status (Sat (d, env.sat_env)) (Steps.get_steps ()); - env.res <- `Sat + set_result env `Sat | SAT.Unsat expl' -> (* This case should mainly occur when a new assumption results in an unsat @@ -486,7 +489,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct let expl = Ex.union env.expl expl' in if get_debug_unsat_core () then check_produced_unsat_core expl; (* print_status (Inconsistent d) (Steps.get_steps ()); *) - env.res <- `Unsat; + set_result env `Unsat; env.expl <- expl | SAT.I_dont_know -> @@ -500,7 +503,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct hook_on_status status (Steps.get_steps ()); (* TODO: Is it an appropriate behaviour? *) (* if timeout != NoTimeout then raise Util.Timeout; *) - env.res <- `Unknown + set_result env `Unknown | Util.Timeout as e -> (* In this case, we obviously want to print the status, diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index 1ea043114e..5f22fd4ba8 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -169,6 +169,7 @@ module Make (Th : Theory.S) = struct ilevel : int; tbox : Th.t; unit_tbox : Th.t; (* theory env of facts at level 0 *) + tbox_stack: (Th.t * Th.t) Stack.t; (* For push and pop. TODO: pure version *) inst : Inst.t; heuristics : Heuristics.t ref; model_gen_phase : bool ref; @@ -1612,13 +1613,6 @@ module Make (Th : Theory.S) = struct raise e let push env to_push = - if Options.get_tableaux_cdcl () then - Errors.run_error - (Errors.Unsupported_feature - "Incremental commands are not implemented in \ - Tableaux(CDCL) solver ! \ - Please use the Tableaux or CDLC SAT solvers instead" - ); Util.loop ~f:(fun _n () acc -> let new_guard = E.fresh_name Ty.Tbool in @@ -1626,6 +1620,7 @@ module Make (Th : Theory.S) = struct let guards = ME.add new_guard (mk_gf new_guard "" true true,Ex.empty) acc.guards.guards in + Stack.push (env.tbox, env.unit_tbox) env.tbox_stack; {acc with guards = { acc.guards with current_guard = new_guard; @@ -1637,13 +1632,6 @@ module Make (Th : Theory.S) = struct ~init:env let pop env to_pop = - if Options.get_tableaux_cdcl () then - Errors.run_error - (Errors.Unsupported_feature - "Incremental commands are not implemented in \ - Tableaux(CDCL) solver ! \ - Please use the Tableaux or CDLC SAT solvers instead" - ); Util.loop ~f:(fun _n () acc -> let acc,guard_to_neg = restore_guards_and_refs acc in @@ -1654,6 +1642,17 @@ module Make (Th : Theory.S) = struct (mk_gf (E.neg guard_to_neg) "" true true,Ex.empty) acc.guards.guards in + let gamma = + (* If we made a check-sat and we want to work again on the + environment, we have to remove the guard from gamma. *) + match ME.find_opt guard_to_neg acc.gamma with + | None -> acc.gamma + | Some (_, _, dlvl, plvl) -> + ME.filter + (fun _ (_, _, dlvl', plvl') -> not (dlvl = dlvl' && plvl' >= plvl)) + acc.gamma + in + let tbox, unit_tbox = Stack.pop env.tbox_stack in acc.model_gen_phase := false; env.last_saved_model := None; {acc with inst; @@ -1661,7 +1660,11 @@ module Make (Th : Theory.S) = struct { acc.guards with current_guard = new_current_guard; guards = guards; - }}) + }; + gamma; + tbox; + unit_tbox; + }) ~max:to_pop ~elt:() ~init:env @@ -1673,12 +1676,10 @@ module Make (Th : Theory.S) = struct ME.fold (fun _g gf_guard_with_ex acc -> gf_guard_with_ex :: acc ) env.guards.guards [] in - if Options.get_tableaux_cdcl () then begin cdcl_assume false env guards_to_assume; cdcl_assume false env [gf,Ex.empty]; end; - let env = assume env guards_to_assume in let env = assume env [gf, Ex.empty] in let env = @@ -1829,6 +1830,7 @@ module Make (Th : Theory.S) = struct ilevel = 0; tbox = tbox; unit_tbox = tbox; + tbox_stack = Stack.create (); inst = inst; heuristics = ref (Heuristics.empty ()); model_gen_phase = ref false; diff --git a/src/lib/reasoners/fun_sat_frontend.ml b/src/lib/reasoners/fun_sat_frontend.ml index bad7812b0a..2d6da36307 100644 --- a/src/lib/reasoners/fun_sat_frontend.ml +++ b/src/lib/reasoners/fun_sat_frontend.ml @@ -39,6 +39,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let empty () = ref (FS.empty ()) + let cdcl_tab_push_pop_stack = Stack.create () + let empty_with_inst f = ref (FS.empty_with_inst f) let exn_handler f env = @@ -47,9 +49,36 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct | FS.Unsat expl -> raise (Unsat expl) | FS.I_dont_know e -> env := e; raise I_dont_know - let push t i = exn_handler (fun env -> t := FS.push env i) t - - let pop t i = exn_handler (fun env -> t := FS.pop env i) t + (* Push and pop are not implemented with get_tableaux_cdcl, so we have to + manually save and restore environments. *) + + let push_cdcl_tableaux t i = + assert (i > 0); + for _ = 1 to i do + Stack.push t cdcl_tab_push_pop_stack + done + + let pop_cdcl_tableaux _t i = + assert (i > 0); + let rec aux acc = function + | 1 -> acc + | i -> aux (Stack.pop cdcl_tab_push_pop_stack) (i - 1) + in + aux (Stack.pop cdcl_tab_push_pop_stack) i + + let push t i = exn_handler (fun env -> + if Options.get_tableaux_cdcl () then + push_cdcl_tableaux env i + else + t := FS.push env i + ) t + + let pop t i = exn_handler (fun env -> + if Options.get_tableaux_cdcl () then + t := pop_cdcl_tableaux env i + else + t := FS.pop env i + ) t let assume t g expl = exn_handler (fun env -> t := FS.assume env g expl) t diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml index db6e0d6ffe..0fcc318d98 100644 --- a/src/lib/reasoners/satml.ml +++ b/src/lib/reasoners/satml.ml @@ -116,6 +116,9 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct (* si vrai, les contraintes sont deja fausses *) mutable is_unsat : bool; + (* le nombre de fois que l'on a poussé un environnement unsat *) + mutable is_unsat_cpt : int; + mutable unsat_core : Atom.clause list option; (* clauses du probleme *) @@ -244,6 +247,8 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct { is_unsat = false; + is_unsat_cpt = 0; + unsat_core = None; clauses = Vec.make 0 Atom.dummy_clause; @@ -999,9 +1004,11 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct let print_aux fmt hc = Format.fprintf fmt "%a@," Atom.pr_clause hc + let is_unsat env : unit = env.is_unsat <- true + let report_b_unsat env linit = if not (Options.get_unsat_core ()) then begin - env.is_unsat <- true; + is_unsat env; env.unsat_core <- None; raise (Unsat None) end @@ -1043,7 +1050,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct let unsat_core = HUC.fold (fun c _ l -> c :: l) uc [] in Printer.print_dbg ~header:false "@[UNSAT_CORE:@ %a@]" (Printer.pp_list_no_space print_aux) unsat_core; - env.is_unsat <- true; + is_unsat env; let unsat_core = Some unsat_core in env.unsat_core <- unsat_core; raise (Unsat unsat_core) @@ -1051,7 +1058,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct let report_t_unsat env dep = if not (Options.get_unsat_core ()) then begin - env.is_unsat <- true; + is_unsat env; env.unsat_core <- None; raise (Unsat None) end @@ -1093,7 +1100,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct Printer.print_dbg ~header:false "@[T-UNSAT_CORE:@ %a@]" (Printer.pp_list_no_space print_aux) unsat_core; - env.is_unsat <- true; + is_unsat env; let unsat_core = Some unsat_core in env.unsat_core <- unsat_core; raise (Unsat unsat_core) @@ -1826,12 +1833,15 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct guard.is_guard <- true; guard.neg.is_guard <- false; cancel_until env env.next_dec_guard; - Vec.push env.increm_guards guard + Vec.push env.increm_guards guard; + env.is_unsat_cpt <- if env.is_unsat then env.is_unsat_cpt + 1 else 0 let pop env = (assert (not (Vec.is_empty env.increm_guards))); let g = Vec.last env.increm_guards in Vec.pop env.increm_guards; + env.is_unsat <- env.is_unsat_cpt <> 0; + env.is_unsat_cpt <- max 0 (env.is_unsat_cpt - 1); g.is_guard <- false; g.neg.is_guard <- false; assert (not g.var.na.is_true); (* atom not false *) diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index 7853e29d32..694591c261 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -1277,7 +1277,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct Inst.add_terms env.inst (E.max_ground_terms_rec_of_form gf.E.ff) gf; try - assert (SAT.decision_level env.satml == 0); + (* assert (SAT.decision_level env.satml == 0); *) let _updated = assume_aux ~dec_lvl:0 env [gf] in let max_t = max_term_depth_in_sat env in env.inst <- Inst.register_max_term_depth env.inst max_t; @@ -1303,7 +1303,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let assume env gf _dep = (* dep currently not used. No unsat-cores in satML yet *) - assert (SAT.decision_level env.satml == 0); + (* assert (SAT.decision_level env.satml == 0); *) try ignore (assume_aux ~dec_lvl:0 env [add_guard env gf]) with | IUnsat (_env, dep) -> raise (Unsat dep) | Util.Timeout -> diff --git a/tests/cram.t/postlude.smt2 b/tests/cram.t/postlude.smt2 index b709d1db6e..e5e0009218 100644 --- a/tests/cram.t/postlude.smt2 +++ b/tests/cram.t/postlude.smt2 @@ -22,8 +22,8 @@ (assert (not (my_leq (f x) x))) (check-sat) - ; Now that x > 10 is known, the trigger should apply - (assert (> x 10)) + ; Now that f x > 10 is known, the trigger should apply + (assert (> (f x) 10)) (check-sat) (pop 1) diff --git a/tests/cram.t/prelude.ae b/tests/cram.t/prelude.ae index 25143cfb95..af49416e00 100644 --- a/tests/cram.t/prelude.ae +++ b/tests/cram.t/prelude.ae @@ -10,5 +10,5 @@ logic f : real -> real theory F_theory extends FPA = axiom f_triggers : - forall x : real [ int_floor(x), x in ]0., ?] ]. my_leq(f(x), x) + forall x: real [ f(x), f(x) in ]0., ?] ]. my_leq(f(x), x) end diff --git a/tests/issues/926.models.smt2 b/tests/issues/926.models.smt2 index 2c9860dae8..ead54d8246 100644 --- a/tests/issues/926.models.smt2 +++ b/tests/issues/926.models.smt2 @@ -1,5 +1,5 @@ -(set-logic ALL) (set-option :produce-models true) +(set-logic ALL) (declare-const x1 Int) (declare-const x2 Int) (declare-const y1 Real) diff --git a/tests/smtlib/testfile-get-info1.dolmen.expected b/tests/smtlib/testfile-get-info1.dolmen.expected index f3993ae214..d206212dc2 100644 --- a/tests/smtlib/testfile-get-info1.dolmen.expected +++ b/tests/smtlib/testfile-get-info1.dolmen.expected @@ -1,7 +1,7 @@ unknown ( - :steps 7) + :steps 10) unsupported