fix(CC): give proper explanations to on-merge hook conflicts

the conflict is a clause purely made of negative equalities, but it
comes from a lemma with an additional literal [t=u]. we resolve this
literal away using a theory lemma before triggering the conflict proper.

checking CC lemma must occur on the original clause, not the conflict
itself.

src/cc/CC.ml

@@ -32,7 +32,10 @@ module Handler_action = struct
     | Act_merge of E_node.t * E_node.t * Expl.t
     | Act_propagate of Lit.t * propagation_reason
 
-  type conflict = Conflict of Expl.t [@@unboxed]
+  type conflict =
+    | Conflict of { expl: Expl.t; t: Term.t; u: Term.t; pr: Proof.step_id }
+        (** Conflict: [expl => t=u], where [pr] is a proof of [|- t!=u] *)
+
   type or_conflict = (t list, conflict) result
 end
 
@@ -216,13 +219,15 @@ let[@unroll 2] rec reroot_expl (self : t) (n : e_node) : unit =
 
 exception E_confl of Result_action.conflict
 
-let raise_conflict_ (cc : t) ~th (e : Lit.t list) (p : Sidekick_proof.Step.id) :
+let raise_conflict_ (cc : t) ~th (e : Lit.t list) ~cc_lemma
-    _ =
+    (p : Sidekick_proof.Step.id) : _ =
   Profile.instant "cc.conflict";
   (* clear tasks queue *)
   Vec.clear cc.pending;
   Vec.clear cc.combine;
-  Event.emit cc.on_conflict { cc; th; c = e };
+  (* here we emit the original CC lemma, not the final clause that might
+     have been simplified *)
+  Event.emit cc.on_conflict { cc; th; c = cc_lemma };
   Stat.incr cc.count_conflict;
   Vec.clear cc.res_acts;
   raise (E_confl (Conflict (e, p)))
@@ -617,7 +622,8 @@ and task_merge_ self a b e_ab : unit =
       (* regular conflict *)
       let lits, pr = lits_and_proof_of_expl self expl_st in
       let pr = Proof.Tracer.add_step self.proof pr in
-      raise_conflict_ self ~th:!th (List.rev_map Lit.neg lits) pr
+      let c = List.rev_map Lit.neg lits in
+      raise_conflict_ self ~th:!th c ~cc_lemma:c pr
     );
     (* We will merge [r_from] into [r_into].
        we try to ensure that [size ra <= size rb] in general, but always
@@ -647,14 +653,14 @@ and task_merge_ self a b e_ab : unit =
     Log.debugf 15 (fun k ->
         k "(@[cc.merge@ :from %a@ :into %a@])" E_node.pp r_from E_node.pp r_into);
 
-    (* call [on_pre_merge] functions, and merge theory data items *)
+    (* call [on_pre_merge] functions, and merge theory data items.
-    (* explanation is [a=ra & e_ab & b=rb] *)
+       explanation is [a=ra & e_ab & b=rb] *)
     (let expl = Expl.mk_list [ e_ab; Expl.mk_merge a ra; Expl.mk_merge b rb ] in
 
      let handle_act = function
        | Ok l -> push_action_l self l
-       | Error (Handler_action.Conflict expl) ->
+       | Error (Handler_action.Conflict { t; u; expl; pr }) ->
-         raise_conflict_from_expl self expl
+         raise_conflict_from_expl self t u expl pr
      in
 
      Event.emit_iter self.on_pre_merge
@@ -764,18 +770,31 @@ and propagate_bools self r1 t1 r2 t2 (e_12 : explanation) sign : unit =
         Stat.incr self.count_props
       | _ -> ())
 
-(* raise a conflict from an explanation, typically from an event handler.
+(* raise a conflict from an explanation [expl] which justifies [a=b],
-   Raises E_confl with a result conflict. *)
+   when [a] and [b] cannot be equal.
-and raise_conflict_from_expl self (expl : Expl.t) : 'a =
+   This is typically called from an event handler.
+   @raises E_confl with a result conflict. *)
+and raise_conflict_from_expl self (t : Term.t) (u : Term.t) (expl : Expl.t)
+    (pr_t_neq_u : Proof.step_id) : 'a =
   Log.debugf 5 (fun k ->
       k "(@[cc.theory.raise-conflict@ :expl %a@])" Expl.pp expl);
   let st = Expl_state.create () in
   explain_decompose_expl self st expl;
-  let lits, pr = lits_and_proof_of_expl self st in
+  let lits, pr_c = lits_and_proof_of_expl self st in
-  let c = List.rev_map Lit.neg lits in
+  (* we obtain [c_result] by resolving [t=u] away using the theory lemma
+     which proves [|- t != u] *)
+  let c_result = List.rev_map Lit.neg lits in
+  let cc_lemma = Lit.make_eq ~sign:true self.tst t u :: c_result in
   let th = st.th_lemmas <> [] in
-  let pr = Proof.Tracer.add_step self.proof pr in
+  let pr =
-  raise_conflict_ self ~th c pr
+    (* resolve [expl => t=u] with [pr_t_neq_u] : [|- t != u] *)
+    Proof.Tracer.add_step self.proof @@ fun () ->
+    let pivot = Term.eq self.tst t u in
+    Proof.Core_rules.proof_res ~pivot
+      (Proof.Tracer.add_step self.proof pr_c)
+      pr_t_neq_u
+  in
+  raise_conflict_ self ~th c_result ~cc_lemma pr
 
 let add_iter self it : unit = it (fun t -> ignore @@ add_term_rec_ self t)
 

src/cc/CC.mli

@@ -90,7 +90,9 @@ module Handler_action : sig
      - an action to modify data associated with a class
   *)
 
-  type conflict = Conflict of Expl.t [@@unboxed]
+  type conflict =
+    | Conflict of { expl: Expl.t; t: Term.t; u: Term.t; pr: Proof.step_id }
+        (** Conflict: [expl => t=u], where [pr] is a proof of [|- t!=u] *)
 
   type or_conflict = (t list, conflict) result
   (** Actions or conflict scheduled by an event handler.

src/cc/plugin.ml

@@ -88,10 +88,12 @@ module Make (M : MONOID_PLUGIN_ARG) :
             in
 
             match M.merge cc plugin_st n_u m_u n_u m_u' (Expl.mk_list []) with
-            | Error (CC.Handler_action.Conflict expl) ->
+            | Error (CC.Handler_action.Conflict { t; u; expl; pr = _ }) ->
               Error.errorf
-                "when merging@ @[for node %a@],@ values %a and %a:@ conflict %a"
+                "when merging@ @[for node %a@],@ values %a and %a:@ conflict \
-                E_node.pp n_u M.pp m_u M.pp m_u' Expl.pp expl
+                 %a ==> %a=%a"
+                E_node.pp n_u M.pp m_u M.pp m_u' Expl.pp expl Term.pp t Term.pp
+                u
             | Ok (m_u_merged, merge_acts) ->
               acts := List.rev_append merge_acts !acts;
               Log.debugf 20 (fun k ->

src/th-cstor/Sidekick_th_cstor.ml

@@ -43,7 +43,7 @@ end = struct
         Some { n; t; cstor; args }, []
       | _ -> None, []
 
-    let merge _cc state n1 v1 n2 v2 e_n1_n2 : _ result =
+    let merge cc state n1 v1 n2 v2 e_n1_n2 : _ result =
       Log.debugf 5 (fun k ->
           k "(@[%s.merge@ @[:c1 %a (t %a)@]@ @[:c2 %a (t %a)@]@])" name
             E_node.pp n1 T.pp_debug v1.t E_node.pp n2 T.pp_debug v2.t);
@@ -69,7 +69,15 @@ end = struct
       ) else (
         (* different function: disjointness *)
         Stat.incr state.n_conflict;
-        Error (CC.Handler_action.Conflict expl)
+        let t = E_node.term n1 in
+        let u = E_node.term n2 in
+        let pr =
+          let tst = CC.term_store cc in
+          let proof = CC.proof_tracer cc in
+          Proof.Tracer.add_step proof @@ fun () ->
+          A.lemma_cstor [ Lit.make_eq ~sign:false tst t u ]
+        in
+        Error (CC.Handler_action.Conflict { t; u; expl; pr })
       )
   end
 

src/th-data/Sidekick_th_data.ml

@@ -175,7 +175,7 @@ end = struct
         Some { c_n = n; c_cstor = cstor; c_args = args }, []
       | _ -> None, []
 
-    let merge _cc state n1 c1 n2 c2 e_n1_n2 : _ result =
+    let merge cc state n1 c1 n2 c2 e_n1_n2 : _ result =
       Log.debugf 5 (fun k ->
           k "(@[%s.merge@ (@[:c1 %a@ %a@])@ (@[:c2 %a@ %a@])@])" name E_node.pp
             n1 pp c1 E_node.pp n2 pp c2);
@@ -209,13 +209,19 @@ end = struct
         Ok (c1, !acts)
       ) else (
         (* different function: disjointness *)
+        let t = E_node.term c1.c_n
+        and u = E_node.term c2.c_n in
         let expl =
-          let t1 = E_node.term c1.c_n and t2 = E_node.term c2.c_n in
+          mk_expl t u @@ fun () -> Proof_rules.lemma_cstor_distinct t u
-          mk_expl t1 t2 @@ fun () -> Proof_rules.lemma_cstor_distinct t1 t2
+        in
+        let pr =
+          let proof = CC.proof_tracer cc in
+          Proof.Tracer.add_step proof @@ fun () ->
+          Proof_rules.lemma_cstor_distinct t u
         in
 
         Stat.incr state.n_conflict;
-        Error (CC.Handler_action.Conflict expl)
+        Error (CC.Handler_action.Conflict { t; u; expl; pr })
       )
   end
 

src/th-lra/sidekick_th_lra.ml

@@ -100,25 +100,38 @@ module Make (A : ARG) = (* : S with module A = A *) struct
         Some [ { n; le } ], []
       | LRA_other _ | LRA_pred _ -> None, []
 
-    exception Confl of Expl.t
+    exception Confl of term * term * Expl.t * Proof.step_id
 
     (* merge lists. If two linear expressions equal up to a constant are
        merged, conflict. *)
-    let merge _cc () n1 l1 n2 l2 expl_12 : _ result =
+    let merge cc () n1 l1 n2 l2 expl_12 : _ result =
       try
         let i = Iter.(product (of_list l1) (of_list l2)) in
         i (fun (s1, s2) ->
             let le = LE.(s1.le - s2.le) in
             if LE.is_const le && not (LE.is_zero le) then (
-              (* conflict: [le+c = le + d] is impossible *)
+              (* conflict: [le + c = le + d] is impossible *)
+              let t1 = E_node.term s1.n in
+              let t2 = E_node.term s2.n in
               let expl =
                 let open Expl in
                 mk_list [ mk_merge s1.n n1; mk_merge s2.n n2; expl_12 ]
               in
-              raise (Confl expl)
+              let pr =
+                let tst = CC.term_store cc in
+                Proof.Tracer.add_step (CC.proof_tracer cc) @@ fun () ->
+                Proof_rules.lemma_lra [ Lit.make_eq ~sign:false tst t1 t2 ]
+              in
+
+              Log.debugf 50 (fun k ->
+                  k "(@[lra.on-merge.conflict@ :n1 %a@ :n2 %a@])" E_node.pp n1
+                    E_node.pp n2);
+
+              raise (Confl (t1, t2, expl, pr))
             ));
         Ok (List.rev_append l1 l2, [])
-      with Confl expl -> Error (CC.Handler_action.Conflict expl)
+      with Confl (t, u, expl, pr) ->
+        Error (CC.Handler_action.Conflict { t; u; expl; pr })
   end
 
   module ST_exprs = Sidekick_cc.Plugin.Make (Monoid_exprs)
@@ -720,14 +733,21 @@ module Make (A : ARG) = (* : S with module A = A *) struct
     SI.on_final_check si (final_check_ st);
     (* SI.on_partial_check si (partial_check_ st); *)
     SI.on_model si ~ask:(model_ask_ st) ~complete:(model_complete_ st);
-    SI.on_cc_pre_merge si (fun (_cc, n1, n2, expl) ->
+    SI.on_cc_pre_merge si (fun (cc, n1, n2, expl) ->
-        match as_const_ (E_node.term n1), as_const_ (E_node.term n2) with
+        let t = E_node.term n1 in
+        let u = E_node.term n2 in
+        let tst = CC.term_store cc in
+        match as_const_ t, as_const_ u with
         | Some q1, Some q2 when A.Q.(q1 <> q2) ->
           (* classes with incompatible constants *)
+          let pr =
+            Proof.Tracer.add_step (CC.proof_tracer cc) @@ fun () ->
+            Proof_rules.lemma_lra [ Lit.make_eq ~sign:false tst t u ]
+          in
           Log.debugf 30 (fun k ->
               k "(@[lra.merge-incompatible-consts@ %a@ %a@])" E_node.pp n1
                 E_node.pp n2);
-          Error (CC.Handler_action.Conflict expl)
+          Error (CC.Handler_action.Conflict { t; u; expl; pr })
         | _ -> Ok []);
     st