Merge branch 'wip-datatype-proofs'

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

@@ -84,6 +84,7 @@ end = struct
   let conv_clause (c:PS.Clause.t) : P.clause lazy_t = conv_lits c.lits
 
   let name_clause (id: PS.ID.t) : string = Printf.sprintf "c%ld" id
+  let name_step (id: PS.ID.t) : string = Printf.sprintf "s%ld" id
   let name_term (id: PS.ID.t) : string = Printf.sprintf "t%ld" id
 
   (* TODO: see if we can allow `(stepc c5 (cl …) (… (@ c5) …))`.
@@ -259,14 +260,28 @@ end = struct
           ) in
           L_proofs.add lid p;
 
-        | PS.Step_view.Step_bool_c { rule; exprs } ->
+        | PS.Step_view.Step_proof_res { pivot; c1; c2; } ->
-          Array.iter add_needed_step exprs;
+          add_needed_step c1;
+          add_needed_step c2;
+          add_needed_step pivot;
           let p = lazy (
-            let exprs = Util.array_to_list_map L_terms.find exprs in
+            let pivot = L_terms.find pivot in
-            P.bool_c rule exprs
+            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 } ->
+          let name = name_step lid in
+          Array.iter add_needed_step exprs;
+          let step = lazy (
+            let exprs = Util.array_to_list_map L_terms.find exprs in
+            P.step_anon ~name @@ P.bool_c rule exprs
+          ) in
+          add_top_step step;
+          L_proofs.add lid (lazy (P.ref_by_name name));
+
         | PS.Step_view.Step_preprocess { t; u; using } ->
           let name = name_clause lid in
           add_needed_step t;

src/cc/Sidekick_cc.ml

@@ -96,7 +96,7 @@ module Make (A: CC_ARG)
     | E_merge_t of term * term
     | E_congruence of node * node (* caused by normal congruence *)
     | E_and of explanation * explanation
-    | E_theory of proof_step * explanation list
+    | E_theory of term * term * (term * term * explanation list) list * proof_step
 
   type repr = node
 
@@ -166,8 +166,12 @@ module Make (A: CC_ARG)
       | E_lit lit -> Lit.pp out lit
       | E_congruence (n1,n2) -> Fmt.fprintf out "(@[congruence@ %a@ %a@])" N.pp n1 N.pp n2
       | E_merge (a,b) -> Fmt.fprintf out "(@[merge@ %a@ %a@])" N.pp a N.pp b
-      | E_merge_t (a,b) -> Fmt.fprintf out "(@[<hv>merge@ @[:n1 %a@]@ @[:n2 %a@]@])" Term.pp a Term.pp b
+      | E_merge_t (a,b) ->
-      | E_theory (_p,es) -> Fmt.fprintf out "(@[th@ %a@])" (Util.pp_list pp) es
+        Fmt.fprintf out "(@[<hv>merge@ @[:n1 %a@]@ @[:n2 %a@]@])" Term.pp a Term.pp b
+      | E_theory (t,u,es,_) ->
+        Fmt.fprintf out "(@[th@ :t `%a`@ :u `%a`@ :expl_sets %a@])"
+          Term.pp t Term.pp u
+          (Util.pp_list @@ Fmt.Dump.triple Term.pp Term.pp (Fmt.Dump.list pp)) es
       | E_and (a,b) ->
         Format.fprintf out "(@[<hv1>and@ %a@ %a@])" pp a pp b
 
@@ -176,7 +180,7 @@ module Make (A: CC_ARG)
     let[@inline] mk_merge a b : t = if N.equal a b then mk_reduction else E_merge (a,b)
     let[@inline] mk_merge_t a b : t = if Term.equal a b then mk_reduction else E_merge_t (a,b)
     let[@inline] mk_lit l : t = E_lit l
-    let[@inline] mk_theory p es = E_theory (p,es)
+    let[@inline] mk_theory t u es pr = E_theory (t,u,es,pr)
 
     let rec mk_list l =
       match l with
@@ -436,72 +440,99 @@ module Make (A: CC_ARG)
     cleanup_ b;
     n
 
+  module Expl_state = struct
+    type t = {
+      mutable lits: Lit.t list;
+      mutable th_lemmas:
+        (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) 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
+      self.lits <- List.rev_append o_lits self.lits;
+      self.th_lemmas <- List.rev_append o_lemmas self.th_lemmas
+  end
+
   (* decompose explanation [e] into a list of literals added to [acc] *)
-  let rec explain_decompose_expl cc ~th (acc:lit list) (e:explanation) : _ list =
+  let rec explain_decompose_expl cc (st:Expl_state.t) (e:explanation) : unit =
     Log.debugf 5 (fun k->k "(@[cc.decompose_expl@ %a@])" Expl.pp e);
     match e with
-    | E_reduction -> acc
+    | E_reduction -> ()
     | E_congruence (n1, n2) ->
       begin match n1.n_sig0, n2.n_sig0 with
         | Some (App_fun (f1, a1)), Some (App_fun (f2, a2)) ->
           assert (Fun.equal f1 f2);
           assert (List.length a1 = List.length a2);
-          List.fold_left2 (explain_equal_rec_ cc ~th) acc a1 a2
+          List.iter2 (explain_equal_rec_ cc st) a1 a2
         | Some (App_ho (f1, a1)), Some (App_ho (f2, a2)) ->
-          let acc = explain_equal_rec_ cc ~th acc f1 f2 in
+          explain_equal_rec_ cc st f1 f2;
-          explain_equal_rec_ cc ~th acc a1 a2
+          explain_equal_rec_ cc st a1 a2
         | Some (If (a1,b1,c1)), Some (If (a2,b2,c2)) ->
-          let acc = explain_equal_rec_ cc ~th acc a1 a2 in
+          explain_equal_rec_ cc st a1 a2;
-          let acc = explain_equal_rec_ cc ~th acc b1 b2 in
+          explain_equal_rec_ cc st b1 b2;
-          explain_equal_rec_ cc ~th acc c1 c2
+          explain_equal_rec_ cc st c1 c2;
         | _ ->
           assert false
       end
-    | E_lit lit -> lit :: acc
+    | E_lit lit -> Expl_state.add_lit st lit
-    | E_theory (_pr, sub_l) ->
+    | E_theory (t, u, expl_sets, pr) ->
-      (* FIXME: use pr as a subproof. We need to accumulate subproofs too, because
+      let sub_proofs =
-         there is some amount of resolution done inside the congruence closure
+        List.map
-         itself to resolve Horn clauses produced by theories.
+          (fun (t_i,u_i,expls_i) ->
-
+             let lit_i = A.mk_lit_eq cc.tst t_i u_i in
-         maybe we need to store [t=u] where [pr] is the proof of [Gamma |- t=u],
+             (* use a separate call to [explain_expls] for each set *)
-         add [t=u] to the explanation, and use a subproof to resolve
+             let sub = explain_expls cc expls_i in
-         it away using [pr] and add [Gamma] to the mix *)
+             Expl_state.merge st sub;
-      th := true;
+             lit_i, sub.lits)
-      List.fold_left (explain_decompose_expl cc ~th) acc sub_l
+          expl_sets
-    | E_merge (a,b) -> explain_equal_rec_ cc ~th acc a b
+      in
+      let lit_t_u = A.mk_lit_eq cc.tst t u in
+      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 *)
       begin match T_tbl.find cc.tbl a, T_tbl.find cc.tbl b with
-        | a, b -> explain_equal_rec_ cc ~th acc a b
+        | a, b -> explain_equal_rec_ cc st a b
         | exception Not_found ->
           Error.errorf "expl: cannot find node(s) for %a, %a" Term.pp a Term.pp b
       end
     | E_and (a,b) ->
-      let acc = explain_decompose_expl cc ~th acc a in
+      explain_decompose_expl cc st a;
-      explain_decompose_expl cc ~th acc b
+      explain_decompose_expl cc st b
 
-  and explain_equal_rec_ (cc:t) ~th (acc:lit list) (a:node) (b:node) : _ list =
+  and explain_expls cc (es:explanation list) : Expl_state.t =
+    let st = Expl_state.create() in
+    List.iter (explain_decompose_expl cc st) es;
+    st
+
+  and explain_equal_rec_ (cc:t) (st:Expl_state.t) (a:node) (b:node) : unit =
     Log.debugf 5
       (fun k->k "(@[cc.explain_loop.at@ %a@ =?= %a@])" N.pp a N.pp b);
     assert (N.equal (find_ a) (find_ b));
     let ancestor = find_common_ancestor cc a b in
-    let acc = explain_along_path cc ~th acc a ancestor in
+    explain_along_path cc st a ancestor;
-    explain_along_path cc ~th acc b ancestor
+    explain_along_path cc st b ancestor
 
   (* explain why [a = parent_a], where [a -> ... -> target] in the
      proof forest *)
-  and explain_along_path cc ~th acc (a:node) (target:node) : _ list =
+  and explain_along_path cc (st:Expl_state.t) (a:node) (target:node) : unit =
-    let rec aux acc n =
+    let rec aux n =
-      if n == target then acc
+      if n == target then ()
       else (
         match n.n_expl with
         | FL_none -> assert false
         | FL_some {next=next_n; expl=expl} ->
-          let acc = explain_decompose_expl cc ~th acc expl in
+          explain_decompose_expl cc st expl;
           (* now prove [next_n = target] *)
-          aux acc next_n
+          aux next_n
       )
-    in aux acc a
+    in aux a
 
   (* add a term *)
   let [@inline] rec add_term_rec_ cc t : node =
@@ -587,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 =
@@ -664,13 +734,12 @@ module Make (A: CC_ARG)
            C2: lemma [lits |- true=false]  (and resolve on theory proofs)
            C3: r1 C1 C2
         *)
-        let lits = explain_decompose_expl cc ~th [] e_ab in
+        let expl_st = Expl_state.create() in
-        let lits = explain_equal_rec_ cc ~th lits a ra in
+        explain_decompose_expl cc expl_st e_ab;
-        let lits = explain_equal_rec_ cc ~th lits b rb in
+        explain_equal_rec_ cc expl_st a ra;
-        let pr =
+        explain_equal_rec_ cc expl_st b rb;
-          let p_lits = Iter.of_list lits |> Iter.map Lit.neg in
+
-          P.lemma_cc p_lits @@ Actions.proof acts
+        let lits, pr = lits_and_proof_of_expl cc expl_st in
-        in
         raise_conflict_ cc ~th:!th acts (List.rev_map Lit.neg lits) pr
       );
       (* We will merge [r_from] into [r_into].
@@ -763,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 half_expl_and_pr = lazy (
-      let th = ref false in
+      let st = Expl_state.create() in
-      let lits = explain_decompose_expl cc ~th [] e_12 in
+      explain_decompose_expl cc st e_12;
-      th, explain_equal_rec_ cc ~th lits r2 t2
+      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 *)
@@ -784,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 lazy st = half_expl_and_pr in
-               let lits = explain_equal_rec_ cc ~th acc u1 t1 in
+               explain_equal_rec_ cc st u1 t1;
-               let pr =
+               (* assert that [guard /\ ¬lit] is absurd, to propagate [lit] *)
-                 (* make a tautology, not a true guard *)
+               Expl_state.add_lit st (Lit.neg lit);
-                 let p_lits = Iter.cons lit (Iter.of_list lits |> Iter.map Lit.neg) in
+               lits_and_proof_of_expl cc st
-                 P.lemma_cc p_lits @@ Actions.proof acts
-               in
-               lits, pr
              ) in
              fun () -> Lazy.force e
            in
@@ -855,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 st = Expl_state.create() in
-    let lits = explain_decompose_expl cc ~th [] expl in
+    explain_decompose_expl cc st expl;
-    let lits = List.rev_map Lit.neg lits in
+    let lits, pr = lits_and_proof_of_expl cc st in
-    let pr =
+    let c = List.rev_map Lit.neg lits in
-      let p_lits = Iter.of_list lits in
+    let th = st.th_lemmas <> [] in
-      P.lemma_cc p_lits @@ Actions.proof acts
+    raise_conflict_ cc ~th acts c pr
-    in
-    raise_conflict_ cc ~th:!th acts lits pr
 
   let merge cc n1 n2 expl =
     Log.debugf 5
@@ -874,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
+    let st = Expl_state.create() in
-    explain_equal_rec_ cc ~th [] n1 n2
+    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,17 +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. *)
-end
-
 (** Signature for SAT-solver proof emission. *)
 module type SAT_PROOF = sig
   type t
@@ -209,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].
@@ -235,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. *)
@@ -317,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
@@ -351,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
@@ -363,6 +359,9 @@ module type CC_ARG = sig
 
   val cc_view : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) CC_view.t
   (** View the term through the lens of the congruence closure *)
+
+  val mk_lit_eq : ?sign:bool -> T.Term.store -> T.Term.t -> T.Term.t -> Lit.t
+  (** [mk_lit_eq store t u] makes the literal [t=u] *)
 end
 
 (** Main congruence closure signature.
@@ -388,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
@@ -482,17 +481,40 @@ module type CC_S = sig
     val pp : t Fmt.printer
 
     val mk_merge : N.t -> N.t -> t
-    val mk_merge_t : term -> term -> t
-    val mk_lit : lit -> t
-    val mk_list : t list -> t
-    val mk_theory : proof_step -> t list -> t
-    (* FIXME: this should probably take [t, u, proof(Gamma |- t=u), expls],
-       where [expls] is a list of explanation of the equations in [Gamma].
 
-       For example for the lemma [a=b] deduced by injectivity from [Some a=Some b]
+    val mk_merge_t : term -> term -> t
-       in the theory of datatypes,
+    (** Explanation: the terms were explicitly merged *)
-       the arguments would be [a, b, proof(Some a=Some b |- a=b), e0]
+
-       where [e0] is an explanation of [Some a=Some b] *)
+    val mk_lit : lit -> t
+    (** Explanation: we merged [t] and [u] because of literal [t=u],
+        or we merged [t] and [true] because of literal [t],
+        or [t] and [false] because of literal [¬t] *)
+
+    val mk_list : t list -> t
+    (** Conjunction of explanations *)
+
+    val mk_theory :
+      term -> term ->
+      (term * term * t list) list ->
+      proof_step -> t
+    (** [mk_theory t u expl_sets pr] builds a theory explanation for
+        why [|- t=u]. It depends on sub-explanations [expl_sets] which
+        are tuples [ (t_i, u_i, expls_i) ] where [expls_i] are
+        explanations that justify [t_i = u_i] in the current congruence closure.
+
+        The proof [pr] is the theory lemma, of the form
+        [ (t_i = u_i)_i |- t=u ].
+        It is resolved against each [expls_i |- t_i=u_i] obtained from
+        [expl_sets], on pivot [t_i=u_i], to obtain a proof of [Gamma |- t=u]
+        where [Gamma] is a subset of the literals asserted into the congruence
+        closure.
+
+        For example for the lemma [a=b] deduced by injectivity
+        from [Some a=Some b] in the theory of datatypes,
+        the arguments would be
+        [a, b, [Some a, Some b, mk_merge_t (Some a)(Some b)], pr]
+        where [pr] is the injectivity lemma [Some a=Some b |- a=b].
+    *)
   end
 
   type node = N.t

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)
+    | 11L -> Step_proof_res (Step_proof_res.decode dec)
-    | 12L -> Fun_decl (Fun_decl.decode dec)
+    | 12L -> Step_true (Step_true.decode dec)
-    | 13L -> Expr_def (Expr_def.decode dec)
+    | 13L -> Fun_decl (Fun_decl.decode dec)
-    | 14L -> Expr_bool (Expr_bool.decode dec)
+    | 14L -> Expr_def (Expr_def.decode dec)
-    | 15L -> Expr_if (Expr_if.decode dec)
+    | 15L -> Expr_bool (Expr_bool.decode dec)
-    | 16L -> Expr_not (Expr_not.decode dec)
+    | 16L -> Expr_if (Expr_if.decode dec)
-    | 17L -> Expr_isa (Expr_isa.decode dec)
+    | 17L -> Expr_not (Expr_not.decode dec)
-    | 18L -> Expr_eq (Expr_eq.decode dec)
+    | 18L -> Expr_isa (Expr_isa.decode dec)
-    | 19L -> Expr_app (Expr_app.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/quip/Proof.ml

@@ -141,6 +141,18 @@ and composite_step =
       res: clause; (* result of [proof] *)
       proof: t; (* sub-proof *)
     }
+  (** A named step in {!Composite}, with the expected result.
+      This decouples the checking of the sub-proof, from its use in the rest
+      of the proof, as we can use [res] even if checking [proof] failed. *)
+
+  | S_step_anon of {
+      name: string; (* name of step *)
+      proof: t; (* proof *)
+    }
+    (** A named intermediate proof, to be reused in subsequent proofs.
+        Unlike {!S_step_c} we do not specify the expected result
+        so if this fails, any proof downstream will also fail. *)
+
   | S_define_t of term * term (* [const := t] *)
   | S_define_t_name of string * term (* [const := t] *)
 
@@ -156,6 +168,7 @@ let p p ~lhs ~rhs : hres_step = P { p; lhs; rhs }
 let p1 p = P1 p
 
 let stepc ~name res proof : composite_step = S_step_c {proof;name;res}
+let step_anon ~name proof : composite_step = S_step_anon {name;proof}
 let deft c rhs : composite_step = S_define_t (c,rhs)
 let deft_name c rhs : composite_step = S_define_t_name (c,rhs)
 

src/quip/Sidekick_quip.ml

@@ -113,6 +113,8 @@ module Make_printer(Out : OUT) = struct
     match proof_rule with
     | S_step_c {name;res;proof} ->
       l[a"stepc";a name;pp_cl res;pp_rec proof]
+    | S_step_anon {name;proof} ->
+      l[a"step";a name;pp_rec proof]
     | S_define_t (c,rhs) ->
       (* disable sharing for [rhs], otherwise it'd print [c] *)
       l[a"deft";pp_t c; pp_t rhs]

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 =
+      let mk_expl t1 t2 pr =
-        Expl.mk_theory 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 @@
+          let t1 = N.term c1.c_n in
-          A.P.lemma_cstor_inj (N.term c1.c_n) (N.term c2.c_n) i (SI.CC.proof cc)
+          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 @@
+          let t1 = N.term c1.c_n and t2 = N.term c2.c_n in
-          A.P.lemma_cstor_distinct (N.term c1.c_n) (N.term c2.c_n) (SI.CC.proof cc)
+          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)
+          let n_bool = SI.CC.n_bool cc is_true in
-            Expl.(mk_theory pr [mk_merge n_u cstor.c_n])
+          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)
+      let n_bool = SI.CC.n_bool cc is_true in
-        Expl.(mk_theory pr
+      SI.CC.merge cc is_a2.is_a_n n_bool
-                [mk_merge n1 c1.c_n; mk_merge n1 n2;
+        (Expl.mk_theory (N.term is_a2.is_a_n) (N.term n_bool)
-                 mk_merge n2 is_a2.is_a_arg])
+           [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
+          (Expl.mk_theory (N.term sel2.sel_n) (N.term u_i)
-                  [mk_merge n1 c1.c_n; mk_merge n1 n2;
+             [N.term n1, N.term n2,
-                   mk_merge n2 sel2.sel_arg]);
+              [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
+            let subs =
-            |> CCList.flat_map
+              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