From 21e0c5dd0de5edef8ec12f48b76887109b67db52 Mon Sep 17 00:00:00 2001 From: Tim King Date: Wed, 17 Feb 2010 21:29:57 +0000 Subject: [PATCH] Initial draft of TheoryUF. Should compile without problems. A decent amount of functionality is stubbed out. Still needs a bit of cleanup. --- src/context/context.h | 5 ++ src/theory/theory.h | 14 ++++ src/theory/uf/Makefile.am | 6 +- src/theory/uf/ecdata.cpp | 105 ++++++++++++++++++++++++++ src/theory/uf/ecdata.h | 147 ++++++++++++++++++++++++++++++++++++ src/theory/uf/theory_uf.cpp | 138 +++++++++++++++++++++++++++++++++ src/theory/uf/theory_uf.h | 47 ++++++++++++ 7 files changed, 461 insertions(+), 1 deletion(-) create mode 100644 src/theory/uf/ecdata.cpp create mode 100644 src/theory/uf/ecdata.h create mode 100644 src/theory/uf/theory_uf.cpp create mode 100644 src/theory/uf/theory_uf.h diff --git a/src/context/context.h b/src/context/context.h index ff40542d1..1af4480f9 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -101,6 +101,11 @@ public: */ int getLevel() const { return ((int)d_scopeList.size()) - 1; } + /** + * Return the ContextMemoryManager associated with the context. + */ + ContextMemoryManager* getCMM(){ return d_pCMM; } + /** * Save the current state, create a new Scope */ diff --git a/src/theory/theory.h b/src/theory/theory.h index 8aa76ea81..8b83f71cf 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -18,6 +18,7 @@ #include "expr/node.h" #include "theory/output_channel.h" +#include "context/context.h" namespace CVC4 { namespace theory { @@ -101,6 +102,19 @@ public: const Node& n, Effort level = FULL_EFFORT) = 0; +protected: + /** + * Returns the next atom in the assertFact() queue. + * Guarentees that registerTerm is called on the theory specific subterms. + * @return the next atom in the assertFact() queue. + */ + Node get(); + + /** + * Returns true if the assertFactQueue is empty + */ + bool done() { return true; } + };/* class Theory */ }/* CVC4::theory namespace */ diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am index 7895803a6..537b8b124 100644 --- a/src/theory/uf/Makefile.am +++ b/src/theory/uf/Makefile.am @@ -5,6 +5,10 @@ AM_CXXFLAGS = -Wall -fvisibility=hidden noinst_LTLIBRARIES = libuf.la -libuf_la_SOURCES = +libuf_la_SOURCES = \ + ecdata.h \ + ecdata.cpp \ + theory_uf.h \ + theory_uf.cpp EXTRA_DIST = kinds diff --git a/src/theory/uf/ecdata.cpp b/src/theory/uf/ecdata.cpp new file mode 100644 index 000000000..a22faf61e --- /dev/null +++ b/src/theory/uf/ecdata.cpp @@ -0,0 +1,105 @@ +#include "theory/uf/ecdata.h" + +using namespace CVC4; +using namespace context; +using namespace theory; + + +ECData::ECData(Context * context, const Node & n) : + ContextObj(context), + find(this), + rep(n), + watchListSize(0), + first(NULL), + last(NULL) +{} + + +bool ECData::isClassRep(){ + return this == this->find; +} + +void ECData::addPredecessor(Node n, Context* context){ + Assert(isClassRep()); + + makeCurrent(); + + Link * newPred = new (context->getCMM()) Link(context, n, first); + first = newPred; + if(last == NULL){ + last = newPred; + } + + ++watchListSize; +} + +ContextObj* ECData::save(ContextMemoryManager* pCMM) { + return new(pCMM) ECData(*this); +} + +void ECData::restore(ContextObj* pContextObj) { + *this = *((ECData*)pContextObj); +} + +Node ECData::getRep(){ + return rep; +} + +unsigned ECData::getWatchListSize(){ + return watchListSize; +} + +void ECData::setWatchListSize(unsigned newSize){ + Assert(isClassRep()); + + makeCurrent(); + watchListSize = newSize; +} + +void ECData::setFind(ECData * ec){ + makeCurrent(); + find = ec; +} + +ECData * ECData::getFind(){ + return find; +} + + +Link* ECData::getFirst(){ + return first; +} + + +Link* ECData::getLast(){ + return last; +} + +void ECData::setFirst(Link * nfirst){ + makeCurrent(); + first = nfirst; +} + +void ECData::setLast(Link * nlast){ + makeCurrent(); + last = nlast; +} + + +void ECData::takeOverDescendantWatchList(ECData * nslave, ECData * nmaster){ + Assert(nslave != nmaster); + Assert(nslave->getFind() == nmaster ); + + nmaster->makeCurrent(); + + nmaster->watchListSize += nslave->watchListSize; + + if(nmaster->first == NULL){ + nmaster->first = nslave->first; + nmaster->last = nslave->last; + }else if(nslave->first != NULL){ + Link * currLast = nmaster->last; + currLast->next = nslave->first; + nmaster->last = nslave->last; + } +} diff --git a/src/theory/uf/ecdata.h b/src/theory/uf/ecdata.h new file mode 100644 index 000000000..fd0855bee --- /dev/null +++ b/src/theory/uf/ecdata.h @@ -0,0 +1,147 @@ +/********************* */ +/** ecdata.h + ** Original author: taking + ** Major contributors: barrett + ** 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. + ** + ** Context dependent equivalence class datastructure for nodes. + ** Currently keeps a context dependent watch list. + **/ + +#ifndef __CVC4__THEORY__UF__ECDATA_H +#define __CVC4__THEORY__UF__ECDATA_H + +#include "expr/node.h" +#include "context/context.h" +#include "context/context_mm.h" + +namespace CVC4 { +namespace theory { + +struct Link { + context::CDO< Link* > next; + + //TODO soft reference + Node data; + + Link(context::Context* context, Node n, Link * l = NULL): + next(context, l), data(n) + {} + + static void* operator new(size_t size, context::ContextMemoryManager* pCMM) { + return pCMM->newData(size); + } + +}; + + + +class ECData : public context::ContextObj { +private: + ECData * find; + + Node rep; + + unsigned watchListSize; + Link * first; + Link * last; + + + context::ContextObj* save(context::ContextMemoryManager* pCMM); + void restore(context::ContextObj* pContextObj); + + +public: + /** + * Returns true if this ECData object is the current representative of + * the equivalence class. + */ + bool isClassRep(); + + /** + * Adds a node to the watch list of the equivalence class. + * Requires a context to do memory management. + * @param n the node to be added. + * @pre isClassRep() == true + */ + void addPredecessor(Node n, context::Context* context); + + + + /** + * Creates a EQ with the representative n + * @param context the context to associate with this ecdata. + * This is required as ECData is context dependent + * @param n the node that corresponds to this ECData + */ + ECData(context::Context* context, const Node & n); + + static void takeOverDescendantWatchList(ECData * nslave, ECData * nmaster); + + static ECData * ccFind(ECData * fp); + + + /** + * Returns the representative of this ECData. + */ + Node getRep(); + + /** + * Returns the size of the equivalence class. + */ + unsigned getWatchListSize(); + + /** + * Returns a pointer the first member of the watch list. + */ + Link* getFirst(); + + + /** + * Returns the find pointer of the ECData. + * If isClassRep(), then getFind() == this + */ + ECData* getFind(); + + + /** + * @pre isClassRep() == true + * @pre ec->isClassRep() == true + * @post isClassRep() == false + * @post ec->isClassRep() == true + */ + void setFind(ECData * ec); + +private: + + + /** + * @pre isClassRep() == true + */ + void setWatchListSize(unsigned newSize); + + /** + * @pre isClassRep() == true + */ + void setFirst(Link * nfirst); + + Link* getLast(); + + /** + * @pre isClassRep() == true + */ + void setLast(Link * nlast); + +}; /* class ECData */ + +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + + +#endif /* __CVC4__THEORY__UF__ECDATA_H */ diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp new file mode 100644 index 000000000..840c7b51e --- /dev/null +++ b/src/theory/uf/theory_uf.cpp @@ -0,0 +1,138 @@ + +#include "theory/uf/theory_uf.h" +#include "theory/uf/ecdata.h" +#include "expr/kind.h" + +using namespace CVC4; +using namespace theory; +using namespace context; + + +/* Temporaries to facilitate compiling. */ +enum TmpEnum {EC}; +void setAttribute(Node n, TmpEnum te, ECData * ec){} +ECData* getAttribute(Node n, TmpEnum te) { return NULL; } +Node getOperator(Node x) { return Node::null(); } + + +void TheoryUF::setup(const Node& n){ + ECData * ecN = new (true) ECData(d_context, n); + + //TODO Make sure attribute manager owns the pointer + setAttribute(n, EC, ecN); + + if(n.getKind() == APPLY){ + for(Node::iterator cIter = n.begin(); cIter != n.end(); ++cIter){ + Node child = *cIter; + + ECData * ecChild = getAttribute(child, EC); + ecChild = ccFind(ecChild); + + ecChild->addPredecessor(n, d_context); + } + } +} + +bool TheoryUF::equiv(Node x, Node y){ + if(x.getNumChildren() != y.getNumChildren()) + return false; + + if(getOperator(x) != getOperator(y)) + return false; + + Node::iterator xIter = x.begin(); + Node::iterator yIter = y.begin(); + + while(xIter != x.end()){ + + if(ccFind(getAttribute(*xIter, EC)) != + ccFind(getAttribute(*yIter, EC))) + return false; + + ++xIter; + ++yIter; + } + return true; +} + +ECData* TheoryUF::ccFind(ECData * x){ + if( x->getFind() == x) + return x; + else{ + return ccFind(x->getFind()); + } +} + +void TheoryUF::ccUnion(ECData* ecX, ECData* ecY){ + ECData* nslave; + ECData* nmaster; + + if(ecX->getWatchListSize() <= ecY->getWatchListSize()){ + nslave = ecX; + nmaster = ecY; + }else{ + nslave = ecY; + nmaster = ecX; + } + + nslave->setFind(nmaster); + + for(Link* Px = nmaster->getFirst(); Px != NULL; Px = Px->next ){ + for(Link* Py = nslave->getFirst(); Py != NULL; Py = Py->next ){ + if(equiv(Px->data,Py->data)){ + d_pending.push_back((Px->data).eqExpr(Py->data)); + } + } + } + + ECData::takeOverDescendantWatchList(nslave, nmaster); +} + +//TODO make parameters soft references +void TheoryUF::merge(){ + do{ + Node assertion = d_pending[d_currentPendingIdx]; + d_currentPendingIdx = d_currentPendingIdx + 1; + + Node x = assertion[0]; + Node y = assertion[1]; + + ECData* ecX = ccFind(getAttribute(x, EC)); + ECData* ecY = ccFind(getAttribute(y, EC)); + + if(ecX == ecY) + continue; + + ccUnion(ecX, ecY); + }while( d_currentPendingIdx < d_pending.size() ); +} + +void TheoryUF::check(OutputChannel& out, Effort level){ + while(!done()){ + Node assertion = get(); + + + switch(assertion.getKind()){ + case EQUAL: + d_pending.push_back(assertion); + merge(); + break; + case NOT: + d_disequality.push_back(assertion[0]); + break; + default: + Unreachable(); + } + } + if(fullEffort(level)){ + for(CDList::const_iterator diseqIter = d_disequality.begin(); + diseqIter != d_disequality.end(); + ++diseqIter){ + + if(ccFind(getAttribute((*diseqIter)[0], EC)) == + ccFind(getAttribute((*diseqIter)[1], EC))){ + out.conflict(*diseqIter, true); + } + } + } +} diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h new file mode 100644 index 000000000..06b0ee4f8 --- /dev/null +++ b/src/theory/uf/theory_uf.h @@ -0,0 +1,47 @@ + +#ifndef __CVC4__THEORY__THEORY_UF_H +#define __CVC4__THEORY__THEORY_UF_H + +#include "expr/node.h" +#include "theory/theory.h" +#include "theory/output_channel.h" +#include "context/context.h" +#include "theory/uf/ecdata.h" + +namespace CVC4 { +namespace theory { + +class TheoryUF : public Theory { +private: + context::Context* d_context; + context::CDList d_pending; + context::CDList d_disequality; + context::CDO d_currentPendingIdx; + +public: + void setup(const Node& n); + + void check(OutputChannel& out, Effort level= FULL_EFFORT); + + void propagate(OutputChannel& out, Effort level= FULL_EFFORT){} + + void explain(OutputChannel& out, + const Node& n, + Effort level = FULL_EFFORT){} + +private: + bool equiv(Node x, Node y); + void ccUnion(ECData* ecX, ECData* ecY); + ECData* ccFind(ECData* x); + + void merge(); + //TODO put back in theory + + +}; + +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ + + +#endif /* __CVC4__THEORY__THEORY_UF_H */ -- 2.30.2