CVCL::ExprMap< Data > Class Template Reference

#include <expr_map.h>

Inheritance diagram for CVCL::ExprMap< Data >:

[legend]List of all members.

Public Member Functions

• ExprMap ()
• ExprMap (const ExprMap &map)
• bool empty () const
• size_t size () const
• int count (const Expr &e) const
• Data & operator[] (const Expr &e)
• void clear ()
• void insert (const Expr &e, const Data &d)
• void erase (const Expr &e)
• template<class InputIterator> void insert (InputIterator l, InputIterator r)
• template<class InputIterator> void erase (InputIterator l, InputIterator r)
• iterator begin () const
• iterator end () const
• iterator find (const Expr &e) const

Private Types

• typedef std::map< Expr, Data > ExprMapType

Private Attributes

• ExprMapType d_map

Friends

• bool operator== (const ExprMap &m1, const ExprMap &m2)
• bool operator!= (const ExprMap &m1, const ExprMap &m2)

Classes

• class iterator

---

Detailed Description

template<class Data>
class CVCL::ExprMap< Data >

Definition at line 70 of file expr_map.h.

---

Member Typedef Documentation

template<class Data> typedef std::map<Expr, Data> CVCL::ExprMap< Data >::ExprMapType [private]

Definition at line 73 of file expr_map.h.

---

Constructor & Destructor Documentation

template<class Data> CVCL::ExprMap< Data >::ExprMap (   )  [inline]

Definition at line 130 of file expr_map.h.

template<class Data> CVCL::ExprMap< Data >::ExprMap (  const ExprMap< Data > &  map  )  [inline]

Definition at line 132 of file expr_map.h.

---

Member Function Documentation

template<class Data> bool CVCL::ExprMap< Data >::empty (   )  const [inline]

Definition at line 135 of file expr_map.h. Referenced by CVCL::BitvectorTheoremProducer::collectOneTermOfPlus(), and CVCL::TheoryArith::substAndCanonize().

template<class Data> size_t CVCL::ExprMap< Data >::size (   )  const [inline]

Definition at line 136 of file expr_map.h. Referenced by CVCL::ExprStream::addLetHeader(), CVCL::TheoryArith::findBounds(), CVCL::TheoryQuant::goodSynMatch(), CVCL::TheoryDatatypeLazy::initializeLabels(), CVCL::TheoryDatatype::initializeLabels(), CVCL::CommonTheoremProducer::rewriteAnd(), CVCL::CommonTheoremProducer::rewriteOr(), and CVCL::TheoryQuant::setupTriggers().

template<class Data> int CVCL::ExprMap< Data >::count (  const Expr &  e  )  const [inline]

Definition at line 138 of file expr_map.h. Referenced by CVCL::QuantTheoremProducer::boundVarElim(), CVCL::ArithTheoremProducer::canonComboLikeTerms(), CVCL::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVCL::ExprStream::collectShared(), CVCL::TheoryArith::VarOrderGraph::dfs(), CVCL::VCCmd::findAxioms(), CVCL::TheoryArith::findBounds(), CVCL::TheoryQuant::findInstAssumptions(), CVCL::DecisionEngine::findSplitterRec(), CVCL::DecisionEngineCaching::goalSatisfied(), CVCL::TheoryDatatype::parseExprOp(), CVCL::QuantTheoremProducer::recFindBoundVars(), CVCL::TheoryQuant::recursiveMap(), CVCL::CommonTheoremProducer::rewriteAnd(), and CVCL::CommonTheoremProducer::rewriteOr().

template<class Data> Data& CVCL::ExprMap< Data >::operator[] (  const Expr &  e  )  [inline]

Definition at line 139 of file expr_map.h.

template<class Data> void CVCL::ExprMap< Data >::clear (   )  [inline]

Definition at line 140 of file expr_map.h. Referenced by CVCL::ExprStream::addLetHeader(), CVCL::TheoryBitvector::bitBlastDisEqn(), CVCL::TheoryBitvector::bitBlastEqn(), CVCL::BitvectorTheoremProducer::collectLikeTermsOfPlus(), CVCL::DecisionEngineMBTF::findSplitter(), CVCL::DecisionEngineDFS::findSplitter(), CVCL::DecisionEngineCaching::findSplitter(), CVCL::DecisionEngineMBTF::goalSatisfied(), CVCL::DecisionEngineCaching::goalSatisfied(), CVCL::TheoryQuant::goodSynMatch(), CVCL::TheoryArith::VarOrderGraph::lessThan(), CVCL::ExprStream::popDag(), CVCL::TheoryBitvector::pushNegation(), and CVCL::ExprTransform::pushNegation().

template<class Data> void CVCL::ExprMap< Data >::insert (  const Expr &  e, const Data &  d )  [inline]

Definition at line 142 of file expr_map.h. Referenced by CVCL::BitvectorTheoremProducer::computeCarryPreComputed(), CVCL::VCCmd::findAxioms(), and CVCL::TheoryDatatype::parseExprOp().

template<class Data> void CVCL::ExprMap< Data >::erase (  const Expr &  e  )  [inline]

Definition at line 143 of file expr_map.h. Referenced by CVCL::ExprStream::popDag().

template<class Data> template<class InputIterator> void CVCL::ExprMap< Data >::insert (  InputIterator  l, InputIterator  r )  [inline]

Definition at line 146 of file expr_map.h.

template<class Data> template<class InputIterator> void CVCL::ExprMap< Data >::erase (  InputIterator  l, InputIterator  r )  [inline]

Definition at line 149 of file expr_map.h.

template<class Data> iterator CVCL::ExprMap< Data >::begin (   )  const [inline]

Definition at line 155 of file expr_map.h. Referenced by CVCL::ExprStream::addLetHeader(), TheoryCore::assertEqualities(), CVCL::ArithTheoremProducer::canonComboLikeTerms(), CVCL::TheoryDatatypeLazy::checkSat(), CVCL::TheoryDatatype::checkSat(), CVCL::BitvectorTheoremProducer::createNewPlusCollection(), CVCL::TheoryArith::VarOrderGraph::dfs(), CVCL::VCCmd::evaluateCommand(), CVCL::TheoryDatatype::getConstant(), CVCL::TheoryDatatypeLazy::instantiate(), CVCL::TheoryDatatype::instantiate(), CVCL::TheoryBitvector::pushNegationRec(), CVCL::ExprTransform::pushNegationRec(), CVCL::CommonTheoremProducer::rewriteAnd(), CVCL::CommonTheoremProducer::rewriteOr(), and CVCL::TheoryArith::~TheoryArith().

template<class Data> iterator CVCL::ExprMap< Data >::end (   )  const [inline]

Definition at line 156 of file expr_map.h. Referenced by CVCL::ExprStream::addLetHeader(), TheoryCore::assertEqualities(), CVCL::TheoryUF::assertFact(), CVCL::ArithTheoremProducer::canonComboLikeTerms(), CVCL::TheoryDatatypeLazy::checkSat(), CVCL::TheoryDatatype::checkSat(), CVCL::BitvectorTheoremProducer::collectOneTermOfPlus(), CVCL::BitvectorTheoremProducer::computeCarryPreComputed(), CVCL::BitvectorTheoremProducer::createNewPlusCollection(), CVCL::VCCmd::evaluateCommand(), CVCL::DecisionEngine::findSplitterRec(), SAT::CNF_Manager::getCNFLit(), CVCL::TheoryDatatype::getConsForTester(), CVCL::TheoryDatatype::getConsPos(), CVCL::TheoryDatatype::getConstant(), CVCL::TheoryDatatype::getReachablePredicate(), CVCL::TheoryDatatype::getSelectorInfo(), CVCL::DecisionEngineMBTF::goalSatisfied(), CVCL::DecisionEngineCaching::goalSatisfied(), CVCL::TheoryQuant::goodSynMatch(), CVCL::TheoryDatatypeLazy::initializeLabels(), CVCL::TheoryDatatype::initializeLabels(), CVCL::TheoryDatatypeLazy::instantiate(), CVCL::TheoryDatatype::instantiate(), CVCL::DecisionEngineMBTF::isBetter(), CVCL::DecisionEngineCaching::isBetter(), CVCL::operator<<(), CVCL::Translator::preprocessRec(), CVCL::TheoryArith::processFiniteIntervals(), CVCL::TheoryArith::projectInequalities(), CVCL::TheoryBitvector::pushNegationRec(), CVCL::ExprTransform::pushNegationRec(), CVCL::TheoryQuant::recSynMatch(), SAT::CNF_Manager::replaceITErec(), CVCL::CommonTheoremProducer::rewriteAnd(), CVCL::TheoryBitvector::rewriteBV(), CVCL::CommonTheoremProducer::rewriteOr(), CVCL::BitvectorTheoremProducer::sameKidCheck(), CVCL::TheoryArith::substAndCanonize(), CVCL::ArithTheoremProducer::substitute(), SAT::CNF_Manager::translateExprRec(), and CVCL::TheoryArith::~TheoryArith().

template<class Data> iterator CVCL::ExprMap< Data >::find (  const Expr &  e  )  const [inline]

Definition at line 157 of file expr_map.h. Referenced by CVCL::TheoryUF::assertFact(), CVCL::TheoryDatatypeLazy::checkSat(), CVCL::TheoryDatatype::checkSat(), CVCL::BitvectorTheoremProducer::collectOneTermOfPlus(), CVCL::BitvectorTheoremProducer::computeCarryPreComputed(), CVCL::DecisionEngine::findSplitterRec(), SAT::CNF_Manager::getCNFLit(), CVCL::TheoryDatatype::getConsForTester(), CVCL::TheoryDatatype::getConsPos(), CVCL::TheoryDatatype::getConstant(), CVCL::TheoryDatatype::getReachablePredicate(), CVCL::TheoryDatatype::getSelectorInfo(), CVCL::DecisionEngineMBTF::goalSatisfied(), CVCL::DecisionEngineCaching::goalSatisfied(), CVCL::TheoryQuant::goodSynMatch(), CVCL::TheoryDatatypeLazy::initializeLabels(), CVCL::TheoryDatatype::initializeLabels(), CVCL::TheoryDatatypeLazy::instantiate(), CVCL::TheoryDatatype::instantiate(), CVCL::DecisionEngineMBTF::isBetter(), CVCL::DecisionEngineCaching::isBetter(), CVCL::operator<<(), CVCL::Translator::preprocessRec(), CVCL::TheoryArith::processFiniteIntervals(), CVCL::TheoryArith::projectInequalities(), CVCL::TheoryBitvector::pushNegationRec(), CVCL::ExprTransform::pushNegationRec(), CVCL::TheoryQuant::recSynMatch(), SAT::CNF_Manager::replaceITErec(), CVCL::TheoryBitvector::rewriteBV(), CVCL::BitvectorTheoremProducer::sameKidCheck(), CVCL::TheoryArith::substAndCanonize(), CVCL::ArithTheoremProducer::substitute(), and SAT::CNF_Manager::translateExprRec().

---

Friends And Related Function Documentation

template<class Data> bool operator== (  const ExprMap< Data > &  m1, const ExprMap< Data > &  m2 )  [friend]

Definition at line 159 of file expr_map.h.

template<class Data> bool operator!= (  const ExprMap< Data > &  m1, const ExprMap< Data > &  m2 )  [friend]

Definition at line 162 of file expr_map.h.

---

Member Data Documentation

template<class Data> ExprMapType CVCL::ExprMap< Data >::d_map [private]

Definition at line 75 of file expr_map.h. Referenced by CVCL::ExprMap< std::vector< Expr > >::begin(), CVCL::ExprMap< std::vector< Expr > >::clear(), CVCL::ExprMap< std::vector< Expr > >::count(), CVCL::ExprMap< std::vector< Expr > >::empty(), CVCL::ExprMap< std::vector< Expr > >::end(), CVCL::ExprMap< std::vector< Expr > >::erase(), CVCL::ExprMap< std::vector< Expr > >::find(), CVCL::ExprMap< std::vector< Expr > >::insert(), CVCL::ExprMap< std::vector< Expr > >::operator[](), and CVCL::ExprMap< std::vector< Expr > >::size().

---

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

• expr_map.h

---