CVC3
2.4.1
|
#include <cdlist.h>
Public Types | |
typedef std::deque< T > ::const_iterator | const_iterator |
Public Member Functions | |
CDList (Context *context) | |
virtual | ~CDList () |
unsigned | size () const |
bool | empty () const |
T & | push_back (const T &data, int scope=-1) |
void | pop_back () |
const T & | operator[] (unsigned i) const |
const T & | at (unsigned i) const |
const T & | back () const |
const_iterator | begin () const |
const_iterator | end () const |
![]() | |
ContextObj (Context *context) | |
Create a new ContextObj. More... | |
virtual | ~ContextObj () |
int | level () const |
bool | isCurrent (int scope=-1) const |
void | makeCurrent (int scope=-1) |
void * | operator new (size_t size, MemoryManager *mm) |
void | operator delete (void *pMem, MemoryManager *mm) |
void * | operator new (size_t size, bool b) |
void | operator delete (void *pMem, bool b) |
void | operator delete (void *) |
Private Member Functions | |
virtual ContextObj * | makeCopy (ContextMemoryManager *cmm) |
Make a copy of the current object so it can be restored to its current state. More... | |
virtual void | restoreData (ContextObj *data) |
Restore the current object from the given data. More... | |
virtual void | setNull (void) |
Set the current object to be invalid. More... | |
CDList (const CDList< T > &l) | |
Private Attributes | |
std::deque< T > * | d_list |
The actual data. More... | |
unsigned | d_size |
Additional Inherited Members | |
![]() | |
ContextObj (const ContextObj &co) | |
Copy constructor (defined mainly for debugging purposes) More... | |
ContextObj & | operator= (const ContextObj &co) |
Assignment operator (defined mainly for debugging purposes) More... | |
const ContextObj * | getRestore () |
ContextMemoryManager * | getCMM () |
Return our name (for debugging) More... | |
typedef std::deque<T>::const_iterator CVC3::CDList< T >::const_iterator |
|
inlineprivate |
|
inline |
|
inlinevirtual |
|
inlineprivatevirtual |
Make a copy of the current object so it can be restored to its current state.
Implements CVC3::ContextObj.
|
inlineprivatevirtual |
Restore the current object from the given data.
Reimplemented from CVC3::ContextObj.
|
inlineprivatevirtual |
Set the current object to be invalid.
Implements CVC3::ContextObj.
|
inline |
Definition at line 64 of file cdlist.h.
Referenced by CVC3::TheoryArithOld::DifferenceLogicGraph::addEdge(), CVC3::TheoryUF::assertFact(), CVC3::CDList< CVC3::TheoryArith3::Ineq >::at(), CVC3::CDList< CVC3::TheoryArith3::Ineq >::back(), CVC3::SearchSat::check(), CVC3::TheoryDatatypeLazy::checkSat(), CVC3::TheoryUF::checkSat(), CVC3::TheoryArray::checkSat(), CVC3::TheoryDatatype::checkSat(), CVC3::TheoryQuant::checkSat(), CVC3::TheoryQuant::collectChangedTerms(), CVC3::TheoryArithOld::computeTermBounds(), CVC3::TheoryQuant::debug(), CVC3::DatatypeTheoremProducer::dummyTheorem(), CVC3::TheoryArithNew::findBounds(), CVC3::TheoryArith3::findBounds(), CVC3::TheoryArithOld::findBounds(), CVC3::TheoryArithOld::DifferenceLogicGraph::hasIncoming(), CVC3::TheoryArithOld::DifferenceLogicGraph::hasOutgoing(), CVC3::TheoryQuant::instantiate(), CVC3::TheoryQuant::iterBKList(), CVC3::TheoryQuant::iterFWList(), CVC3::TheoryQuant::mapTermsByType(), CVC3::TheoryQuant::matchListOld(), CVC3::TheoryQuant::naiveCheckSat(), CVC3::CDList< CVC3::TheoryArith3::Ineq >::operator[](), CVC3::TheoryArithNew::processFiniteIntervals(), CVC3::TheoryArith3::processFiniteIntervals(), CVC3::TheoryArithOld::processFiniteIntervals(), CVC3::TheoryArith3::projectInequalities(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryQuant::recInstantiate(), CVC3::TheoryQuant::recMultMatchDebug(), CVC3::TheoryQuant::recMultMatchOldWay(), CVC3::TheoryQuant::recursiveMap(), CVC3::DatatypeTheoremProducer::rewriteSelCons(), CVC3::TheoryQuant::saveContext(), CVC3::TheoryQuant::synCheckSat(), CVC3::TheoryQuant::synNewInst(), CVC3::TheoryQuant::update(), and CVC3::TheoryArithOld::DifferenceLogicGraph::writeGraph().
|
inline |
|
inline |
Definition at line 66 of file cdlist.h.
Referenced by CVC3::NotifyList::add(), CVC3::TheoryArray::addSharedTerm(), CVC3::TheoryArithOld::addSharedTerm(), CVC3::TheoryUF::assertFact(), CVC3::TheoryQuant::checkSat(), CVC3::TheoryQuant::collectChangedTerms(), CVC3::TheoryQuant::combineOldNewTrigs(), CVC3::TheoryArithOld::DifferenceLogicGraph::getEdge(), CVC3::TheoryDatatypeLazy::initializeLabels(), CVC3::TheoryDatatype::initializeLabels(), CVC3::TheoryDatatypeLazy::instantiate(), CVC3::TheoryQuant::mapTermsByType(), CVC3::TheoryArith3::projectInequalities(), CVC3::TheoryArithOld::projectInequalities(), CVC3::DecisionEngine::pushDecision(), CVC3::TheoryQuant::recursiveMap(), CVC3::TheoryDatatypeLazy::setup(), CVC3::TheoryUF::setup(), CVC3::TheoryArray::setup(), CVC3::TheoryDatatype::setup(), CVC3::TheoryCore::setupTerm(), CVC3::TheoryQuant::synCheckSat(), CVC3::TheoryQuant::synNewInst(), CVC3::TheoryDatatypeLazy::update(), and CVC3::TheoryArray::update().
|
inline |
|
inline |
|
inline |
|
inline |
Definition at line 82 of file cdlist.h.
Referenced by CVC3::DecisionEngine::lastSplitter().
|
inline |
Definition at line 88 of file cdlist.h.
Referenced by CVC3::TheoryUF::computeModel(), CVC3::TheoryArray::computeModel(), CVC3::TheoryUF::computeModelTerm(), CVC3::TheoryArray::computeModelTerm(), and CVC3::CDList< CVC3::TheoryArith3::Ineq >::end().
|
inline |
Definition at line 91 of file cdlist.h.
Referenced by CVC3::TheoryUF::computeModel(), CVC3::TheoryArray::computeModel(), CVC3::TheoryUF::computeModelTerm(), and CVC3::TheoryArray::computeModelTerm().
|
private |
The actual data.
Use deque because it doesn't create/destroy data on resize. This pointer is only non-NULL in the master copy.
Definition at line 45 of file cdlist.h.
Referenced by CVC3::CDList< CVC3::TheoryArith3::Ineq >::at(), CVC3::CDList< CVC3::TheoryArith3::Ineq >::back(), CVC3::CDList< CVC3::TheoryArith3::Ineq >::begin(), CVC3::CDList< CVC3::TheoryArith3::Ineq >::CDList(), CVC3::CDList< CVC3::TheoryArith3::Ineq >::operator[](), CVC3::CDList< CVC3::TheoryArith3::Ineq >::pop_back(), CVC3::CDList< CVC3::TheoryArith3::Ineq >::push_back(), CVC3::CDList< CVC3::TheoryArith3::Ineq >::restoreData(), CVC3::CDList< CVC3::TheoryArith3::Ineq >::setNull(), and CVC3::CDList< CVC3::TheoryArith3::Ineq >::~CDList().
|
private |
Definition at line 46 of file cdlist.h.
Referenced by CVC3::CDList< CVC3::TheoryArith3::Ineq >::empty(), CVC3::CDList< CVC3::TheoryArith3::Ineq >::end(), CVC3::CDList< CVC3::TheoryArith3::Ineq >::pop_back(), CVC3::CDList< CVC3::TheoryArith3::Ineq >::push_back(), CVC3::CDList< CVC3::TheoryArith3::Ineq >::restoreData(), CVC3::CDList< CVC3::TheoryArith3::Ineq >::setNull(), and CVC3::CDList< CVC3::TheoryArith3::Ineq >::size().