From 912ada0fb5368f3420b455b8bc76e88db164c37c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 18 Oct 2020 18:42:46 -0500 Subject: [PATCH] (proof-new) Witness axiom reconstruction for purification skolems (#5289) This formalizes the proofs of existentials that justify purification variables, e.g. those with witness form witness x. x = t for the term t they purify. This PR generalizes EXISTS_INTRO to do this, and makes some simplifications to SkolemManager. --- src/expr/proof_rule.h | 5 +-- src/expr/skolem_manager.cpp | 25 +++++---------- src/expr/skolem_manager.h | 17 ++++------ src/smt/witness_form.cpp | 40 +++++++++++++++++++++++- src/smt/witness_form.h | 6 ++++ src/theory/quantifiers/proof_checker.cpp | 22 +++++++++++-- 6 files changed, 81 insertions(+), 34 deletions(-) diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 4000d4df7..9c955d067 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -670,10 +670,11 @@ enum class PfRule : uint32_t WITNESS_INTRO, // ======== Exists intro // Children: (P:F[t]) - // Arguments: (t) + // Arguments: ((exists ((x T)) F[x])) // ---------------------------------------- // Conclusion: (exists ((x T)) F[x]) - // where x is a BOUND_VARIABLE unique to the pair F,t. + // This rule verifies that F[x] indeed matches F[t] with a substitution + // over x. EXISTS_INTRO, // ======== Skolemize // Children: (P:(exists ((x1 T1) ... (xn Tn)) F)) diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp index e34813dcd..a3647e84f 100644 --- a/src/expr/skolem_manager.cpp +++ b/src/expr/skolem_manager.cpp @@ -33,6 +33,7 @@ struct SkolemFormAttributeId }; typedef expr::Attribute SkolemFormAttribute; +// Maps terms to their purify skolem variables struct PurifySkolemAttributeId { }; @@ -125,7 +126,7 @@ Node SkolemManager::skolemize(Node q, // method deterministic ensures that the proof checker (e.g. for // quantifiers) is capable of proving the expected value for conclusions // of proof rules, instead of an alpha-equivalent variant of a conclusion. - Node avp = getOrMakeBoundVariable(av, av); + Node avp = getOrMakeBoundVariable(av); ovarsW.push_back(avp); ovars.push_back(av); } @@ -182,19 +183,9 @@ Node SkolemManager::mkBooleanTermVariable(Node t) return mkPurifySkolem(t, "", "", NodeManager::SKOLEM_BOOL_TERM_VAR); } -Node SkolemManager::mkExistential(Node t, Node p) +ProofGenerator* SkolemManager::getProofGenerator(Node t) const { - Assert(p.getType().isBoolean()); - NodeManager* nm = NodeManager::currentNM(); - Node v = getOrMakeBoundVariable(t, p); - Node bvl = nm->mkNode(BOUND_VAR_LIST, v); - Node psubs = p.substitute(TNode(t), TNode(v)); - return nm->mkNode(EXISTS, bvl, psubs); -} - -ProofGenerator* SkolemManager::getProofGenerator(Node t) -{ - std::map::iterator it = d_gens.find(t); + std::map::const_iterator it = d_gens.find(t); if (it != d_gens.end()) { return it->second; @@ -353,18 +344,16 @@ Node SkolemManager::getOrMakeSkolem(Node w, return k; } -Node SkolemManager::getOrMakeBoundVariable(Node t, Node s) +Node SkolemManager::getOrMakeBoundVariable(Node t) { - std::pair key(t, s); - std::map, Node>::iterator it = - d_witnessBoundVar.find(key); + std::map::iterator it = d_witnessBoundVar.find(t); if (it != d_witnessBoundVar.end()) { return it->second; } TypeNode tt = t.getType(); Node v = NodeManager::currentNM()->mkBoundVar(tt); - d_witnessBoundVar[key] = v; + d_witnessBoundVar[t] = v; return v; } diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h index ec5189d6d..537c0b1e9 100644 --- a/src/expr/skolem_manager.h +++ b/src/expr/skolem_manager.h @@ -159,13 +159,7 @@ class SkolemManager * Get proof generator for existentially quantified formula q. This returns * the proof generator that was provided in a call to mkSkolem above. */ - ProofGenerator* getProofGenerator(Node q); - /** - * Make existential. Given t and p[t] where p is a formula, this returns - * (exists ((x T)) p[x]) - * where T is the type of t, and x is a variable unique to t,p. - */ - Node mkExistential(Node t, Node p); + ProofGenerator* getProofGenerator(Node q) const; /** * Convert to witness form, where notice this recursively replaces *all* * skolems in n by their corresponding witness term. This is intended to be @@ -197,7 +191,7 @@ class SkolemManager * Map to canonical bound variables. This is used for example by the method * mkExistential. */ - std::map, Node> d_witnessBoundVar; + std::map d_witnessBoundVar; /** Convert to witness or skolem form */ static Node convertInternal(Node n, bool toWitness); /** Get or make skolem attribute for witness term w */ @@ -224,10 +218,11 @@ class SkolemManager const std::string& comment = "", int flags = NodeManager::SKOLEM_DEFAULT); /** - * Get or make bound variable unique to (s,t), for d_witnessBoundVar, where - * t and s are terms. + * Get or make bound variable unique to t whose type is the same as t. This + * is used to construct canonical bound variables e.g. for constructing + * bound variables for witness terms in the skolemize method above. */ - Node getOrMakeBoundVariable(Node t, Node s); + Node getOrMakeBoundVariable(Node t); }; } // namespace CVC4 diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp index e8d4f7356..e4f0a56dc 100644 --- a/src/smt/witness_form.cpp +++ b/src/smt/witness_form.cpp @@ -28,7 +28,8 @@ WitnessFormGenerator::WitnessFormGenerator(ProofNodeManager* pnm) "WfGenerator::TConvProofGenerator", nullptr, true), - d_wintroPf(pnm, nullptr, nullptr, "WfGenerator::LazyCDProof") + d_wintroPf(pnm, nullptr, nullptr, "WfGenerator::LazyCDProof"), + d_pskPf(pnm, nullptr, "WfGenerator::PurifySkolemProof") { } @@ -92,6 +93,20 @@ Node WitnessFormGenerator::convertToWitnessForm(Node t) Node skBody = SkolemManager::getSkolemForm(curw[1]); Node exists = nm->mkNode(kind::EXISTS, curw[0], skBody); ProofGenerator* pg = skm->getProofGenerator(exists); + if (pg == nullptr) + { + // it may be a purification skolem + pg = convertExistsInternal(exists); + if (pg == nullptr) + { + // if no proof generator is provided, we justify the existential + // using the WITNESS_AXIOM trusted rule by providing it to the + // call to addLazyStep below. + Trace("witness-form") + << "WitnessFormGenerator: No proof generator for " << exists + << std::endl; + } + } // --------------------------- from pg // (exists ((x T)) (P x)) // --------------------------- WITNESS_INTRO @@ -141,5 +156,28 @@ WitnessFormGenerator::getWitnessFormEqs() const return d_eqs; } +ProofGenerator* WitnessFormGenerator::convertExistsInternal(Node exists) +{ + Assert(exists.getKind() == kind::EXISTS); + if (exists[0].getNumChildren() == 1 && exists[1].getKind() == kind::EQUAL + && exists[1][0] == exists[0][0]) + { + Node tpurified = exists[1][1]; + Trace("witness-form") << "convertExistsInternal: infer purification " + << exists << " for " << tpurified << std::endl; + // ------ REFL + // t = t + // ---------------- EXISTS_INTRO + // exists x. x = t + // The concluded existential is then used to construct the witness term + // via witness intro. + Node teq = tpurified.eqNode(tpurified); + d_pskPf.addStep(teq, PfRule::REFL, {}, {tpurified}); + d_pskPf.addStep(exists, PfRule::EXISTS_INTRO, {teq}, {exists}); + return &d_pskPf; + } + return nullptr; +} + } // namespace smt } // namespace CVC4 diff --git a/src/smt/witness_form.h b/src/smt/witness_form.h index 50c913ae9..eb0cf3005 100644 --- a/src/smt/witness_form.h +++ b/src/smt/witness_form.h @@ -81,6 +81,10 @@ class WitnessFormGenerator : public ProofGenerator * of this class (d_tcpg). */ Node convertToWitnessForm(Node t); + /** + * Return a proof generator that can prove the given axiom exists. + */ + ProofGenerator* convertExistsInternal(Node exists); /** The term conversion proof generator */ TConvProofGenerator d_tcpg; /** The nodes we have already added rewrite steps for in d_tcpg */ @@ -89,6 +93,8 @@ class WitnessFormGenerator : public ProofGenerator std::unordered_set d_eqs; /** Lazy proof storing witness intro steps */ LazyCDProof d_wintroPf; + /** CDProof for justifying purification existentials */ + CDProof d_pskPf; }; } // namespace smt diff --git a/src/theory/quantifiers/proof_checker.cpp b/src/theory/quantifiers/proof_checker.cpp index e2a416120..8371492b5 100644 --- a/src/theory/quantifiers/proof_checker.cpp +++ b/src/theory/quantifiers/proof_checker.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/proof_checker.h" +#include "expr/node_algorithm.h" #include "expr/skolem_manager.h" #include "theory/builtin/proof_checker.h" @@ -43,8 +44,25 @@ Node QuantifiersProofRuleChecker::checkInternal( Assert(children.size() == 1); Assert(args.size() == 1); Node p = children[0]; - Node t = args[0]; - return sm->mkExistential(t, p); + Node exists = args[0]; + if (exists.getKind() != kind::EXISTS || exists[0].getNumChildren() != 1) + { + return Node::null(); + } + std::unordered_map subs; + if (!expr::match(exists[1], p, subs)) + { + return Node::null(); + } + // substitution must contain only the variable of the existential + for (const std::pair& s : subs) + { + if (s.first != exists[0][0]) + { + return Node::null(); + } + } + return exists; } else if (id == PfRule::WITNESS_INTRO) { -- 2.30.2