From 01a15ef0ed38cabd33ce56f46fc605e28019cb18 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 24 Oct 2022 23:00:06 -0400 Subject: [PATCH] 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 | 51 +++++++++++++++++++++---------- src/cc/CC.mli | 4 ++- src/cc/plugin.ml | 8 +++-- src/th-cstor/Sidekick_th_cstor.ml | 12 ++++++-- src/th-data/Sidekick_th_data.ml | 14 ++++++--- src/th-lra/sidekick_th_lra.ml | 36 +++++++++++++++++----- 6 files changed, 91 insertions(+), 34 deletions(-) diff --git a/src/cc/CC.ml b/src/cc/CC.ml index 577519dd..5c84c813 100644 --- a/src/cc/CC.ml +++ b/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 *) - (* explanation is [a=ra & e_ab & b=rb] *) + (* call [on_pre_merge] functions, and merge theory data items. + 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) -> - raise_conflict_from_expl self expl + | Error (Handler_action.Conflict { t; u; expl; pr }) -> + 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. - Raises E_confl with a result conflict. *) -and raise_conflict_from_expl self (expl : Expl.t) : 'a = +(* raise a conflict from an explanation [expl] which justifies [a=b], + when [a] and [b] cannot be equal. + 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 c = List.rev_map Lit.neg lits in + let lits, pr_c = lits_and_proof_of_expl self st 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 - raise_conflict_ self ~th c pr + let 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) diff --git a/src/cc/CC.mli b/src/cc/CC.mli index 9d1ad0aa..be13b747 100644 --- a/src/cc/CC.mli +++ b/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. diff --git a/src/cc/plugin.ml b/src/cc/plugin.ml index 32cc5547..12cd7e9d 100644 --- a/src/cc/plugin.ml +++ b/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" - E_node.pp n_u M.pp m_u M.pp m_u' Expl.pp expl + "when merging@ @[for node %a@],@ values %a and %a:@ conflict \ + %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 -> diff --git a/src/th-cstor/Sidekick_th_cstor.ml b/src/th-cstor/Sidekick_th_cstor.ml index f9663f38..b7b28baa 100644 --- a/src/th-cstor/Sidekick_th_cstor.ml +++ b/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 diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index fb548bc1..1dfa1316 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/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 t1 t2 @@ fun () -> Proof_rules.lemma_cstor_distinct t1 t2 + mk_expl t u @@ fun () -> Proof_rules.lemma_cstor_distinct t u + 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 diff --git a/src/th-lra/sidekick_th_lra.ml b/src/th-lra/sidekick_th_lra.ml index e76c4115..50cf722a 100644 --- a/src/th-lra/sidekick_th_lra.ml +++ b/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) -> - match as_const_ (E_node.term n1), as_const_ (E_node.term n2) with + SI.on_cc_pre_merge si (fun (cc, n1, n2, expl) -> + 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