From a75a304d8e3be1e33a209a55866f20f7fc7ecf8e Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Thu, 16 Nov 2023 16:18:16 +0100 Subject: [PATCH] Adding utils to steps for properly handling step errors --- src/bin/common/parse_command.ml | 1 + src/bin/common/solving_loop.ml | 26 +++++++++++++++ src/lib/reasoners/fun_sat.ml | 33 ++++++++++++------- src/lib/reasoners/satml_frontend.ml | 26 ++++++++++----- src/lib/util/steps.ml | 17 +++++++--- src/lib/util/steps.mli | 6 ++++ tests/dune.inc | 21 ++++++++++++ tests/smtlib/testfile-steps-bound.dolmen.smt2 | 22 +++++++++++++ 8 files changed, 128 insertions(+), 24 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 dfe1b3e9ae..f004be9ca6 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 26990849e2..2db78d1233 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -351,10 +351,26 @@ let main () = State.create_key ~pipe:"" "produce_assignment" 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@]@." @@ -491,6 +507,7 @@ let main () = |> State.set partial_model_key partial_model |> State.set optimize_key (O.get_optimize ()) |> State.set produce_assignment false + |> set_steps_bound (O.get_steps_bound ()) |> State.set named_terms Util.MS.empty |> State.init ~debug ~report_style ~reports ~max_warn ~time_limit ~size_limit ~response_file @@ -651,6 +668,14 @@ let main () = | Some b -> set_optimize b st end + | ":steps-bound", Symbol { name = Simple n; _ } -> + begin + match int_of_string_opt n with + | None -> + print_wrn_opt ~name st_loc "integer" value; + st + | Some i -> set_steps_bound i st + end | _ -> unsupported_opt name; st in @@ -890,6 +915,7 @@ let main () = |> State.set solver_ctx_key empty_solver_ctx |> State.set optimize_key (O.get_optimize ()) |> State.set produce_assignment false + |> set_steps_bound (O.get_steps_bound ()) |> State.set named_terms Util.MS.empty | {contents = `Exit; _} -> raise Exit diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index ad0e31d4d6..46b5ba43c6 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -1621,16 +1621,24 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct ); Util.loop ~f:(fun _n () acc -> - let new_guard = E.fresh_name Ty.Tbool in - save_guard_and_refs acc new_guard; - let guards = ME.add new_guard - (mk_gf new_guard "" true true,Ex.empty) - acc.guards.guards in - {acc with guards = - { acc.guards with - current_guard = new_guard; - guards = guards; - }}) + try + let new_guard = E.fresh_name Ty.Tbool in + save_guard_and_refs acc new_guard; + let guards = ME.add new_guard + (mk_gf new_guard "" true true,Ex.empty) + acc.guards.guards in + {acc with guards = + { acc.guards with + current_guard = new_guard; + guards = guards; + }} + with + | Util.Step_limit_reached _ -> + (* If we reached the step limit while pushing, we have to cancel the + push. + TODO: properly cancel the push. *) + env + ) ~max:to_push ~elt:() ~init:env @@ -1754,7 +1762,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 n -> i_dont_know env (Steps_limit n) + | 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/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index 71ca82e48f..3f4e76ee29 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -1270,13 +1270,20 @@ 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 _ -> + (* If we reached the step limit while pushing, we have to cancel the + push. + TODO: properly cancel the push. *) + env ) ~max:to_push ~elt:() @@ -1351,7 +1358,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 n -> i_dont_know env (Steps_limit n) + | 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/util/steps.ml b/src/lib/util/steps.ml index d13e9ee3f2..3e2f685121 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,15 +106,14 @@ 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 raise (Util.Step_limit_reached n) end @@ -158,3 +159,9 @@ 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 diff --git a/src/lib/util/steps.mli b/src/lib/util/steps.mli index 2753aa222f..3fbe4ed2c6 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 diff --git a/tests/dune.inc b/tests/dune.inc index 62c2b6d2f6..8404d7382a 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 0000000000..be770cecfc --- /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