feat(api): add callbacks to measure progress or ask solver to stop

src/core/Sidekick_core.ml

@@ -961,7 +961,7 @@ module type SOLVER_INTERNAL = sig
   (** Add a hook that will be called when a model is being produced *)
 end
 
-(** User facing view of the solver
+(** User facing view of the solver.
 
     This is the solver a user of sidekick can see, after instantiating
     everything. The user can add some theories, clauses, etc. and asks
@@ -1164,6 +1164,7 @@ module type SOLVER = sig
     ?on_exit:(unit -> unit) list ->
     ?check:bool ->
     ?on_progress:(t -> unit) ->
+    ?should_stop:(t -> int -> bool) ->
     assumptions:lit list ->
     t ->
     res
@@ -1172,6 +1173,11 @@ module type SOLVER = sig
       @param on_progress called regularly during solving.
       @param assumptions a set of atoms held to be true. The unsat core,
         if any, will be a subset of [assumptions].
+      @param should_stop a callback regularly called with the solver,
+        and with a number of "steps" done since last call. The exact notion
+        of step is not defined, but is guaranteed to increase regularly.
+        The function should return [true] if it judges solving
+        must stop (returning [Unknown]), [false] if solving can proceed.
       @param on_exit functions to be run before this returns *)
 
   (* TODO: allow on_progress to return a bool to know whether to stop? *)

src/sat/Solver.ml

@@ -2125,7 +2125,7 @@ module Make(Plugin : PLUGIN)
 
   (* fixpoint of propagation and decisions until a model is found, or a
      conflict is reached *)
-  let solve_ (self:t) : unit =
+  let solve_ ~on_progress (self:t) : unit =
     Log.debugf 5 (fun k->k "(@[sat.solve :assms %d@])" (AVec.size self.assumptions));
     check_unsat_ self;
     try
@@ -2133,6 +2133,7 @@ module Make(Plugin : PLUGIN)
       let max_conflicts = ref (float_of_int restart_first) in
       let max_learnt = ref ((float_of_int (nb_clauses self)) *. learntsize_factor) in
       while true do
+        on_progress();
         begin try
             self.max_clauses_learnt := int_of_float !max_learnt ;
             search self ~max_conflicts:(int_of_float !max_conflicts)
@@ -2341,7 +2342,9 @@ module Make(Plugin : PLUGIN)
     Vec.push self.clause_pools p;
     Clause_pool_id._unsafe_of_int id
 
-  let solve ?(assumptions=[]) (self:t) : res =
+  let solve
+      ?(on_progress=fun _ -> ())
+      ?(assumptions=[]) (self:t) : res =
     cancel_until self 0;
     AVec.clear self.assumptions;
     List.iter
@@ -2350,7 +2353,7 @@ module Make(Plugin : PLUGIN)
          AVec.push self.assumptions a)
       assumptions;
     try
-      solve_ self;
+      solve_ ~on_progress self;
       Sat (mk_sat self)
     with E_unsat us ->
       (* FIXME

src/sat/Solver_intf.ml

@@ -378,12 +378,15 @@ module type S = sig
   (* TODO: API to push/pop/clear assumptions from an inner vector *)
 
   val solve :
+    ?on_progress:(unit -> unit) ->
     ?assumptions:lit list ->
     t -> res
   (** Try and solves the current set of clauses.
       @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. *)
+        not saved in the solver's state.
+      @param on_progress regularly called during solving
+  *)
 
   val add_lit : t -> ?default_pol:bool -> lit -> unit
   (** Ensure the SAT solver handles this particular literal, ie add

src/smt-solver/DESIGN.md

@@ -1,148 +0,0 @@
-
-## CC with eval
-
-evaluation should be based on a form of conditional rewriting for first-order
-symbols.
-
-### Terms
-
-Roughly:
-
-```ocaml
-type t = {
-  id: int;
-  ty: ty;
-  repr: ty_repr;
-}
-and ty_repr =
-  | App of cst * t array
-  | Custom of {
-    view: term_view;
-    tc: term_tc;
-  } (** Custom theory stuff (e.g. LRA polynomial) *)
-
-(* typeclass for evaluation *)
-and term_tc = {
-  t_pp : term_view printer;
-  t_map : (t -> t) -> term_view -> term_view;
-  t_children : term_view -> t Bag.t;
-  t_equal : term_view -> term_view -> bool;
-  t_hash : term_view -> int;
-}
-
-and term_view = ..
-```
-
-Constants and types are also extensible:
-
-
-```ocaml
-type ty = {
-  ty_id : int;
-  ty_repr: ty_repr;
-}
-and ty_repr =
-  | Bool
-  | Arrow of ty list * ty
-  | Var of db
-  | Forall of ty (* polymorphic type *)
-  | Ty_custom of {
-    view: ty_view;
-    tc: ty_tc
-  } (** Extensible case *)
-and ty_tc = {
-  ty_pp : term_view printer;
-  ty_equal : term_view -> term_view -> bool;
-  ty_hash : term_view -> int;
-}
-and ty_view = ..
-```
-
-and
-
-```ocaml
-type cst = {
-  cst_id: ID.t;
-  cst_ty: Ty.t;
-  cst_decl: decl_view;
-  cst_rules: rule list;
-  cst_fields: Fields.t;
-  (* assoc, comm, injective, etc? *)
-}
-
-(** Per-theory custom info for the constant *)
-and decl_view = ..
-
-(** A rewrite rule *)
-and rule = {
-  r_guards: decl_view -> args:t array -> Lit.t list;
-  r_rhs: decl_view -> args:term array -> term;
-}
-
-```
-
-### Example : ite
-
-If-then-else (`ite`) would be a special constant of type `Πα. bool -> α → α → α`
-and two rules:
-
-```ocaml
-[ {r_guards=(fun _ [cond;_;_] -> [Lit.of_term cond]);
-   r_rhs=(fun _ [_;a;_] -> a);
-  };
-  {r_guards=(fun _ [cond;_;_] -> [Lit.neg @@ Lit.of_term cond]);
-   r_rhs=(fun _ [_;_;b] -> b);
-  };
-]
-```
-
-The first rule will fire if `cond` is true, and reduce `(ite cond a b)` into `a`;
-the second rule fires if `¬cond` is true, and reduces to `b`.
-
-Rules should be pairwise exclusive (i.e. the conjunction of guards of
-any two rules must be unsat)
-
-### Congruence closure
-
-Classic CC with additional support for injectivity, etc.
-
-- injectivity based on flag on `cst` heads
-- mutual exclusion of constructors (for datatypes)
-- → need notion of "value" (extensible, per theory/per type)
-    such as at most one value per equiv. class, and values *never* reduce.
-- notion of relevancy for evaluation (and SAT literals).
-  E.g. in `ite cond a b`, only `cond` is relevant. `a` and `b` only become
-  relevant when the term reduces to either of them.
-  → also allows control of evaluation under datatypes
-  (in `S(n)`, `n` can only become relevant if a projection/match/function call
-   brings it into a relevant context by removing `S` ⇒ emulate WHNF)
-
-Given a *relevant* node of the CC, of the form `f t1…tn`, where `f` has evaluation
-rules:
-
-- we instantiate all literals in the guards of the rules (to know which
-  rule applies).
-- if all literals in the guard of one of the rules applies, then the rule
-  fires.
-  * We *replace* `f t1…tn` by RHS of the rule applied
-    to `f` and `repr(t1)…repr(tn)`, and flag `f t1…tn` as masked.
-  * It remains in the equivalence class, but points directly to its new
-    normal form and should not participate in regular congruence checking.
-  * Upon backtrack (as soon as the guard is not true anymore) we restore
-    the old term and make it active again.
-
-It's very important that, in a long chain of reduction `t1 → t2 → … → tn`,
-only `tn` is active and the other terms are only there to provide explanations
-but do not cost any complexity during CC.
-
-## Theories
-
-- have `x+2y+z` be arith terms
-- shostak like canonizer (turns equations into `x := …`)
-- use same evaluation mechanism as for evaluation of terms,
-  for dynamic simplifications (rewriting).
-  * no preprocessing, everything done dynamically
-  * theory terms subscribe to their arguments (subterms) to potentially
-    rewrite themselves if their arguments change
-    e.g.  `x+y+1` subscribes to {x,y} so as to reduce to `y+z+3` when
-    x:=z+2 happens

src/smt-solver/Sidekick_smt_solver.ml

@@ -733,11 +733,13 @@ module Make(A : ARG)
       | U_timeout
       | U_max_depth
       | U_incomplete
+      | U_asked_to_stop
 
     let pp out = function
       | U_timeout -> Fmt.string out "timeout"
       | U_max_depth -> Fmt.string out "max depth reached"
       | U_incomplete -> Fmt.string out "incomplete fragment"
+      | U_asked_to_stop -> Fmt.string out "asked to stop by callback"
   end [@@ocaml.warning "-37"]
 
   module Model = struct
@@ -860,17 +862,31 @@ module Make(A : ARG)
               )));
     Model.Map model
 
-  let solve ?(on_exit=[]) ?(check=true) ?(on_progress=fun _ -> ())
+  exception Should_stop
+
+  let solve
+      ?(on_exit=[]) ?(check=true)
+      ?(on_progress=fun _ -> ())
+      ?(should_stop=fun _ _ -> false)
       ~assumptions (self:t) : res =
     Profile.with_ "smt-solver.solve" @@ fun () ->
     let do_on_exit () =
       List.iter (fun f->f()) on_exit;
     in
-    self.si.on_progress <- (fun () -> on_progress self);
 
-    let r = Sat_solver.solve ~assumptions (solver self) in
-    Stat.incr self.count_solve;
-    match r with
+    let on_progress =
+      let resource_counter = ref 0 in
+      fun() ->
+        incr resource_counter;
+        on_progress self;
+        if should_stop self !resource_counter then raise_notrace Should_stop
+    in
+    self.si.on_progress <- on_progress;
+
+    match
+      Stat.incr self.count_solve;
+      Sat_solver.solve ~on_progress ~assumptions (solver self)
+    with
     | Sat_solver.Sat (module SAT) ->
       Log.debug 1 "(sidekick.smt-solver: SAT)";
 
@@ -895,6 +911,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
 
   let mk_theory (type st)
       ~name ~create_and_setup