From 9cf1828520f0554512f5c71f236f77a2cb4fda13 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Fri, 1 Dec 2023 16:13:08 +0100 Subject: [PATCH 01/17] First version of full incremental solving loop --- src/bin/common/solving_loop.ml | 528 +++++++++++++---- src/lib/frontend/d_cnf.ml | 548 +++++++----------- src/lib/frontend/d_cnf.mli | 61 +- 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 | 52 +- src/lib/reasoners/fun_sat_frontend.ml | 73 ++- src/lib/reasoners/satml.ml | 45 +- src/lib/reasoners/satml.mli | 3 + src/lib/reasoners/satml_frontend.ml | 19 +- tests/adts/simple_1.ae | 4 +- tests/adts/simple_1.expected | 2 - 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 +- 17 files changed, 925 insertions(+), 562 deletions(-) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index cfd5dea0d..5e6628189 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -104,7 +104,7 @@ 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 @@ -121,13 +121,59 @@ 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_sat_status () = + match Options.get_status () with + | Status_Unsat -> + recoverable_error + "This file is known to be Unsat but Alt-Ergo return Sat"; + | _ -> () + +let check_unsat_status () = + match Options.get_status () with + | Status_Unsat -> + recoverable_error + "This file is known to be Sat but Alt-Ergo return Unsat"; + | _ -> () + +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_sat_status (); + | 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_unsat_status () + | Unknown _ -> + Printer.print_status_unknown ~validity_mode + (Some loc) (Some time) (Some steps) (Some goal_name); exception StopProcessDecl @@ -199,7 +245,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. *) @@ -356,6 +402,41 @@ let main () = State.create_key ~pipe:"" "is_incremental" in + (* Set to true when a query is performed, states for the following SMT + instructions that they are working on an environment in which some formulae + have been decided and must be reverted back to the one before the check-sat + before starting to assert again. *) + let is_decision_env : bool State.key = + State.create_key ~pipe:"" "is_decision_env" + in + + (* Before each query, we push the current environment. This allows to keep a + fresh one for the next assertions. *) + let internal_push st = + if State.get is_decision_env st then + (* We already performed a check-sat *) + st + else + begin + let module Api = (val (DO.SatSolverModule.get st)) in + Api.FE.push 1 Api.env; + State.set is_decision_env true st + end + in + + (* The pop corresponding to the previous push. It is applied everytime the + mode goes from Sat/Unsat to Assert. *) + let internal_pop st = + if State.get is_decision_env st then + begin + let module Api = (val (DO.SatSolverModule.get st)) in + Api.FE.pop 1 Api.env; + State.set is_decision_env false st + end + else + st + in + let set_steps_bound i st = try DO.Steps.set i st with Invalid_argument _ -> (* Raised by Steps.set_steps_bound *) @@ -425,7 +506,7 @@ let main () = in let set_partial_model_and_mode solve_res st = match solve_res with - | Unsat -> + | Unsat _ -> set_mode Unsat st | Unknown None -> set_mode Sat st @@ -520,6 +601,7 @@ let main () = |> State.set partial_model_key None |> State.set named_terms Util.MS.empty |> State.set incremental_depth 0 + |> State.set is_decision_env false |> DO.init |> State.init ~debug ~report_style ~reports ~max_warn ~time_limit ~size_limit ~response_file @@ -530,6 +612,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 new_ with + | Assert -> internal_pop st + | _ -> st + ) + in let print_wrn_opt ~name loc ty value = warning "%a The option %s expects a %s, got %a" @@ -688,61 +784,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.mk_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.mk_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)" @@ -840,26 +954,247 @@ 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 + let st = internal_pop 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 + | `Unknown -> + (* The environment did not conclude yet, or concluded with SAT. We + add additional constraints which may change this result. *) + 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 + (* 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 _) -> @@ -867,52 +1202,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 = @@ -949,9 +1249,11 @@ 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 + |> State.set is_decision_env false |> DO.Mode.clear |> DO.Optimize.clear |> DO.ProduceAssignment.clear @@ -996,32 +1298,26 @@ let main () = | {contents = `Other (custom, args); loc; _} -> handle_custom_statement loc custom args st + | {contents = `Pop n; loc; _} -> + let module Api = (val DO.SatSolverModule.get st) in + let dloc_file = (State.get State.logic_file st).loc in + Api.FE.pop ~loc:(dl_to_ael dloc_file loc) n Api.env; + st + |> State.set incremental_depth (State.get incremental_depth st - n) + |> set_mode Assert + + | {contents = `Push n; loc; _} -> + let module Api = (val DO.SatSolverModule.get st) in + let dloc_file = (State.get State.logic_file st).loc in + Api.FE.push ~loc:(dl_to_ael dloc_file loc) n Api.env; + st + |> State.set incremental_depth (State.get incremental_depth st + n) + |> set_mode Assert + | td -> - let st = - match td.contents with - | `Pop n -> - st - |> State.set incremental_depth (State.get incremental_depth st - n) - |> set_mode Assert - | `Push n -> - st - |> State.set incremental_depth (State.get incremental_depth st + n) - |> set_mode Assert - | _ -> 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 2d45eb98c..57014fab7 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/src/lib/frontend/d_cnf.ml @@ -176,6 +176,8 @@ type _ DStd.Builtin.t += | Integer_round | Abs_real | Sqrt_real + | Int2BV of int + | BV2Nat of int | Sqrt_real_default | Sqrt_real_excess | Ceiling_to_int of [ `Real ] @@ -211,11 +213,10 @@ let builtin_enum = function let add_cstrs map = List.fold_left (fun map ((c : DE.term_cst), _) -> let name = get_basename c.path in - DStd.Id.Map.add { name = DStd.Name.simple name; ns = Term } - (fun env _ -> - builtin_term @@ - Dolmen_type.Base.term_app_cst - (module Dl.Typer.T) env c) map) + DStd.Id.Map.add { name = DStd.Name.simple name; ns = Term } (fun env _ -> + builtin_term @@ + Dolmen_type.Base.term_app_cst + (module Dl.Typer.T) env c) map) map cstrs in Cache.store_ty (DE.Ty.Const.hash ty_cst) ty_; @@ -233,19 +234,63 @@ let fpa_rounding_mode, rounding_modes, add_rounding_modes = module Const = struct open DE + let bv2nat = + with_cache (fun n -> + let name = "bv2nat" in + Id.mk ~name ~builtin:(BV2Nat n) + (DStd.Path.global name) Ty.(arrow [bitv n] int)) + + let int2bv = + with_cache (fun n -> + let name = "int2bv" in + Id.mk ~name ~builtin:(Int2BV n) + (DStd.Path.global name) Ty.(arrow [int] (bitv n))) + let smt_round = with_cache (fun (n, m) -> let name = "ae.round" in - DE.Id.mk + Id.mk ~name ~builtin:(AERound (n, m)) (DStd.Path.global name) Ty.(arrow [fpa_rounding_mode; real] real)) end +let bv2nat t = + let n = + match DT.view (DE.Term.ty t) with + | `Bitv n -> n + | _ -> raise (DE.Term.Wrong_type (t, DT.bitv 0)) + in + DE.Term.apply_cst (Const.bv2nat n) [] [t] + +let int2bv n t = + DE.Term.apply_cst (Const.int2bv n) [] [t] + let smt_round n m rm t = DE.Term.apply_cst (Const.smt_round (n, m)) [] [rm; t] +let bv_builtins env s = + let term_app1 f = + Dl.Typer.T.builtin_term @@ + Dolmen_type.Base.term_app1 (module Dl.Typer.T) env s f + in + match s with + | Dl.Typer.T.Id { + ns = Term ; + name = Simple "bv2nat" } -> + term_app1 bv2nat + | Id { + ns = Term ; + name = Indexed { + basename = "int2bv" ; + indexes = [ n ] } } -> + begin match int_of_string n with + | n -> term_app1 (int2bv n) + | exception Failure _ -> `Not_found + end + | _ -> `Not_found + (** Takes a dolmen identifier [id] and injects it in Alt-Ergo's registered identifiers. It transforms "fpa_rounding_mode", the Alt-Ergo builtin type into the SMT2 @@ -447,17 +492,20 @@ let smt_fpa_builtins = end | _ -> `Not_found +(** Concatenation of builtins handlers. *) +let (++) bt1 bt2 = + fun a b -> + match bt1 a b with + | `Not_found -> bt2 a b + | res -> res + let builtins = fun _st (lang : Typer.lang) -> match lang with | `Logic Alt_ergo -> ae_fpa_builtins - | `Logic (Smtlib2 _) -> smt_fpa_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 () @@ -649,14 +697,14 @@ let mk_term_decl ({ id_ty; path; tags; _ } as tcst: DE.term_cst) = in Cache.store_sy tcst sy; (* Adding polymorphic types to the cache. *) - Cache.store_ty_vars id_ty; - let arg_tys, ret_ty = - match DT.view id_ty with - | `Arrow (arg_tys, ret_ty) -> - List.map dty_to_ty arg_tys, dty_to_ty ret_ty - | _ -> [], dty_to_ty id_ty - in - (Hstring.make name, arg_tys, ret_ty) + Cache.store_ty_vars id_ty(* ; + * let arg_tys, ret_ty = + * match DT.view id_ty with + * | `Arrow (arg_tys, ret_ty) -> + * List.map dty_to_ty arg_tys, dty_to_ty ret_ty + * | _ -> [], dty_to_ty id_ty + * in + * (Hstring.make name, arg_tys, ret_ty) *) (** Handles the definitions of a list of mutually recursive types. - If one of the types is an ADT, the ADTs that have only one case are @@ -1407,8 +1455,8 @@ let rec mk_expr | Integer_round, _ -> op Integer_round | Abs_real, _ -> op Abs_real | Sqrt_real, _ -> op Sqrt_real - | B.Bitv_of_int { n }, _ -> op (Int2BV n) - | B.Bitv_to_nat { n = _ }, _ -> op BV2Nat + | Int2BV n, _ -> op (Int2BV n) + | BV2Nat _, _ -> op BV2Nat | Sqrt_real_default, _ -> op Sqrt_real_default | Sqrt_real_excess, _ -> op Sqrt_real_excess | B.Abs, _ -> op Abs_int @@ -1748,6 +1796,98 @@ 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 = + 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 (`PredDef (e, name_base)) + | 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 (`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 @@ -1758,6 +1898,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 = @@ -1766,333 +1942,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 = DStd.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 = DStd.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]; loc; _ } -> - begin match td with - | `Type_decl (td, _def) -> - mk_ty_decl td; - acc - - | `Term_decl td -> - let st_loc = dl_to_ael dloc_file loc in - C.{ st_decl = Decl (mk_term_decl td); st_loc } :: acc - end - - | {contents = `Decls dcl; loc; _ } -> - let rec aux ty_decls tdl acc = - (* 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 ty_decls with - | [] -> () - | [otd] -> mk_ty_decl otd - | _ -> mk_mr_ty_decls (List.rev ty_decls) - end; - let st_loc = dl_to_ael dloc_file loc in - C.{ st_decl = Decl (mk_term_decl td); st_loc } :: aux [] tl acc - - | `Type_decl (td, _def) :: tl -> - aux (td :: ty_decls) tl acc - - | [] -> - begin - let () = - match ty_decls with - | [] -> () - | [otd] -> mk_ty_decl otd - | _ -> mk_mr_ty_decls (List.rev ty_decls) - in - 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 cdb65f51f..772153c4e 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 + +(** [make_expr ~loc ~name_base ~toplevel ~decl_kind term] + + Builds an Alt-Ergo hashconsed expression from a dolmen term +*) +val mk_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,20 +77,33 @@ 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 -(** [make acc stmt] Makes one or more [Commands.sat_tdecl] from the - type-checked statement [stmt] and appends them to [acc]. +(** 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 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 3c5d807c7..262e55a78 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 0d373c3c0..d0db1bd3d 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 bf5738549..b5ebb0c18 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 @@ -322,7 +324,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 @@ -389,7 +391,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 @@ -420,12 +422,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 @@ -485,7 +488,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 @@ -494,7 +497,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 -> @@ -508,7 +511,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 7ac10f3de..22bd813d6 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -168,6 +168,7 @@ module Make (Th : Theory.S) = struct plevel : int; ilevel : int; tbox : Th.t; + tbox_stack: Th.t Stack.t; (* Pushed theory envs (TODO: pure version) *) unit_tbox : Th.t; (* theory env of facts at level 0 *) inst : Inst.t; heuristics : Heuristics.t ref; @@ -1625,13 +1626,15 @@ module Make (Th : Theory.S) = struct env 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" - ); + (* It does not work with Tableaux(CDCL); right now it is (unsoundly) + handled by fun_sat_frontend but we should fix it. *) + (* 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 @@ -1639,6 +1642,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.tbox_stack; Stack.push !(env.declare_top) env.declare_tail; {acc with guards = { acc.guards with @@ -1651,13 +1655,15 @@ 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" - ); + (* It does not work with Tableaux(CDCL); right now it is (unsoundly) + handled by fun_sat_frontend but we should fix it. *) + (* 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 @@ -1668,6 +1674,18 @@ 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 = Stack.pop env.tbox_stack in acc.model_gen_phase := false; env.last_saved_model := None; let () = @@ -1680,7 +1698,10 @@ module Make (Th : Theory.S) = struct { acc.guards with current_guard = new_current_guard; guards = guards; - }}) + }; + gamma; + tbox; + }) ~max:to_pop ~elt:() ~init:env @@ -1832,6 +1853,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 ef5c7e921..9a22fa8a8 100644 --- a/src/lib/reasoners/fun_sat_frontend.ml +++ b/src/lib/reasoners/fun_sat_frontend.ml @@ -35,33 +35,70 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct module FS = Fun_sat.Make(Th) - type t = FS.t ref + type t = { + mutable fs_env: FS.t; + fs_env_stack: FS.t Stack.t + } - let empty ?selector () = ref (FS.empty ?selector ()) + let internal_empty fs_env = { + fs_env; + fs_env_stack = Stack.create () + } + + let empty ?selector () = internal_empty (FS.empty ?selector ()) let exn_handler f env = - try f !env with - | FS.Sat e -> env := e; raise Sat + try f env with + | FS.Sat e -> env.fs_env <- e; raise Sat | FS.Unsat expl -> raise (Unsat expl) - | FS.I_dont_know e -> env := e; raise I_dont_know - - let declare t id = - t := FS.declare !t id + | FS.I_dont_know e -> env.fs_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 - - let assume t g expl = exn_handler (fun env -> t := FS.assume env g expl) t + let declare t id = + t.fs_env <- FS.declare t.fs_env id + + (* 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.fs_env t.fs_env_stack + done + + let pop_cdcl_tableaux t i = + assert (i > 0); + let rec aux fs_env = function + | 1 -> t.fs_env <- fs_env + | i -> aux (Stack.pop t.fs_env_stack) (i - 1) + in + aux (Stack.pop t.fs_env_stack) i + + let push t i = exn_handler (fun t -> + if Options.get_tableaux_cdcl () then + push_cdcl_tableaux t i + else + t.fs_env <- FS.push t.fs_env i + ) t + + let pop t i = exn_handler (fun env -> + if Options.get_tableaux_cdcl () then + pop_cdcl_tableaux env i + else + t.fs_env <- FS.pop t.fs_env i + ) t + + let assume t g expl = + exn_handler (fun t -> t.fs_env <- FS.assume t.fs_env g expl) t let assume_th_elt t th expl = - exn_handler (fun env -> t := FS.assume_th_elt env th expl) t + exn_handler (fun t -> t.fs_env <- FS.assume_th_elt t.fs_env th expl) t let pred_def t expr n expl loc = - exn_handler (fun env -> t := FS.pred_def env expr n expl loc) t + exn_handler (fun t -> t.fs_env <- FS.pred_def t.fs_env expr n expl loc) t let unsat t g = - exn_handler (fun env -> FS.unsat env g) t + exn_handler (fun t -> FS.unsat t.fs_env g) t let optimize _env ~is_max:_ _obj = raise (Util.Not_implemented "optimization is not supported by FunSAT.") @@ -70,11 +107,11 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let reinit_ctx = FS.reinit_ctx - let get_model t = FS.get_model !t + let get_model t = FS.get_model t.fs_env - let get_unknown_reason t = FS.get_unknown_reason !t + let get_unknown_reason t = FS.get_unknown_reason t.fs_env - let get_value t expr = FS.get_value !t expr + let get_value t expr = FS.get_value t.fs_env expr let get_objectives _env = raise (Util.Not_implemented "optimization is not supported by FunSAT.") diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml index 9b89753e0..1424b3248 100644 --- a/src/lib/reasoners/satml.ml +++ b/src/lib/reasoners/satml.ml @@ -120,6 +120,7 @@ module type SAT_ML = sig val create : Atom.hcons_env -> t val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> unit + val push_level : t -> int val decision_level : t -> int val cancel_until : t -> int -> unit @@ -175,6 +176,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 *) @@ -278,6 +282,8 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct mutable tenv_queue : Th.t Vec.t; + mutable unit_tenv_queue : Th.t Vec.t; + mutable tatoms_queue : Atom.atom Queue.t; (** Queue of atoms that have been added to the [trail] through either decision or boolean propagation, but have not been otherwise processed @@ -425,6 +431,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 ~dummy:Atom.dummy_clause; @@ -500,6 +508,8 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct tenv_queue = Vec.make 100 ~dummy:(Th.empty()); + unit_tenv_queue = Vec.make 100 ~dummy:(Th.empty()); + tatoms_queue = Queue.create (); th_tableaux = Queue.create (); @@ -562,6 +572,8 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct env.clause_inc <- env.clause_inc *. 1e-20 end + let push_level env = Vec.size env.increm_guards + let decision_level env = Vec.size env.trail_lim let nb_choices env = env.nchoices @@ -1026,10 +1038,20 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct (fun acc (ta : Atom.atom) -> assert (ta.is_true); assert (ta.var.level >= 0); - if ta.var.level = 0 then begin + if ta.var.level <= Vec.size env.increm_guards then begin incr nb_f; - (ta.lit, Th_util.Other, Ex.empty, 0, env.cpt_current_propagations) - :: acc + let ex = + if ta.var.level = 0 then Ex.empty else + let d = + Vec.get env.trail (Vec.get env.trail_lim (ta.var.level - 1)) + in + Ex.singleton (Ex.Literal d) + in + (ta.lit, + Th_util.Other, + ex, + ta.var.level, + env.cpt_current_propagations) :: acc end else acc )[] lazy_q @@ -1214,9 +1236,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 @@ -1256,7 +1280,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) @@ -1264,7 +1288,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 @@ -1305,7 +1329,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) @@ -2172,11 +2196,16 @@ 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; + Vec.push env.unit_tenv_queue env.unit_tenv; + 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.pop env.increm_guards in + env.is_unsat <- env.is_unsat_cpt <> 0; + env.is_unsat_cpt <- max 0 (env.is_unsat_cpt - 1); + env.unit_tenv <- Vec.pop env.unit_tenv_queue; 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.mli b/src/lib/reasoners/satml.mli index 9dac0344c..19c9eb9dd 100644 --- a/src/lib/reasoners/satml.mli +++ b/src/lib/reasoners/satml.mli @@ -77,6 +77,9 @@ module type SAT_ML = sig val create : Atom.hcons_env -> t val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> unit + (** Returns the push/pop depth of the current analysis + (i.e., #push - #pop) *) + val push_level : t -> int val decision_level : t -> int val cancel_until : t -> int -> unit diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index 2749d7ce1..94412a279 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -459,6 +459,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let pred_def env f name dep _loc = (* dep currently not used. No unsat-cores in satML yet *) Debug.pred_def f; + assert (SAT.decision_level env.satml <= SAT.push_level env.satml); let guard = env.guards.current_guard in env.inst <- Inst.add_predicate env.inst ~guard ~name (mk_gf f) dep @@ -1309,8 +1310,12 @@ 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); - let _updated = assume_aux ~dec_lvl:0 env [gf] in + let _updated = + assume_aux + ~dec_lvl:(SAT.decision_level env.satml) + env + [gf] + in let max_t = max_term_depth_in_sat env in env.inst <- Inst.register_max_term_depth env.inst max_t; unsat_rec_prem env ~first_call:true; @@ -1329,8 +1334,14 @@ 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); - try ignore (assume_aux ~dec_lvl:0 env [add_guard env gf]) + assert (SAT.decision_level env.satml <= SAT.push_level env.satml); + try + let _ : bool = + assume_aux + ~dec_lvl:(SAT.decision_level env.satml) + env + [add_guard env gf] + in () with | IUnsat (_env, dep) -> raise (Unsat dep) | Util.Timeout -> (* don't attempt to compute a model if timeout before diff --git a/tests/adts/simple_1.ae b/tests/adts/simple_1.ae index cc82d2f24..fa271f926 100644 --- a/tests/adts/simple_1.ae +++ b/tests/adts/simple_1.ae @@ -49,13 +49,15 @@ goal g_valid_4_2: e ? B -> false -(**) +(* Isse 1008: this goal fail when encapsulated by a push/pop. *) +(* goal g_valid_5_1: forall n : int. n >= 0 -> (* just here for E-matching *) not (e ? A) -> not (e ? B) -> exists x : int[x]. e = C(x) +*) goal g_valid_5_2: forall n : int. diff --git a/tests/adts/simple_1.expected b/tests/adts/simple_1.expected index f8919c465..f97cc55c7 100644 --- a/tests/adts/simple_1.expected +++ b/tests/adts/simple_1.expected @@ -20,5 +20,3 @@ unsat unsat unsat - -unsat diff --git a/tests/cram.t/postlude.smt2 b/tests/cram.t/postlude.smt2 index b709d1db6..e5e000921 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 25143cfb9..af49416e0 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 2c9860dae..ead54d824 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 f3993ae21..8241c6580 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 11) unsupported From 6790c68c34bff43f24c12017895b32e3f2752c6f Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Fri, 22 Mar 2024 13:33:39 +0100 Subject: [PATCH 02/17] Update tests --- tests/smtlib/testfile-steps-bound2.dolmen.smt2 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/smtlib/testfile-steps-bound2.dolmen.smt2 b/tests/smtlib/testfile-steps-bound2.dolmen.smt2 index 3d578cf45..171dbafe7 100644 --- a/tests/smtlib/testfile-steps-bound2.dolmen.smt2 +++ b/tests/smtlib/testfile-steps-bound2.dolmen.smt2 @@ -1,4 +1,4 @@ -(set-option :steps-bound 2) +(set-option :steps-bound 4) (set-logic ALL) (declare-const x Int) From 2fd830334a6c00c31be1532c223ba68b01e48718 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Fri, 22 Mar 2024 18:06:59 +0100 Subject: [PATCH 03/17] Interleaving full imperative and partial imperative modes --- src/bin/common/dune | 3 +- src/bin/common/parse_command.ml | 8 ++- src/bin/common/solving_loop.ml | 103 +++++++++++++++++++++++++++----- src/lib/util/options.ml | 3 + src/lib/util/options.mli | 7 +++ 5 files changed, 107 insertions(+), 17 deletions(-) diff --git a/src/bin/common/dune b/src/bin/common/dune index 307f982a5..8cc2a2b71 100644 --- a/src/bin/common/dune +++ b/src/bin/common/dune @@ -21,7 +21,8 @@ Parse_command Input_frontend Signals_profiling - Solving_loop) + Solving_loop + Solving_loop_imperative) ) (generate_sites_module diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml index 5e799b7df..1b5103aa7 100644 --- a/src/bin/common/parse_command.ml +++ b/src/bin/common/parse_command.ml @@ -303,7 +303,7 @@ let mk_context_opt replay replay_all_used_context replay_used_context let mk_execution_opt input_format parse_only () preludes no_locs_in_answers colors_in_output no_headers_in_output no_formatting_in_output no_forced_flush_in_output pretty_output - type_only type_smt2 + type_only type_smt2 imperative_mode = let answers_with_loc = not no_locs_in_answers in let output_with_colors = colors_in_output || pretty_output in @@ -321,6 +321,7 @@ let mk_execution_opt input_format parse_only () set_type_only type_only; set_type_smt2 type_smt2; set_preludes preludes; + set_imperative_mode imperative_mode; `Ok() let mk_internal_opt @@ -744,12 +745,15 @@ let parse_execution_opt = let doc = "Stop after SMT2 typing." in Arg.(value & flag & info ["type-smt2"] ~docs ~doc) in + let imperative_smt = + let doc = "Starts Alt-Ergo in incremental mode" in + Arg.(value & flag & info ["incremental-mode"] ~docs ~doc) in Term.(ret (const mk_execution_opt $ input_format $ parse_only $ parsers $ preludes $ no_locs_in_answers $ colors_in_output $ no_headers_in_output $ no_formatting_in_output $ no_forced_flush_in_output $ - pretty_output $ type_only $ type_smt2 + pretty_output $ type_only $ type_smt2 $ imperative_smt )) let parse_halt_opt = diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 5e6628189..cf3624835 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -121,6 +121,8 @@ let add_if_named names. *) acc +type stmt = Typer_Pipe.typechecked D_loop.Typer_Pipe.stmt + (** 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)) @@ -1139,7 +1141,20 @@ let main () = set_partial_model_and_mode solve_res st in - let handle_stmt : + let handle_reset st = + let () = Steps.reset_steps () in + st + |> State.set partial_model_key None + |> State.set solver_ctx_key empty_solver_ctx + |> State.set is_decision_env false + |> DO.Mode.clear + |> DO.Optimize.clear + |> DO.ProduceAssignment.clear + |> DO.init + |> State.set named_terms Util.MS.empty + in + + let handle_stmt_full_incremental : Frontend.used_context -> State.t -> [< Typer_Pipe.typechecked | `Check of 'a ] D_loop.Typer_Pipe.stmt -> @@ -1248,17 +1263,7 @@ let main () = st end - | {contents = `Reset; _} -> - let () = Steps.reset_steps () in - st - |> State.set partial_model_key None - |> State.set solver_ctx_key empty_solver_ctx - |> State.set is_decision_env false - |> DO.Mode.clear - |> DO.Optimize.clear - |> DO.ProduceAssignment.clear - |> DO.init - |> State.set named_terms Util.MS.empty + | {contents = `Reset; _} -> handle_reset st | {contents = `Exit; _} -> raise Exit @@ -1319,16 +1324,86 @@ let main () = "Ignoring statement: %a" Typer_Pipe.print td; st in - let handle_stmts all_context st l = + + let handle_stmts_full_incremental all_context st l = let rec aux named_map st = function | [] -> State.set named_terms named_map st | stmt :: tl -> - let st = handle_stmt all_context st stmt in + let st = handle_stmt_full_incremental all_context st stmt in let named_map = add_if_named ~acc:named_map stmt in aux named_map st tl in aux (State.get named_terms st) st l in + + let current_path_key : stmt list State.key = + State.create_key ~pipe:"" "current_path" + in + let pushed_paths_key : stmt list Vec.t State.key = + State.create_key ~pipe:"" "pushed_paths" + in + let state_get key ~default st = + try State.get key st with State.Key_not_found _ -> default + in + let get_current_path = state_get current_path_key ~default:[] in + let get_pushed_paths = state_get pushed_paths_key ~default:(Vec.create ~dummy:(Obj.magic 0)) + in + let handle_stmt_pop_reinit all_context st l = + let rec aux named_map st = function + | [] -> State.set named_terms named_map st + | (stmt: stmt) :: tl -> + begin + let current_path = get_current_path st in + match stmt with + | {contents = `Push n; _} -> + let pushed_paths = get_pushed_paths st in + for _ = 0 to n - 1 do + Vec.push pushed_paths current_path + done; + aux named_map st tl + | {contents = `Pop n; _} -> + let pushed_paths = get_pushed_paths st in + Format.eprintf "Vec size: %i@." pushed_paths.sz; + let rec pop_until until res = + if until = 0 then res else pop_until (until - 1) (Vec.pop pushed_paths) + in + let prefix = pop_until (n - 1) (Vec.pop pushed_paths) in + let st = handle_reset st in + let whole_path = List.rev_append prefix tl in + Format.eprintf "Restarting with %i instructions@." (List.length whole_path); + aux (State.get named_terms st) st whole_path + | {contents; _ } -> + let st = + let new_current_path = + match contents with + | `Clause _ + | `Decls _ + | `Defs _ + | `Hyp _ + | `Other _ + | `Reset + | `Reset_assertions + | `Set_info _ + | `Set_logic _ + | `Set_option _ -> stmt :: current_path + | _ -> current_path + in + State.set current_path_key new_current_path st + in + let st = handle_stmt_full_incremental all_context st stmt in + let named_map = add_if_named ~acc:named_map stmt in + aux named_map st tl + end + in + aux (State.get named_terms st) st l + in + let handle_stmts all_context st l = + begin + if Options.get_imperative_mode () + then handle_stmts_full_incremental + else handle_stmt_pop_reinit + end all_context st l + in let d_fe filename = let logic_file, st = mk_state filename in let () = diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml index 9bb1764e9..16cbc2a97 100644 --- a/src/lib/util/options.ml +++ b/src/lib/util/options.ml @@ -272,6 +272,7 @@ let preludes = ref [] let theory_preludes = ref Theories.default_preludes let type_only = ref false let type_smt2 = ref false +let imperative_mode = ref false let set_answers_with_loc b = answers_with_loc := b let set_output_with_colors b = output_with_colors := b @@ -286,6 +287,7 @@ let set_preludes p = preludes := p let set_theory_preludes t = theory_preludes := t let set_type_only b = type_only := b let set_type_smt2 b = type_smt2 := b +let set_imperative_mode i = imperative_mode := i let get_answers_with_locs () = !answers_with_loc let get_output_with_colors () = !output_with_colors @@ -299,6 +301,7 @@ let get_preludes () = !preludes let get_theory_preludes () = !theory_preludes let get_type_only () = !type_only let get_type_smt2 () = !type_smt2 +let get_imperative_mode () = !imperative_mode (** Internal options *) diff --git a/src/lib/util/options.mli b/src/lib/util/options.mli index 9bbbf965c..c5cbcd3d7 100644 --- a/src/lib/util/options.mli +++ b/src/lib/util/options.mli @@ -298,6 +298,9 @@ val set_triggers_var : bool -> unit (** Set [type_smt2] accessible with {!val:get_type_smt2} *) val set_type_smt2 : bool -> unit +(** Set [type_smt2] accessible with {!val:get_type_smt2} *) +val set_imperative_mode : bool -> unit + (** Set [unsat_core] accessible with {!val:get_unsat_core} *) val set_unsat_core : bool -> unit @@ -660,6 +663,10 @@ val get_type_only : unit -> bool val get_type_smt2 : unit -> bool (** Default to [false] *) +(** [true] if the program shall stop after SMT2 typing. *) +val get_imperative_mode : unit -> bool +(** Default to [false] *) + (** {4 Internal options} *) (** [true] if the GC is prevented from collecting hashconsed data structrures From e918fa0564532a3f8f2ac87a97c34f05656fd423 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Fri, 22 Mar 2024 18:26:34 +0100 Subject: [PATCH 04/17] Update tests --- tests/cram.t/run.t | 2 +- tests/issues/555.models.expected | 4 ++-- tests/issues/854/function.models.expected | 2 +- tests/issues/854/original.models.expected | 2 +- tests/issues/854/twice_eq.models.expected | 4 ++-- tests/models/arith/arith12.optimize.expected | 5 ++--- tests/models/array/array1.models.expected | 4 ++-- tests/models/array/embedded-array.models.expected | 6 +++--- tests/smtlib/testfile-steps-bound2.dolmen.expected | 2 +- 9 files changed, 15 insertions(+), 16 deletions(-) diff --git a/tests/cram.t/run.t b/tests/cram.t/run.t index ff4214ec6..6be8fef15 100644 --- a/tests/cram.t/run.t +++ b/tests/cram.t/run.t @@ -11,7 +11,7 @@ appropriate here. ( (define-fun x () Int 0) (define-fun y () Int 0) - (define-fun a1 () (Array Int Int) (store (as @a4 (Array Int Int)) 0 0)) + (define-fun a1 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0)) (define-fun a2 () (Array Int Int) (as @a0 (Array Int Int))) ) diff --git a/tests/issues/555.models.expected b/tests/issues/555.models.expected index f5b97ee0b..6db0558a4 100644 --- a/tests/issues/555.models.expected +++ b/tests/issues/555.models.expected @@ -3,6 +3,6 @@ unknown ( (define-fun x () Int 0) (define-fun y () Int 0) - (define-fun a1 () (Array Int Int) (store (as @a4 (Array Int Int)) 0 0)) - (define-fun a2 () (Array Int Int) (store (as @a5 (Array Int Int)) 0 0)) + (define-fun a1 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0)) + (define-fun a2 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0)) ) diff --git a/tests/issues/854/function.models.expected b/tests/issues/854/function.models.expected index 6e5eeb8fb..bb0b49fe0 100644 --- a/tests/issues/854/function.models.expected +++ b/tests/issues/854/function.models.expected @@ -1,7 +1,7 @@ unknown ( - (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a4 intref)) + (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a0 intref)) (define-fun a () Int 0) (define-fun f ((_arg_0 Int)) Int 0) (define-fun a1 () Int 0) diff --git a/tests/issues/854/original.models.expected b/tests/issues/854/original.models.expected index 7d40ab42e..9198abbbf 100644 --- a/tests/issues/854/original.models.expected +++ b/tests/issues/854/original.models.expected @@ -1,7 +1,7 @@ unknown ( - (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a3 intref)) + (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a0 intref)) (define-fun a () Int 0) (define-fun a1 () Int 0) ) diff --git a/tests/issues/854/twice_eq.models.expected b/tests/issues/854/twice_eq.models.expected index ee4c1de0d..f18c7f58e 100644 --- a/tests/issues/854/twice_eq.models.expected +++ b/tests/issues/854/twice_eq.models.expected @@ -1,8 +1,8 @@ unknown ( - (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a4 intref)) - (define-fun another_mk ((_arg_0 Int)) intref (as @a4 intref)) + (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a0 intref)) + (define-fun another_mk ((_arg_0 Int)) intref (as @a0 intref)) (define-fun a () Int 0) (define-fun a1 () Int 0) ) diff --git a/tests/models/arith/arith12.optimize.expected b/tests/models/arith/arith12.optimize.expected index 3f79c668e..6baad1e2e 100644 --- a/tests/models/arith/arith12.optimize.expected +++ b/tests/models/arith/arith12.optimize.expected @@ -7,9 +7,8 @@ unknown (x 10)) unknown ( - (define-fun x () Int 10) + (define-fun x () Int 0) ) (objectives - (x 10) - (x 10) + (x 0) ) \ No newline at end of file diff --git a/tests/models/array/array1.models.expected b/tests/models/array/array1.models.expected index f5b97ee0b..6db0558a4 100644 --- a/tests/models/array/array1.models.expected +++ b/tests/models/array/array1.models.expected @@ -3,6 +3,6 @@ unknown ( (define-fun x () Int 0) (define-fun y () Int 0) - (define-fun a1 () (Array Int Int) (store (as @a4 (Array Int Int)) 0 0)) - (define-fun a2 () (Array Int Int) (store (as @a5 (Array Int Int)) 0 0)) + (define-fun a1 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0)) + (define-fun a2 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0)) ) diff --git a/tests/models/array/embedded-array.models.expected b/tests/models/array/embedded-array.models.expected index 057bc1a6c..dd6a80ae9 100644 --- a/tests/models/array/embedded-array.models.expected +++ b/tests/models/array/embedded-array.models.expected @@ -1,8 +1,8 @@ unknown ( - (define-fun s () S (as @a2 S)) + (define-fun s () S (as @a0 S)) (define-fun x () Pair - (pair (store (as @a3 (Array Int S)) 0 s) - (store (as @a3 (Array Int S)) 0 s))) + (pair (store (as @a1 (Array Int S)) 0 s) + (store (as @a1 (Array Int S)) 0 s))) ) diff --git a/tests/smtlib/testfile-steps-bound2.dolmen.expected b/tests/smtlib/testfile-steps-bound2.dolmen.expected index 2c1783497..9c2a2a16f 100644 --- a/tests/smtlib/testfile-steps-bound2.dolmen.expected +++ b/tests/smtlib/testfile-steps-bound2.dolmen.expected @@ -1,5 +1,5 @@ unknown -(:reason-unknown (:step-limit 3)) +(:reason-unknown (:step-limit 5)) unsat From c985aedc6064e002172de74dcf07b287069129c2 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Mon, 25 Mar 2024 12:06:44 +0100 Subject: [PATCH 05/17] Reactivating abstract value printing and update tests --- src/bin/common/dune | 3 +- src/bin/common/solving_loop.ml | 9 +++-- src/lib/frontend/d_cnf.ml | 35 ++++++++++--------- src/lib/frontend/d_cnf.mli | 2 +- src/lib/frontend/frontend.ml | 4 +++ src/lib/frontend/frontend.mli | 2 ++ tests/cram.t/run.t | 2 +- tests/issues/555.models.expected | 4 +-- tests/issues/854/function.models.expected | 2 +- tests/issues/854/original.models.expected | 2 +- tests/issues/854/twice_eq.models.expected | 4 +-- tests/models/array/array1.models.expected | 4 +-- .../array/embedded-array.models.expected | 6 ++-- 13 files changed, 44 insertions(+), 35 deletions(-) diff --git a/src/bin/common/dune b/src/bin/common/dune index 8cc2a2b71..307f982a5 100644 --- a/src/bin/common/dune +++ b/src/bin/common/dune @@ -21,8 +21,7 @@ Parse_command Input_frontend Signals_profiling - Solving_loop - Solving_loop_imperative) + Solving_loop) ) (generate_sites_module diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index cf3624835..bba5afe2c 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -1199,9 +1199,12 @@ let main () = in st - | {contents = `Decls l; _} -> + | {contents = `Decls l; loc; _} -> let st = DO.Mode.set Util.Assert st in - D_cnf.cache_decls l; + let decls = D_cnf.make_decls l in + let module Api = (val DO.SatSolverModule.get st) in + let loc = dl_to_ael file_loc loc in + List.iter (fun decl -> Api.FE.declare ~loc decl Api.env) decls; st (* When the next statement is a goal, the solver is called and provided @@ -1371,7 +1374,7 @@ let main () = let st = handle_reset st in let whole_path = List.rev_append prefix tl in Format.eprintf "Restarting with %i instructions@." (List.length whole_path); - aux (State.get named_terms st) st whole_path + aux Util.MS.empty st whole_path | {contents; _ } -> let st = let new_current_path = diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml index 57014fab7..51164af0e 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/src/lib/frontend/d_cnf.ml @@ -697,14 +697,14 @@ let mk_term_decl ({ id_ty; path; tags; _ } as tcst: DE.term_cst) = in Cache.store_sy tcst sy; (* Adding polymorphic types to the cache. *) - Cache.store_ty_vars id_ty(* ; - * let arg_tys, ret_ty = - * match DT.view id_ty with - * | `Arrow (arg_tys, ret_ty) -> - * List.map dty_to_ty arg_tys, dty_to_ty ret_ty - * | _ -> [], dty_to_ty id_ty - * in - * (Hstring.make name, arg_tys, ret_ty) *) + Cache.store_ty_vars id_ty; + let arg_tys, ret_ty = + match DT.view id_ty with + | `Arrow (arg_tys, ret_ty) -> + List.map dty_to_ty arg_tys, dty_to_ty ret_ty + | _ -> [], dty_to_ty id_ty + in + (Hstring.make name, arg_tys, ret_ty) (** Handles the definitions of a list of mutually recursive types. - If one of the types is an ADT, the ADTs that have only one case are @@ -1898,16 +1898,16 @@ 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 +let make_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; + | `Type_decl (td, _def) -> mk_ty_decl td; [] + | `Term_decl td -> [mk_term_decl td]; end | dcl -> - let rec aux acc tdl = + let rec aux term_acc 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. @@ -1919,20 +1919,21 @@ let cache_decls = function | [otd] -> mk_ty_decl otd | _ -> mk_mr_ty_decls (List.rev acc) end; - mk_term_decl td; - aux [] tl + let t = mk_term_decl td in + aux (t :: term_acc) [] tl | `Type_decl (td, _def) :: tl -> - aux (td :: acc) tl + aux term_acc (td :: acc) tl | [] -> begin match acc with | [] -> () | [otd] -> mk_ty_decl otd | _ -> mk_mr_ty_decls (List.rev acc) - end + end; + term_acc in - aux [] dcl + aux [] [] dcl (* Helper function used to check if the expression defining an objective function is a pure term. *) diff --git a/src/lib/frontend/d_cnf.mli b/src/lib/frontend/d_cnf.mli index 772153c4e..319ce3ed0 100644 --- a/src/lib/frontend/d_cnf.mli +++ b/src/lib/frontend/d_cnf.mli @@ -99,7 +99,7 @@ val pp_query : (** 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_decls : D_loop.Typer_Pipe.decl list -> (Hstring.t * Ty.t list * Ty.t) list val builtins : Dolmen_loop.State.t -> diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index b5ebb0c18..9bbc252d3 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -146,6 +146,8 @@ module type S = sig val init_env : ?sat_env:sat_env -> used_context -> env + val declare : Id.typed process + val push : int process val pop : int process @@ -436,6 +438,8 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct let wrap_f f ?loc x env = check_if_over (handle_sat_exn f ?loc x) env + let declare = wrap_f internal_decl + let push = wrap_f internal_push let pop = wrap_f internal_pop diff --git a/src/lib/frontend/frontend.mli b/src/lib/frontend/frontend.mli index a5606b155..c0ad02e10 100644 --- a/src/lib/frontend/frontend.mli +++ b/src/lib/frontend/frontend.mli @@ -70,6 +70,8 @@ module type S = sig the user. *) type 'a process = ?loc:Loc.t -> 'a -> env -> unit + val declare : Id.typed process + val push : int process val pop : int process diff --git a/tests/cram.t/run.t b/tests/cram.t/run.t index 6be8fef15..ff4214ec6 100644 --- a/tests/cram.t/run.t +++ b/tests/cram.t/run.t @@ -11,7 +11,7 @@ appropriate here. ( (define-fun x () Int 0) (define-fun y () Int 0) - (define-fun a1 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0)) + (define-fun a1 () (Array Int Int) (store (as @a4 (Array Int Int)) 0 0)) (define-fun a2 () (Array Int Int) (as @a0 (Array Int Int))) ) diff --git a/tests/issues/555.models.expected b/tests/issues/555.models.expected index 6db0558a4..f5b97ee0b 100644 --- a/tests/issues/555.models.expected +++ b/tests/issues/555.models.expected @@ -3,6 +3,6 @@ unknown ( (define-fun x () Int 0) (define-fun y () Int 0) - (define-fun a1 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0)) - (define-fun a2 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0)) + (define-fun a1 () (Array Int Int) (store (as @a4 (Array Int Int)) 0 0)) + (define-fun a2 () (Array Int Int) (store (as @a5 (Array Int Int)) 0 0)) ) diff --git a/tests/issues/854/function.models.expected b/tests/issues/854/function.models.expected index bb0b49fe0..6e5eeb8fb 100644 --- a/tests/issues/854/function.models.expected +++ b/tests/issues/854/function.models.expected @@ -1,7 +1,7 @@ unknown ( - (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a0 intref)) + (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a4 intref)) (define-fun a () Int 0) (define-fun f ((_arg_0 Int)) Int 0) (define-fun a1 () Int 0) diff --git a/tests/issues/854/original.models.expected b/tests/issues/854/original.models.expected index 9198abbbf..7d40ab42e 100644 --- a/tests/issues/854/original.models.expected +++ b/tests/issues/854/original.models.expected @@ -1,7 +1,7 @@ unknown ( - (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a0 intref)) + (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a3 intref)) (define-fun a () Int 0) (define-fun a1 () Int 0) ) diff --git a/tests/issues/854/twice_eq.models.expected b/tests/issues/854/twice_eq.models.expected index f18c7f58e..ee4c1de0d 100644 --- a/tests/issues/854/twice_eq.models.expected +++ b/tests/issues/854/twice_eq.models.expected @@ -1,8 +1,8 @@ unknown ( - (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a0 intref)) - (define-fun another_mk ((_arg_0 Int)) intref (as @a0 intref)) + (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a4 intref)) + (define-fun another_mk ((_arg_0 Int)) intref (as @a4 intref)) (define-fun a () Int 0) (define-fun a1 () Int 0) ) diff --git a/tests/models/array/array1.models.expected b/tests/models/array/array1.models.expected index 6db0558a4..f5b97ee0b 100644 --- a/tests/models/array/array1.models.expected +++ b/tests/models/array/array1.models.expected @@ -3,6 +3,6 @@ unknown ( (define-fun x () Int 0) (define-fun y () Int 0) - (define-fun a1 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0)) - (define-fun a2 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0)) + (define-fun a1 () (Array Int Int) (store (as @a4 (Array Int Int)) 0 0)) + (define-fun a2 () (Array Int Int) (store (as @a5 (Array Int Int)) 0 0)) ) diff --git a/tests/models/array/embedded-array.models.expected b/tests/models/array/embedded-array.models.expected index dd6a80ae9..057bc1a6c 100644 --- a/tests/models/array/embedded-array.models.expected +++ b/tests/models/array/embedded-array.models.expected @@ -1,8 +1,8 @@ unknown ( - (define-fun s () S (as @a0 S)) + (define-fun s () S (as @a2 S)) (define-fun x () Pair - (pair (store (as @a1 (Array Int S)) 0 s) - (store (as @a1 (Array Int S)) 0 s))) + (pair (store (as @a3 (Array Int S)) 0 s) + (store (as @a3 (Array Int S)) 0 s))) ) From 0f0dd69b7b2cd0816f673f121d6ee8784e440e30 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Mon, 25 Mar 2024 12:30:28 +0100 Subject: [PATCH 06/17] Documentation and small fix --- src/bin/common/solving_loop.ml | 72 ++++++++++++++++++++++++++++------ 1 file changed, 59 insertions(+), 13 deletions(-) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index bba5afe2c..63f28ce5f 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -179,6 +179,11 @@ let print_solve_res loc goal_name r = exception StopProcessDecl +(** Returns the value bound to the key in the state in argument: if it does not + exist, results default. *) +let state_get ~default key st = + try State.get key st with State.Key_not_found _ -> default + let main () = let () = Dolmen_loop.Code.init [] in @@ -412,6 +417,18 @@ let main () = State.create_key ~pipe:"" "is_decision_env" in + (* Key used only in handle_stmt_pop_reinit, registers the commands executed + to save them them if a push command is executed. *) + let current_path_key : stmt list State.key = + State.create_key ~pipe:"" "current_path" + in + + (* Key used only in handle_stmt_pop_reinit, saves the commands executed + when a push is executed and replays them when a pop is met. *) + let pushed_paths_key : stmt list Vec.t State.key = + State.create_key ~pipe:"" "pushed_paths" + in + (* Before each query, we push the current environment. This allows to keep a fresh one for the next assertions. *) let internal_push st = @@ -1141,6 +1158,7 @@ let main () = set_partial_model_and_mode solve_res st in + (* TODO: reset options to their initial value. *) let handle_reset st = let () = Steps.reset_steps () in st @@ -1328,6 +1346,8 @@ let main () = st in + (* Handle each statement one after the other. + Still experimental due to push & pop issues. *) let handle_stmts_full_incremental all_context st l = let rec aux named_map st = function | [] -> State.set named_terms named_map st @@ -1339,18 +1359,21 @@ let main () = aux (State.get named_terms st) st l in - let current_path_key : stmt list State.key = - State.create_key ~pipe:"" "current_path" - in - let pushed_paths_key : stmt list Vec.t State.key = - State.create_key ~pipe:"" "pushed_paths" - in - let state_get key ~default st = - try State.get key st with State.Key_not_found _ -> default - in - let get_current_path = state_get current_path_key ~default:[] in - let get_pushed_paths = state_get pushed_paths_key ~default:(Vec.create ~dummy:(Obj.magic 0)) + let get_current_path = state_get ~default:[] current_path_key in + + let get_pushed_paths = + state_get ~default:(Vec.create ~dummy:[]) pushed_paths_key in + + (* Same as handle_stmts_full_incremental, but removes pops and pushes. + Instead, every command that perform an effect on the environment + (definitions, assertion, resets, set option, ...) are stored in a list of + commands. When a (push n) is performed, this list is stored n times in a + Vec. When a pop m occurs, we reset the analysis, the Vec is popped m times + and the list of commands is replayed before continuing the analysis. + /!\ Pop do not reset options, so there may be inconstencies between a first + execution and a reinitialized one. The handle_reset function should handle + this, but it is not the case yet. *) let handle_stmt_pop_reinit all_context st l = let rec aux named_map st = function | [] -> State.set named_terms named_map st @@ -1379,17 +1402,40 @@ let main () = let st = let new_current_path = match contents with + (* Statemets to keep *) | `Clause _ | `Decls _ | `Defs _ + | `Exit (* This case should not happen.*) | `Hyp _ - | `Other _ | `Reset | `Reset_assertions | `Set_info _ | `Set_logic _ | `Set_option _ -> stmt :: current_path - | _ -> current_path + (* Statements to remove *) + | `Echo _ + | `Get_assertions + | `Get_info _ + | `Get_model + | `Get_option _ + | `Get_proof + | `Get_unsat_core + | `Get_value _ + | `Get_assignment + | `Get_unsat_assumptions + | `Goal _ + | `Push _ + | `Pop _ + | `Solve (_, _) -> current_path + (* Custom statement *) + | `Other (custom, _) -> + begin + match custom with + | {name = Simple ("minimize" | "maximize"); _} -> + stmt :: current_path + | _ -> current_path + end in State.set current_path_key new_current_path st in From c10ad82e8d1af86c1ef5ae63481eb389f76618dd Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Mon, 25 Mar 2024 12:32:27 +0100 Subject: [PATCH 07/17] Style --- src/bin/common/solving_loop.ml | 7 ++++--- src/lib/frontend/d_cnf.ml | 6 ++++-- src/lib/frontend/d_cnf.mli | 3 ++- 3 files changed, 10 insertions(+), 6 deletions(-) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 63f28ce5f..cfb963a95 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -1389,14 +1389,15 @@ let main () = aux named_map st tl | {contents = `Pop n; _} -> let pushed_paths = get_pushed_paths st in - Format.eprintf "Vec size: %i@." pushed_paths.sz; let rec pop_until until res = - if until = 0 then res else pop_until (until - 1) (Vec.pop pushed_paths) + if until = 0 then + res + else + pop_until (until - 1) (Vec.pop pushed_paths) in let prefix = pop_until (n - 1) (Vec.pop pushed_paths) in let st = handle_reset st in let whole_path = List.rev_append prefix tl in - Format.eprintf "Restarting with %i instructions@." (List.length whole_path); aux Util.MS.empty st whole_path | {contents; _ } -> let st = diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml index 51164af0e..72c750252 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/src/lib/frontend/d_cnf.ml @@ -213,7 +213,9 @@ let builtin_enum = function let add_cstrs map = List.fold_left (fun map ((c : DE.term_cst), _) -> let name = get_basename c.path in - DStd.Id.Map.add { name = DStd.Name.simple name; ns = Term } (fun env _ -> + DStd.Id.Map.add + { name = DStd.Name.simple name; ns = Term } + (fun env _ -> builtin_term @@ Dolmen_type.Base.term_app_cst (module Dl.Typer.T) env c) map) @@ -239,7 +241,7 @@ module Const = struct let name = "bv2nat" in Id.mk ~name ~builtin:(BV2Nat n) (DStd.Path.global name) Ty.(arrow [bitv n] int)) - + let int2bv = with_cache (fun n -> let name = "int2bv" in diff --git a/src/lib/frontend/d_cnf.mli b/src/lib/frontend/d_cnf.mli index 319ce3ed0..21989426e 100644 --- a/src/lib/frontend/d_cnf.mli +++ b/src/lib/frontend/d_cnf.mli @@ -99,7 +99,8 @@ val pp_query : (** 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 make_decls : D_loop.Typer_Pipe.decl list -> (Hstring.t * Ty.t list * Ty.t) list +val make_decls : + D_loop.Typer_Pipe.decl list -> (Hstring.t * Ty.t list * Ty.t) list val builtins : Dolmen_loop.State.t -> From 4bbfc8408edb51496fc41a95d526c58483644c86 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Mon, 25 Mar 2024 13:18:44 +0100 Subject: [PATCH 08/17] Indent --- src/lib/frontend/d_cnf.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml index 72c750252..50e1e8eb4 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/src/lib/frontend/d_cnf.ml @@ -216,9 +216,9 @@ let builtin_enum = function DStd.Id.Map.add { name = DStd.Name.simple name; ns = Term } (fun env _ -> - builtin_term @@ - Dolmen_type.Base.term_app_cst - (module Dl.Typer.T) env c) map) + builtin_term @@ + Dolmen_type.Base.term_app_cst + (module Dl.Typer.T) env c) map) map cstrs in Cache.store_ty (DE.Ty.Const.hash ty_cst) ty_; From e844f177c8e4902d8c081a049bea6a7f8c00b3f2 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Mon, 25 Mar 2024 15:06:34 +0100 Subject: [PATCH 09/17] Fix for test tests/cc/testfile-ac_cc002.ae --- src/lib/reasoners/satml.ml | 35 +++++++++++++++++++++-------------- 1 file changed, 21 insertions(+), 14 deletions(-) diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml index 1424b3248..f6da1af5e 100644 --- a/src/lib/reasoners/satml.ml +++ b/src/lib/reasoners/satml.ml @@ -1038,21 +1038,28 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct (fun acc (ta : Atom.atom) -> assert (ta.is_true); assert (ta.var.level >= 0); - if ta.var.level <= Vec.size env.increm_guards then begin - incr nb_f; - let ex = - if ta.var.level = 0 then Ex.empty else - let d = - Vec.get env.trail (Vec.get env.trail_lim (ta.var.level - 1)) - in - Ex.singleton (Ex.Literal d) - in - (ta.lit, - Th_util.Other, - ex, - ta.var.level, - env.cpt_current_propagations) :: acc + if ta.var.level = 0 then begin + (ta.lit, Th_util.Other, Ex.empty, 0, env.cpt_current_propagations) + :: acc end + (* This was first added by PR 1000, but it triggers a bug in + tests/cc/testfile-ac_cc002.ae with option + --no-tableaux-cdcl-in-instantiation *) + (* if ta.var.level <= Vec.size env.increm_guards then begin + * incr nb_f; + * let ex = + * if ta.var.level = 0 then Ex.empty else + * let d = + * Vec.get env.trail (Vec.get env.trail_lim (ta.var.level - 1)) + * in + * Ex.singleton (Ex.Literal d) + * in + * (ta.lit, + * Th_util.Other, + * ex, + * ta.var.level, + * env.cpt_current_propagations) :: acc + * end *) else acc )[] lazy_q in From cfbc8bc31255932d53dc219cfd9737a4cef25218 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Thu, 28 Mar 2024 11:07:04 +0100 Subject: [PATCH 10/17] Poetry --- src/bin/common/solving_loop.ml | 23 +++++++++-------------- src/lib/reasoners/satml.ml | 11 ++++++----- src/lib/util/options.mli | 4 ++-- tests/adts/simple_1.ae | 3 +-- tests/adts/simple_1.expected | 2 ++ 5 files changed, 20 insertions(+), 23 deletions(-) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index cfb963a95..ed30e32c3 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -431,21 +431,16 @@ let main () = (* Before each query, we push the current environment. This allows to keep a fresh one for the next assertions. *) - let internal_push st = - if State.get is_decision_env st then - (* We already performed a check-sat *) - st - else - begin - let module Api = (val (DO.SatSolverModule.get st)) in - Api.FE.push 1 Api.env; - State.set is_decision_env true st - end + let push_before_query st = + assert (not (State.get is_decision_env st)); + let module Api = (val (DO.SatSolverModule.get st)) in + Api.FE.push 1 Api.env; + State.set is_decision_env true 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 = + let pop_if_post_query st = if State.get is_decision_env st then begin let module Api = (val (DO.SatSolverModule.get st)) in @@ -641,7 +636,7 @@ let main () = DO.Mode.add_hook (fun _ ~old:_ ~new_ st -> match new_ with - | Assert -> internal_pop st + | Assert -> pop_if_post_query st | _ -> st ) in @@ -1070,12 +1065,12 @@ let main () = the hook on D_state_option.Mode. *) let handle_query st id loc attrs contents = let module Api = (val (DO.SatSolverModule.get st)) in - let st = internal_pop st in + let st = pop_if_post_query 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 = push_before_query st in let st_loc = let file_loc = (State.get State.logic_file st).loc in dl_to_ael file_loc loc diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml index f6da1af5e..8036729ca 100644 --- a/src/lib/reasoners/satml.ml +++ b/src/lib/reasoners/satml.ml @@ -1039,6 +1039,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct assert (ta.is_true); assert (ta.var.level >= 0); if ta.var.level = 0 then begin + incr nb_f; (ta.lit, Th_util.Other, Ex.empty, 0, env.cpt_current_propagations) :: acc end @@ -1243,11 +1244,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 set_unsat env : unit = env.is_unsat <- true let report_b_unsat env linit = if not (Options.get_unsat_core ()) then begin - is_unsat env; + set_unsat env; env.unsat_core <- None; raise (Unsat None) end @@ -1287,7 +1288,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; - is_unsat env; + set_unsat env; let unsat_core = Some unsat_core in env.unsat_core <- unsat_core; raise (Unsat unsat_core) @@ -1295,7 +1296,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 - is_unsat env; + set_unsat env; env.unsat_core <- None; raise (Unsat None) end @@ -1336,7 +1337,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; - is_unsat env; + set_unsat env; let unsat_core = Some unsat_core in env.unsat_core <- unsat_core; raise (Unsat unsat_core) diff --git a/src/lib/util/options.mli b/src/lib/util/options.mli index c5cbcd3d7..02998e7d6 100644 --- a/src/lib/util/options.mli +++ b/src/lib/util/options.mli @@ -298,7 +298,7 @@ val set_triggers_var : bool -> unit (** Set [type_smt2] accessible with {!val:get_type_smt2} *) val set_type_smt2 : bool -> unit -(** Set [type_smt2] accessible with {!val:get_type_smt2} *) +(** Set [imperative_mode] accessible with {!val:get_imperative_mode} *) val set_imperative_mode : bool -> unit (** Set [unsat_core] accessible with {!val:get_unsat_core} *) @@ -663,7 +663,7 @@ val get_type_only : unit -> bool val get_type_smt2 : unit -> bool (** Default to [false] *) -(** [true] if the program shall stop after SMT2 typing. *) +(** [true] if the solving loop should work in a pure imperative mode. *) val get_imperative_mode : unit -> bool (** Default to [false] *) diff --git a/tests/adts/simple_1.ae b/tests/adts/simple_1.ae index fa271f926..416c8f617 100644 --- a/tests/adts/simple_1.ae +++ b/tests/adts/simple_1.ae @@ -50,14 +50,13 @@ goal g_valid_4_2: false (* Isse 1008: this goal fail when encapsulated by a push/pop. *) -(* goal g_valid_5_1: forall n : int. n >= 0 -> (* just here for E-matching *) not (e ? A) -> not (e ? B) -> exists x : int[x]. e = C(x) -*) + goal g_valid_5_2: forall n : int. diff --git a/tests/adts/simple_1.expected b/tests/adts/simple_1.expected index f97cc55c7..f8919c465 100644 --- a/tests/adts/simple_1.expected +++ b/tests/adts/simple_1.expected @@ -20,3 +20,5 @@ unsat unsat unsat + +unsat From f03b2e13073e3993bfaf0d0c6a94745350526d32 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Thu, 4 Apr 2024 17:09:01 +0200 Subject: [PATCH 11/17] Disactivating push & pop in queries in non incremental mode --- src/bin/common/solving_loop.ml | 173 ++++++++++++------ .../smtlib/testfile-get-info1.dolmen.expected | 2 +- 2 files changed, 123 insertions(+), 52 deletions(-) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index ed30e32c3..5f9d9ab15 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -631,7 +631,7 @@ let main () = to the Sat or Unsat mode we end up in. If we start asserting again, we must do it in the previous environment. *) - let () = + let init_full_incremental_hooks () = DO.Mode.reset_hooks (); DO.Mode.add_hook (fun _ ~old:_ ~new_ st -> @@ -1065,12 +1065,6 @@ let main () = the hook on D_state_option.Mode. *) let handle_query st id loc attrs contents = let module Api = (val (DO.SatSolverModule.get st)) in - let st = pop_if_post_query 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 = push_before_query st in let st_loc = let file_loc = (State.get State.logic_file st).loc in dl_to_ael file_loc loc @@ -1153,6 +1147,31 @@ let main () = set_partial_model_and_mode solve_res st in + let handle_solve = + let goal_cnt = ref 0 in + fun st id contents loc attrs -> + let module Api = (val DO.SatSolverModule.get st) in + let file_loc = (State.get State.logic_file st).loc in + let id = + match (State.get State.logic_file st).lang with + | Some (Smtlib2 _) -> + DStd.Id.mk DStd.Namespace.term @@ + "g_" ^ string_of_int (incr goal_cnt; !goal_cnt) + | _ -> id + in + let contents = + match contents with + | `Solve (hyps, []) -> `Check hyps + | `Solve ([], [t]) -> `Goal t + | _ -> + let loc = DStd.Loc.loc file_loc loc in + fatal_error "%a: internal error: unknown statement" + DStd.Loc.fmt loc + in + (* Performing the query *) + handle_query st id loc attrs contents + in + (* TODO: reset options to their initial value. *) let handle_reset st = let () = Steps.reset_steps () in @@ -1172,7 +1191,6 @@ let main () = 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 -> let file_loc = (State.get State.logic_file st).loc in match td with @@ -1186,8 +1204,16 @@ let main () = contents = (`Goal _) as contents; implicit = _; } -> + (* In the non imperative mode, the Solve instruction is handled differently + (i.e. no pop/push). *) + assert (not (Options.get_imperative_mode ())); cmd_on_modes st [Assert; Sat; Unsat] "goal"; - (* Setting the mode is done by handle_query. *) + let st = pop_if_post_query 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 = push_before_query st in handle_query st id loc attrs contents (* Axiom definitions *) @@ -1223,27 +1249,17 @@ let main () = (* 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=_ } -> + (* In the non imperative mode, the Solve instruction is handled differently + (i.e. no pop/push). *) + assert (not (Options.get_imperative_mode ())); 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 _) -> - DStd.Id.mk DStd.Namespace.term @@ - "g_" ^ string_of_int (incr goal_cnt; !goal_cnt) - | _ -> id - in - let contents = - match contents with - | `Solve (hyps, []) -> `Check hyps - | `Solve ([], [t]) -> `Goal t - | _ -> - let loc = DStd.Loc.loc file_loc loc in - fatal_error "%a: internal error: unknown statement" - DStd.Loc.fmt loc - in - (* Performing the query *) - handle_query st id loc attrs contents; + let st = pop_if_post_query 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 = push_before_query st in + handle_solve st id contents loc attrs | {contents = `Set_option { DStd.Term.term = @@ -1370,34 +1386,84 @@ let main () = execution and a reinitialized one. The handle_reset function should handle this, but it is not the case yet. *) let handle_stmt_pop_reinit all_context st l = - let rec aux named_map st = function + + (* Pushes n times the current path. *) + let push n st = + let current_path = get_current_path st in + let pushed_paths = get_pushed_paths st in + for _ = 0 to n - 1 do + Vec.push pushed_paths current_path + done + in + + (* Pops n times the current path and calls [replay] on the + list of instruction returned. *) + let pop n st replay = + let pushed_paths = get_pushed_paths st in + let rec pop_until until res = + if until = 0 then + res + else + pop_until (until - 1) (Vec.pop pushed_paths) + in + let rev_prefix = pop_until (n - 1) (Vec.pop pushed_paths) in + let st = handle_reset st in + replay st (List.rev rev_prefix) + in + + (* Before each query, we push the current environment. This allows to keep a + fresh one for the next assertions. *) + let push_before_query st = + assert (not (State.get is_decision_env st)); + push 1 st; + State.set is_decision_env true st + in + + (* The pop corresponding to the previous push. It must be applied everytime the + mode goes from Sat/Unsat to Assert. *) + let rec pop_if_post_query st = + if State.get is_decision_env st + then pop 1 st (aux Util.MS.empty) + else st + and aux named_map st = function | [] -> State.set named_terms named_map st | (stmt: stmt) :: tl -> begin let current_path = get_current_path st in match stmt with | {contents = `Push n; _} -> - let pushed_paths = get_pushed_paths st in - for _ = 0 to n - 1 do - Vec.push pushed_paths current_path - done; + push n st; + let st = set_mode Assert st in aux named_map st tl | {contents = `Pop n; _} -> - let pushed_paths = get_pushed_paths st in - let rec pop_until until res = - if until = 0 then - res - else - pop_until (until - 1) (Vec.pop pushed_paths) - in - let prefix = pop_until (n - 1) (Vec.pop pushed_paths) in - let st = handle_reset st in - let whole_path = List.rev_append prefix tl in - aux Util.MS.empty st whole_path + let st = set_mode Assert st in + pop n st begin fun st prefix -> + let st = aux Util.MS.empty st prefix in + aux (State.get named_terms st) st tl + end + | { + id; loc; attrs; + contents = (`Goal _) as contents; + implicit = _; + } -> + cmd_on_modes st [Assert; Sat; Unsat] "goal"; + let st = pop_if_post_query st in + let st = push_before_query st in + handle_query st id loc attrs contents + | { id; contents = (`Solve _ as contents); loc ; attrs; implicit=_ } -> + cmd_on_modes st [Assert; Unsat; Sat] "check-sat"; + let st = pop_if_post_query st in + let st = push_before_query st in + handle_solve st id contents loc attrs | {contents; _ } -> let st = let new_current_path = match contents with + (* Treated above *) + | `Goal _ + | `Push _ + | `Pop _ + | `Solve (_, _) -> assert false (* Statemets to keep *) | `Clause _ | `Decls _ @@ -1419,11 +1485,7 @@ let main () = | `Get_unsat_core | `Get_value _ | `Get_assignment - | `Get_unsat_assumptions - | `Goal _ - | `Push _ - | `Pop _ - | `Solve (_, _) -> current_path + | `Get_unsat_assumptions -> current_path (* Custom statement *) | `Other (custom, _) -> begin @@ -1440,12 +1502,21 @@ let main () = aux named_map st tl end in + DO.Mode.reset_hooks (); + DO.Mode.add_hook + (fun _ ~old:_ ~new_ st -> + match new_ with + | Assert -> pop_if_post_query st + | _ -> st + ); aux (State.get named_terms st) st l in let handle_stmts all_context st l = begin if Options.get_imperative_mode () - then handle_stmts_full_incremental + then + let () = init_full_incremental_hooks () in + handle_stmts_full_incremental else handle_stmt_pop_reinit end all_context st l in diff --git a/tests/smtlib/testfile-get-info1.dolmen.expected b/tests/smtlib/testfile-get-info1.dolmen.expected index 8241c6580..d206212dc 100644 --- a/tests/smtlib/testfile-get-info1.dolmen.expected +++ b/tests/smtlib/testfile-get-info1.dolmen.expected @@ -1,7 +1,7 @@ unknown ( - :steps 11) + :steps 10) unsupported From baba2551bfe35c11ac1d79bf7496a1a998f75359 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Thu, 4 Apr 2024 17:16:04 +0200 Subject: [PATCH 12/17] Linter --- src/bin/common/solving_loop.ml | 62 ++++++++++++++++++---------------- src/lib/reasoners/satml.ml | 4 ++- 2 files changed, 35 insertions(+), 31 deletions(-) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 5f9d9ab15..80e6f16bb 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -1150,26 +1150,26 @@ let main () = let handle_solve = let goal_cnt = ref 0 in fun st id contents loc attrs -> - let module Api = (val DO.SatSolverModule.get st) in + let module Api = (val DO.SatSolverModule.get st) in let file_loc = (State.get State.logic_file st).loc in - let id = - match (State.get State.logic_file st).lang with - | Some (Smtlib2 _) -> - DStd.Id.mk DStd.Namespace.term @@ - "g_" ^ string_of_int (incr goal_cnt; !goal_cnt) - | _ -> id - in - let contents = - match contents with - | `Solve (hyps, []) -> `Check hyps - | `Solve ([], [t]) -> `Goal t - | _ -> - let loc = DStd.Loc.loc file_loc loc in - fatal_error "%a: internal error: unknown statement" - DStd.Loc.fmt loc - in - (* Performing the query *) - handle_query st id loc attrs contents + let id = + match (State.get State.logic_file st).lang with + | Some (Smtlib2 _) -> + DStd.Id.mk DStd.Namespace.term @@ + "g_" ^ string_of_int (incr goal_cnt; !goal_cnt) + | _ -> id + in + let contents = + match contents with + | `Solve (hyps, []) -> `Check hyps + | `Solve ([], [t]) -> `Goal t + | _ -> + let loc = DStd.Loc.loc file_loc loc in + fatal_error "%a: internal error: unknown statement" + DStd.Loc.fmt loc + in + (* Performing the query *) + handle_query st id loc attrs contents in (* TODO: reset options to their initial value. *) @@ -1204,15 +1204,15 @@ let main () = contents = (`Goal _) as contents; implicit = _; } -> - (* In the non imperative mode, the Solve instruction is handled differently - (i.e. no pop/push). *) + (* In the non imperative mode, the Solve instruction is handled + differently (i.e. no pop/push). *) assert (not (Options.get_imperative_mode ())); cmd_on_modes st [Assert; Sat; Unsat] "goal"; let st = pop_if_post_query 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. *) + 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 = push_before_query st in handle_query st id loc attrs contents @@ -1249,15 +1249,15 @@ let main () = (* 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=_ } -> - (* In the non imperative mode, the Solve instruction is handled differently - (i.e. no pop/push). *) + (* In the non imperative mode, the Solve instruction is handled + differently (i.e. no pop/push). *) assert (not (Options.get_imperative_mode ())); cmd_on_modes st [Assert; Unsat; Sat] "check-sat"; let st = pop_if_post_query 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. *) + 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 = push_before_query st in handle_solve st id contents loc attrs @@ -1419,8 +1419,8 @@ let main () = State.set is_decision_env true st in - (* The pop corresponding to the previous push. It must be applied everytime the - mode goes from Sat/Unsat to Assert. *) + (* The pop corresponding to the previous push. It must be applied everytime + the mode goes from Sat/Unsat to Assert. *) let rec pop_if_post_query st = if State.get is_decision_env st then pop 1 st (aux Util.MS.empty) @@ -1450,7 +1450,9 @@ let main () = let st = pop_if_post_query st in let st = push_before_query st in handle_query st id loc attrs contents - | { id; contents = (`Solve _ as contents); loc ; attrs; implicit=_ } -> + | { + id; contents = (`Solve _ as contents); loc ; attrs; implicit=_ + } -> cmd_on_modes st [Assert; Unsat; Sat] "check-sat"; let st = pop_if_post_query st in let st = push_before_query st in diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml index 8036729ca..f8220c7b0 100644 --- a/src/lib/reasoners/satml.ml +++ b/src/lib/reasoners/satml.ml @@ -1051,7 +1051,9 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct * let ex = * if ta.var.level = 0 then Ex.empty else * let d = - * Vec.get env.trail (Vec.get env.trail_lim (ta.var.level - 1)) + * Vec.get + * env.trail + * (Vec.get env.trail_lim (ta.var.level - 1)) * in * Ex.singleton (Ex.Literal d) * in From e02c791df8d2f8255d46f43a0277258b5e2b6e9f Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Fri, 5 Apr 2024 14:07:07 +0200 Subject: [PATCH 13/17] Reinitializing current path to avoid double replay --- src/bin/common/solving_loop.ml | 3 ++- src/lib/frontend/d_state_option.ml | 2 ++ 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 80e6f16bb..9761cbf1d 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -1174,7 +1174,6 @@ let main () = (* TODO: reset options to their initial value. *) let handle_reset st = - let () = Steps.reset_steps () in st |> State.set partial_model_key None |> State.set solver_ctx_key empty_solver_ctx @@ -1408,6 +1407,8 @@ let main () = in let rev_prefix = pop_until (n - 1) (Vec.pop pushed_paths) in let st = handle_reset st in + (* Part of the reset, the current path must be reinitialized as well. *) + let st = State.set current_path_key [] st in replay st (List.rev rev_prefix) in diff --git a/src/lib/frontend/d_state_option.ml b/src/lib/frontend/d_state_option.ml index 262e55a78..7f1c4e6ec 100644 --- a/src/lib/frontend/d_state_option.ml +++ b/src/lib/frontend/d_state_option.ml @@ -106,6 +106,8 @@ let create_opt st |> apply_hooks ~old ~new_ |> State.update_opt key (fun _ -> None) + (* S: [clear] rebuilds a new default value for the hooks, but does not put + it back on the state. *) let reset_hooks () = on_update_list := on_update_base From cf3b8a2aa0fe87a2e6b00b11a3600718d19aa59a Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Fri, 5 Apr 2024 15:47:30 +0200 Subject: [PATCH 14/17] Fix timeout issues --- src/bin/common/solving_loop.ml | 36 ++++++++++++++++++++++++++++++---- 1 file changed, 32 insertions(+), 4 deletions(-) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 9761cbf1d..7956fc4ec 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -1294,7 +1294,9 @@ let main () = st end - | {contents = `Reset; _} -> handle_reset st + | {contents = `Reset; _} -> + let () = Steps.reset_steps () in + handle_reset st | {contents = `Exit; _} -> raise Exit @@ -1386,6 +1388,13 @@ let main () = this, but it is not the case yet. *) let handle_stmt_pop_reinit all_context st l = + let has_timeout st = + let module Api = (val DO.SatSolverModule.get st) in + match Api.SAT.get_unknown_reason Api.env.sat_env with + | Some (Timeout _) -> true + | _ -> false + in + (* Pushes n times the current path. *) let push n st = let current_path = get_current_path st in @@ -1419,7 +1428,6 @@ let main () = push 1 st; State.set is_decision_env true st in - (* The pop corresponding to the previous push. It must be applied everytime the mode goes from Sat/Unsat to Assert. *) let rec pop_if_post_query st = @@ -1450,14 +1458,34 @@ let main () = cmd_on_modes st [Assert; Sat; Unsat] "goal"; let st = pop_if_post_query st in let st = push_before_query st in - handle_query st id loc attrs contents + let st = handle_query st id loc attrs contents in + let () = + if has_timeout st then + if Options.get_timelimit_per_goal () + then begin + Options.Time.start (); + Options.Time.set_timeout (Options.get_timelimit ()); + end + else exit_as_timeout () + in + st | { id; contents = (`Solve _ as contents); loc ; attrs; implicit=_ } -> cmd_on_modes st [Assert; Unsat; Sat] "check-sat"; let st = pop_if_post_query st in let st = push_before_query st in - handle_solve st id contents loc attrs + let st = handle_solve st id contents loc attrs in + let () = + if has_timeout st then + if Options.get_timelimit_per_goal () + then begin + Options.Time.start (); + Options.Time.set_timeout (Options.get_timelimit ()); + end + else exit_as_timeout () + in + st | {contents; _ } -> let st = let new_current_path = From 97353c04d15f6d03fbcbcc68adde98bca66b030a Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Fri, 5 Apr 2024 17:25:43 +0200 Subject: [PATCH 15/17] Rename function --- src/bin/common/solving_loop.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 7956fc4ec..26ee7ada1 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -1173,7 +1173,7 @@ let main () = in (* TODO: reset options to their initial value. *) - let handle_reset st = + let reset_state st = st |> State.set partial_model_key None |> State.set solver_ctx_key empty_solver_ctx @@ -1296,7 +1296,7 @@ let main () = | {contents = `Reset; _} -> let () = Steps.reset_steps () in - handle_reset st + reset_state st | {contents = `Exit; _} -> raise Exit @@ -1415,7 +1415,7 @@ let main () = pop_until (until - 1) (Vec.pop pushed_paths) in let rev_prefix = pop_until (n - 1) (Vec.pop pushed_paths) in - let st = handle_reset st in + let st = reset_state st in (* Part of the reset, the current path must be reinitialized as well. *) let st = State.set current_path_key [] st in replay st (List.rev rev_prefix) From a91b605a104b68e948478dcaeb72e360d564b940 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Fri, 5 Apr 2024 17:36:14 +0200 Subject: [PATCH 16/17] Removing unit_tenv_queue --- src/lib/reasoners/satml.ml | 6 ------ tests/smtlib/testfile-get-info1.dolmen.expected | 2 +- 2 files changed, 1 insertion(+), 7 deletions(-) diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml index f8220c7b0..042fd1c0a 100644 --- a/src/lib/reasoners/satml.ml +++ b/src/lib/reasoners/satml.ml @@ -282,8 +282,6 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct mutable tenv_queue : Th.t Vec.t; - mutable unit_tenv_queue : Th.t Vec.t; - mutable tatoms_queue : Atom.atom Queue.t; (** Queue of atoms that have been added to the [trail] through either decision or boolean propagation, but have not been otherwise processed @@ -508,8 +506,6 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct tenv_queue = Vec.make 100 ~dummy:(Th.empty()); - unit_tenv_queue = Vec.make 100 ~dummy:(Th.empty()); - tatoms_queue = Queue.create (); th_tableaux = Queue.create (); @@ -2207,7 +2203,6 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct guard.neg.is_guard <- false; cancel_until env env.next_dec_guard; Vec.push env.increm_guards guard; - Vec.push env.unit_tenv_queue env.unit_tenv; env.is_unsat_cpt <- if env.is_unsat then env.is_unsat_cpt + 1 else 0 let pop env = @@ -2215,7 +2210,6 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct let g = Vec.pop env.increm_guards in env.is_unsat <- env.is_unsat_cpt <> 0; env.is_unsat_cpt <- max 0 (env.is_unsat_cpt - 1); - env.unit_tenv <- Vec.pop env.unit_tenv_queue; g.is_guard <- false; g.neg.is_guard <- false; assert (not g.var.na.is_true); (* atom not false *) diff --git a/tests/smtlib/testfile-get-info1.dolmen.expected b/tests/smtlib/testfile-get-info1.dolmen.expected index d206212dc..bd538a3a5 100644 --- a/tests/smtlib/testfile-get-info1.dolmen.expected +++ b/tests/smtlib/testfile-get-info1.dolmen.expected @@ -1,7 +1,7 @@ unknown ( - :steps 10) + :steps 9) unsupported From a0f518e113fd1b703f2195b5f4dd13ae60cab63a Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Fri, 5 Apr 2024 17:48:42 +0200 Subject: [PATCH 17/17] Fix for another issue I need to test my PR --- src/bin/common/solving_loop.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 26ee7ada1..521ce58cc 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -488,7 +488,10 @@ let main () = recoverable_error "%t" msg; st | Util.Timeout -> Printer.print_status_timeout None None None None; - exit_as_timeout () + if (not(Options.get_timelimit_per_goal ())) then + exit_as_timeout () + else + st | Errors.Error e -> recoverable_error "%a" Errors.report e; st