From 09d37d488ec410a7adaebc39d2f478e202050007 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Thu, 16 Nov 2023 11:48:21 +0100 Subject: [PATCH 01/10] Treating step limit as an unknown reason and not a fatal error --- src/bin/common/parse_command.ml | 1 + src/bin/common/solving_loop.ml | 18 ++++++++++ src/bin/js/worker_js.ml | 9 ++--- src/lib/frontend/frontend.ml | 33 ++++++++++++++----- src/lib/reasoners/fun_sat.ml | 8 ++++- src/lib/reasoners/sat_solver_sig.ml | 2 ++ src/lib/reasoners/sat_solver_sig.mli | 1 + src/lib/reasoners/satml_frontend.ml | 25 ++++++++++---- src/lib/structures/errors.ml | 3 -- src/lib/structures/errors.mli | 1 - src/lib/util/steps.ml | 26 +++++++++++---- src/lib/util/steps.mli | 13 ++++++-- src/lib/util/util.ml | 1 + src/lib/util/util.mli | 1 + tests/dune.inc | 21 ++++++++++++ tests/smtlib/testfile-steps-bound.dolmen.smt2 | 22 +++++++++++++ 16 files changed, 150 insertions(+), 35 deletions(-) create mode 100644 tests/smtlib/testfile-steps-bound.dolmen.smt2 diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml index dfe1b3e9a..f004be9ca 100644 --- a/src/bin/common/parse_command.ml +++ b/src/bin/common/parse_command.ml @@ -362,6 +362,7 @@ let mk_limit_opt age_bound fm_cross_limit timelimit_interpretation set_fm_cross_limit fm_cross_limit; set_timelimit_interpretation timelimit_interpretation; set_steps_bound steps_bound; + Steps.set_steps_bound steps_bound; set_timelimit timelimit; set_timelimit_per_goal timelimit_per_goal; `Ok() diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index c1dd28bbf..26550924f 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -334,10 +334,26 @@ let main () = State.create_key ~pipe:"" "sat_state" in + let steps_bound: int State.key = + State.create_key ~pipe:"" "steps-bound" + in + let named_terms: DStd.Expr.term Util.MS.t State.key = State.create_key ~pipe:"" "named_terms" in + let set_steps_bound i st = + try + Steps.set_steps_bound i; + State.set steps_bound i st + with + Invalid_argument _ -> (* Raised by Steps.set_steps_bound*) + fatal_error + "Error while setting steps bound to %i: current step = %i." + i + (Steps.get_steps ()) + in + let debug_parsed_pipe st c = if State.get State.debug st then Format.eprintf "[logic][parsed][%a] @[%a@]@." @@ -471,6 +487,7 @@ let main () = State.empty |> State.set solver_ctx_key solver_ctx |> State.set partial_model_key partial_model + |> set_steps_bound (O.get_steps_bound ()) |> State.set named_terms Util.MS.empty |> DO.init |> State.init ~debug ~report_style ~reports ~max_warn ~time_limit @@ -496,6 +513,7 @@ let main () = sat; st | Tableaux | Tableaux_CDCL | CDCL | CDCL_Tableaux -> + O.set_sat_solver sat; (* `make_sat` returns the sat solver corresponding to the new sat_solver option. *) DO.SatSolver.set sat st diff --git a/src/bin/js/worker_js.ml b/src/bin/js/worker_js.ml index b66f946fc..a1d98c3b5 100644 --- a/src/bin/js/worker_js.ml +++ b/src/bin/js/worker_js.ml @@ -179,13 +179,8 @@ let main worker_id content = raise Exit | Errors.Error e -> begin match e with - | Errors.Run_error r -> begin - match r with - | Steps_limit _ -> - returned_status := - Worker_interface.LimitReached "Steps limit" - | _ -> returned_status := Worker_interface.Error "Run error" - end + | Errors.Run_error _ -> + returned_status := Worker_interface.Error "Run error" | _ -> returned_status := Worker_interface.Error "Error" end; Printer.print_err "%a" Errors.report e; diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index b69d7265c..5ccb39c46 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -302,7 +302,10 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct ignore loc; Util.loop ~f:(fun _ res () -> Stack.push res env.consistent_dep_stack) ~max:n ~elt:(env.res, env.expl) ~init:(); - {env with sat_env = SAT.push env.sat_env n} + let sat_env = + Steps.apply_without_step_limit (fun () -> SAT.push env.sat_env n) + in + {env with sat_env} let internal_pop ?(loc = Loc.dummy) (env : env) (n : int) : env = ignore loc; @@ -398,6 +401,11 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct {env with sat_env; expl} | `Unsat -> env + let check_step_limit f env = + match SAT.get_unknown_reason env.sat_env with + | Some (Step_limit _) -> env + | _ -> f env + let handle_sat_exn f ?loc env x = try f ?loc env x with | SAT.Sat t -> {env with res = `Sat t} @@ -405,19 +413,25 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct | SAT.I_dont_know t -> {env with res = `Unknown t} (* The SAT.Timeout exception is not catched. *) - let push = handle_sat_exn internal_push + (* 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 + exceptions. *) + let wrap_f f ?loc env x = + check_step_limit (fun env -> handle_sat_exn f ?loc env x) env - let pop = handle_sat_exn internal_pop + let push = wrap_f internal_push - let assume = handle_sat_exn internal_assume + let pop = wrap_f internal_pop - let pred_def = handle_sat_exn internal_pred_def + let assume = wrap_f internal_assume - let query = handle_sat_exn internal_query + let pred_def = wrap_f internal_pred_def - let th_assume = handle_sat_exn internal_th_assume + let query = wrap_f internal_query - let process_decl ?(hook_on_status=(fun _ -> ignore)) env d = + let th_assume = wrap_f internal_th_assume + + let process_decl ~hook_on_status env d = try match d.st_decl with | Push n -> internal_push ~loc:d.st_loc env n @@ -470,6 +484,9 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct hook_on_status (Timeout (Some d)) (Steps.get_steps ()); raise e + let process_decl ?(hook_on_status=(fun _ -> ignore)) env d = + check_step_limit (fun env -> process_decl ~hook_on_status env d) env + let print_model ppf env = match SAT.get_model env with | None -> diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index 90c67dcd3..66e570125 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -1630,7 +1630,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct { acc.guards with current_guard = new_guard; guards = guards; - }}) + }} + ) ~max:to_push ~elt:() ~init:env @@ -1735,6 +1736,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct assert (Ex.has_no_bj dep); dep | Util.Timeout -> model_gen_on_timeout env + | Util.Step_limit_reached n -> i_dont_know env (Step_limit n) let add_guard env gf = let current_guard = env.guards.current_guard in @@ -1753,6 +1755,10 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct (* don't attempt to compute a model if timeout before calling unsat function *) i_dont_know env (Timeout Assume) + | Util.Step_limit_reached _ -> + (* When reaching the step limit on an assume, we do not want to answer + 'unknown' right away. *) + env let pred_def env f name dep _loc = Debug.pred_def f; diff --git a/src/lib/reasoners/sat_solver_sig.ml b/src/lib/reasoners/sat_solver_sig.ml index 9caf2c457..935336565 100644 --- a/src/lib/reasoners/sat_solver_sig.ml +++ b/src/lib/reasoners/sat_solver_sig.ml @@ -40,11 +40,13 @@ type timeout_reason = type unknown_reason = | Incomplete | Memout + | Step_limit of int | Timeout of timeout_reason let pp_unknown_reason ppf = function | Incomplete -> Fmt.pf ppf "Incomplete" | Memout -> Fmt.pf ppf "Memout" + | Step_limit i -> Fmt.pf ppf "Step limit: %i" i | Timeout t -> Fmt.pf ppf "Timeout:%a" pp_timeout_reason t let pp_unknown_reason_opt ppf = function diff --git a/src/lib/reasoners/sat_solver_sig.mli b/src/lib/reasoners/sat_solver_sig.mli index 4b1b7e703..cf93a97c1 100644 --- a/src/lib/reasoners/sat_solver_sig.mli +++ b/src/lib/reasoners/sat_solver_sig.mli @@ -36,6 +36,7 @@ type timeout_reason = type unknown_reason = | Incomplete | Memout + | Step_limit of int | Timeout of timeout_reason val pp_unknown_reason: unknown_reason Fmt.t diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index 4bee0e004..772a80e8b 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -1278,13 +1278,19 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let push env to_push = Util.loop ~f:(fun _n () acc -> - let expr_guard, atom_guard = create_guard acc in - SAT.push acc.satml atom_guard; - Stack.push expr_guard acc.guards.stack_guard; - Steps.push_steps (); - {acc with guards = - {acc.guards with - current_guard = expr_guard;} } + try + let expr_guard, atom_guard = create_guard acc in + SAT.push acc.satml atom_guard; + Stack.push expr_guard acc.guards.stack_guard; + Steps.push_steps (); + {acc with guards = + {acc.guards with + current_guard = expr_guard;} } + with + | Util.Step_limit_reached _ -> + (* This function should be called without step limit + (see Steps.apply_without_step_limit) *) + assert false ) ~max:to_push ~elt:() @@ -1343,6 +1349,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct end; dep | (Util.Timeout | I_dont_know _ ) as e -> raise e + | Util.Step_limit_reached n -> i_dont_know env (Step_limit n) | e -> Printer.print_dbg ~module_name:"Satml_frontend" ~function_name:"unsat" @@ -1360,6 +1367,10 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct (* don't attempt to compute a model if timeout before calling unsat function *) i_dont_know env (Timeout Assume) *) + | Util.Step_limit_reached _ -> + (* When reaching the step limit on an assume, we do not want to + answer 'unknown' right away. *) + env (* instrumentation of relevant exported functions for profiling *) let assume t ff dep = diff --git a/src/lib/structures/errors.ml b/src/lib/structures/errors.ml index bef21f1fc..c2f2d108f 100644 --- a/src/lib/structures/errors.ml +++ b/src/lib/structures/errors.ml @@ -81,7 +81,6 @@ type typing_error = type run_error = | Invalid_steps_count of int - | Steps_limit of int | Failed_check_unsat_core | Unsupported_feature of string | Dynlink_error of string @@ -229,8 +228,6 @@ let report_typing_error fmt = function let report_run_error fmt = function | Invalid_steps_count i -> fprintf fmt "%d is not a valid number of steps" i - | Steps_limit i -> - fprintf fmt "Steps limit reached: %d" i | Failed_check_unsat_core -> fprintf fmt "Checking produced unsat-core failed" | Unsupported_feature f -> diff --git a/src/lib/structures/errors.mli b/src/lib/structures/errors.mli index e66a5e4e3..59563364d 100644 --- a/src/lib/structures/errors.mli +++ b/src/lib/structures/errors.mli @@ -88,7 +88,6 @@ type typing_error = (** Errors that can be raised at solving*) type run_error = | Invalid_steps_count of int - | Steps_limit of int | Failed_check_unsat_core | Unsupported_feature of string | Dynlink_error of string diff --git a/src/lib/util/steps.ml b/src/lib/util/steps.ml index f859a7534..21c63d289 100644 --- a/src/lib/util/steps.ml +++ b/src/lib/util/steps.ml @@ -39,6 +39,8 @@ type incr_kind = | Th_assumed of int (* Increment the counter for each term assumed in the theories environment *) +let steps_bound = ref (Options.get_steps_bound ()) + let naive_steps = ref 0 let steps = ref 0 let mult_f = ref 0 @@ -104,17 +106,16 @@ let incr k = Errors.run_error (Invalid_steps_count n); naive_steps := !naive_steps + n; end; - let steps_bound = Options.get_steps_bound () in - if steps_bound <> -1 - && ((Stdlib.compare !steps ((steps_bound)) > 0) - || (Stdlib.compare !naive_steps ((steps_bound)) > 0)) then + if !steps_bound <> -1 + && ((Stdlib.compare !steps !steps_bound > 0) + || (Stdlib.compare !naive_steps !steps_bound > 0)) then begin let n = if !naive_steps > 0 then !naive_steps else if !steps > 0 then !steps - else steps_bound + else !steps_bound in - Errors.run_error (Steps_limit n) + raise (Util.Step_limit_reached n) end let reset_steps () = @@ -158,3 +159,16 @@ let get_steps () = let cs_steps_cpt = ref 0 let cs_steps () = !cs_steps_cpt let incr_cs_steps () = Stdlib.incr cs_steps_cpt + +let set_steps_bound i = + if get_steps () > i && i >= 0 then invalid_arg "Steps.set_steps_bound"; + steps_bound := i + +let get_steps_bound () = !steps_bound + +let apply_without_step_limit cont = + let bound = !steps_bound in + steps_bound := -1; + match cont () with + | res -> steps_bound := bound; res + | exception e -> steps_bound := bound; raise e diff --git a/src/lib/util/steps.mli b/src/lib/util/steps.mli index 33b139ea9..b8d4893f5 100644 --- a/src/lib/util/steps.mli +++ b/src/lib/util/steps.mli @@ -47,6 +47,12 @@ type incr_kind = theories environment *) (** Define the type of increment *) +(** Returns the max number of bounds *) +val get_steps_bound : unit -> int + +(** Sets the max number of bounds *) +val set_steps_bound : int -> unit + val incr : incr_kind -> unit (** Increment the number of steps depending of the incr_kind @raise Errors.Error.Invalid_steps_count if the number of steps is inbound @@ -54,7 +60,7 @@ val incr : incr_kind -> unit @raise Run_error {!Errors.Invalid_steps_count} if the number of steps sent to the theories is invalid. - {!Errors.Steps_limit} if the number of steps is reached *) + @raise {!Util.Step_limit_reached} if the number of steps is reached *) val reset_steps : unit -> unit (** Reset the global steps counter *) @@ -74,10 +80,13 @@ val cs_steps : unit -> int (** Increase the number of case-split steps *) val incr_cs_steps : unit -> unit +(** Disables the step limit during the execution of the continuation. *) +val apply_without_step_limit : (unit -> 'a) -> 'a + (** {2 Incrementality} *) val push_steps : unit -> unit (** Save all the steps value in an internal stack for each push command *) val pop_steps : unit -> unit -(** Pop the last steps value when a pop command is processed *) \ No newline at end of file +(** Pop the last steps value when a pop command is processed *) diff --git a/src/lib/util/util.ml b/src/lib/util/util.ml index fdbe3b2ba..2ac39acfa 100644 --- a/src/lib/util/util.ml +++ b/src/lib/util/util.ml @@ -29,6 +29,7 @@ (**************************************************************************) exception Timeout +exception Step_limit_reached of int exception Unsolvable exception Cmp of int diff --git a/src/lib/util/util.mli b/src/lib/util/util.mli index 9a6d6e115..7fa2b0976 100644 --- a/src/lib/util/util.mli +++ b/src/lib/util/util.mli @@ -29,6 +29,7 @@ (**************************************************************************) exception Timeout +exception Step_limit_reached of int exception Unsolvable exception Cmp of int diff --git a/tests/dune.inc b/tests/dune.inc index 62c2b6d2f..8404d7382 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -204043,6 +204043,27 @@ ; Auto-generated part begin (subdir smtlib + (rule + (target testfile-steps-bound.dolmen_dolmen.output) + (deps (:input testfile-steps-bound.dolmen.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) + (rule + (deps testfile-steps-bound.dolmen_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-steps-bound.dolmen.expected testfile-steps-bound.dolmen_dolmen.output))) (rule (target testfile-reset_ci_cdcl_no_minimal_bj.output) (deps (:input testfile-reset.smt2)) diff --git a/tests/smtlib/testfile-steps-bound.dolmen.smt2 b/tests/smtlib/testfile-steps-bound.dolmen.smt2 new file mode 100644 index 000000000..be770cecf --- /dev/null +++ b/tests/smtlib/testfile-steps-bound.dolmen.smt2 @@ -0,0 +1,22 @@ +(set-logic ALL) + +(declare-const x Int) +(declare-const y Int) +(assert (= (* x x) 3)) + +; Should answer 'unknown' +(push 1) +(set-option :steps-bound 2) +(check-sat) +(get-info :reason-unknown) +(pop 1) + +(reset) + +; Should answer 'unsat' +(set-logic ALL) +(declare-const x Int) +(declare-const y Int) +(set-option :steps-bound 100) +(assert (= (* x x) 3)) +(check-sat) \ No newline at end of file From 115830a78fb61cfe4caf95314b805e8c41065098 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Tue, 21 Nov 2023 11:49:51 +0100 Subject: [PATCH 02/10] Update env when step limit is reached --- src/lib/reasoners/satml_frontend.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index 772a80e8b..afc4ef215 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -1361,16 +1361,16 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct assert (SAT.decision_level env.satml == 0); try fst (assume_aux ~dec_lvl:0 env [add_guard env gf]) with | IUnsat (_env, dep) -> raise (Unsat dep) - (* Timeout -> I_dont_know conversions temporarily disabled - https://github.com/OCamlPro/alt-ergo/issues/946 *) - (* | Util.Timeout -> - (* don't attempt to compute a model if timeout before - calling unsat function *) - i_dont_know env (Timeout Assume) *) - | Util.Step_limit_reached _ -> + (* Timeout -> I_dont_know conversions temporarily disabled + https://github.com/OCamlPro/alt-ergo/issues/946 *) + (* | Util.Timeout -> + (* don't attempt to compute a model if timeout before + calling unsat function *) + i_dont_know env (Timeout Assume) *) + | Util.Step_limit_reached n -> (* When reaching the step limit on an assume, we do not want to answer 'unknown' right away. *) - env + {env with unknown_reason = Some (Step_limit n)} (* instrumentation of relevant exported functions for profiling *) let assume t ff dep = From ecc098dd54631fd36249f463413d2c6d36dbe847 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Tue, 21 Nov 2023 11:50:52 +0100 Subject: [PATCH 03/10] Also update env in fun_sat --- src/lib/reasoners/fun_sat.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index 66e570125..64f52f625 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -1755,10 +1755,10 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct (* don't attempt to compute a model if timeout before calling unsat function *) i_dont_know env (Timeout Assume) - | Util.Step_limit_reached _ -> + | Util.Step_limit_reached n -> (* When reaching the step limit on an assume, we do not want to answer 'unknown' right away. *) - env + {env with unknown_reason = Some (Step_limit n)} let pred_def env f name dep _loc = Debug.pred_def f; From 7612d0f8a43b066781af7260b7b8d56248c6413b Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Tue, 21 Nov 2023 13:33:23 +0100 Subject: [PATCH 04/10] Rebase artifact --- src/bin/common/solving_loop.ml | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 26550924f..1b88f6b41 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -645,6 +645,12 @@ let main () = | Some b -> set_optimize b st end + | ":steps-bound", Symbol { name = Simple level; _ } -> + begin + match int_of_string_opt level with + | None -> print_wrn_opt ~name st_loc "integer" value; st + | Some i -> set_steps_bound i st + end | _ -> unsupported_opt name; st in From d7ff1db02520e169bc04dcdc15b3a155de727ca5 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Tue, 21 Nov 2023 13:33:41 +0100 Subject: [PATCH 05/10] Update frontend to handle query when unknown is already decided --- src/lib/frontend/frontend.ml | 70 ++++++++++++++++++++--------------- src/lib/frontend/frontend.mli | 2 +- 2 files changed, 42 insertions(+), 30 deletions(-) diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index 5ccb39c46..74528c047 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -142,7 +142,7 @@ module type S = sig expl : Explanation.t } - type 'a process = ?loc : Loc.t -> env -> 'a -> env + type 'a process = ?loc : Loc.t -> 'a -> env -> env val init_env : ?sat_env:sat_env -> used_context -> env @@ -226,7 +226,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct expl : Explanation.t } - type 'a process = ?loc : Loc.t -> env -> 'a -> env + type 'a process = ?loc : Loc.t -> 'a -> env -> env let init_env ?(sat_env=SAT.empty ()) used_context = { @@ -298,7 +298,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct if Options.get_unsat_core () then Ex.singleton (Ex.RootDep {name;f;loc}) else Ex.empty - let internal_push ?(loc = Loc.dummy) (env : env) (n : int) : env = + let internal_push ?(loc = Loc.dummy) (n : int) (env : env) : env = ignore loc; Util.loop ~f:(fun _ res () -> Stack.push res env.consistent_dep_stack) ~max:n ~elt:(env.res, env.expl) ~init:(); @@ -307,7 +307,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct in {env with sat_env} - let internal_pop ?(loc = Loc.dummy) (env : env) (n : int) : env = + let internal_pop ?(loc = Loc.dummy) (n : int) (env : env) : env = ignore loc; let res, expl = Util.loop ~f:(fun _n () _env -> Stack.pop env.consistent_dep_stack) @@ -318,8 +318,8 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct let internal_assume ?(loc = Loc.dummy) - (env : env) - ((name, f, mf) : string * E.t * bool) = + ((name, f, mf) : string * E.t * bool) + (env : env) = let is_hyp = try (Char.equal '@' name.[0]) with _ -> false in if not is_hyp && unused_context name env.used_context then env @@ -352,7 +352,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct in {env with sat_env; expl} - let internal_pred_def ?(loc = Loc.dummy) env (name, f) = + let internal_pred_def ?(loc = Loc.dummy) (name, f) env = if unused_context name env.used_context then env else @@ -360,7 +360,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct let sat_env = SAT.pred_def env.sat_env f name expl loc in {env with sat_env; expl} - let internal_query ?(loc = Loc.dummy) env (n, f, sort) = + let internal_query ?(loc = Loc.dummy) (n, f, sort) env = ignore loc; let expl = match env.res with @@ -389,8 +389,8 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct let internal_th_assume ?(loc = Loc.dummy) - env - ({ Expr.ax_name; Expr.ax_form ; _ } as th_elt) = + ({ Expr.ax_name; Expr.ax_form ; _ } as th_elt) + env = if unused_context ax_name env.used_context then env else @@ -406,8 +406,8 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct | Some (Step_limit _) -> env | _ -> f env - let handle_sat_exn f ?loc env x = - try f ?loc env x with + let handle_sat_exn f ?loc x env = + try f ?loc x env with | SAT.Sat t -> {env with res = `Sat t} | SAT.Unsat expl -> {env with res = `Unsat; expl = Ex.union expl env.expl} | SAT.I_dont_know t -> {env with res = `Unknown t} @@ -416,8 +416,8 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct (* 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 exceptions. *) - let wrap_f f ?loc env x = - check_step_limit (fun env -> handle_sat_exn f ?loc env x) env + let wrap_f f ?loc x env = + check_step_limit (handle_sat_exn f ?loc x) env let push = wrap_f internal_push @@ -431,24 +431,39 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct let th_assume = wrap_f internal_th_assume - let process_decl ~hook_on_status env d = + let process_decl ?(hook_on_status=(fun _ -> ignore)) env d = try match d.st_decl with - | Push n -> internal_push ~loc:d.st_loc env n - | Pop n -> internal_pop ~loc:d.st_loc env n - | Assume (n, f, mf) -> internal_assume ~loc:d.st_loc env (n, f, mf) - | PredDef (f, name) -> internal_pred_def ~loc:d.st_loc env (name, f) + | Push n -> check_step_limit (internal_push ~loc:d.st_loc n) env + | Pop n -> check_step_limit (internal_pop ~loc:d.st_loc n) env + | Assume (n, f, mf) -> + check_step_limit (internal_assume ~loc:d.st_loc (n, f, mf)) env + | PredDef (f, name) -> + check_step_limit (internal_pred_def ~loc:d.st_loc (name, f)) env | RwtDef _ -> assert false | Query (n, f, sort) -> begin - let env = internal_query ~loc:d.st_loc env (n, f, sort) in - match env.res with - | `Unsat -> - hook_on_status (Unsat (d, env.expl)) (Steps.get_steps ()); - env - | _ -> assert false + (* If we have reached an unknown state, we can return it right + away. *) + match SAT.get_unknown_reason env.sat_env with + | Some (Step_limit _) -> raise (SAT.I_dont_know env.sat_env) + | Some _ -> + (* For now, only the step limit is an unknown step reachable + here. We could raise SAT.I_dont_know as in the previous case, + but we have choosen a defensive strategy. *) + assert false + | None -> + let env = + internal_query ~loc:d.st_loc (n, f, sort) env + in + match env.res with + | `Unsat -> + hook_on_status (Unsat (d, env.expl)) (Steps.get_steps ()); + env + | _ -> assert false end - | ThAssume th_elt -> internal_th_assume ~loc:d.st_loc env th_elt + | ThAssume th_elt -> + check_step_limit (internal_th_assume ~loc:d.st_loc th_elt) env with | SAT.Sat t -> (* This case should mainly occur when a query has a non-unsat result, @@ -484,9 +499,6 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct hook_on_status (Timeout (Some d)) (Steps.get_steps ()); raise e - let process_decl ?(hook_on_status=(fun _ -> ignore)) env d = - check_step_limit (fun env -> process_decl ~hook_on_status env d) env - let print_model ppf env = match SAT.get_model env with | None -> diff --git a/src/lib/frontend/frontend.mli b/src/lib/frontend/frontend.mli index b16bd7821..40ee55128 100644 --- a/src/lib/frontend/frontend.mli +++ b/src/lib/frontend/frontend.mli @@ -68,7 +68,7 @@ module type S = sig They catch the [Sat], [Unsat] and [I_dont_know] exceptions to update the frontend environment, but not the [Timeout] exception which is raised to the user. *) - type 'a process = ?loc:Loc.t -> env -> 'a -> env + type 'a process = ?loc:Loc.t -> 'a -> env -> env val push : int process From ab9e774cc818f07bd1ea4b00a2e3b595e2ee6c18 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Tue, 21 Nov 2023 13:40:28 +0100 Subject: [PATCH 06/10] Steps as a dolmen option --- src/bin/common/solving_loop.ml | 11 ++--------- src/lib/frontend/d_state_option.ml | 6 ++++++ src/lib/frontend/d_state_option.mli | 5 +++++ 3 files changed, 13 insertions(+), 9 deletions(-) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 1b88f6b41..0408db351 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -334,20 +334,13 @@ let main () = State.create_key ~pipe:"" "sat_state" in - let steps_bound: int State.key = - State.create_key ~pipe:"" "steps-bound" - in - let named_terms: DStd.Expr.term Util.MS.t State.key = State.create_key ~pipe:"" "named_terms" in let set_steps_bound i st = - try - Steps.set_steps_bound i; - State.set steps_bound i st - with - Invalid_argument _ -> (* Raised by Steps.set_steps_bound*) + try DO.Steps.set i st with + Invalid_argument _ -> (* Raised by Steps.set_steps_bound *) fatal_error "Error while setting steps bound to %i: current step = %i." i diff --git a/src/lib/frontend/d_state_option.ml b/src/lib/frontend/d_state_option.ml index 6a6181afc..0b454cd95 100644 --- a/src/lib/frontend/d_state_option.ml +++ b/src/lib/frontend/d_state_option.ml @@ -99,6 +99,12 @@ let msatsolver = module SatSolver = (val msatsolver) +let mstate = + let on_update _ sat st = Steps.set_steps_bound sat; st in + (create_opt ~on_update "steps_bound" O.get_steps_bound) + +module Steps = (val mstate) + (* Some options can be initialized to gain some performance. *) let options_requiring_initialization = [ (module SatSolverModule : S); diff --git a/src/lib/frontend/d_state_option.mli b/src/lib/frontend/d_state_option.mli index f4989606f..56ec3d432 100644 --- a/src/lib/frontend/d_state_option.mli +++ b/src/lib/frontend/d_state_option.mli @@ -64,5 +64,10 @@ module SatSolver : S with type t = Util.sat_solver on SatSolver: when SatSolver is updated, this one also is. *) module SatSolverModule : Accessor with type t = (module Sat_solver_sig.S) +(** Option for setting the max number of steps. Interfaces with Steps. + The [set] function may raise Invalid_arg from the Steps.set_steps_bound call + if the new option value is lower than the current number of steps. *) +module Steps : S with type t = int + (** Initializes the state with options that requires some preprocessing. *) val init : D_loop.Typer.state -> D_loop.Typer.state From 0768f30b26b04f7f0b477bcd79c3070723813c11 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Tue, 21 Nov 2023 13:41:17 +0100 Subject: [PATCH 07/10] Adding missing file --- tests/smtlib/testfile-steps-bound.dolmen.expected | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 tests/smtlib/testfile-steps-bound.dolmen.expected diff --git a/tests/smtlib/testfile-steps-bound.dolmen.expected b/tests/smtlib/testfile-steps-bound.dolmen.expected new file mode 100644 index 000000000..512df716c --- /dev/null +++ b/tests/smtlib/testfile-steps-bound.dolmen.expected @@ -0,0 +1,5 @@ + +unknown +(:reason-unknown Step limit: 3) + +unsat From 14d9d91f4a64a8102541ec900becfe58b1fe670c Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Wed, 22 Nov 2023 10:35:39 +0100 Subject: [PATCH 08/10] Poetry --- src/bin/common/solving_loop.ml | 1 - src/lib/frontend/d_state_option.ml | 4 ++-- src/lib/frontend/d_state_option.mli | 3 ++- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 0408db351..37457ba98 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -480,7 +480,6 @@ let main () = State.empty |> State.set solver_ctx_key solver_ctx |> State.set partial_model_key partial_model - |> set_steps_bound (O.get_steps_bound ()) |> State.set named_terms Util.MS.empty |> DO.init |> State.init ~debug ~report_style ~reports ~max_warn ~time_limit diff --git a/src/lib/frontend/d_state_option.ml b/src/lib/frontend/d_state_option.ml index 0b454cd95..5fdf04332 100644 --- a/src/lib/frontend/d_state_option.ml +++ b/src/lib/frontend/d_state_option.ml @@ -99,11 +99,11 @@ let msatsolver = module SatSolver = (val msatsolver) -let mstate = +let msteps = let on_update _ sat st = Steps.set_steps_bound sat; st in (create_opt ~on_update "steps_bound" O.get_steps_bound) -module Steps = (val mstate) +module Steps = (val msteps) (* Some options can be initialized to gain some performance. *) let options_requiring_initialization = [ diff --git a/src/lib/frontend/d_state_option.mli b/src/lib/frontend/d_state_option.mli index 56ec3d432..70472f77a 100644 --- a/src/lib/frontend/d_state_option.mli +++ b/src/lib/frontend/d_state_option.mli @@ -64,7 +64,8 @@ module SatSolver : S with type t = Util.sat_solver on SatSolver: when SatSolver is updated, this one also is. *) module SatSolverModule : Accessor with type t = (module Sat_solver_sig.S) -(** Option for setting the max number of steps. Interfaces with Steps. +(** Option for setting the max number of steps. Interfaces with the toplevel + Steps module. The [set] function may raise Invalid_arg from the Steps.set_steps_bound call if the new option value is lower than the current number of steps. *) module Steps : S with type t = int From 97d7de90220dbc184f9780cb186804da05c11d4b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Wed, 22 Nov 2023 11:53:07 +0100 Subject: [PATCH 09/10] Print unknown reason in SMT-LIB syntax The old format is preserved for legacy messages in the Alt-Ergo format, but the SMT-LIB format is the default one for pretty-printers, since we are moving towards preferring the SMT-LIB format. Fixes #966 --- src/bin/common/solving_loop.ml | 2 +- src/lib/frontend/frontend.ml | 2 +- src/lib/reasoners/sat_solver_sig.ml | 30 +++++++++++++------ src/lib/reasoners/sat_solver_sig.mli | 5 +++- .../smtlib/testfile-get-info1.dolmen.expected | 2 +- .../testfile-steps-bound.dolmen.expected | 2 +- 6 files changed, 29 insertions(+), 14 deletions(-) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 37457ba98..b9e7fe313 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -182,7 +182,7 @@ let main () = let ur = SAT.get_unknown_reason partial_model in Printer.print_fmt (Options.Output.get_fmt_diagnostic ()) "@[Returned unknown reason = %a@]" - Sat_solver_sig.pp_unknown_reason_opt ur; + Sat_solver_sig.pp_ae_unknown_reason_opt ur; FE.print_model (Options.Output.get_fmt_models ()) partial_model end; Some mdl diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index 74528c047..2dd7690f4 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -508,7 +508,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct far. You may need to change your model generation strategy \ or to increase your timeouts. \ Returned unknown reason = %a@]" - Sat_solver_sig.pp_unknown_reason_opt ur; + Sat_solver_sig.pp_ae_unknown_reason_opt ur; | Some (lazy model) -> Models.output_concrete_model ppf model diff --git a/src/lib/reasoners/sat_solver_sig.ml b/src/lib/reasoners/sat_solver_sig.ml index 935336565..6e83f8046 100644 --- a/src/lib/reasoners/sat_solver_sig.ml +++ b/src/lib/reasoners/sat_solver_sig.ml @@ -35,7 +35,16 @@ type timeout_reason = | Assume | ProofSearch | ModelGen -[@@deriving show] + +let pp_timeout_reason ppf = function + | Assume -> Fmt.pf ppf ":assume" + | ProofSearch -> Fmt.pf ppf ":proof-search" + | ModelGen -> Fmt.pf ppf ":model-gen" + +let pp_ae_timeout_reason ppf = function + | Assume -> Fmt.pf ppf "Assume" + | ProofSearch -> Fmt.pf ppf "ProofSearch" + | ModelGen -> Fmt.pf ppf "ModelGen" type unknown_reason = | Incomplete @@ -44,14 +53,17 @@ type unknown_reason = | Timeout of timeout_reason let pp_unknown_reason ppf = function - | Incomplete -> Fmt.pf ppf "Incomplete" - | Memout -> Fmt.pf ppf "Memout" - | Step_limit i -> Fmt.pf ppf "Step limit: %i" i - | Timeout t -> Fmt.pf ppf "Timeout:%a" pp_timeout_reason t - -let pp_unknown_reason_opt ppf = function - | None -> Fmt.pf ppf "Decided" - | Some ur -> pp_unknown_reason ppf ur + | Incomplete -> Fmt.pf ppf "incomplete" + | Memout -> Fmt.pf ppf "memout" + | Step_limit i -> Fmt.pf ppf "(:step-limit %i)" i + | Timeout t -> Fmt.pf ppf "(:timeout %a)" pp_timeout_reason t + +let pp_ae_unknown_reason_opt ppf = function + | None -> Fmt.pf ppf ":decided" + | Some Incomplete -> Fmt.pf ppf "Incomplete" + | Some Memout -> Fmt.pf ppf "Memout" + | Some Step_limit i -> Fmt.pf ppf "StepLimit:%i" i + | Some Timeout t -> Fmt.pf ppf "Timeout:%a" pp_ae_timeout_reason t module type S = sig type t diff --git a/src/lib/reasoners/sat_solver_sig.mli b/src/lib/reasoners/sat_solver_sig.mli index cf93a97c1..ff5101d35 100644 --- a/src/lib/reasoners/sat_solver_sig.mli +++ b/src/lib/reasoners/sat_solver_sig.mli @@ -39,8 +39,11 @@ type unknown_reason = | Step_limit of int | Timeout of timeout_reason +(** Prints the unknown reason in the default SMT-LIB format *) val pp_unknown_reason: unknown_reason Fmt.t -val pp_unknown_reason_opt : unknown_reason option Fmt.t + +(** Prints an optional unknown reason in Alt-Ergo format *) +val pp_ae_unknown_reason_opt : unknown_reason option Fmt.t module type S = sig type t diff --git a/tests/smtlib/testfile-get-info1.dolmen.expected b/tests/smtlib/testfile-get-info1.dolmen.expected index 5b23cbed9..c1bb88b5e 100644 --- a/tests/smtlib/testfile-get-info1.dolmen.expected +++ b/tests/smtlib/testfile-get-info1.dolmen.expected @@ -8,5 +8,5 @@ unsupported (:authors "Alt-Ergo developers") (:error-behavior immediate-exit) (:name "Alt-Ergo") -(:reason-unknown Incomplete) +(:reason-unknown incomplete) (:version dev) diff --git a/tests/smtlib/testfile-steps-bound.dolmen.expected b/tests/smtlib/testfile-steps-bound.dolmen.expected index 512df716c..2c1783497 100644 --- a/tests/smtlib/testfile-steps-bound.dolmen.expected +++ b/tests/smtlib/testfile-steps-bound.dolmen.expected @@ -1,5 +1,5 @@ unknown -(:reason-unknown Step limit: 3) +(:reason-unknown (:step-limit 3)) unsat From 267f0119ee30d933c71b548ec6c660983ee36ea1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Wed, 22 Nov 2023 18:57:53 +0100 Subject: [PATCH 10/10] Address review --- src/lib/reasoners/sat_solver_sig.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/lib/reasoners/sat_solver_sig.ml b/src/lib/reasoners/sat_solver_sig.ml index 6e83f8046..c1efda916 100644 --- a/src/lib/reasoners/sat_solver_sig.ml +++ b/src/lib/reasoners/sat_solver_sig.ml @@ -36,7 +36,7 @@ type timeout_reason = | ProofSearch | ModelGen -let pp_timeout_reason ppf = function +let pp_smt_timeout_reason ppf = function | Assume -> Fmt.pf ppf ":assume" | ProofSearch -> Fmt.pf ppf ":proof-search" | ModelGen -> Fmt.pf ppf ":model-gen" @@ -56,10 +56,10 @@ let pp_unknown_reason ppf = function | Incomplete -> Fmt.pf ppf "incomplete" | Memout -> Fmt.pf ppf "memout" | Step_limit i -> Fmt.pf ppf "(:step-limit %i)" i - | Timeout t -> Fmt.pf ppf "(:timeout %a)" pp_timeout_reason t + | Timeout t -> Fmt.pf ppf "(:timeout %a)" pp_smt_timeout_reason t let pp_ae_unknown_reason_opt ppf = function - | None -> Fmt.pf ppf ":decided" + | None -> Fmt.pf ppf "Decided" | Some Incomplete -> Fmt.pf ppf "Incomplete" | Some Memout -> Fmt.pf ppf "Memout" | Some Step_limit i -> Fmt.pf ppf "StepLimit:%i" i