diff --git a/src/smt/dune b/src/smt/dune
index 0e86c9da..f6d84486 100644
--- a/src/smt/dune
+++ b/src/smt/dune
@@ -3,5 +3,5 @@
  (public_name sidekick.smt-solver)
  (synopsis "main SMT solver")
  (libraries containers iter sidekick.core sidekick.util sidekick.cc
-   sidekick.sat)
+   sidekick.sat sidekick.simplify)
  (flags :standard -w +32 -open Sidekick_util))
diff --git a/src/smt/model.ml b/src/smt/model.ml
index 34cba314..d7f0ad6b 100644
--- a/src/smt/model.ml
+++ b/src/smt/model.ml
@@ -22,3 +22,7 @@ let pp out = function
     in
     Fmt.fprintf out "(@[<hv>model@ %a@])" (Util.pp_iter pp_pair)
       (Term.Tbl.to_iter tbl)
+
+module Internal_ = struct
+  let of_tbl t = Map t
+end
diff --git a/src/smt/model.mli b/src/smt/model.mli
new file mode 100644
index 00000000..bcabd13c
--- /dev/null
+++ b/src/smt/model.mli
@@ -0,0 +1,18 @@
+(** Models
+
+      A model can be produced when the solver is found to be in a
+      satisfiable state after a call to {!solve}. *)
+
+open Sigs
+
+type t
+
+val empty : t
+val mem : t -> term -> bool
+val find : t -> term -> term option
+val eval : t -> term -> term option
+val pp : t Fmt.printer
+
+module Internal_ : sig
+  val of_tbl : term Term.Tbl.t -> t
+end
diff --git a/src/smt/sigs.ml b/src/smt/sigs.ml
index fb0ba9b6..20ee7b04 100644
--- a/src/smt/sigs.ml
+++ b/src/smt/sigs.ml
@@ -13,6 +13,7 @@
 *)
 
 include Sidekick_core
+module Simplify = Sidekick_simplify
 module CC = Sidekick_cc.CC
 module E_node = Sidekick_cc.E_node
 module CC_expl = Sidekick_cc.Expl
diff --git a/src/smt/simplify.ml b/src/smt/simplify.ml
deleted file mode 100644
index 2bbd3da8..00000000
--- a/src/smt/simplify.ml
+++ /dev/null
@@ -1,81 +0,0 @@
-open Sidekick_core
-open Sigs
-
-open struct
-  module P = Proof_trace
-  module Rule_ = Proof_core
-end
-
-type t = {
-  tst: term_store;
-  proof: proof_trace;
-  mutable hooks: hook list;
-  (* store [t --> u by step_ids] in the cache.
-     We use a bag for the proof steps because it gives us structural
-     sharing of subproofs. *)
-  cache: (Term.t * step_id Bag.t) Term.Tbl.t;
-}
-
-and hook = t -> term -> (term * step_id Iter.t) option
-
-let create tst ~proof : t =
-  { tst; proof; hooks = []; cache = Term.Tbl.create 32 }
-
-let[@inline] tst self = self.tst
-let[@inline] proof self = self.proof
-let add_hook self f = self.hooks <- f :: self.hooks
-let clear self = Term.Tbl.clear self.cache
-
-let normalize (self : t) (t : Term.t) : (Term.t * step_id) option =
-  (* compute and cache normal form of [t] *)
-  let rec loop t : Term.t * _ Bag.t =
-    match Term.Tbl.find self.cache t with
-    | res -> res
-    | exception Not_found ->
-      let steps_u = ref Bag.empty in
-      let u = aux_rec ~steps:steps_u t self.hooks in
-      Term.Tbl.add self.cache t (u, !steps_u);
-      u, !steps_u
-  and loop_add ~steps t =
-    let u, pr_u = loop t in
-    steps := Bag.append !steps pr_u;
-    u
-  (* try each function in [hooks] successively, and rewrite subterms *)
-  and aux_rec ~steps t hooks : Term.t =
-    match hooks with
-    | [] ->
-      let u =
-        Term.map_shallow self.tst ~f:(fun _inb u -> loop_add ~steps u) t
-      in
-      if Term.equal t u then
-        t
-      else
-        loop_add ~steps u
-    | h :: hooks_tl ->
-      (match h self t with
-      | None -> aux_rec ~steps t hooks_tl
-      | Some (u, _) when Term.equal t u -> aux_rec ~steps t hooks_tl
-      | Some (u, pr_u) ->
-        let bag_u = Bag.of_iter pr_u in
-        steps := Bag.append !steps bag_u;
-        let v, pr_v = loop u in
-        (* fixpoint *)
-        steps := Bag.append !steps pr_v;
-        v)
-  in
-  let u, pr_u = loop t in
-  if Term.equal t u then
-    None
-  else (
-    (* proof: [sub_proofs |- t=u] by CC + subproof *)
-    let step =
-      P.add_step self.proof
-      @@ Rule_.lemma_preprocess t u ~using:(Bag.to_iter pr_u)
-    in
-    Some (u, step)
-  )
-
-let normalize_t self t =
-  match normalize self t with
-  | Some (u, pr_u) -> u, Some pr_u
-  | None -> t, None
diff --git a/src/smt/simplify.mli b/src/smt/simplify.mli
deleted file mode 100644
index 4ecccd29..00000000
--- a/src/smt/simplify.mli
+++ /dev/null
@@ -1,39 +0,0 @@
-(** Term simplifier *)
-
-open Sidekick_core
-open Sigs
-
-type t
-
-val tst : t -> term_store
-
-val clear : t -> unit
-(** Reset internal cache, etc. *)
-
-val proof : t -> proof_trace
-(** Access proof *)
-
-type hook = t -> term -> (term * step_id Iter.t) option
-(** Given a term, try to simplify it. Return [None] if it didn't change.
-
-        A simple example could be a hook that takes a term [t],
-        and if [t] is [app "+" (const x) (const y)] where [x] and [y] are number,
-        returns [Some (const (x+y))], and [None] otherwise.
-
-        The simplifier will take care of simplifying the resulting term further,
-        caching (so that work is not duplicated in subterms), etc.
-    *)
-
-val add_hook : t -> hook -> unit
-
-val normalize : t -> term -> (term * step_id) option
-(** Normalize a term using all the hooks. This performs
-    a fixpoint, i.e. it only stops when no hook applies anywhere inside
-    the term. *)
-
-val normalize_t : t -> term -> term * step_id option
-(** Normalize a term using all the hooks, along with a proof that the
-    simplification is correct.
-    returns [t, ø] if no simplification occurred. *)
-
-val create : Term.store -> proof:Proof_trace.t -> t
diff --git a/src/smt/solver.ml b/src/smt/solver.ml
index f4741fb8..670a5630 100644
--- a/src/smt/solver.ml
+++ b/src/smt/solver.ml
@@ -1,6 +1,7 @@
 open Sigs
 
 open struct
+  module SI = Solver_internal
   module P = Proof_trace
   module Rule_ = Proof_core
 end
@@ -30,7 +31,7 @@ end
      end)
 *)
 
-module Sat_solver = Sidekick_sat.Make_cdcl_t (Solver_internal)
+module Sat_solver = Sidekick_sat
 (** the parametrized SAT Solver *)
 
 (** {2 Result} *)
@@ -100,7 +101,7 @@ let create arg ?(stat = Stat.global) ?size ~proof ~theories tst () : t =
       si;
       proof;
       last_res = None;
-      solver = Sat_solver.create ~proof ?size ~stat si;
+      solver = Sat_solver.create ~proof ?size ~stat (SI.to_sat_plugin si);
       stat;
       count_clause = Stat.mk_int stat "solver.add-clause";
       count_solve = Stat.mk_int stat "solver.solve";
@@ -127,11 +128,11 @@ let reset_last_res_ self = self.last_res <- None
 (* preprocess clause, return new proof *)
 let preprocess_clause_ (self : t) (c : lit array) (pr : step_id) :
     lit array * step_id =
-  Solver_internal.preprocess_clause_iarray_ self.si c pr
+  Solver_internal.preprocess_clause_array self.si c pr
 
 let mk_lit_t (self : t) ?sign (t : term) : lit =
   let lit = Lit.atom ?sign t in
-  let lit, _ = Solver_internal.simplify_and_preproc_lit_ self.si lit in
+  let lit, _ = Solver_internal.simplify_and_preproc_lit self.si lit in
   lit
 
 (** {2 Main} *)
@@ -171,16 +172,14 @@ let add_clause (self : t) (c : lit array) (proof : step_id) : unit =
 let add_clause_l self c p = add_clause self (CCArray.of_list c) p
 
 let assert_terms self c =
-  let c = CCList.map (fun t -> Lit.atom (tst self) t) c in
+  let c = CCList.map Lit.atom c in
   let pr_c =
-    P.add_step self.proof @@ A.Rule_sat.sat_input_clause (Iter.of_list c)
+    P.add_step self.proof @@ Proof_sat.sat_input_clause (Iter.of_list c)
   in
   add_clause_l self c pr_c
 
 let assert_term self t = assert_terms self [ t ]
 
-exception Resource_exhausted = Sidekick_sat.Resource_exhausted
-
 let solve ?(on_exit = []) ?(check = true) ?(on_progress = fun _ -> ())
     ?(should_stop = fun _ _ -> false) ~assumptions (self : t) : res =
   Profile.with_ "smt-solver.solve" @@ fun () ->
@@ -194,14 +193,14 @@ let solve ?(on_exit = []) ?(check = true) ?(on_progress = fun _ -> ())
       if should_stop self !resource_counter then
         raise_notrace Resource_exhausted
   in
-  self.si.on_progress <- on_progress;
+  Event.on ~f:on_progress (SI.on_progress self.si);
 
   let res =
     match
       Stat.incr self.count_solve;
       Sat_solver.solve ~on_progress ~assumptions (solver self)
     with
-    | Sat_solver.Sat _ when not self.si.complete ->
+    | Sat_solver.Sat _ when not (SI.is_complete self.si) ->
       Log.debugf 1 (fun k ->
           k
             "(@[sidekick.smt-solver: SAT@ actual: UNKNOWN@ :reason \
@@ -212,14 +211,14 @@ let solve ?(on_exit = []) ?(check = true) ?(on_progress = fun _ -> ())
 
       Log.debugf 5 (fun k ->
           let ppc out n =
-            Fmt.fprintf out "{@[<hv>class@ %a@]}" (Util.pp_iter N.pp)
-              (N.iter_class n)
+            Fmt.fprintf out "{@[<hv>class@ %a@]}" (Util.pp_iter E_node.pp)
+              (E_node.iter_class n)
           in
           k "(@[sidekick.smt-solver.classes@ (@[%a@])@])" (Util.pp_iter ppc)
             (CC.all_classes @@ Solver_internal.cc self.si));
 
       let m =
-        match self.si.last_model with
+        match SI.last_model self.si with
         | Some m -> m
         | None -> assert false
       in
diff --git a/src/smt/solver.mli b/src/smt/solver.mli
index b645adb6..97628abd 100644
--- a/src/smt/solver.mli
+++ b/src/smt/solver.mli
@@ -14,32 +14,15 @@ type t
 val registry : t -> Registry.t
 (** A solver contains a registry so that theories can share data *)
 
-type theory = Theory.t
-type 'a theory_p = 'a Theory.p
-
 val mk_theory :
   name:string ->
   create_and_setup:(Solver_internal.t -> 'th) ->
   ?push_level:('th -> unit) ->
   ?pop_levels:('th -> int -> unit) ->
   unit ->
-  theory
+  Theory.t
 (** Helper to create a theory. *)
 
-(** Models
-
-      A model can be produced when the solver is found to be in a
-      satisfiable state after a call to {!solve}. *)
-module Model : sig
-  type t
-
-  val empty : t
-  val mem : t -> term -> bool
-  val find : t -> term -> term option
-  val eval : t -> term -> term option
-  val pp : t Fmt.printer
-end
-
 (* TODO *)
 module Unknown : sig
   type t
@@ -65,7 +48,7 @@ val create :
   ?size:[ `Big | `Tiny | `Small ] ->
   (* TODO? ?config:Config.t -> *)
   proof:proof_trace ->
-  theories:theory list ->
+  theories:Theory.t list ->
   Term.store ->
   unit ->
   t
@@ -82,15 +65,15 @@ val create :
       @param theories theories to load from the start. Other theories
       can be added using {!add_theory}. *)
 
-val add_theory : t -> theory -> unit
+val add_theory : t -> Theory.t -> unit
 (** Add a theory to the solver. This should be called before
       any call to {!solve} or to {!add_clause} and the likes (otherwise
       the theory will have a partial view of the problem). *)
 
-val add_theory_p : t -> 'a theory_p -> 'a
+val add_theory_p : t -> 'a Theory.p -> 'a
 (** Add the given theory and obtain its state *)
 
-val add_theory_l : t -> theory list -> unit
+val add_theory_l : t -> Theory.t list -> unit
 
 val mk_lit_t : t -> ?sign:bool -> term -> lit
 (** [mk_lit_t _ ~sign t] returns [lit'],
diff --git a/src/smt/solver_internal.ml b/src/smt/solver_internal.ml
index db0995e1..35d28732 100644
--- a/src/smt/solver_internal.ml
+++ b/src/smt/solver_internal.ml
@@ -1,7 +1,6 @@
 open Sigs
 module Proof_rules = Sidekick_core.Proof_sat
 module P_core_rules = Sidekick_core.Proof_core
-module N = Sidekick_cc.E_node
 module Ty = Term
 
 open struct
@@ -46,7 +45,7 @@ type t = {
   cc: CC.t;  (** congruence closure *)
   proof: proof_trace;  (** proof logger *)
   registry: Registry.t;
-  mutable on_progress: unit -> unit;
+  on_progress: (unit, unit) Event.Emitter.t;
   mutable on_partial_check: (t -> theory_actions -> lit Iter.t -> unit) list;
   mutable on_final_check: (t -> theory_actions -> lit Iter.t -> unit) list;
   mutable on_th_combination:
@@ -69,7 +68,10 @@ type t = {
 }
 
 and preprocess_hook = t -> preprocess_actions -> term -> unit
-and model_ask_hook = recurse:(t -> N.t -> term) -> t -> N.t -> term option
+
+and model_ask_hook =
+  recurse:(t -> E_node.t -> term) -> t -> E_node.t -> term option
+
 and model_completion_hook = t -> add:(term -> term -> unit) -> unit
 
 type solver = t
@@ -172,8 +174,7 @@ let preprocess_term_ (self : t) (t0 : term) : unit =
   preproc_rec_ t0
 
 (* simplify literal, then preprocess the result *)
-let simplify_and_preproc_lit_ (self : t) (lit : Lit.t) : Lit.t * step_id option
-    =
+let simplify_and_preproc_lit (self : t) (lit : Lit.t) : Lit.t * step_id option =
   let t = Lit.term lit in
   let sign = Lit.sign lit in
   let u, pr =
@@ -191,7 +192,7 @@ let simplify_and_preproc_lit_ (self : t) (lit : Lit.t) : Lit.t * step_id option
 let push_decision (self : t) (acts : theory_actions) (lit : lit) : unit =
   let (module A) = acts in
   (* make sure the literal is preprocessed *)
-  let lit, _ = simplify_and_preproc_lit_ self lit in
+  let lit, _ = simplify_and_preproc_lit self lit in
   let sign = Lit.sign lit in
   A.add_decision_lit (Lit.abs lit) sign
 
@@ -210,7 +211,7 @@ module Preprocess_clause (A : ARR) = struct
 
     (* simplify a literal, then preprocess it *)
     let[@inline] simp_lit lit =
-      let lit, pr = simplify_and_preproc_lit_ self lit in
+      let lit, pr = simplify_and_preproc_lit self lit in
       Option.iter (fun pr -> steps := pr :: !steps) pr;
       lit
     in
@@ -233,8 +234,8 @@ end
 module PC_list = Preprocess_clause (CCList)
 module PC_arr = Preprocess_clause (CCArray)
 
-let preprocess_clause_ = PC_list.top
-let preprocess_clause_iarray_ = PC_arr.top
+let preprocess_clause = PC_list.top
+let preprocess_clause_array = PC_arr.top
 
 module type PERFORM_ACTS = sig
   type t
@@ -250,7 +251,7 @@ module Perform_delayed (A : PERFORM_ACTS) = struct
       let act = Queue.pop self.delayed_actions in
       match act with
       | DA_add_clause { c; pr = pr_c; keep } ->
-        let c', pr_c' = preprocess_clause_ self c pr_c in
+        let c', pr_c' = preprocess_clause self c pr_c in
         A.add_clause self acts ~keep c' pr_c'
       | DA_add_lit { default_pol; lit } ->
         preprocess_term_ self (Lit.term lit);
@@ -270,11 +271,11 @@ module Perform_delayed_th = Perform_delayed (struct
 end)
 
 let[@inline] add_clause_temp self _acts c (proof : step_id) : unit =
-  let c, proof = preprocess_clause_ self c proof in
+  let c, proof = preprocess_clause self c proof in
   delayed_add_clause self ~keep:false c proof
 
 let[@inline] add_clause_permanent self _acts c (proof : step_id) : unit =
-  let c, proof = preprocess_clause_ self c proof in
+  let c, proof = preprocess_clause self c proof in
   delayed_add_clause self ~keep:true c proof
 
 let[@inline] mk_lit _ ?sign t : lit = Lit.atom ?sign t
@@ -284,7 +285,7 @@ let[@inline] add_lit self _acts ?default_pol lit =
 
 let add_lit_t self _acts ?sign t =
   let lit = Lit.atom ?sign t in
-  let lit, _ = simplify_and_preproc_lit_ self lit in
+  let lit, _ = simplify_and_preproc_lit self lit in
   delayed_add_lit self lit
 
 let on_final_check self f = self.on_final_check <- f :: self.on_final_check
@@ -292,6 +293,7 @@ let on_final_check self f = self.on_final_check <- f :: self.on_final_check
 let on_partial_check self f =
   self.on_partial_check <- f :: self.on_partial_check
 
+let on_progress self = Event.of_emitter self.on_progress
 let on_cc_new_term self f = Event.on (CC.on_new_term (cc self)) ~f
 let on_cc_pre_merge self f = Event.on (CC.on_pre_merge (cc self)) ~f
 let on_cc_post_merge self f = Event.on (CC.on_post_merge (cc self)) ~f
@@ -301,11 +303,13 @@ let on_cc_is_subterm self f = Event.on (CC.on_is_subterm (cc self)) ~f
 let cc_add_term self t = CC.add_term (cc self) t
 let cc_mem_term self t = CC.mem_term (cc self) t
 let cc_find self n = CC.find (cc self) n
+let is_complete self = self.complete
+let last_model self = self.last_model
 
 let cc_are_equal self t1 t2 =
   let n1 = cc_add_term self t1 in
   let n2 = cc_add_term self t2 in
-  N.equal (cc_find self n1) (cc_find self n2)
+  E_node.equal (cc_find self n1) (cc_find self n2)
 
 let cc_resolve_expl self e : lit list * _ =
   let r = CC.explain_expl (cc self) e in
@@ -337,19 +341,6 @@ let rec pop_lvls_ n = function
     r.pop_levels r.st n;
     pop_lvls_ n r.next
 
-let push_level (self : t) : unit =
-  self.level <- 1 + self.level;
-  CC.push_level (cc self);
-  push_lvl_ self.th_states
-
-let pop_levels (self : t) n : unit =
-  self.last_model <- None;
-  self.level <- self.level - n;
-  CC.pop_levels (cc self) n;
-  pop_lvls_ n self.th_states
-
-let n_levels self = self.level
-
 (** {2 Model construction and theory combination} *)
 
 (* make model from the congruence closure *)
@@ -372,7 +363,7 @@ let mk_model_ (self : t) (lits : lit Iter.t) : Model.t =
      CC.get_model_for_each_class cc (fun (_, ts, v) ->
          Iter.iter
            (fun n ->
-             let t = N.term n in
+             let t = E_node.term n in
              M.replace model t v)
            ts);
   *)
@@ -390,20 +381,20 @@ let mk_model_ (self : t) (lits : lit Iter.t) : Model.t =
   List.iter complete_with model_complete;
 
   (* compute a value for [n]. *)
-  let rec val_for_class (n : N.t) : term =
-    Log.debugf 5 (fun k -> k "val-for-term %a" N.pp n);
+  let rec val_for_class (n : E_node.t) : term =
+    Log.debugf 5 (fun k -> k "val-for-term %a" E_node.pp n);
     let repr = CC.find cc n in
-    Log.debugf 5 (fun k -> k "val-for-term.repr %a" N.pp repr);
+    Log.debugf 5 (fun k -> k "val-for-term.repr %a" E_node.pp repr);
 
     (* see if a value is found already (always the case if it's a boolean) *)
-    match M.get model (N.term repr) with
+    match M.get model (E_node.term repr) with
     | Some t_val ->
       Log.debugf 5 (fun k -> k "cached val is %a" Term.pp_debug t_val);
       t_val
     | None ->
       (* try each model hook *)
       let rec try_hooks_ = function
-        | [] -> N.term repr
+        | [] -> E_node.term repr
         | h :: hooks ->
           (match h ~recurse:(fun _ n -> val_for_class n) self repr with
           | None -> try_hooks_ hooks
@@ -415,15 +406,15 @@ let mk_model_ (self : t) (lits : lit Iter.t) : Model.t =
         (* FIXME: the more complete version?
            match
              (* look for a value in the model for any term in the class *)
-             N.iter_class repr
-             |> Iter.find_map (fun n -> M.get model (N.term n))
+             E_node.iter_class repr
+             |> Iter.find_map (fun n -> M.get model (E_node.term n))
            with
            | Some v -> v
            | None -> try_hooks_ model_ask_hooks
         *)
       in
 
-      M.replace model (N.term repr) t_val;
+      M.replace model (E_node.term repr) t_val;
       (* be sure to cache the value *)
       Log.debugf 5 (fun k -> k "val is %a" Term.pp_debug t_val);
       t_val
@@ -433,11 +424,11 @@ let mk_model_ (self : t) (lits : lit Iter.t) : Model.t =
   CC.all_classes cc (fun repr ->
       let t_val = val_for_class repr in
       (* value for this class *)
-      N.iter_class repr (fun u ->
-          let t_u = N.term u in
-          if (not (N.equal u repr)) && not (Term.equal t_u t_val) then
+      E_node.iter_class repr (fun u ->
+          let t_u = E_node.term u in
+          if (not (E_node.equal u repr)) && not (Term.equal t_u t_val) then
             M.replace model t_u t_val));
-  Model.Map model
+  Model.Internal_.of_tbl model
 
 (* do theory combination using the congruence closure. Each theory
    can merge classes, *)
@@ -557,7 +548,7 @@ let check_ ~final (self : t) (acts : sat_acts) =
   in
   let iter = iter_atoms_ acts in
   Log.debugf 5 (fun k -> k "(smt-solver.assume :len %d)" (Iter.length iter));
-  self.on_progress ();
+  Event.emit self.on_progress ();
   assert_lits_ ~final self acts iter;
   Profile.exit pb
 
@@ -569,6 +560,28 @@ let[@inline] partial_check (self : t) (acts : Sidekick_sat.acts) : unit =
 let[@inline] final_check (self : t) (acts : Sidekick_sat.acts) : unit =
   check_ ~final:true self acts
 
+let push_level self : unit =
+  self.level <- 1 + self.level;
+  CC.push_level (cc self);
+  push_lvl_ self.th_states
+
+let pop_levels self n : unit =
+  self.last_model <- None;
+  self.level <- self.level - n;
+  CC.pop_levels (cc self) n;
+  pop_lvls_ n self.th_states
+
+let n_levels self = self.level
+
+let to_sat_plugin (self : t) : (module Sidekick_sat.PLUGIN) =
+  (module struct
+    let has_theory = true
+    let push_level () = push_level self
+    let pop_levels n = pop_levels self n
+    let partial_check acts = partial_check self acts
+    let final_check acts = final_check self acts
+  end)
+
 let declare_pb_is_incomplete self =
   if self.complete then Log.debug 1 "(solver.declare-pb-is-incomplete)";
   self.complete <- false
@@ -587,7 +600,7 @@ let create (module A : ARG) ~stat ~proof (tst : Term.store) () : t =
       stat;
       simp = Simplify.create tst ~proof;
       last_model = None;
-      on_progress = (fun () -> ());
+      on_progress = Event.Emitter.create ();
       preprocess = [];
       model_ask = [];
       model_complete = [];
diff --git a/src/smt/solver_internal.mli b/src/smt/solver_internal.mli
index 508df6fc..72a28d30 100644
--- a/src/smt/solver_internal.mli
+++ b/src/smt/solver_internal.mli
@@ -35,12 +35,14 @@ include Sidekick_sigs.BACKTRACKABLE0 with type t := t
 
 (** {3 Interface to SAT} *)
 
-include Sidekick_sat.PLUGIN_CDCL_T with type t := t
+val to_sat_plugin : t -> (module Sidekick_sat.PLUGIN)
 
 (** {3 Simplifiers} *)
 
 type simplify_hook = Simplify.hook
 
+val simplifier : t -> Simplify.t
+
 val add_simplifier : t -> Simplify.hook -> unit
 (** Add a simplifier hook for preprocessing. *)
 
@@ -90,6 +92,12 @@ type preprocess_hook = t -> preprocess_actions -> term -> unit
 val on_preprocess : t -> preprocess_hook -> unit
 (** Add a hook that will be called when terms are preprocessed *)
 
+val preprocess_clause : t -> lit list -> step_id -> lit list * step_id
+val preprocess_clause_array : t -> lit array -> step_id -> lit array * step_id
+
+val simplify_and_preproc_lit : t -> lit -> lit * step_id option
+(** Simplify literal then preprocess it *)
+
 (** {3 hooks for the theory} *)
 
 val raise_conflict : t -> theory_actions -> lit list -> step_id -> 'a
@@ -245,6 +253,26 @@ val on_model :
   ?ask:model_ask_hook -> ?complete:model_completion_hook -> t -> unit
 (** Add model production/completion hooks. *)
 
+val on_progress : t -> (unit, unit) Event.t
+
+val is_complete : t -> bool
+(** Are we still in a complete logic fragment? *)
+
+val last_model : t -> Model.t option
+
+(** {2 Delayed actions} *)
+
+module type PERFORM_ACTS = sig
+  type t
+
+  val add_clause : solver -> t -> keep:bool -> lit list -> step_id -> unit
+  val add_lit : solver -> t -> ?default_pol:bool -> lit -> unit
+end
+
+module Perform_delayed (A : PERFORM_ACTS) : sig
+  val top : t -> A.t -> unit
+end
+
 val add_theory_state :
   st:'a ->
   push_level:('a -> unit) ->