From 63f50d03faae609a3cc3b1fda7f83dc030f6e6b5 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 29 Dec 2021 15:56:54 -0500 Subject: [PATCH] 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 | 1 + src/base/Proof.ml | 5 + src/base/Proof_dummy.ml | 1 + src/base/Proof_quip.ml | 12 ++ src/cc/Sidekick_cc.ml | 112 +++++++++++------- src/core/Sidekick_core.ml | 43 +++---- src/proof-trace/proof_ser.bare | 8 ++ src/proof-trace/proof_ser.ml | 76 +++++++++--- src/smt-solver/Sidekick_smt_solver.ml | 4 + src/th-bool-static/Sidekick_th_bool_static.ml | 3 +- src/th-data/Sidekick_th_data.ml | 72 ++++++----- 11 files changed, 217 insertions(+), 120 deletions(-) diff --git a/src/base-solver/sidekick_base_solver.ml b/src/base-solver/sidekick_base_solver.ml index 11791794..bc631436 100644 --- a/src/base-solver/sidekick_base_solver.ml +++ b/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 diff --git a/src/base/Proof.ml b/src/base/Proof.ml index 8ff068e6..46ad614b 100644 --- a/src/base/Proof.ml +++ b/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 diff --git a/src/base/Proof_dummy.ml b/src/base/Proof_dummy.ml index ffce3632..dd794cc5 100644 --- a/src/base/Proof_dummy.ml +++ b/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 _ _ = () diff --git a/src/base/Proof_quip.ml b/src/base/Proof_quip.ml index e087c7a5..2a05bc6e 100644 --- a/src/base/Proof_quip.ml +++ b/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 ( diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index cb0be7fd..20635b22 100644 --- a/src/cc/Sidekick_cc.ml +++ b/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 diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 0bd4093f..9e259129 100644 --- a/src/core/Sidekick_core.ml +++ b/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,9 +310,11 @@ module type CC_ACTIONS = sig type proof type proof_step - module P : CC_PROOF with type lit = Lit.t - and type t = proof - and type proof_step = proof_step + 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 (** An action handle. It is used by the congruence closure @@ -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 diff --git a/src/proof-trace/proof_ser.bare b/src/proof-trace/proof_ser.bare index 919f9c12..23d658a7 100644 --- a/src/proof-trace/proof_ser.bare +++ b/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 diff --git a/src/proof-trace/proof_ser.ml b/src/proof-trace/proof_ser.ml index bf9a67db..875b546a 100644 --- a/src/proof-trace/proof_ser.ml +++ b/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 -> diff --git a/src/smt-solver/Sidekick_smt_solver.ml b/src/smt-solver/Sidekick_smt_solver.ml index 727fbcad..597312f4 100644 --- a/src/smt-solver/Sidekick_smt_solver.ml +++ b/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 diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index 7d401aae..60cc5178 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/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; () diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index 228eca5b..aac8d061 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/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 @@ [ - e_n1_n2; - Expl.mk_merge n1 c1.c_n; - Expl.mk_merge n2 c2.c_n; - ] + 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 - (fun (n,node) -> - [ Expl.mk_merge node.cstor_n node.repr; - Expl.mk_merge n node.repr; - ]) - |> Expl.mk_theory pr - in + 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; + ]) + 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