feat: change signature of explanations for CC theory merges

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,100 @@ module Make (A: CC_ARG)
     cleanup_ b;
     n
 
+  module Expl_state = struct
+    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;
+    }
+
+    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 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;
+             t_i, u_i, 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 t u 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 =
@@ -664,12 +696,27 @@ 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;
+        explain_equal_rec_ cc expl_st b rb;
+        let {Expl_state.lits; th_lemmas} = expl_st in
         let pr =
-          let p_lits = Iter.of_list lits |> Iter.map Lit.neg in
+          let proof = Actions.proof acts in
-          P.lemma_cc p_lits @@ Actions.proof acts
+          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
         raise_conflict_ cc ~th:!th acts (List.rev_map Lit.neg lits) pr
       );

src/core/Sidekick_core.ml

@@ -154,6 +154,11 @@ module type CC_PROOF = sig
   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. *)
@@ -363,6 +368,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.
@@ -482,17 +490,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