summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/prop/sat.h2
-rw-r--r--src/theory/Makefile.am6
-rw-r--r--src/theory/arith/theory_arith.cpp4
-rw-r--r--src/theory/arith/theory_arith.h2
-rw-r--r--src/theory/arrays/theory_arrays.cpp21
-rw-r--r--src/theory/arrays/theory_arrays.h4
-rw-r--r--src/theory/booleans/theory_bool.h4
-rw-r--r--src/theory/builtin/theory_builtin.h2
-rw-r--r--src/theory/bv/theory_bv.h4
-rw-r--r--src/theory/shared_data.cpp90
-rw-r--r--src/theory/shared_data.h193
-rw-r--r--src/theory/shared_term_manager.cpp199
-rw-r--r--src/theory/shared_term_manager.h86
-rw-r--r--src/theory/theory.h45
-rw-r--r--src/theory/theory_engine.cpp12
-rw-r--r--src/theory/theory_engine.h35
-rw-r--r--src/theory/uf/theory_uf.cpp4
-rw-r--r--src/theory/uf/theory_uf.h2
-rw-r--r--test/unit/theory/theory_arith_white.h2
-rw-r--r--test/unit/theory/theory_black.h2
-rw-r--r--test/unit/theory/theory_engine_white.h2
-rw-r--r--test/unit/theory/theory_uf_white.h2
22 files changed, 689 insertions, 34 deletions
diff --git a/src/prop/sat.h b/src/prop/sat.h
index c58a198b3..2e74a954c 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -97,6 +97,8 @@ inline std::string stringOfLiteralValue(SatLiteralValue val) {
*/
class SatInputInterface {
public:
+ /** Virtual destructor to make g++ happy */
+ virtual ~SatInputInterface() { }
/** Assert a clause in the solver. */
virtual void addClause(SatClause& clause, bool lemma) = 0;
/** Create a new boolean variable in the solver. */
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index ce15b86d4..c82968ef6 100644
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -12,7 +12,11 @@ libtheory_la_SOURCES = \
theory_engine.cpp \
theory_test_utils.h \
theory.h \
- theory.cpp
+ theory.cpp \
+ shared_term_manager.h \
+ shared_term_manager.cpp \
+ shared_data.h \
+ shared_data.cpp
nodist_libtheory_la_SOURCES = \
theoryof_table.h
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index f11f38ab4..21a86c345 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -50,8 +50,8 @@ using namespace CVC4::theory::arith;
-TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) :
- Theory(c, out),
+TheoryArith::TheoryArith(int id, context::Context* c, OutputChannel& out) :
+ Theory(id, c, out),
d_constants(NodeManager::currentNM()),
d_partialModel(c),
d_diseq(c),
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 7d9fd1136..7367f5726 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -99,7 +99,7 @@ private:
ArithUnatePropagator d_propagator;
public:
- TheoryArith(context::Context* c, OutputChannel& out);
+ TheoryArith(int id, context::Context* c, OutputChannel& out);
~TheoryArith();
/**
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index ab72a0a8c..b84b1e507 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -16,9 +16,11 @@
** Implementation of the theory of arrays.
**/
+
#include "theory/arrays/theory_arrays.h"
#include "expr/kind.h"
+
using namespace std;
using namespace CVC4;
using namespace CVC4::kind;
@@ -26,14 +28,29 @@ using namespace CVC4::context;
using namespace CVC4::theory;
using namespace CVC4::theory::arrays;
-TheoryArrays::TheoryArrays(Context* c, OutputChannel& out) :
- Theory(c, out)
+
+TheoryArrays::TheoryArrays(int id, Context* c, OutputChannel& out) :
+ Theory(id, c, out)
{
}
+
TheoryArrays::~TheoryArrays() {
}
+
+void TheoryArrays::addSharedTerm(TNode t) {
+ Debug("arrays") << "TheoryArrays::addSharedTerm(): "
+ << t << endl;
+}
+
+
+void TheoryArrays::notifyEq(TNode eq) {
+ Debug("arrays") << "TheoryArrays::notifyEq(): "
+ << eq << endl;
+}
+
+
void TheoryArrays::check(Effort e) {
while(!done()) {
Node assertion = get();
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index cf7f16f52..3cb050287 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -31,7 +31,7 @@ namespace arrays {
class TheoryArrays : public Theory {
public:
- TheoryArrays(context::Context* c, OutputChannel& out);
+ TheoryArrays(int id, context::Context* c, OutputChannel& out);
~TheoryArrays();
void preRegisterTerm(TNode n) { }
void registerTerm(TNode n) { }
@@ -48,6 +48,8 @@ public:
return RewriteComplete(in);
}
+ void addSharedTerm(TNode t);
+ void notifyEq(TNode eq);
void check(Effort e);
void propagate(Effort e) { }
void explain(TNode n, Effort e) { }
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index 512dfebcc..4d8620146 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -30,8 +30,8 @@ namespace booleans {
class TheoryBool : public Theory {
public:
- TheoryBool(context::Context* c, OutputChannel& out) :
- Theory(c, out) {
+ TheoryBool(int id, context::Context* c, OutputChannel& out) :
+ Theory(id, c, out) {
}
void preRegisterTerm(TNode n) {
diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
index 20b6b038b..e76b3fb4b 100644
--- a/src/theory/builtin/theory_builtin.h
+++ b/src/theory/builtin/theory_builtin.h
@@ -32,7 +32,7 @@ class TheoryBuiltin : public Theory {
static Node blastDistinct(TNode in);
public:
- TheoryBuiltin(context::Context* c, OutputChannel& out) : Theory(c, out) { }
+ TheoryBuiltin(int id, context::Context* c, OutputChannel& out) : Theory(id, c, out) { }
~TheoryBuiltin() { }
void preRegisterTerm(TNode n) { Unreachable(); }
void registerTerm(TNode n) { Unreachable(); }
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 4d2f502fd..537e7f5fe 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -30,8 +30,8 @@ namespace bv {
class TheoryBV : public Theory {
public:
- TheoryBV(context::Context* c, OutputChannel& out) :
- Theory(c, out) {
+ TheoryBV(int id, context::Context* c, OutputChannel& out) :
+ Theory(id, c, out) {
}
void preRegisterTerm(TNode n) { Unimplemented(); }
diff --git a/src/theory/shared_data.cpp b/src/theory/shared_data.cpp
new file mode 100644
index 000000000..678595f5f
--- /dev/null
+++ b/src/theory/shared_data.cpp
@@ -0,0 +1,90 @@
+/********************* */
+/*! \file shared_data.cpp
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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 equivalence class data for UF theory.
+ **
+ ** Implementation of equivalence class data for UF theory. 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_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_equality = data->d_equality;
+ 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;
+ Node equality = d_equality;
+ Theory* explainingTheory = d_explainingTheory;
+
+ makeCurrent();
+ d_proofNext = this;
+
+ Node tmpNode;
+ Theory* tmpTheory;
+ SharedData* tmpData;
+
+ while (!current->isProofRoot()) {
+ tmpNode = current->getEquality();
+ current->setEquality(equality);
+ equality = tmpNode;
+
+ tmpTheory = current->getExplainingTheory();
+ current->setExplainingTheory(explainingTheory);
+ explainingTheory = tmpTheory;
+
+ tmpData = current->getProofNext();
+ current->setProofNext(parent);
+ parent = current;
+ current = tmpData;
+ }
+ current->setEquality(equality);
+ current->setExplainingTheory(explainingTheory);
+ current->setProofNext(parent);
+}
diff --git a/src/theory/shared_data.h b/src/theory/shared_data.h
new file mode 100644
index 000000000..d8ed63387
--- /dev/null
+++ b/src/theory/shared_data.h
@@ -0,0 +1,193 @@
+/********************* */
+/*! \file shared_data.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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 equivalence class datastructure for nodes.
+ **
+ ** Context dependent equivalence class datastructure for nodes.
+ ** Currently keeps a context dependent watch list.
+ **/
+
+#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;
+
+ /**
+ * The equality that justifies this node being equal to
+ * the node at d_proofNext. Not valid if this is proof root.
+ */
+ Node d_equality;
+
+ /**
+ * The theory that can explain d_equality. 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 equality associated with the link in the proof tree.
+ */
+ Node getEquality() const { return d_equality; }
+
+ /**
+ * Set the equality associated with the link in the proof tree.
+ */
+ void setEquality(TNode eq) { makeCurrent(); d_equality = eq; }
+
+ /**
+ * Get the explaining theory
+ */
+ theory::Theory* getExplainingTheory() const { return d_explainingTheory; }
+
+ /**
+ * Set the explaining theory
+ */
+ void setExplainingTheory(theory::Theory* t) { makeCurrent(); d_explainingTheory = t; }
+
+ /**
+ * Get the shared term associated with this data
+ */
+ Node getRep() const { return d_rep; }
+
+ /**
+ * Reverse the edges in the proof tree from here to the root.
+ */
+ void reverseEdges();
+
+};/* class SharedData */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__SHARED_DATA_H */
diff --git a/src/theory/shared_term_manager.cpp b/src/theory/shared_term_manager.cpp
new file mode 100644
index 000000000..55087ecbd
--- /dev/null
+++ b/src/theory/shared_term_manager.cpp
@@ -0,0 +1,199 @@
+/********************* */
+/*! \file shared_term_manager.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 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) {
+ SharedData* next = pData->getFind();
+ if (next == pData) return pData;
+ SharedData* nextNext = next->getFind();
+ if (nextNext == next) return next;
+ 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 newTags = parentTag | childTag;
+ SharedData* pData;
+ if(n.getAttribute(SharedAttr(), pData)) {
+ // The attribute already exists, just update it if necessary
+ uint64_t tags = pData->getTheories();
+ newTags |= tags;
+ if (tags == newTags) return;
+ if (!(tags & parentTag)) {
+ parent->addSharedTerm(n);
+ }
+ if (!(tags & childTag)) {
+ child->addSharedTerm(n);
+ }
+ pData->setTheories(newTags);
+ } else {
+ // The attribute does not exist, so it is created and set
+ pData = new (true) SharedData(d_context, n, newTags);
+ n.setAttribute(SharedAttr(), pData);
+ parent->addSharedTerm(n);
+ child->addSharedTerm(n);
+ }
+}
+
+
+void SharedTermManager::addEq(Theory* thReason, TNode eq) {
+ Assert(eq.getKind() == kind::EQUAL &&
+ eq[0].hasAttribute(SharedAttr()) && eq[1].hasAttribute(SharedAttr()),
+ "SharedTermManager::addEq precondition violated");
+
+ TNode x = eq[0];
+ TNode y = eq[1];
+
+ SharedData* pDataX = x.getAttribute(SharedAttr());
+ SharedData* pDataY = y.getAttribute(SharedAttr());
+
+ SharedData* pDataXX = find(pDataX);
+ SharedData* pDataYY = find(pDataY);
+
+ if(pDataXX == pDataYY) return;
+
+ if(pDataXX->getSize() > pDataYY->getSize()) {
+ SharedData* tmp = pDataXX;
+ pDataXX = pDataYY;
+ pDataYY = tmp;
+
+ tmp = pDataX;
+ pDataX = pDataY;
+ pDataY = tmp;
+ }
+
+ pDataX->reverseEdges();
+ pDataX->setEquality(eq);
+ pDataX->setExplainingTheory(thReason);
+ pDataX->setProofNext(pDataY);
+
+ pDataXX->setFind(pDataYY);
+ pDataYY->setSize(pDataYY->getSize() + pDataXX->getSize());
+ uint64_t tags = pDataXX->getTheories();
+ pDataYY->setTheories(pDataYY->getTheories() | tags);
+ int id = 0;
+ while (tags != 0) {
+ if (tags & 1) {
+ d_theories[id]->notifyEq(pDataXX->getRep(), pDataYY->getRep());
+ }
+ tags = tags >> 1;
+ ++id;
+ }
+}
+
+
+// Explain this equality
+Node SharedTermManager::explain(TNode eq) {
+ 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];
+
+ SharedData* pDataX = x.getAttribute(SharedAttr());
+ SharedData* pDataY = y.getAttribute(SharedAttr());
+
+ Assert(find(pDataX) == find(pDataY),
+ "invalid equality input to SharedTermManager::explain");
+
+ std::set<Node> s;
+ Node n;
+ 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) {
+ n = d_engine->getExplanation(pDataX->getEquality(),
+ pDataX->getExplainingTheory());
+ for (Node::iterator it = n.begin(), iend = n.end(); it != iend; ++it) {
+ s.insert(*it);
+ }
+ 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) {
+ n = d_engine->getExplanation(pDataY->getEquality(),
+ pDataY->getExplainingTheory());
+ for (Node::iterator it = n.begin(), iend = n.end(); it != iend; ++it) {
+ s.insert(*it);
+ }
+ pDataY = pDataY->getProofNext();
+ }
+ }
+ if (pDataX != pDataY) {
+ // X and Y are on different branches - have to traverse both
+ while (!pDataX->isProofRoot()) {
+ n = d_engine->getExplanation(pDataX->getEquality(),
+ pDataX->getExplainingTheory());
+ for (Node::iterator it = n.begin(), iend = n.end(); it != iend; ++it) {
+ s.insert(*it);
+ }
+ pDataX = pDataX->getProofNext();
+ }
+ }
+
+ // Build explanation from s
+ NodeBuilder<kind::AND> nb;
+ set<Node>::iterator it = s.begin(), iend = s.end();
+ for (; it != iend; ++it) {
+ nb << *it;
+ }
+ return nb.constructNode();
+}
+
+
+}/* CVC4 namespace */
diff --git a/src/theory/shared_term_manager.h b/src/theory/shared_term_manager.h
new file mode 100644
index 000000000..e6a58cdc9
--- /dev/null
+++ b/src/theory/shared_term_manager.h
@@ -0,0 +1,86 @@
+/********************* */
+/*! \file shared_term_manager.h
+ ** \verbatim
+ ** Original author: barrett
+ ** Major contributors:
+ ** Minor contributors (to current version):
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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 "expr/node.h"
+#include "theory/shared_data.h"
+
+namespace CVC4 {
+
+namespace context {
+ class Context;
+}
+
+namespace theory {
+ class Theory;
+}
+
+/**
+ * Manages shared terms
+ */
+class SharedTermManager {
+
+ TheoryEngine* d_engine;
+
+ context::Context* d_context;
+
+ std::vector<theory::Theory*> d_theories;
+
+ SharedData* find(SharedData* pData);
+
+public:
+ SharedTermManager(TheoryEngine* engine, context::Context* context);
+
+ void registerTheory(theory::Theory* th);
+
+ void addTerm(TNode n, theory::Theory* parent,
+ theory::Theory* child);
+
+ void addEq(theory::Theory* thReason, TNode eq);
+
+ Node explain(TNode eq);
+
+};/* class SharedTermManager */
+
+/**
+ * Cleanup function for SharedData. This will be called whenever
+ * a SharedAttr is being destructed.
+ */
+struct SharedDataCleanupStrategy {
+ static void cleanup(SharedData* sd) {
+ sd->deleteSelf();
+ }
+};/* struct SharedDataCleanupStrategy */
+
+/** Unique name to use for constructing ECAttr. */
+struct SharedAttrTag {};
+
+/**
+ * SharedAttr is the attribute that maps a node to its SharedData.
+ */
+typedef expr::Attribute<SharedAttrTag, SharedData*,
+ SharedDataCleanupStrategy> SharedAttr;
+
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__SHARED_TERM_MANAGER_H */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index bcb2d011b..6da47fbd8 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -136,6 +136,11 @@ private:
Theory();
/**
+ * A unique integer identifying the theory
+ */
+ int d_id;
+
+ /**
* The context for the Theory.
*/
context::Context* d_context;
@@ -175,7 +180,8 @@ protected:
/**
* Construct a Theory.
*/
- Theory(context::Context* ctxt, OutputChannel& out) throw() :
+ Theory(int id, context::Context* ctxt, OutputChannel& out) throw() :
+ d_id(id),
d_context(ctxt),
d_facts(),
d_factsResetter(*this),
@@ -196,13 +202,6 @@ protected:
}
/**
- * Get the context associated to this Theory.
- */
- context::Context* getContext() const {
- return d_context;
- }
-
- /**
* The output channel for the Theory.
*/
OutputChannel* d_out;
@@ -269,6 +268,20 @@ public:
static bool fullEffort(Effort e) { return e >= FULL_EFFORT; }
/**
+ * Get the id for this Theory.
+ */
+ int getId() const {
+ return d_id;
+ }
+
+ /**
+ * Get the context associated to this Theory.
+ */
+ context::Context* getContext() const {
+ return d_context;
+ }
+
+ /**
* Set the output channel associated to this theory.
*/
void setOutputChannel(OutputChannel& out) {
@@ -340,6 +353,22 @@ public:
}
/**
+ * This method is called to notify a theory that the node n should be considered a "shared term" by this theory
+ */
+ virtual void addSharedTerm(TNode n) { }
+
+ /**
+ * This method is called by the shared term manager when a shared term t
+ * which this theory cares about (either because it received a previous
+ * addSharedTerm call with t or because it received a previous notifyEq call
+ * with t as the second argument) becomes equal to another shared term u.
+ * This call also serves as notice to the theory that the shared term manager
+ * now considers u the representative for this equivalence class of shared
+ * terms, so future notifications for this class will be based on u not t.
+ */
+ virtual void notifyEq(TNode t, TNode u) { }
+
+ /**
* Check the current assignment's consistency.
*
* An implementation of check() is required to either:
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 839add67c..d16d80090 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -42,6 +42,11 @@ typedef expr::Attribute<IteRewriteTag, Node> IteRewriteAttr;
}/* CVC4::theory namespace */
void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
+ //FIXME: Assert(fact.isLiteral(), "expected literal");
+ if (fact.getKind() == kind::NOT) {
+ // No need to register negations - only atoms
+ fact = fact[0];
+ }
if(! fact.getAttribute(RegisteredAttr())) {
std::list<TNode> toReg;
toReg.push_back(fact);
@@ -56,6 +61,7 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
++workp) {
TNode n = *workp;
+ Theory* thParent = d_engine->theoryOf(n);
// I don't think we need to register operators @CB
@@ -74,11 +80,15 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
TNode c = *i;
+ Theory* thChild = d_engine->theoryOf(c);
+ if (thParent != thChild) {
+ d_engine->getSharedTermManager()->addTerm(c, thParent, thChild);
+ }
if(! c.getAttribute(RegisteredAttr())) {
if(c.getNumChildren() == 0) {
c.setAttribute(RegisteredAttr(), true);
- d_engine->theoryOf(c)->registerTerm(c);
+ thChild->registerTerm(c);
} else {
toReg.push_back(c);
}
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index f467d0d8f..bb9131023 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -26,6 +26,7 @@
#include "theory/theoryof_table.h"
#include "prop/prop_engine.h"
+#include "theory/shared_term_manager.h"
#include "theory/builtin/theory_builtin.h"
#include "theory/booleans/theory_bool.h"
#include "theory/uf/theory_uf.h"
@@ -122,6 +123,9 @@ class TheoryEngine {
EngineOutputChannel d_theoryOut;
+ /** Pointer to Shared Term Manager */
+ SharedTermManager* d_sharedTermManager;
+
theory::builtin::TheoryBuiltin d_builtin;
theory::booleans::TheoryBool d_bool;
theory::uf::TheoryUF d_uf;
@@ -192,14 +196,23 @@ public:
TheoryEngine(context::Context* ctxt) :
d_propEngine(NULL),
d_theoryOut(this, ctxt),
- d_builtin(ctxt, d_theoryOut),
- d_bool(ctxt, d_theoryOut),
- d_uf(ctxt, d_theoryOut),
- d_arith(ctxt, d_theoryOut),
- d_arrays(ctxt, d_theoryOut),
- d_bv(ctxt, d_theoryOut),
+ d_builtin(0, ctxt, d_theoryOut),
+ d_bool(1, ctxt, d_theoryOut),
+ d_uf(2, ctxt, d_theoryOut),
+ d_arith(3, ctxt, d_theoryOut),
+ d_arrays(4, ctxt, d_theoryOut),
+ d_bv(5, ctxt, d_theoryOut),
d_statistics() {
+ d_sharedTermManager = new SharedTermManager(this, ctxt);
+
+ d_sharedTermManager->registerTheory(&d_builtin);
+ d_sharedTermManager->registerTheory(&d_bool);
+ d_sharedTermManager->registerTheory(&d_uf);
+ d_sharedTermManager->registerTheory(&d_arith);
+ d_sharedTermManager->registerTheory(&d_arrays);
+ d_sharedTermManager->registerTheory(&d_bv);
+
d_theoryOfTable.registerTheory(&d_builtin);
d_theoryOfTable.registerTheory(&d_bool);
d_theoryOfTable.registerTheory(&d_uf);
@@ -208,6 +221,10 @@ public:
d_theoryOfTable.registerTheory(&d_bv);
}
+ SharedTermManager* getSharedTermManager() {
+ return d_sharedTermManager;
+ }
+
void setPropEngine(prop::PropEngine* propEngine)
{
Assert(d_propEngine == NULL);
@@ -226,6 +243,7 @@ public:
d_arith.shutdown();
d_arrays.shutdown();
d_bv.shutdown();
+ delete d_sharedTermManager;
}
/**
@@ -314,6 +332,11 @@ public:
//d_bv.propagate(theory::Theory::FULL_EFFORT);
}
+ inline Node getExplanation(TNode node, theory::Theory* theory) {
+ theory->explain(node);
+ return d_theoryOut.d_explanationNode;
+ }
+
inline Node getExplanation(TNode node){
d_theoryOut.d_explanationNode = Node::null();
theory::Theory* theory =
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index f440c3d0f..9060568b2 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -26,8 +26,8 @@ using namespace CVC4::context;
using namespace CVC4::theory;
using namespace CVC4::theory::uf;
-TheoryUF::TheoryUF(Context* c, OutputChannel& out) :
- Theory(c, out),
+TheoryUF::TheoryUF(int id, Context* c, OutputChannel& out) :
+ Theory(id, c, out),
d_assertions(c),
d_pending(c),
d_currentPendingIdx(c,0),
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 091fc5156..f0be0668a 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -84,7 +84,7 @@ private:
public:
/** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
- TheoryUF(context::Context* c, OutputChannel& out);
+ TheoryUF(int id, context::Context* c, OutputChannel& out);
/** Destructor for the TheoryUF object. */
~TheoryUF();
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index d8c41bf3a..ea1ee698f 100644
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -70,7 +70,7 @@ public:
d_nm = new NodeManager(d_ctxt);
d_scope = new NodeManagerScope(d_nm);
d_outputChannel.clear();
- d_arith = new TheoryArith(d_ctxt, d_outputChannel);
+ d_arith = new TheoryArith(0, d_ctxt, d_outputChannel);
preregistered = new std::set<Node>();
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 967a53462..0c6a38d0b 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -95,7 +95,7 @@ public:
vector<Node> d_getSequence;
DummyTheory(Context* ctxt, OutputChannel& out) :
- Theory(ctxt, out) {
+ Theory(0, ctxt, out) {
}
void registerTerm(TNode n) {
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index addf15af3..570fa74a4 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -80,7 +80,7 @@ class FakeTheory : public Theory {
public:
FakeTheory(context::Context* ctxt, OutputChannel& out, std::string id) :
- Theory(ctxt, out),
+ Theory(0, ctxt, out),
d_id(id) {
}
diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_white.h
index a959d01ba..8e72c428f 100644
--- a/test/unit/theory/theory_uf_white.h
+++ b/test/unit/theory/theory_uf_white.h
@@ -59,7 +59,7 @@ public:
d_nm = new NodeManager(d_ctxt);
d_scope = new NodeManagerScope(d_nm);
d_outputChannel.clear();
- d_euf = new TheoryUF(d_ctxt, d_outputChannel);
+ d_euf = new TheoryUF(0, d_ctxt, d_outputChannel);
d_booleanType = new TypeNode(d_nm->booleanType());
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback