wip: feat: additional clause allocators in SAT

src/sat/Sidekick_sat.ml

@@ -27,6 +27,11 @@ let pp_lbool out = function
   | L_false -> Format.fprintf out "false"
   | L_undefined -> Format.fprintf out "undefined"
 
+type 'a clause_lifetime = 'a Solver_intf.clause_lifetime =
+  | CL_keep
+  | CL_can_gc
+  | CL_use_allocator of 'a
+
 exception No_proof = Solver_intf.No_proof
 
 module Solver = Solver

src/sat/Solver_intf.ml

@@ -37,6 +37,21 @@ end
 type 'form sat_state = (module SAT_STATE with type lit = 'form)
 (** The type of values returned when the solver reaches a SAT state. *)
 
+(** Lifetime for clauses added with {!add_clause}.
+    See {!CLAUSE_ALLOCATOR} to see what allocators are
+    (here they are referred to by their index). *)
+type clause_lifetime =
+  | CL_keep
+  | CL_can_gc
+  | CL_use_allocator of {
+      allocator_idx: int;
+    }
+
+let pp_clause_lifetime out = function
+  | CL_keep -> Fmt.string out "keep"
+  | CL_can_gc -> Fmt.string out "can-gc"
+  | CL_use_allocator {allocator_idx=idx} -> Fmt.fprintf out "(custom %d)" idx
+
 module type UNSAT_STATE = sig
   type lit
   type clause
@@ -82,6 +97,31 @@ type ('lit, 'proof) reason =
 type lbool = L_true | L_false | L_undefined
 (** Valuation of an atom *)
 
+(** {2 Clause Allocators}
+
+    A clause allocator holds a set of clauses. Each clause lives in
+    exactly one clause allocator.
+
+    Each allocator is responsible for the lifetime of its clause: some will
+    keep the clauses forever (e.g. for axioms), some will GC the clauses
+    after reaching a maximum size, etc. *)
+module type CLAUSE_ALLOCATOR = sig
+  type t
+
+  type behavior
+  (** Behavior for the clause allocator *)
+
+  val gc_fixed_size : int -> behavior
+  (** GC clauses when the allocator reaches the given size *)
+
+  (* TODO: scoped allocator? different GCs? *)
+end
+
+(** Actions available to the Plugin
+
+    The plugin provides callbacks for the SAT solver to use. These callbacks
+    are provided with a [(module ACTS)] so they can modify the SAT solver
+    by adding new lemmas, raise conflicts, etc. *)
 module type ACTS = sig
   type lit
   type proof
@@ -97,11 +137,18 @@ module type ACTS = sig
   (** Map the given lit to an internal atom, which will be decided by the
       SAT solver. *)
 
-  val add_clause: ?keep:bool -> lit list -> dproof -> unit
+  val add_clause:
+    ?lifetime:clause_lifetime ->
+    lit list ->
+    dproof ->
+    unit
   (** Add a clause to the solver.
-      @param keep if true, the clause will be kept by the solver.
-        Otherwise the solver is allowed to GC the clause and propose this
+      @param lifetime lifetime to use for the clause.
+
+      - [C_keep] will make the clause unremovable
+      - [C_can_gc] the solver is allowed to GC the clause and propose this
         partial model again.
+      - [C_use_allocator alloc] puts the clause in the given allocator.
   *)
 
   val raise_conflict: lit list -> dproof -> 'b
@@ -293,6 +340,22 @@ module type S = sig
   (** Exception raised by the evaluating functions when a literal
       has not yet been assigned a value. *)
 
+  module Clause_allocator : CLAUSE_ALLOCATOR
+
+  type clause_allocator = Clause_allocator.t
+
+  val add_clause_allocator :
+    descr:string ->
+    behavior:Clause_allocator.behavior ->
+    t ->
+    clause_allocator
+  (** Make a new clause allocator for this solver.
+      @param descr short description of this allocator and what it contains
+      @param behavior controls the behavior of the allocator, i.e. whether
+      it collects clauses, which clauses are kept, what its maximum size
+      is, etc.
+  *)
+
   (** {2 Base operations} *)
 
   val assume : t -> lit list list -> unit

src/smt-solver/Sidekick_smt_solver.ml

@@ -235,10 +235,10 @@ module Make(A : ARG)
     let[@inline] propagate_l self acts p cs proof : unit =
       propagate self acts p ~reason:(fun()->cs,proof)
 
-    let add_sat_clause_ self (acts:theory_actions) ~keep lits (proof:dproof) : unit =
+    let add_sat_clause_ self (acts:theory_actions) ~lifetime lits (proof:dproof) : unit =
       let (module A) = acts in
       Stat.incr self.count_axiom;
-      A.add_clause ~keep lits proof
+      A.add_clause ~lifetime lits proof
 
     let add_sat_lit _self ?default_pol (acts:theory_actions) (lit:Lit.t) : unit =
       let (module A) = acts in