Reactivating timeouts

Stevendeo · Nov 27, 2023 · 0762819 · 0762819
1 parent 7363cd0
commit 0762819
Show file tree

Hide file tree

Showing 4 changed files with 43 additions and 38 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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. *)