diff options
| -rw-r--r-- | src/theory/Makefile.am | 1 | ||||
| -rw-r--r-- | src/theory/example/Makefile | 4 | ||||
| -rw-r--r-- | src/theory/example/Makefile.am | 14 | ||||
| -rw-r--r-- | src/theory/example/ecdata.cpp | 105 | ||||
| -rw-r--r-- | src/theory/example/ecdata.h | 261 | ||||
| -rw-r--r-- | src/theory/example/theory_uf_tim.cpp | 325 | ||||
| -rw-r--r-- | src/theory/example/theory_uf_tim.h | 225 |
7 files changed, 935 insertions, 0 deletions
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index 6e8734b4d..c1a77d988 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -4,6 +4,7 @@ AM_CPPFLAGS = \ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) SUBDIRS = builtin booleans uf arith arrays bv datatypes +DIST_SUBDIRS = $(SUBDIRS) example noinst_LTLIBRARIES = libtheory.la diff --git a/src/theory/example/Makefile b/src/theory/example/Makefile new file mode 100644 index 000000000..be6721f80 --- /dev/null +++ b/src/theory/example/Makefile @@ -0,0 +1,4 @@ +topdir = ../../.. +srcdir = src/theory/example + +include $(topdir)/Makefile.subdir diff --git a/src/theory/example/Makefile.am b/src/theory/example/Makefile.am new file mode 100644 index 000000000..4d08f7a69 --- /dev/null +++ b/src/theory/example/Makefile.am @@ -0,0 +1,14 @@ +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../.. +AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) + +noinst_LTLIBRARIES = libexample.la + +libexample_la_SOURCES = \ + ecdata.h \ + ecdata.cpp \ + theory_uf_tim.h \ + theory_uf_tim.cpp + +EXTRA_DIST = diff --git a/src/theory/example/ecdata.cpp b/src/theory/example/ecdata.cpp new file mode 100644 index 000000000..52a110ff2 --- /dev/null +++ b/src/theory/example/ecdata.cpp @@ -0,0 +1,105 @@ +/********************* */ +/*! \file ecdata.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/uf/tim/ecdata.h" + +using namespace CVC4; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::uf; +using namespace CVC4::theory::uf::tim; + +ECData::ECData(Context * context, TNode n) : + ContextObj(context), + d_find(this), + d_rep(n), + d_watchListSize(0), + d_first(NULL), + d_last(NULL) { +} + +bool ECData::isClassRep() { + return this == this->d_find; +} + +void ECData::addPredecessor(TNode n) { + Assert(isClassRep()); + + makeCurrent(); + + Link * newPred = new(getCMM()) Link(getContext(), n, d_first); + d_first = newPred; + if(d_last == NULL) { + d_last = newPred; + } + + ++d_watchListSize; +} + +ContextObj* ECData::save(ContextMemoryManager* pCMM) { + return new(pCMM) ECData(*this); +} + +void ECData::restore(ContextObj* pContextObj) { + ECData* data = (ECData*)pContextObj; + d_find = data->d_find; + d_first = data->d_first; + d_last = data->d_last; + d_rep = data->d_rep; + d_watchListSize = data->d_watchListSize; +} + +Node ECData::getRep() { + return d_rep; +} + +unsigned ECData::getWatchListSize() { + return d_watchListSize; +} + +void ECData::setFind(ECData * ec) { + makeCurrent(); + d_find = ec; +} + +ECData* ECData::getFind() { + return d_find; +} + +Link* ECData::getFirst() { + return d_first; +} + +void ECData::takeOverDescendantWatchList(ECData* nslave, ECData* nmaster) { + Assert(nslave != nmaster); + Assert(nslave->getFind() == nmaster); + + nmaster->makeCurrent(); + + nmaster->d_watchListSize += nslave->d_watchListSize; + + if(nmaster->d_first == NULL) { + nmaster->d_first = nslave->d_first; + nmaster->d_last = nslave->d_last; + } else if(nslave->d_first != NULL) { + Link* currLast = nmaster->d_last; + currLast->d_next = nslave->d_first; + nmaster->d_last = nslave->d_last; + } +} diff --git a/src/theory/example/ecdata.h b/src/theory/example/ecdata.h new file mode 100644 index 000000000..5e72f0042 --- /dev/null +++ b/src/theory/example/ecdata.h @@ -0,0 +1,261 @@ +/********************* */ +/*! \file ecdata.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__UF__TIM__ECDATA_H +#define __CVC4__THEORY__UF__TIM__ECDATA_H + +#include "expr/node.h" +#include "context/context.h" +#include "context/cdo.h" +#include "context/context_mm.h" + +namespace CVC4 { +namespace theory { +namespace uf { +namespace tim { + +/** + * Link is a context dependent linked list of nodes. + * Link is intended to be allocated in a Context's memory manager. + * The next pointer of the list is context dependent, but the node being + * pointed to is fixed for the life of the Link. + * + * Clients of Link are intended not to modify the node that is being pointed + * to in good faith. This may change in the future. + */ +struct Link { + /** + * Pointer to the next element in linked list. + * This is context dependent. + */ + context::CDO<Link*> d_next; + + /** + * Link is supposed to be allocated in a region of a + * ContextMemoryManager. In order to avoid having to decrement the + * ref count at deletion time, it is preferrable for the user of + * Link to maintain the invariant that data will survival for the + * entire scope of the TNode. + */ + TNode d_data; + + /** + * Creates a new Link w.r.t. a context for the node n. + * An optional parameter is to specify the next element in the link. + */ + Link(context::Context* context, TNode n, Link* l = NULL) : + d_next(true, context, l), + d_data(n) { + Debug("context") << "Link: " << this + << " so cdo is " << &d_next << std::endl; + } + + /** + * Allocates a new Link in the region for the provided ContextMemoryManager. + * This allows for cheap cleanup on pop. + */ + static void* operator new(size_t size, context::ContextMemoryManager* pCMM) { + return pCMM->newData(size); + } + +private: + + /** + * The destructor isn't actually defined. This declaration keeps + * the compiler from creating (wastefully) a default definition, and + * ensures that we get a link error if someone uses Link in a way + * that requires destruction. Objects of class Link should always + * be allocated in a ContextMemoryManager, which doesn't call + * destructors. + */ + ~Link() throw(); + + /** + * Just like the destructor, this is not defined. This ensures no + * one tries to create a Link on the heap. + */ + static void* operator new(size_t size); + +};/* struct Link */ + + +/** + * ECData is a equivalence class object that is context dependent. + * It is developed in order to support the congruence closure algorithm + * in TheoryUF, and is not intended to be used outside of that package. + * + * ECData maintains: + * - find pointer for the equivalence class (disjoint set forest) + * - the node that represents the equivalence class. + * - maintains a predecessorlist/watchlist + * + * ECData does not have support for the canonical find and union operators + * for disjoint set forests. Instead it only provides access to the find + * pointer. The implementation of find is ccFind in TheoryUF. + * union is broken into 2 phases: + * 1) setting the find point with setFind + * 2) taking over the watch list of the other node. + * This is a technical requirement for the implementation of TheoryUF. + * (See ccUnion in TheoryUF for more information.) + * + * The intended paradigm for iterating over the watch list of ec is: + * for(Link* i = ec->getFirst(); i != NULL; i = i->next ); + * + * See also ECAttr() in theory_uf.h, and theory_uf.cpp where the codde that uses + * ECData lives. + */ +class ECData : public context::ContextObj { +private: + /** + * This is the standard disjoint set forest find pointer. + * + * Why an ECData pointer instead of a node? + * This was chosen to be a ECData pointer in order to shortcut at least one + * table every time the find pointer is examined. + */ + ECData* d_find; + + /** + * This is pointer back to the node that represents this equivalence class. + * + * The following invariant should be maintained: + * (n.getAttribute(ECAttr()))->rep == n + * i.e. rep is equal to the node that maps to the ECData using ECAttr. + * + * Tricky part: This needs to be a TNode, not a Node. + * Suppose that rep were a hard link. + * When a node n maps to an ECData via the ECAttr() there will be a hard + * link back to n in the ECData. The attribute does not do garbage collection + * until the node gets garbage collected, which does not happen until its + * ref count drops to 0. So because of this cycle neither the node and + * the ECData will never get garbage collected. + * So this needs to be a soft link. + */ + TNode d_rep; + + // Watch list data structures follow + + /** + * Maintains watch list size for more efficient merging. + */ + unsigned d_watchListSize; + + /** + * Pointer to the beginning of the watchlist. + * This value is NULL iff the watch list is empty. + */ + Link* d_first; + + /** + * Pointer to the end of the watch-list. + * This is maintained in order to constant time list merging. + * (This does not give any asymptotic improve as this is currently always + * preceeded by an O(|watchlist|) operation.) + * This value is NULL iff the watch list is empty. + */ + Link* d_last; + + /** Context-dependent operation: save this ECData */ + context::ContextObj* save(context::ContextMemoryManager* pCMM); + + /** Context-dependent operation: restore this ECData */ + 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. Does + * context-dependent memory allocation in the Context with which + * this ECData was created. + * + * @param n the node to be added. + * @pre isClassRep() == true + */ + void addPredecessor(TNode n); + + /** + * 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, TNode n); + + /** Destructor for ECDatas */ + ~ECData() { + Debug("ufgc") << "Calling ECData destructor" << std::endl; + destroy(); + } + + /** + * An ECData takes over the watch list of another ECData. + * This is the second step in the union operator for ECData. + * This should be called after nslave->setFind(nmaster); + * After this is done nslave's watch list should never be accessed by + * getLast() or getFirst() + */ + static void takeOverDescendantWatchList(ECData * nslave, ECData * nmaster); + + /** + * 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(); + + /** + * Sets the find pointer of the equivalence class to be another ECData object. + * + * @pre isClassRep() == true + * @pre ec->isClassRep() == true + * @post isClassRep() == false + * @post ec->isClassRep() == true + */ + void setFind(ECData * ec); + +};/* class ECData */ + +}/* CVC4::theory::uf::tim namespace */ +}/* CVC4::theory::uf namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__UF__TIM__ECDATA_H */ diff --git a/src/theory/example/theory_uf_tim.cpp b/src/theory/example/theory_uf_tim.cpp new file mode 100644 index 000000000..ae37dfe99 --- /dev/null +++ b/src/theory/example/theory_uf_tim.cpp @@ -0,0 +1,325 @@ +/********************* */ +/*! \file theory_uf_tim.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: mdeters + ** Minor contributors (to current version): dejan + ** 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 the theory of uninterpreted functions. + ** + ** Implementation of the theory of uninterpreted functions. + **/ + +#include "theory/uf/tim/theory_uf_tim.h" +#include "theory/uf/tim/ecdata.h" +#include "expr/kind.h" + +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::uf; +using namespace CVC4::theory::uf::tim; + +TheoryUFTim::TheoryUFTim(Context* c, OutputChannel& out, Valuation valuation) : + TheoryUF(c, out, valuation), + d_assertions(c), + d_pending(c), + d_currentPendingIdx(c,0), + d_disequality(c), + d_registered(c) { + Warning() << "NOTE:" << std::endl + << "NOTE: currently the 'Tim' UF solver is broken," << std::endl + << "NOTE: since its registerTerm() function is never" << std::endl + << "NOTE: called." << std::endl + << "NOTE:" << std::endl; +} + +TheoryUFTim::~TheoryUFTim() { +} + +void TheoryUFTim::preRegisterTerm(TNode n) { + Debug("uf") << "uf: begin preRegisterTerm(" << n << ")" << std::endl; + Debug("uf") << "uf: end preRegisterTerm(" << n << ")" << std::endl; +} + +void TheoryUFTim::registerTerm(TNode n) { + + Debug("uf") << "uf: begin registerTerm(" << n << ")" << std::endl; + + d_registered.push_back(n); + + ECData* ecN; + + if(n.getAttribute(ECAttr(), ecN)) { + /* registerTerm(n) is only called when a node has not been seen in the + * current context. ECAttr() is not a context-dependent attribute. + * When n.hasAttribute(ECAttr(),...) is true on a registerTerm(n) call, + * then it must be the case that this attribute was created in a previous + * and no longer valid context. Because of this we have to reregister the + * predecessors lists. + * Also we do not have to worry about duplicates because all of the Link* + * setup before are removed when the context n was setup in was popped out + * of. All we are going to do here are sanity checks. + */ + + /* + * Consider the following chain of events: + * 1) registerTerm(n) is called on node n where n : f(m) in context level X, + * 2) A new ECData is created on the heap, ecN, + * 3) n is added to the predessecor list of m in context level X, + * 4) We pop out of X, + * 5) n is removed from the predessecor list of m because this is context + * dependent, the Link* will be destroyed and pointers to the Link + * structs in the ECData objects will be updated. + * 6) registerTerm(n) is called on node n in context level Y, + * 7) If n.hasAttribute(ECAttr(), &ecN), then ecN is still around, + * but the predecessor list is not + * + * The above assumes that the code is working correctly. + */ + Assert(ecN->getFirst() == NULL, + "Equivalence class data exists for the node being registered. " + "Expected getFirst() == NULL. " + "This data is either already in use or was not properly maintained " + "during backtracking"); + /*Assert(ecN->getLast() == NULL, + "Equivalence class data exists for the node being registered. " + "Expected getLast() == NULL. " + "This data is either already in use or was not properly maintained " + "during backtracking.");*/ + Assert(ecN->isClassRep(), + "Equivalence class data exists for the node being registered. " + "Expected isClassRep() to be true. " + "This data is either already in use or was not properly maintained " + "during backtracking"); + Assert(ecN->getWatchListSize() == 0, + "Equivalence class data exists for the node being registered. " + "Expected getWatchListSize() == 0. " + "This data is either already in use or was not properly maintained " + "during backtracking"); + } else { + //The attribute does not exist, so it is created and set + ecN = new (true) ECData(getContext(), n); + n.setAttribute(ECAttr(), ecN); + } + + /* If the node is an APPLY_UF, we need to add it to the predecessor list + * of its children. + */ + if(n.getKind() == APPLY_UF) { + TNode::iterator cIter = n.begin(); + + for(; cIter != n.end(); ++cIter) { + TNode child = *cIter; + + /* Because this can be called after nodes have been merged, we need + * to lookup the representative in the UnionFind datastructure. + */ + ECData* ecChild = ccFind(child.getAttribute(ECAttr())); + + /* Because this can be called after nodes have been merged we may need + * to be merged with other predecessors of the equivalence class. + */ + for(Link* Px = ecChild->getFirst(); Px != NULL; Px = Px->d_next ) { + if(equiv(n, Px->d_data)) { + Node pend = n.eqNode(Px->d_data); + d_pending.push_back(pend); + } + } + + ecChild->addPredecessor(n); + } + } + Debug("uf") << "uf: end registerTerm(" << n << ")" << std::endl; + +} + +bool TheoryUFTim::sameCongruenceClass(TNode x, TNode y) { + return + ccFind(x.getAttribute(ECAttr())) == + ccFind(y.getAttribute(ECAttr())); +} + +bool TheoryUFTim::equiv(TNode x, TNode y) { + Assert(x.getKind() == kind::APPLY_UF); + Assert(y.getKind() == kind::APPLY_UF); + + if(x.getNumChildren() != y.getNumChildren()) { + return false; + } + + if(x.getOperator() != y.getOperator()) { + return false; + } + + // intentionally don't look at operator + + TNode::iterator xIter = x.begin(); + TNode::iterator yIter = y.begin(); + + while(xIter != x.end()) { + + if(!sameCongruenceClass(*xIter, *yIter)) { + return false; + } + + ++xIter; + ++yIter; + } + return true; +} + +/* This is a very basic, but *obviously correct* find implementation + * of the classic find algorithm. + * TODO after we have done some more testing: + * 1) Add path compression. This is dependent on changes to ccUnion as + * many better algorithms use eager path compression. + * 2) Elminate recursion. + */ +ECData* TheoryUFTim::ccFind(ECData * x) { + if(x->getFind() == x) { + return x; + } else { + return ccFind(x->getFind()); + } + /* Slightly better Find w/ path compression and no recursion*/ + /* + ECData* start; + ECData* next = x; + while(x != x->getFind()) x=x->getRep(); + while( (start = next) != x) { + next = start->getFind(); + start->setFind(x); + } + return x; + */ +} + +void TheoryUFTim::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->d_next ) { + for(Link* Py = nslave->getFirst(); Py != NULL; Py = Py->d_next ) { + if(equiv(Px->d_data,Py->d_data)) { + Node pendingEq = (Px->d_data).eqNode(Py->d_data); + d_pending.push_back(pendingEq); + } + } + } + + ECData::takeOverDescendantWatchList(nslave, nmaster); +} + +void TheoryUFTim::merge() { + while(d_currentPendingIdx < d_pending.size() ) { + Node assertion = d_pending[d_currentPendingIdx]; + d_currentPendingIdx = d_currentPendingIdx + 1; + + TNode x = assertion[0]; + TNode y = assertion[1]; + + ECData* tmpX = x.getAttribute(ECAttr()); + ECData* tmpY = y.getAttribute(ECAttr()); + + ECData* ecX = ccFind(tmpX); + ECData* ecY = ccFind(tmpY); + if(ecX == ecY) + continue; + + Debug("uf") << "merging equivalence classes for " << std::endl; + Debug("uf") << "left equivalence class :" << (ecX->getRep()) << std::endl; + Debug("uf") << "right equivalence class :" << (ecY->getRep()) << std::endl; + Debug("uf") << std::endl; + + ccUnion(ecX, ecY); + } +} + +Node TheoryUFTim::constructConflict(TNode diseq) { + Debug("uf") << "uf: begin constructConflict()" << std::endl; + + NodeBuilder<> nb(kind::AND); + nb << diseq; + for(unsigned i = 0; i < d_assertions.size(); ++i) { + nb << d_assertions[i]; + } + + Assert(nb.getNumChildren() > 0); + Node conflict = nb.getNumChildren() == 1 ? nb[0] : nb; + + Debug("uf") << "conflict constructed : " << conflict << std::endl; + + Debug("uf") << "uf: ending constructConflict()" << std::endl; + + return conflict; +} + +void TheoryUFTim::check(Effort level) { + + Debug("uf") << "uf: begin check(" << level << ")" << std::endl; + + while(!done()) { + Node assertion = get(); + Debug("uf") << "TheoryUFTim::check(): " << assertion << std::endl; + + switch(assertion.getKind()) { + case EQUAL: + d_assertions.push_back(assertion); + d_pending.push_back(assertion); + merge(); + break; + case NOT: + Assert(assertion[0].getKind() == EQUAL, + "predicates not supported in this UF implementation"); + d_disequality.push_back(assertion[0]); + break; + case APPLY_UF: + Unhandled("predicates not supported in this UF implementation"); + default: + Unhandled(assertion.getKind()); + } + + Debug("uf") << "TheoryUFTim::check(): done = " << (done() ? "true" : "false") << std::endl; + } + + //Make sure all outstanding merges are completed. + if(d_currentPendingIdx < d_pending.size()) { + merge(); + } + + if(standardEffortOrMore(level)) { + for(CDList<Node>::const_iterator diseqIter = d_disequality.begin(); + diseqIter != d_disequality.end(); + ++diseqIter) { + + TNode left = (*diseqIter)[0]; + TNode right = (*diseqIter)[1]; + if(sameCongruenceClass(left, right)) { + Node remakeNeq = (*diseqIter).notNode(); + Node conflict = constructConflict(remakeNeq); + d_out->conflict(conflict, false); + return; + } + } + } + + Debug("uf") << "uf: end check(" << level << ")" << std::endl; +} diff --git a/src/theory/example/theory_uf_tim.h b/src/theory/example/theory_uf_tim.h new file mode 100644 index 000000000..70c60728f --- /dev/null +++ b/src/theory/example/theory_uf_tim.h @@ -0,0 +1,225 @@ +/********************* */ +/*! \file theory_uf_tim.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 This is a basic implementation of the Theory of Uninterpreted Functions + ** with Equality. + ** + ** This is a basic implementation of the Theory of Uninterpreted Functions + ** with Equality. It is based on the Nelson-Oppen algorithm given in + ** "Fast Decision Procedures Based on Congruence Closure" + ** (http://portal.acm.org/ft_gateway.cfm?id=322198&type=pdf) + ** This has been extended to work in a context-dependent way. + ** This interacts heavily with the data-structures given in ecdata.h . + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__UF__TIM__THEORY_UF_TIM_H +#define __CVC4__THEORY__UF__TIM__THEORY_UF_TIM_H + +#include "expr/node.h" +#include "expr/attribute.h" + +#include "theory/theory.h" + +#include "context/context.h" +#include "context/cdo.h" +#include "context/cdlist.h" +#include "theory/uf/theory_uf.h" +#include "theory/uf/tim/ecdata.h" + +namespace CVC4 { +namespace theory { +namespace uf { +namespace tim { + +class TheoryUFTim : public TheoryUF { + +private: + + /** + * List of all of the non-negated literals from the assertion queue. + * This is used only for conflict generation. + * This differs from pending as the program generates new equalities that + * are not in this list. + * This will probably be phased out in future version. + */ + context::CDList<Node> d_assertions; + + /** + * List of pending equivalence class merges. + * + * Tricky part: + * Must keep a hard link because new equality terms are created and appended + * to this list. + */ + context::CDList<Node> d_pending; + + /** Index of the next pending equality to merge. */ + context::CDO<unsigned> d_currentPendingIdx; + + /** List of all disequalities this theory has seen. */ + context::CDList<Node> d_disequality; + + /** + * List of all of the terms that are registered in the current context. + * When registerTerm is called on a term we want to guarentee that there + * is a hard link to the term for the duration of the context in which + * register term is called. + * This invariant is enough for us to use soft links where we want is the + * current implementation as well as making ECAttr() not context dependent. + * Soft links used both in ECData, and Link. + */ + context::CDList<Node> d_registered; + +public: + + /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ + TheoryUFTim(context::Context* c, OutputChannel& out, Valuation valuation); + + /** Destructor for the TheoryUF object. */ + ~TheoryUFTim(); + + /** + * Registers a previously unseen [in this context] node n. + * For TheoryUF, this sets up and maintains invaraints about + * equivalence class data-structures. + * + * Overloads a void registerTerm(TNode n); from theory.h. + * See theory/theory.h for more information about this method. + */ + void registerTerm(TNode n); + + /** + * Currently this does nothing. + * + * Overloads a void preRegisterTerm(TNode n); from theory.h. + * See theory/theory.h for more information about this method. + */ + void preRegisterTerm(TNode n); + + /** + * Checks whether the set of literals provided to the theory is consistent. + * + * If this is called at any effort level, it computes the congruence closure + * of all of the positive literals in the context. + * + * If this is called at full effort it checks if any of the negative literals + * are inconsistent with the congruence closure. + * + * Overloads void check(Effort level); from theory.h. + * See theory/theory.h for more information about this method. + */ + void check(Effort level); + + void presolve() { + // do nothing + } + + /** + * Propagates theory literals. Currently does nothing. + * + * Overloads void propagate(Effort level); from theory.h. + * See theory/theory.h for more information about this method. + */ + void propagate(Effort level) {} + + /** + * Explains a previously reported conflict. Currently does nothing. + * + * Overloads void explain(TNode n, Effort level); from theory.h. + * See theory/theory.h for more information about this method. + */ + void explain(TNode n) {} + + /** + * Get a theory value. + * + * Overloads Node getValue(TNode n); from theory.h. + * See theory/theory.h for more information about this method. + */ + Node getValue(TNode n) { + Unimplemented("TheoryUFTim doesn't support model generation"); + } + + std::string identify() const { return std::string("TheoryUFTim"); } + +private: + /** + * Checks whether 2 nodes are already in the same equivalence class tree. + * This should only be used internally, and it should only be called when + * the only thing done with the equivalence classes is an equality check. + * + * @returns true iff ccFind(x) == ccFind(y); + */ + bool sameCongruenceClass(TNode x, TNode y); + + /** + * Checks whether Node x and Node y are currently congruent + * using the equivalence class data structures. + * @returns true iff + * |x| = n = |y| and + * x.getOperator() == y.getOperator() and + * forall 1 <= i < n : ccFind(x[i]) == ccFind(y[i]) + */ + bool equiv(TNode x, TNode y); + + /** + * Merges 2 equivalence classes, checks wether any predecessors need to + * be set equal to complete congruence closure. + * The class with the smaller class size will be merged. + * @pre ecX->isClassRep() + * @pre ecY->isClassRep() + */ + void ccUnion(ECData* ecX, ECData* ecY); + + /** + * Returns the representative of the equivalence class. + * May modify the find pointers associated with equivalence classes. + */ + ECData* ccFind(ECData* x); + + /** Performs Congruence Closure to reflect the new additions to d_pending. */ + void merge(); + + /** Constructs a conflict from an inconsistent disequality. */ + Node constructConflict(TNode diseq); + +};/* class TheoryUFTim */ + + +/** + * Cleanup function for ECData. This will be used for called whenever + * a ECAttr is being destructed. + */ +struct ECCleanupStrategy { + static void cleanup(ECData* ec) { + Debug("ufgc") << "cleaning up ECData " << ec << "\n"; + ec->deleteSelf(); + } +};/* struct ECCleanupStrategy */ + +/** Unique name to use for constructing ECAttr. */ +struct ECAttrTag {}; + +/** + * ECAttr is the attribute that maps a node to an equivalence class. + */ +typedef expr::Attribute<ECAttrTag, ECData*, ECCleanupStrategy> ECAttr; + +}/* CVC4::theory::uf::tim namespace */ +}/* CVC4::theory::uf namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__UF__TIM__THEORY_UF_TIM_H */ |