From: Andrew Reynolds Date: Tue, 9 Jun 2020 21:36:25 +0000 (-0500) Subject: (proof-new) Refactor skolemization (#4586) X-Git-Tag: cvc5-1.0.0~3233 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2a518941922855626c015a73572a5a9a5a2d0ed7;p=cvc5.git (proof-new) Refactor skolemization (#4586) This PR refactors skolemization in SkolemManager so that we use a "curried" form, where witnesses for a variable x is based on the existential where the prefix up to x has already been skolemized. This additionally adds more utility functions that will be used in the internal proof checker for quantifiers. --- diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp index 0570af687..ced58eaf2 100644 --- a/src/expr/skolem_manager.cpp +++ b/src/expr/skolem_manager.cpp @@ -20,6 +20,8 @@ using namespace CVC4::kind; namespace CVC4 { +// Attributes are global maps from Nodes to data. Thus, note that these could +// be implemented as internal maps in SkolemManager. struct WitnessFormAttributeId { }; @@ -50,43 +52,97 @@ Node SkolemManager::mkSkolem(Node v, Node predw = getWitnessForm(pred); // make the witness term, which should not contain any skolem Node w = nm->mkNode(WITNESS, bvl, predw); - // store the mapping to proof generator - d_gens[w] = pg; + // store the mapping to proof generator if it exists + if (pg != nullptr) + { + Node q = nm->mkNode(EXISTS, w[0], w[1]); + // Notice this may overwrite an existing proof generator. This does not + // matter since either should be able to prove q. + d_gens[q] = pg; + } return getOrMakeSkolem(w, prefix, comment, flags); } -Node SkolemManager::mkSkolemExists(Node v, - Node q, - const std::string& prefix, - const std::string& comment, - int flags, - ProofGenerator* pg) +Node SkolemManager::mkSkolemize(Node q, + std::vector& skolems, + const std::string& prefix, + const std::string& comment, + int flags, + ProofGenerator* pg) +{ + Trace("sk-manager-debug") << "mkSkolemize..." << std::endl; + Assert(q.getKind() == EXISTS); + Node currQ = q; + for (const Node& av : q[0]) + { + Assert(currQ.getKind() == EXISTS && av == currQ[0][0]); + // currQ is updated to the result of skolemizing its first variable in + // the method below. + Node sk = skolemize(currQ, currQ, prefix, comment, flags); + Trace("sk-manager-debug") + << "made skolem " << sk << " for " << av << std::endl; + skolems.push_back(sk); + } + if (pg != nullptr) + { + // Same as above, this may overwrite an existing proof generator + d_gens[q] = pg; + } + return currQ; +} + +Node SkolemManager::skolemize(Node q, + Node& qskolem, + const std::string& prefix, + const std::string& comment, + int flags) { Assert(q.getKind() == EXISTS); - bool foundVar = false; + Node v; std::vector ovars; + std::vector ovarsW; + Trace("sk-manager-debug") << "mkSkolemize..." << std::endl; + NodeManager* nm = NodeManager::currentNM(); for (const Node& av : q[0]) { - if (av == v) + if (v.isNull()) { - foundVar = true; + v = av; continue; } + // must make fresh variable to avoid shadowing, which is unique per + // variable av to ensure that this method is deterministic. Having this + // 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); + ovarsW.push_back(avp); ovars.push_back(av); } - if (!foundVar) - { - Assert(false); - return Node::null(); - } + Assert(!v.isNull()); Node pred = q[1]; + qskolem = q[1]; + Trace("sk-manager-debug") << "make exists predicate" << std::endl; if (!ovars.empty()) { - NodeManager* nm = NodeManager::currentNM(); - Node bvl = nm->mkNode(BOUND_VAR_LIST, ovars); + Node bvl = nm->mkNode(BOUND_VAR_LIST, ovarsW); pred = nm->mkNode(EXISTS, bvl, pred); + // skolem form keeps the old variables + bvl = nm->mkNode(BOUND_VAR_LIST, ovars); + qskolem = nm->mkNode(EXISTS, bvl, pred); } - return mkSkolem(v, pred, prefix, comment, flags, pg); + Trace("sk-manager-debug") << "call sub mkSkolem" << std::endl; + // don't use a proof generator, since this may be an intermediate, partially + // skolemized formula. + Node k = mkSkolem(v, pred, prefix, comment, flags, nullptr); + Assert(k.getType() == v.getType()); + TNode tv = v; + TNode tk = k; + Trace("sk-manager-debug") + << "qskolem apply " << tv << " -> " << tk << " to " << pred << std::endl; + qskolem = qskolem.substitute(tv, tk); + Trace("sk-manager-debug") << "qskolem done substitution" << std::endl; + return k; } Node SkolemManager::mkPurifySkolem(Node t, @@ -111,6 +167,16 @@ Node SkolemManager::mkPurifySkolem(Node t, return k; } +Node SkolemManager::mkExistential(Node t, Node p) +{ + 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); @@ -131,8 +197,8 @@ Node SkolemManager::convertInternal(Node n, bool toWitness) { return n; } - Trace("pf-skolem-debug") << "SkolemManager::convertInternal: " << toWitness - << " " << n << std::endl; + Trace("sk-manager-debug") << "SkolemManager::convertInternal: " << toWitness + << " " << n << std::endl; WitnessFormAttribute wfa; SkolemFormAttribute sfa; NodeManager* nm = NodeManager::currentNM(); @@ -217,7 +283,7 @@ Node SkolemManager::convertInternal(Node n, bool toWitness) } while (!visit.empty()); Assert(visited.find(n) != visited.end()); Assert(!visited.find(n)->second.isNull()); - Trace("pf-skolem-debug") << "..return " << visited[n] << std::endl; + Trace("sk-manager-debug") << "..return " << visited[n] << std::endl; return visited[n]; } @@ -256,9 +322,24 @@ Node SkolemManager::getOrMakeSkolem(Node w, k.setAttribute(wfa, w); // set skolem form attribute for w w.setAttribute(sfa, k); - Trace("pf-skolem") << "SkolemManager::mkSkolem: " << k << " : " << w - << std::endl; + Trace("sk-manager") << "SkolemManager::mkSkolem: " << k << " : " << w + << std::endl; return k; } +Node SkolemManager::getOrMakeBoundVariable(Node t, Node s) +{ + std::pair key(t, s); + std::map, Node>::iterator it = + d_witnessBoundVar.find(key); + if (it != d_witnessBoundVar.end()) + { + return it->second; + } + TypeNode tt = t.getType(); + Node v = NodeManager::currentNM()->mkBoundVar(tt); + d_witnessBoundVar[key] = v; + return v; +} + } // namespace CVC4 diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h index eaf74bcce..557947214 100644 --- a/src/expr/skolem_manager.h +++ b/src/expr/skolem_manager.h @@ -84,7 +84,7 @@ class SkolemManager * @param comment Debug information about the Skolem * @param flags The flags for the Skolem (see NodeManager::mkSkolem) * @param pg The proof generator for this skolem. If non-null, this proof - * generator must respond to a call to getProofFor(exists x. pred) during + * generator must respond to a call to getProofFor(exists v. pred) during * the lifetime of the current node manager. * @return The skolem whose witness form is registered by this class. */ @@ -95,20 +95,40 @@ class SkolemManager int flags = NodeManager::SKOLEM_DEFAULT, ProofGenerator* pg = nullptr); /** - * Same as above, but where pred is an existential quantified formula - * whose bound variable list contains v. For example, calling this method on: - * x, (exists ((x Int) (y Int)) (P x y)) - * will return: - * (witness ((x Int)) (exists ((y Int)) (P x y))) - * If the variable v is not in the bound variable list of q, then null is - * returned and an assertion failure is thrown. + * Make skolemized form of existentially quantified formula q, and store its + * Skolems into the argument skolems. + * + * For example, calling this method on: + * (exists ((x Int) (y Int)) (P x y)) + * returns: + * (P w1 w2) + * where w1 and w2 are skolems with witness forms: + * (witness ((x Int)) (exists ((y' Int)) (P x y'))) + * (witness ((y Int)) (P w1 y)) + * respectively. Additionally, this method will add { w1, w2 } to skolems. + * Notice that y is renamed to y' in the witness form of w1 to avoid variable + * shadowing. + * + * In contrast to mkSkolem, the proof generator is for the *entire* + * existentially quantified formula q, which may have multiple variables in + * its prefix. + * + * @param q The existentially quantified formula to skolemize, + * @param skolems Vector to add Skolems of q to, + * @param prefix The prefix of the name of each of the Skolems + * @param comment Debug information about each of the Skolems + * @param flags The flags for the Skolem (see NodeManager::mkSkolem) + * @param pg The proof generator for this skolem. If non-null, this proof + * generator must respond to a call to getProofFor(q) during + * the lifetime of the current node manager. + * @return The skolemized form of q. */ - Node mkSkolemExists(Node v, - Node q, - const std::string& prefix, - const std::string& comment = "", - int flags = NodeManager::SKOLEM_DEFAULT, - ProofGenerator* pg = nullptr); + Node mkSkolemize(Node q, + std::vector& skolems, + const std::string& prefix, + const std::string& comment = "", + int flags = NodeManager::SKOLEM_DEFAULT, + ProofGenerator* pg = nullptr); /** * Same as above, but for special case of (witness ((x T)) (= x t)) * where T is the type of t. This skolem is unique for each t, which we @@ -123,10 +143,16 @@ class SkolemManager const std::string& comment = "", int flags = NodeManager::SKOLEM_DEFAULT); /** - * Get proof generator for witness term t. This returns the proof generator - * that was provided in a call to mkSkolem above. + * 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 t); + 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); /** convert to witness form * * @param n The term or formula to convert to witness form described above @@ -149,6 +175,11 @@ class SkolemManager * Mapping from witness terms to proof generators. */ std::map d_gens; + /** + * Map to canonical bound variables. This is used for example by the method + * mkExistential. + */ + std::map, Node> d_witnessBoundVar; /** Convert to witness or skolem form */ static Node convertInternal(Node n, bool toWitness); /** Get or make skolem attribute for witness term w */ @@ -156,6 +187,29 @@ class SkolemManager const std::string& prefix, const std::string& comment, int flags); + /** + * Skolemize the first variable of existentially quantified formula q. + * For example, calling this method on: + * (exists ((x Int) (y Int)) (P x y)) + * will return: + * (witness ((x Int)) (exists ((y Int)) (P x y))) + * If q is not an existentially quantified formula, then null is + * returned and an assertion failure is thrown. + * + * This method additionally updates qskolem to be the skolemized form of q. + * In the above example, this is set to: + * (exists ((y Int)) (P (witness ((x Int)) (exists ((y' Int)) (P x y'))) y)) + */ + Node skolemize(Node q, + Node& qskolem, + const std::string& prefix, + 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. + */ + Node getOrMakeBoundVariable(Node t, Node s); }; } // namespace CVC4