diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-16 21:52:25 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-16 21:52:25 +0000 |
commit | 67bc89bd3fa304ea39934c14a7187c088e600011 (patch) | |
tree | 605dd06960842c354c8ca712690dbf605ef80fbc /src/theory/example/ecdata.cpp | |
parent | 438bec4894e3696d80152b420d7815ff88f07797 (diff) |
include example theory (former "UF-Tim") that's included in the dist but not built for the library
Diffstat (limited to 'src/theory/example/ecdata.cpp')
-rw-r--r-- | src/theory/example/ecdata.cpp | 105 |
1 files changed, 105 insertions, 0 deletions
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; + } +} |