From cbc9c5ac6f291dacc072115ece4f06090e31c1a1 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 4 Feb 2022 16:08:01 -0500
Subject: [PATCH] refactor(smt): preprocessing is now using a queue of delayed
 actions

- preprocessing doesn't simplify anymore, it assumes terms are already
  simplified. It only adds clauses/adds literals, it does not return
  new terms.
- adding clauses/literals to SAT is done as delayed actions, to avoid
  issues of reentrancy.
  These actions are performed after preprocessing, in a loop that has
  access to the SAT solver.
---
 src/base-solver/sidekick_base_solver.ml       |   3 -
 src/base/Base_types.ml                        |   4 +
 src/base/Form.ml                              |   3 -
 src/core/Sidekick_core.ml                     |  35 +-
 src/lia/Sidekick_arith_lia.ml                 |  13 +-
 src/lra/sidekick_arith_lra.ml                 |  99 ++---
 src/smt-solver/Sidekick_smt_solver.ml         | 420 ++++++++----------
 src/th-bool-static/Sidekick_th_bool_static.ml | 239 +++-------
 src/th-data/Sidekick_th_data.ml               |  13 +-
 9 files changed, 298 insertions(+), 531 deletions(-)

diff --git a/src/base-solver/sidekick_base_solver.ml b/src/base-solver/sidekick_base_solver.ml
index 7dab535d..6579fa8a 100644
--- a/src/base-solver/sidekick_base_solver.ml
+++ b/src/base-solver/sidekick_base_solver.ml
@@ -119,7 +119,6 @@ module Th_lra = Sidekick_arith_lra.Make(struct
   let rec view_as_lra t = match T.view t with
     | T.LIA (Const i) -> LRA.LRA_const (Q.of_bigint i)
     | T.LRA l ->
-      let open Base_types in
       let module LRA = Sidekick_arith_lra in
       begin match l with
         | Const c -> LRA.LRA_const c
@@ -165,7 +164,6 @@ module Th_lia = Sidekick_arith_lia.Make(struct
 
   let view_as_lia t = match T.view t with
     | T.LIA l ->
-      let open Base_types in
       let module LIA = Sidekick_arith_lia in
       begin match l with
         | Const c -> LIA.LIA_const c
@@ -183,7 +181,6 @@ module Th_lia = Sidekick_arith_lia.Make(struct
 
   let lemma_lia = Proof.lemma_lia
   let lemma_relax_to_lra = Proof.lemma_relax_to_lra
-  module Gensym = Gensym
 end)
 
 let th_bool : Solver.theory = Th_bool.theory
diff --git a/src/base/Base_types.ml b/src/base/Base_types.ml
index 5387bdb1..bdcfc266 100644
--- a/src/base/Base_types.ml
+++ b/src/base/Base_types.ml
@@ -992,6 +992,7 @@ module Term : sig
   val iter_dag : t -> t Iter.t
 
   val map_shallow : store -> (t -> t) -> t -> t
+  val iter_shallow : store -> (t -> unit) -> t -> unit
 
   val pp : t Fmt.printer
 
@@ -1210,6 +1211,9 @@ end = struct
 
   let pp = pp_term
 
+  let[@inline] iter_shallow _tst f (t:t) : unit =
+    Term_cell.iter f (view t)
+
   module Iter_dag = struct
     type t = unit Tbl.t
     type order = Pre | Post
diff --git a/src/base/Form.ml b/src/base/Form.ml
index 58623633..9a8dd54f 100644
--- a/src/base/Form.ml
+++ b/src/base/Form.ml
@@ -188,6 +188,3 @@ module Gensym = struct
     let id = ID.make name in
     T.const self.tst @@ Fun.mk_undef_const id ty
 end
-
-(* NOTE: no plugin produces new boolean formulas *)
-let check_congruence_classes = false
diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml
index c89a9c14..033f9694 100644
--- a/src/core/Sidekick_core.ml
+++ b/src/core/Sidekick_core.ml
@@ -119,6 +119,9 @@ module type TERM = sig
     val map_shallow : store -> (t -> t) -> t -> t
     (** Map function on immediate subterms. This should not be recursive. *)
 
+    val iter_shallow : store -> (t -> unit) -> t -> unit
+    (** Iterate function on immediate subterms. This should not be recursive. *)
+
     val iter_dag : t -> (t -> unit) -> unit
     (** [iter_dag t f] calls [f] once on each subterm of [t], [t] included.
         It must {b not} traverse [t] as a tree, but rather as a
@@ -809,7 +812,11 @@ module type SOLVER_INTERNAL = sig
 
         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. *)
+        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 normalize : t -> term -> (term * proof_step) option
     (** Normalize a term using all the hooks. This performs
@@ -845,14 +852,9 @@ module type SOLVER_INTERNAL = sig
   module type PREPROCESS_ACTS = sig
     val proof : proof
 
-    val mk_lit_nopreproc : ?sign:bool -> term -> lit
+    val mk_lit : ?sign:bool -> term -> lit
     (** [mk_lit t] creates a new literal for a boolean term [t]. *)
 
-    val mk_lit : ?sign:bool -> term -> lit * proof_step option
-    (** [mk_lit t] creates a new literal for a boolean term [t].
-        Also returns an optional proof of preprocessing, which if present
-        is the proof of [|- t = lit] with [lit] the result. *)
-
     val add_clause : lit list -> proof_step -> unit
     (** pushes a new clause into the SAT solver. *)
 
@@ -866,14 +868,13 @@ module type SOLVER_INTERNAL = sig
   type preprocess_hook =
     t ->
     preprocess_actions ->
-    term -> (term * proof_step Iter.t) option
-  (** Given a term, try to preprocess it. Return [None] if it didn't change,
-      or [Some (u)] if [t=u].
-      Can also add clauses to define new terms.
+    term -> unit
+  (** Given a term, preprocess it.
 
-      Preprocessing might transform terms to make them more amenable
-      to reasoning, e.g. by removing boolean formulas via Tseitin encoding,
-      adding clauses that encode their meaning in the same move.
+      The idea is to add literals and clauses to help define the meaning of
+      the term, if needed. For example for boolean formulas, clauses
+      for their Tseitin encoding can be added, with the formula acting
+      as its own proxy symbol.
 
       @param preprocess_actions actions available during preprocessing.
   *)
@@ -881,9 +882,6 @@ module type SOLVER_INTERNAL = sig
   val on_preprocess : t -> preprocess_hook -> unit
   (** Add a hook that will be called when terms are preprocessed *)
 
-  val preprocess_acts_of_acts : t -> theory_actions -> preprocess_actions
-  (** Obtain preprocessor actions, from theory actions *)
-
   (** {3 hooks for the theory} *)
 
   val raise_conflict : t -> theory_actions -> lit list -> proof_step -> 'a
@@ -914,9 +912,6 @@ module type SOLVER_INTERNAL = sig
   val mk_lit : t -> theory_actions -> ?sign:bool -> term -> lit
   (** Create a literal. This automatically preprocesses the term. *)
 
-  val preprocess_term : t -> preprocess_actions -> term -> term * proof_step option
-  (** Preprocess a term. *)
-
   val add_lit : t -> theory_actions -> ?default_pol:bool -> lit -> unit
   (** Add the given literal to the SAT solver, so it gets assigned
       a boolean value.
diff --git a/src/lia/Sidekick_arith_lia.ml b/src/lia/Sidekick_arith_lia.ml
index b4f4b7a2..5fdaaa47 100644
--- a/src/lia/Sidekick_arith_lia.ml
+++ b/src/lia/Sidekick_arith_lia.ml
@@ -74,7 +74,7 @@ module Make(A : ARG) : S with module A = A = struct
 
   (* preprocess linear expressions away *)
   let preproc_lia (self:state) si (module PA:SI.PREPROCESS_ACTS)
-      (t:T.t) : (T.t * SI.proof_step Iter.t) option =
+      (t:T.t) : unit =
     Log.debugf 50 (fun k->k "(@[lia.preprocess@ %a@])" T.pp t);
 
     match A.view_as_lia t with
@@ -85,16 +85,17 @@ module Make(A : ARG) : S with module A = A = struct
         let lits = [Lit.atom ~sign:false self.tst t; Lit.atom self.tst u] in
         A.lemma_relax_to_lra Iter.(of_list lits) self.proof
       in
-      Some (u, Iter.return pr)
+
+      (* add [t => u] *)
+      let cl = [PA.mk_lit ~sign:false t; PA.mk_lit u] in
+      PA.add_clause cl pr;
 
     | LIA_other t when A.has_ty_int t ->
       SI.declare_pb_is_incomplete si;
-      None
     | LIA_op _ | LIA_mult _ ->
+      (* TODO: theory combination?*)
       SI.declare_pb_is_incomplete si;
-      None (* TODO: theory combination?*)
-    | LIA_const _ | LIA_other _ ->
-      None
+    | LIA_const _ | LIA_other _ -> ()
 
   let create_and_setup si =
     Log.debug 2 "(th-lia.setup)";
diff --git a/src/lra/sidekick_arith_lra.ml b/src/lra/sidekick_arith_lra.ml
index fd1692cf..3d6d8430 100644
--- a/src/lra/sidekick_arith_lra.ml
+++ b/src/lra/sidekick_arith_lra.ml
@@ -218,27 +218,25 @@ module Make(A : ARG) : S with module A = A = struct
     Fmt.fprintf out "(@[%a@ :l1 %a@ :l2 %a@])" Predicate.pp p LE.pp l1 LE.pp l2
 
   (* turn the term into a linear expression. Apply [f] on leaves. *)
-  let rec as_linexp ~f (t:T.t) : LE.t =
+  let rec as_linexp (t:T.t) : LE.t =
     let open LE.Infix in
     match A.view_as_lra t with
-    | LRA_other _ -> LE.monomial1 (f t)
+    | LRA_other _ -> LE.monomial1 t
     | LRA_pred _ | LRA_simplex_pred _ ->
       Error.errorf "type error: in linexp, LRA predicate %a" T.pp t
     | LRA_op (op, t1, t2) ->
-      let t1 = as_linexp ~f t1 in
-      let t2 = as_linexp ~f t2 in
+      let t1 = as_linexp t1 in
+      let t2 = as_linexp t2 in
       begin match op with
         | Plus -> t1 + t2
         | Minus -> t1 - t2
       end
     | LRA_mult (n, x) ->
-      let t = as_linexp ~f x in
+      let t = as_linexp x in
       LE.( n * t )
     | LRA_simplex_var v -> LE.monomial1 v
     | LRA_const q -> LE.of_const q
 
-  let as_linexp_id = as_linexp ~f:CCFun.id
-
   (* return a variable that is equal to [le_comb] in the simplex. *)
   let var_encoding_comb ~pre self (le_comb:LE_.Comb.t) : T.t =
     match LE_.Comb.as_singleton le_comb with
@@ -277,19 +275,11 @@ module Make(A : ARG) : S with module A = A = struct
     PA.add_clause lits pr
 
   (* preprocess linear expressions away *)
-  let preproc_lra (self:state) si (module PA:SI.PREPROCESS_ACTS)
-      (t:T.t) : (T.t * SI.proof_step Iter.t) option =
+  let preproc_lra (self:state) si
+      (module PA:SI.PREPROCESS_ACTS) (t:T.t) : unit =
     Log.debugf 50 (fun k->k "(@[lra.preprocess@ %a@])" T.pp t);
     let tst = SI.tst si in
 
-    (* preprocess subterm *)
-    let preproc_t ~steps t =
-      let u, pr = SI.preprocess_term si (module PA) t in
-      T.Tbl.replace self.in_model t ();
-      CCOpt.iter (fun s -> steps := s :: !steps) pr;
-      u
-    in
-
     (* tell the CC this term exists *)
     let declare_term_to_cc t =
       Log.debugf 50 (fun k->k "(@[simplex2.declare-term-to-cc@ %a@])" T.pp t);
@@ -307,20 +297,18 @@ module Make(A : ARG) : S with module A = A = struct
         T.Tbl.add self.encoded_eqs t ();
 
         (* encode [t <=> (u1 /\ u2)] *)
-        let lit_t = PA.mk_lit_nopreproc t in
-        let lit_u1 = PA.mk_lit_nopreproc u1 in
-        let lit_u2 = PA.mk_lit_nopreproc u2 in
+        let lit_t = PA.mk_lit t in
+        let lit_u1 = PA.mk_lit u1 in
+        let lit_u2 = PA.mk_lit u2 in
         add_clause_lra_ (module PA) [SI.Lit.neg lit_t; lit_u1];
         add_clause_lra_ (module PA) [SI.Lit.neg lit_t; lit_u2];
         add_clause_lra_ (module PA)
           [SI.Lit.neg lit_u1; SI.Lit.neg lit_u2; lit_t];
       );
-      None
 
     | LRA_pred (pred, t1, t2) ->
-      let steps = ref [] in
-      let l1 = as_linexp ~f:(preproc_t ~steps) t1 in
-      let l2 = as_linexp ~f:(preproc_t ~steps) t2 in
+      let l1 = as_linexp t1 in
+      let l2 = as_linexp t2 in
       let le = LE.(l1 - l2) in
       let le_comb, le_const = LE.comb le, LE.const le in
       let le_const = A.Q.neg le_const in
@@ -329,10 +317,7 @@ module Make(A : ARG) : S with module A = A = struct
       begin match LE_.Comb.as_singleton le_comb, pred with
         | None, _ ->
           (* non trivial linexp, give it a fresh name in the simplex *)
-          let proxy = var_encoding_comb self ~pre:"_le" le_comb in
-          let pr_def = SI.P.define_term proxy t PA.proof in
-          steps := pr_def :: !steps;
-          declare_term_to_cc proxy;
+          declare_term_to_cc t;
 
           let op =
             match pred with
@@ -343,15 +328,14 @@ module Make(A : ARG) : S with module A = A = struct
             | Gt -> S_op.Gt
           in
 
-          let new_t = A.mk_lra tst (LRA_simplex_pred (proxy, op, le_const)) in
+          let new_t = A.mk_lra tst (LRA_simplex_pred (t, op, le_const)) in
           begin
-            let lit = PA.mk_lit_nopreproc new_t in
-            let constr = SimpSolver.Constraint.mk proxy op le_const in
+            let lit = PA.mk_lit new_t in
+            let constr = SimpSolver.Constraint.mk t op le_const in
             SimpSolver.declare_bound self.simplex constr (Tag.Lit lit);
           end;
 
           Log.debugf 10 (fun k->k "(@[lra.preprocess:@ %a@ :into %a@])" T.pp t T.pp new_t);
-          Some (new_t, Iter.of_list !steps)
 
         | Some (coeff, v), pred ->
           (* [c . v <= const] becomes a direct simplex constraint [v <= const/c] *)
@@ -370,45 +354,33 @@ module Make(A : ARG) : S with module A = A = struct
 
           let new_t = A.mk_lra tst (LRA_simplex_pred (v, op, q)) in
           begin
-            let lit = PA.mk_lit_nopreproc new_t in
+            let lit = PA.mk_lit new_t in
             let constr = SimpSolver.Constraint.mk v op q in
             SimpSolver.declare_bound self.simplex constr (Tag.Lit lit);
           end;
 
           Log.debugf 10 (fun k->k "lra.preprocess@ :%a@ :into %a" T.pp t T.pp new_t);
-          Some (new_t, Iter.of_list !steps)
       end
 
     | LRA_op _ | LRA_mult _ ->
       let steps = ref [] in
-      let le = as_linexp ~f:(preproc_t ~steps) t in
+      let le = as_linexp t in
       let le_comb, le_const = LE.comb le, LE.const le in
 
       if A.Q.(le_const = zero) then (
-        (* if there is no constant, define [proxy] as [proxy := le_comb] and
-           return [proxy] *)
-        let proxy = var_encoding_comb self ~pre:"_le" le_comb in
-        begin
-          let pr_def = SI.P.define_term proxy t PA.proof in
-          steps := pr_def :: !steps;
-        end;
-        declare_term_to_cc proxy;
-
-        Some (proxy, Iter.of_list !steps)
+        (* if there is no constant, define [t] as [t := le_comb] *)
+        declare_term_to_cc t;
       ) else (
-        (* a bit more complicated: we cannot just define [proxy := le_comb]
+        (* a bit more complicated: we cannot just define [t := le_comb]
            because of the coefficient.
-           Instead we assert [proxy - le_comb = le_const] using a secondary
-           variable [proxy2 := le_comb - proxy]
-           and asserting [proxy2 = -le_const] *)
-        let proxy = fresh_term self ~pre:"_le" (T.ty t) in
-        begin
-          let pr_def = SI.P.define_term proxy t PA.proof in
-          steps := pr_def :: !steps;
-        end;
+           Instead we assert [t - le_comb = le_const] using a secondary
+           variable [proxy2 := t - le_comb]
+           and asserting [proxy2 = le_const] *)
         let proxy2 = fresh_term self ~pre:"_le_diff" (T.ty t) in
+        (* TODO
         let pr_def2 =
-          SI.P.define_term proxy (A.mk_lra tst (LRA_op (Minus, t, proxy))) PA.proof
+          SI.P.define_term proxy2
+            (A.mk_lra tst (LRA_op (Minus, t, A.mk_lra tst (LRA_const le_const)))) PA.proof
         in
 
         SimpSolver.add_var self.simplex proxy;
@@ -425,21 +397,22 @@ module Make(A : ARG) : S with module A = A = struct
         declare_term_to_cc proxy2;
 
         add_clause_lra_ ~using:Iter.(return pr_def2) (module PA) [
-          PA.mk_lit_nopreproc (A.mk_lra tst (LRA_simplex_pred (proxy2, Leq, A.Q.neg le_const)))
+          PA.mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Leq, A.Q.neg le_const)))
         ];
         add_clause_lra_ ~using:Iter.(return pr_def2) (module PA) [
-          PA.mk_lit_nopreproc (A.mk_lra tst (LRA_simplex_pred (proxy2, Geq, A.Q.neg le_const)))
+          PA.mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Geq, A.Q.neg le_const)))
         ];
 
         Some (proxy, Iter.of_list !steps)
+           *)
+        ()
       )
 
-    | LRA_other t when A.has_ty_real t -> None
+    | LRA_other t when A.has_ty_real t -> ()
     | LRA_const _ | LRA_simplex_pred _ | LRA_simplex_var _ | LRA_other _ ->
-      None
+      ()
 
   let simplify (self:state) (_recurse:_) (t:T.t) : (T.t * SI.proof_step Iter.t) option =
-
     let proof_eq t u =
       A.lemma_lra
         (Iter.return (SI.Lit.atom self.tst (A.mk_eq self.tst t u))) self.proof
@@ -451,7 +424,7 @@ module Make(A : ARG) : S with module A = A = struct
 
     match A.view_as_lra t with
     | LRA_op _ | LRA_mult _ ->
-      let le = as_linexp_id t in
+      let le = as_linexp t in
       if LE.is_const le then (
         let c = LE.const le in
         let u = A.mk_lra self.tst (LRA_const c) in
@@ -459,7 +432,7 @@ module Make(A : ARG) : S with module A = A = struct
         Some (u, Iter.return pr)
       ) else None
     | LRA_pred (pred, l1, l2) ->
-      let le = LE.(as_linexp_id l1 - as_linexp_id l2) in
+      let le = LE.(as_linexp l1 - as_linexp l2) in
       if LE.is_const le then (
         let c = LE.const le in
         let is_true = match pred with
@@ -527,7 +500,7 @@ module Make(A : ARG) : S with module A = A = struct
     let t2 = N.term n2 in
     let t1, t2 = if T.compare t1 t2 > 0 then t2, t1 else t1, t2 in
 
-    let le = LE.(as_linexp_id t1 - as_linexp_id t2) in
+    let le = LE.(as_linexp t1 - as_linexp t2) in
     let le_comb, le_const = LE.comb le, LE.const le in
     let le_const = A.Q.neg le_const in
 
diff --git a/src/smt-solver/Sidekick_smt_solver.ml b/src/smt-solver/Sidekick_smt_solver.ml
index 36954b9e..2db21dc1 100644
--- a/src/smt-solver/Sidekick_smt_solver.ml
+++ b/src/smt-solver/Sidekick_smt_solver.ml
@@ -129,6 +129,19 @@ module Make(A : ARG)
   module CC = Sidekick_cc.Make(CC_actions)
   module N = CC.N
 
+  (* delayed actions. We avoid doing them on the spot because, when
+     triggered by a theory, they might go back to the theory "too early". *)
+  type delayed_action =
+    | DA_add_clause of {
+        c: lit list;
+        pr: proof_step;
+        keep: bool;
+      }
+    | DA_add_lit of {
+        default_pol: bool option;
+        lit: lit;
+      }
+
   (** Internal solver, given to theories and to Msat *)
   module Solver_internal = struct
     module T = T
@@ -232,8 +245,7 @@ module Make(A : ARG)
 
     module type PREPROCESS_ACTS = sig
       val proof : proof
-      val mk_lit_nopreproc : ?sign:bool -> term -> lit
-      val mk_lit : ?sign:bool -> term -> lit * proof_step option
+      val mk_lit : ?sign:bool -> term -> lit
       val add_clause : lit list -> proof_step -> unit
       val add_lit : ?default_pol:bool -> lit -> unit
     end
@@ -246,30 +258,35 @@ module Make(A : ARG)
       ty_st: Ty.store;
       cc: CC.t lazy_t; (** congruence closure *)
       proof: proof; (** proof logger *)
+      registry: Registry.t;
+
+      mutable on_progress: unit -> unit;
+      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 preprocess: preprocess_hook list;
+      mutable model_ask: model_ask_hook list;
+      mutable model_complete: model_completion_hook list;
+
+      simp: Simplify.t;
+      preprocessed: unit Term.Tbl.t;
+      delayed_actions: delayed_action Queue.t;
+
+      mutable t_defs : (term*term) list; (* term definitions *)
+      mutable th_states : th_states; (** Set of theories *)
+      mutable level: int;
+      mutable complete: bool;
+
       stat: Stat.t;
       count_axiom: int Stat.counter;
       count_preprocess_clause: int Stat.counter;
       count_conflict: int Stat.counter;
       count_propagate: int Stat.counter;
-      registry: Registry.t;
-      mutable on_progress: unit -> unit;
-      simp: Simplify.t;
-      mutable preprocess: preprocess_hook list;
-      mutable model_ask: model_ask_hook list;
-      mutable model_complete: model_completion_hook list;
-      preprocess_cache: (Term.t * proof_step Bag.t) Term.Tbl.t;
-      mutable t_defs : (term*term) list; (* term definitions *)
-      mutable th_states : th_states; (** Set of theories *)
-      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 level: int;
-      mutable complete: bool;
     }
 
     and preprocess_hook =
       t ->
       preprocess_actions ->
-      term -> (term * proof_step Iter.t) option
+      term -> unit
 
     and model_ask_hook =
       recurse:(t -> CC.N.t -> term) ->
@@ -329,222 +346,160 @@ module Make(A : ARG)
       Stat.incr self.count_axiom;
       A.add_clause_in_pool ~pool lits proof
 
-    let add_sat_lit _self ?default_pol (acts:theory_actions) (lit:Lit.t) : unit =
+    let add_sat_lit_ _self ?default_pol (acts:theory_actions) (lit:Lit.t) : unit =
       let (module A) = acts in
       A.add_lit ?default_pol lit
 
-    (* actual preprocessing logic, acting on terms.
-       this calls all the preprocessing hooks on subterms, ensuring
-       a fixpoint. *)
-    let preprocess_term_ (self:t) (module A0:PREPROCESS_ACTS) (t:term) : term * proof_step option =
-      let mk_lit_nopreproc ?sign t = Lit.atom ?sign self.tst t in (* no further simplification *)
+    let delayed_add_lit (self:t) ?default_pol (lit:Lit.t) : unit =
+      Queue.push (DA_add_lit {default_pol; lit}) self.delayed_actions
 
-      (* compute and cache normal form [u] of [t].
+    let delayed_add_clause (self:t) ~keep (c:Lit.t list) (pr:proof_step) : unit =
+      Queue.push (DA_add_clause {c;pr;keep}) self.delayed_actions
 
-         Also cache a list of proofs [ps] such that [ps |- t=u] by CC.
-         It is important that we cache the proofs here, because
-         next time we preprocess [t], we will have to re-emit the same
-         proofs, even though we will not do any actual preprocessing work.
-      *)
-      let rec preproc_rec ~steps t : term =
-        match Term.Tbl.find self.preprocess_cache t with
-        | u, pr_u ->
-          steps := Bag.append pr_u !steps;
-          u
+    (* preprocess a term. We assume the term has been simplified already. *)
+    let preprocess_term_ (self:t) (t0:term) : unit =
+      let module A = struct
+        let proof = self.proof
+        let mk_lit ?sign t : Lit.t = Lit.atom self.tst ?sign t
+        let add_lit ?default_pol lit : unit = delayed_add_lit self ?default_pol lit
+        let add_clause c pr : unit = delayed_add_clause self ~keep:true c pr
+      end in
+      let acts = (module A:PREPROCESS_ACTS) in
 
-        | exception Not_found ->
-          (* try rewrite at root *)
-          let steps = ref Bag.empty in
-          let t1 = preproc_with_hooks ~steps t self.preprocess in
-
-          (* map subterms *)
-          let t2 = Term.map_shallow self.tst (preproc_rec ~steps) t1 in
-
-          let u =
-            if not (Term.equal t t2) then (
-              preproc_rec ~steps t2 (* fixpoint *)
-            ) else (
-              t2
-            )
-          in
+      (* how to preprocess a term and its subterms *)
+      let rec preproc_rec_ t =
+        if not (Term.Tbl.mem self.preprocessed t) then (
+          Term.Tbl.add self.preprocessed t ();
+          Log.debugf 50 (fun k->k "(@[smt.preprocess@ %a@])" Term.pp t);
 
           (* signal boolean subterms, so as to decide them
              in the SAT solver *)
-          if Ty.is_bool (Term.ty u) then (
+          if Ty.is_bool (Term.ty t) then (
             Log.debugf 5
-              (fun k->k "(@[solver.map-bool-subterm-to-lit@ :subterm %a@])" Term.pp u);
+              (fun k->k "(@[solver.map-bool-subterm-to-lit@ :subterm %a@])" Term.pp t);
 
-            (* make a literal (already preprocessed) *)
-            let lit = mk_lit_nopreproc u in
+            (* make a literal *)
+            let lit = Lit.atom self.tst t in
             (* ensure that SAT solver has a boolean atom for [u] *)
-            A0.add_lit lit;
+            delayed_add_lit self lit;
 
             (* also map [sub] to this atom in the congruence closure, for propagation *)
             let cc = cc self in
-            CC.set_as_lit cc (CC.add_term cc u) lit;
+            CC.set_as_lit cc (CC.add_term cc t) lit;
           );
 
-          if t != u then (
-            Log.debugf 5
-              (fun k->k "(@[smt-solver.preprocess.term@ :from %a@ :to %a@])"
-                  Term.pp t Term.pp u);
-          );
+          List.iter
+            (fun f -> f self acts t) self.preprocess;
 
-          let pr_t_u = !steps in
-          Term.Tbl.add self.preprocess_cache t (u, pr_t_u);
-          u
-
-      (* try each function in [hooks] successively *)
-      and preproc_with_hooks ~steps t hooks : term =
-        let[@inline] add_step s = steps := Bag.cons s !steps in
-        match hooks with
-        | [] -> t
-        | h :: hooks_tl ->
-          (* call hook, using [pacts] which will ensure all new
-             literals and clauses are also preprocessed *)
-          match h self (Lazy.force pacts) t with
-          | None -> preproc_with_hooks ~steps t hooks_tl
-          | Some (u, pr_u) ->
-            Iter.iter add_step pr_u;
-            preproc_rec ~steps u
-
-      (* create literal and preprocess it with [pacts], which uses [A0]
-         for the base operations, and preprocesses new literals and clauses
-         recursively. *)
-      and mk_lit ?sign t : _ * proof_step option =
-        let steps = ref Bag.empty in
-        let u = preproc_rec ~steps t in
-        let pr_t_u =
-          if not (Term.equal t u) then (
-            Log.debugf 10
-              (fun k->k "(@[smt-solver.preprocess.t@ :t %a@ :into %a@])"
-                  Term.pp t Term.pp u);
-
-            let p =
-              A.P.lemma_preprocess t u ~using:(Bag.to_iter !steps) self.proof
-            in
-            Some p
-          ) else None
-        in
-        Lit.atom self.tst ?sign u, pr_t_u
-
-      and preprocess_lit ~steps (lit:lit) : lit =
-        let t = Lit.term lit in
-        let sign = Lit.sign lit in
-        let lit, pr = mk_lit ~sign t in
-        CCOpt.iter (fun s -> steps := s :: !steps) pr;
-        lit
-
-      (* wrap [A0] so that all operations go throught preprocessing *)
-      and pacts = lazy (
-        (module struct
-          let proof = A0.proof
-
-          let add_lit ?default_pol lit =
-            (* just drop the proof *)
-            (* TODO: add a clause instead [lit => preprocess(lit)]? *)
-            let lit = preprocess_lit ~steps:(ref []) lit in
-            A0.add_lit ?default_pol lit
-
-          let add_clause c pr_c =
-            Stat.incr self.count_preprocess_clause;
-            let steps = ref [] in
-            let c' = CCList.map (preprocess_lit ~steps) c in
-            let pr_c' =
-              A.P.lemma_rw_clause pr_c
-                ~res:(Iter.of_list c')
-                ~using:(Iter.of_list !steps) proof
-            in
-            A0.add_clause c' pr_c'
-
-          let mk_lit_nopreproc = mk_lit_nopreproc
-
-          let mk_lit = mk_lit
-        end : PREPROCESS_ACTS)
-      ) in
-
-      let steps = ref Bag.empty in
-      let[@inline] add_step s = steps := Bag.cons s !steps in
-
-      (* simplify the term *)
-      let t1, pr_1 = simp_t self t in
-      CCOpt.iter add_step pr_1;
-
-      (* preprocess *)
-      let u = preproc_rec ~steps t1 in
-
-      (* emit [|- t=u] *)
-      let pr_u =
-        if not (Term.equal t u) then (
-          let p = P.lemma_preprocess t u ~using:(Bag.to_iter !steps) self.proof in
-          Some p
-        ) else None
+          (* process sub-terms *)
+          Term.iter_shallow self.tst preproc_rec_ t;
+        )
       in
+      preproc_rec_ t0
 
-      u, pr_u
-
-    (* return preprocessed lit *)
-    let preprocess_lit_ ~steps (self:t) (pacts:preprocess_actions) (lit:lit) : lit =
+    let simplify_lit_ (self:t) (lit:Lit.t) : Lit.t * proof_step option =
       let t = Lit.term lit in
       let sign = Lit.sign lit in
-      let u, pr_u = preprocess_term_ self pacts t in
-      CCOpt.iter (fun s -> steps := s :: !steps) pr_u;
-      Lit.atom self.tst ~sign u
+      let u, pr = match simplify_t self t with
+        | None -> t, None
+        | Some (u, pr_t_u) ->
+          Log.debugf 30
+            (fun k->k "(@[smt-solver.simplify@ :t %a@ :into %a@])"
+                Term.pp t Term.pp u);
+          u, Some pr_t_u
+      in
+      preprocess_term_ self u;
+      Lit.atom self.tst ~sign u, pr
 
-    (* add a clause using [acts] *)
-    let add_clause_ self acts lits (proof:proof_step) : unit =
-      add_sat_clause_ self acts ~keep:true lits proof
+    module type ARR = sig
+      type 'a t
+      val map : ('a -> 'b) -> 'a t -> 'b t
+      val to_iter : 'a t -> 'a Iter.t
+    end
 
-    let[@inline] add_lit _self (acts:theory_actions) ?default_pol lit : unit =
-      let (module A) = acts in
-      A.add_lit ?default_pol lit
+    module Preprocess_clause(A: ARR) = struct
+      (* preprocess a clause's literals, possibly emitting a proof
+         for the preprocessing. *)
+      let top (self:t)
+          (c:lit A.t) (pr_c:proof_step) : lit A.t * proof_step =
 
-    let preprocess_acts_of_acts (self:t) (acts:theory_actions) : preprocess_actions =
-      (module struct
-        let proof = self.proof
-        let mk_lit_nopreproc ?sign t = Lit.atom self.tst ?sign t
-        let mk_lit ?sign t = Lit.atom self.tst ?sign t, None
-        let add_clause = add_clause_ self acts
-        let add_lit = add_lit self acts
+        let steps = ref [] in
+
+        (* simplify a literal, then preprocess it *)
+        let[@inline] simp_lit lit =
+          let lit, pr = simplify_lit_ self lit in
+          CCOpt.iter (fun pr -> steps := pr :: !steps) pr;
+          lit
+        in
+        let c' = A.map simp_lit c in
+
+        let pr_c' =
+          if !steps=[] then pr_c
+          else (
+            Stat.incr self.count_preprocess_clause;
+            P.lemma_rw_clause pr_c
+              ~res:(A.to_iter c')
+              ~using:(Iter.of_list !steps) self.proof
+          )
+        in
+        c', pr_c'
+    end[@@inline]
+
+    module PC_list = Preprocess_clause(CCList)
+    module PC_arr = Preprocess_clause(IArray)
+
+    let preprocess_clause_ = PC_list.top
+    let preprocess_clause_iarray_ = PC_arr.top
+
+    module type PERFORM_ACTS = sig
+      type t
+      val add_clause : solver -> t -> keep:bool -> lit list -> proof_step -> unit
+      val add_lit : solver -> t -> ?default_pol:bool -> lit -> unit
+    end
+
+    module Perform_delayed(A : PERFORM_ACTS) = struct
+      (* perform actions that were delayed *)
+      let top (self:t) (acts:A.t) : unit =
+        while not (Queue.is_empty self.delayed_actions) do
+          let act = Queue.pop self.delayed_actions in
+          begin match act with
+            | DA_add_clause {c; pr=pr_c; keep} ->
+              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);
+              A.add_lit self acts ?default_pol lit
+          end
+        done
+    end[@@inline]
+
+    module Perform_delayed_th = Perform_delayed(struct
+        type t = theory_actions
+        let add_clause self acts ~keep c pr : unit =
+          add_sat_clause_ self acts ~keep c pr
+        let add_lit self acts ?default_pol lit : unit =
+          add_sat_lit_ self acts ?default_pol lit
       end)
 
-    let preprocess_clause_ (self:t) (acts:theory_actions)
-        (c:lit list) (proof:proof_step) : lit list * proof_step =
-      let steps = ref [] in
-      let pacts = preprocess_acts_of_acts self acts in
-      let c = CCList.map (preprocess_lit_ ~steps self pacts) c in
-      let pr =
-        P.lemma_rw_clause proof
-          ~res:(Iter.of_list c) ~using:(Iter.of_list !steps) self.proof
-      in
-      c, pr
+    let[@inline] add_clause_temp self _acts c (proof:proof_step) : unit =
+      let c, proof = preprocess_clause_ self c proof in
+      delayed_add_clause self ~keep:false c proof
 
-    (* make literal and preprocess it *)
-    let[@inline] mk_plit (self:t) (pacts:preprocess_actions) ?sign (t:term) : lit =
+    let[@inline] add_clause_permanent self _acts c (proof:proof_step) : unit =
+      let c, proof = preprocess_clause_ self c proof in
+      delayed_add_clause self ~keep:true c proof
+
+    let[@inline] mk_lit (self:t) (_acts:theory_actions) ?sign t : lit =
+      Lit.atom self.tst ?sign t
+
+    let[@inline] add_lit self _acts ?default_pol lit =
+      delayed_add_lit self ?default_pol lit
+
+    let add_lit_t self _acts ?sign t =
       let lit = Lit.atom self.tst ?sign t in
-      let steps = ref [] in
-      preprocess_lit_ ~steps self pacts lit
-
-    let[@inline] preprocess_term self
-        (pacts:preprocess_actions) (t:term) : term * _ option =
-      preprocess_term_ self pacts t
-
-    let[@inline] add_clause_temp self acts c (proof:proof_step) : unit =
-      let c, proof = preprocess_clause_ self acts c proof in
-      add_sat_clause_ self acts ~keep:false c proof
-
-    let[@inline] add_clause_permanent self acts c (proof:proof_step) : unit =
-      let c, proof = preprocess_clause_ self acts c proof in
-      add_sat_clause_ self acts ~keep:true c proof
-
-    let[@inline] mk_lit (self:t) (acts:theory_actions) ?sign t : lit =
-      let pacts = preprocess_acts_of_acts self acts in
-      mk_plit self pacts ?sign t
-
-    let add_lit_t self acts ?sign t =
-      let pacts = preprocess_acts_of_acts self acts in
-      let lit = mk_plit self pacts ?sign t in
-      add_lit self acts lit
+      let lit, _ = simplify_lit_ self lit in
+      delayed_add_lit self lit
 
     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
@@ -607,7 +562,9 @@ module Make(A : ARG)
           while true do
             (* TODO: theory combination *)
             List.iter (fun f -> f self acts lits) self.on_final_check;
+            Perform_delayed_th.top self acts;
             CC.check cc acts;
+            Perform_delayed_th.top self acts;
             if not @@ CC.new_merges cc then (
               raise_notrace E_loop_exit
             );
@@ -616,6 +573,7 @@ module Make(A : ARG)
           ()
       ) else (
         List.iter (fun f -> f self acts lits) self.on_partial_check;
+        Perform_delayed_th.top self acts;
       );
       ()
 
@@ -664,7 +622,8 @@ module Make(A : ARG)
         model_ask=[];
         model_complete=[];
         registry=Registry.create();
-        preprocess_cache=Term.Tbl.create 32;
+        preprocessed=Term.Tbl.create 32;
+        delayed_actions=Queue.create();
         count_axiom = Stat.mk_int stat "solver.th-axioms";
         count_preprocess_clause = Stat.mk_int stat "solver.preprocess-clause";
         count_propagate = Stat.mk_int stat "solver.th-propagations";
@@ -816,38 +775,13 @@ module Make(A : ARG)
 
   let reset_last_res_ self = self.last_res <- None
 
-  let preprocess_acts_of_solver_
-      (self:t) : (module Solver_internal.PREPROCESS_ACTS) =
-    (module struct
-      let proof = self.proof
-      let mk_lit_nopreproc ?sign t = Lit.atom ?sign self.si.tst t
-      let mk_lit ?sign t = Lit.atom ?sign self.si.tst t, None
-      let add_lit ?default_pol lit =
-        Sat_solver.add_lit self.solver ?default_pol lit
-      let add_clause c pr =
-        Sat_solver.add_clause self.solver c pr
-    end)
-
-  (* preprocess literal *)
-  let preprocess_lit_ ~steps (self:t) (lit:lit) : lit =
-    let pacts = preprocess_acts_of_solver_ self in
-    Solver_internal.preprocess_lit_ ~steps self.si pacts lit
-
   (* preprocess clause, return new proof *)
   let preprocess_clause_ (self:t)
       (c:lit IArray.t) (pr:proof_step) : lit IArray.t * proof_step =
-    let steps = ref [] in
-    let c = IArray.map (preprocess_lit_ self ~steps) c in
-    let pr =
-      P.lemma_rw_clause pr
-        ~res:(IArray.to_iter c) ~using:(Iter.of_list !steps) self.proof
-    in
-    c, pr
+    Solver_internal.preprocess_clause_iarray_ self.si c pr
 
-  (* make a literal from a term, ensuring it is properly preprocessed *)
-  let mk_lit_t (self:t) ?sign (t:term) : lit =
-    let pacts = preprocess_acts_of_solver_ self in
-    Solver_internal.mk_plit self.si pacts ?sign t
+  let[@inline] mk_lit_t (self:t) ?sign (t:term) : lit =
+    Lit.atom self.si.tst ?sign t
 
   (** {2 Main} *)
 
@@ -867,22 +801,26 @@ module Make(A : ARG)
 
   let add_clause_nopreproc_l_ self c p = add_clause_nopreproc_ self (IArray.of_list c) p
 
+  module Perform_delayed_ = Solver_internal.Perform_delayed(struct
+      type nonrec t = t
+      let add_clause _si solver ~keep:_ c pr : unit =
+        add_clause_nopreproc_l_ solver c pr
+      let add_lit _si solver ?default_pol lit : unit =
+        Sat_solver.add_lit solver.solver ?default_pol lit
+    end)
+
   let add_clause (self:t) (c:lit IArray.t) (proof:proof_step) : unit =
     let c, proof = preprocess_clause_ self c proof in
-    add_clause_nopreproc_ self c proof
+    add_clause_nopreproc_ self c proof;
+    Perform_delayed_.top self.si self; (* finish preproc *)
+    ()
 
   let add_clause_l self c p = add_clause self (IArray.of_list c) p
 
   let assert_terms self c =
-    let steps = ref [] in
     let c = CCList.map (fun t -> Lit.atom (tst self) t) c in
-    let c = CCList.map (preprocess_lit_ ~steps self) c in
-    (* TODO: if c != c0 then P.emit_redundant_clause c
-       because we jsut preprocessed it away? *)
-    let pr = P.emit_input_clause (Iter.of_list c) self.proof in
-    let pr = P.lemma_rw_clause pr
-        ~res:(Iter.of_list c) ~using:(Iter.of_list !steps) self.proof in
-    add_clause_l self c pr
+    let pr_c = P.emit_input_clause (Iter.of_list c) self.proof in
+    add_clause_l self c pr_c
 
   let assert_term self t = assert_terms self [t]
 
diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml
index 71008412..9c865d30 100644
--- a/src/th-bool-static/Sidekick_th_bool_static.ml
+++ b/src/th-bool-static/Sidekick_th_bool_static.ml
@@ -53,12 +53,6 @@ module type ARG = sig
   val mk_bool : S.T.Term.store -> (term, term IArray.t) bool_view -> term
   (** Make a term from the given boolean view. *)
 
-  val check_congruence_classes : bool
-  (** Configuration: add final-check handler to verify if new boolean formulas
-      are present in the congruence closure.
-      Only enable if some theories are susceptible to
-      create boolean formulas during the proof search. *)
-
   include PROOF
     with type proof := S.P.t
      and type proof_step := S.P.proof_step
@@ -115,13 +109,11 @@ module Make(A : ARG) : S with module A = A = struct
   type state = {
     tst: T.store;
     ty_st: Ty.store;
-    preprocessed: (T.t * SI.proof_step Iter.t) option T.Tbl.t;
     gensym: A.Gensym.t;
   }
 
   let create tst ty_st : state =
     { tst; ty_st;
-      preprocessed=T.Tbl.create 64;
       gensym=A.Gensym.create tst;
     }
 
@@ -216,223 +208,99 @@ module Make(A : ARG) : S with module A = A = struct
     let proxy = fresh_term ~for_t ~pre self (Ty.bool self.ty_st) in
     proxy, mk_lit proxy
 
-  let pr_p1 p s1 s2 = SI.P.proof_p1 s1 s2 p
-  let pr_p1_opt p s1 s2 : SI.proof_step =
-    CCOpt.map_or ~default:s2 (fun s1 -> SI.P.proof_p1 s1 s2 p) s1
-
-  let preprocess_uncached_ self si (module PA:SI.PREPROCESS_ACTS)
-      (t:T.t) : (T.t * SI.proof_step Iter.t) option =
-    let steps = ref [] in
-    let add_step_ s = steps := s :: !steps in
-
-    let ret u =
-      if t==u then None
-      else Some (u, Iter.of_list !steps)
-    in
-
-    (* FIXME: make sure add-clause is delayed… perhaps return a vector of actions
-       or something like that *)
-    let add_clause_rw lits ~using ~c0 : unit =
-      PA.add_clause lits @@
-      SI.P.lemma_rw_clause c0 ~res:(Iter.of_list lits) ~using PA.proof
-    in
-
-    match A.view_as_bool t with
-    | B_ite (a,b,c) ->
-      let a', pr_a = SI.simp_t si a in
-      CCOpt.iter add_step_ pr_a;
-      begin match A.view_as_bool a' with
-        | B_bool true ->
-          (* [a |- ite a b c=b],  [a=true] implies [ite a b c=b] *)
-          add_step_
-            (pr_p1_opt PA.proof pr_a @@ A.lemma_ite_true ~ite:t PA.proof);
-          ret b
-
-        | B_bool false ->
-          (* [¬a |- ite a b c=c],  [a=false] implies [ite a b c=c] *)
-          add_step_
-            (pr_p1_opt PA.proof pr_a @@ A.lemma_ite_false ~ite:t PA.proof);
-          ret c
-
-        | _ ->
-          let b', pr_b = SI.simp_t si b in
-          CCOpt.iter add_step_ pr_b;
-          let c', pr_c = SI.simp_t si c in
-          CCOpt.iter add_step_ pr_c;
-          let t_ite = A.mk_bool self.tst (B_ite (a', b', c')) in
-          let lit_a = PA.mk_lit_nopreproc a' in
-          add_clause_rw [Lit.neg lit_a; PA.mk_lit_nopreproc (eq self.tst t_ite b')]
-            ~using:Iter.(of_opt pr_a)
-            ~c0:(A.lemma_ite_true ~ite:t PA.proof);
-          add_clause_rw [lit_a; PA.mk_lit_nopreproc (eq self.tst t_ite c')]
-            ~using:Iter.(of_opt pr_a)
-            ~c0:(A.lemma_ite_false ~ite:t PA.proof);
-          ret t_ite
-      end
-    | _ -> None
-
-  let preprocess self si pa t =
-    match T.Tbl.find_opt self.preprocessed t with
-    | None ->
-      let res = preprocess_uncached_ self si pa t in
-      T.Tbl.add self.preprocessed t res;
-      res
-    | Some r -> r
-
   (* TODO: polarity? *)
-  let cnf (self:state) (si:SI.t) (module PA:SI.PREPROCESS_ACTS)
-      (t:T.t) : (T.t * _ Iter.t) option =
+  let cnf (self:state) (si:SI.t)
+      (module PA:SI.PREPROCESS_ACTS) (t:T.t) : unit =
     Log.debugf 50 (fun k->k"(@[th-bool.cnf@ %a@])" T.pp t);
-    let steps = ref [] in
-    let[@inline] add_step s = steps := s :: !steps in
 
     (* handle boolean equality *)
-    let equiv_ _si ~is_xor ~for_t t_a t_b : Lit.t =
-      let a = PA.mk_lit_nopreproc t_a in
-      let b = PA.mk_lit_nopreproc t_b in
+    let equiv_ _si ~is_xor ~t t_a t_b : unit =
+      let a = PA.mk_lit t_a in
+      let b = PA.mk_lit t_b in
       let a = if is_xor then Lit.neg a else a in (* [a xor b] is [(¬a) = b] *)
-      let t_proxy, proxy = fresh_lit ~for_t ~mk_lit:PA.mk_lit_nopreproc ~pre:"equiv_" self in
-
-      let pr_def = SI.P.define_term t_proxy for_t PA.proof in
-      add_step pr_def;
-
-      let[@inline] add_clause c pr = PA.add_clause c pr in
+      let lit = PA.mk_lit t in
 
       (* proxy => a<=> b,
          ¬proxy => a xor b *)
-      add_clause [Lit.neg proxy; Lit.neg a; b]
-        (pr_p1 PA.proof pr_def @@
-         if is_xor then A.lemma_bool_c "xor-e+" [for_t] PA.proof
-         else A.lemma_bool_c "eq-e" [for_t; t_a] PA.proof);
-      add_clause [Lit.neg proxy; Lit.neg b; a]
-        (pr_p1 PA.proof pr_def @@
-         if is_xor then A.lemma_bool_c "xor-e-" [for_t] PA.proof
-         else A.lemma_bool_c "eq-e" [for_t; t_b] PA.proof);
-      add_clause [proxy; a; b]
-        (pr_p1 PA.proof pr_def @@
-         if is_xor then A.lemma_bool_c "xor-i" [for_t; t_a] PA.proof
-         else A.lemma_bool_c "eq-i+" [for_t] PA.proof);
-      add_clause [proxy; Lit.neg a; Lit.neg b]
-        (pr_p1 PA.proof pr_def @@
-         if is_xor then A.lemma_bool_c "xor-i" [for_t; t_b] PA.proof
-         else A.lemma_bool_c "eq-i-" [for_t] PA.proof);
-      proxy
+      PA.add_clause [Lit.neg lit; Lit.neg a; b]
+        (if is_xor then A.lemma_bool_c "xor-e+" [t] PA.proof
+         else A.lemma_bool_c "eq-e" [t; t_a] PA.proof);
+      PA.add_clause [Lit.neg lit; Lit.neg b; a]
+        (if is_xor then A.lemma_bool_c "xor-e-" [t] PA.proof
+         else A.lemma_bool_c "eq-e" [t; t_b] PA.proof);
+      PA.add_clause [lit; a; b]
+        (if is_xor then A.lemma_bool_c "xor-i" [t; t_a] PA.proof
+         else A.lemma_bool_c "eq-i+" [t] PA.proof);
+      PA.add_clause [lit; Lit.neg a; Lit.neg b]
+        (if is_xor then A.lemma_bool_c "xor-i" [t; t_b] PA.proof
+         else A.lemma_bool_c "eq-i-" [t] PA.proof);
     in
 
     (* make a literal for [t], with a proof of [|- abs(t) = abs(lit)] *)
-    let rec get_lit_for_term_ t : Lit.t option =
-      match A.view_as_bool t with
-      | B_opaque_bool _ -> None
-      | B_bool _ -> None
-      | B_not u ->
-        let lit = get_lit_for_term_ u in
-        CCOpt.map Lit.neg lit
+    begin match A.view_as_bool t with
+      | B_opaque_bool _ -> ()
+      | B_bool _ -> ()
+      | B_not _ -> ()
 
       | B_and l ->
         let t_subs = Iter.to_list l in
-        let subs = List.map PA.mk_lit_nopreproc t_subs in
-        let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit_nopreproc ~pre:"and_" self in
-        let pr_def = SI.P.define_term t_proxy t PA.proof in
-        add_step pr_def;
+        let lit = PA.mk_lit t in
+        let subs = List.map PA.mk_lit t_subs in
 
         (* add clauses *)
         List.iter2
           (fun t_u u ->
              PA.add_clause
-               [Lit.neg proxy; u]
-               (pr_p1 PA.proof pr_def @@ A.lemma_bool_c "and-e" [t; t_u] PA.proof))
+               [Lit.neg lit; u]
+               (A.lemma_bool_c "and-e" [t; t_u] PA.proof))
           t_subs subs;
-        PA.add_clause (proxy :: List.map Lit.neg subs)
-          (pr_p1 PA.proof pr_def @@ A.lemma_bool_c "and-i" [t] PA.proof);
-        Some proxy
+        PA.add_clause (lit :: List.map Lit.neg subs)
+          (A.lemma_bool_c "and-i" [t] PA.proof);
 
       | B_or l ->
         let t_subs = Iter.to_list l in
-        let subs = List.map PA.mk_lit_nopreproc t_subs in
-        let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit_nopreproc ~pre:"or_" self in
-        let pr_def = SI.P.define_term t_proxy t PA.proof in
-        add_step pr_def;
+        let subs = List.map PA.mk_lit t_subs in
+        let lit = PA.mk_lit t in
 
         (* add clauses *)
         List.iter2
           (fun t_u u ->
-             PA.add_clause [Lit.neg u; proxy]
-               (pr_p1 PA.proof pr_def @@
-                A.lemma_bool_c "or-i" [t; t_u] PA.proof))
+             PA.add_clause [Lit.neg u; lit]
+               (A.lemma_bool_c "or-i" [t; t_u] PA.proof))
           t_subs subs;
-        PA.add_clause (Lit.neg proxy :: subs)
-          (pr_p1 PA.proof pr_def @@ A.lemma_bool_c "or-e" [t] PA.proof);
-        Some proxy
+        PA.add_clause (Lit.neg lit :: subs)
+          (A.lemma_bool_c "or-e" [t] PA.proof);
 
       | B_imply (t_args, t_u) ->
         (* transform into [¬args \/ u] on the fly *)
         let t_args = Iter.to_list t_args in
-        let args = List.map (fun t -> Lit.neg (PA.mk_lit_nopreproc t)) t_args in
-        let u = PA.mk_lit_nopreproc t_u in
+        let args = List.map (fun t -> Lit.neg (PA.mk_lit t)) t_args in
+        let u = PA.mk_lit t_u in
         let subs = u :: args in
 
         (* now the or-encoding *)
-        let t_proxy, proxy =
-          fresh_lit ~for_t:t ~mk_lit:PA.mk_lit_nopreproc ~pre:"implies_" self in
-        let pr_def = SI.P.define_term t_proxy t PA.proof in
-        add_step pr_def;
+        let lit = PA.mk_lit t in
 
         (* add clauses *)
         List.iter2
           (fun t_u u ->
-             PA.add_clause [Lit.neg u; proxy]
-               (pr_p1 PA.proof pr_def @@
-                A.lemma_bool_c "imp-i" [t_proxy; t_u] PA.proof))
+             PA.add_clause [Lit.neg u; lit]
+               (A.lemma_bool_c "imp-i" [t; t_u] PA.proof))
           (t_u::t_args) subs;
-        PA.add_clause (Lit.neg proxy :: subs)
-          (pr_p1 PA.proof pr_def @@
-           A.lemma_bool_c "imp-e" [t_proxy] PA.proof);
-        Some proxy
+        PA.add_clause (Lit.neg lit :: subs)
+          (A.lemma_bool_c "imp-e" [t] PA.proof);
 
-      | B_ite _ | B_eq _ | B_neq _ -> None
-      | B_equiv (a,b) -> Some (equiv_ si ~for_t:t ~is_xor:false a b)
-      | B_xor  (a,b) -> Some (equiv_ si ~for_t:t ~is_xor:true a b)
-      | B_atom _ -> None
-    in
+      | B_ite (a,b,c) ->
+        let lit_a = PA.mk_lit a in
+        PA.add_clause [Lit.neg lit_a; PA.mk_lit (eq self.tst t b)]
+          (A.lemma_ite_true ~ite:t PA.proof);
+        PA.add_clause [lit_a; PA.mk_lit (eq self.tst t c)]
+          (A.lemma_ite_false ~ite:t PA.proof);
 
-    begin match get_lit_for_term_ t with
-      | None -> None
-      | Some lit ->
-        let u = Lit.term lit in
-        (* put sign back as a "not" *)
-        let u = if Lit.sign lit then u else A.mk_bool self.tst (B_not u) in
-        if T.equal u t then None else Some (u, Iter.of_list !steps)
-    end
-
-  (* check if new terms were added to the congruence closure, that can be turned
-     into clauses *)
-  let check_new_terms (self:state) si (acts:SI.theory_actions) (_trail:_ Iter.t) : unit =
-    let cc_ = SI.cc si in
-    let all_terms =
-      let open SI in
-      CC.all_classes cc_
-      |> Iter.flat_map CC.N.iter_class
-      |> Iter.map CC.N.term
-    in
-    let cnf_of t =
-      let pacts = SI.preprocess_acts_of_acts si acts in
-      cnf self si pacts t
-    in
-    begin
-      all_terms
-        (fun t -> match cnf_of t with
-           | None -> ()
-           | Some (u, pr_t_u) ->
-             Log.debugf 5
-               (fun k->k "(@[th-bool-static.final-check.cnf@ %a@ :yields %a@])"
-                   T.pp t T.pp u);
-
-             (* produce a single step proof of [|- t=u] *)
-             let proof = SI.proof si in
-             let pr = SI.P.lemma_preprocess t u ~using:pr_t_u proof in
-             SI.CC.merge_t cc_ t u
-               (SI.CC.Expl.mk_theory t u [] pr);
-             ());
+      | B_eq _ | B_neq _ -> ()
+      | B_equiv (a,b) -> equiv_ si ~t ~is_xor:false a b
+      | B_xor  (a,b) -> equiv_ si ~t ~is_xor:true a b
+      | B_atom _ -> ()
     end;
     ()
 
@@ -440,12 +308,7 @@ module Make(A : ARG) : S with module A = A = struct
     Log.debug 2 "(th-bool.setup)";
     let st = create (SI.tst si) (SI.ty_st si) in
     SI.add_simplifier si (simplify st);
-    SI.on_preprocess si (preprocess st);
     SI.on_preprocess si (cnf st);
-    if A.check_congruence_classes then (
-      Log.debug 5 "(th-bool.add-final-check)";
-      SI.on_final_check si (check_new_terms st);
-    );
     st
 
   let theory =
diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml
index ffd2e2a6..bc3a37f5 100644
--- a/src/th-data/Sidekick_th_data.ml
+++ b/src/th-data/Sidekick_th_data.ml
@@ -309,10 +309,10 @@ module Make(A : ARG) : S with module A = A = struct
     N_tbl.pop_levels self.to_decide n;
     ()
 
-  let preprocess (self:t) si (acts:SI.preprocess_actions) (t:T.t) : _ option =
+  let preprocess (self:t) si (acts:SI.preprocess_actions) (t:T.t) : unit =
     let ty = T.ty t in
     match A.view_as_data t, A.as_datatype ty with
-    | T_cstor _, _ -> None
+    | T_cstor _, _ -> ()
     | _, Ty_data {cstors; _} ->
       begin match Iter.take 2 cstors |> Iter.to_rev_list with
         | [cstor] when not (T.Tbl.mem self.single_cstor_preproc_done t) ->
@@ -338,7 +338,7 @@ module Make(A : ARG) : S with module A = A = struct
           let proof =
             let pr_isa =
               A.P.lemma_isa_split t
-                (Iter.return @@ Act.mk_lit_nopreproc (A.mk_is_a self.tst cstor t))
+                (Iter.return @@ Act.mk_lit (A.mk_is_a self.tst cstor t))
                 self.proof
             and pr_eq_sel =
               A.P.lemma_select_cstor ~cstor_t:u t self.proof
@@ -349,12 +349,11 @@ module Make(A : ARG) : S with module A = A = struct
           T.Tbl.add self.single_cstor_preproc_done t (); (* avoid loops *)
           T.Tbl.add self.case_split_done t (); (* no need to decide *)
 
-          Act.add_clause [Act.mk_lit_nopreproc (A.mk_eq self.tst t u)] proof;
-          None
+          Act.add_clause [Act.mk_lit (A.mk_eq self.tst t u)] proof;
 
-        | _ -> None
+        | _ -> ()
       end
-    | _ -> None
+    | _ -> ()
 
   (* remember terms of a datatype *)
   let on_new_term_look_at_ty (self:t) n (t:T.t) : unit =