feat: check on_progress in more places

src/sat/Sidekick_sat.ml

@@ -28,6 +28,7 @@ let pp_lbool out = function
   | L_undefined -> Format.fprintf out "undefined"
 
 exception No_proof = Solver_intf.No_proof
+exception Resource_exhausted = Solver_intf.Resource_exhausted
 
 module Solver = Solver
 module Make_cdcl_t = Solver.Make_cdcl_t

src/sat/Solver.ml

@@ -2184,7 +2184,7 @@ module Make(Plugin : PLUGIN)
 
   (* do some amount of search, until the number of conflicts or clause learnt
      reaches the given parameters *)
-  let search (st:t) ~(max_conflicts:int) : unit =
+  let search (st:t) ~on_progress ~(max_conflicts:int) : unit =
     Log.debugf 3
       (fun k->k "(@[sat.search@ :max-conflicts %d@ :max-learnt %d@])"
           max_conflicts !(st.max_clauses_learnt));
@@ -2224,6 +2224,7 @@ module Make(Plugin : PLUGIN)
         in
         if do_gc then (
           reduce_clause_db st;
+          on_progress();
         );
 
         let decided = pick_branch_lit ~full:true st in
@@ -2258,7 +2259,7 @@ module Make(Plugin : PLUGIN)
         on_progress();
         begin try
             self.max_clauses_learnt := int_of_float !max_learnt ;
-            search self ~max_conflicts:(int_of_float !max_conflicts)
+            search self ~on_progress ~max_conflicts:(int_of_float !max_conflicts)
           with
           | Restart ->
             max_conflicts := !max_conflicts *. restart_inc;
@@ -2267,6 +2268,7 @@ module Make(Plugin : PLUGIN)
             assert (self.elt_head = AVec.size self.trail &&
                     has_no_delayed_actions self &&
                     self.next_decisions=[]);
+            on_progress();
             begin match Plugin.final_check self.th (full_slice self) with
               | () ->
                 if self.elt_head = AVec.size self.trail &&
@@ -2287,6 +2289,7 @@ module Make(Plugin : PLUGIN)
                 (match self.on_conflict with Some f -> f self c | None -> ());
                 Delayed_actions.add_clause_learnt self.delayed_actions c;
                 perform_delayed_actions self;
+                on_progress();
             end;
         end
       done

src/sat/Solver_intf.ml

@@ -230,6 +230,9 @@ module type PLUGIN_SAT = sig
      and type proof_step = proof_step
 end
 
+exception Resource_exhausted
+(** Can be raised in a progress handler *)
+
 (** The external interface implemented by safe solvers, such as the one
     created by the {!Solver.Make} and {!Mcsolver.Make} functors. *)
 module type S = sig
@@ -387,7 +390,11 @@ module type S = sig
       @param assumptions additional atomic assumptions to be temporarily added.
         The assumptions are just used for this call to [solve], they are
         not saved in the solver's state.
-      @param on_progress regularly called during solving
+      @param on_progress regularly called during solving.
+        Can raise {!Resource_exhausted}
+        to stop solving.
+
+      @raise Resource_exhausted if the on_progress handler raised it to stop
   *)
 
   (** {2 Evaluating and adding literals} *)

src/smt-solver/Sidekick_smt_solver.ml

@@ -907,7 +907,7 @@ module Make(A : ARG)
               )));
     Model.Map model
 
-  exception Should_stop
+  exception Resource_exhausted = Sidekick_sat.Resource_exhausted
 
   let solve
       ?(on_exit=[]) ?(check=true)
@@ -924,7 +924,7 @@ module Make(A : ARG)
       fun() ->
         incr resource_counter;
         on_progress self;
-        if should_stop self !resource_counter then raise_notrace Should_stop
+        if should_stop self !resource_counter then raise_notrace Resource_exhausted
     in
     self.si.on_progress <- on_progress;
 
@@ -961,7 +961,7 @@ module Make(A : ARG)
         let unsat_proof_step () = Some (UNSAT.unsat_proof()) in
         do_on_exit ();
         Unsat {unsat_core; unsat_proof_step}
-      | exception Should_stop -> Unknown Unknown.U_asked_to_stop
+      | exception Resource_exhausted -> Unknown Unknown.U_asked_to_stop
     in
     self.last_res <- Some res;
     res