feat(smt): provide SAT solver to theories upon initialization

src/core/Sidekick_core.ml

@@ -954,6 +954,18 @@ module type SOLVER = sig
   type dproof = proof -> unit
   (** Delayed proof. This is used to build a proof step on demand. *)
 
+  (** The internal SAT solver *)
+  module Sat_solver : sig
+    type clause_pool_id = Clause_pool_id.t
+    type t
+
+    val new_clause_pool_gc_fixed_size :
+      descr:string ->
+      size:int ->
+      t ->
+      clause_pool_id
+  end
+
   (** {3 A theory}
 
       Theories are abstracted over the concrete implementation of the solver,
@@ -976,7 +988,7 @@ module type SOLVER = sig
     val name : string
     (** Name of the theory (ideally, unique and short) *)
 
-    val create_and_setup : Solver_internal.t -> t
+    val create_and_setup : Solver_internal.t -> Sat_solver.t -> t
     (** Instantiate the theory's state for the given (internal) solver,
         register callbacks, create keys, etc.
 
@@ -1004,7 +1016,7 @@ module type SOLVER = sig
 
   val mk_theory :
     name:string ->
-    create_and_setup:(Solver_internal.t -> 'th) ->
+    create_and_setup:(Solver_internal.t -> Sat_solver.t -> 'th) ->
     ?push_level:('th -> unit) ->
     ?pop_levels:('th -> int -> unit) ->
     unit ->

src/lra/sidekick_arith_lra.ml

@@ -601,7 +601,7 @@ module Make(A : ARG) : S with module A = A = struct
       T.Tbl.add self.needs_th_combination t ()
     )
 
-  let create_and_setup si =
+  let create_and_setup si _ =
     Log.debug 2 "(th-lra.setup)";
     let stat = SI.stats si in
     let st = create ~stat (SI.tst si) (SI.ty_st si) in

src/sat/Solver_intf.ml

@@ -222,7 +222,7 @@ module type S = sig
 
   type clause
 
-  type clause_pool_id
+  type clause_pool_id = Clause_pool_id.t
   (** Pool of clauses, with its own lifetime management *)
 
   type theory

src/smt-solver/Sidekick_smt_solver.ml

@@ -567,7 +567,7 @@ module Make(A : ARG)
   module type THEORY = sig
     type t
     val name : string
-    val create_and_setup : Solver_internal.t -> t
+    val create_and_setup : Solver_internal.t -> Sat_solver.t -> t
     val push_level : t -> unit
     val pop_levels : t -> int -> unit
   end
@@ -581,7 +581,7 @@ module Make(A : ARG)
     let (module Th) = th in
     Log.debugf 2
       (fun k-> k "(@[smt-solver.add-theory@ :name %S@])" Th.name);
-    let st = Th.create_and_setup self.si in
+    let st = Th.create_and_setup self.si self.solver in
     (* add push/pop to the internal solver *)
     begin
       let open Solver_internal in

src/smtlib/Process.ml

@@ -57,7 +57,7 @@ module Check_cc = struct
 
   let theory =
     Solver.mk_theory ~name:"cc-check"
-      ~create_and_setup:(fun si ->
+      ~create_and_setup:(fun si _sat ->
           let n_calls = Stat.mk_int (Solver.Solver_internal.stats si) "check-cc.call" in
           Solver.Solver_internal.on_cc_conflict si
             (fun cc ~th c ->

src/th-bool-static/Sidekick_th_bool_static.ml

@@ -355,7 +355,7 @@ module Make(A : ARG) : S with module A = A = struct
     end;
     ()
 
-  let create_and_setup si =
+  let create_and_setup si _sat =
     Log.debug 2 "(th-bool.setup)";
     let st = create (SI.tst si) (SI.ty_st si) in
     SI.add_simplifier si (simplify st);

src/th-cstor/Sidekick_th_cstor.ml

@@ -83,7 +83,7 @@ module Make(A : ARG) : S with module A = A = struct
   let push_level = ST.push_level
   let pop_levels = ST.pop_levels
 
-  let create_and_setup (solver:SI.t) : t =
+  let create_and_setup (solver:SI.t) _ : t =
     Log.debug 1 "(setup :th-cstor)";
     let self = ST.create_and_setup ~size:32 solver in
     self

src/th-data/Sidekick_th_data.ml

@@ -662,7 +662,7 @@ module Make(A : ARG) : S with module A = A = struct
       let t = A.mk_cstor self.tst c.c_cstor args in
       Some t
 
-  let create_and_setup (solver:SI.t) : t =
+  let create_and_setup (solver:SI.t) _ : t =
     let self = {
       tst=SI.tst solver;
       cstors=ST_cstors.create_and_setup ~size:32 solver;