diff options
Diffstat (limited to 'src')
32 files changed, 1195 insertions, 1187 deletions
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index fe1e31a7b..973163d62 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -127,6 +127,12 @@ ${theory_enum} THEORY_LAST }; +const TheoryId THEORY_FIRST = static_cast<TheoryId>(0); + +inline TheoryId& operator ++ (TheoryId& id) { + return id = static_cast<TheoryId>(((int)id) + 1); +} + inline std::ostream& operator<<(std::ostream& out, TheoryId theoryId) { switch(theoryId) { ${theory_descriptions} diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index e160e1ef5..770433489 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -665,12 +665,10 @@ CRef Solver::propagate(TheoryCheckType type) void Solver::propagateTheory() { std::vector<Lit> propagatedLiterals; proxy->theoryPropagate(propagatedLiterals); - const unsigned i_end = propagatedLiterals.size(); - for (unsigned i = 0; i < i_end; ++ i) { + for (unsigned i = 0, i_end = propagatedLiterals.size(); i < i_end; ++ i) { Debug("minisat") << "Theory propagated: " << propagatedLiterals[i] << std::endl; uncheckedEnqueue(propagatedLiterals[i], CRef_Lazy); } - proxy->clearPropagatedLiterals(); } /*_________________________________________________________________________________________________ diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp index 8bda0fd1e..386fb5aad 100644 --- a/src/prop/sat.cpp +++ b/src/prop/sat.cpp @@ -36,16 +36,12 @@ void SatSolver::theoryCheck(theory::Theory::Effort effort) { } void SatSolver::theoryPropagate(std::vector<SatLiteral>& output) { - // Propagate - d_theoryEngine->propagate(); // Get the propagated literals - const std::vector<TNode>& outputNodes = d_theoryEngine->getPropagatedLiterals(); - // If any literals, make a clause - const unsigned i_end = outputNodes.size(); - for (unsigned i = 0; i < i_end; ++ i) { + std::vector<TNode> outputNodes; + d_theoryEngine->getPropagatedLiterals(outputNodes); + for (unsigned i = 0, i_end = outputNodes.size(); i < i_end; ++ i) { Debug("prop-explain") << "theoryPropagate() => " << outputNodes[i].toString() << std::endl; - SatLiteral l = d_cnfStream->getLiteral(outputNodes[i]); - output.push_back(l); + output.push_back(d_cnfStream->getLiteral(outputNodes[i])); } } @@ -67,10 +63,6 @@ void SatSolver::explainPropagation(SatLiteral l, SatClause& explanation) { } } -void SatSolver::clearPropagatedLiterals() { - d_theoryEngine->clearPropagatedLiterals(); -} - void SatSolver::enqueueTheoryLiteral(const SatLiteral& l) { Node literalNode = d_cnfStream->getNode(l); Debug("prop") << "enqueueing theory literal " << l << " " << literalNode << std::endl; diff --git a/src/prop/sat.h b/src/prop/sat.h index 39977a96b..ee3978555 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -226,8 +226,6 @@ public: void theoryPropagate(std::vector<SatLiteral>& output); - void clearPropagatedLiterals(); - void enqueueTheoryLiteral(const SatLiteral& l); void setCnfStream(CnfStream* cnfStream); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3f1111879..d11130aac 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -191,13 +191,13 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : d_theoryEngine = new TheoryEngine(d_context); // Add the theories - d_theoryEngine->addTheory<theory::builtin::TheoryBuiltin>(); - d_theoryEngine->addTheory<theory::booleans::TheoryBool>(); - d_theoryEngine->addTheory<theory::arith::TheoryArith>(); - d_theoryEngine->addTheory<theory::arrays::TheoryArrays>(); - d_theoryEngine->addTheory<theory::bv::TheoryBV>(); - d_theoryEngine->addTheory<theory::datatypes::TheoryDatatypes>(); - d_theoryEngine->addTheory<theory::uf::TheoryUF>(); + d_theoryEngine->addTheory<theory::builtin::TheoryBuiltin>(theory::THEORY_BUILTIN); + d_theoryEngine->addTheory<theory::booleans::TheoryBool>(theory::THEORY_BOOL); + d_theoryEngine->addTheory<theory::arith::TheoryArith>(theory::THEORY_ARITH); + d_theoryEngine->addTheory<theory::arrays::TheoryArrays>(theory::THEORY_ARRAY); + d_theoryEngine->addTheory<theory::bv::TheoryBV>(theory::THEORY_BV); + d_theoryEngine->addTheory<theory::datatypes::TheoryDatatypes>(theory::THEORY_DATATYPES); + d_theoryEngine->addTheory<theory::uf::TheoryUF>(theory::THEORY_UF); d_propEngine = new PropEngine(d_theoryEngine, d_context); d_theoryEngine->setPropEngine(d_propEngine); diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index 9e31bd7a3..6e8734b4d 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -15,10 +15,6 @@ libtheory_la_SOURCES = \ theory_test_utils.h \ theory.h \ theory.cpp \ - shared_term_manager.h \ - shared_term_manager.cpp \ - shared_data.h \ - shared_data.cpp \ registrar.h \ rewriter.h \ rewriter_attributes.h \ @@ -26,7 +22,11 @@ libtheory_la_SOURCES = \ substitutions.h \ substitutions.cpp \ valuation.h \ - valuation.cpp + valuation.cpp \ + shared_terms_database.h \ + shared_terms_database.cpp \ + term_registration_visitor.h \ + term_registration_visitor.cpp nodist_libtheory_la_SOURCES = \ rewriter_tables.h \ diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 4369c6de0..1b13b9ee6 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -786,12 +786,10 @@ void TheoryArith::debugPrintModel(){ } } -void TheoryArith::explain(TNode n) { +Node TheoryArith::explain(TNode n) { Debug("explain") << "explain @" << getContext()->getLevel() << ": " << n << endl; - Assert(d_propManager.isPropagated(n)); - Node explanation = d_propManager.explain(n); - d_out->explanation(explanation, true); + return d_propManager.explain(n); } void TheoryArith::propagate(Effort e) { diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 2e85659e4..6bcf6a613 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -173,7 +173,7 @@ public: void check(Effort e); void propagate(Effort e); - void explain(TNode n); + Node explain(TNode n); void notifyEq(TNode lhs, TNode rhs); diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 6985aaea8..0aff30d74 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -118,7 +118,7 @@ void TheoryArrays::check(Effort e) { // which can lead to a conflict Node conflict = constructConflict(d_conflict); d_conflict = Node::null(); - d_out->conflict(conflict, false); + d_out->conflict(conflict); return; } merge(assertion[0], assertion[1]); @@ -139,13 +139,13 @@ void TheoryArrays::check(Effort e) { // after addTerm since we weren't watching a or b before Node conflict = constructConflict(d_conflict); d_conflict = Node::null(); - d_out->conflict(conflict, false); + d_out->conflict(conflict); return; } else if(find(a) == find(b)) { Node conflict = constructConflict(assertion[0]); d_conflict = Node::null(); - d_out->conflict(conflict, false); + d_out->conflict(conflict); return; } Assert(!d_cc.areCongruent(a,b)); @@ -764,7 +764,7 @@ bool TheoryArrays::isRedundantInContext(TNode a, TNode b, TNode i, TNode j) { nb << literal1.notNode() << literal2.notNode(); literal1 = nb; d_conflict = Node::null(); - d_out->conflict(literal1, false); + d_out->conflict(literal1); Trace("arrays") << "TheoryArrays::isRedundantInContext() " << "conflict via lemma: " << literal1 << endl; return true; @@ -870,7 +870,7 @@ bool TheoryArrays::propagateFromRow(TNode a, TNode b, TNode i, TNode j) { return false; } -void TheoryArrays::explain(TNode n) { +Node TheoryArrays::explain(TNode n) { Trace("arrays")<<"Arrays::explain start for "<<n<<"\n"; @@ -901,7 +901,7 @@ void TheoryArrays::explain(TNode n) { } Node reason = nb; - d_out->explanation(reason); + return reason; /* context::CDMap<TNode, std::pair<TNode, TNode>, TNodeHashFunction>::const_iterator diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 37fffd2ec..a984cb342 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -476,7 +476,7 @@ public: */ } - void explain(TNode n); + Node explain(TNode n); Node getValue(TNode n); SolveStatus solve(TNode in, SubstitutionMap& outSubstitutions); diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index c1fa692b9..c977435ec 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -224,7 +224,7 @@ Node TheoryBV::getValue(TNode n) { } } -void TheoryBV::explain(TNode node) { +Node TheoryBV::explain(TNode node) { BVDebug("bitvector") << "TheoryBV::explain(" << node << ")" << std::endl; TNode equality = node.getKind() == kind::NOT ? node[0] : node; @@ -237,6 +237,5 @@ void TheoryBV::explain(TNode node) { BVDebug("bitvector") << " assumptions " << utils::setToString(d_normalization[equality]->assumptions[i]) << std::endl; assumptions.insert(vec[i].begin(), vec[i].end()); } - d_out->explanation(utils::mkConjunction(assumptions)); - return; + return utils::mkConjunction(assumptions); } diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 5c6797e76..8ab806bd8 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -145,7 +145,7 @@ public: void propagate(Effort e) { } - void explain(TNode n); + Node explain(TNode n); Node getValue(TNode n); diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 7c474a811..4e185febc 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -223,7 +223,7 @@ void TheoryDatatypes::check(Effort e) { //if( conflict.getKind()!=kind::AND ){ // conflict = NodeManager::currentNM()->mkNode(kind::AND, conflict, conflict); //} - d_out->conflict( conflict, false ); + d_out->conflict(conflict); return; } } diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits index 852b29711..8e503f53e 100755 --- a/src/theory/mktheorytraits +++ b/src/theory/mktheorytraits @@ -49,6 +49,7 @@ theory_has_presolve="false" theory_stable_infinite="false" theory_finite="false" theory_polite="false" +theory_parametric="false" rewriter_class= rewriter_header= @@ -125,6 +126,7 @@ struct TheoryTraits<${theory_id}> { static const bool isStableInfinite = ${theory_stable_infinite}; static const bool isFinite = ${theory_finite}; static const bool isPolite = ${theory_polite}; + static const bool isParametric = ${theory_parametric}; static const bool hasCheck = ${theory_has_check}; static const bool hasPropagate = ${theory_has_propagate}; @@ -159,6 +161,7 @@ struct TheoryTraits<${theory_id}> { theory_stable_infinite="false" theory_finite="false" theory_polite="false" + theory_parametric="false" rewriter_class= rewriter_header= @@ -191,6 +194,7 @@ function properties { case "$property" in finite) theory_finite="true";; stable-infinite) theory_stable_infinite="true";; + parametric) theory_parametric="true";; polite) theory_polite="true";; check) theory_has_check="true";; propagate) theory_has_propagate="true";; diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index bf928cb62..f5bf620bf 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -69,59 +69,41 @@ public: * assigned false), or else a literal by itself (in the case of a * unit conflict) which is assigned TRUE (and T-conflicting) in the * current assignment. - * - * @param safe - whether it is safe to be interrupted */ - virtual void conflict(TNode n, bool safe = false) - throw(Interrupted, AssertionException) = 0; + virtual void conflict(TNode n) throw(AssertionException) = 0; /** * Propagate a theory literal. * * @param n - a theory consequence at the current decision level - * @param safe - whether it is safe to be interrupted */ - virtual void propagate(TNode n, bool safe = false) - throw(Interrupted, AssertionException) = 0; + virtual void propagate(TNode n) throw(AssertionException) = 0; /** * Tell the core that a valid theory lemma at decision level 0 has * been detected. (This requests a split.) * * @param n - a theory lemma valid at decision level 0 - * @param safe - whether it is safe to be interrupted + * @param removable - whether the lemma can be removed at any point */ - virtual void lemma(TNode n, bool safe = false) - throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException) = 0; + virtual void lemma(TNode n, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) = 0; /** * Request a split on a new theory atom. This is equivalent to * calling lemma({OR n (NOT n)}). * * @param n - a theory atom; must be of Boolean type - * @param safe - whether it is safe to be interrupted */ - void split(TNode n, bool safe = false) - throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException) { + void split(TNode n) throw(TypeCheckingExceptionPrivate, AssertionException) { lemma(n.orNode(n.notNode())); } /** - * Provide an explanation in response to an explanation request. - * - * @param n - an explanation - * @param safe - whether it is safe to be interrupted - */ - virtual void explanation(TNode n, bool safe = false) - throw(Interrupted, AssertionException) = 0; - - /** * Notification from a theory that it realizes it is incomplete at * this context level. If SAT is later determined by the * TheoryEngine, it should actually return an UNKNOWN result. */ - virtual void setIncomplete() - throw(Interrupted, AssertionException) = 0; + virtual void setIncomplete() throw(AssertionException) = 0; };/* class OutputChannel */ diff --git a/src/theory/shared_data.cpp b/src/theory/shared_data.cpp deleted file mode 100644 index 3e89dec7e..000000000 --- a/src/theory/shared_data.cpp +++ /dev/null @@ -1,94 +0,0 @@ -/********************* */ -/*! \file shared_data.cpp - ** \verbatim - ** Original author: barrett - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Implementation of shared data for shared term manager. - ** - ** Implementation of shared data used by the shared term manager. This is a - ** context-dependent object. - **/ - - -#include "theory/shared_data.h" -#include "theory/theory.h" - - -using namespace CVC4; -using namespace context; -using namespace theory; - - -SharedData::SharedData(Context * context, TNode n, uint64_t theories) : - ContextObj(context), - d_theories(theories), - d_size(1), - d_find(this), - d_proofNext(this), - d_edgeReversed(false), - d_explainingTheory(NULL), - d_rep(n) { -} - - -ContextObj* SharedData::save(ContextMemoryManager* pCMM) { - return new(pCMM) SharedData(*this); -} - - -void SharedData::restore(ContextObj* pContextObj) { - SharedData* data = (SharedData*)pContextObj; - d_theories = data->d_theories; - d_size = data->d_size; - d_find = data->d_find; - d_proofNext = data->d_proofNext; - d_edgeReversed = data->d_edgeReversed; - d_explainingTheory = data->d_explainingTheory; - d_rep = data->d_rep; -} - - -void SharedData::reverseEdges() { - Assert(!isProofRoot(), "reverseEdges called on proof root"); - - SharedData* parent = this; - SharedData* current = d_proofNext; - bool reversed = d_edgeReversed; - Theory* explainingTheory = d_explainingTheory; - - makeCurrent(); - - // Make this the proof root - d_proofNext = this; - - // Reverse the edges from here to the former root - bool tmpReversed; - Theory* tmpTheory; - SharedData* tmpData; - - while (!current->isProofRoot()) { - tmpReversed = current->getEdgeReversed(); - current->setEdgeReversed(!reversed); - reversed = tmpReversed; - - tmpTheory = current->getExplainingTheory(); - current->setExplainingTheory(explainingTheory); - explainingTheory = tmpTheory; - - tmpData = current->getProofNext(); - current->setProofNext(parent); - parent = current; - current = tmpData; - } - current->setEdgeReversed(!reversed); - current->setExplainingTheory(explainingTheory); - current->setProofNext(parent); -} diff --git a/src/theory/shared_data.h b/src/theory/shared_data.h deleted file mode 100644 index 7d6a9ebd2..000000000 --- a/src/theory/shared_data.h +++ /dev/null @@ -1,214 +0,0 @@ -/********************* */ -/*! \file shared_data.h - ** \verbatim - ** Original author: barrett - ** Major contributors: mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Context-dependent data class for shared terms - ** - ** Context-dependent data class for shared terms. - ** Used by SharedTermManager. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__SHARED_DATA_H -#define __CVC4__THEORY__SHARED_DATA_H - -#include "expr/node.h" -#include "context/context.h" -#include "context/cdo.h" -#include "context/context_mm.h" - -namespace CVC4 { - -namespace theory { - class Theory; -} - -/** - * SharedData is the data for shared terms and is context dependent. - * - * SharedData maintains: - * - list of theories sharing this term (as a bit-vector) - * - size of the equivalence class (valid only if it is a find-representative) - * - find pointer - * - proof tree pointer (for explanations) - * - equality associated with proof tree pointer - * - theory associated with proof tree pointer - * - the node associated with this data - * - * See also SharedAttr() in shared_term_manager.h - */ - -class SharedData : public context::ContextObj { -private: - /** - * Bit-vector representation of list of theories needing to be - * notified if this shared term is no longer the representative - */ - uint64_t d_theories; - - /** - * Size of this equivalence class - */ - unsigned d_size; - - /** - * Find pointer (standard union/find algorithm) - */ - SharedData* d_find; - - /** - * Pointer to next node (towards root) in proof forest - */ - SharedData* d_proofNext; - - /** - * In order to precisely reconstruct the equality that justifies - * this node being equal to the node at d_proofNext, we need to know - * whether this edge has been switched. Value is meaningless at the - * proof root. - */ - bool d_edgeReversed; - - /** - * The theory that can explain the equality of this node and the - * node at d_proofNext. Not valid if this is proof root. - */ - theory::Theory* d_explainingTheory; - - /** - * This is a pointer back to the node associated with this - * SharedData object. - * - * The following invariant should be maintained: - * - * (n.getAttribute(SharedAttr()))->d_rep == n - * - * i.e. rep is equal to the node that maps to the SharedData using - * SharedAttr. - */ - TNode d_rep; - - /** Context-dependent operation: save this SharedData */ - context::ContextObj* save(context::ContextMemoryManager* pCMM); - - /** Context-dependent operation: restore this SharedData */ - void restore(context::ContextObj* pContextObj); - -public: - /** - * Creates a SharedData object with the representative n - */ - SharedData(context::Context* context, TNode n, uint64_t theories); - - /** Destructor for SharedDatas */ - ~SharedData() { - destroy(); - } - - /** - * Get list of theories for this shared term - */ - uint64_t getTheories() const { return d_theories; } - - /** - * Set list of theories for this shared term - */ - void setTheories(uint64_t t) { makeCurrent(); d_theories = t; } - - /** - * Get size of equivalence class (valid if getFind() == this) - */ - unsigned getSize() const { return d_size; } - - /** - * Set size of equivalence class - */ - - void setSize(unsigned size) { makeCurrent(); d_size = size; } - - /** - * Returns the find pointer of the SharedData. If this is the - * representative of the equivalence class, then getFind() == this - */ - SharedData* getFind() const { return d_find; } - - /** - * Sets the find pointer - */ - void setFind(SharedData * pData) { makeCurrent(); d_find = pData; } - - /** - * Return true iff this is the root of the proof tree - */ - bool isProofRoot() const { return d_proofNext == this; } - - /** - * Get the next link in the proof tree - */ - SharedData* getProofNext() const { return d_proofNext; } - - /** - * Set the next link in the proof tree - */ - void setProofNext(SharedData* pData) { makeCurrent(); d_proofNext = pData; } - - /** - * Get the edge reversed property of this node - */ - bool getEdgeReversed() const { return d_edgeReversed; } - - /** - * Set the edge reversed flag to value - */ - void setEdgeReversed(bool value) { makeCurrent(); d_edgeReversed = value; } - - /** - * Get the original equality that created the link from this node to - * the next proof node. - */ - Node getEquality() const { - return d_edgeReversed - ? NodeManager::currentNM()->mkNode(kind::EQUAL, - d_proofNext->getRep(), d_rep) - : NodeManager::currentNM()->mkNode(kind::EQUAL, - d_rep, d_proofNext->getRep()); - } - - /** - * Get the explaining theory - */ - theory::Theory* getExplainingTheory() const { return d_explainingTheory; } - - /** - * Set the explaining theory - */ - void setExplainingTheory(theory::Theory* t) { - makeCurrent(); - d_explainingTheory = t; - } - - /** - * Get the shared term associated with this data - */ - Node getRep() const { return d_rep; } - - /** - * Reverse the edges in the proof tree from here to the root. - */ - void reverseEdges(); - -};/* class SharedData */ - -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__SHARED_DATA_H */ diff --git a/src/theory/shared_term_manager.cpp b/src/theory/shared_term_manager.cpp deleted file mode 100644 index 20f7a82f1..000000000 --- a/src/theory/shared_term_manager.cpp +++ /dev/null @@ -1,272 +0,0 @@ -/********************* */ -/*! \file shared_term_manager.cpp - ** \verbatim - ** Original author: barrett - ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief The shared term manager - ** - ** The shared term manager - **/ - -#include "theory/theory_engine.h" - -using namespace std; -using namespace CVC4; -using namespace CVC4::theory; - -namespace CVC4 { - - -SharedTermManager::SharedTermManager(TheoryEngine* engine, - context::Context* context) - : d_engine(engine), d_context(context), d_theories(64) { -} - - -SharedData* SharedTermManager::find(SharedData* pData) const { - // Check if pData is the representative - SharedData* next = pData->getFind(); - if (next == pData) return pData; - - // Check if its successor is the representative - SharedData* nextNext = next->getFind(); - if (nextNext == next) return next; - - // Otherwise, recurse and do find path-compression - next = find(nextNext); - pData->setFind(next); - return next; -} - - -void SharedTermManager::registerTheory(Theory* th) { - Assert(th->getId() < 64, "Theory ID out of bounds"); - d_theories[th->getId()] = th; -} - - -void SharedTermManager::addTerm(TNode n, Theory* parent, Theory* child) { - Assert(parent->getId() < 64 && child->getId() < 64, - "Theory ID out of bounds"); - Assert(d_theories[parent->getId()] == parent && - d_theories[child->getId()] == child, - "Theory not registered"); - - // A theory tag is represented by a 1 in the i^th bit where i is the - // theory id - uint64_t parentTag = (1 << parent->getId()); - uint64_t childTag = (1 << child->getId()); - uint64_t bothTags = parentTag | childTag; - - // Create or update the SharedData for n - SharedData* pData = NULL; - if(n.getAttribute(SharedAttr(), pData)) { - // The attribute already exists, just update it if necessary - uint64_t tags = pData->getTheories(); - uint64_t newTags = tags | bothTags; - if (tags == newTags) return; - - // Get the equivalence class representative -- if this is different from - // the current node, then we will need to notify the theories of that and - // update the theory tags on the representative node - SharedData* pDataFind = find(pData); - - // Notify parent theory if necessary - if (!(tags & parentTag)) { - parent->addSharedTerm(n); - if (pData != pDataFind) { - parent->notifyEq(n, pDataFind->getRep()); - } - } - - // Notify child theory if necessary - if (!(tags & childTag)) { - child->addSharedTerm(n); - if (pData != pDataFind) { - child->notifyEq(n, pDataFind->getRep()); - } - } - - // Update theory tags - pData->setTheories(newTags); - if (pData != pDataFind) { - tags = pDataFind->getTheories(); - newTags = tags | bothTags; - if (tags != newTags) { - pDataFind->setTheories(newTags); - } - } - } else { - // The attribute does not exist, so it is created and set - pData = new (true) SharedData(d_context, n, bothTags); - n.setAttribute(SharedAttr(), pData); - parent->addSharedTerm(n); - child->addSharedTerm(n); - } -} - - -void SharedTermManager::addEq(TNode eq, Theory* thReason) { - Assert(eq.getKind() == kind::EQUAL, - "SharedTermManager::addEq precondition violated"); - - TNode x = eq[0]; - TNode y = eq[1]; - - SharedData* pDataX = NULL; - SharedData* pDataY = NULL; - - // Grab the SharedData for each side of the equality, create if necessary - if(!x.getAttribute(SharedAttr(), pDataX)) { - pDataX = new (true) SharedData(d_context, x, 0); - x.setAttribute(SharedAttr(), pDataX); - } - if(!y.getAttribute(SharedAttr(), pDataY)) { - pDataY = new (true) SharedData(d_context, y, 0); - y.setAttribute(SharedAttr(), pDataY); - } - - // Get the representatives - SharedData* pDataXX = find(pDataX); - SharedData* pDataYY = find(pDataY); - - // If already in the same equivalence class, nothing to do - if(pDataXX == pDataYY) return; - - // Make sure we reverse the edges in the smaller tree - bool switched = false; - if(pDataXX->getSize() > pDataYY->getSize()) { - SharedData* tmp = pDataXX; - pDataXX = pDataYY; - pDataYY = tmp; - - tmp = pDataX; - pDataX = pDataY; - pDataY = tmp; - - switched = true; - } - - // Reverse the edges in the left proof tree and link the two trees - if(!pDataX->isProofRoot()) { - pDataX->reverseEdges(); - } - pDataX->setEdgeReversed(switched); - pDataX->setExplainingTheory(thReason); - pDataX->setProofNext(pDataY); - - // Set the equivalence class representative for the left node to be the right node - pDataXX->setFind(pDataYY); - pDataYY->setSize(pDataYY->getSize() + pDataXX->getSize()); - - // Update the theory tags for the new representative - uint64_t tags = pDataXX->getTheories(); - pDataYY->setTheories(pDataYY->getTheories() | tags); - - // Notify the theories that care about the left node - int id = 0; - while (tags != 0) { - if (tags & 1) { - d_theories[id]->notifyEq(pDataXX->getRep(), pDataYY->getRep()); - } - tags = tags >> 1; - ++id; - } -} - - -void SharedTermManager::collectExplanations(SharedData* pData, std::set<Node>& s) const { - Theory* expTh = pData->getExplainingTheory(); - if(expTh == NULL) { - // This equality is directly from SAT, no need to ask a theory for an explanation - s.insert(pData->getEquality()); - } - else { - // This equality was sent by a theory - ask the theory for the explanation - Node n = d_engine->getExplanation(pData->getEquality(), expTh); - if(n.getKind() == kind::AND) { - for (Node::iterator it = n.begin(), iend = n.end(); it != iend; ++it) { - s.insert(*it); - } - } - else { - s.insert(n); - } - } -} - - -// Explain this equality -Node SharedTermManager::explain(TNode eq) const { - Assert(eq.getKind() == kind::EQUAL && - eq[0].hasAttribute(SharedAttr()) && eq[1].hasAttribute(SharedAttr()), - "SharedTermManager::explain precondition violated"); - - TNode x = eq[0]; - TNode y = eq[1]; - - // Get the SharedData for both sides of the equality - SharedData* pDataX = x.getAttribute(SharedAttr()); - SharedData* pDataY = y.getAttribute(SharedAttr()); - - Assert(find(pDataX) == find(pDataY), - "invalid equality input to SharedTermManager::explain"); - - // Find the path between the two nodes and build up the explanation - std::set<Node> s; - SharedData* tmp = pDataX; - - // Check to see if Y is on path from X to root - while (!tmp->isProofRoot() && tmp != pDataY) { - tmp = tmp->getProofNext(); - } - if (tmp == pDataY) { - // Y is on path from X to root, just traverse that path - while (pDataX != pDataY) { - collectExplanations(pDataX, s); - pDataX = pDataX->getProofNext(); - } - } - else { - // Y is not on path from X to root, so traverse from Y to root instead - while (!pDataY->isProofRoot() && pDataX != pDataY) { - collectExplanations(pDataY, s); - pDataY = pDataY->getProofNext(); - } - } - if (pDataX != pDataY) { - // X and Y are on different branches - have to traverse both - while (!pDataX->isProofRoot()) { - collectExplanations(pDataX, s); - pDataX = pDataX->getProofNext(); - } - } - - // Build explanation from s - NodeBuilder<> nb(kind::AND); - set<Node>::iterator it = s.begin(), iend = s.end(); - for (; it != iend; ++it) { - nb << *it; - } - return nb.constructNode(); -} - - -Node SharedTermManager::getRep(TNode n) const { - Assert(n.hasAttribute(SharedAttr()), - "SharedTermManager::getRep precondition violated"); - - SharedData* pData = n.getAttribute(SharedAttr()); - return find(pData)->getRep(); -} - - -}/* CVC4 namespace */ diff --git a/src/theory/shared_term_manager.h b/src/theory/shared_term_manager.h deleted file mode 100644 index faea8d687..000000000 --- a/src/theory/shared_term_manager.h +++ /dev/null @@ -1,146 +0,0 @@ -/********************* */ -/*! \file shared_term_manager.h - ** \verbatim - ** Original author: barrett - ** Major contributors: mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Manager for shared terms - ** - ** Manager for shared terms. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__SHARED_TERM_MANAGER_H -#define __CVC4__SHARED_TERM_MANAGER_H - -#include <set> -#include <vector> - -#include "expr/node.h" -#include "theory/shared_data.h" - -namespace CVC4 { - -namespace context { - class Context; -} - -namespace theory { - class Theory; -} - -/** - * Manages shared terms - */ -class SharedTermManager { - - /** - * Pointer back to theory engine - */ - TheoryEngine* d_engine; - - /** - * Pointer to context - */ - context::Context* d_context; - - /** - * List of all theories indexed by theory id (built by calls to - * registerTheory()) - */ - std::vector<theory::Theory*> d_theories; - - /** - * Private method to find equivalence class representative in - * union-find data structure. - */ - SharedData* find(SharedData* pData) const; - - /** - * Helper function for explain: add all reasons for equality at - * pData to set s - */ - void collectExplanations(SharedData* pData, std::set<Node>& s) const; - -public: - /** - * Constructor - */ - SharedTermManager(TheoryEngine* engine, context::Context* context); - - /** - * Should be called once for each theory at setup time - */ - void registerTheory(theory::Theory* th); - - /** - * Called by theory engine to indicate that node n is shared by - * theories parent and child. - */ - void addTerm(TNode n, theory::Theory* parent, - theory::Theory* child); - - /** - * Called by theory engine or theories to notify the shared term - * manager that two terms are equal. - * - * @param eq the equality between shared terms - * @param thReason the theory that knows why, NULL means it's a SAT - * assertion - */ - void addEq(TNode eq, theory::Theory* thReason = NULL); - - /** - * Called by theory engine or theories to notify the shared term - * manager that two terms are disequal. - * - * @param eq the equality between shared terms whose negation now - * holds - * @param thReason the theory that knows why, NULL means it's a SAT - * assertion - */ - void addDiseq(TNode eq, theory::Theory* thReason = NULL) { } - - /** - * Get an explanation for an equality known by the SharedTermManager - */ - Node explain(TNode eq) const; - - /** - * Get the representative node in the equivalence class containing n - */ - Node getRep(TNode n) const; - -};/* class SharedTermManager */ - -/** - * Cleanup function for SharedData. This will be called whenever - * a SharedAttr is being destructed. - */ -struct SharedDataCleanupStrategy { - static void cleanup(SharedData* sd) { - sd->deleteSelf(); - } -};/* struct SharedDataCleanupStrategy */ - -/** Unique name to use for constructing ECAttr. */ -struct SharedAttrTag {}; - -/** - * SharedAttr is the attribute that maps a node to its SharedData. - */ -typedef expr::Attribute<SharedAttrTag, SharedData*, - SharedDataCleanupStrategy> SharedAttr; - - -}/* CVC4 namespace */ - -#endif /* __CVC4__SHARED_TERM_MANAGER_H */ diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp new file mode 100644 index 000000000..9ec421677 --- /dev/null +++ b/src/theory/shared_terms_database.cpp @@ -0,0 +1,92 @@ +/********************* */ +/*! \file shared_terms_manager.cpp + ** \verbatim + ** Original author: dejan + ** Major contributors: + ** Minor contributors (to current version): + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + **/ + +#include "theory/shared_terms_database.h" + +using namespace CVC4; +using namespace CVC4::theory; + +void SharedTermsDatabase::addSharedTerm(TNode atom, TNode term, Theory::Set theories) { + Debug("register") << "SharedTermsDatabase::addSharedTerm(" << atom << ", " << term << ", " << Theory::setToString(theories) << ")" << std::endl; + std::pair<TNode, TNode> search_pair(atom, term); + SharedTermsTheoriesMap::iterator find = d_termsToTheories.find(search_pair); + if (find == d_termsToTheories.end()) { + // First time for this term and this atom + d_atomsToTerms[atom].push_back(term); + d_addedSharedTerms.push_back(atom); + d_addedSharedTermsSize = d_addedSharedTermsSize + 1; + d_termsToTheories[search_pair] = theories; + } else { + Assert(theories != (*find).second); + d_termsToTheories[search_pair] = Theory::setUnion(theories, (*find).second); + } +} + +SharedTermsDatabase::shared_terms_iterator SharedTermsDatabase::begin(TNode atom) const { + Assert(hasSharedTerms(atom)); + return d_atomsToTerms.find(atom)->second.begin(); +} + +SharedTermsDatabase::shared_terms_iterator SharedTermsDatabase::end(TNode atom) const { + Assert(hasSharedTerms(atom)); + return d_atomsToTerms.find(atom)->second.end(); +} + +bool SharedTermsDatabase::hasSharedTerms(TNode atom) const { + return d_atomsToTerms.find(atom) != d_atomsToTerms.end(); +} + +void SharedTermsDatabase::backtrack() { + for (int i = d_addedSharedTerms.size() - 1, i_end = (int)d_addedSharedTermsSize; i >= i_end; -- i) { + TNode atom = d_addedSharedTerms[i]; + shared_terms_list& list = d_atomsToTerms[atom]; + list.pop_back(); + if (list.empty()) { + d_atomsToTerms.erase(atom); + } + } + d_addedSharedTerms.resize(d_addedSharedTermsSize); +} + +Theory::Set SharedTermsDatabase::getTheoriesToNotify(TNode atom, TNode term) const { + // Get the theories that share this term from this atom + std::pair<TNode, TNode> search_pair(atom, term); + SharedTermsTheoriesMap::iterator find = d_termsToTheories.find(search_pair); + Assert(find != d_termsToTheories.end()); + + // Get the theories that were already notified + Theory::Set alreadyNotified = 0; + AlreadyNotifiedMap::iterator theoriesFind = d_alreadyNotifiedMap.find(term); + if (theoriesFind != d_alreadyNotifiedMap.end()) { + alreadyNotified = (*theoriesFind).second; + } + + // Return the ones that haven't been notified yet + return Theory::setDifference((*find).second, alreadyNotified); +} + +Theory::Set SharedTermsDatabase::getNotifiedTheories(TNode term) const { + // Get the theories that were already notified + AlreadyNotifiedMap::iterator theoriesFind = d_alreadyNotifiedMap.find(term); + if (theoriesFind != d_alreadyNotifiedMap.end()) { + return (*theoriesFind).second; + } else { + return 0; + } +} + +void SharedTermsDatabase::markNotified(TNode term, Theory::Set theories) { + d_alreadyNotifiedMap[term] = Theory::setUnion(theories, d_alreadyNotifiedMap[term]); +} + diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h new file mode 100644 index 000000000..a5481b807 --- /dev/null +++ b/src/theory/shared_terms_database.h @@ -0,0 +1,128 @@ +/********************* */ +/*! \file node_visitor.h + ** \verbatim + ** Original author: dejan + ** Major contributors: + ** Minor contributors (to current version): + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + **/ + +#pragma once + +#include "cvc4_private.h" + +#include "expr/node.h" +#include "theory/theory.h" +#include "context/context.h" +#include "util/stats.h" + +namespace CVC4 { + +class SharedTermsDatabase : public context::ContextNotifyObj { + +public: + + /** A conainer for a list of shared terms */ + typedef std::vector<TNode> shared_terms_list; + /** The iterator to go rhough the shared terms list */ + typedef shared_terms_list::const_iterator shared_terms_iterator; + +private: + + /** The context */ + context::Context* d_context; + + /** Some statistics */ + IntStat d_statSharedTerms; + + // Needs to be a map from Nodes as after a backtrack they might not exist + typedef std::hash_map<Node, shared_terms_list, TNodeHashFunction> SharedTermsMap; + /** A map from atoms to a list of shared terms */ + SharedTermsMap d_atomsToTerms; + + /** Each time we add a shared term, we add it's parent to this list */ + std::vector<TNode> d_addedSharedTerms; + + /** Context-dependent size of the d_addedSharedTerms list */ + context::CDO<unsigned> d_addedSharedTermsSize; + + typedef context::CDMap<std::pair<Node, TNode>, theory::Theory::Set, TNodePairHashFunction> SharedTermsTheoriesMap; + /** A map from atoms and subterms to the theories that use it */ + SharedTermsTheoriesMap d_termsToTheories; + + typedef context::CDMap<TNode, theory::Theory::Set, TNodeHashFunction> AlreadyNotifiedMap; + /** Map from term to theories that have already been notified about the shared term */ + AlreadyNotifiedMap d_alreadyNotifiedMap; + + /** This method removes all the un-necessary stuff from the maps */ + void backtrack(); + +public: + + SharedTermsDatabase(context::Context* context) + : ContextNotifyObj(context), + d_context(context), + d_statSharedTerms("theory::shared_terms", 0), + d_addedSharedTermsSize(context, 0), + d_termsToTheories(context), + d_alreadyNotifiedMap(context) + { + StatisticsRegistry::registerStat(&d_statSharedTerms); + } + + ~SharedTermsDatabase() throw(AssertionException) + { + StatisticsRegistry::unregisterStat(&d_statSharedTerms); + } + + /** + * Add a shared term to the database. The shared term is a subterm of the atom and + * should be associated with the given theory. + */ + void addSharedTerm(TNode atom, TNode term, theory::Theory::Set theories); + + /** + * Returns true if the atom contains any shared terms, false otherwise. + */ + bool hasSharedTerms(TNode atom) const; + + /** + * Iterator pointing to the first shared term belonging to the given atom. + */ + shared_terms_iterator begin(TNode atom) const; + + /** + * Iterator pointing to the end of the list of shared terms belonging to the given atom. + */ + shared_terms_iterator end(TNode atom) const; + + /** + * Get the theories that share the term in a given atom (and have not yet been notified). + */ + theory::Theory::Set getTheoriesToNotify(TNode atom, TNode term) const; + + /** + * Get the theories that share the term and have been notified already. + */ + theory::Theory::Set getNotifiedTheories(TNode term) const; + + /** + * Mark that the given theories have been notified of the given shared term. + */ + void markNotified(TNode term, theory::Theory::Set theories); + + /** + * This method gets called on backtracks from the context manager. + */ + void notify() { + backtrack(); + } +}; + +} + diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp new file mode 100644 index 000000000..1e7222532 --- /dev/null +++ b/src/theory/term_registration_visitor.cpp @@ -0,0 +1,182 @@ +/********************* */ +/*! \file term_registration_visitor.h + ** \verbatim + ** Original author: dejan + ** Major contributors: + ** Minor contributors (to current version): + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + **/ + +#include "theory/term_registration_visitor.h" +#include "theory/theory_engine.h" + +using namespace std; +using namespace CVC4; +using namespace theory; + +std::string PreRegisterVisitor::toString() const { + std::stringstream ss; + TNodeVisitedMap::const_iterator it = d_visited.begin(); + for (; it != d_visited.end(); ++ it) { + ss << (*it).first << ": " << Theory::setToString((*it).second) << std::endl; + } + return ss.str(); +} + +bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) const { + + Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ") => "; + + TNodeVisitedMap::iterator find = d_visited.find(current); + + // If node is not visited at all, just return false + if (find == d_visited.end()) { + Debug("register::internal") << "1:false" << std::endl; + return false; + } + + Theory::Set theories = (*find).second; + + TheoryId currentTheoryId = Theory::theoryOf(current); + TheoryId parentTheoryId = Theory::theoryOf(parent); + + if (Theory::setContains(currentTheoryId, theories)) { + // The current theory has already visited it, so now it depends on the parent + Debug("register::internal") << (Theory::setContains(parentTheoryId, theories) ? "2:true" : "2:false") << std::endl; + return Theory::setContains(parentTheoryId, theories); + } else { + // If the current theory is not registered, it still needs to be visited + Debug("register::internal") << "2:false" << std::endl; + return false; + } +} + +void PreRegisterVisitor::visit(TNode current, TNode parent) { + + Debug("register") << "PreRegisterVisitor::visit(" << current << "," << parent << ")" << std::endl; + Debug("register::internal") << toString() << std::endl; + + // Get the theories of the terms + TheoryId currentTheoryId = Theory::theoryOf(current); + TheoryId parentTheoryId = Theory::theoryOf(parent); + + Theory::Set theories = d_visited[current]; + Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(theories) << std::endl; + if (!Theory::setContains(currentTheoryId, theories)) { + d_multipleTheories = d_multipleTheories || (theories != 0); + d_visited[current] = theories = Theory::setInsert(currentTheoryId, theories); + d_engine->theoryOf(currentTheoryId)->preRegisterTerm(current); + d_theories = Theory::setInsert(currentTheoryId, d_theories); + Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl; + } + if (!Theory::setContains(parentTheoryId, theories)) { + d_multipleTheories = d_multipleTheories || (theories != 0); + d_visited[current] = theories = Theory::setInsert(parentTheoryId, theories); + d_engine->theoryOf(parentTheoryId)->preRegisterTerm(current); + d_theories = Theory::setInsert(parentTheoryId, d_theories); + Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl; + } + Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(theories) << std::endl; + + Assert(d_visited.find(current) != d_visited.end()); + Assert(alreadyVisited(current, parent)); +} + +void PreRegisterVisitor::start(TNode node) { + d_theories = 0; + d_multipleTheories = false; +} + +bool PreRegisterVisitor::done(TNode node) { + d_engine->markActive(d_theories); + return d_multipleTheories; +} + +std::string SharedTermsVisitor::toString() const { + std::stringstream ss; + TNodeVisitedMap::const_iterator it = d_visited.begin(); + for (; it != d_visited.end(); ++ it) { + ss << (*it).first << ": " << Theory::setToString((*it).second) << std::endl; + } + return ss.str(); +} + +bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { + + Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ") => "; + + TNodeVisitedMap::const_iterator find = d_visited.find(current); + + // If node is not visited at all, just return false + if (find == d_visited.end()) { + Debug("register::internal") << "1:false" << std::endl; + return false; + } + + Theory::Set theories = (*find).second; + + TheoryId currentTheoryId = Theory::theoryOf(current); + TheoryId parentTheoryId = Theory::theoryOf(parent); + + if (Theory::setContains(currentTheoryId, theories)) { + // The current theory has already visited it, so now it depends on the parent + Debug("register::internal") << (Theory::setContains(parentTheoryId, theories) ? "2:true" : "2:false") << std::endl; + return Theory::setContains(parentTheoryId, theories); + } else { + // If the current theory is not registered, it still needs to be visited + Debug("register::internal") << "2:false" << std::endl; + return false; + } +} + +void SharedTermsVisitor::visit(TNode current, TNode parent) { + + Debug("register") << "SharedTermsVisitor::visit(" << current << "," << parent << ")" << std::endl; + Debug("register::internal") << toString() << std::endl; + + // Get the theories of the terms + TheoryId currentTheoryId = Theory::theoryOf(current); + TheoryId parentTheoryId = Theory::theoryOf(parent); + + Theory::Set theories = d_visited[current]; + unsigned theoriesCount = theories == 0 ? 0 : 1; + Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(theories) << std::endl; + if (!Theory::setContains(currentTheoryId, theories)) { + d_visited[current] = theories = Theory::setInsert(currentTheoryId, theories); + theoriesCount ++; + Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl; + } + if (!Theory::setContains(parentTheoryId, theories)) { + d_visited[current] = theories = Theory::setInsert(parentTheoryId, theories); + theoriesCount ++; + Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl; + } + Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(theories) << std::endl; + + // If there is more than two theories and a new one has been added notify the shared terms database + if (theoriesCount > 1) { + d_sharedTerms.addSharedTerm(d_atom, current, theories); + } + + Assert(d_visited.find(current) != d_visited.end()); + Assert(alreadyVisited(current, parent)); +} + +void SharedTermsVisitor::start(TNode node) { + clear(); + d_atom = node; +} + +void SharedTermsVisitor::done(TNode node) { + clear(); +} + +void SharedTermsVisitor::clear() { + d_atom = TNode(); + d_visited.clear(); +} diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h new file mode 100644 index 000000000..29269bb52 --- /dev/null +++ b/src/theory/term_registration_visitor.h @@ -0,0 +1,146 @@ +/********************* */ +/*! \file node_visitor.h + ** \verbatim + ** Original author: dejan + ** Major contributors: + ** Minor contributors (to current version): + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + **/ + +#pragma once + +#include "context/context.h" +#include "theory/shared_terms_database.h" + +#include <ext/hash_map> + +namespace CVC4 { + +class TheoryEngine; + +/** + * Visitor that calls the apropriate theory to preregister the term. + */ +class PreRegisterVisitor { + + /** The engine */ + TheoryEngine* d_engine; + + /** + * Map from nodes to the theories that have already seen them. + */ + typedef context::CDMap<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap; + TNodeVisitedMap d_visited; + + /** + * All the theories of the visitation. + */ + theory::Theory::Set d_theories; + + /** + * String representation of the visited map, for debugging purposes. + */ + std::string toString() const; + + /** + * Is there more than one theory involved. + */ + bool d_multipleTheories; + +public: + + /** Return type tells us if there are more than one theory or not */ + typedef bool return_type; + + PreRegisterVisitor(TheoryEngine* engine, context::Context* context) + : d_engine(engine), d_visited(context), d_theories(0) {} + + /** + * Returns true is current has already been pre-registered with both current and parent theories. + */ + bool alreadyVisited(TNode current, TNode parent) const; + + /** + * Pre-registeres current with any of the current and parent theories that haven't seen the term yet. + */ + void visit(TNode current, TNode parent); + + /** + * Marks the node as the starting literal. + */ + void start(TNode node); + + /** + * Notifies the engine of all the theories used. + */ + bool done(TNode node); + +}; + + +/** + * The reason why we need to make this outside of the pre-registration loop is because we need a shared term x to + * be associated with every atom that contains it. For example, if given f(x) >= 0 and f(x) + 1 >= 0, although f(x) has + * been visited already, we need to visit it again, since we need to associate it with both atoms. + */ +class SharedTermsVisitor { + + /** The shared terms database */ + SharedTermsDatabase& d_sharedTerms; + + /** + * Cache from proprocessing of atoms. + */ + typedef std::hash_map<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap; + TNodeVisitedMap d_visited; + + /** + * String representation of the visited map, for debugging purposes. + */ + std::string toString() const; + + /** + * The initial atom. + */ + TNode d_atom; + +public: + + typedef void return_type; + + SharedTermsVisitor(SharedTermsDatabase& sharedTerms) + : d_sharedTerms(sharedTerms) {} + + /** + * Returns true is current has already been pre-registered with both current and parent theories. + */ + bool alreadyVisited(TNode current, TNode parent) const; + + /** + * Pre-registeres current with any of the current and parent theories that haven't seen the term yet. + */ + void visit(TNode current, TNode parent); + + /** + * Marks the node as the starting literal. + */ + void start(TNode node); + + /** + * Just clears the state. + */ + void done(TNode node); + + /** + * Clears the internal state. + */ + void clear(); +}; + + +} diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index b772d9d23..1451f654a 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -45,5 +45,35 @@ std::ostream& operator<<(std::ostream& os, Theory::Effort level){ return os; }/* ostream& operator<<(ostream&, Theory::Effort) */ +void Theory::addSharedTermInternal(TNode n) { + Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << std::endl; + d_sharedTerms.push_back(n); + addSharedTerm(n); +} + +void Theory::computeCareGraph(CareGraph& careGraph) { + for (; d_sharedTermsIndex < d_sharedTerms.size(); d_sharedTermsIndex = d_sharedTermsIndex + 1) { + TNode a = d_sharedTerms[d_sharedTermsIndex]; + TypeNode aType = a.getType(); + for (unsigned i = 0; i < d_sharedTermsIndex; ++ i) { + TNode b = d_sharedTerms[i]; + if (b.getType() != aType) { + // We don't care about the terms of different types + continue; + } + switch (equalityStatus(a, b)) { + case EQUALITY_TRUE: + case EQUALITY_FALSE: + // If we know about it, we should have propagated it, so we can skip + break; + default: + // Let's split on it + careGraph.push_back(CarePair(a, b, getId())); + break; + } + } + } +} + }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/theory.h b/src/theory/theory.h index a1d62ca04..931b1155e 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -42,6 +42,37 @@ class TheoryEngine; namespace theory { /** + * The status of an equality in the current context. + */ +enum EqualityStatus { + /** The eqaulity is known to be true */ + EQUALITY_TRUE, + /** The equality is known to be false */ + EQUALITY_FALSE, + /** The equality is not known, but is true in the current model */ + EQUALITY_TRUE_IN_MODEL, + /** The equality is not known, but is false in the current model */ + EQUALITY_FALSE_IN_MODEL, + /** The equality is completely unknown */ + EQUALITY_UNKNOWN +}; + +/** + * A pair of terms a theory cares about. + */ +struct CarePair { + TNode a, b; + TheoryId theory; + CarePair(TNode a, TNode b, TheoryId theory) + : a(a), b(b), theory(theory) {} +}; + +/** + * A set of care pairs. + */ +typedef std::vector<CarePair> CareGraph; + +/** * Base class for T-solvers. Abstract DPLL(T). * * This is essentially an interface class. The TheoryEngine has @@ -62,7 +93,7 @@ private: Theory& operator=(const Theory&) CVC4_UNUSED; /** - * A unique integer identifying the theory + * An integer identifying the type of the theory */ TheoryId d_id; @@ -77,19 +108,28 @@ private: * These can not be TNodes as some atoms (such as equalities) are sent * across theories without being stored in a global map. */ - context::CDList<Node> d_facts; + context::CDList<TNode> d_facts; /** Index into the head of the facts list */ context::CDO<unsigned> d_factsHead; /** - * Whether the last retrieved fact via get() was a shared term fact - * or not. + * Add shared term to the theory. + */ + void addSharedTermInternal(TNode node); + + /** + * Indices for splitting on the shared terms. */ - bool d_wasSharedTermFact; + context::CDO<unsigned> d_sharedTermsIndex; protected: + /** + * A list of shared terms that the theory has. + */ + context::CDList<TNode> d_sharedTerms; + /** * Construct a Theory. */ @@ -98,9 +138,11 @@ protected: d_context(ctxt), d_facts(ctxt), d_factsHead(ctxt, 0), - d_wasSharedTermFact(false), + d_sharedTermsIndex(ctxt, 0), + d_sharedTerms(ctxt), d_out(&out), - d_valuation(valuation) { + d_valuation(valuation) + { } /** @@ -126,43 +168,31 @@ protected: Valuation d_valuation; /** - * Returns the next atom in the assertFact() queue. + * Returns the next assertion in the assertFact() queue. * - * @return the next atom in the assertFact() queue + * @return the next assertion in the assertFact() queue */ TNode get() { - Assert( !done(), "Theory::get() called with assertion queue empty!" ); + Assert( !done(), "Theory`() called with assertion queue empty!" ); + + // Get the assertion TNode fact = d_facts[d_factsHead]; - d_wasSharedTermFact = false; d_factsHead = d_factsHead + 1; - Trace("theory") << "Theory::get() => " << fact - << " (" << d_facts.size() - d_factsHead << " left)" - << std::endl; + Trace("theory") << "Theory::get() => " << fact << " (" << d_facts.size() - d_factsHead << " left)" << std::endl; if(Dump.isOn("state")) { Dump("state") << AssertCommand(fact.toExpr()) << std::endl; } + return fact; } /** - * Returns whether the last fact retrieved by get() was a shared - * term fact. - * - * @return true if the fact just retrieved via get() was a shared - * term fact, false if the fact just retrieved was a "normal channel" - * fact. - */ - bool isSharedTermFact() const throw() { - return d_wasSharedTermFact; - } - - /** * Provides access to the facts queue, primarily intended for theory * debugging purposes. * * @return the iterator to the beginning of the fact queue */ - context::CDList<Node>::const_iterator facts_begin() const { + context::CDList<TNode>::const_iterator facts_begin() const { return d_facts.begin(); } @@ -172,7 +202,7 @@ protected: * * @return the iterator to the end of the fact queue */ - context::CDList<Node>::const_iterator facts_end() const { + context::CDList<TNode>::const_iterator facts_end() const { return d_facts.end(); } @@ -263,7 +293,8 @@ public: MIN_EFFORT = 0, QUICK_CHECK = 10, STANDARD = 50, - FULL_EFFORT = 100 + FULL_EFFORT = 100, + COMBINATION = 150 };/* enum Effort */ // simple, useful predicates for effort values @@ -278,7 +309,9 @@ public: static inline bool standardEffortOnly(Effort e) CVC4_CONST_FUNCTION { return e >= STANDARD && e < FULL_EFFORT; } static inline bool fullEffort(Effort e) CVC4_CONST_FUNCTION - { return e >= FULL_EFFORT; } + { return e == FULL_EFFORT; } + static inline bool combination(Effort e) CVC4_CONST_FUNCTION + { return e == COMBINATION; } /** * Get the id for this Theory. @@ -316,9 +349,9 @@ public: /** * Assert a fact in the current context. */ - void assertFact(TNode node) { - Trace("theory") << "Theory::assertFact(" << node << ")" << std::endl; - d_facts.push_back(node); + void assertFact(TNode assertion) { + Trace("theory") << "Theory<" << getId() << ">::assertFact(" << assertion << ")" << std::endl; + d_facts.push_back(assertion); } /** @@ -328,6 +361,18 @@ public: virtual void addSharedTerm(TNode n) { } /** + * The function should compute the care graph over the shared terms. + * The default function returns all the pairs among the shared variables. + */ + virtual void computeCareGraph(CareGraph& careGraph); + + /** + * Return the status of two terms in the current context. Should be implemented in + * sub-theories to enable more efficient theory-combination. + */ + virtual EqualityStatus equalityStatus(TNode a, TNode b) { return EQUALITY_UNKNOWN; } + + /** * This method is called by the shared term manager when a shared * term lhs which this theory cares about (either because it * received a previous addSharedTerm call with lhs or because it @@ -358,10 +403,9 @@ public: /** * Return an explanation for the literal represented by parameter n - * (which was previously propagated by this theory). Report - * explanations to an output channel. + * (which was previously propagated by this theory). */ - virtual void explain(TNode n) { + virtual Node explain(TNode n) { Unimplemented("Theory %s propagated a node but doesn't implement the " "Theory::explain() interface!", identify().c_str()); } @@ -481,6 +525,9 @@ public: /** A set of theories */ typedef uint32_t Set; + /** A set of all theories */ + static const Set AllTheories = (1 << theory::THEORY_LAST) - 1; + /** Add the theory to the set. If no set specified, just returns a singleton set */ static inline Set setInsert(TheoryId theory, Set set = 0) { return set | (1 << theory); @@ -491,10 +538,23 @@ public: return set & (1 << theory); } + static inline Set setComplement(Set a) { + return (~a) & AllTheories; + } + + static inline Set setIntersection(Set a, Set b) { + return a & b; + } + static inline Set setUnion(Set a, Set b) { return a | b; } + /** a - b */ + static inline Set setDifference(Set a, Set b) { + return ((~b) & AllTheories) & a; + } + static inline std::string setToString(theory::Theory::Set theorySet) { std::stringstream ss; ss << "["; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 040582c9f..d5ac8ddbb 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -37,40 +37,40 @@ using namespace std; using namespace CVC4; using namespace CVC4::theory; -TheoryEngine::TheoryEngine(context::Context* ctxt) : - d_propEngine(NULL), +TheoryEngine::TheoryEngine(context::Context* ctxt) +: d_propEngine(NULL), d_context(ctxt), d_activeTheories(0), + d_sharedTerms(ctxt), d_atomPreprocessingCache(), d_possiblePropagations(), d_hasPropagated(ctxt), - d_theoryOut(this, ctxt), - d_sharedTermManager(NULL), + d_inConflict(ctxt, false), d_hasShutDown(false), d_incomplete(ctxt, false), + d_sharedAssertions(ctxt), d_logic(""), - d_statistics(), - d_preRegistrationVisitor(*this, ctxt) { - - for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) { + d_propagatedLiterals(ctxt), + d_propagatedLiteralsIndex(ctxt, 0), + d_preRegistrationVisitor(this, ctxt), + d_sharedTermsVisitor(d_sharedTerms) +{ + for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) { d_theoryTable[theoryId] = NULL; + d_theoryOut[theoryId] = NULL; } - Rewriter::init(); - - d_sharedTermManager = new SharedTermManager(this, ctxt); } TheoryEngine::~TheoryEngine() { Assert(d_hasShutDown); - for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) { + for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) { if(d_theoryTable[theoryId] != NULL) { delete d_theoryTable[theoryId]; + delete d_theoryOut[theoryId]; } } - - delete d_sharedTermManager; } void TheoryEngine::setLogic(std::string logic) { @@ -79,62 +79,156 @@ void TheoryEngine::setLogic(std::string logic) { d_logic = logic; } -struct preregister_stack_element { - TNode node; - bool children_added; - preregister_stack_element(TNode node) - : node(node), children_added(false) {} -};/* struct preprocess_stack_element */ - void TheoryEngine::preRegister(TNode preprocessed) { if(Dump.isOn("missed-t-propagations")) { d_possiblePropagations.push_back(preprocessed); } - NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed); + // Pre-register the terms in the atom + bool multipleTheories = NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed); + if (multipleTheories) { + // Collect the shared terms if there are multipe theories + NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, preprocessed); + } } /** * Check all (currently-active) theories for conflicts. * @param effort the effort level to use */ -void TheoryEngine::check(theory::Theory::Effort effort) { - - d_theoryOut.d_propagatedLiterals.clear(); +void TheoryEngine::check(Theory::Effort effort) { #ifdef CVC4_FOR_EACH_THEORY_STATEMENT #undef CVC4_FOR_EACH_THEORY_STATEMENT #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ - if (theory::TheoryTraits<THEORY>::hasCheck && isActive(THEORY)) { \ - reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->check(effort); \ - if (d_theoryOut.d_inConflict) { \ - return; \ - } \ - } + if (theory::TheoryTraits<THEORY>::hasCheck && isActive(THEORY)) { \ + reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->check(effort); \ + if (d_inConflict) { \ + break; \ + } \ + } // Do the checking try { - CVC4_FOR_EACH_THEORY; - if(Dump.isOn("missed-t-conflicts")) { - Dump("missed-t-conflicts") - << CommentCommand("Completeness check for T-conflicts; expect sat") << endl - << CheckSatCommand() << endl; + // Clear any leftover propagated equalities + d_propagatedEqualities.clear(); + + // Mark the lemmas flag (no lemmas added) + d_lemmasAdded = false; + + while (true) { + + // Do the checking + CVC4_FOR_EACH_THEORY; + + if(Dump.isOn("missed-t-conflicts")) { + Dump("missed-t-conflicts") + << CommentCommand("Completeness check for T-conflicts; expect sat") << endl + << CheckSatCommand() << endl; + } + + // We are still satisfiable, propagate as much as possible + propagate(effort); + + // If we have any propagated equalities, we enqueue them to the theories and re-check + if (d_propagatedEqualities.size() > 0) { + assertSharedEqualities(); + continue; + } + + // If we added any lemmas, we're done + if (d_lemmasAdded) { + break; + } + + // If in full check and no lemmas added, run the combination + if (Theory::fullEffort(effort)) { + // Do the combination + combineTheories(); + // If we have any propagated equalities, we enqueue them to the theories and re-check + if (d_propagatedEqualities.size() > 0) { + assertSharedEqualities(); + } else { + // No propagated equalities, we're either sat, or there are lemmas added + break; + } + } else { + break; + } } + + // Clear any leftover propagated equalities + d_propagatedEqualities.clear(); + } catch(const theory::Interrupted&) { Trace("theory") << "TheoryEngine::check() => conflict" << endl; } } -void TheoryEngine::propagate() { +void TheoryEngine::assertSharedEqualities() { + // Assert all the shared equalities + for (unsigned i = 0; i < d_propagatedEqualities.size(); ++ i) { + const SharedEquality& eq = d_propagatedEqualities[i]; + // Check if the theory already got this one + if (d_sharedAssertions.find(eq.toAssert) != d_sharedAssertions.end()) { + d_sharedAssertions[eq.toAssert] = eq.toExplain; + theoryOf(eq.toAssert.theory)->assertFact(eq.toAssert.node); + } + } + // Clear the equalities + d_propagatedEqualities.clear(); +} + + +void TheoryEngine::combineTheories() { + + CareGraph careGraph; +#ifdef CVC4_FOR_EACH_THEORY_STATEMENT +#undef CVC4_FOR_EACH_THEORY_STATEMENT +#endif +#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ + if (theory::TheoryTraits<THEORY>::isParametric && isActive(THEORY)) { \ + CareGraph theoryGraph; \ + reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->computeCareGraph(theoryGraph); \ + careGraph.insert(careGraph.end(), theoryGraph.begin(), theoryGraph.end()); \ + } + + CVC4_FOR_EACH_THEORY; + + // Now add splitters for the ones we are interested in + for (unsigned i = 0; i < careGraph.size(); ++ i) { + const CarePair& carePair = careGraph[i]; + + Node equality = carePair.a.eqNode(carePair.b); + Node normalizedEquality = Rewriter::rewrite(equality); + + // If the node has a literal, it has been asserted so we should just check it + bool value; + if (d_propEngine->isSatLiteral(normalizedEquality) && d_propEngine->hasValue(normalizedEquality, value)) { + // Normalize the equality to the theory that requested it + Node toAssert = Rewriter::rewriteTo(carePair.theory, equality); + if (value) { + d_propagatedEqualities.push_back(SharedEquality(toAssert, normalizedEquality, theory::THEORY_LAST, carePair.theory)); + } else { + d_propagatedEqualities.push_back(SharedEquality(toAssert.notNode(), normalizedEquality.notNode(), theory::THEORY_LAST, carePair.theory)); + } + } else { + // There is no value, so we need to split on it + lemma(equality.orNode(equality.notNode()), false, false); + } + } +} + +void TheoryEngine::propagate(Theory::Effort effort) { // Definition of the statement that is to be run by every theory #ifdef CVC4_FOR_EACH_THEORY_STATEMENT #undef CVC4_FOR_EACH_THEORY_STATEMENT #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits<THEORY>::hasPropagate && isActive(THEORY)) { \ - reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->propagate(theory::Theory::FULL_EFFORT); \ + reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->propagate(effort); \ } // Propagate for each theory using the statement above @@ -154,21 +248,26 @@ void TheoryEngine::propagate() { } Node TheoryEngine::getExplanation(TNode node, theory::Theory* theory) { - theory->explain(node); + Node explanation = theory->explain(node); if(Dump.isOn("t-explanations")) { Dump("t-explanations") - << CommentCommand(string("theory explanation from ") + - theory->identify() + ": expect valid") << endl - << QueryCommand(d_theoryOut.d_explanationNode.get().impNode(node).toExpr()) - << endl; + << CommentCommand(string("theory explanation from ") + theory->identify() + ": expect valid") << endl + << QueryCommand(explanation.impNode(node).toExpr()) << endl; } - Assert(properExplanation(node, d_theoryOut.d_explanationNode.get())); - return d_theoryOut.d_explanationNode; + return explanation; } bool TheoryEngine::properConflict(TNode conflict) const { - Assert(!conflict.isNull()); -#warning fixme + bool value; + if (conflict.getKind() == kind::AND) { + for (unsigned i = 0; i < conflict.getNumChildren(); ++ i) { + if (!getPropEngine()->hasValue(conflict[i], value)) return false; + if (!value) return false; + } + } else { + if (!getPropEngine()->hasValue(conflict, value)) return false; + return value; + } return true; } @@ -206,8 +305,6 @@ bool TheoryEngine::presolve() { // at doing something with the input formula, even if it wouldn't // otherwise be active. - d_theoryOut.d_propagatedLiterals.clear(); - try { // Definition of the statement that is to be run by every theory #ifdef CVC4_FOR_EACH_THEORY_STATEMENT @@ -215,8 +312,8 @@ bool TheoryEngine::presolve() { #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits<THEORY>::hasPresolve) { \ - reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->presolve(); \ - if(d_theoryOut.d_inConflict) { \ + reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->presolve(); \ + if(d_inConflict) { \ return true; \ } \ } @@ -238,7 +335,7 @@ void TheoryEngine::notifyRestart() { #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits<THEORY>::hasNotifyRestart && isActive(THEORY)) { \ - reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->notifyRestart(); \ + reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->notifyRestart(); \ } // notify each theory using the statement above @@ -258,7 +355,7 @@ void TheoryEngine::staticLearning(TNode in, NodeBuilder<>& learned) { #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits<THEORY>::hasStaticLearning) { \ - reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->staticLearning(in, learned); \ + reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->staticLearning(in, learned); \ } // static learning for each theory using the statement above @@ -274,7 +371,7 @@ void TheoryEngine::shutdown() { // Shutdown all the theories for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) { if(d_theoryTable[theoryId]) { - d_theoryTable[theoryId]->shutdown(); + theoryOf(static_cast<TheoryId>(theoryId))->shutdown(); } } @@ -367,3 +464,74 @@ Node TheoryEngine::preprocess(TNode assertion) { return d_atomPreprocessingCache[assertion]; } +void TheoryEngine::assertFact(TNode node) +{ + Trace("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl; + + // Get the atom + TNode atom = node.getKind() == kind::NOT ? node[0] : node; + + // Assert the fact to the apropriate theory + theoryOf(atom)->assertFact(node); + + // If any shared terms, notify the theories + if (d_sharedTerms.hasSharedTerms(atom)) { + SharedTermsDatabase::shared_terms_iterator it = d_sharedTerms.begin(atom); + SharedTermsDatabase::shared_terms_iterator it_end = d_sharedTerms.end(atom); + for (; it != it_end; ++ it) { + TNode term = *it; + Theory::Set theories = d_sharedTerms.getTheoriesToNotify(atom, term); + for (TheoryId theory = THEORY_FIRST; theory != THEORY_LAST; ++ theory) { + if (Theory::setContains(theory, theories)) { + theoryOf(theory)->addSharedTermInternal(term); + } + } + d_sharedTerms.markNotified(term, theories); + } + } +} + +void TheoryEngine::propagate(TNode literal, TheoryId theory) { + + Debug("theory") << "EngineOutputChannel::propagate(" << literal << ")" << std::endl; + + if(Dump.isOn("t-propagations")) { + Dump("t-propagations") << CommentCommand("negation of theory propagation: expect valid") << std::endl + << QueryCommand(literal.toExpr()) << std::endl; + } + if(Dump.isOn("missed-t-propagations")) { + d_hasPropagated.insert(literal); + } + + if (literal.getKind() != kind::EQUAL) { + // If not an equality it must be a SAT literal so we enlist it, and it can only + // be propagated by the theory that owns it, as it is the only one that got + // a preregister call with it. + Assert(d_propEngine->isSatLiteral(literal)); + d_propagatedLiterals.push_back(literal); + } else { + // Otherwise it might be a shared-term (dis-)equality + Node normalizedEquality = Rewriter::rewrite(literal); + if (d_propEngine->isSatLiteral(normalizedEquality)) { + // If there is a literal, just enqueue it, same as above + d_propagatedLiterals.push_back(literal); + } else { + // Otherwise, we assert it to all interested theories + bool negated = literal.getKind() == kind::NOT; + Node equality = negated ? literal[0] : literal; + Theory::Set lhsNotified = d_sharedTerms.getNotifiedTheories(equality[0]); + Theory::Set rhsNotified = d_sharedTerms.getNotifiedTheories(equality[1]); + // Now notify the theories + for (TheoryId current = theory::THEORY_FIRST; current != theory::THEORY_LAST; ++ current) { + if (Theory::setContains(current, lhsNotified) && Theory::setContains(current, rhsNotified)) { + // Normalize the equality + Node equalityNormalized = Rewriter::rewriteTo(current, equality); + // The assertion + Node assertion = negated ? equalityNormalized.notNode() : equalityNormalized; + // Remember it to assert later + d_propagatedEqualities.push_back(SharedEquality(assertion, literal, theory, current)); + } + } + } + } +} diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 815a79a5a..04f15e89f 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -29,11 +29,12 @@ #include "expr/command.h" #include "prop/prop_engine.h" #include "context/cdset.h" -#include "theory/shared_term_manager.h" #include "theory/theory.h" #include "theory/substitutions.h" #include "theory/rewriter.h" #include "theory/substitutions.h" +#include "theory/shared_terms_database.h" +#include "theory/term_registration_visitor.h" #include "theory/valuation.h" #include "util/options.h" #include "util/stats.h" @@ -46,6 +47,25 @@ namespace CVC4 { // In terms of abstraction, this is below (and provides services to) // PropEngine. +struct NodeTheoryPair { + Node node; + theory::TheoryId theory; + NodeTheoryPair(Node node, theory::TheoryId theory) + : node(node), theory(theory) {} + NodeTheoryPair() + : theory(theory::THEORY_LAST) {} + bool operator == (const NodeTheoryPair& pair) const { + return node == pair.node && theory == pair.theory; + } +}; + +struct NodeTheoryPairHashFunction { + NodeHashFunction hashFunction; + size_t operator()(const NodeTheoryPair& pair) const { + return hashFunction(pair.node)*0x9e3779b9 + pair.theory; + } +}; + /** * This is essentially an abstraction for a collection of theories. A * TheoryEngine provides services to a PropEngine, making various @@ -60,7 +80,10 @@ class TheoryEngine { /** Our context */ context::Context* d_context; - /** A table of from theory IDs to theory pointers */ + /** + * A table of from theory IDs to theory pointers. Never use this table + * directly, use theoryOf() instead. + */ theory::Theory* d_theoryTable[theory::THEORY_LAST]; /** @@ -73,9 +96,15 @@ class TheoryEngine { theory::Theory::Set d_activeTheories; /** - * Cache from proprocessing of atoms. + * The database of shared terms. */ + SharedTermsDatabase d_sharedTerms; + typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; + + /** + * Cache from proprocessing of atoms. + */ NodeMap d_atomPreprocessingCache; /** @@ -92,6 +121,39 @@ class TheoryEngine { context::CDSet<TNode, TNodeHashFunction> d_hasPropagated; /** + * Statistics for a particular theory. + */ + class Statistics { + + static std::string mkName(std::string prefix, theory::TheoryId theory, std::string suffix) { + std::stringstream ss; + ss << prefix << theory << suffix; + return ss.str(); + } + + public: + + IntStat conflicts, propagations, lemmas; + + Statistics(theory::TheoryId theory): + conflicts(mkName("theory<", theory, ">::conflicts"), 0), + propagations(mkName("theory<", theory, ">::propagations"), 0), + lemmas(mkName("theory<", theory, ">::lemmas"), 0) + { + StatisticsRegistry::registerStat(&conflicts); + StatisticsRegistry::registerStat(&propagations); + StatisticsRegistry::registerStat(&lemmas); + } + + ~Statistics() { + StatisticsRegistry::unregisterStat(&conflicts); + StatisticsRegistry::unregisterStat(&propagations); + StatisticsRegistry::unregisterStat(&lemmas); + } + };/* class TheoryEngine::Statistics */ + + + /** * An output channel for Theory that passes messages * back to a TheoryEngine. */ @@ -99,113 +161,78 @@ class TheoryEngine { friend class TheoryEngine; + /** + * The theory engine we're communicating with. + */ TheoryEngine* d_engine; - context::Context* d_context; - context::CDO<bool> d_inConflict; - context::CDO<Node> d_explanationNode; /** - * Literals that are propagated by the theory. Note that these are TNodes. - * The theory can only propagate nodes that have an assigned literal in the - * sat solver and are hence referenced in the SAT solver. + * The statistics of the theory interractions. */ - std::vector<TNode> d_propagatedLiterals; + Statistics d_statistics; /** - * Check if the node is in conflict for debug purposes + * The theory owning this chanell. */ - bool isProperConflict(TNode conflictNode) { - bool value; - if (conflictNode.getKind() == kind::AND) { - for (unsigned i = 0; i < conflictNode.getNumChildren(); ++ i) { - if (!d_engine->getPropEngine()->hasValue(conflictNode[i], value)) return false; - if (!value) return false; - } - } else { - if (!d_engine->getPropEngine()->hasValue(conflictNode, value)) return false; - return value; - } - return true; - } + theory::TheoryId d_theory; public: - EngineOutputChannel(TheoryEngine* engine, context::Context* context) : + EngineOutputChannel(TheoryEngine* engine, theory::TheoryId theory) : d_engine(engine), - d_context(context), - d_inConflict(context, false), - d_explanationNode(context) { + d_statistics(theory), + d_theory(theory) + { } - void conflict(TNode conflictNode, bool safe) - throw(theory::Interrupted, AssertionException) { - Trace("theory") << "EngineOutputChannel::conflict(" << conflictNode << ")" << std::endl; - d_inConflict = true; - - if(Dump.isOn("t-conflicts")) { - Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat") << std::endl - << CheckSatCommand(conflictNode.toExpr()) << std::endl; - } - Assert(d_engine->properConflict(conflictNode)); - ++(d_engine->d_statistics.d_statConflicts); - - // Construct the lemma (note that no CNF caching should happen as all the literals already exists) - Assert(isProperConflict(conflictNode)); - d_engine->newLemma(conflictNode, true, false); - - if(safe) { - throw theory::Interrupted(); - } + void conflict(TNode conflictNode) throw(AssertionException) { + Trace("theory") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl; + ++ d_statistics.conflicts; + d_engine->conflict(conflictNode); } - void propagate(TNode lit, bool) - throw(theory::Interrupted, AssertionException) { - Trace("theory") << "EngineOutputChannel::propagate(" - << lit << ")" << std::endl; - if(Dump.isOn("t-propagations")) { - Dump("t-propagations") - << CommentCommand("negation of theory propagation: expect valid") << std::endl - << QueryCommand(lit.toExpr()) << std::endl; - } - if(Dump.isOn("missed-t-propagations")) { - d_engine->d_hasPropagated.insert(lit); - } - Assert(d_engine->properPropagation(lit)); - d_propagatedLiterals.push_back(lit); - ++(d_engine->d_statistics.d_statPropagate); + void propagate(TNode literal) throw(AssertionException) { + Trace("theory") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl; + ++ d_statistics.propagations; + d_engine->propagate(literal, d_theory); } - void lemma(TNode node, bool removable = false) - throw(theory::Interrupted, TypeCheckingExceptionPrivate, AssertionException) { - Trace("theory") << "EngineOutputChannel::lemma(" - << node << ")" << std::endl; - if(Dump.isOn("t-lemmas")) { - Dump("t-lemmas") << CommentCommand("theory lemma: expect valid") << std::endl - << QueryCommand(node.toExpr()) << std::endl; - } - ++(d_engine->d_statistics.d_statLemma); - - d_engine->newLemma(node, false, removable); + void lemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) { + Trace("theory") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; + ++ d_statistics.lemmas; + d_engine->lemma(lemma, false, removable); } - void explanation(TNode explanationNode, bool) - throw(theory::Interrupted, AssertionException) { - Trace("theory") << "EngineOutputChannel::explanation(" - << explanationNode << ")" << std::endl; - // handle dumping of explanations elsewhere.. - d_explanationNode = explanationNode; - ++(d_engine->d_statistics.d_statExplanation); - } - - void setIncomplete() throw(theory::Interrupted, AssertionException) { - d_engine->d_incomplete = true; + void setIncomplete() throw(AssertionException) { + d_engine->setIncomplete(d_theory); } };/* class EngineOutputChannel */ - EngineOutputChannel d_theoryOut; + /** + * Output channels for individual theories. + */ + EngineOutputChannel* d_theoryOut[theory::THEORY_LAST]; + + /** + * Are we in conflict. + */ + context::CDO<bool> d_inConflict; + + void conflict(TNode conflict) { + + Assert(properConflict(conflict)); - /** Pointer to Shared Term Manager */ - SharedTermManager* d_sharedTermManager; + // Mark that we are in conflict + d_inConflict = true; + + if(Dump.isOn("t-conflicts")) { + Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat") << std::endl + << CheckSatCommand(conflict.toExpr()) << std::endl; + } + + // Construct the lemma (note that no CNF caching should happen as all the literals already exists) + lemma(conflict, true, false); + } /** * Debugging flag to ensure that shutdown() is called before the @@ -220,10 +247,10 @@ class TheoryEngine { context::CDO<bool> d_incomplete; /** - * Mark a theory active if it's not already. + * Called by the theories to notify that the current branch is incomplete. */ - void markActive(theory::Theory::Set theories) { - d_activeTheories = theory::Theory::setUnion(d_activeTheories, theories); + void setIncomplete(theory::TheoryId theory) { + d_incomplete = true; } /** @@ -233,9 +260,86 @@ class TheoryEngine { return theory::Theory::setContains(theory, d_activeTheories); } + struct SharedEquality { + /** The node/theory pair for the assertion */ + NodeTheoryPair toAssert; + /** This is the node/theory pair that we will use to explain it */ + NodeTheoryPair toExplain; + + SharedEquality(TNode assertion, TNode original, theory::TheoryId sendingTheory, theory::TheoryId receivingTheory) + : toAssert(assertion, sendingTheory), + toExplain(original, receivingTheory) + { } + }; + + /** + * A map from asserted facts to where they came from (for explanations). + */ + context::CDMap<NodeTheoryPair, NodeTheoryPair, NodeTheoryPairHashFunction> d_sharedAssertions; + + /** + * Assert a shared equalities propagated by theories. + */ + void assertSharedEqualities(); + /** The logic of the problem */ std::string d_logic; + /** + * Literals that are propagated by the theory. Note that these are TNodes. + * The theory can only propagate nodes that have an assigned literal in the + * sat solver and are hence referenced in the SAT solver. + */ + context::CDList<TNode> d_propagatedLiterals; + + /** + * The index of the next literal to be propagated by a theory. + */ + context::CDO<unsigned> d_propagatedLiteralsIndex; + + /** + * Shared term equalities that should be asserted to the individual theories. + */ + std::vector<SharedEquality> d_propagatedEqualities; + + /** + * Called by the output channel to propagate literals and facts + */ + void propagate(TNode literal, theory::TheoryId theory); + + /** + * Internal method to call the propagation routines and collect the + * propagated literals. + */ + void propagate(theory::Theory::Effort effort); + + /** + * A variable to mark if we added any lemmas. + */ + bool d_lemmasAdded; + + /** + * Adds a new lemma + */ + void lemma(TNode node, bool negated, bool removable) { + + if(Dump.isOn("t-lemmas")) { + Dump("t-lemmas") << CommentCommand("theory lemma: expect valid") << std::endl + << QueryCommand(node.toExpr()) << std::endl; + } + // Remove the ITEs and assert to prop engine + std::vector<Node> additionalLemmas; + additionalLemmas.push_back(node); + RemoveITE::run(additionalLemmas); + d_propEngine->assertLemma(theory::Rewriter::rewrite(additionalLemmas[0]), negated, removable); + for (unsigned i = 1; i < additionalLemmas.size(); ++ i) { + d_propEngine->assertLemma(theory::Rewriter::rewrite(additionalLemmas[i]), false, removable); + } + + // Mark that we added some lemmas + d_lemmasAdded = true; + } + public: /** Constructs a theory engine */ @@ -249,10 +353,10 @@ public: * there is another theory it will be deleted. */ template <class TheoryClass> - inline void addTheory() { - TheoryClass* theory = new TheoryClass(d_context, d_theoryOut, theory::Valuation(this)); - d_theoryTable[theory->getId()] = theory; - d_sharedTermManager->registerTheory(static_cast<TheoryClass*>(theory)); + inline void addTheory(theory::TheoryId theoryId) { + Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL); + d_theoryOut[theoryId] = new EngineOutputChannel(this, theoryId); + d_theoryTable[theoryId] = new TheoryClass(d_context, *d_theoryOut[theoryId], theory::Valuation(this)); } /** @@ -261,8 +365,11 @@ public: */ void setLogic(std::string logic); - SharedTermManager* getSharedTermManager() { - return d_sharedTermManager; + /** + * Mark a theory active if it's not already. + */ + void markActive(theory::Theory::Set theories) { + d_activeTheories = theory::Theory::setUnion(d_activeTheories, theories); } inline void setPropEngine(prop::PropEngine* propEngine) { @@ -298,26 +405,6 @@ public: void shutdown(); /** - * Get the theory associated to a given Node. - * - * @returns the theory, or NULL if the TNode is - * of built-in type. - */ - inline theory::Theory* theoryOf(TNode node) { - return d_theoryTable[theory::Theory::theoryOf(node)]; - } - - /** - * Get the theory associated to a the given theory id. - * - * @returns the theory, or NULL if the TNode is - * of built-in type. - */ - inline theory::Theory* theoryOf(theory::TheoryId theoryId) { - return d_theoryTable[theoryId]; - } - - /** * Solve the given literal with a theory that owns it. */ theory::Theory::SolveStatus solve(TNode literal, theory::SubstitutionMap& substitionOut); @@ -341,16 +428,7 @@ public: * Assert the formula to the appropriate theory. * @param node the assertion */ - inline void assertFact(TNode node) { - Trace("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl; - - // Get the atom - TNode atom = node.getKind() == kind::NOT ? node[0] : node; - - theory::Theory* theory = theoryOf(atom); - Trace("theory") << "asserting " << node << " to " << theory->getId() << std::endl; - theory->assertFact(node); - } + void assertFact(TNode node); /** * Check all (currently-active) theories for conflicts. @@ -359,6 +437,11 @@ public: void check(theory::Theory::Effort effort); /** + * Run the combination framework. + */ + void combineTheories(); + + /** * Calls staticLearning() on all theories, accumulating their * combined contributions in the "learned" builder. */ @@ -375,27 +458,12 @@ public: */ void notifyRestart(); - inline const std::vector<TNode>& getPropagatedLiterals() const { - return d_theoryOut.d_propagatedLiterals; - } - - inline void clearPropagatedLiterals() { - d_theoryOut.d_propagatedLiterals.clear(); - } - - inline void newLemma(TNode node, bool negated, bool removable) { - // Remove the ITEs and assert to prop engine - std::vector<Node> additionalLemmas; - additionalLemmas.push_back(node); - RemoveITE::run(additionalLemmas); - d_propEngine->assertLemma(theory::Rewriter::rewrite(additionalLemmas[0]), negated, removable); - for (unsigned i = 1; i < additionalLemmas.size(); ++ i) { - d_propEngine->assertLemma(theory::Rewriter::rewrite(additionalLemmas[i]), false, removable); + void getPropagatedLiterals(std::vector<TNode>& literals) { + for (; d_propagatedLiteralsIndex < d_propagatedLiterals.size(); d_propagatedLiteralsIndex = d_propagatedLiteralsIndex + 1) { + literals.push_back(d_propagatedLiterals[d_propagatedLiteralsIndex]); } } - void propagate(); - Node getExplanation(TNode node, theory::Theory* theory); bool properConflict(TNode conflict) const; @@ -403,160 +471,49 @@ public: bool properExplanation(TNode node, TNode expl) const; inline Node getExplanation(TNode node) { - d_theoryOut.d_explanationNode = Node::null(); TNode atom = node.getKind() == kind::NOT ? node[0] : node; - theoryOf(atom)->explain(node); - Assert(!d_theoryOut.d_explanationNode.get().isNull()); + Node explanation = theoryOf(atom)->explain(node); + Assert(!explanation.isNull()); if(Dump.isOn("t-explanations")) { - Dump("t-explanations") - << CommentCommand(std::string("theory explanation from ") + - theoryOf(atom)->identify() + ": expect valid") << std::endl - << QueryCommand(d_theoryOut.d_explanationNode.get().impNode(node).toExpr()) - << std::endl; + Dump("t-explanations") << CommentCommand(std::string("theory explanation from ") + theoryOf(atom)->identify() + ": expect valid") << std::endl + << QueryCommand(explanation.impNode(node).toExpr()) << std::endl; } - Assert(properExplanation(node, d_theoryOut.d_explanationNode.get())); - return d_theoryOut.d_explanationNode; + Assert(properExplanation(node, explanation)); + return explanation; } Node getValue(TNode node); -private: - class Statistics { - public: - IntStat d_statConflicts, d_statPropagate, d_statLemma, d_statAugLemma, d_statExplanation; - Statistics(): - d_statConflicts("theory::conflicts", 0), - d_statPropagate("theory::propagate", 0), - d_statLemma("theory::lemma", 0), - d_statAugLemma("theory::aug_lemma", 0), - d_statExplanation("theory::explanation", 0) { - StatisticsRegistry::registerStat(&d_statConflicts); - StatisticsRegistry::registerStat(&d_statPropagate); - StatisticsRegistry::registerStat(&d_statLemma); - StatisticsRegistry::registerStat(&d_statAugLemma); - StatisticsRegistry::registerStat(&d_statExplanation); - } - - ~Statistics() { - StatisticsRegistry::unregisterStat(&d_statConflicts); - StatisticsRegistry::unregisterStat(&d_statPropagate); - StatisticsRegistry::unregisterStat(&d_statLemma); - StatisticsRegistry::unregisterStat(&d_statAugLemma); - StatisticsRegistry::unregisterStat(&d_statExplanation); - } - };/* class TheoryEngine::Statistics */ - Statistics d_statistics; - - /////////////////////////// - // Visitors - /////////////////////////// - /** - * Visitor that calls the apropriate theory to preregister the term. + * Get the theory associated to a given Node. + * + * @returns the theory, or NULL if the TNode is + * of built-in type. */ - class PreRegisterVisitor { - - /** The engine */ - TheoryEngine& d_engine; - - /** - * Cache from proprocessing of atoms. - */ - typedef context::CDMap<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap; - TNodeVisitedMap d_visited; - - /** - * All the theories of the visitation. - */ - theory::Theory::Set d_theories; - - std::string toString() const { - std::stringstream ss; - TNodeVisitedMap::const_iterator it = d_visited.begin(); - for (; it != d_visited.end(); ++ it) { - ss << (*it).first << ": " << theory::Theory::setToString((*it).second) << std::endl; - } - return ss.str(); - } - - public: - - PreRegisterVisitor(TheoryEngine& engine, context::Context* context): d_engine(engine), d_visited(context), d_theories(0){} - - bool alreadyVisited(TNode current, TNode parent) { - - Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ") => "; - - using namespace theory; - - TNodeVisitedMap::iterator find = d_visited.find(current); - - // If node is not visited at all, just return false - if (find == d_visited.end()) { - Debug("register::internal") << "1:false" << std::endl; - return false; - } - - Theory::Set theories = (*find).second; - - TheoryId currentTheoryId = Theory::theoryOf(current); - TheoryId parentTheoryId = Theory::theoryOf(parent); - - if (Theory::setContains(currentTheoryId, theories)) { - // The current theory has already visited it, so now it depends on the parent - Debug("register::internal") << (Theory::setContains(parentTheoryId, theories) ? "2:true" : "2:false") << std::endl; - return Theory::setContains(parentTheoryId, theories); - } else { - // If the current theory is not registered, it still needs to be visited - Debug("register::internal") << "2:false" << std::endl; - return false; - } - } - - void visit(TNode current, TNode parent) { - - Debug("register") << "PreRegisterVisitor::visit(" << current << "," << parent << ")" << std::endl; - Debug("register::internal") << toString() << std::endl; - - using namespace theory; - - // Get the theories of the terms - TheoryId currentTheoryId = Theory::theoryOf(current); - TheoryId parentTheoryId = Theory::theoryOf(parent); - - Theory::Set theories = d_visited[current]; - Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(theories) << std::endl; - if (!Theory::setContains(currentTheoryId, theories)) { - d_visited[current] = theories = Theory::setInsert(currentTheoryId, theories); - d_engine.theoryOf(currentTheoryId)->preRegisterTerm(current); - d_theories = Theory::setInsert(currentTheoryId, d_theories); - Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl; - } - if (!Theory::setContains(parentTheoryId, theories)) { - d_visited[current] = theories = Theory::setInsert(parentTheoryId, theories); - d_engine.theoryOf(parentTheoryId)->preRegisterTerm(current); - d_theories = Theory::setInsert(parentTheoryId, d_theories); - Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl; - } - Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(theories) << std::endl; - - Assert(d_visited.find(current) != d_visited.end()); - Assert(alreadyVisited(current, parent)); - } - - void start(TNode node) { - d_theories = 0; - } + inline theory::Theory* theoryOf(TNode node) { + return d_theoryTable[theory::Theory::theoryOf(node)]; + } - void done(TNode node) { - d_engine.markActive(d_theories); - } + /** + * Get the theory associated to a the given theory id. It will also mark the + * theory as currently active, we assume that theories are called only through + * theoryOf. + * + * @returns the theory, or NULL if the TNode is + * of built-in type. + */ + inline theory::Theory* theoryOf(theory::TheoryId theoryId) { + return d_theoryTable[theoryId]; + } - }; +private: /** Default visitor for pre-registration */ PreRegisterVisitor d_preRegistrationVisitor; + /** Visitor for collecting shared terms */ + SharedTermsVisitor d_sharedTermsVisitor; + };/* class TheoryEngine */ }/* CVC4 namespace */ diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index ec2405295..bcb1c46d7 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -71,27 +71,21 @@ public: void safePoint() throw(Interrupted, AssertionException) {} - void conflict(TNode n, bool safe = false) - throw(Interrupted, AssertionException) { + void conflict(TNode n) + throw(AssertionException) { push(CONFLICT, n); } - void propagate(TNode n, bool safe = false) - throw(Interrupted, AssertionException) { + void propagate(TNode n) + throw(AssertionException) { push(PROPAGATE, n); } - void lemma(TNode n, bool safe = false) throw(Interrupted, AssertionException) { + void lemma(TNode n, bool removable) throw(AssertionException) { push(LEMMA, n); } - void augmentingLemma(TNode n, bool safe = false) throw(Interrupted, AssertionException){ - push(AUG_LEMMA, n); - } - void explanation(TNode n, bool safe = false) throw(Interrupted, AssertionException) { - push(EXPLANATION, n); - } - void setIncomplete() throw(Interrupted, AssertionException) {} + void setIncomplete() throw(AssertionException) {} void clear() { d_callHistory.clear(); diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index 1f8643330..2de3715e1 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -7,7 +7,7 @@ theory THEORY_UF ::CVC4::theory::uf::TheoryUF "theory/uf/theory_uf.h" typechecker "theory/uf/theory_uf_type_rules.h" -properties stable-infinite +properties stable-infinite parametric properties check propagate staticLearning presolve rewriter ::CVC4::theory::uf::TheoryUfRewriter "theory/uf/theory_uf_rewriter.h" diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index b388dd1cb..84fad2f19 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -224,11 +224,11 @@ void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions) { d_equalityEngine.getExplanation(lhs, rhs, assumptions); } -void TheoryUF::explain(TNode literal) { +Node TheoryUF::explain(TNode literal) { Debug("uf") << "TheoryUF::explain(" << literal << ")" << std::endl; std::vector<TNode> assumptions; explain(literal, assumptions); - d_out->explanation(mkAnd(assumptions)); + return mkAnd(assumptions); } void TheoryUF::presolve() { diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index a3871f3a2..6cea8b85b 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -121,7 +121,7 @@ public: void check(Effort); void propagate(Effort); void preRegisterTerm(TNode term); - void explain(TNode n); + Node explain(TNode n); void staticLearning(TNode in, NodeBuilder<>& learned); void presolve(); diff --git a/src/util/node_visitor.h b/src/util/node_visitor.h index 1adc0ff20..06a1a83e8 100644 --- a/src/util/node_visitor.h +++ b/src/util/node_visitor.h @@ -50,7 +50,7 @@ public: /** * Performs the traversal. */ - static void run(Visitor& visitor, TNode node) { + static typename Visitor::return_type run(Visitor& visitor, TNode node) { // Notify of a start visitor.start(node); @@ -86,7 +86,7 @@ public: } // Notify that we're done - visitor.done(node); + return visitor.done(node); } }; |