diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-09 16:36:25 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-09 16:36:25 -0500 |
commit | 2a518941922855626c015a73572a5a9a5a2d0ed7 (patch) | |
tree | fda12a6d12ebb8e8896fa2301543013f0d1e09c7 /src/expr/skolem_manager.cpp | |
parent | c118e34b040eddffe0e2155645b47c811188c82a (diff) |
(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.
Diffstat (limited to 'src/expr/skolem_manager.cpp')
-rw-r--r-- | src/expr/skolem_manager.cpp | 129 |
1 files changed, 105 insertions, 24 deletions
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<Node>& 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<Node> ovars; + std::vector<Node> 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<Node, ProofGenerator*>::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<Node, Node> key(t, s); + std::map<std::pair<Node, Node>, 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 |