From d3537f2c3ffc24e26f4b0fe552c3f28e10f3b1a5 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Thu, 7 Oct 2021 20:49:39 -0400
Subject: [PATCH] wip: refactor proof

---
 src/cc/Sidekick_cc.ml                         |  24 +-
 src/core/Sidekick_core.ml                     |  73 +++---
 src/sat/Sidekick_sat.ml                       |   2 +-
 src/sat/Solver.ml                             |  75 +++---
 src/sat/Solver.mli                            |   2 +
 src/sat/Solver_intf.ml                        |  30 +--
 src/smt-solver/Sidekick_smt_solver.ml         | 247 +++++++++++-------
 src/th-bool-static/Sidekick_th_bool_static.ml |  18 +-
 src/util/Bag.ml                               |  11 +
 src/util/Bag.mli                              |   4 +
 10 files changed, 286 insertions(+), 200 deletions(-)

diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml
index 1b0c853e..9ab10f1f 100644
--- a/src/cc/Sidekick_cc.ml
+++ b/src/cc/Sidekick_cc.ml
@@ -29,7 +29,6 @@ module Make (A: CC_ARG)
   type fun_ = T.Fun.t
   type proof = A.proof
   type proof_step = A.proof_step
-  type proof_rule = proof -> proof_step
   type actions = Actions.t
 
   module Term = T.Term
@@ -281,7 +280,7 @@ module Make (A: CC_ARG)
   and ev_on_post_merge = t -> actions -> N.t -> N.t -> unit
   and ev_on_new_term = t -> N.t -> term -> unit
   and ev_on_conflict = t -> th:bool -> lit list -> unit
-  and ev_on_propagate = t -> lit -> (unit -> lit list * (proof -> unit)) -> unit
+  and ev_on_propagate = t -> lit -> (unit -> lit list * proof_step) -> unit
   and ev_on_is_subterm = N.t -> term -> unit
 
   let[@inline] size_ (r:repr) = r.n_size
@@ -374,7 +373,7 @@ module Make (A: CC_ARG)
         n.n_expl <- FL_none;
     end
 
-  let raise_conflict_ (cc:t) ~th (acts:actions) (e:lit list) p : _ =
+  let raise_conflict_ (cc:t) ~th (acts:actions) (e:lit list) (p:proof_step) : _ =
     Profile.instant "cc.conflict";
     (* clear tasks queue *)
     Vec.clear cc.pending;
@@ -658,10 +657,11 @@ module Make (A: CC_ARG)
         let lits = explain_decompose_expl cc ~th [] e_ab in
         let lits = explain_equal_rec_ cc ~th lits a ra in
         let lits = explain_equal_rec_ cc ~th lits b rb in
-        let emit_proof p =
+        let pr =
           let p_lits = Iter.of_list lits |> Iter.map Lit.neg in
-          P.lemma_cc p_lits p in
-        raise_conflict_ cc ~th:!th acts (List.rev_map Lit.neg lits) emit_proof
+          P.lemma_cc p_lits @@ Actions.proof acts
+        in
+        raise_conflict_ cc ~th:!th acts (List.rev_map Lit.neg lits) pr
       );
       (* We will merge [r_from] into [r_into].
          we try to ensure that [size ra <= size rb] in general, but always
@@ -776,12 +776,12 @@ module Make (A: CC_ARG)
              let e = lazy (
                let lazy (th, acc) = half_expl in
                let lits = explain_equal_rec_ cc ~th acc u1 t1 in
-               let emit_proof p =
+               let pr =
                  (* make a tautology, not a true guard *)
                  let p_lits = Iter.cons lit (Iter.of_list lits |> Iter.map Lit.neg) in
-                 P.lemma_cc p_lits p
+                 P.lemma_cc p_lits @@ Actions.proof acts
                in
-               lits, emit_proof
+               lits, pr
              ) in
              fun () -> Lazy.force e
            in
@@ -848,11 +848,11 @@ module Make (A: CC_ARG)
     let th = ref true in
     let lits = explain_decompose_expl cc ~th [] expl in
     let lits = List.rev_map Lit.neg lits in
-    let emit_proof p =
+    let pr =
       let p_lits = Iter.of_list lits in
-      P.lemma_cc p_lits p
+      P.lemma_cc p_lits @@ Actions.proof acts
     in
-    raise_conflict_ cc ~th:!th acts lits emit_proof
+    raise_conflict_ cc ~th:!th acts lits pr
 
   let merge cc n1 n2 expl =
     Log.debugf 5
diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml
index e009e342..26726dff 100644
--- a/src/core/Sidekick_core.ml
+++ b/src/core/Sidekick_core.ml
@@ -162,7 +162,7 @@ module type SAT_PROOF = sig
   (** The stored proof (possibly nil, possibly on disk, possibly in memory) *)
 
   type proof_step
-  (** identifier for a proof proof_rule *)
+  (** identifier for a proof *)
 
   module Step_vec : Vec_sig.S with type elt = proof_step
   (** A vector of steps *)
@@ -176,11 +176,6 @@ module type SAT_PROOF = sig
   val enabled : t -> bool
   (** Returns true if proof production is enabled *)
 
-  val with_proof : t -> (t -> 'a) -> 'a
-  (** If proof is enabled, call [f] on it to emit steps.
-      if proof is disabled, the callback won't even be called, and
-      a dummy proof_rule is returned. *)
-
   val emit_input_clause : lit Iter.t -> proof_rule
   (** Emit an input clause. *)
 
@@ -193,7 +188,7 @@ module type SAT_PROOF = sig
       FIXME: probably needs the list of proof_step that disprove the lits? *)
 
   val emit_unsat : proof_step -> t -> unit
-  (** Signal "unsat" result at the given proof_rule *)
+  (** Signal "unsat" result at the given proof *)
 
   val del_clause : proof_step -> t -> unit
   (** Forget a clause. Only useful for performance considerations. *)
@@ -248,6 +243,12 @@ module type PROOF = sig
 
       From now on, [t] and [u] will be used interchangeably.
       @return a proof_rule ID for the clause [(t=u)]. *)
+
+  val lemma_rw_clause : proof_step -> lit_rw:proof_step Iter.t -> proof_rule
+  (** [lemma_rw_clause prc ~lit_rw], where [prc] is the proof of [|- c],
+      uses the equations [|- p_i = q_i] from [lit_rw]
+      to rewrite some literals of [c] into [c']. This is used to preprocess
+      literals of a clause (using {!lemma_preprocess} individually). *)
 end
 
 (** Literals
@@ -307,21 +308,24 @@ module type CC_ACTIONS = sig
 
   type proof
   type proof_step
-  type proof_rule = proof -> proof_step
-  module P : CC_PROOF with type lit = Lit.t and type t = proof
+  module P : CC_PROOF with type lit = Lit.t
+                       and type t = proof
+                       and type proof_step = proof_step
 
   type t
   (** An action handle. It is used by the congruence closure
       to perform the actions below. How it performs the actions
       is not specified and is solver-specific. *)
 
-  val raise_conflict : t -> Lit.t list -> proof_rule -> 'a
+  val proof : t -> proof
+
+  val raise_conflict : t -> Lit.t list -> proof_step -> 'a
   (** [raise_conflict acts c pr] declares that [c] is a tautology of
       the theory of congruence. This does not return (it should raise an
       exception).
       @param pr the proof of [c] being a tautology *)
 
-  val propagate : t -> Lit.t -> reason:(unit -> Lit.t list * proof_rule) -> unit
+  val propagate : t -> Lit.t -> reason:(unit -> Lit.t list * proof_step) -> unit
   (** [propagate acts lit ~reason pr] declares that [reason() => lit]
       is a tautology.
 
@@ -375,7 +379,6 @@ module type CC_S = sig
   module Lit : LIT with module T = T
   type proof
   type proof_step
-  type proof_rule = proof -> proof_step
   module P : CC_PROOF
     with type lit = Lit.t
      and type t = proof
@@ -525,7 +528,7 @@ module type CC_S = sig
       participating in the conflict are purely syntactic theories
       like injectivity of constructors. *)
 
-  type ev_on_propagate = t -> lit -> (unit -> lit list * proof_rule) -> unit
+  type ev_on_propagate = t -> lit -> (unit -> lit list * proof_step) -> unit
   (** [ev_on_propagate cc lit reason] is called whenever [reason() => lit]
       is a propagated lemma. See {!CC_ACTIONS.propagate}. *)
 
@@ -680,8 +683,6 @@ module type SOLVER_INTERNAL = sig
   type clause_pool
   type proof
   type proof_step
-  type proof_rule = proof -> proof_step
-  (** Delayed proof. This is used to build a proof proof_rule on demand. *)
 
   (** {3 Proofs} *)
   module P : PROOF
@@ -698,7 +699,8 @@ module type SOLVER_INTERNAL = sig
   val ty_st : t -> ty_store
   val stats : t -> Stat.t
 
-  val with_proof : t -> (proof -> unit) -> unit
+  val proof : t -> proof
+  (** Access the proof object *)
 
   (** {3 Actions for the theories} *)
 
@@ -740,7 +742,8 @@ module type SOLVER_INTERNAL = sig
     val clear : t -> unit
     (** Reset internal cache, etc. *)
 
-    val with_proof : t -> (proof -> 'a) -> 'a
+    val proof : t -> proof
+    (** Access proof *)
 
     type hook = t -> term -> (term * proof_step Iter.t) option
     (** Given a term, try to simplify it. Return [None] if it didn't change.
@@ -749,12 +752,12 @@ module type SOLVER_INTERNAL = sig
         and if [t] is [app "+" (const x) (const y)] where [x] and [y] are number,
         returns [Some (const (x+y))], and [None] otherwise. *)
 
-    val normalize : t -> term -> (term * proof_step Iter.t) option
+    val normalize : t -> term -> (term * proof_step) 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 * proof_step Iter.t
+    val normalize_t : t -> term -> term * proof_step option
     (** Normalize a term using all the hooks, along with a proof that the
         simplification is correct.
         returns [t, ø] if no simplification occurred. *)
@@ -781,10 +784,14 @@ module type SOLVER_INTERNAL = sig
       Typically some clauses are also added to the solver. *)
 
   module type PREPROCESS_ACTS = sig
-    val mk_lit : ?sign:bool -> term -> lit
-    (** creates a new literal for a boolean term. *)
+    val proof : proof
 
-    val add_clause : lit list -> proof_rule -> unit
+    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. *)
 
     val add_lit : ?default_pol:bool -> lit -> unit
@@ -817,7 +824,7 @@ module type SOLVER_INTERNAL = sig
 
   (** {3 hooks for the theory} *)
 
-  val raise_conflict : t -> theory_actions -> lit list -> proof_rule -> 'a
+  val raise_conflict : t -> theory_actions -> lit list -> proof_step -> 'a
   (** Give a conflict clause to the solver *)
 
   val push_decision : t -> theory_actions -> lit -> unit
@@ -826,27 +833,27 @@ module type SOLVER_INTERNAL = sig
       If the SAT solver backtracks, this (potential) decision is removed
       and forgotten. *)
 
-  val propagate: t -> theory_actions -> lit -> reason:(unit -> lit list * proof_rule) -> unit
+  val propagate: t -> theory_actions -> lit -> reason:(unit -> lit list * proof_step) -> unit
   (** Propagate a boolean using a unit clause.
       [expl => lit] must be a theory lemma, that is, a T-tautology *)
 
-  val propagate_l: t -> theory_actions -> lit -> lit list -> proof_rule -> unit
+  val propagate_l: t -> theory_actions -> lit -> lit list -> proof_step -> unit
   (** Propagate a boolean using a unit clause.
       [expl => lit] must be a theory lemma, that is, a T-tautology *)
 
-  val add_clause_temp : t -> theory_actions -> lit list -> proof_rule -> unit
+  val add_clause_temp : t -> theory_actions -> lit list -> proof_step -> unit
   (** Add local clause to the SAT solver. This clause will be
       removed when the solver backtracks. *)
 
-  val add_clause_permanent : t -> theory_actions -> lit list -> proof_rule -> unit
+  val add_clause_permanent : t -> theory_actions -> lit list -> proof_step -> unit
   (** Add toplevel clause to the SAT solver. This clause will
       not be backtracked. *)
 
   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
-  (** Preprocess a term. The preprocessing proof is automatically emitted. *)
+  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
@@ -902,7 +909,7 @@ module type SOLVER_INTERNAL = sig
   val on_cc_conflict : t -> (CC.t -> th:bool -> lit list -> unit) -> unit
   (** Callback called on every CC conflict *)
 
-  val on_cc_propagate : t -> (CC.t -> lit -> (unit -> lit list * proof_rule) -> unit) -> unit
+  val on_cc_propagate : t -> (CC.t -> lit -> (unit -> lit list * proof_step) -> unit) -> unit
   (** Callback called on every CC propagation *)
 
   val on_partial_check : t -> (t -> theory_actions -> lit Iter.t -> unit) -> unit
@@ -972,8 +979,6 @@ module type SOLVER = sig
   type term = T.Term.t
   type ty = T.Ty.t
   type lit = Lit.t
-  type proof_rule = proof -> proof_step
-  (** Proof proof_rule. *)
 
   (** {3 A theory}
 
@@ -1108,11 +1113,11 @@ module type SOLVER = sig
 
       The proof of [|- lit = lit'] is directly added to the solver's proof. *)
 
-  val add_clause : t -> lit IArray.t -> proof_rule -> unit
+  val add_clause : t -> lit IArray.t -> proof_step -> unit
   (** [add_clause solver cs] adds a boolean clause to the solver.
       Subsequent calls to {!solve} will need to satisfy this clause. *)
 
-  val add_clause_l : t -> lit list -> proof_rule -> unit
+  val add_clause_l : t -> lit list -> proof_step -> unit
   (** Add a clause to the solver, given as a list. *)
 
   val assert_terms : t -> term list -> unit
diff --git a/src/sat/Sidekick_sat.ml b/src/sat/Sidekick_sat.ml
index fa07f294..ccbeda03 100644
--- a/src/sat/Sidekick_sat.ml
+++ b/src/sat/Sidekick_sat.ml
@@ -17,7 +17,7 @@ type ('lit, 'proof) reason = ('lit, 'proof) Solver_intf.reason =
   | Consequence of (unit -> 'lit list * 'proof) [@@unboxed]
 
 module type ACTS = Solver_intf.ACTS
-type ('lit, 'proof) acts = ('lit, 'proof) Solver_intf.acts
+type ('lit, 'proof, 'proof_step) acts = ('lit, 'proof, 'proof_step) Solver_intf.acts
 
 type negated = bool
 
diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml
index 347a6935..7832614c 100644
--- a/src/sat/Solver.ml
+++ b/src/sat/Solver.ml
@@ -20,7 +20,6 @@ module Make(Plugin : PLUGIN)
   type theory = Plugin.t
   type proof = Plugin.proof
   type proof_step = Plugin.proof_step
-  type proof_rule = proof -> proof_step
   type clause_pool_id = Clause_pool_id.t
 
   module Lit = Plugin.Lit
@@ -1074,7 +1073,7 @@ module Make(Plugin : PLUGIN)
         self.unsat_at_0 <- Some c;
         (match self.on_learnt with Some f -> f self c | None -> ());
         let p = Clause.proof_step self.store c in
-        Proof.with_proof self.proof (Proof.emit_unsat p);
+        Proof.emit_unsat p self.proof;
         US_false c
       | US_local _ -> us
     in
@@ -1410,10 +1409,10 @@ module Make(Plugin : PLUGIN)
           report_unsat self (US_false confl)
         ) else (
           let p =
-            Proof.with_proof self.proof @@
             Proof.emit_redundant_clause
               (Iter.of_array cr.cr_learnt |> Iter.map (Atom.lit self.store))
               ~hyps:(Step_vec.to_iter cr.cr_steps)
+              self.proof
           in
           let uclause = Clause.make_a store ~removable:true cr.cr_learnt p in
 
@@ -1425,10 +1424,9 @@ module Make(Plugin : PLUGIN)
       | _ ->
         let fuip = cr.cr_learnt.(0) in
         let p =
-          Proof.with_proof self.proof @@
           Proof.emit_redundant_clause
             (Iter.of_array cr.cr_learnt |> Iter.map (Atom.lit self.store))
-            ~hyps:(Step_vec.to_iter cr.cr_steps)
+            ~hyps:(Step_vec.to_iter cr.cr_steps) self.proof
         in
         let lclause = Clause.make_a store ~removable:true cr.cr_learnt p in
 
@@ -1620,21 +1618,17 @@ module Make(Plugin : PLUGIN)
 
   let[@inline] slice_get st i = AVec.get st.trail i
 
-  let acts_add_clause self ?(keep=false) (l:lit list) (proof_rule:proof_rule): unit =
+  let acts_add_clause self ?(keep=false) (l:lit list) (p:proof_step): unit =
     let atoms = List.rev_map (make_atom_ self) l in
     let removable = not keep in
-    let c =
-      let p = Proof.with_proof self.proof proof_rule in
-      Clause.make_l self.store ~removable atoms p in
+    let c = Clause.make_l self.store ~removable atoms p in
     Log.debugf 5 (fun k->k "(@[sat.th.add-clause@ %a@])" (Clause.debug self.store) c);
     CVec.push self.clauses_to_add_learnt c
 
-  let acts_add_clause_in_pool self ~pool (l:lit list) (proof_rule:proof_rule): unit =
+  let acts_add_clause_in_pool self ~pool (l:lit list) (p:proof_step): unit =
     let atoms = List.rev_map (make_atom_ self) l in
     let removable = true in
-    let c =
-      let p = Proof.with_proof self.proof proof_rule in
-      Clause.make_l self.store ~removable atoms p in
+    let c = Clause.make_l self.store ~removable atoms p in
     let pool = Vec.get self.clause_pools (pool:clause_pool_id:>int) in
     Log.debugf 5 (fun k->k "(@[sat.th.add-clause-in-pool@ %a@ :pool %s@])"
                      (Clause.debug self.store) c
@@ -1650,12 +1644,10 @@ module Make(Plugin : PLUGIN)
       self.next_decisions <- a :: self.next_decisions
     )
 
-  let acts_raise self (l:lit list) (proof_rule:proof_rule) : 'a =
+  let acts_raise self (l:lit list) (p:proof_step) : 'a =
     let atoms = List.rev_map (make_atom_ self) l in
     (* conflicts can be removed *)
-    let c =
-      let p = Proof.with_proof self.proof proof_rule in
-      Clause.make_l self.store ~removable:true atoms p in
+    let c = Clause.make_l self.store ~removable:true atoms p in
     Log.debugf 5 (fun k->k "(@[@{<yellow>sat.th.raise-conflict@}@ %a@])"
                      (Clause.debug self.store) c);
     raise_notrace (Th_conflict c)
@@ -1669,24 +1661,22 @@ module Make(Plugin : PLUGIN)
         (Atom.debug store) (Atom.neg a)
     | exception Not_found -> ()
 
-  let acts_propagate (self:t) f expl =
+  let acts_propagate (self:t) f (expl:(_,proof_step) Solver_intf.reason) =
     let store = self.store in
     match expl with
     | Solver_intf.Consequence mk_expl ->
       let p = make_atom_ self f in
       if Atom.is_true store p then ()
       else if Atom.is_false store p then (
-        let lits, proof_rule = mk_expl() in
+        let lits, proof = mk_expl() in
         let l = List.rev_map (fun f -> Atom.neg @@ make_atom_ self f) lits in
         check_consequence_lits_false_ self l;
-        let c =
-          let proof = Proof.with_proof self.proof proof_rule in
-          Clause.make_l store ~removable:true (p :: l) proof in
+        let c = Clause.make_l store ~removable:true (p :: l) proof in
         raise_notrace (Th_conflict c)
       ) else (
         insert_var_order self (Atom.var p);
         let c = lazy (
-          let lits, proof_rule = mk_expl () in
+          let lits, proof = mk_expl () in
           let l = List.rev_map (fun f -> Atom.neg @@ make_atom_ self f) lits in
           (* note: we can check that invariant here in the [lazy] block,
              as conflict analysis will run in an environment where
@@ -1695,7 +1685,6 @@ module Make(Plugin : PLUGIN)
              (otherwise the propagated lit would have been backtracked and
              discarded already.) *)
           check_consequence_lits_false_ self l;
-          let proof = Proof.with_proof self.proof proof_rule in
           Clause.make_l store ~removable:true (p :: l) proof
         ) in
         let level = decision_level self in
@@ -1725,9 +1714,9 @@ module Make(Plugin : PLUGIN)
     let module M = struct
       type nonrec proof = proof
       type nonrec proof_step = proof_step
-      type proof_rule = proof -> proof_step
       type nonrec clause_pool_id = clause_pool_id
       type nonrec lit = lit
+      let proof = st.proof
       let iter_assumptions=acts_iter st ~full:false st.th_head
       let eval_lit= acts_eval_lit st
       let add_lit=acts_add_lit st
@@ -1744,9 +1733,9 @@ module Make(Plugin : PLUGIN)
     let module M = struct
       type nonrec proof = proof
       type nonrec proof_step = proof_step
-      type proof_rule = proof -> proof_step
       type nonrec clause_pool_id = clause_pool_id
       type nonrec lit = lit
+      let proof = st.proof
       let iter_assumptions=acts_iter st ~full:true st.th_head
       let eval_lit= acts_eval_lit st
       let add_lit=acts_add_lit st
@@ -1901,8 +1890,7 @@ module Make(Plugin : PLUGIN)
       (match self.on_gc with
        | Some f -> let lits = Clause.lits_a store c in f self lits
        | None -> ());
-      Proof.with_proof self.proof
-        (Proof.del_clause (Clause.proof_step store c));
+      Proof.del_clause (Clause.proof_step store c) self.proof;
     in
 
     let gc_arg =
@@ -2098,9 +2086,7 @@ module Make(Plugin : PLUGIN)
     List.iter
       (fun l ->
          let atoms = Util.array_of_list_map (make_atom_ self) l in
-         let proof =
-           Proof.with_proof self.proof (Proof.emit_input_clause (Iter.of_list l))
-         in
+         let proof = Proof.emit_input_clause (Iter.of_list l) self.proof in
          let c = Clause.make_a self.store ~removable:false atoms proof in
          Log.debugf 10 (fun k -> k "(@[sat.assume-clause@ @[<hov 2>%a@]@])"
                            (Clause.debug self.store) c);
@@ -2162,7 +2148,7 @@ module Make(Plugin : PLUGIN)
           assert (Atom.equal first @@ List.hd core);
           let proof =
             let lits = Iter.of_list core |> Iter.map (Atom.lit self.store) in
-            Proof.with_proof self.proof (Proof.emit_unsat_core lits) in
+            Proof.emit_unsat_core lits self.proof in
           Clause.make_l self.store ~removable:false [] proof
         ) in
         fun () -> Lazy.force c
@@ -2179,27 +2165,26 @@ module Make(Plugin : PLUGIN)
     end in
     (module M)
 
-  let add_clause_atoms_ self ~pool ~removable (c:atom array) proof_rule : unit =
+  let add_clause_atoms_ self ~pool ~removable (c:atom array) (pr:proof_step) : unit =
     try
-      let proof = Proof.with_proof self.proof proof_rule in
-      let c = Clause.make_a self.store ~removable c proof in
+      let c = Clause.make_a self.store ~removable c pr in
       add_clause_ ~pool self c
     with
     | E_unsat (US_false c) ->
       self.unsat_at_0 <- Some c
 
-  let add_clause_a self c dp : unit =
+  let add_clause_a self c pr : unit =
     let c = Array.map (make_atom_ self) c in
-    add_clause_atoms_ ~pool:self.clauses_learnt ~removable:false self c dp
+    add_clause_atoms_ ~pool:self.clauses_learnt ~removable:false self c pr
 
-  let add_clause self (c:lit list) dp : unit =
+  let add_clause self (c:lit list) (pr:proof_step) : unit =
     let c = Util.array_of_list_map (make_atom_ self) c in
-    add_clause_atoms_ ~pool:self.clauses_learnt ~removable:false self c dp
+    add_clause_atoms_ ~pool:self.clauses_learnt ~removable:false self c pr
 
-  let add_clause_a_in_pool self ~pool c dp : unit =
+  let add_clause_a_in_pool self ~pool c (pr:proof_step) : unit =
     let c = Array.map (make_atom_ self) c in
     let pool = Vec.get self.clause_pools (pool:clause_pool_id:>int) in
-    add_clause_atoms_ ~pool ~removable:true self c dp
+    add_clause_atoms_ ~pool ~removable:true self c pr
 
   let add_clause_in_pool self ~pool (c:lit list) dp : unit =
     let c = Util.array_of_list_map (make_atom_ self) c in
@@ -2207,12 +2192,12 @@ module Make(Plugin : PLUGIN)
     add_clause_atoms_ ~pool ~removable:true self c dp
 
   let add_input_clause self (c:lit list) =
-    let dp = Proof.emit_input_clause (Iter.of_list c) in
-    add_clause self c dp
+    let pr = Proof.emit_input_clause (Iter.of_list c) self.proof in
+    add_clause self c pr
 
   let add_input_clause_a self c =
-    let dp = Proof.emit_input_clause (Iter.of_array c) in
-    add_clause_a self c dp
+    let pr = Proof.emit_input_clause (Iter.of_array c) self.proof in
+    add_clause_a self c pr
 
   let new_clause_pool_gc_fixed_size ~descr ~size (self:t) : clause_pool_id =
     let p =
diff --git a/src/sat/Solver.mli b/src/sat/Solver.mli
index bf79e97b..710a9e87 100644
--- a/src/sat/Solver.mli
+++ b/src/sat/Solver.mli
@@ -6,6 +6,7 @@ module Make_pure_sat(Th: Solver_intf.PLUGIN_SAT)
   : S with type lit = Th.lit
        and module Lit = Th.Lit
        and type proof = Th.proof
+       and type proof_step = Th.proof_step
        and module Proof = Th.Proof
        and type theory = unit
 
@@ -13,5 +14,6 @@ module Make_cdcl_t(Th : Solver_intf.PLUGIN_CDCL_T)
   : S with type lit = Th.lit
        and module Lit = Th.Lit
        and type proof = Th.proof
+       and type proof_step = Th.proof_step
        and module Proof = Th.Proof
        and type theory = Th.t
diff --git a/src/sat/Solver_intf.ml b/src/sat/Solver_intf.ml
index eb521412..7a6e3d79 100644
--- a/src/sat/Solver_intf.ml
+++ b/src/sat/Solver_intf.ml
@@ -104,7 +104,8 @@ module type ACTS = sig
   type proof
   type proof_step
   type clause_pool_id = Clause_pool_id.t
-  type proof_rule = proof -> proof_step
+
+  val proof : proof
 
   val iter_assumptions: (lit -> unit) -> unit
   (** Traverse the new assumptions on the boolean trail. *)
@@ -116,7 +117,7 @@ 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 -> proof_rule -> unit
+  val add_clause: ?keep:bool -> lit list -> proof_step -> 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
@@ -124,16 +125,16 @@ module type ACTS = sig
       - [C_use_allocator alloc] puts the clause in the given allocator.
   *)
 
-  val add_clause_in_pool : pool:clause_pool_id -> lit list -> proof_rule -> unit
+  val add_clause_in_pool : pool:clause_pool_id -> lit list -> proof_step -> unit
   (** Like {!add_clause} but uses a custom clause pool for the clause,
       with its own lifetime. *)
 
-  val raise_conflict: lit list -> proof_rule -> 'b
+  val raise_conflict: lit list -> proof_step -> 'b
   (** Raise a conflict, yielding control back to the solver.
       The list of atoms must be a valid theory lemma that is false in the
       current trail. *)
 
-  val propagate: lit -> (lit, proof_rule) reason -> unit
+  val propagate: lit -> (lit, proof_step) reason -> unit
   (** Propagate a lit, i.e. the theory can evaluate the lit to be true
       (see the definition of {!type:eval_res} *)
 
@@ -143,9 +144,10 @@ module type ACTS = sig
       Useful for theory combination. This will be undone on backtracking. *)
 end
 
-type ('lit, 'proof) acts =
+type ('lit, 'proof, 'proof_step) acts =
   (module ACTS with type lit = 'lit
-                and type proof = 'proof)
+                and type proof = 'proof
+                and type proof_step = 'proof_step)
 (** The type for a slice of assertions to assume/propagate in the theory. *)
 
 exception No_proof
@@ -203,12 +205,12 @@ module type PLUGIN_CDCL_T = sig
   val pop_levels : t -> int -> unit
   (** Pop [n] levels of the theory *)
 
-  val partial_check : t -> (lit, proof) acts -> unit
+  val partial_check : t -> (lit, proof, proof_step) acts -> unit
   (** Assume the lits in the slice, possibly using the [slice]
       to push new lits to be propagated or to raising a conflict or to add
       new lemmas. *)
 
-  val final_check : t -> (lit, proof) acts -> unit
+  val final_check : t -> (lit, proof, proof_step) acts -> unit
   (** Called at the end of the search in case a model has been found.
       If no new clause is pushed, then proof search ends and "sat" is returned;
       if lemmas are added, search is resumed;
@@ -251,8 +253,6 @@ module type S = sig
 
   type proof_step
 
-  type proof_rule = proof -> proof_step
-
   type solver
   (** The main solver type. *)
 
@@ -357,10 +357,10 @@ module type S = sig
   (** Add the list of clauses to the current set of assumptions.
       Modifies the sat solver state in place. *)
 
-  val add_clause : t -> lit list -> proof_rule -> unit
+  val add_clause : t -> lit list -> proof_step -> unit
   (** Lower level addition of clauses *)
 
-  val add_clause_a : t -> lit array -> proof_rule -> unit
+  val add_clause_a : t -> lit array -> proof_step -> unit
   (** Lower level addition of clauses *)
 
   val add_input_clause : t -> lit list -> unit
@@ -369,10 +369,10 @@ module type S = sig
   val add_input_clause_a : t -> lit array -> unit
   (** Like {!add_clause_a} but with justification of being an input clause *)
 
-  val add_clause_in_pool : t -> pool:clause_pool_id -> lit list -> proof_rule -> unit
+  val add_clause_in_pool : t -> pool:clause_pool_id -> lit list -> proof_step -> unit
   (** Like {!add_clause} but using a specific clause pool *)
 
-  val add_clause_a_in_pool : t -> pool:clause_pool_id -> lit array -> proof_rule -> unit
+  val add_clause_a_in_pool : t -> pool:clause_pool_id -> lit array -> proof_step -> unit
   (** Like {!add_clause_a} but using a specific clause pool *)
 
   (* TODO: API to push/pop/clear assumptions from an inner vector *)
diff --git a/src/smt-solver/Sidekick_smt_solver.ml b/src/smt-solver/Sidekick_smt_solver.ml
index 442eac14..ae260af2 100644
--- a/src/smt-solver/Sidekick_smt_solver.ml
+++ b/src/smt-solver/Sidekick_smt_solver.ml
@@ -47,11 +47,10 @@ module Make(A : ARG)
   type ty = Ty.t
   type proof = A.proof
   type proof_step = A.proof_step
-  type proof_rule = proof -> proof_step
   type lit = Lit.t
 
   (* actions from the sat solver *)
-  type sat_acts = (lit, proof) Sidekick_sat.acts
+  type sat_acts = (lit, proof, proof_step) Sidekick_sat.acts
 
   (* the full argument to the congruence closure *)
   module CC_actions = struct
@@ -59,6 +58,7 @@ module Make(A : ARG)
     module P = P
     module Lit = Lit
     type nonrec proof = proof
+    type nonrec proof_step = proof_step
     let cc_view = A.cc_view
 
     module Actions = struct
@@ -66,11 +66,14 @@ module Make(A : ARG)
       module P = P
       module Lit = Lit
       type nonrec proof = proof
-      type dproof = proof -> unit
+      type nonrec proof_step = proof_step
       type t = sat_acts
-      let[@inline] raise_conflict (a:t) lits (dp:dproof) =
+      let[@inline] proof (a:t) =
         let (module A) = a in
-        A.raise_conflict lits dp
+        A.proof
+      let[@inline] raise_conflict (a:t) lits (pr:proof_step) =
+        let (module A) = a in
+        A.raise_conflict lits pr
       let[@inline] propagate (a:t) lit ~reason =
         let (module A) = a in
         let reason = Sidekick_sat.Consequence reason in
@@ -90,7 +93,6 @@ module Make(A : ARG)
     module N = CC.N
     type nonrec proof = proof
     type nonrec proof_step = proof_step
-    type proof_rule = proof -> proof_step
     type term = Term.t
     type ty = Ty.t
     type lit = Lit.t
@@ -115,57 +117,78 @@ module Make(A : ARG)
         ty_st: ty_store;
         proof: proof;
         mutable hooks: hook list;
-        cache: Term.t Term.Tbl.t;
+        (* store [t --> u by proof_steps] in the cache.
+           We use a bag for the proof steps because it gives us structural
+           sharing of subproofs. *)
+        cache: (Term.t * proof_step Bag.t) Term.Tbl.t;
       }
-      and hook = t -> term -> term option
+
+      and hook = t -> term -> (term * proof_step Iter.t) option
 
       let create tst ty_st ~proof : t =
         {tst; ty_st; proof; hooks=[]; cache=Term.Tbl.create 32;}
 
       let[@inline] tst self = self.tst
       let[@inline] ty_st self = self.ty_st
-      let[@inline] with_proof self f = P.with_proof self.proof f
+      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 option =
+      let normalize (self:t) (t:Term.t) : (Term.t * proof_step) option =
         (* compute and cache normal form of [t] *)
-        let rec aux t : Term.t =
+        let rec loop t : Term.t * _ Bag.t =
           match Term.Tbl.find self.cache t with
-          | u -> u
+          | res -> res
           | exception Not_found ->
-            let u = aux_rec t self.hooks in
-            Term.Tbl.add self.cache t u;
-            u
+            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 t hooks = match hooks with
+        and aux_rec ~steps t hooks : Term.t =
+          match hooks with
           | [] ->
-            let u = Term.map_shallow self.tst aux t in
-            if Term.equal t u then t else aux u
+            let u = Term.map_shallow self.tst (loop_add ~steps) 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 t hooks_tl
-            | Some u when Term.equal t u -> aux_rec t hooks_tl
-            | Some u -> aux u (* fixpoint *)
+            | 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 = aux t in
+        let u, pr_u = loop t in
         if Term.equal t u then None
         else (
           (* proof: [sub_proofs |- t=u] by CC + subproof *)
-          P.with_proof self.proof (P.lemma_preprocess t u);
-          Some u
+          let step =
+            P.lemma_preprocess t u ~using:(Bag.to_iter pr_u) self.proof in
+          Some (u, step)
         )
 
       let normalize_t self t =
         match normalize self t with
-        | Some u -> u
-        | None -> t
+        | Some (u, pr_u) -> u, Some pr_u
+        | None -> t, None
     end
     type simplify_hook = Simplify.hook
 
     module type PREPROCESS_ACTS = sig
-      val mk_lit : ?sign:bool -> term -> lit
-      val add_clause : lit list -> proof_rule -> unit
+      val proof : proof
+      val mk_lit : ?sign:bool -> term -> lit * proof_step option
+      val add_clause : lit list -> proof_step -> unit
       val add_lit : ?default_pol:bool -> lit -> unit
     end
     type preprocess_actions = (module PREPROCESS_ACTS)
@@ -184,7 +207,7 @@ module Make(A : ARG)
       simp: Simplify.t;
       mutable preprocess: preprocess_hook list;
       mutable mk_model: model_hook list;
-      preprocess_cache: Term.t Term.Tbl.t;
+      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;
@@ -195,7 +218,7 @@ module Make(A : ARG)
     and preprocess_hook =
       t ->
       preprocess_actions ->
-      term -> term option
+      term -> (term * proof_step Iter.t) option
 
     and model_hook =
       recurse:(t -> CC.N.t -> term) ->
@@ -208,7 +231,7 @@ module Make(A : ARG)
     let[@inline] cc (t:t) = Lazy.force t.cc
     let[@inline] tst t = t.tst
     let[@inline] ty_st t = t.ty_st
-    let[@inline] with_proof self f = Proof.with_proof self.proof f
+    let[@inline] proof self = self.proof
     let stats t = t.stat
 
     let define_const (self:t) ~const ~rhs : unit =
@@ -216,7 +239,7 @@ module Make(A : ARG)
 
     let simplifier self = self.simp
     let simplify_t self (t:Term.t) : _ option = Simplify.normalize self.simp t
-    let simp_t self (t:Term.t) : Term.t = Simplify.normalize_t self.simp t
+    let simp_t self (t:Term.t) : Term.t * _ = Simplify.normalize_t self.simp t
 
     let add_simplifier (self:t) f : unit = Simplify.add_hook self.simp f
 
@@ -241,12 +264,12 @@ 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:proof_rule) : unit =
+    let add_sat_clause_ self (acts:theory_actions) ~keep lits (proof:proof_step) : unit =
       let (module A) = acts in
       Stat.incr self.count_axiom;
       A.add_clause ~keep lits proof
 
-    let add_sat_clause_pool_ self (acts:theory_actions) ~pool lits (proof:proof_rule) : unit =
+    let add_sat_clause_pool_ self (acts:theory_actions) ~pool lits (proof:proof_step) : unit =
       let (module A) = acts in
       Stat.incr self.count_axiom;
       A.add_clause_in_pool ~pool lits proof
@@ -258,7 +281,7 @@ module Make(A : ARG)
     (* 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 =
+    let preprocess_term_ (self:t) (module A0:PREPROCESS_ACTS) (t:term) : term * proof_step option =
       let mk_lit_nopreproc t = Lit.atom self.tst t in (* no further simplification *)
 
       (* compute and cache normal form [u] of [t].
@@ -268,19 +291,23 @@ module Make(A : ARG)
          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 t : term =
+      let rec preproc_rec ~steps t : term =
         match Term.Tbl.find self.preprocess_cache t with
-        | u -> u
+        | u, pr_u ->
+          steps := Bag.append pr_u !steps;
+          u
+
         | exception Not_found ->
           (* try rewrite at root *)
-          let t1 = preproc_with_hooks t self.preprocess in
+          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 t1 in
+          let t2 = Term.map_shallow self.tst (preproc_rec ~steps) t1 in
 
           let u =
             if not (Term.equal t t2) then (
-              preproc_rec t2 (* fixpoint *)
+              preproc_rec ~steps t2 (* fixpoint *)
             ) else (
               t2
             )
@@ -308,75 +335,103 @@ module Make(A : ARG)
                   Term.pp t Term.pp u);
           );
 
-          Term.Tbl.add self.preprocess_cache t u;
+          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 t hooks : term =
+      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 t hooks_tl
-          | Some u -> preproc_rec u
+          | 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 =
-        let u = preproc_rec t in
-        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);
-        );
-        Lit.atom self.tst ?sign u
+      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);
 
-      and preprocess_lit (lit:lit) : lit =
+            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
-        mk_lit ~sign t
+        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 =
-            let lit = preprocess_lit lit in
+            (* just drop the proof *)
+            let lit = preprocess_lit ~steps:(ref []) lit in
             A0.add_lit ?default_pol lit
-          let add_clause c pr =
+          let add_clause c pr_c =
             Stat.incr self.count_preprocess_clause;
-            let c = CCList.map preprocess_lit c in
-            A0.add_clause c pr
+            let steps = ref [] in
+            let c' = CCList.map (preprocess_lit ~steps) c in
+            let pr_c' =
+              if !steps=[] then pr_c
+              else A.P.lemma_rw_clause pr_c ~lit_rw:(Iter.of_list !steps) proof
+            in
+            A0.add_clause c' pr_c'
+
           let mk_lit = mk_lit
         end : PREPROCESS_ACTS)
       ) in
 
-      P.begin_subproof self.proof;
+      let steps = ref Bag.empty in
+      let[@inline] add_step s = steps := Bag.cons s !steps in
 
       (* simplify the term *)
-      let t1 = simp_t self t in
+      let t1, pr_1 = simp_t self t in
+      CCOpt.iter add_step pr_1;
 
       (* preprocess *)
-      let u = preproc_rec t1 in
-      (* emit [|- t=u] *)
-      if not (Term.equal t u) then (
-        P.with_proof self.proof (P.lemma_preprocess t u);
-      );
+      let u = preproc_rec ~steps t1 in
 
-      P.end_subproof self.proof;
-      u
+      (* 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
+      in
+
+      u, pr_u
 
     (* return preprocessed lit *)
-    let preprocess_lit_ (self:t) (pacts:preprocess_actions) (lit:lit) : lit =
+    let preprocess_lit_ ~steps (self:t) (pacts:preprocess_actions) (lit:lit) : lit =
       let t = Lit.term lit in
       let sign = Lit.sign lit in
-      let u = preprocess_term_ self pacts t 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
 
     (* add a clause using [acts] *)
-    let add_clause_ self acts lits (proof:proof_rule) : unit =
+    let add_clause_ self acts lits (proof:proof_step) : unit =
       add_sat_clause_ self acts ~keep:true lits proof
 
     let[@inline] add_lit _self (acts:theory_actions) ?default_pol lit : unit =
@@ -385,30 +440,41 @@ module Make(A : ARG)
 
     let preprocess_acts_of_acts (self:t) (acts:theory_actions) : preprocess_actions =
       (module struct
-        let mk_lit ?sign t = Lit.atom self.tst ?sign t
+        let proof = self.proof
+        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
       end)
 
-    let preprocess_clause_ (self:t) (acts:theory_actions) (c:lit list) : lit list =
+    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_ self pacts) c in
-      c
+      let c = CCList.map (preprocess_lit_ ~steps self pacts) c in
+      let pr =
+        if !steps=[] then proof
+        else (
+          P.lemma_rw_clause proof ~lit_rw:(Iter.of_list !steps) self.proof
+        )
+      in
+      c, pr
 
     (* make literal and preprocess it *)
     let[@inline] mk_plit (self:t) (pacts:preprocess_actions) ?sign (t:term) : lit =
       let lit = Lit.atom self.tst ?sign t in
-      preprocess_lit_ self pacts lit
+      let steps = ref [] in
+      preprocess_lit_ ~steps self pacts lit
 
-    let[@inline] preprocess_term self (pacts:preprocess_actions) (t:term) : term =
+    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_rule) : unit =
-      let c = preprocess_clause_ self acts c in
+    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_rule) : unit =
-      let c = preprocess_clause_ self acts c in
+    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 =
@@ -613,7 +679,7 @@ module Make(A : ARG)
       let t_true = Term.bool tst true in
       Sat_solver.add_clause self.solver
         [Lit.atom tst t_true]
-        (P.lemma_true t_true)
+        (P.lemma_true t_true self.proof)
     end;
     self
 
@@ -626,7 +692,8 @@ module Make(A : ARG)
   let preprocess_acts_of_solver_
       (self:t) : (module Solver_internal.PREPROCESS_ACTS) =
     (module struct
-      let mk_lit ?sign t = Lit.atom ?sign self.si.tst t
+      let proof = self.proof
+      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 =
@@ -634,9 +701,9 @@ module Make(A : ARG)
     end)
 
   (* preprocess literal *)
-  let preprocess_lit_ (self:t) (lit:lit) : lit =
+  let preprocess_lit_ ~steps (self:t) (lit:lit) : lit =
     let pacts = preprocess_acts_of_solver_ self in
-    Solver_internal.preprocess_lit_ self.si pacts lit
+    Solver_internal.preprocess_lit_ ~steps self.si pacts lit
 
   (* make a literal from a term, ensuring it is properly preprocessed *)
   let mk_lit_t (self:t) ?sign (t:term) : lit =
@@ -692,7 +759,7 @@ module Make(A : ARG)
   let pp_stats out (self:t) : unit =
     Stat.pp_all out (Stat.all @@ stats self)
 
-  let add_clause (self:t) (c:lit IArray.t) (proof:proof_rule) : unit =
+  let add_clause (self:t) (c:lit IArray.t) (proof:proof_step) : unit =
     Stat.incr self.count_clause;
     Log.debugf 50 (fun k->
         k "(@[solver.add-clause@ %a@])"
@@ -704,12 +771,16 @@ module Make(A : ARG)
   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_ self) 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 dp = P.emit_input_clause (Iter.of_list c) in
-    add_clause_l self c dp
+    let pr = P.emit_input_clause (Iter.of_list c) self.proof in
+    let pr = if !steps=[] then pr
+      else P.lemma_rw_clause pr ~lit_rw:(Iter.of_list !steps) self.proof
+    in
+    add_clause_l self c pr
 
   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 cd469f07..6fa88936 100644
--- a/src/th-bool-static/Sidekick_th_bool_static.ml
+++ b/src/th-bool-static/Sidekick_th_bool_static.ml
@@ -189,6 +189,14 @@ 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 p1_opt s1 s2 p : SI.proof_step =
+    let s2 = s2 p in
+    CCOpt.map_or ~default:s2 (fun s1 -> SI.P.proof_p1 s1 s2 p) s1
+
+  let p1_map s1 s2 p =
+    let s2 = s2 p in
+    SI.P.proof_p1 s1 s2 p
+
   (* preprocess "ite" away *)
   let preproc_ite self si (module PA:SI.PREPROCESS_ACTS) (t:T.t) : (T.t * SI.proof_step Iter.t) option =
     let steps = ref [] in
@@ -212,14 +220,14 @@ module Make(A : ARG) : S with module A = A = struct
         | _ ->
           let t_ite = fresh_term self ~for_t:t ~pre:"ite" (T.ty b) in
           SI.define_const si ~const:t_ite ~rhs:t;
-          let pr = SI.with_proof si (SI.P.define_term t_ite t) in
+          let pr_def = SI.with_proof si (SI.P.define_term t_ite t) in
           let lit_a = PA.mk_lit a' in
           (* TODO: use unit paramod on each clause with side t=t_ite and on a=a' *)
           PA.add_clause [Lit.neg lit_a; PA.mk_lit (eq self.tst t_ite b)]
-            (fun p -> SI.P.proof_p1 pr_a (A.lemma_ite_true ~a:a' ~ite:t p) p);
+            (p1_map pr_def @@ p1_opt pr_a (A.lemma_ite_true ~a:a' ~ite:t));
           PA.add_clause [lit_a; PA.mk_lit (eq self.tst t_ite c)]
-            (fun p -> A.lemma_ite_false p ~a:a' ~ite:t);
-          Some t_ite
+            (p1_map pr_def @@ p1_opt pr_a (A.lemma_ite_false ~a:a' ~ite:t));
+          ret t_ite
       end
     | _ -> None
 
@@ -237,7 +245,7 @@ module Make(A : ARG) : S with module A = A = struct
       let t_proxy, proxy = fresh_lit ~for_t ~mk_lit:PA.mk_lit ~pre:"equiv_" self in
 
       SI.define_const si ~const:t_proxy ~rhs:for_t;
-      SI.with_proof si (SI.P.define_term t_proxy for_t);
+      let pr_def = SI.with_proof si (SI.P.define_term t_proxy for_t) in
 
       let add_clause c pr =
         PA.add_clause c pr
diff --git a/src/util/Bag.ml b/src/util/Bag.ml
index b8fc38db..30e5c2b3 100644
--- a/src/util/Bag.ml
+++ b/src/util/Bag.ml
@@ -29,6 +29,17 @@ let cons x t = match t with
   | L _ -> N (L x, t)
   | N (_,_) -> N (L x, t)
 
+let snoc t x = match t with
+  | E -> L x
+  | L _ -> N (t, L x)
+  | N (_, _) -> N (t, L x)
+
+let of_iter i =
+  let r = ref empty in
+
+  i (fun x -> r := snoc !r x);
+  !r
+
 let rec fold f acc = function
   | E -> acc
   | L x -> f acc x
diff --git a/src/util/Bag.mli b/src/util/Bag.mli
index f205df93..09618d29 100644
--- a/src/util/Bag.mli
+++ b/src/util/Bag.mli
@@ -19,8 +19,12 @@ val return : 'a -> 'a t
 
 val cons : 'a -> 'a t -> 'a t
 
+val snoc : 'a t -> 'a -> 'a t
+
 val append : 'a t -> 'a t -> 'a t
 
+val of_iter : 'a Iter.t -> 'a t
+
 val to_iter : 'a t -> 'a Iter.t
 
 val fold : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a