CVCL::CDMap< Key, Data, HashFcn > Class Template Reference

#include <cdmap.h>

Inheritance diagram for CVCL::CDMap< Key, Data, HashFcn >:

[legend]Collaboration diagram for CVCL::CDMap< Key, Data, HashFcn >:

[legend]List of all members.

Public Member Functions

• CDMap (Context *context, int scope=-1)
• ~CDMap ()
• size_t size () const
• size_t count (const Key &k) const
• CDOmap< Key, Data, HashFcn > & operator[] (const Key &k)
• void insert (const Key &k, const Data &d, int scope=-1)
• iterator begin () const
• iterator end () const
• orderedIterator orderedBegin () const
• orderedIterator orderedEnd () const
• iterator find (const Key &k) 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.
  

• void emptyTrash ()
• virtual void setNull (void)

  Set the current object to be invalid.
  

Private Attributes

• std::hash_map< Key, CDOmap<
  Key, Data, HashFcn > * > d_map
• std::vector< CDOmap< Key,
  Data, HashFcn > * > d_trash
• CDOmap< Key, Data, HashFcn > * d_first
• Context * d_context

Friends

• class CDOmap< Key, Data, HashFcn >

Classes

• class iterator
• class orderedIterator

---

Detailed Description

template<class Key, class Data, class HashFcn>
class CVCL::CDMap< Key, Data, HashFcn >

Definition at line 135 of file cdmap.h.

---

Constructor & Destructor Documentation

template<class Key, class Data, class HashFcn> CVCL::CDMap< Key, Data, HashFcn >::CDMap (  Context *  context, int  scope = -1 )  [inline]

Definition at line 166 of file cdmap.h.

template<class Key, class Data, class HashFcn> CVCL::CDMap< Key, Data, HashFcn >::~CDMap (   )  [inline]

Definition at line 170 of file cdmap.h.

---

Member Function Documentation

template<class Key, class Data, class HashFcn> virtual ContextObj* CVCL::CDMap< Key, Data, HashFcn >::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 145 of file cdmap.h.

template<class Key, class Data, class HashFcn> virtual void CVCL::CDMap< Key, Data, HashFcn >::restoreData (  ContextObj *  data  )  [inline, private, virtual]

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

template<class Key, class Data, class HashFcn> void CVCL::CDMap< Key, Data, HashFcn >::emptyTrash (   )  [inline, private]

Definition at line 150 of file cdmap.h. Referenced by CVCL::CDMap< Expr, UserAssertion >::insert(), CVCL::CDMap< Expr, UserAssertion >::operator[](), and CVCL::CDMap< Expr, UserAssertion >::setNull().

template<class Key, class Data, class HashFcn> virtual void CVCL::CDMap< Key, Data, HashFcn >::setNull (  void   )  [inline, private, virtual]

Set the current object to be invalid. Implements CVCL::ContextObj. Definition at line 157 of file cdmap.h. Referenced by CVCL::CDMap< Expr, UserAssertion >::~CDMap().

template<class Key, class Data, class HashFcn> size_t CVCL::CDMap< Key, Data, HashFcn >::size (   )  const [inline]

Definition at line 172 of file cdmap.h. Referenced by CVCL::SearchEngineFast::addNonLiteralFact(), CVCL::TheoryCore::incomplete(), and TheoryCore::incomplete().

template<class Key, class Data, class HashFcn> size_t CVCL::CDMap< Key, Data, HashFcn >::count (  const Key &  k  )  const [inline]

Definition at line 173 of file cdmap.h. Referenced by CVCL::SearchEngineFast::addNonLiteralFact(), CVCL::SearchImplBase::addToCNFCache(), CVCL::VCL::assertFormula(), CVCL::TheoryBitvector::assertTypePred(), checkAssump(), CVCL::SearchSimple::checkValidInternal(), CVCL::SearchEngineFast::checkValidInternal(), CVCL::TheoryBitvector::collectSharedSubterms(), CVCL::SearchImplBase::enqueueCNFrec(), CVCL::SearchImplBase::isAssumption(), CVCL::SearchEngineFast::isAssumption(), CVCL::SearchImplBase::isCNFVar(), CVCL::SearchImplBase::newIntAssumption(), CVCL::TheoryArith::pickMonomial(), CVCL::TheoryQuant::recursiveMap(), CVCL::SearchSimple::restartInternal(), CVCL::SearchEngineFast::restartInternal(), CVCL::TheoryBitvector::update(), and CVCL::TheoryArith::updateStats().

template<class Key, class Data, class HashFcn> CDOmap<Key, Data, HashFcn>& CVCL::CDMap< Key, Data, HashFcn >::operator[] (  const Key &  k  )  [inline]

Definition at line 176 of file cdmap.h.

template<class Key, class Data, class HashFcn> void CVCL::CDMap< Key, Data, HashFcn >::insert (  const Key &  k, const Data &  d, int  scope = -1 )  [inline]

Definition at line 189 of file cdmap.h. Referenced by SAT::CNF_Manager::addLemma(), CVCL::SearchEngineFast::addLiteralFact(), CVCL::SearchImplBase::addToCNFCache(), TheoryCore::collectBasicVars(), SAT::CNF_Manager::convertLemma(), CVCL::SearchSat::getImplication(), CVCL::TheoryDatatypeLazy::initializeLabels(), CVCL::TheoryDatatype::initializeLabels(), CVCL::SearchEngineFast::recordFact(), TheoryCore::setIncomplete(), TheoryCore::setupTerm(), CVCL::CommonTheoremProducer::skolemize(), SAT::CNF_Manager::translateExpr(), and CVCL::CommonTheoremProducer::varIntroSkolem().

template<class Key, class Data, class HashFcn> iterator CVCL::CDMap< Key, Data, HashFcn >::begin (   )  const [inline]

Definition at line 256 of file cdmap.h. Referenced by CVCL::SearchEngineFast::checkValidMain(), TheoryCore::incomplete(), CVCL::SearchImplBase::newUserAssumption(), and CVCL::TheoryArith::refineCounterExample().

template<class Key, class Data, class HashFcn> iterator CVCL::CDMap< Key, Data, HashFcn >::end (   )  const [inline]

Definition at line 257 of file cdmap.h. Referenced by CVCL::TheoryDatatype::addSharedTerm(), CVCL::SearchImplBase::applyCNFRules(), CVCL::TheoryBitvector::bitBlastTerm(), CVCL::TheoryDatatype::canCollapse(), CVCL::TheoryDatatypeLazy::checkSat(), CVCL::TheoryDatatype::checkSat(), CVCL::SearchEngineFast::checkValidMain(), CVCL::SearchImplBase::findInCNFCache(), TheoryCore::incomplete(), CVCL::TheoryDatatypeLazy::initializeLabels(), CVCL::TheoryDatatype::initializeLabels(), CVCL::TheoryDatatypeLazy::mergeLabels(), CVCL::TheoryDatatype::mergeLabels(), CVCL::SearchImplBase::newUserAssumption(), CVCL::TheoryArith::refineCounterExample(), CVCL::SearchImplBase::replaceITE(), CVCL::TheoryDatatypeLazy::setup(), CVCL::TheoryDatatype::setup(), CVCL::CommonTheoremProducer::skolemize(), CVCL::TheoryArith::updateSubsumptionDB(), and CVCL::CommonTheoremProducer::varIntroSkolem().

template<class Key, class Data, class HashFcn> orderedIterator CVCL::CDMap< Key, Data, HashFcn >::orderedBegin (   )  const [inline]

Definition at line 299 of file cdmap.h. Referenced by CVCL::SearchImplBase::getAssumptions(), and CVCL::SearchImplBase::getInternalAssumptions().

template<class Key, class Data, class HashFcn> orderedIterator CVCL::CDMap< Key, Data, HashFcn >::orderedEnd (   )  const [inline]

Definition at line 300 of file cdmap.h. Referenced by CVCL::SearchImplBase::getAssumptions(), and CVCL::SearchImplBase::getInternalAssumptions().

template<class Key, class Data, class HashFcn> iterator CVCL::CDMap< Key, Data, HashFcn >::find (  const Key &  k  )  const [inline]

Definition at line 302 of file cdmap.h. Referenced by CVCL::TheoryDatatype::addSharedTerm(), CVCL::SearchImplBase::applyCNFRules(), CVCL::TheoryBitvector::bitBlastTerm(), CVCL::TheoryDatatype::canCollapse(), CVCL::TheoryDatatypeLazy::checkSat(), CVCL::TheoryDatatype::checkSat(), CVCL::SearchImplBase::findInCNFCache(), CVCL::TheoryDatatypeLazy::initializeLabels(), CVCL::TheoryDatatype::initializeLabels(), CVCL::TheoryDatatypeLazy::mergeLabels(), CVCL::TheoryDatatype::mergeLabels(), CVCL::SearchImplBase::newUserAssumption(), CVCL::SearchImplBase::replaceITE(), CVCL::TheoryDatatypeLazy::setup(), CVCL::TheoryDatatype::setup(), CVCL::CommonTheoremProducer::skolemize(), CVCL::TheoryArith::updateSubsumptionDB(), and CVCL::CommonTheoremProducer::varIntroSkolem().

---

Friends And Related Function Documentation

template<class Key, class Data, class HashFcn> friend class CDOmap< Key, Data, HashFcn > [friend]

Definition at line 136 of file cdmap.h.

---

Member Data Documentation

template<class Key, class Data, class HashFcn> std::hash_map<Key,CDOmap<Key, Data, HashFcn>*> CVCL::CDMap< Key, Data, HashFcn >::d_map [private]

Definition at line 138 of file cdmap.h. Referenced by CVCL::CDMap< Expr, UserAssertion >::begin(), CVCL::CDMap< Expr, UserAssertion >::count(), CVCL::CDMap< Expr, UserAssertion >::end(), CVCL::CDMap< Expr, UserAssertion >::find(), CVCL::CDMap< Expr, UserAssertion >::insert(), CVCL::CDMap< Expr, UserAssertion >::operator[](), CVCL::CDMap< Expr, UserAssertion >::setNull(), and CVCL::CDMap< Expr, UserAssertion >::size().

template<class Key, class Data, class HashFcn> std::vector<CDOmap<Key, Data, HashFcn>*> CVCL::CDMap< Key, Data, HashFcn >::d_trash [private]

Definition at line 140 of file cdmap.h. Referenced by CVCL::CDMap< Expr, UserAssertion >::emptyTrash().

template<class Key, class Data, class HashFcn> CDOmap<Key, Data, HashFcn>* CVCL::CDMap< Key, Data, HashFcn >::d_first [private]

Definition at line 141 of file cdmap.h. Referenced by CVCL::CDMap< Expr, UserAssertion >::orderedBegin().

template<class Key, class Data, class HashFcn> Context* CVCL::CDMap< Key, Data, HashFcn >::d_context [private]

Definition at line 142 of file cdmap.h. Referenced by CVCL::CDMap< Expr, UserAssertion >::insert(), and CVCL::CDMap< Expr, UserAssertion >::operator[]().

---

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

• cdmap.h

---