This code is unused and obsolete.
+++ /dev/null
-/********************* */
-/*! \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;
- }
-}
+++ /dev/null
-/********************* */
-/*! \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<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();
-
- /**
- * 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
- ** 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<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
- ** 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<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, 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<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