diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-05 19:40:12 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-01-05 19:40:12 -0600 |
commit | c32c2c5f5203fff6d4982755e3784f6f2f315b3b (patch) | |
tree | effbd75543b4004c4080814a2e8e435243f67c82 /src/smt | |
parent | 2d2ee68b75d1fd3ea0d523b44815d2dc63529e54 (diff) |
Add new interfaces to term formula removal and theory preprocess (#5717)
This is in preparation for lazy lemmas for term formula removal.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/term_formula_removal.cpp | 80 | ||||
-rw-r--r-- | src/smt/term_formula_removal.h | 33 |
2 files changed, 106 insertions, 7 deletions
diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index ae3039ffa..42166d074 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -28,7 +28,12 @@ namespace CVC4 { RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u, ProofNodeManager* pnm) - : d_tfCache(u), d_skolem_cache(u), d_pnm(pnm), d_tpg(nullptr), d_lp(nullptr) + : d_tfCache(u), + d_skolem_cache(u), + d_lemmaCache(u), + d_pnm(pnm), + d_tpg(nullptr), + d_lp(nullptr) { // enable proofs if necessary if (d_pnm != nullptr) @@ -48,7 +53,7 @@ RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u, RemoveTermFormulas::~RemoveTermFormulas() {} theory::TrustNode RemoveTermFormulas::run( - Node assertion, + TNode assertion, std::vector<theory::TrustNode>& newAsserts, std::vector<Node>& newSkolems, bool fixedPoint) @@ -81,6 +86,13 @@ theory::TrustNode RemoveTermFormulas::run( return theory::TrustNode::mkTrustRewrite(assertion, itesRemoved, d_tpg.get()); } +theory::TrustNode RemoveTermFormulas::run(TNode assertion) +{ + std::vector<theory::TrustNode> newAsserts; + std::vector<Node> newSkolems; + return run(assertion, newAsserts, newSkolems, false); +} + theory::TrustNode RemoveTermFormulas::runLemma( theory::TrustNode lem, std::vector<theory::TrustNode>& newAsserts, @@ -121,7 +133,7 @@ theory::TrustNode RemoveTermFormulas::runLemma( return theory::TrustNode::mkTrustLemma(newAssertion, d_lp.get()); } -Node RemoveTermFormulas::runInternal(Node assertion, +Node RemoveTermFormulas::runInternal(TNode assertion, std::vector<theory::TrustNode>& output, std::vector<Node>& newSkolems) { @@ -481,6 +493,9 @@ Node RemoveTermFormulas::runCurrent(std::pair<Node, uint32_t>& curr, newLem = theory::TrustNode::mkTrustLemma(newAssertion, d_lp.get()); + // store in the lemma cache + d_lemmaCache.insert(skolem, newLem); + Trace("rtf-proof-debug") << "Checking closed..." << std::endl; newLem.debugCheckClosed("rtf-proof-debug", "RemoveTermFormulas::run:new_assert"); @@ -494,10 +509,10 @@ Node RemoveTermFormulas::runCurrent(std::pair<Node, uint32_t>& curr, return Node::null(); } -Node RemoveTermFormulas::getSkolemForNode(Node node) const +Node RemoveTermFormulas::getSkolemForNode(Node k) const { context::CDInsertHashMap<Node, Node, NodeHashFunction>::const_iterator itk = - d_skolem_cache.find(node); + d_skolem_cache.find(k); if (itk != d_skolem_cache.end()) { return itk->second; @@ -505,6 +520,50 @@ Node RemoveTermFormulas::getSkolemForNode(Node node) const return Node::null(); } +bool RemoveTermFormulas::getSkolems( + TNode n, std::unordered_set<Node, NodeHashFunction>& skolems) const +{ + // if n was unchanged by term formula removal, just return immediately + std::pair<Node, uint32_t> initial(n, d_rtfc.initialValue()); + TermFormulaCache::const_iterator itc = d_tfCache.find(initial); + if (itc != d_tfCache.end()) + { + if (itc->second == n) + { + return false; + } + } + // otherwise, traverse it + bool ret = false; + std::unordered_set<TNode, TNodeHashFunction> visited; + std::unordered_set<TNode, TNodeHashFunction>::iterator it; + std::vector<TNode> visit; + TNode cur; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + it = visited.find(cur); + if (it == visited.end()) + { + visited.insert(cur); + if (cur.isVar()) + { + if (d_lemmaCache.find(cur) != d_lemmaCache.end()) + { + // technically could already be in skolems if skolems was non-empty, + // regardless set return value to true. + skolems.insert(cur); + ret = true; + } + } + visit.insert(visit.end(), cur.begin(), cur.end()); + } + } while (!visit.empty()); + return ret; +} + Node RemoveTermFormulas::getAxiomFor(Node n) { NodeManager* nm = NodeManager::currentNM(); @@ -516,6 +575,17 @@ Node RemoveTermFormulas::getAxiomFor(Node n) return Node::null(); } +theory::TrustNode RemoveTermFormulas::getLemmaForSkolem(TNode n) const +{ + context::CDInsertHashMap<Node, theory::TrustNode, NodeHashFunction>:: + const_iterator it = d_lemmaCache.find(n); + if (it == d_lemmaCache.end()) + { + return theory::TrustNode::null(); + } + return (*it).second; +} + ProofGenerator* RemoveTermFormulas::getTConvProofGenerator() { return d_tpg.get(); diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index e5453254c..ac2644182 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -91,11 +91,17 @@ class RemoveTermFormulas { * right hand side is assertion after removing term formulas, and the proof * generator (if provided) that can prove the equivalence. */ - theory::TrustNode run(Node assertion, + theory::TrustNode run(TNode assertion, std::vector<theory::TrustNode>& newAsserts, std::vector<Node>& newSkolems, bool fixedPoint = false); /** + * Same as above, but does not track lemmas, and does not run to fixed point. + * The relevant lemmas can be extracted by the caller later using getSkolems + * and getLemmaForSkolem. + */ + theory::TrustNode run(TNode assertion); + /** * Same as above, but transforms a lemma, returning a LEMMA trust node that * proves the same formula as lem with term formulas removed. */ @@ -120,6 +126,24 @@ class RemoveTermFormulas { */ static Node getAxiomFor(Node n); + /** + * Get the set of skolems introduced by this class that occur in node n, + * add them to skolems. + * + * This method uses an optimization that returns false immediately if n + * was unchanged by term formula removal, based on the initial context. + * + * Return true if any nodes were added to skolems. + */ + bool getSkolems(TNode n, + std::unordered_set<Node, NodeHashFunction>& skolems) const; + + /** + * Get the lemma for the skolem, or the null node if k is not a skolem this + * class introduced. + */ + theory::TrustNode getLemmaForSkolem(TNode k) const; + private: typedef context::CDInsertHashMap< std::pair<Node, uint32_t>, @@ -153,6 +177,11 @@ class RemoveTermFormulas { * d_tfCache[<ite( G, a, b ),0>] = d_tfCache[<ite( G, a, b ),1>] = k. */ context::CDInsertHashMap<Node, Node, NodeHashFunction> d_skolem_cache; + /** + * Mapping from skolems to their corresponding lemma. + */ + context::CDInsertHashMap<Node, theory::TrustNode, NodeHashFunction> + d_lemmaCache; /** gets the skolem for node * @@ -186,7 +215,7 @@ class RemoveTermFormulas { * This uses a term-context-sensitive stack to process assertion. It returns * the version of assertion with all term formulas removed. */ - Node runInternal(Node assertion, + Node runInternal(TNode assertion, std::vector<theory::TrustNode>& newAsserts, std::vector<Node>& newSkolems); /** |