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}
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();
}
/*_________________________________________________________________________________________________
}
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]));
}
}
}
}
-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;
void theoryPropagate(std::vector<SatLiteral>& output);
- void clearPropagatedLiterals();
-
void enqueueTheoryLiteral(const SatLiteral& l);
void setCnfStream(CnfStream* cnfStream);
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);
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 \
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 \
}
}
-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) {
void check(Effort e);
void propagate(Effort e);
- void explain(TNode n);
+ Node explain(TNode n);
void notifyEq(TNode lhs, TNode rhs);
// 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]);
// 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));
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;
return false;
}
-void TheoryArrays::explain(TNode n) {
+Node TheoryArrays::explain(TNode n) {
Trace("arrays")<<"Arrays::explain start for "<<n<<"\n";
}
Node reason = nb;
- d_out->explanation(reason);
+ return reason;
/*
context::CDMap<TNode, std::pair<TNode, TNode>, TNodeHashFunction>::const_iterator
*/
}
- void explain(TNode n);
+ Node explain(TNode n);
Node getValue(TNode n);
SolveStatus solve(TNode in, SubstitutionMap& outSubstitutions);
}
}
-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;
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);
}
void propagate(Effort e) { }
- void explain(TNode n);
+ Node explain(TNode n);
Node getValue(TNode n);
//if( conflict.getKind()!=kind::AND ){
// conflict = NodeManager::currentNM()->mkNode(kind::AND, conflict, conflict);
//}
- d_out->conflict( conflict, false );
+ d_out->conflict(conflict);
return;
}
}
theory_stable_infinite="false"
theory_finite="false"
theory_polite="false"
+theory_parametric="false"
rewriter_class=
rewriter_header=
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};
theory_stable_infinite="false"
theory_finite="false"
theory_polite="false"
+ theory_parametric="false"
rewriter_class=
rewriter_header=
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";;
* 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 */
+++ /dev/null
-/********************* */
-/*! \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);
-}
+++ /dev/null
-/********************* */
-/*! \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 */
+++ /dev/null
-/********************* */
-/*! \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 */
+++ /dev/null
-/********************* */
-/*! \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 */
--- /dev/null
+/********************* */
+/*! \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]);
+}
+
--- /dev/null
+/********************* */
+/*! \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();
+ }
+};
+
+}
+
--- /dev/null
+/********************* */
+/*! \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();
+}
--- /dev/null
+/********************* */
+/*! \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();
+};
+
+
+}
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 */
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).
*
Theory& operator=(const Theory&) CVC4_UNUSED;
/**
- * A unique integer identifying the theory
+ * An integer identifying the type of the theory
*/
TheoryId d_id;
* 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.
*/
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)
+ {
}
/**
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();
}
*
* @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();
}
MIN_EFFORT = 0,
QUICK_CHECK = 10,
STANDARD = 50,
- FULL_EFFORT = 100
+ FULL_EFFORT = 100,
+ COMBINATION = 150
};/* enum Effort */
// simple, useful predicates for effort values
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.
/**
* 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);
}
/**
*/
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
/**
* 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());
}
/** 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);
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 << "[";
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) {
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
}
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;
}
// 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
#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; \
} \
}
#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
#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
// 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();
}
}
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));
+ }
+ }
+ }
+ }
+}
#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"
// 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
/** 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];
/**
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;
/**
*/
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.
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
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;
}
/**
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 */
* 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));
}
/**
*/
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) {
*/
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.
*/
* 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.
*/
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.
*/
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;
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 */
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();
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"
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() {
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();
/**
* 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);
}
// Notify that we're done
- visitor.done(node);
+ return visitor.done(node);
}
};
# put it below in "TESTS +="
# Regression tests for SMT inputs
-SMT_TESTS = \
- pb_real_10_0100_10_10.smt \
- pb_real_10_0100_10_11.smt \
- pb_real_10_0100_10_15.smt \
- pb_real_10_0100_10_16.smt \
- pb_real_10_0100_10_19.smt \
- pb_real_10_0200_10_22.smt \
- pb_real_10_0200_10_26.smt \
- pb_real_10_0200_10_29.smt
+#SMT_TESTS = \
+# pb_real_10_0100_10_10.smt \
+# pb_real_10_0100_10_11.smt \
+# pb_real_10_0100_10_15.smt \
+# pb_real_10_0100_10_16.smt \
+# pb_real_10_0100_10_19.smt \
+# pb_real_10_0200_10_22.smt \
+# pb_real_10_0200_10_26.smt \
+# pb_real_10_0200_10_29.smt
# Regression tests for SMT2 inputs
SMT2_TESTS =
# All unit tests
UNIT_TESTS = \
- theory/shared_term_manager_black \
theory/theory_engine_white \
theory/theory_black \
theory/theory_arith_white \
theory/union_find_black \
expr/expr_public \
- expr/expr_manager_public \
+ expr/expr_manager_public \
expr/node_white \
expr/node_black \
expr/kind_black \
NodeManagerScope nms(d_nodeManager);
d_satSolver = new FakeSatSolver;
d_theoryEngine = new TheoryEngine(d_context);
- d_theoryEngine->addTheory<theory::builtin::TheoryBuiltin>();
- d_theoryEngine->addTheory<theory::booleans::TheoryBool>();
- d_theoryEngine->addTheory<theory::arith::TheoryArith>();
+ 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);
theory::Registrar registrar(d_theoryEngine);
d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, registrar);
}
+++ /dev/null
-/********************* */
-/*! \file shared_term_manager_black.h
- ** \verbatim
- ** Original author: barrett
- ** Major contributors: none
- ** Minor contributors (to current version): cconway, 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 Black box testing of CVC4::SharedTermManager.
- **
- ** Black box testing of CVC4::SharedTermManager.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include <iostream>
-#include <string>
-#include <deque>
-
-#include "theory/theory.h"
-#include "theory/theory_engine.h"
-#include "expr/node.h"
-#include "expr/node_manager.h"
-#include "expr/kind.h"
-#include "context/context.h"
-#include "util/rational.h"
-#include "util/integer.h"
-#include "util/options.h"
-#include "util/Assert.h"
-
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::expr;
-using namespace CVC4::context;
-using namespace CVC4::kind;
-
-using namespace std;
-
-/**
- * Test the SharedTermManager.
- */
-class SharedTermManagerBlack : public CxxTest::TestSuite {
- Context* d_ctxt;
-
- NodeManager* d_nm;
- NodeManagerScope* d_scope;
- TheoryEngine* d_theoryEngine;
-
-public:
-
- void setUp() {
- d_ctxt = new Context;
-
- d_nm = new NodeManager(d_ctxt, NULL);
- d_scope = new NodeManagerScope(d_nm);
-
- d_theoryEngine = new TheoryEngine(d_ctxt);
- }
-
- void tearDown() {
- d_theoryEngine->shutdown();
- delete d_theoryEngine;
-
- delete d_scope;
- delete d_nm;
-
- delete d_ctxt;
- }
-
- void testExplanation() {
- // Example from Barcelogic paper
- SharedTermManager* stm = d_theoryEngine->getSharedTermManager();
-
- Node x1 = d_nm->mkVar("x1", d_nm->integerType());
- Node x2 = d_nm->mkVar("x2", d_nm->integerType());
- Node x3 = d_nm->mkVar("x3", d_nm->integerType());
- Node x4 = d_nm->mkVar("x4", d_nm->integerType());
- Node x5 = d_nm->mkVar("x5", d_nm->integerType());
- Node x6 = d_nm->mkVar("x6", d_nm->integerType());
- Node x7 = d_nm->mkVar("x7", d_nm->integerType());
- Node x8 = d_nm->mkVar("x8", d_nm->integerType());
- Node x9 = d_nm->mkVar("x9", d_nm->integerType());
- Node x10 = d_nm->mkVar("x10", d_nm->integerType());
- Node x11 = d_nm->mkVar("x11", d_nm->integerType());
- Node x12 = d_nm->mkVar("x12", d_nm->integerType());
- Node x13 = d_nm->mkVar("x13", d_nm->integerType());
- Node x14 = d_nm->mkVar("x14", d_nm->integerType());
-
- Node a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12;
-
- d_ctxt->push();
-
- stm->addEq(a1 = d_nm->mkNode(EQUAL, x1, x8));
- stm->addEq(a2 = d_nm->mkNode(EQUAL, x7, x2));
- stm->addEq(a3 = d_nm->mkNode(EQUAL, x3, x13));
- stm->addEq(a4 = d_nm->mkNode(EQUAL, x7, x1));
- stm->addEq(a5 = d_nm->mkNode(EQUAL, x6, x7));
- stm->addEq(a6 = d_nm->mkNode(EQUAL, x9, x5));
- stm->addEq(a7 = d_nm->mkNode(EQUAL, x9, x3));
- stm->addEq(a8 = d_nm->mkNode(EQUAL, x14, x11));
- stm->addEq(a9 = d_nm->mkNode(EQUAL, x10, x4));
- stm->addEq(a10 = d_nm->mkNode(EQUAL, x12, x9));
- stm->addEq(a11 = d_nm->mkNode(EQUAL, x4, x11));
- stm->addEq(a12 = d_nm->mkNode(EQUAL, x10, x7));
-
- Node explanation = stm->explain(d_nm->mkNode(EQUAL, x1, x4));
-
- TS_ASSERT(explanation.getNumChildren() == 3);
-
- Node e0 = explanation[0];
- Node e1 = explanation[1];
- Node e2 = explanation[2];
-
- TS_ASSERT(e0 == a4 && e1 == a9 && e2 == a12);
-
- TS_ASSERT(stm->getRep(x8) == stm->getRep(x14));
- TS_ASSERT(stm->getRep(x2) != stm->getRep(x12));
-
- d_ctxt->pop();
-
- TS_ASSERT(stm->getRep(x8) != stm->getRep(x14));
-
- d_ctxt->push();
-
- stm->addEq(a1 = d_nm->mkNode(EQUAL, x1, x8));
- stm->addEq(a2 = d_nm->mkNode(EQUAL, x8, x2));
- stm->addEq(a3 = d_nm->mkNode(EQUAL, x2, x3));
-
- explanation = stm->explain(d_nm->mkNode(EQUAL, x1, x3));
- TS_ASSERT(explanation.getNumChildren() == 3);
-
- e0 = explanation[0];
- e1 = explanation[1];
- e2 = explanation[2];
-
- TS_ASSERT(e0 == a1 && e1 == a2 && e2 == a3);
-
- TS_ASSERT(stm->getRep(x8) == stm->getRep(x2));
-
- d_ctxt->pop();
- }
-
-};
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) {
- Unreachable();
- }
-
- void explanation(TNode n, bool safe = false)
- throw(Interrupted, AssertionException) {
- push(EXPLANATION, n);
- }
void setIncomplete()
- throw(Interrupted, AssertionException) {
+ throw(AssertionException) {
Unreachable();
}
void testOutputChannel() {
Node n = atom0.orNode(atom1);
- d_outputChannel.lemma(n);
+ d_outputChannel.lemma(n, false);
d_outputChannel.split(atom0);
Node s = atom0.orNode(atom0.notNode());
TS_ASSERT_EQUALS(d_outputChannel.d_callHistory.size(), 2u);
using namespace std;
class FakeOutputChannel : public OutputChannel {
- void conflict(TNode n, bool safe) throw(AssertionException) {
+ void conflict(TNode n) throw(AssertionException) {
Unimplemented();
}
- void propagate(TNode n, bool safe) throw(AssertionException) {
+ void propagate(TNode n) throw(AssertionException) {
Unimplemented();
}
- void lemma(TNode n, bool safe) throw(AssertionException) {
+ void lemma(TNode n, bool removable) throw(AssertionException) {
Unimplemented();
}
- void augmentingLemma(TNode n, bool safe) throw(AssertionException) {
- Unimplemented();
- }
- void explanation(TNode n, bool safe) throw(AssertionException) {
+ void explanation(TNode n) throw(AssertionException) {
Unimplemented();
}
void setIncomplete() throw(AssertionException) {
// create the TheoryEngine
d_theoryEngine = new TheoryEngine(d_ctxt);
- d_theoryEngine->addTheory< FakeTheory<THEORY_BUILTIN> >();
- d_theoryEngine->addTheory< FakeTheory<THEORY_BOOL> >();
- d_theoryEngine->addTheory< FakeTheory<THEORY_UF> >();
- d_theoryEngine->addTheory< FakeTheory<THEORY_ARITH> >();
- d_theoryEngine->addTheory< FakeTheory<THEORY_ARRAY> >();
- d_theoryEngine->addTheory< FakeTheory<THEORY_BV> >();
+ d_theoryEngine->addTheory< FakeTheory<THEORY_BUILTIN> >(THEORY_BUILTIN);
+ d_theoryEngine->addTheory< FakeTheory<THEORY_BOOL> >(THEORY_BOOL);
+ d_theoryEngine->addTheory< FakeTheory<THEORY_UF> >(THEORY_UF);
+ d_theoryEngine->addTheory< FakeTheory<THEORY_ARITH> >(THEORY_ARITH);
+ d_theoryEngine->addTheory< FakeTheory<THEORY_ARRAY> >(THEORY_ARRAY);
+ d_theoryEngine->addTheory< FakeTheory<THEORY_BV> >(THEORY_BV);
//Debug.on("theory-rewrite");
}
projects / cvc5.git / commitdiff