CVCL::CDList< T > Class Template Reference

#include <cdlist.h>

Inheritance diagram for CVCL::CDList< T >:

[legend]Collaboration diagram for CVCL::CDList< T >:

[legend]List of all members.

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)
• const T & operator[] (unsigned i) const
• const T & at (unsigned i) const
• const T & back () const
• const_iterator begin () const
• const_iterator end () const

Private Member Functions

• virtual ContextObj * makeCopy (void)

  Make a copy of the current object so it can be restored to its current state.
  

• virtual void restoreData (ContextObj *data)

  Restore the current object from the given data.
  

• virtual void setNull (void)

  Set the current object to be invalid.
  

• CDList (const CDList< T > &l)

Private Attributes

• std::deque< T > * d_list

  The actual data.
  

• unsigned d_size

---

Detailed Description

template<class T>
class CVCL::CDList< T >

Definition at line 49 of file cdlist.h.

---

Member Typedef Documentation

template<class T> typedef std::deque<T>::const_iterator CVCL::CDList< T >::const_iterator

Definition at line 91 of file cdlist.h.

---

Constructor & Destructor Documentation

template<class T> CVCL::CDList< T >::CDList (  const CDList< T > &  l  )  [inline, private]

Definition at line 65 of file cdlist.h.

template<class T> CVCL::CDList< T >::CDList (  Context *  context  )  [inline]

Definition at line 67 of file cdlist.h.

template<class T> virtual CVCL::CDList< T >::~CDList (   )  [inline, virtual]

Definition at line 71 of file cdlist.h.

---

Member Function Documentation

template<class T> virtual ContextObj* CVCL::CDList< T >::makeCopy (  void   )  [inline, private, virtual]

Make a copy of the current object so it can be restored to its current state. Implements CVCL::ContextObj. Definition at line 56 of file cdlist.h.

template<class T> virtual void CVCL::CDList< T >::restoreData (  ContextObj *  data  )  [inline, private, virtual]

Restore the current object from the given data. Reimplemented from CVCL::ContextObj. Definition at line 57 of file cdlist.h.

template<class T> virtual void CVCL::CDList< T >::setNull (  void   )  [inline, private, virtual]

Set the current object to be invalid. Implements CVCL::ContextObj. Definition at line 60 of file cdlist.h.

template<class T> unsigned CVCL::CDList< T >::size (   )  const [inline]

Definition at line 72 of file cdlist.h. Referenced by CVCL::TheoryUF::assertFact(), CVCL::TheoryArith::assertFact(), CVCL::CDList< SmartCDO< Theorem > >::at(), CVCL::CDList< SmartCDO< Theorem > >::back(), CVCL::SearchEngineFast::bcp(), CVCL::SearchSat::check(), CVCL::TheoryUF::checkSat(), CVCL::TheoryDatatypeLazy::checkSat(), CVCL::TheoryDatatype::checkSat(), CVCL::TheoryBitvector::checkSat(), CVCL::TheoryArith::checkSat(), CVCL::SearchEngineFast::checkValidInternal(), CVCL::DatatypeTheoremProducer::dummyTheorem(), CVCL::TheoryArith::findBounds(), CVCL::SearchEngineFast::findSplitter(), TheoryCore::getImpliedLiteral(), TheoryCore::getImpliedLiteralByIndex(), CVCL::DecisionEngineMBTF::goalSatisfied(), CVCL::DecisionEngineCaching::goalSatisfied(), CVCL::TheoryQuant::goodSynMatch(), CVCL::TheoryQuant::instantiate(), CVCL::TheoryQuant::mapTermsByType(), CVCL::TheoryQuant::naiveCheckSat(), CVCL::TheoryQuant::notifyInconsistent(), SAT::CD_CNF_Formula::numClauses(), CVCL::TheoryCore::numImpliedLiterals(), CVCL::CDList< SmartCDO< Theorem > >::operator[](), CVCL::TheoryArith::processBuffer(), CVCL::TheoryArith::processFiniteIntervals(), CVCL::TheoryArith::projectInequalities(), CVCL::TheoryQuant::recInstantiate(), CVCL::TheoryQuant::recursiveMap(), CVCL::DatatypeTheoremProducer::rewriteSelCons(), CVCL::TheoryQuant::semCheckSat(), CVCL::NotifyList::size(), and CVCL::TheoryQuant::synCheckSat().

template<class T> bool CVCL::CDList< T >::empty (   )  const [inline]

Definition at line 73 of file cdlist.h. Referenced by SAT::CD_CNF_Formula::empty().

template<class T> T& CVCL::CDList< T >::push_back (  const T &  data, int  scope = -1 )  [inline]

Definition at line 74 of file cdlist.h. Referenced by CVCL::NotifyList::add(), CVCL::SearchSat::addLemma(), CVCL::SearchEngineFast::addNewClause(), CVCL::SearchEngineFast::addNonLiteralFact(), CVCL::SearchImplBase::addSplitter(), CVCL::SearchEngineFast::addSplitter(), CVCL::TheoryArith::addToBuffer(), TheoryCore::addToVarDB(), CVCL::TheoryUF::assertFact(), CVCL::TheoryQuant::assertFact(), CVCL::TheoryBitvector::assertFact(), CVCL::TheoryArith::assertFact(), TheoryCore::assertFormula(), CVCL::SearchSat::assertLit(), CVCL::TheoryBitvector::assertTypePred(), CVCL::SearchEngineFast::bcp(), CVCL::SearchSat::check(), CVCL::TheoryDatatypeLazy::checkSat(), CVCL::TheoryUF::computeModel(), CVCL::TheoryArray::computeModel(), CVCL::TheoryDatatypeLazy::initializeLabels(), CVCL::TheoryDatatype::initializeLabels(), CVCL::TheoryDatatypeLazy::instantiate(), CVCL::TheoryQuant::mapTermsByType(), CVCL::TheoryDatatypeLazy::mergeLabels(), CVCL::TheoryDatatype::mergeLabels(), SAT::CD_CNF_Formula::newClause(), CVCL::SearchEngineFast::newIntAssumption(), CVCL::SearchSat::newUserAssumption(), TheoryCore::processUpdates(), CVCL::TheoryArith::projectInequalities(), CVCL::DecisionEngine::pushDecision(), CVCL::TheoryQuant::recursiveMap(), TheoryCore::registerAtom(), CVCL::TheoryUF::setup(), CVCL::TheoryDatatypeLazy::setup(), CVCL::TheoryDatatype::setup(), CVCL::TheoryArray::setup(), TheoryCore::setupTerm(), CVCL::TheoryDatatypeLazy::update(), and CVCL::TheoryDatatype::update().

template<class T> const T& CVCL::CDList< T >::operator[] (  unsigned  i  )  const [inline]

Definition at line 76 of file cdlist.h.

template<class T> const T& CVCL::CDList< T >::at (  unsigned  i  )  const [inline]

Definition at line 81 of file cdlist.h.

template<class T> const T& CVCL::CDList< T >::back (   )  const [inline]

Definition at line 86 of file cdlist.h. Referenced by CVCL::DecisionEngine::lastSplitter().

template<class T> const_iterator CVCL::CDList< T >::begin (   )  const [inline]

Definition at line 92 of file cdlist.h. Referenced by SAT::CD_CNF_Formula::begin(), TheoryCore::buildModel(), TheoryCore::checkSat(), TheoryCore::collectBasicVars(), CVCL::TheoryUF::computeModel(), CVCL::TheoryArray::computeModel(), CVCL::TheoryUF::computeModelTerm(), CVCL::TheoryArray::computeModelTerm(), CVCL::CDList< SmartCDO< Theorem > >::end(), and CVCL::SearchSat::makeDecision().

template<class T> const_iterator CVCL::CDList< T >::end (   )  const [inline]

Definition at line 95 of file cdlist.h. Referenced by TheoryCore::buildModel(), TheoryCore::checkSat(), TheoryCore::collectBasicVars(), CVCL::TheoryUF::computeModel(), CVCL::TheoryArray::computeModel(), CVCL::TheoryUF::computeModelTerm(), CVCL::TheoryArray::computeModelTerm(), SAT::CD_CNF_Formula::end(), and CVCL::SearchSat::makeDecision().

---

Member Data Documentation

template<class T> std::deque<T>* CVCL::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 53 of file cdlist.h. Referenced by CVCL::CDList< SmartCDO< Theorem > >::at(), CVCL::CDList< SmartCDO< Theorem > >::back(), CVCL::CDList< SmartCDO< Theorem > >::begin(), CVCL::CDList< SmartCDO< Theorem > >::CDList(), CVCL::CDList< SmartCDO< Theorem > >::operator[](), CVCL::CDList< SmartCDO< Theorem > >::push_back(), CVCL::CDList< SmartCDO< Theorem > >::restoreData(), CVCL::CDList< SmartCDO< Theorem > >::setNull(), and CVCL::CDList< SmartCDO< Theorem > >::~CDList().

template<class T> unsigned CVCL::CDList< T >::d_size [private]

Definition at line 54 of file cdlist.h. Referenced by CVCL::CDList< SmartCDO< Theorem > >::empty(), CVCL::CDList< SmartCDO< Theorem > >::end(), CVCL::CDList< SmartCDO< Theorem > >::push_back(), CVCL::CDList< SmartCDO< Theorem > >::restoreData(), CVCL::CDList< SmartCDO< Theorem > >::setNull(), and CVCL::CDList< SmartCDO< Theorem > >::size().

---

The documentation for this class was generated from the following file:

• cdlist.h

---