diff options
| -rw-r--r-- | src/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | src/prop/prop_engine.cpp | 22 | ||||
| -rw-r--r-- | src/prop/prop_engine.h | 4 | ||||
| -rw-r--r-- | src/prop/skolem_def_manager.cpp | 173 | ||||
| -rw-r--r-- | src/prop/skolem_def_manager.h | 91 | ||||
| -rw-r--r-- | src/prop/theory_proxy.cpp | 33 | ||||
| -rw-r--r-- | src/prop/theory_proxy.h | 12 | ||||
| -rw-r--r-- | src/smt/term_formula_removal.cpp | 122 | ||||
| -rw-r--r-- | src/smt/term_formula_removal.h | 25 |
9 files changed, 319 insertions, 165 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 5ceb44615..54ece796a 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -209,6 +209,8 @@ libcvc4_add_sources( prop/sat_solver_factory.h prop/sat_solver_types.cpp prop/sat_solver_types.h + prop/skolem_def_manager.cpp + prop/skolem_def_manager.h prop/theory_proxy.cpp prop/theory_proxy.h smt/abduction_solver.cpp diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 71b27d8ec..3f53433ae 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -174,17 +174,15 @@ theory::TrustNode PropEngine::removeItes( void PropEngine::notifyPreprocessedAssertions( const std::vector<Node>& assertions) { - // notify the theory engine of preprocessed assertions - d_theoryEngine->notifyPreprocessedAssertions(assertions); - for (const Node& assertion : assertions) - { - d_decisionEngine->addAssertion(assertion); - } + // notify the theory proxy of preprocessed assertions + d_theoryProxy->notifyPreprocessedAssertions(assertions); } void PropEngine::assertFormula(TNode node) { Assert(!d_inCheckSat) << "Sat solver in solve()!"; Debug("prop") << "assertFormula(" << node << ")" << std::endl; + // NOTE: we do not notify the theory proxy here, since we've already + // notified the theory proxy during notifyPreprocessedAssertions assertInternal(node, false, false, true); } @@ -192,7 +190,7 @@ void PropEngine::assertSkolemDefinition(TNode node, TNode skolem) { Assert(!d_inCheckSat) << "Sat solver in solve()!"; Debug("prop") << "assertFormula(" << node << ")" << std::endl; - d_decisionEngine->addSkolemDefinition(node, skolem); + d_theoryProxy->notifyAssertion(node, skolem); assertInternal(node, false, false, true); } @@ -284,13 +282,13 @@ void PropEngine::assertLemmasInternal( if (!trn.isNull()) { // notify the theory proxy of the lemma - d_decisionEngine->addAssertion(trn.getProven()); + d_theoryProxy->notifyAssertion(trn.getProven()); } Assert(ppSkolems.size() == ppLemmas.size()); for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i) { Node lem = ppLemmas[i].getProven(); - d_decisionEngine->addSkolemDefinition(lem, ppSkolems[i]); + d_theoryProxy->notifyAssertion(ppLemmas[i].getProven(), ppSkolems[i]); } } } @@ -465,14 +463,14 @@ Node PropEngine::getPreprocessedTerm(TNode n, // get the preprocessed form of the term Node pn = getPreprocessedTerm(n); // initialize the set of skolems and assertions to process - std::vector<theory::TrustNode> toProcessAsserts; + std::vector<Node> toProcessAsserts; std::vector<Node> toProcess; d_theoryProxy->getSkolems(pn, toProcessAsserts, toProcess); size_t index = 0; // until fixed point is reached while (index < toProcess.size()) { - theory::TrustNode ka = toProcessAsserts[index]; + Node ka = toProcessAsserts[index]; Node k = toProcess[index]; index++; if (std::find(sks.begin(), sks.end(), k) != sks.end()) @@ -481,7 +479,7 @@ Node PropEngine::getPreprocessedTerm(TNode n, continue; } // must preprocess lemmas as well - Node kap = getPreprocessedTerm(ka.getProven()); + Node kap = getPreprocessedTerm(ka); skAsserts.push_back(kap); sks.push_back(k); // get the skolems in the preprocessed form of the lemma ka diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index d0810324a..fe5d94122 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -220,6 +220,10 @@ class PropEngine * another skolem introduced by term formula removal, then calling this * method on (P k1) will include both k1 and k2 in sks, and their definitions * in skAsserts. + * + * Notice that this method is not frequently used. It is used for algorithms + * that explicitly care about knowing which skolems occur in the preprocessed + * form of a term, recursively. */ Node getPreprocessedTerm(TNode n, std::vector<Node>& skAsserts, diff --git a/src/prop/skolem_def_manager.cpp b/src/prop/skolem_def_manager.cpp new file mode 100644 index 000000000..c2a6a8462 --- /dev/null +++ b/src/prop/skolem_def_manager.cpp @@ -0,0 +1,173 @@ +/********************* */ +/*! \file skolem_def_manager.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Skolem definition manager + **/ + +#include "prop/skolem_def_manager.h" + +#include "expr/attribute.h" + +namespace CVC4 { +namespace prop { + +SkolemDefManager::SkolemDefManager(context::Context* context, + context::UserContext* userContext) + : d_skDefs(userContext), d_skActive(context) +{ +} + +SkolemDefManager::~SkolemDefManager() {} + +void SkolemDefManager::notifySkolemDefinition(TNode skolem, Node def) +{ + // Notice that skolem may have kind SKOLEM or BOOLEAN_TERM_VARIABLE + Trace("sk-defs") << "notifySkolemDefinition: " << def << " for " << skolem + << std::endl; + // in very rare cases, a skolem may be generated twice for terms that are + // equivalent up to purification + if (d_skDefs.find(skolem) == d_skDefs.end()) + { + d_skDefs.insert(skolem, def); + } +} + +TNode SkolemDefManager::getDefinitionForSkolem(TNode skolem) const +{ + NodeNodeMap::const_iterator it = d_skDefs.find(skolem); + AlwaysAssert(it != d_skDefs.end()) << "No skolem def for " << skolem; + return it->second; +} + +void SkolemDefManager::notifyAsserted(TNode literal, + std::vector<TNode>& activatedSkolems) +{ + std::unordered_set<Node, NodeHashFunction> skolems; + getSkolems(literal, skolems); + for (const Node& k : skolems) + { + if (d_skActive.find(k) != d_skActive.end()) + { + // already active + continue; + } + d_skActive.insert(k); + // add to the activated list + activatedSkolems.push_back(k); + } +} + +struct HasSkolemTag +{ +}; +struct HasSkolemComputedTag +{ +}; +/** Attribute true for nodes with skolems in them */ +typedef expr::Attribute<HasSkolemTag, bool> HasSkolemAttr; +/** Attribute true for nodes where we have computed the above attribute */ +typedef expr::Attribute<HasSkolemComputedTag, bool> HasSkolemComputedAttr; + +bool SkolemDefManager::hasSkolems(TNode n) const +{ + 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(); + if (cur.getAttribute(HasSkolemComputedAttr())) + { + visit.pop_back(); + // already computed + continue; + } + it = visited.find(cur); + if (it == visited.end()) + { + visited.insert(cur); + if (cur.getNumChildren() == 0) + { + visit.pop_back(); + bool hasSkolem = false; + if (cur.isVar()) + { + hasSkolem = (d_skDefs.find(cur) != d_skDefs.end()); + } + cur.setAttribute(HasSkolemAttr(), hasSkolem); + cur.setAttribute(HasSkolemComputedAttr(), true); + } + else + { + visit.insert(visit.end(), cur.begin(), cur.end()); + } + } + else + { + visit.pop_back(); + bool hasSkolem = false; + for (TNode i : cur) + { + Assert(i.getAttribute(HasSkolemComputedAttr())); + if (i.getAttribute(HasSkolemAttr())) + { + hasSkolem = true; + break; + } + } + cur.setAttribute(HasSkolemAttr(), hasSkolem); + cur.setAttribute(HasSkolemComputedAttr(), true); + } + } while (!visit.empty()); + Assert(n.getAttribute(HasSkolemComputedAttr())); + return n.getAttribute(HasSkolemAttr()); +} + +void SkolemDefManager::getSkolems( + TNode n, std::unordered_set<Node, NodeHashFunction>& skolems) const +{ + 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(); + if (!hasSkolems(cur)) + { + // does not have skolems, continue + continue; + } + it = visited.find(cur); + if (it == visited.end()) + { + visited.insert(cur); + if (cur.isVar()) + { + if (d_skDefs.find(cur) != d_skDefs.end()) + { + skolems.insert(cur); + } + } + else + { + visit.insert(visit.end(), cur.begin(), cur.end()); + } + } + } while (!visit.empty()); +} + +} // namespace prop +} // namespace CVC4 diff --git a/src/prop/skolem_def_manager.h b/src/prop/skolem_def_manager.h new file mode 100644 index 000000000..9bb118356 --- /dev/null +++ b/src/prop/skolem_def_manager.h @@ -0,0 +1,91 @@ +/********************* */ +/*! \file skolem_def_manager.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Skolem definition manager + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__PROP__SKOLEM_DEF_MANAGER_H +#define CVC4__PROP__SKOLEM_DEF_MANAGER_H + +#include <iosfwd> +#include <unordered_set> +#include <vector> + +#include "context/cdhashset.h" +#include "context/cdinsert_hashmap.h" +#include "context/context.h" +#include "expr/node.h" + +namespace CVC4 { +namespace prop { + +/** + * This class manages the mapping between introduced skolems and the lemmas + * that define their behavior. It can be used to manage which lemmas are + * relevant in the current context, e.g. a lemma corresponding to a skolem + * definition for k is relevant when k appears in an asserted literal. + * + * It also has utilities for tracking (in a SAT-context-dependent manner) which + * skolems are "active", e.g. appear in any asserted literal. + */ +class SkolemDefManager +{ + using NodeNodeMap = context::CDInsertHashMap<Node, Node, NodeHashFunction>; + using NodeSet = context::CDHashSet<Node, NodeHashFunction>; + + public: + SkolemDefManager(context::Context* context, + context::UserContext* userContext); + + ~SkolemDefManager(); + + /** + * Notify skolem definition. This is called when a lemma def is added to the + * SAT solver that corresponds to the skolem definition for skolem k. + */ + void notifySkolemDefinition(TNode k, Node def); + /** + * Get skolem definition for k, where k must be a skolem having a definition + * managed by this class. + */ + TNode getDefinitionForSkolem(TNode k) const; + /** + * Notify that the given literal has been asserted. This method adds skolems + * that become "active" as a result of asserting this literal. A skolem + * is active in the SAT context if it appears in an asserted literal. + */ + void notifyAsserted(TNode literal, std::vector<TNode>& activatedSkolems); + + /** + * Get the set of skolems maintained by this class that occur in node n, + * add them to skolems. + * + * @param n The node to traverse + * @param skolems The set where the skolems are added + */ + void getSkolems(TNode n, + std::unordered_set<Node, NodeHashFunction>& skolems) const; + /** Does n have skolems having definitions managed by this class? */ + bool hasSkolems(TNode n) const; + + private: + /** skolems to definitions (user-context dependent) */ + NodeNodeMap d_skDefs; + /** set of active skolems (SAT-context dependent) */ + NodeSet d_skActive; +}; + +} // namespace prop +} // namespace CVC4 + +#endif /* CVC4__PROP__SKOLEM_DEF_MANAGER_H */ diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 5ee472b93..66023cd88 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -42,7 +42,8 @@ TheoryProxy::TheoryProxy(PropEngine* propEngine, d_decisionEngine(decisionEngine), d_theoryEngine(theoryEngine), d_queue(context), - d_tpp(*theoryEngine, userContext, pnm) + d_tpp(*theoryEngine, userContext, pnm), + d_skdm(new SkolemDefManager(context, userContext)) { } @@ -52,6 +53,29 @@ TheoryProxy::~TheoryProxy() { void TheoryProxy::finishInit(CnfStream* cnfStream) { d_cnfStream = cnfStream; } +void TheoryProxy::notifyPreprocessedAssertions( + const std::vector<Node>& assertions) +{ + d_theoryEngine->notifyPreprocessedAssertions(assertions); + for (const Node& assertion : assertions) + { + d_decisionEngine->addAssertion(assertion); + } +} + +void TheoryProxy::notifyAssertion(Node lem, TNode skolem) +{ + if (skolem.isNull()) + { + d_decisionEngine->addAssertion(lem); + } + else + { + d_skdm->notifySkolemDefinition(skolem, lem); + d_decisionEngine->addSkolemDefinition(lem, skolem); + } +} + void TheoryProxy::variableNotify(SatVariable var) { d_theoryEngine->preRegister(getNode(SatLiteral(var))); } @@ -194,16 +218,15 @@ theory::TrustNode TheoryProxy::removeItes( } void TheoryProxy::getSkolems(TNode node, - std::vector<theory::TrustNode>& skAsserts, + std::vector<Node>& skAsserts, std::vector<Node>& sks) { - RemoveTermFormulas& rtf = d_tpp.getRemoveTermFormulas(); std::unordered_set<Node, NodeHashFunction> skolems; - rtf.getSkolems(node, skolems); + d_skdm->getSkolems(node, skolems); for (const Node& k : skolems) { sks.push_back(k); - skAsserts.push_back(rtf.getLemmaForSkolem(k)); + skAsserts.push_back(d_skdm->getDefinitionForSkolem(k)); } } diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 83c64d726..01d98f1b9 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -29,6 +29,7 @@ #include "expr/node.h" #include "prop/registrar.h" #include "prop/sat_solver_types.h" +#include "prop/skolem_def_manager.h" #include "theory/theory.h" #include "theory/theory_preprocessor.h" #include "theory/trust_node.h" @@ -62,6 +63,12 @@ class TheoryProxy : public Registrar /** Finish initialize */ void finishInit(CnfStream* cnfStream); + /** Notify (preprocessed) assertions. */ + void notifyPreprocessedAssertions(const std::vector<Node>& assertions); + + /** Notify a lemma, possibly corresponding to a skolem definition */ + void notifyAssertion(Node lem, TNode skolem = TNode::null()); + void theoryCheck(theory::Theory::Effort effort); void explainPropagation(SatLiteral l, SatClause& explanation); @@ -124,7 +131,7 @@ class TheoryProxy : public Registrar * fixed point is reached. */ void getSkolems(TNode node, - std::vector<theory::TrustNode>& skAsserts, + std::vector<Node>& skAsserts, std::vector<Node>& sks); /** Preregister term */ void preRegister(Node n) override; @@ -153,6 +160,9 @@ class TheoryProxy : public Registrar /** The theory preprocessor */ theory::TheoryPreprocessor d_tpp; + + /** The skolem definition manager */ + std::unique_ptr<SkolemDefManager> d_skdm; }; /* class TheoryProxy */ }/* CVC4::prop namespace */ diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index 6f2f77a14..6202ab80c 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -34,7 +34,6 @@ RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u, ProofNodeManager* pnm) : d_tfCache(u), d_skolem_cache(u), - d_lemmaCache(u), d_pnm(pnm), d_tpg(nullptr), d_lp(nullptr) @@ -503,12 +502,6 @@ Node RemoveTermFormulas::runCurrent(std::pair<Node, uint32_t>& curr, newLem = theory::TrustNode::mkTrustLemma(newAssertion, d_lp.get()); - // store in the lemma cache, if it is not already there. - if (d_lemmaCache.find(skolem) == d_lemmaCache.end()) - { - d_lemmaCache.insert(skolem, newLem); - } - Trace("rtf-proof-debug") << "Checking closed..." << std::endl; newLem.debugCheckClosed("rtf-proof-debug", "RemoveTermFormulas::run:new_assert"); @@ -533,110 +526,6 @@ Node RemoveTermFormulas::getSkolemForNode(Node k) const return Node::null(); } -struct HasSkolemTag -{ -}; -struct HasSkolemComputedTag -{ -}; -/** Attribute true for nodes with skolems in them */ -typedef expr::Attribute<HasSkolemTag, bool> HasSkolemAttr; -/** Attribute true for nodes where we have computed the above attribute */ -typedef expr::Attribute<HasSkolemComputedTag, bool> HasSkolemComputedAttr; - -bool RemoveTermFormulas::hasSkolems(TNode n) const -{ - 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(); - if (cur.getAttribute(HasSkolemComputedAttr())) - { - visit.pop_back(); - // already computed - continue; - } - it = visited.find(cur); - if (it == visited.end()) - { - visited.insert(cur); - if (cur.getNumChildren() == 0) - { - visit.pop_back(); - bool hasSkolem = false; - if (cur.isVar()) - { - hasSkolem = (d_lemmaCache.find(cur) != d_lemmaCache.end()); - } - cur.setAttribute(HasSkolemAttr(), hasSkolem); - cur.setAttribute(HasSkolemComputedAttr(), true); - } - else - { - visit.insert(visit.end(), cur.begin(), cur.end()); - } - } - else - { - visit.pop_back(); - bool hasSkolem = false; - for (TNode i : cur) - { - Assert(i.getAttribute(HasSkolemComputedAttr())); - if (i.getAttribute(HasSkolemAttr())) - { - hasSkolem = true; - break; - } - } - cur.setAttribute(HasSkolemAttr(), hasSkolem); - cur.setAttribute(HasSkolemComputedAttr(), true); - } - } while (!visit.empty()); - Assert(n.getAttribute(HasSkolemComputedAttr())); - return n.getAttribute(HasSkolemAttr()); -} - -void RemoveTermFormulas::getSkolems( - TNode n, std::unordered_set<Node, NodeHashFunction>& skolems) const -{ - 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(); - if (!hasSkolems(cur)) - { - // does not have skolems, continue - continue; - } - it = visited.find(cur); - if (it == visited.end()) - { - visited.insert(cur); - if (cur.isVar()) - { - if (d_lemmaCache.find(cur) != d_lemmaCache.end()) - { - skolems.insert(cur); - } - } - else - { - visit.insert(visit.end(), cur.begin(), cur.end()); - } - } - } while (!visit.empty()); -} - Node RemoveTermFormulas::getAxiomFor(Node n) { NodeManager* nm = NodeManager::currentNM(); @@ -648,17 +537,6 @@ 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 b6abaaa1f..22d5870b7 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -124,26 +124,6 @@ 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. - * - * @param n The node to traverse - * @param skolems The set where the skolems are added - */ - void getSkolems(TNode n, - std::unordered_set<Node, NodeHashFunction>& skolems) const; - /** - * Does n have skolems introduced by this class? - */ - bool hasSkolems(TNode n) 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>, @@ -177,11 +157,6 @@ 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 * |