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