Removing Sat/Unsat/I_dont_know exceptions from the Sat solvers API

src/lib/frontend/frontend.ml

@@ -87,6 +87,18 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
     | Timeout of Commands.sat_tdecl option
     | Preprocess
 
+  exception SAT of SAT.t
+  exception UNSAT of Explanation.t
+  exception I_DONT_KNOW of SAT.t
+
+  (** Returns the environment if the API call was successful
+      (i.e., returned 'Done'). Otherwise, raises an exceptio*)
+  let process_sat_res : SAT.res -> SAT.t = function
+    | Done t -> t
+    | Sat t -> raise (SAT t)
+    | Unsat e -> raise (UNSAT e)
+    | I_dont_know t -> raise (I_DONT_KNOW t)
+
   let output_used_context g_name dep =
     if not (Options.get_js_mode ()) then begin
       let f = Options.get_used_context_file () in
@@ -108,20 +120,26 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
       let env =
         List.fold_left
           (fun env f ->
-             SAT.assume env
-               {E.ff=f;
-                origin_name = "";
-                gdist = -1;
-                hdist = -1;
-                trigger_depth = max_int;
-                nb_reductions = 0;
-                age=0;
-                lem=None;
-                mf=false;
-                gf=false;
-                from_terms = [];
-                theory_elim = true;
-               } Ex.empty
+             match
+               SAT.assume env
+                 {E.ff=f;
+                  origin_name = "";
+                  gdist = -1;
+                  hdist = -1;
+                  trigger_depth = max_int;
+                  nb_reductions = 0;
+                  age=0;
+                  lem=None;
+                  mf=false;
+                  gf=false;
+                  from_terms = [];
+                  theory_elim = true;
+                 } Ex.empty
+             with
+             | Done e -> e
+             | Sat t -> raise (SAT t)
+             | Unsat e -> raise (UNSAT e)
+             | I_dont_know t -> raise (I_DONT_KNOW t)
           ) (SAT.empty ()) pb
       in
       ignore (SAT.unsat
@@ -141,8 +159,11 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
                 });
       Errors.run_error Errors.Failed_check_unsat_core
     with
-    | SAT.Unsat _  -> ()
-    | (SAT.Sat _ | SAT.I_dont_know _) as e -> raise e
+    | UNSAT _  -> ()
+    | SAT _ | I_DONT_KNOW _ as e ->
+      (* Useless line, but keeping it to ease the reading. These should be the
+         only exceptions raised. *)
+      raise e
 
 
   let unused_context name context =
@@ -177,6 +198,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
           begin
             match consistent with
             | `Sat _ | `Unknown _ ->
+              process_sat_res @@
               SAT.assume env
                 {E.ff=f;
                  origin_name = n;
@@ -199,28 +221,38 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
         if unused_context name used_context then acc
         else
           let dep = mk_root_dep name f d.st_loc in
-          SAT.pred_def env f name dep d.st_loc, consistent, dep
+          process_sat_res @@ SAT.pred_def env f name dep d.st_loc,
+          consistent,
+          dep
 
       | RwtDef _ -> assert false
 
       | Query(n, f, sort) ->
         let dep =
           match consistent with
           | `Sat _ | `Unknown _ ->
-            let dep' = SAT.unsat env
-                {E.ff=f;
-                 origin_name = n;
-                 hdist = -1;
-                 gdist = 0;
-                 trigger_depth = max_int;
-                 nb_reductions = 0;
-                 age=0;
-                 lem=None;
-                 mf=(sort != Check);
-                 gf=true;
-                 from_terms = [];
-                 theory_elim = true;
-                } in
+            let dep' =
+              match
+                SAT.unsat env
+                  {E.ff=f;
+                   origin_name = n;
+                   hdist = -1;
+                   gdist = 0;
+                   trigger_depth = max_int;
+                   nb_reductions = 0;
+                   age=0;
+                   lem=None;
+                   mf=(sort != Check);
+                   gf=true;
+                   from_terms = [];
+                   theory_elim = true;
+                  }
+              with
+              | Unsat d -> d
+              | Done t | I_dont_know t ->
+                raise (I_DONT_KNOW t)
+              | Sat t -> raise (SAT t)
+            in
             Ex.union dep' dep
           | `Unsat -> dep
         in
@@ -236,27 +268,26 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
           match consistent with
           | `Sat _ | `Unknown _ ->
             let dep = mk_root_dep ax_name ax_form d.st_loc in
-            let env = SAT.assume_th_elt env th_elt dep in
+            let env = process_sat_res @@ SAT.assume_th_elt env th_elt dep in
             env, consistent, dep
           | `Unsat ->
             env, consistent, dep
-
     with
-    | SAT.Sat t ->
+    | SAT t ->
       (* This case should mainly occur when a query has a non-unsat result,
          so we want to print the status in this case. *)
       print_status (Sat (d,t)) (Steps.get_steps ());
       (*if get_model () then SAT.print_model ~header:true (get_fmt_mdl ()) t;*)
       env, `Sat t, dep
-    | SAT.Unsat dep' ->
+    | UNSAT dep' ->
       (* This case should mainly occur when a new assumption results in an unsat
          env, in which case we do not want to print status, since the correct
          status should be printed at the next query. *)
       let dep = Ex.union dep dep' in
       if get_debug_unsat_core () then check_produced_unsat_core dep;
       (* print_status (Inconsistent d) (Steps.get_steps ()); *)
       env, `Unsat, dep
-    | SAT.I_dont_know t ->
+    | I_DONT_KNOW t ->
       (* In this case, it's not clear whether we want to print the status.
          Instead, it'd be better to accumulate in `consistent` a 3-case adt
          and not a simple bool. *)

src/lib/reasoners/fun_sat.ml

@@ -196,11 +196,24 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     { env with
       unit_facts_cache = ref refs.unit_facts}, guard
 
-  exception Sat of t
+  exception Sat of t [@@warning "-38"]
   exception Unsat of Ex.t
   exception I_dont_know of t
   exception IUnsat of Ex.t * SE.t list
 
+  type res =
+    | Done of t
+    | Sat of t
+    | Unsat of Explanation.t
+    | I_dont_know of t
+
+  let safe_call f =
+    try
+      Done (f ())
+    with
+    | Sat t -> Sat t
+    | Unsat e -> Unsat e
+    | I_dont_know t -> I_dont_know t
 
   (*BISECT-IGNORE-BEGIN*)
   module Debug = struct
@@ -1803,7 +1816,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     let current_guard = env.guards.current_guard in
     {gf with E.ff = E.mk_imp current_guard gf.E.ff}
 
-  let assume env fg dep =
+  let unsafe_assume env fg dep =
     try
       if Options.get_tableaux_cdcl () then
         cdcl_assume false env [add_guard env fg,dep];
@@ -1815,7 +1828,6 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
       raise (Unsat d)
     | Util.Timeout when switch_to_model_gen env -> do_switch_to_model_gen env
 
-
   let pred_def env f name dep _loc =
     Debug.pred_def f;
     let gf = mk_gf f name true false in
@@ -1824,6 +1836,10 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
       inst =
         Inst.add_predicate env.inst ~guard ~name gf dep }
 
+  let pred_def env f name dep _loc = safe_call (fun () -> pred_def env f name dep _loc)
+
+  let unsat env fg = safe_call (fun () -> raise (Unsat (unsat env fg)))
+
   let unsat env fg =
     if Options.get_timers() then
       try
@@ -1836,17 +1852,19 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
         raise e
     else unsat env fg
 
-  let assume env fg =
+  let safe_assume env fg ex = safe_call (fun () -> unsafe_assume env fg ex)
+
+  let assume env fg ex =
     if Options.get_timers() then
       try
         Timers.exec_timer_start Timers.M_Sat Timers.F_assume;
-        let env = assume env fg in
+        let env = safe_assume env fg ex in
         Timers.exec_timer_pause Timers.M_Sat Timers.F_assume;
         env
       with e ->
         Timers.exec_timer_pause Timers.M_Sat Timers.F_assume;
         raise e
-    else assume env fg
+    else safe_assume env fg ex
 
   let empty_guards () = {
     current_guard = Expr.vrai;
@@ -1893,7 +1911,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
       add_inst = fun _ -> true;
     }
     in
-    assume env gf_true Ex.empty
+    unsafe_assume env gf_true Ex.empty
   (*maybe usefull when -no-theory is on*)
 
   let empty_with_inst add_inst =
@@ -1902,6 +1920,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
   let assume_th_elt env th_elt dep =
     {env with tbox = Th.assume_th_elt env.tbox th_elt dep}
 
+  let assume_th_elt env th_elt dep =
+    safe_call (fun () -> assume_th_elt env th_elt dep)
+
   let reinit_ctx () =
     (* all_models_sat_env := None; *)
     latest_saved_env := None;

src/lib/reasoners/sat_solver_sig.ml

@@ -34,9 +34,11 @@
 module type S = sig
   type t
 
-  exception Sat of t
-  exception Unsat of Explanation.t
-  exception I_dont_know of t
+  type res =
+    | Done of t
+    | Sat of t
+    | Unsat of Explanation.t
+    | I_dont_know of t
 
   (* the empty sat-solver context *)
   val empty : unit -> t
@@ -56,17 +58,17 @@ module type S = sig
 
   (* [assume env f] assume a new formula [f] in [env]. Raises Unsat if
      [f] is unsatisfiable in [env] *)
-  val assume : t -> Expr.gformula -> Explanation.t -> t
+  val assume : t -> Expr.gformula -> Explanation.t -> res
 
-  val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t
+  val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> res
 
   (* [pred_def env f] assume a new predicate definition [f] in [env]. *)
-  val pred_def : t -> Expr.t -> string -> Explanation.t -> Loc.t -> t
+  val pred_def : t -> Expr.t -> string -> Explanation.t -> Loc.t -> res
 
   (* [unsat env f size] checks the unsatisfiability of [f] in
      [env]. Raises I_dont_know when the proof tree's height reaches
      [size]. Raises Sat if [f] is satisfiable in [env] *)
-  val unsat : t -> Expr.gformula -> Explanation.t
+  val unsat : t -> Expr.gformula -> res
 
   val reset_refs : unit -> unit
 

src/lib/reasoners/sat_solver_sig.mli

@@ -31,9 +31,11 @@
 module type S = sig
   type t
 
-  exception Sat of t
-  exception Unsat of Explanation.t
-  exception I_dont_know of t
+  type res =
+    | Done of t
+    | Sat of t
+    | Unsat of Explanation.t
+    | I_dont_know of t
 
   (** the empty sat-solver context *)
   val empty : unit -> t
@@ -53,19 +55,19 @@ module type S = sig
 
   (** [assume env f] assume a new formula [f] in [env]. Raises Unsat if
       [f] is unsatisfiable in [env] *)
-  val assume : t -> Expr.gformula -> Explanation.t -> t
+  val assume : t -> Expr.gformula -> Explanation.t -> res
 
   (** [assume env f exp] assume a new formula [f] with the explanation [exp]
       in the theories environment of [env]. *)
-  val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t
+  val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> res
 
   (** [pred_def env f] assume a new predicate definition [f] in [env]. *)
-  val pred_def : t -> Expr.t -> string -> Explanation.t -> Loc.t -> t
+  val pred_def : t -> Expr.t -> string -> Explanation.t -> Loc.t -> res
 
   (** [unsat env f size] checks the unsatisfiability of [f] in
       [env]. Raises I_dont_know when the proof tree's height reaches
       [size]. Raises Sat if [f] is satisfiable in [env] *)
-  val unsat : t -> Expr.gformula -> Explanation.t
+  val unsat : t -> Expr.gformula -> res
 
   (** [print_model header fmt env] print propositional model and theory model
       on the corresponding fmt. *)