From: Andrew Reynolds Date: Thu, 20 Aug 2020 01:09:07 +0000 (-0500) Subject: Remove example theory (#4922) X-Git-Tag: cvc5-1.0.0~2974 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=45412d0158992ae193f8e26b25a21e735ac7be8b;p=cvc5.git Remove example theory (#4922) This code is unused and obsolete. --- diff --git a/src/theory/example/ecdata.cpp b/src/theory/example/ecdata.cpp deleted file mode 100644 index bc19f657b..000000000 --- a/src/theory/example/ecdata.cpp +++ /dev/null @@ -1,103 +0,0 @@ -/********************* */ -/*! \file ecdata.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. 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 deleted file mode 100644 index 7b8fcaef5..000000000 --- a/src/theory/example/ecdata.h +++ /dev/null @@ -1,258 +0,0 @@ -/********************* */ -/*! \file ecdata.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Mathias Preiner, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. 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 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(); - - /** - * 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 deleted file mode 100644 index 07cad60e5..000000000 --- a/src/theory/example/theory_uf_tim.cpp +++ /dev/null @@ -1,327 +0,0 @@ -/********************* */ -/*! \file theory_uf_tim.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. 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, UserContext* u, OutputChannel& out, Valuation valuation) : - Theory(THEORY_UF, c, u, 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) { - if (done() && !fullEffort(level)) { - return; - } - - TimerStat::CodeTimer checkTimer(d_checkTime); - - 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::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 deleted file mode 100644 index 438fe33dc..000000000 --- a/src/theory/example/theory_uf_tim.h +++ /dev/null @@ -1,213 +0,0 @@ -/********************* */ -/*! \file theory_uf_tim.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. 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 Theory { - -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 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 d_pending; - - /** Index of the next pending equality to merge. */ - context::CDO d_currentPendingIdx; - - /** List of all disequalities this theory has seen. */ - context::CDList 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 d_registered; - -public: - - /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ - TheoryUFTim(context::Context* c, context::UserContext* u, 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) {} - - 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 ECAttr; - -}/* CVC4::theory::uf::tim namespace */ -}/* CVC4::theory::uf namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* CVC4__THEORY__UF__TIM__THEORY_UF_TIM_H */