From ef1d4a434f468e06ecbfb2e71b5b64b0c5ecc665 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Thu, 16 Nov 2023 16:18:16 +0100 Subject: [PATCH] Tmp title: steps handling --- src/bin/common/parse_command.ml | 1 + src/bin/common/solving_loop.ml | 19 +++++++++ src/lib/reasoners/fun_sat.ml | 40 +++++++++++-------- src/lib/reasoners/satml_frontend.ml | 25 +++++++----- src/lib/util/steps.ml | 14 ++++--- src/lib/util/steps.mli | 6 +++ tests/dune.inc | 21 ++++++++++ tests/smtlib/testfile-steps-bound.dolmen.smt2 | 12 ++++++ 8 files changed, 108 insertions(+), 30 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 173529ebb9..448797ed39 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -340,10 +340,19 @@ 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 = + Steps.set_steps_bound i; + State.set steps_bound i st + in + let debug_parsed_pipe st c = if State.get State.debug st then Format.eprintf "[logic][parsed][%a] @[%a@]@." @@ -457,6 +466,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 @@ -617,6 +627,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 @@ -866,6 +884,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 457d85034a..ed0f4e0256 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -1301,10 +1301,11 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let env = do_case_split env Util.AfterMatching in if ok1 || ok2 || ok3 || ok4 then env else - update_model_and_return_unknown - env (Options.get_last_interpretation ()) - ~unknown_reason:Incomplete (* may becomes ModelGen *) - + begin + update_model_and_return_unknown + env (Options.get_last_interpretation ()) + ~unknown_reason:Incomplete (* may becomes ModelGen *) + end let normal_instantiation env try_greedy = Debug.print_nb_related env; let env = do_case_split env Util.BeforeMatching in @@ -1621,16 +1622,19 @@ 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 _ -> acc) ~max:to_push ~elt:() ~init:env @@ -1660,7 +1664,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct { acc.guards with current_guard = new_current_guard; guards = guards; - }}) + }} + ) ~max:to_pop ~elt:() ~init:env @@ -1754,7 +1759,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 a80a20a5bd..39e0efe2aa 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -1270,13 +1270,16 @@ 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 _ -> acc ) ~max:to_push ~elt:() @@ -1296,7 +1299,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct {acc with inst; guards = { acc.guards with - current_guard = b;}}) + current_guard = b;}} + ) ~max:to_pop ~elt:() ~init:env @@ -1351,7 +1355,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..419aaf93d2 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 @@ -50,6 +52,9 @@ let mult_a = ref 0 let all_steps = Stack.create () +let set_steps_bound i = steps_bound := i +let get_steps_bound () = !steps_bound + let push_steps () = Stack.push (!naive_steps,!steps,!mult_f,!mult_m, @@ -104,15 +109,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 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 3a9ff782c4..a99eb72c77 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -204172,6 +204172,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..4f62ea349c --- /dev/null +++ b/tests/smtlib/testfile-steps-bound.dolmen.smt2 @@ -0,0 +1,12 @@ +(set-logic ALL) + +(declare-const x Int) +(declare-const y Int) +(assert (= (* x x) 4)) + +; Should answer 'unknown' +(push 1) +(set-option :steps-bound 2) +(check-sat) +(get-info :reason-unknown) +(pop 1) \ No newline at end of file