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
--- /dev/null
+topdir = ../../..
+srcdir = src/theory/example
+
+include $(topdir)/Makefile.subdir
--- /dev/null
+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 =
--- /dev/null
+/********************* */
+/*! \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;
+ }
+}
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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;
+}
--- /dev/null
+/********************* */
+/*! \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 */
projects / cvc5.git / commitdiff