#include <cdlist.h>
Inheritance diagram for CVC3::CDList< T >:
Definition at line 41 of file cdlist.h.
typedef std::deque<T>::const_iterator CVC3::CDList< T >::const_iterator |
CVC3::CDList< T >::CDList | ( | const CDList< T > & | l | ) | [inline, private] |
CVC3::CDList< T >::CDList | ( | Context * | context | ) | [inline] |
virtual CVC3::CDList< T >::~CDList | ( | ) | [inline, virtual] |
virtual ContextObj* CVC3::CDList< T >::makeCopy | ( | ContextMemoryManager * | cmm | ) | [inline, private, virtual] |
Make a copy of the current object so it can be restored to its current state.
Implements CVC3::ContextObj.
virtual void CVC3::CDList< T >::restoreData | ( | ContextObj * | data | ) | [inline, private, virtual] |
virtual void CVC3::CDList< T >::setNull | ( | void | ) | [inline, private, virtual] |
unsigned CVC3::CDList< T >::size | ( | ) | const [inline] |
Definition at line 64 of file cdlist.h.
Referenced by CVC3::TheoryUF::assertFact(), CVC3::CDList< CVC3::Literal >::at(), CVC3::CDList< CVC3::Literal >::back(), CVC3::SearchSat::check(), CVC3::TheoryQuant::checkSat(), CVC3::DatatypeTheoremProducer::dummyTheorem(), CVC3::TheoryArithOld::findBounds(), CVC3::TheoryArithNew::findBounds(), CVC3::TheoryQuant::goodSynMatch(), CVC3::TheoryQuant::mapTermsByType(), CVC3::TheoryQuant::naiveCheckSat(), CVC3::CDList< CVC3::Literal >::operator[](), CVC3::TheoryArithOld::processFiniteIntervals(), CVC3::TheoryArithNew::processFiniteIntervals(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryQuant::recInstantiate(), CVC3::TheoryQuant::recSearchCover(), CVC3::DatatypeTheoremProducer::rewriteSelCons(), CVC3::TheoryQuant::synCheckSat(), and CVC3::TheoryQuant::synNewInst().
bool CVC3::CDList< T >::empty | ( | ) | const [inline] |
T& CVC3::CDList< T >::push_back | ( | const T & | data, | |
int | scope = -1 | |||
) | [inline] |
Definition at line 66 of file cdlist.h.
Referenced by CVC3::TheoryUF::assertFact(), CVC3::TheoryQuant::collectChangedTerms(), CVC3::TheoryQuant::combineOldNewTrigs(), CVC3::SearchSat::getAssumptions(), and CVC3::TheoryQuant::synNewInst().
void CVC3::CDList< T >::pop_back | ( | ) | [inline] |
const T& CVC3::CDList< T >::operator[] | ( | unsigned | i | ) | const [inline] |
const T& CVC3::CDList< T >::at | ( | unsigned | i | ) | const [inline] |
const T& CVC3::CDList< T >::back | ( | ) | const [inline] |
const_iterator CVC3::CDList< T >::begin | ( | ) | const [inline] |
const_iterator CVC3::CDList< T >::end | ( | ) | const [inline] |
std::deque<T>* CVC3::CDList< T >::d_list [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::Literal >::at(), CVC3::CDList< CVC3::Literal >::back(), CVC3::CDList< CVC3::Literal >::begin(), CVC3::CDList< CVC3::Literal >::CDList(), CVC3::CDList< CVC3::Literal >::operator[](), CVC3::CDList< CVC3::Literal >::pop_back(), CVC3::CDList< CVC3::Literal >::push_back(), CVC3::CDList< CVC3::Literal >::restoreData(), CVC3::CDList< CVC3::Literal >::setNull(), and CVC3::CDList< CVC3::Literal >::~CDList().
unsigned CVC3::CDList< T >::d_size [private] |
Definition at line 46 of file cdlist.h.
Referenced by CVC3::CDList< CVC3::Literal >::empty(), CVC3::CDList< CVC3::Literal >::end(), CVC3::CDList< CVC3::Literal >::pop_back(), CVC3::CDList< CVC3::Literal >::push_back(), CVC3::CDList< CVC3::Literal >::restoreData(), CVC3::CDList< CVC3::Literal >::setNull(), and CVC3::CDList< CVC3::Literal >::size().