From 80cb096e8a6bee26b47f4c72be5456c7cb78e2f1 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 28 Dec 2021 23:07:10 -0500 Subject: [PATCH 1/3] feat: change signature of explanations for CC theory merges --- src/cc/Sidekick_cc.ml | 129 ++++++++++++++++++++++++++------------ src/core/Sidekick_core.ml | 51 ++++++++++++--- 2 files changed, 129 insertions(+), 51 deletions(-) diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index a3d761b4..cb0be7fd 100644 --- a/src/cc/Sidekick_cc.ml +++ b/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 "(@[merge@ @[:n1 %a@]@ @[:n2 %a@]@])" Term.pp a Term.pp b - | E_theory (_p,es) -> Fmt.fprintf out "(@[th@ %a@])" (Util.pp_list pp) es + | E_merge_t (a,b) -> + Fmt.fprintf out "(@[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 "(@[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 ~th acc a1 a2 + explain_equal_rec_ cc st f1 f2; + 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 - let acc = explain_equal_rec_ cc ~th acc b1 b2 in - explain_equal_rec_ cc ~th acc c1 c2 + explain_equal_rec_ cc st a1 a2; + explain_equal_rec_ cc st b1 b2; + explain_equal_rec_ cc st c1 c2; | _ -> assert false end - | E_lit lit -> lit :: acc - | E_theory (_pr, sub_l) -> - (* FIXME: use pr as a subproof. We need to accumulate subproofs too, because - there is some amount of resolution done inside the congruence closure - itself to resolve Horn clauses produced by theories. - - maybe we need to store [t=u] where [pr] is the proof of [Gamma |- t=u], - add [t=u] to the explanation, and use a subproof to resolve - it away using [pr] and add [Gamma] to the mix *) - th := true; - List.fold_left (explain_decompose_expl cc ~th) acc sub_l - | E_merge (a,b) -> explain_equal_rec_ cc ~th acc a b + | E_lit lit -> Expl_state.add_lit st lit + | E_theory (t, u, expl_sets, pr) -> + let sub_proofs = + List.map + (fun (t_i,u_i,expls_i) -> + let lit_i = A.mk_lit_eq cc.tst t_i u_i in + (* 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) + 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 + | 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 ~th acc b + explain_decompose_expl cc st a; + 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 ~th acc b ancestor + explain_along_path cc st a 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 = - let rec aux acc n = - if n == target then acc + and explain_along_path cc (st:Expl_state.t) (a:node) (target:node) : unit = + let rec aux n = + 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 lits = explain_equal_rec_ cc ~th lits a ra in - let lits = explain_equal_rec_ cc ~th lits b rb in + let expl_st = Expl_state.create() in + 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 p_lits = Iter.of_list lits |> Iter.map Lit.neg in - P.lemma_cc p_lits @@ Actions.proof acts + 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 raise_conflict_ cc ~th:!th acts (List.rev_map Lit.neg lits) pr ); diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index e6b42b33..0bd4093f 100644 --- a/src/core/Sidekick_core.ml +++ b/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] - in the theory of datatypes, - 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_merge_t : term -> term -> t + (** Explanation: the terms were explicitly merged *) + + 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 From 63f50d03faae609a3cc3b1fda7f83dc030f6e6b5 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 29 Dec 2021 15:56:54 -0500 Subject: [PATCH 2/3] 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 From b6df2cd974d0b85a848a6baa994a7298fd1d8da5 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 3 Jan 2022 22:59:31 -0500 Subject: [PATCH 3/3] clause-less steps in proofs these steps are checked only once, to accelerate checking, but the result isn't known. --- src/base/Proof_quip.ml | 9 ++++++--- src/quip/Proof.ml | 13 +++++++++++++ src/quip/Sidekick_quip.ml | 2 ++ 3 files changed, 21 insertions(+), 3 deletions(-) diff --git a/src/base/Proof_quip.ml b/src/base/Proof_quip.ml index 2a05bc6e..bb542800 100644 --- a/src/base/Proof_quip.ml +++ b/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) …))`. @@ -272,12 +273,14 @@ end = struct 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 p = lazy ( + let step = lazy ( let exprs = Util.array_to_list_map L_terms.find exprs in - P.bool_c rule exprs + P.step_anon ~name @@ P.bool_c rule exprs ) in - L_proofs.add lid p; + 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 diff --git a/src/quip/Proof.ml b/src/quip/Proof.ml index 0a1b2322..3211adb6 100644 --- a/src/quip/Proof.ml +++ b/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) diff --git a/src/quip/Sidekick_quip.ml b/src/quip/Sidekick_quip.ml index f996ecb5..70d8bd10 100644 --- a/src/quip/Sidekick_quip.ml +++ b/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]