From daf3b024547deaf1cf53b66ed046fbb15584b9d3 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Wed, 7 Jul 2010 02:18:42 +0000 Subject: [PATCH] Added shared term manager. Basic mechanism for identifying shared terms is working. Still need to implement theory-specific shared term propagation. --- src/prop/sat.h | 2 + src/theory/Makefile.am | 6 +- src/theory/arith/theory_arith.cpp | 4 +- src/theory/arith/theory_arith.h | 2 +- src/theory/arrays/theory_arrays.cpp | 21 ++- src/theory/arrays/theory_arrays.h | 4 +- src/theory/booleans/theory_bool.h | 4 +- src/theory/builtin/theory_builtin.h | 2 +- src/theory/bv/theory_bv.h | 4 +- src/theory/shared_data.cpp | 90 +++++++++++ src/theory/shared_data.h | 193 ++++++++++++++++++++++++ src/theory/shared_term_manager.cpp | 199 +++++++++++++++++++++++++ src/theory/shared_term_manager.h | 86 +++++++++++ src/theory/theory.h | 45 +++++- src/theory/theory_engine.cpp | 12 +- src/theory/theory_engine.h | 35 ++++- src/theory/uf/theory_uf.cpp | 4 +- src/theory/uf/theory_uf.h | 2 +- test/unit/theory/theory_arith_white.h | 2 +- test/unit/theory/theory_black.h | 2 +- test/unit/theory/theory_engine_white.h | 2 +- test/unit/theory/theory_uf_white.h | 2 +- 22 files changed, 689 insertions(+), 34 deletions(-) create mode 100644 src/theory/shared_data.cpp create mode 100644 src/theory/shared_data.h create mode 100644 src/theory/shared_term_manager.cpp create mode 100644 src/theory/shared_term_manager.h 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 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 nb; + set::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 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 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 @@ -135,6 +135,11 @@ private: */ Theory(); + /** + * A unique integer identifying the theory + */ + int d_id; + /** * The context for the Theory. */ @@ -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), @@ -195,13 +201,6 @@ protected: d_facts.clear(); } - /** - * Get the context associated to this Theory. - */ - context::Context* getContext() const { - return d_context; - } - /** * The output channel for the Theory. */ @@ -268,6 +267,20 @@ public: static bool standardEffortOnly(Effort e) { return e >= STANDARD && e < FULL_EFFORT; } 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. */ @@ -339,6 +352,22 @@ public: d_facts.push_back(n); } + /** + * 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. * 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 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 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(); 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 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()); } -- 2.30.2