feat: proper proof production for theory merges in CC

this involves resolution steps between the lemma (typically a kind of
horn clause with the merge as conclusion) and a bunch of literals
responsible for some equational hypotheses of this horn clause, being true

src/base-solver/sidekick_base_solver.ml

@@ -13,6 +13,7 @@ module Solver_arg = struct
   module Lit = Sidekick_base.Lit
 
   let cc_view = Term.cc_view
+  let mk_eq = Term.eq
   let is_valid_literal _ = true
   module P = Sidekick_base.Proof
   type proof = P.t

src/base/Proof.ml

@@ -211,6 +211,11 @@ let proof_r1 unit c (self:t) =
   emit_ self @@ fun() ->
   PS.(Step_view.Step_proof_r1 {Step_proof_r1.c; unit})
 
+let proof_res ~pivot c1 c2 (self:t) =
+  emit_ self @@ fun() ->
+  let pivot = emit_term_ self pivot in
+  PS.(Step_view.Step_proof_res {Step_proof_res.c1; c2; pivot})
+
 let lemma_preprocess t u ~using (self:t) =
   emit_ self @@ fun () ->
   let t = emit_term_ self t and u = emit_term_ self u in

src/base/Proof_dummy.ml

@@ -21,6 +21,7 @@ let define_term _ _ _ = ()
 let emit_unsat _ _ = ()
 let proof_p1 _ _ (_pr:t) = ()
 let proof_r1 _ _ (_pr:t) = ()
+let proof_res ~pivot:_ _ _ (_pr:t) = ()
 let emit_unsat_core _ (_pr:t) = ()
 let lemma_preprocess _ _ ~using:_ (_pr:t) = ()
 let lemma_true _ _ = ()

src/base/Proof_quip.ml

@@ -259,6 +259,18 @@ end = struct
           ) in
           L_proofs.add lid p;
 
+        | PS.Step_view.Step_proof_res { pivot; c1; c2; } ->
+          add_needed_step c1;
+          add_needed_step c2;
+          add_needed_step pivot;
+          let p = lazy (
+            let pivot = L_terms.find pivot in
+            let c1 = L_proofs.find c2 in
+            let c2 = L_proofs.find c2 in
+            P.res ~pivot c1 c2
+          ) in
+          L_proofs.add lid p;
+
         | PS.Step_view.Step_bool_c { rule; exprs } ->
           Array.iter add_needed_step exprs;
           let p = lazy (

src/cc/Sidekick_cc.ml

@@ -444,15 +444,14 @@ module Make (A: CC_ARG)
     type t = {
       mutable lits: Lit.t list;
       mutable th_lemmas:
-        (Term.t * Term.t * Lit.t *
-         (Term.t * Term.t * Lit.t * Lit.t list) list * proof_step) list;
+        (Lit.t * (Lit.t * Lit.t list) list * proof_step) list;
     }
 
     let create(): t = { lits=[]; th_lemmas=[] }
 
     let[@inline] add_lit (self:t) lit = self.lits <- lit :: self.lits
-    let[@inline] add_th (self:t) t u lit l pr : unit =
-      self.th_lemmas <- (t,u,lit,l,pr) :: self.th_lemmas
+    let[@inline] add_th (self:t) lit hyps pr : unit =
+      self.th_lemmas <- (lit,hyps,pr) :: self.th_lemmas
 
     let merge self other =
       let {lits=o_lits; th_lemmas=o_lemmas} = other in
@@ -490,11 +489,11 @@ module Make (A: CC_ARG)
              (* use a separate call to [explain_expls] for each set *)
              let sub = explain_expls cc expls_i in
              Expl_state.merge st sub;
-             t_i, u_i, lit_i, sub.lits)
+             lit_i, sub.lits)
           expl_sets
       in
       let lit_t_u = A.mk_lit_eq cc.tst t u in
-      Expl_state.add_th st t u lit_t_u sub_proofs pr
+      Expl_state.add_th st lit_t_u sub_proofs pr
     | E_merge (a,b) -> explain_equal_rec_ cc st a b
     | E_merge_t (a,b) ->
       (* find nodes for [a] and [b] on the fly *)
@@ -619,6 +618,45 @@ module Make (A: CC_ARG)
   let n_is_bool_value (self:t) n : bool =
     N.equal n (n_true self) || N.equal n (n_false self)
 
+  (* gather a pair [lits, pr], where [lits] is the set of
+     asserted literals needed in the explanation (which is useful for
+     the SAT solver), and [pr] is a proof, including sub-proofs for theory
+     merges. *)
+  let lits_and_proof_of_expl
+      (self:t) (st:Expl_state.t) : Lit.t list * proof_step =
+    let {Expl_state.lits; th_lemmas} = st in
+    let proof = self.proof in
+    (* proof of [\/_i ¬lits[i]] *)
+    let pr =
+      let p_lits1 = Iter.of_list lits |> Iter.map Lit.neg in
+      let p_lits2 =
+        Iter.of_list th_lemmas
+        |> Iter.map (fun (lit_t_u,_,_) -> Lit.neg lit_t_u)
+      in
+      let p_cc = P.lemma_cc (Iter.append p_lits1 p_lits2) proof in
+      let resolve_with_th_proof pr (lit_t_u,sub_proofs,pr_th) =
+        (* pr_th: [sub_proofs |- t=u].
+              now resolve away [sub_proofs] to get literals that were
+              asserted in the congruence closure *)
+        let pr_th = List.fold_left
+            (fun pr_th (lit_i,hyps_i) ->
+               (* [hyps_i |- lit_i] *)
+               let lemma_i =
+                 P.lemma_cc Iter.(cons lit_i (of_list hyps_i |> map Lit.neg)) proof
+               in
+               (* resolve [lit_i] away. *)
+               P.proof_res ~pivot:(Lit.term lit_i) lemma_i pr_th proof)
+            pr_th sub_proofs
+        in
+        P.proof_res ~pivot:(Lit.term lit_t_u) pr_th pr proof
+      in
+
+
+      (* resolve with theory proofs responsible for some merges, if any. *)
+      List.fold_left resolve_with_th_proof p_cc th_lemmas
+    in
+    lits, pr
+
   (* main CC algo: add terms from [pending] to the signature table,
      check for collisions *)
   let rec update_tasks (cc:t) (acts:actions) : unit =
@@ -700,24 +738,8 @@ module Make (A: CC_ARG)
         explain_decompose_expl cc expl_st e_ab;
         explain_equal_rec_ cc expl_st a ra;
         explain_equal_rec_ cc expl_st b rb;
-        let {Expl_state.lits; th_lemmas} = expl_st in
-        let pr =
-          let proof = Actions.proof acts in
-          let p_lits1 = Iter.of_list lits |> Iter.map Lit.neg in
-          let p_lits2 =
-            Iter.of_list th_lemmas
-            |> Iter.map (fun (_,_,lit_t_u,_,_) -> Lit.neg lit_t_u)
-          in
-          let p_cc = P.lemma_cc (Iter.append p_lits1 p_lits2) proof in
-          List.fold_left
-            (fun pr (_,_,lit_t_u,sub_proofs,pr_th) ->
-               let pr_th = List.fold_left
-                   (fun pr_th (_,_,lit_i,pr_i) -> P.proof_r1 pr_i pr_th proof)
-                   pr_th sub_proofs
-               in
-               P.proof_r1 pr_th pr proof)
-            p_cc th_lemmas
-        in
+
+        let lits, pr = lits_and_proof_of_expl cc expl_st in
         raise_conflict_ cc ~th:!th acts (List.rev_map Lit.neg lits) pr
       );
       (* We will merge [r_from] into [r_into].
@@ -810,10 +832,11 @@ module Make (A: CC_ARG)
      We can explain the propagation with [u1 = t1 =e= t2 = r2==bool] *)
   and propagate_bools cc acts r1 t1 r2 t2 (e_12:explanation) sign : unit =
     (* explanation for [t1 =e= t2 = r2] *)
-    let half_expl = lazy (
-      let th = ref false in
-      let lits = explain_decompose_expl cc ~th [] e_12 in
-      th, explain_equal_rec_ cc ~th lits r2 t2
+    let half_expl_and_pr = lazy (
+      let st = Expl_state.create() in
+      explain_decompose_expl cc st e_12;
+      explain_equal_rec_ cc st r2 t2;
+      st
     ) in
     (* TODO: flag per class, `or`-ed on merge, to indicate if the class
        contains at least one lit *)
@@ -831,14 +854,11 @@ module Make (A: CC_ARG)
            (* complete explanation with the [u1=t1] chunk *)
            let reason =
              let e = lazy (
-               let lazy (th, acc) = half_expl in
-               let lits = explain_equal_rec_ cc ~th acc u1 t1 in
-               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 @@ Actions.proof acts
-               in
-               lits, pr
+               let lazy st = half_expl_and_pr in
+               explain_equal_rec_ cc st u1 t1;
+               (* assert that [guard /\ ¬lit] is absurd, to propagate [lit] *)
+               Expl_state.add_lit st (Lit.neg lit);
+               lits_and_proof_of_expl cc st
              ) in
              fun () -> Lazy.force e
            in
@@ -902,14 +922,12 @@ module Make (A: CC_ARG)
   let raise_conflict_from_expl cc (acts:actions) expl =
     Log.debugf 5
       (fun k->k "(@[cc.theory.raise-conflict@ :expl %a@])" Expl.pp expl);
-    let th = ref true in
-    let lits = explain_decompose_expl cc ~th [] expl in
-    let lits = List.rev_map Lit.neg lits in
-    let pr =
-      let p_lits = Iter.of_list lits in
-      P.lemma_cc p_lits @@ Actions.proof acts
-    in
-    raise_conflict_ cc ~th:!th acts lits pr
+    let st = Expl_state.create() in
+    explain_decompose_expl cc st expl;
+    let lits, pr = lits_and_proof_of_expl cc st in
+    let c = List.rev_map Lit.neg lits in
+    let th = st.th_lemmas <> [] in
+    raise_conflict_ cc ~th acts c pr
 
   let merge cc n1 n2 expl =
     Log.debugf 5
@@ -921,8 +939,10 @@ module Make (A: CC_ARG)
     merge cc (add_term cc t1) (add_term cc t2) expl
 
   let explain_eq cc n1 n2 : lit list =
-    let th = ref true in
-    explain_equal_rec_ cc ~th [] n1 n2
+    let st = Expl_state.create() in
+    explain_equal_rec_ cc st n1 n2;
+    (* FIXME: also need to return the proof? *)
+    st.lits
 
   let on_pre_merge cc f = cc.on_pre_merge <- f :: cc.on_pre_merge
   let on_post_merge cc f = cc.on_post_merge <- f :: cc.on_post_merge

src/core/Sidekick_core.ml

@@ -145,22 +145,6 @@ module type TERM = sig
   end
 end
 
-(** Proofs for the congruence closure *)
-module type CC_PROOF = sig
-  type proof_step
-  type t
-  type lit
-
-  val lemma_cc : lit Iter.t -> t -> proof_step
-  (** [lemma_cc proof lits] asserts that [lits] form a tautology for the theory
-      of uninterpreted functions. *)
-
-  val proof_r1 : proof_step -> proof_step -> t -> proof_step
-  (** [proof_r1 p1 p2], where [p1] proves the unit clause [|- t] (t:bool)
-      and [p2] proves [C \/ ¬t], is the rule that produces [C \/ u],
-      i.e unit resolution. *)
-end
-
 (** Signature for SAT-solver proof emission. *)
 module type SAT_PROOF = sig
   type t
@@ -214,17 +198,16 @@ module type PROOF = sig
   type lit
   type proof_rule = t -> proof_step
 
-  include CC_PROOF
-    with type t := t
-     and type lit := lit
-     and type proof_step := proof_step
-
   include SAT_PROOF
     with type t := t
      and type lit := lit
      and type proof_step := proof_step
      and type proof_rule := proof_rule
 
+  val lemma_cc : lit Iter.t -> proof_rule
+  (** [lemma_cc proof lits] asserts that [lits] form a tautology for the theory
+      of uninterpreted functions. *)
+
   val define_term : term -> term -> proof_rule
   (** [define_term cst u proof] defines the new constant [cst] as being equal
       to [u].
@@ -240,6 +223,11 @@ module type PROOF = sig
       and [p2] proves [C \/ ¬t], is the rule that produces [C \/ u],
       i.e unit resolution. *)
 
+  val proof_res : pivot:term -> proof_step -> proof_step -> proof_rule
+  (** [proof_res ~pivot p1 p2], where [p1] proves the clause [|- C \/ l]
+      and [p2] proves [D \/ ¬l], where [l] is either [pivot] or [¬pivot],
+      is the rule that produces [C \/ D], i.e boolean resolution. *)
+
   val with_defs : proof_step -> proof_step Iter.t -> proof_rule
   (** [with_defs pr defs] specifies that [pr] is valid only in
       a context where the definitions [defs] are present. *)
@@ -322,8 +310,10 @@ module type CC_ACTIONS = sig
 
   type proof
   type proof_step
-  module P : CC_PROOF with type lit = Lit.t
+  module P : PROOF
+    with type lit = Lit.t
      and type t = proof
+     and type term = T.Term.t
      and type proof_step = proof_step
 
   type t
@@ -356,9 +346,10 @@ module type CC_ARG = sig
   module Lit : LIT with module T = T
   type proof
   type proof_step
-  module P : CC_PROOF
+  module P : PROOF
     with type lit = Lit.t
      and type t = proof
+     and type term = T.Term.t
      and type proof_step = proof_step
   module Actions : CC_ACTIONS
     with module T=T
@@ -396,7 +387,7 @@ module type CC_S = sig
   module Lit : LIT with module T = T
   type proof
   type proof_step
-  module P : CC_PROOF
+  module P : PROOF
     with type lit = Lit.t
      and type t = proof
      and type proof_step = proof_step

src/proof-trace/proof_ser.bare

@@ -58,6 +58,13 @@ type Step_proof_r1 {
   c: ID
 }
 
+# resolve `c1` with `c2` on pivot `pivot` *)
+type Step_proof_res {
+  pivot: ID
+  c1: ID
+  c2: ID
+}
+
 type Step_bool_tauto {
   lits: []Lit
 }
@@ -122,6 +129,7 @@ type Step_view
   | Step_bool_c
   | Step_proof_p1
   | Step_proof_r1
+  | Step_proof_res
   | Step_true
   | Fun_decl
   | Expr_def

src/proof-trace/proof_ser.ml

@@ -612,6 +612,39 @@ module Step_proof_r1 = struct
 
 end
 
+module Step_proof_res = struct
+  type t = {
+    pivot: ID.t;
+    c1: ID.t;
+    c2: ID.t;
+  }
+  
+  (** @raise Bare.Decode.Error in case of error. *)
+  let decode (dec: Bare.Decode.t) : t =
+    let pivot = ID.decode dec in
+    let c1 = ID.decode dec in
+    let c2 = ID.decode dec in
+    {pivot; c1; c2; }
+  
+  let encode (enc: Bare.Encode.t) (self: t) : unit =
+    begin
+      ID.encode enc self.pivot;
+      ID.encode enc self.c1;
+      ID.encode enc self.c2;
+    end
+  
+  let pp out (self:t) : unit =
+    (fun out x ->
+     begin
+       Format.fprintf out "{ @[";
+       Format.fprintf out "pivot=%a;@ " ID.pp x.pivot;
+       Format.fprintf out "c1=%a;@ " ID.pp x.c1;
+       Format.fprintf out "c2=%a;@ " ID.pp x.c2;
+       Format.fprintf out "@]}";
+     end) out self
+
+end
+
 module Step_bool_tauto = struct
   type t = {
     lits: Lit.t array;
@@ -916,6 +949,7 @@ module Step_view = struct
     | Step_bool_c of Step_bool_c.t
     | Step_proof_p1 of Step_proof_p1.t
     | Step_proof_r1 of Step_proof_r1.t
+    | Step_proof_res of Step_proof_res.t
     | Step_true of Step_true.t
     | Fun_decl of Fun_decl.t
     | Expr_def of Expr_def.t
@@ -942,15 +976,16 @@ module Step_view = struct
     | 8L -> Step_bool_c (Step_bool_c.decode dec)
     | 9L -> Step_proof_p1 (Step_proof_p1.decode dec)
     | 10L -> Step_proof_r1 (Step_proof_r1.decode dec)
-    | 11L -> Step_true (Step_true.decode dec)
-    | 12L -> Fun_decl (Fun_decl.decode dec)
-    | 13L -> Expr_def (Expr_def.decode dec)
-    | 14L -> Expr_bool (Expr_bool.decode dec)
-    | 15L -> Expr_if (Expr_if.decode dec)
-    | 16L -> Expr_not (Expr_not.decode dec)
-    | 17L -> Expr_isa (Expr_isa.decode dec)
-    | 18L -> Expr_eq (Expr_eq.decode dec)
-    | 19L -> Expr_app (Expr_app.decode dec)
+    | 11L -> Step_proof_res (Step_proof_res.decode dec)
+    | 12L -> Step_true (Step_true.decode dec)
+    | 13L -> Fun_decl (Fun_decl.decode dec)
+    | 14L -> Expr_def (Expr_def.decode dec)
+    | 15L -> Expr_bool (Expr_bool.decode dec)
+    | 16L -> Expr_if (Expr_if.decode dec)
+    | 17L -> Expr_not (Expr_not.decode dec)
+    | 18L -> Expr_isa (Expr_isa.decode dec)
+    | 19L -> Expr_eq (Expr_eq.decode dec)
+    | 20L -> Expr_app (Expr_app.decode dec)
     | _ -> raise (Bare.Decode.Error(Printf.sprintf "unknown union tag Step_view.t: %Ld" tag))
     
   
@@ -989,32 +1024,35 @@ module Step_view = struct
     | Step_proof_r1 x ->
       Bare.Encode.uint enc 10L;
       Step_proof_r1.encode enc x
-    | Step_true x ->
+    | Step_proof_res x ->
       Bare.Encode.uint enc 11L;
+      Step_proof_res.encode enc x
+    | Step_true x ->
+      Bare.Encode.uint enc 12L;
       Step_true.encode enc x
     | Fun_decl x ->
-      Bare.Encode.uint enc 12L;
+      Bare.Encode.uint enc 13L;
       Fun_decl.encode enc x
     | Expr_def x ->
-      Bare.Encode.uint enc 13L;
+      Bare.Encode.uint enc 14L;
       Expr_def.encode enc x
     | Expr_bool x ->
-      Bare.Encode.uint enc 14L;
+      Bare.Encode.uint enc 15L;
       Expr_bool.encode enc x
     | Expr_if x ->
-      Bare.Encode.uint enc 15L;
+      Bare.Encode.uint enc 16L;
       Expr_if.encode enc x
     | Expr_not x ->
-      Bare.Encode.uint enc 16L;
+      Bare.Encode.uint enc 17L;
       Expr_not.encode enc x
     | Expr_isa x ->
-      Bare.Encode.uint enc 17L;
+      Bare.Encode.uint enc 18L;
       Expr_isa.encode enc x
     | Expr_eq x ->
-      Bare.Encode.uint enc 18L;
+      Bare.Encode.uint enc 19L;
       Expr_eq.encode enc x
     | Expr_app x ->
-      Bare.Encode.uint enc 19L;
+      Bare.Encode.uint enc 20L;
       Expr_app.encode enc x
     
     
@@ -1042,6 +1080,8 @@ module Step_view = struct
         Format.fprintf out "(@[Step_proof_p1@ %a@])" Step_proof_p1.pp x
       | Step_proof_r1 x ->
         Format.fprintf out "(@[Step_proof_r1@ %a@])" Step_proof_r1.pp x
+      | Step_proof_res x ->
+        Format.fprintf out "(@[Step_proof_res@ %a@])" Step_proof_res.pp x
       | Step_true x ->
         Format.fprintf out "(@[Step_true@ %a@])" Step_true.pp x
       | Fun_decl x ->

src/smt-solver/Sidekick_smt_solver.ml

@@ -22,6 +22,9 @@ module type ARG = sig
 
   val cc_view : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) CC_view.t
 
+  val mk_eq : T.Term.store -> T.Term.t -> T.Term.t -> T.Term.t
+  (** [mk_eq store t u] builds the term [t=u] *)
+
   val is_valid_literal : T.Term.t -> bool
   (** Is this a valid boolean literal? (e.g. is it a closed term, not inside
       a quantifier) *)
@@ -60,6 +63,7 @@ module Make(A : ARG)
     type nonrec proof = proof
     type nonrec proof_step = proof_step
     let cc_view = A.cc_view
+    let[@inline] mk_lit_eq ?sign store t u = A.Lit.atom ?sign store (A.mk_eq store t u)
 
     module Actions = struct
       module T = T

src/th-bool-static/Sidekick_th_bool_static.ml

@@ -413,7 +413,8 @@ module Make(A : ARG) : S with module A = A = struct
              (* 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 pr []);
+             SI.CC.merge_t cc_ t u
+               (SI.CC.Expl.mk_theory t u [] pr);
              ());
     end;
     ()

src/th-data/Sidekick_th_data.ml

@@ -180,20 +180,23 @@ module Make(A : ARG) : S with module A = A = struct
         (fun k->k "(@[%s.merge@ (@[:c1 %a@ %a@])@ (@[:c2 %a@ %a@])@])"
             name N.pp n1 pp c1 N.pp n2 pp c2);
 
-      let mk_expl pr =
-        Expl.mk_theory pr @@ [
+      let mk_expl t1 t2 pr =
+        Expl.mk_theory t1 t2 [
+          N.term n1, N.term n2, [
             e_n1_n2;
             Expl.mk_merge n1 c1.c_n;
             Expl.mk_merge n2 c2.c_n;
-        ]
+          ]] pr
       in
 
       if A.Cstor.equal c1.c_cstor c2.c_cstor then (
         (* same function: injectivity *)
 
         let expl_merge i =
-          mk_expl @@
-          A.P.lemma_cstor_inj (N.term c1.c_n) (N.term c2.c_n) i (SI.CC.proof cc)
+          let t1 = N.term c1.c_n in
+          let t2 = N.term c2.c_n in
+          mk_expl t1 t2 @@
+          A.P.lemma_cstor_inj t1 t2 i (SI.CC.proof cc)
         in
 
         assert (IArray.length c1.c_args = IArray.length c2.c_args);
@@ -205,8 +208,9 @@ module Make(A : ARG) : S with module A = A = struct
         (* different function: disjointness *)
 
         let expl =
-          mk_expl @@
-          A.P.lemma_cstor_distinct (N.term c1.c_n) (N.term c2.c_n) (SI.CC.proof cc)
+          let t1 = N.term c1.c_n and t2 = N.term c2.c_n in
+          mk_expl t1 t2 @@
+          A.P.lemma_cstor_distinct t1 t2 (SI.CC.proof cc)
         in
 
         Error expl
@@ -387,8 +391,10 @@ module Make(A : ARG) : S with module A = A = struct
             (fun k->k "(@[%s.on-new-term.is-a.reduce@ :t %a@ :to %B@ :n %a@ :sub-cstor %a@])"
                 name T.pp t is_true N.pp n Monoid_cstor.pp cstor);
           let pr = A.P.lemma_isa_cstor ~cstor_t:(N.term cstor.c_n) t (SI.CC.proof cc) in
-          SI.CC.merge cc n (SI.CC.n_bool cc is_true)
-            Expl.(mk_theory pr [mk_merge n_u cstor.c_n])
+          let n_bool = SI.CC.n_bool cc is_true in
+          SI.CC.merge cc n n_bool
+            Expl.(mk_theory (N.term n) (N.term n_bool)
+                    [N.term n_u, N.term cstor.c_n, [mk_merge n_u cstor.c_n]] pr)
       end
     | T_select (c_t, i, u) ->
       let n_u = SI.CC.add_term cc u in
@@ -402,7 +408,8 @@ module Make(A : ARG) : S with module A = A = struct
           let u_i = IArray.get cstor.c_args i in
           let pr = A.P.lemma_select_cstor ~cstor_t:(N.term cstor.c_n) t (SI.CC.proof cc) in
           SI.CC.merge cc n u_i
-            Expl.(mk_theory pr [mk_merge n_u cstor.c_n])
+            Expl.(mk_theory (N.term n) (N.term u_i)
+                    [N.term n_u, N.term cstor.c_n, [mk_merge n_u cstor.c_n]] pr)
         | Some _ -> ()
         | None ->
           N_tbl.add self.to_decide repr_u (); (* needs to be decided *)
@@ -422,10 +429,12 @@ module Make(A : ARG) : S with module A = A = struct
             name Monoid_parents.pp_is_a is_a2 is_true N.pp n1 N.pp n2 Monoid_cstor.pp c1);
       let pr =
         A.P.lemma_isa_cstor ~cstor_t:(N.term c1.c_n) (N.term is_a2.is_a_n) self.proof in
-      SI.CC.merge cc is_a2.is_a_n (SI.CC.n_bool cc is_true)
-        Expl.(mk_theory pr
-                [mk_merge n1 c1.c_n; mk_merge n1 n2;
-                 mk_merge n2 is_a2.is_a_arg])
+      let n_bool = SI.CC.n_bool cc is_true in
+      SI.CC.merge cc is_a2.is_a_n n_bool
+        (Expl.mk_theory (N.term is_a2.is_a_n) (N.term n_bool)
+           [N.term n1, N.term n2,
+            [Expl.mk_merge n1 c1.c_n; Expl.mk_merge n1 n2;
+             Expl.mk_merge n2 is_a2.is_a_arg]] pr)
     in
     let merge_select n1 (c1:Monoid_cstor.t) n2 (sel2:Monoid_parents.select) =
       if A.Cstor.equal c1.c_cstor sel2.sel_cstor then (
@@ -437,9 +446,10 @@ module Make(A : ARG) : S with module A = A = struct
           A.P.lemma_select_cstor ~cstor_t:(N.term c1.c_n) (N.term sel2.sel_n) self.proof in
         let u_i = IArray.get c1.c_args sel2.sel_idx in
         SI.CC.merge cc sel2.sel_n u_i
-          Expl.(mk_theory pr
-                  [mk_merge n1 c1.c_n; mk_merge n1 n2;
-                   mk_merge n2 sel2.sel_arg]);
+          (Expl.mk_theory (N.term sel2.sel_n) (N.term u_i)
+             [N.term n1, N.term n2,
+              [Expl.mk_merge n1 c1.c_n; Expl.mk_merge n1 n2;
+               Expl.mk_merge n2 sel2.sel_arg]] pr);
       )
     in
     let merge_c_p n1 n2 =
@@ -529,14 +539,16 @@ module Make(A : ARG) : S with module A = A = struct
               self.proof
           in
           let expl =
-            path
-            |> CCList.flat_map
+            let subs =
+              CCList.map
                 (fun (n,node) ->
+                   N.term n, N.term node.cstor_n,
                    [ Expl.mk_merge node.cstor_n node.repr;
                      Expl.mk_merge n node.repr;
                    ])
-            |> Expl.mk_theory pr
+                path
             in
+            Expl.mk_theory (N.term n) (N.term cstor_n) subs pr in
           Stat.incr self.stat_acycl_conflict;
           Log.debugf 5
             (fun k->k "(@[%s.acyclicity.raise_confl@ %a@ @[:path %a@]@])"
@@ -570,7 +582,9 @@ module Make(A : ARG) : S with module A = A = struct
           (fun k->k"(@[%s.assign-is-a@ :lhs %a@ :rhs %a@ :lit %a@])"
               name T.pp u  T.pp rhs SI.Lit.pp lit);
         let pr = A.P.lemma_isa_sel t self.proof in
-        SI.cc_merge_t solver acts u rhs (Expl.mk_theory pr [Expl.mk_lit lit])
+        SI.cc_merge_t solver acts u rhs
+          (Expl.mk_theory u rhs
+             [t, N.term (SI.CC.n_true @@ SI.cc solver), [Expl.mk_lit lit]] pr)
       | _ -> ()
     in
     Iter.iter check_lit trail