Save a timeout reason in the exception Util.Timeout

In some situations, we need to retrieve the reason of a timeout in the
binary but we have no environment of the SAT solver in these locations.

I add an argument to the timeout exception to save its reason.

src/bin/common/solving_loop.ml

@@ -73,7 +73,16 @@ let recoverable_error ?(code = 1) =
 let fatal_error ?(code = 1) =
   Format.kasprintf (fun msg -> recoverable_error ~code "%s" msg; exit code)
 
-let exit_as_timeout () = fatal_error ~code:142 "timeout"
+let print_timeout_reason tr =
+  match tr with
+  | Some tr ->
+    Printer.print_fmt (Options.Output.get_fmt_diagnostic ())
+      "@[<v 0>; 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 warning (msg : ('a, Format.formatter, unit, unit, unit, 'b) format6) : 'a =
   if Options.get_warning_as_error () then
@@ -210,8 +219,8 @@ let main () =
           Some mdl
         end
       | `Unsat -> None
-    with Util.Timeout ->
-      if not (Options.get_timelimit_per_goal()) then exit_as_timeout ();
+    with Util.Timeout tr ->
+      if not (Options.get_timelimit_per_goal()) then exit_as_timeout tr;
       None
   in
 
@@ -290,9 +299,9 @@ let main () =
         Stdcompat.Seq.append theory_preludes @@
         I.parse_files ~filename ~preludes
       with
-      | Util.Timeout ->
+      | Util.Timeout tr ->
         Frontend.print_status (Timeout None) 0;
-        exit_as_timeout ()
+        exit_as_timeout tr
       | Parsing.Parse_error ->
         (* TODO(Steven): displaying a dummy value is a bad idea.
            This should only be executed with the legacy frontend, which should
@@ -337,9 +346,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 ->
+    with Util.Timeout tr ->
       Frontend.print_status (Timeout None) 0;
-      exit_as_timeout ()
+      exit_as_timeout tr
   in
 
   let solver_ctx_key: solver_ctx State.key =
@@ -389,9 +398,9 @@ let main () =
   let handle_exn st bt = function
     | Dolmen.Std.Loc.Syntax_error (_, `Regular msg) ->
       recoverable_error "%t" msg; st
-    | Util.Timeout ->
+    | Util.Timeout tr ->
       Printer.print_status_timeout None None None None;
-      exit_as_timeout ()
+      exit_as_timeout tr
     | Errors.Error e ->
       recoverable_error "%a" Errors.report e;
       st

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 ());

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)

src/lib/reasoners/sat_solver_sig.ml

@@ -31,21 +31,15 @@
 (* 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 timeout_reason
+  | Timeout of Util.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" pp_timeout_reason t
+  | Timeout t -> Fmt.pf ppf "Timeout:%a" Util.pp_timeout_reason t
 
 let pp_unknown_reason_opt ppf = function
   | None -> Fmt.pf ppf "Decided"

src/lib/reasoners/sat_solver_sig.mli

@@ -28,15 +28,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
-type timeout_reason =
-  | Assume
-  | ProofSearch
-  | ModelGen
-
 type unknown_reason =
   | Incomplete
   | Memout
-  | Timeout of timeout_reason
+  | Timeout of Util.timeout_reason
 
 val pp_unknown_reason: unknown_reason Fmt.t
 val pp_unknown_reason_opt : unknown_reason option Fmt.t

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)

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)
+  ref (fun () -> raise (Util.Timeout (Some Signal)))
 
 let set_timeout f = timeout := f
 

src/lib/util/util.ml

@@ -28,7 +28,14 @@
 (*                                                                        *)
 (**************************************************************************)
 
-exception Timeout
+type timeout_reason =
+  | Assume
+  | ProofSearch
+  | ModelGen
+  | Signal
+[@@deriving show]
+
+exception Timeout of timeout_reason option
 exception Unsolvable
 
 exception Cmp of int

src/lib/util/util.mli

@@ -28,7 +28,14 @@
 (*                                                                        *)
 (**************************************************************************)
 
-exception Timeout
+type timeout_reason =
+  | Assume
+  | ProofSearch
+  | ModelGen
+  | Signal
+[@@deriving show]
+
+exception Timeout of timeout_reason option
 exception Unsolvable
 
 exception Cmp of int