From 6104473a9fdb400a613484236a18ae0755ba4beb Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Mon, 27 Nov 2023 14:38:16 +0100 Subject: [PATCH 1/4] Reactivating timeouts --- src/lib/frontend/frontend.ml | 2 +- src/lib/reasoners/sat_solver_sig.ml | 3 ++ src/lib/reasoners/sat_solver_sig.mli | 1 + src/lib/reasoners/satml_frontend.ml | 78 +++++++++++++++------------- 4 files changed, 46 insertions(+), 38 deletions(-) diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index 30c71fb3c..fc34241ef 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -444,7 +444,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct (* If we have reached an unknown state, we can return it right away. *) match SAT.get_unknown_reason env.sat_env with - | Some (Step_limit _) -> raise SAT.I_dont_know + | Some (Step_limit _ | Timeout _) -> raise SAT.I_dont_know | Some _ -> (* For now, only the step limit is an unknown step reachable here. We could raise SAT.I_dont_know as in the previous case, diff --git a/src/lib/reasoners/sat_solver_sig.ml b/src/lib/reasoners/sat_solver_sig.ml index 09ac87b57..861ccd5d8 100644 --- a/src/lib/reasoners/sat_solver_sig.ml +++ b/src/lib/reasoners/sat_solver_sig.ml @@ -35,16 +35,19 @@ type timeout_reason = | Assume | ProofSearch | ModelGen + | ExnRaised of exn let pp_smt_timeout_reason ppf = function | Assume -> Fmt.pf ppf ":assume" | ProofSearch -> Fmt.pf ppf ":proof-search" | ModelGen -> Fmt.pf ppf ":model-gen" + | ExnRaised e -> Fmt.pf ppf "(:failure \"%s\")" (Printexc.to_string e) let pp_ae_timeout_reason ppf = function | Assume -> Fmt.pf ppf "Assume" | ProofSearch -> Fmt.pf ppf "ProofSearch" | ModelGen -> Fmt.pf ppf "ModelGen" + | ExnRaised e -> Fmt.pf ppf "Failure (\"%s\")" (Printexc.to_string e) type unknown_reason = | Incomplete diff --git a/src/lib/reasoners/sat_solver_sig.mli b/src/lib/reasoners/sat_solver_sig.mli index c27f3f096..176a129f4 100644 --- a/src/lib/reasoners/sat_solver_sig.mli +++ b/src/lib/reasoners/sat_solver_sig.mli @@ -32,6 +32,7 @@ type timeout_reason = | Assume | ProofSearch | ModelGen + | ExnRaised of exn type unknown_reason = | Incomplete diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index 9d5f39b94..66e4e213d 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -1001,32 +1001,44 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct may_update_last_saved_model env compute_model; Options.Time.unset_timeout (); i_dont_know env unknown_reason - (* Timeout -> I_dont_know conversions temporarily disabled - https://github.com/OCamlPro/alt-ergo/issues/946 *) - with Util.Timeout when env.model_gen_phase && false -> + with Util.Timeout when env.model_gen_phase -> (* In this case, timeout reason becomes 'ModelGen' *) i_dont_know env (Timeout ModelGen) - (* WARNING: temporary unused after the PR #950. *) - (* let model_gen_on_timeout env = - let i = Options.get_interpretation () in - let ti = Options.get_timelimit_interpretation () in - if not i || (* not asked to gen a model *) - !(env.model_gen_phase) || (* we timeouted in model-gen-phase *) - Stdlib.(=) ti 0. (* no time allocated for extra model search *) - then - i_dont_know env (Timeout ProofSearch) - else - begin - (* Beware: models generated on timeout of ProofSearch phase may - be incoherent wrt. the ground part of the pb (ie. if delta - is not empty ? *) - env.model_gen_phase := true; - Options.Time.unset_timeout (); - Options.Time.set_timeout ti; - update_model_and_return_unknown - env i ~unknown_reason:(Timeout ProofSearch) (* may becomes ModelGen *) - end *) + (* Tries to generate a model on the environment after the computation was + interrupted by a Timeout exception. + for that reason, it is impossible to guarantee the environment is sound. + A model generated by this function may not be sound at all as well. + *) + let model_gen_on_timeout env = + let i = Options.get_interpretation () in + let ti = Options.get_timelimit_interpretation () in + if not i || (* not asked to gen a model *) + env.model_gen_phase || (* we timeouted in model-gen-phase *) + Stdlib.(=) ti 0. (* no time allocated for extra model search *) + then + i_dont_know env (Timeout ProofSearch) + else + try + (* Beware: models generated on timeout of ProofSearch phase may + be incoherent wrt. the ground part of the pb (ie. if delta + is not empty ? *) + env.model_gen_phase <- true; + Options.Time.unset_timeout (); + Options.Time.set_timeout ti; + update_model_and_return_unknown + env + i + ~unknown_reason:(Timeout ProofSearch) (* may becomes ModelGen *) + with + (* We raised an exception. This can come from four sources: + - we raised I_dont_know (legit) + - we raised Timeout (Timeout on model generation, legit as weel) + - we raised Unsat -> maybe unsound, returning I_dont_know + - we broke an invaraiant because the timeout happened during a + critical instruction and now the environment is invalid. *) + | I_dont_know | Util.Timeout as e -> raise e + | e -> i_dont_know env (Timeout (ExnRaised e)) exception Give_up of (E.t * E.t * bool * bool) list @@ -1143,9 +1155,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)) - (* Timeout -> I_dont_know conversions temporarily disabled - https://github.com/OCamlPro/alt-ergo/issues/946 *) - (* | Util.Timeout -> model_gen_on_timeout env *) + | Util.Timeout -> model_gen_on_timeout env | Satml.Sat -> try do_case_split env Util.BeforeMatching; @@ -1185,9 +1195,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct unsat_rec env ~first_call:false with - (* Timeout -> I_dont_know conversions temporarily disabled - https://github.com/OCamlPro/alt-ergo/issues/946 *) - (* | 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 @@ -1196,9 +1204,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)) - (* Timeout -> I_dont_know conversions temporarily disabled - https://github.com/OCamlPro/alt-ergo/issues/946 *) - (* | Util.Timeout -> model_gen_on_timeout env *) + | Util.Timeout -> model_gen_on_timeout env end let rec unsat_rec_prem env ~first_call : unit = @@ -1337,12 +1343,10 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct assert (SAT.decision_level env.satml == 0); try ignore (assume_aux ~dec_lvl:0 env [add_guard env gf]) with | IUnsat (_env, dep) -> raise (Unsat dep) - (* Timeout -> I_dont_know conversions temporarily disabled - https://github.com/OCamlPro/alt-ergo/issues/946 *) - (* | Util.Timeout -> - (* don't attempt to compute a model if timeout before + | Util.Timeout -> + (* don't attempt to compute a model if timeout before calling unsat function *) - i_dont_know env (Timeout Assume) *) + i_dont_know env (Timeout Assume) | Util.Step_limit_reached n -> (* When reaching the step limit on an assume, we do not want to answer 'unknown' right away. *) From d9e34826b61ebb6630592be8f371858ef2a64f0e Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Mon, 27 Nov 2023 16:54:10 +0100 Subject: [PATCH 2/4] Removing model generation when timeout on satml --- src/lib/reasoners/sat_solver_sig.ml | 3 -- src/lib/reasoners/sat_solver_sig.mli | 1 - src/lib/reasoners/satml_frontend.ml | 41 ++-------------------------- 3 files changed, 3 insertions(+), 42 deletions(-) diff --git a/src/lib/reasoners/sat_solver_sig.ml b/src/lib/reasoners/sat_solver_sig.ml index 861ccd5d8..09ac87b57 100644 --- a/src/lib/reasoners/sat_solver_sig.ml +++ b/src/lib/reasoners/sat_solver_sig.ml @@ -35,19 +35,16 @@ type timeout_reason = | Assume | ProofSearch | ModelGen - | ExnRaised of exn let pp_smt_timeout_reason ppf = function | Assume -> Fmt.pf ppf ":assume" | ProofSearch -> Fmt.pf ppf ":proof-search" | ModelGen -> Fmt.pf ppf ":model-gen" - | ExnRaised e -> Fmt.pf ppf "(:failure \"%s\")" (Printexc.to_string e) let pp_ae_timeout_reason ppf = function | Assume -> Fmt.pf ppf "Assume" | ProofSearch -> Fmt.pf ppf "ProofSearch" | ModelGen -> Fmt.pf ppf "ModelGen" - | ExnRaised e -> Fmt.pf ppf "Failure (\"%s\")" (Printexc.to_string e) type unknown_reason = | Incomplete diff --git a/src/lib/reasoners/sat_solver_sig.mli b/src/lib/reasoners/sat_solver_sig.mli index 176a129f4..c27f3f096 100644 --- a/src/lib/reasoners/sat_solver_sig.mli +++ b/src/lib/reasoners/sat_solver_sig.mli @@ -32,7 +32,6 @@ type timeout_reason = | Assume | ProofSearch | ModelGen - | ExnRaised of exn type unknown_reason = | Incomplete diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index 66e4e213d..9f5115187 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -1005,41 +1005,6 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct (* In this case, timeout reason becomes 'ModelGen' *) i_dont_know env (Timeout ModelGen) - (* Tries to generate a model on the environment after the computation was - interrupted by a Timeout exception. - for that reason, it is impossible to guarantee the environment is sound. - A model generated by this function may not be sound at all as well. - *) - let model_gen_on_timeout env = - let i = Options.get_interpretation () in - let ti = Options.get_timelimit_interpretation () in - if not i || (* not asked to gen a model *) - env.model_gen_phase || (* we timeouted in model-gen-phase *) - Stdlib.(=) ti 0. (* no time allocated for extra model search *) - then - i_dont_know env (Timeout ProofSearch) - else - try - (* Beware: models generated on timeout of ProofSearch phase may - be incoherent wrt. the ground part of the pb (ie. if delta - is not empty ? *) - env.model_gen_phase <- true; - Options.Time.unset_timeout (); - Options.Time.set_timeout ti; - update_model_and_return_unknown - env - i - ~unknown_reason:(Timeout ProofSearch) (* may becomes ModelGen *) - with - (* We raised an exception. This can come from four sources: - - we raised I_dont_know (legit) - - we raised Timeout (Timeout on model generation, legit as weel) - - we raised Unsat -> maybe unsound, returning I_dont_know - - we broke an invaraiant because the timeout happened during a - critical instruction and now the environment is invalid. *) - | I_dont_know | Util.Timeout as e -> raise e - | e -> i_dont_know env (Timeout (ExnRaised e)) - exception Give_up of (E.t * E.t * bool * bool) list (* Getting [unknown] after a query can mean two things: @@ -1155,7 +1120,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 -> i_dont_know env (Timeout ProofSearch) | Satml.Sat -> try do_case_split env Util.BeforeMatching; @@ -1195,7 +1160,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 -> i_dont_know env (Timeout ProofSearch) | Satml.Unsat lc -> raise (IUnsat (env, make_explanation lc)) | Ex.Inconsistent (expl, _cls) -> (*may be raised during matching or CS*) begin @@ -1204,7 +1169,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 -> i_dont_know env (Timeout ProofSearch) end let rec unsat_rec_prem env ~first_call : unit = From aefb37b01e1669bf7f5bdf77417dd98b44369999 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Mon, 27 Nov 2023 17:52:45 +0100 Subject: [PATCH 3/4] Processing timeout on the binary side --- src/bin/common/solving_loop.ml | 8 +++++++- src/lib/frontend/frontend.ml | 18 ++++++++++-------- 2 files changed, 17 insertions(+), 9 deletions(-) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 18d03e05f..e7515b375 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -137,9 +137,15 @@ let main () = end; SAT.reset_refs (); let ftdn_env = FE.init_env used_context in + let hook_on_status status i = + Frontend.print_status status i; + match status with + | Timeout _ -> exit_as_timeout () + | _ -> () + in let () = List.iter - (FE.process_decl ~hook_on_status:Frontend.print_status ftdn_env) + (FE.process_decl ~hook_on_status ftdn_env) cnf in if Options.get_timelimit_per_goal() then diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index fc34241ef..877aa6c50 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -396,9 +396,11 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct env.expl <- expl | `Unsat -> () - let check_step_limit f env = + (** Checks whether the env can be used before actually calling the + function. *) + let check_if_over f env = match SAT.get_unknown_reason env.sat_env with - | Some (Step_limit _) -> () + | Some (Step_limit _ | Timeout _) -> () | _ -> f env let handle_sat_exn f ?loc x env = @@ -415,7 +417,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct don't do anything), and then calls the function & catches the exceptions. *) let wrap_f f ?loc x env = - check_step_limit (handle_sat_exn f ?loc x) env + check_if_over (handle_sat_exn f ?loc x) env let push = wrap_f internal_push @@ -432,12 +434,12 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct let process_decl ?(hook_on_status=(fun _ -> ignore)) env d = try match d.st_decl with - | Push n -> check_step_limit (internal_push ~loc:d.st_loc n) env - | Pop n -> check_step_limit (internal_pop ~loc:d.st_loc n) env + | Push n -> check_if_over (internal_push ~loc:d.st_loc n) env + | Pop n -> check_if_over (internal_pop ~loc:d.st_loc n) env | Assume (n, f, mf) -> - check_step_limit (internal_assume ~loc:d.st_loc (n, f, mf)) env + check_if_over (internal_assume ~loc:d.st_loc (n, f, mf)) env | PredDef (f, name) -> - check_step_limit (internal_pred_def ~loc:d.st_loc (name, f)) env + check_if_over (internal_pred_def ~loc:d.st_loc (name, f)) env | RwtDef _ -> assert false | Query (n, f, sort) -> begin @@ -458,7 +460,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct | _ -> assert false end | ThAssume th_elt -> - check_step_limit (internal_th_assume ~loc:d.st_loc th_elt) env + check_if_over (internal_th_assume ~loc:d.st_loc th_elt) env with | SAT.Sat -> (* This case should mainly occur when a query has a non-unsat result, From 0ce1664bab59d4193e7ca408bb65b3f605c9add2 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Tue, 28 Nov 2023 11:01:04 +0100 Subject: [PATCH 4/4] Poetry --- src/bin/common/solving_loop.ml | 5 ++++- src/lib/reasoners/satml_frontend.ml | 13 +++---------- 2 files changed, 7 insertions(+), 11 deletions(-) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index e7515b375..40d46ea51 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -140,7 +140,8 @@ let main () = let hook_on_status status i = Frontend.print_status status i; match status with - | Timeout _ -> exit_as_timeout () + | Timeout _ when not (Options.get_timelimit_per_goal ()) -> + exit_as_timeout () | _ -> () in let () = @@ -173,6 +174,8 @@ let main () = end | `Unsat -> None with Util.Timeout -> + (* It is still necessary to leave this catch here, because we may + trigger this exception in between calls of the sat solver. *) if not (Options.get_timelimit_per_goal()) then exit_as_timeout (); None in diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index 9f5115187..dc855e1c6 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -61,7 +61,6 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct add_inst : E.t -> bool; guards : guards; mutable last_saved_model : Models.t Lazy.t option; - mutable model_gen_phase : bool; mutable unknown_reason : Sat_solver_sig.unknown_reason option; (** The reason why satml raised [I_dont_know] if it does; [None] by default. *) @@ -95,7 +94,6 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct guards = init_guards (); add_inst = (fun _ -> true); last_saved_model = None; - model_gen_phase = false; unknown_reason = None; objectives = None } @@ -997,13 +995,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct end let update_model_and_return_unknown env compute_model ~unknown_reason = - try - may_update_last_saved_model env compute_model; - Options.Time.unset_timeout (); - i_dont_know env unknown_reason - with Util.Timeout when env.model_gen_phase -> - (* In this case, timeout reason becomes 'ModelGen' *) - i_dont_know env (Timeout ModelGen) + may_update_last_saved_model env compute_model; + Options.Time.unset_timeout (); + i_dont_know env unknown_reason exception Give_up of (E.t * E.t * bool * bool) list @@ -1256,7 +1250,6 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct assert (not (Stack.is_empty env.guards.stack_guard)); let b = Stack.top env.guards.stack_guard in Steps.pop_steps (); - env.model_gen_phase <- false; env.last_saved_model <- None; env.inst <- inst; env.guards.current_guard <- b