*/
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
*/
#include "expr/node.h"
#include "theory/output_channel.h"
+#include "context/context.h"
namespace CVC4 {
namespace theory {
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 */
noinst_LTLIBRARIES = libuf.la
-libuf_la_SOURCES =
+libuf_la_SOURCES = \
+ ecdata.h \
+ ecdata.cpp \
+ theory_uf.h \
+ theory_uf.cpp
EXTRA_DIST = kinds
--- /dev/null
+#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;
+ }
+}
--- /dev/null
+/********************* */
+/** 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 */
--- /dev/null
+
+#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<Node>::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);
+ }
+ }
+ }
+}
--- /dev/null
+
+#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<Node> d_pending;
+ context::CDList<Node> d_disequality;
+ context::CDO<unsigned> 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 */
projects / cvc5.git / commitdiff