From 80bbea8952e8b3194922a8a693792103774c4956 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Thu, 16 Nov 2023 11:48:21 +0100 Subject: [PATCH] Treating step limit as an unknown reason and not a fatal error --- src/bin/js/worker_js.ml | 3 --- src/lib/frontend/frontend.ml | 16 ++++++++++++++++ src/lib/reasoners/fun_sat.ml | 2 ++ src/lib/reasoners/sat_solver_sig.ml | 1 + src/lib/reasoners/sat_solver_sig.mli | 1 + src/lib/reasoners/satml_frontend.ml | 2 ++ src/lib/structures/errors.ml | 3 --- src/lib/structures/errors.mli | 1 - src/lib/util/steps.ml | 2 +- src/lib/util/steps.mli | 4 ++-- src/lib/util/util.ml | 1 + src/lib/util/util.mli | 1 + 12 files changed, 27 insertions(+), 10 deletions(-) diff --git a/src/bin/js/worker_js.ml b/src/bin/js/worker_js.ml index b66f946fc0..eecdcb162c 100644 --- a/src/bin/js/worker_js.ml +++ b/src/bin/js/worker_js.ml @@ -181,9 +181,6 @@ let main worker_id content = 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 | _ -> returned_status := Worker_interface.Error "Error" diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index b69d7265c9..d153284314 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -32,6 +32,22 @@ open Commands open Format open Options +let timeout_reason_to_string = function + | Sat_solver_sig.Assume -> "Assume" + | ProofSearch -> "ProofSearch" + | ModelGen -> "ModelGen" + +let unknown_reason_to_string = function + | Sat_solver_sig.Incomplete -> "Incomplete" + | Memout -> "Memout" + | Steps_limit n -> Fmt.str "Step limit reached: %i" n + | Timeout t -> Fmt.str "Timeout:%s" (timeout_reason_to_string t) + +let unknown_reason_opt_to_string = + function + | None -> "Decided" + | Some r -> unknown_reason_to_string r + module E = Expr module Ex = Explanation diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index 90c67dcd32..ad0e31d4d6 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -1735,6 +1735,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 (Steps_limit n) let add_guard env gf = let current_guard = env.guards.current_guard in @@ -1753,6 +1754,7 @@ 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) 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 9caf2c4574..99b0ccc838 100644 --- a/src/lib/reasoners/sat_solver_sig.ml +++ b/src/lib/reasoners/sat_solver_sig.ml @@ -40,6 +40,7 @@ type timeout_reason = type unknown_reason = | Incomplete | Memout + | Steps_limit of int | Timeout of timeout_reason let pp_unknown_reason ppf = function diff --git a/src/lib/reasoners/sat_solver_sig.mli b/src/lib/reasoners/sat_solver_sig.mli index 4b1b7e7032..46d5587d1f 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 + | Steps_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 20cbee6343..71ca82e48f 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -1335,6 +1335,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 (Steps_limit n) | e -> Printer.print_dbg ~module_name:"Satml_frontend" ~function_name:"unsat" @@ -1350,6 +1351,7 @@ 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) (* 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 bef21f1fc1..c2f2d108f8 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 e66a5e4e36..59563364d7 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 f859a75347..d13e9ee3f2 100644 --- a/src/lib/util/steps.ml +++ b/src/lib/util/steps.ml @@ -114,7 +114,7 @@ let incr k = else if !steps > 0 then !steps else steps_bound in - Errors.run_error (Steps_limit n) + raise (Util.Step_limit_reached n) end let reset_steps () = diff --git a/src/lib/util/steps.mli b/src/lib/util/steps.mli index 33b139ea96..2753aa222f 100644 --- a/src/lib/util/steps.mli +++ b/src/lib/util/steps.mli @@ -54,7 +54,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 *) @@ -80,4 +80,4 @@ 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 fdbe3b2bae..2ac39acfac 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 9a6d6e1151..7fa2b09760 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