diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index 30c71fb3ca..fc34241ef2 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 09ac87b574..861ccd5d82 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 c27f3f096b..176a129f46 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 9d5f39b946..40d274ec0a 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -1001,32 +1001,41 @@ 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 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 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 +1152,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 +1192,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 +1201,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 +1340,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. *)