From 29c3841c30a59a2bbfce5616d676782fcf8a6964 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Tue, 14 Nov 2023 11:08:07 +0100 Subject: [PATCH] Revert "Save a timeout reason in the exception Util.Timeout" This reverts commit dbfed1b65a7636a359e7aee22d03713018529070. --- src/bin/common/solving_loop.ml | 27 +++++++++------------------ src/lib/frontend/frontend.ml | 2 +- src/lib/reasoners/fun_sat.ml | 8 ++++---- src/lib/reasoners/sat_solver_sig.ml | 10 ++++++++-- src/lib/reasoners/sat_solver_sig.mli | 7 ++++++- src/lib/reasoners/satml_frontend.ml | 14 +++++++------- src/lib/util/options.ml | 2 +- src/lib/util/util.ml | 9 +-------- src/lib/util/util.mli | 9 +-------- 9 files changed, 38 insertions(+), 50 deletions(-) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index af038f564..b3e6aed97 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -73,16 +73,7 @@ let recoverable_error ?(code = 1) = let fatal_error ?(code = 1) = Format.kasprintf (fun msg -> recoverable_error ~code "%s" msg; exit code) -let print_timeout_reason tr = - match tr with - | Some tr -> - Printer.print_fmt (Options.Output.get_fmt_diagnostic ()) - "@[; Returned timeout reason = %a@]" Util.pp_timeout_reason tr; - | None -> () - -let exit_as_timeout tr = - print_timeout_reason tr; - fatal_error ~code:142 "timeout" +let exit_as_timeout () = fatal_error ~code:142 "timeout" let warning (msg : ('a, Format.formatter, unit, unit, unit, 'b) format6) : 'a = if Options.get_warning_as_error () then @@ -219,8 +210,8 @@ let main () = Some mdl end | `Unsat -> None - with Util.Timeout tr -> - if not (Options.get_timelimit_per_goal()) then exit_as_timeout tr; + with Util.Timeout -> + if not (Options.get_timelimit_per_goal()) then exit_as_timeout (); None in @@ -299,9 +290,9 @@ let main () = Stdcompat.Seq.append theory_preludes @@ I.parse_files ~filename ~preludes with - | Util.Timeout tr -> + | Util.Timeout -> Frontend.print_status (Timeout None) 0; - exit_as_timeout tr + exit_as_timeout () | Parsing.Parse_error -> (* TODO(Steven): displaying a dummy value is a bad idea. This should only be executed with the legacy frontend, which should @@ -346,9 +337,9 @@ let main () = let parsed_seq = parsed () in let _ : _ state = Seq.fold_left typing_loop state parsed_seq in Options.Time.unset_timeout (); - with Util.Timeout tr -> + with Util.Timeout -> Frontend.print_status (Timeout None) 0; - exit_as_timeout tr + exit_as_timeout () in let solver_ctx_key: solver_ctx State.key = @@ -398,9 +389,9 @@ let main () = let handle_exn st bt = function | Dolmen.Std.Loc.Syntax_error (_, `Regular msg) -> recoverable_error "%t" msg; st - | Util.Timeout tr -> + | Util.Timeout -> Printer.print_status_timeout None None None None; - exit_as_timeout tr + exit_as_timeout () | Errors.Error e -> recoverable_error "%a" Errors.report e; st diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index c07a721f1..7ccc2c3b5 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -462,7 +462,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct (* if timeout != NoTimeout then raise Util.Timeout; *) {env with res = `Unknown t} - | Util.Timeout _ as e -> + | Util.Timeout as e -> (* In this case, we obviously want to print the status, since we exit right after *) hook_on_status (Timeout (Some d)) (Steps.get_steps ()); diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index 541291c09..9df7efe6a 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -1138,7 +1138,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let env = may_update_last_saved_model env compute_model in Options.Time.unset_timeout (); i_dont_know env unknown_reason - with Util.Timeout _ when !(env.model_gen_phase) -> + with Util.Timeout when !(env.model_gen_phase) -> (* In this case, timeout reason becomes 'ModelGen' *) i_dont_know env (Timeout ModelGen) @@ -1415,7 +1415,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct with No_suitable_decision -> back_tracking (normal_instantiation env true) with - | Util.Timeout _ -> model_gen_on_timeout env + | Util.Timeout -> model_gen_on_timeout env and make_one_decision env = try @@ -1734,7 +1734,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct Debug.unsat (); assert (Ex.has_no_bj dep); dep - | Util.Timeout _ -> model_gen_on_timeout env + | Util.Timeout -> model_gen_on_timeout env let add_guard env gf = let current_guard = env.guards.current_guard in @@ -1749,7 +1749,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct | IUnsat (d, classes) -> Debug.bottom classes; raise (Unsat d) - | Util.Timeout _ -> + | Util.Timeout -> (* don't attempt to compute a model if timeout before calling unsat function *) i_dont_know env (Timeout Assume) diff --git a/src/lib/reasoners/sat_solver_sig.ml b/src/lib/reasoners/sat_solver_sig.ml index e842a1bf9..9caf2c457 100644 --- a/src/lib/reasoners/sat_solver_sig.ml +++ b/src/lib/reasoners/sat_solver_sig.ml @@ -31,15 +31,21 @@ (* We put an ml file for the module type, to avoid issues when building the lib *) +type timeout_reason = + | Assume + | ProofSearch + | ModelGen +[@@deriving show] + type unknown_reason = | Incomplete | Memout - | Timeout of Util.timeout_reason + | Timeout of timeout_reason let pp_unknown_reason ppf = function | Incomplete -> Fmt.pf ppf "Incomplete" | Memout -> Fmt.pf ppf "Memout" - | Timeout t -> Fmt.pf ppf "Timeout:%a" Util.pp_timeout_reason t + | Timeout t -> Fmt.pf ppf "Timeout:%a" pp_timeout_reason t let pp_unknown_reason_opt ppf = function | None -> Fmt.pf ppf "Decided" diff --git a/src/lib/reasoners/sat_solver_sig.mli b/src/lib/reasoners/sat_solver_sig.mli index 6a1c9423b..4b1b7e703 100644 --- a/src/lib/reasoners/sat_solver_sig.mli +++ b/src/lib/reasoners/sat_solver_sig.mli @@ -28,10 +28,15 @@ (* *) (**************************************************************************) +type timeout_reason = + | Assume + | ProofSearch + | ModelGen + type unknown_reason = | Incomplete | Memout - | Timeout of Util.timeout_reason + | Timeout of timeout_reason val pp_unknown_reason: unknown_reason Fmt.t val pp_unknown_reason_opt : unknown_reason option Fmt.t diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index e30da6188..f9a00f5ea 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -1014,7 +1014,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let env = may_update_last_saved_model env compute_model in Options.Time.unset_timeout (); i_dont_know env unknown_reason - with Util.Timeout _ when !(env.model_gen_phase) -> + with Util.Timeout when !(env.model_gen_phase) -> (* In this case, timeout reason becomes 'ModelGen' *) i_dont_know env (Timeout ModelGen) @@ -1153,7 +1153,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct try SAT.solve env.satml; assert false with | Satml.Unsat lc -> raise (IUnsat (env, make_explanation lc)) - | Util.Timeout _ -> model_gen_on_timeout env + | Util.Timeout -> model_gen_on_timeout env | Satml.Sat -> try @@ -1197,7 +1197,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct unsat_rec env ~first_call:false with - | Util.Timeout _ -> model_gen_on_timeout env + | Util.Timeout -> model_gen_on_timeout env | Satml.Unsat lc -> raise (IUnsat (env, make_explanation lc)) | Ex.Inconsistent (expl, _cls) -> (*may be raised during matching or CS*) begin @@ -1206,7 +1206,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct unsat_rec env ~first_call:false with | Satml.Unsat lc -> raise (IUnsat (env, make_explanation lc)) - | Util.Timeout _ -> model_gen_on_timeout env + | Util.Timeout -> model_gen_on_timeout env end let rec unsat_rec_prem env ~first_call : unit = @@ -1223,7 +1223,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct side-effect to best value *) raise (I_dont_know env) end - | Util.Timeout _ as e -> raise e + | Util.Timeout as e -> raise e | IUnsat (env, _) as e -> if !(env.objectives) == None then raise e; @@ -1334,7 +1334,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct )dep true end; dep - | (Util.Timeout _ | I_dont_know _ ) as e -> raise e + | (Util.Timeout | I_dont_know _ ) as e -> raise e | e -> Printer.print_dbg ~module_name:"Satml_frontend" ~function_name:"unsat" @@ -1346,7 +1346,7 @@ 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) - | Util.Timeout _ -> + | Util.Timeout -> (* don't attempt to compute a model if timeout before calling unsat function *) i_dont_know env (Timeout Assume) diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml index 68dda4f17..a23a762e3 100644 --- a/src/lib/util/options.ml +++ b/src/lib/util/options.ml @@ -600,7 +600,7 @@ let thread_yield = ref (fun () -> ()) let set_thread_yield f = thread_yield := f let (timeout : (unit -> unit) ref) = - ref (fun () -> raise (Util.Timeout (Some Signal))) + ref (fun () -> raise Util.Timeout) let set_timeout f = timeout := f diff --git a/src/lib/util/util.ml b/src/lib/util/util.ml index f607ab56e..fdbe3b2ba 100644 --- a/src/lib/util/util.ml +++ b/src/lib/util/util.ml @@ -28,14 +28,7 @@ (* *) (**************************************************************************) -type timeout_reason = - | Assume - | ProofSearch - | ModelGen - | Signal -[@@deriving show] - -exception Timeout of timeout_reason option +exception Timeout exception Unsolvable exception Cmp of int diff --git a/src/lib/util/util.mli b/src/lib/util/util.mli index 2fab15ac3..9a6d6e115 100644 --- a/src/lib/util/util.mli +++ b/src/lib/util/util.mli @@ -28,14 +28,7 @@ (* *) (**************************************************************************) -type timeout_reason = - | Assume - | ProofSearch - | ModelGen - | Signal -[@@deriving show] - -exception Timeout of timeout_reason option +exception Timeout exception Unsolvable exception Cmp of int