CVC3
Classes | Public Member Functions | Private Types | Private Attributes | Friends | List of all members
CVC3::ExprMap< Data > Class Template Reference

#include <expr_map.h>

Collaboration diagram for CVC3::ExprMap< Data >:
Collaboration graph

Classes

class  const_iterator
 
class  iterator
 

Public Member Functions

 ExprMap ()
 
 ExprMap (const ExprMap &map)
 
bool empty () const
 
size_t size () const
 
size_t 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 ()
 
iterator end ()
 
const_iterator begin () const
 
const_iterator end () const
 
iterator find (const Expr &e)
 
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)
 

Detailed Description

template<class Data>
class CVC3::ExprMap< Data >

Definition at line 62 of file expr_map.h.

Member Typedef Documentation

template<class Data>
typedef std::map<Expr, Data> CVC3::ExprMap< Data >::ExprMapType
private

Definition at line 65 of file expr_map.h.

Constructor & Destructor Documentation

template<class Data>
CVC3::ExprMap< Data >::ExprMap ( )
inline

Definition at line 165 of file expr_map.h.

template<class Data>
CVC3::ExprMap< Data >::ExprMap ( const ExprMap< Data > &  map)
inline

Definition at line 167 of file expr_map.h.

Member Function Documentation

template<class Data>
bool CVC3::ExprMap< Data >::empty ( ) const
inline
template<class Data>
size_t CVC3::ExprMap< Data >::size ( ) const
inline
template<class Data>
size_t CVC3::ExprMap< Data >::count ( const Expr e) const
inline
template<class Data>
Data& CVC3::ExprMap< Data >::operator[] ( const Expr e)
inline

Definition at line 174 of file expr_map.h.

template<class Data>
void CVC3::ExprMap< Data >::clear ( )
inline
template<class Data>
void CVC3::ExprMap< Data >::insert ( const Expr e,
const Data &  d 
)
inline
template<class Data>
void CVC3::ExprMap< Data >::erase ( const Expr e)
inline
template<class Data>
template<class InputIterator >
void CVC3::ExprMap< Data >::insert ( InputIterator  l,
InputIterator  r 
)
inline

Definition at line 181 of file expr_map.h.

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

Definition at line 184 of file expr_map.h.

template<class Data>
iterator CVC3::ExprMap< Data >::begin ( )
inline

Definition at line 190 of file expr_map.h.

Referenced by CVC3::ExprStream::addLetHeader(), CVC3::TheoryDatatype::assertFact(), CVC3::BitvectorTheoremProducer::bitwiseFlatten(), CVC3::BitvectorTheoremProducer::buildPlusTerm(), CVC3::BitvectorTheoremProducer::BVMult_order_subterms(), CVC3::BitvectorTheoremProducer::canonBVEQ(), CVC3::ArithTheoremProducer3::canonComboLikeTerms(), CVC3::ArithTheoremProducerOld::canonComboLikeTerms(), CVC3::ArithTheoremProducer::canonComboLikeTerms(), CVC3::TheoryDatatypeLazy::checkSat(), CVC3::TheoryArray::checkSat(), CVC3::TheoryDatatype::checkSat(), CVC3::TheoryQuant::checkSat(), CVC3::CompleteInstPreProcessor::collect_forall_index(), CVC3::TheoryQuant::collectChangedTerms(), CVC3::CompleteInstPreProcessor::collectIndex(), CVC3::TheoryQuant::combineOldNewTrigs(), CVC3::BitvectorTheoremProducer::createNewPlusCollection(), CVC3::TheoryDatatype::dataType(), CVC3::TheoryQuant::delNewTrigs(), CVC3::VCCmd::evaluateCommand(), CVC3::TheoryDatatype::finiteTypeInfo(), CVC3::TheoryDatatype::getConstant(), CVC3::TheoryArithOld::VarOrderGraph::getVerticesTopological(), CVC3::TheoryDatatypeLazy::instantiate(), CVC3::TheoryDatatype::instantiate(), CVC3::CompleteInstPreProcessor::isGood(), CVC3::CompleteInstPreProcessor::isGoodQuant(), LFSCConvert::make_let_proof(), CVC3::TheoryQuant::matchListNew(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::TheoryDatatype::print(), LFSCPrinter::print_LFSC(), CVC3::VCCmd::printCounterExample(), CVC3::VCCmd::printModel(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::CommonTheoremProducer::rewriteOr(), CVC3::TheoryQuant::simplifyExprMap(), CVC3::TheoryArithNew::solvedForm(), CVC3::TheoryArith3::solvedForm(), CVC3::TheoryArithOld::solvedForm(), CVC3::TheoryQuant::synNewInst(), CVC3::TheoryArithOld::DifferenceLogicGraph::~DifferenceLogicGraph(), CVC3::TheoryArith3::~TheoryArith3(), CVC3::TheoryArithNew::~TheoryArithNew(), and CVC3::TheoryArithOld::~TheoryArithOld().

template<class Data>
iterator CVC3::ExprMap< Data >::end ( )
inline

Definition at line 191 of file expr_map.h.

Referenced by CVC3::TheoryQuant::add_parent(), CVC3::ExprStream::addLetHeader(), CVC3::TheoryUF::assertFact(), CVC3::TheoryDatatype::assertFact(), CVC3::BitvectorTheoremProducer::bitwiseFlatten(), CVC3::BitvectorTheoremProducer::buildPlusTerm(), CVC3::BitvectorTheoremProducer::BVMult_order_subterms(), LFSCObj::can_pnorm(), CVC3::BitvectorTheoremProducer::canonBVEQ(), CVC3::ArithTheoremProducer3::canonComboLikeTerms(), CVC3::ArithTheoremProducerOld::canonComboLikeTerms(), CVC3::ArithTheoremProducer::canonComboLikeTerms(), LFSCObj::cascade_expr(), CVC3::TheoryDatatypeLazy::checkSat(), CVC3::TheoryArray::checkSat(), CVC3::TheoryDatatype::checkSat(), CVC3::TheoryQuant::checkSat(), CVC3::CompleteInstPreProcessor::collect_forall_index(), CVC3::TheoryQuant::collectChangedTerms(), CVC3::CompleteInstPreProcessor::collectIndex(), CVC3::BitvectorTheoremProducer::collectOneTermOfPlus(), CVC3::TheoryQuant::combineOldNewTrigs(), CVC3::BitvectorTheoremProducer::computeCarryPreComputed(), CVC3::TheoryArithOld::computeTermBounds(), CVC3::BitvectorTheoremProducer::createNewPlusCollection(), CVC3::TheoryArithOld::currentMaxCoefficient(), LFSCConvert::cvc3_to_lfsc(), CVC3::TheoryDatatype::dataType(), CVC3::TheoryQuant::delNewTrigs(), CVC3::TheoryQuant::enqueueInst(), CVC3::VCCmd::evaluateCommand(), CVC3::SearchEngineTheoremProducer::findInLocalCache(), CVC3::DecisionEngine::findSplitterRec(), CVC3::TheoryDatatype::finiteTypeInfo(), CVC3::TheoryDatatype::getConsForTester(), CVC3::TheoryDatatype::getConsPos(), CVC3::TheoryDatatype::getConstant(), LFSCObj::getNumNodes(), CVC3::TheoryDatatype::getReachablePredicate(), CVC3::TheoryDatatype::getSelectorInfo(), CVC3::TheoryQuant::getSubTerms(), CVC3::Theory::getTCC(), CVC3::TheoryArithOld::VarOrderGraph::getVerticesTopological(), goodMultiTriggers(), CVC3::TheoryDatatypeLazy::initializeLabels(), CVC3::TheoryDatatype::initializeLabels(), CVC3::TheoryDatatypeLazy::instantiate(), CVC3::TheoryDatatype::instantiate(), LFSCObj::isFormula(), CVC3::CompleteInstPreProcessor::isGood(), CVC3::CompleteInstPreProcessor::isGoodQuant(), LFSCPrinter::make_let_map(), LFSCConvert::make_let_proof(), CVC3::TheoryQuant::matchListNew(), CVC3::TheoryQuant::matchListOld(), CVC3::TheoryQuant::multMatchChild(), CVC3::ExprTransform::newPPrec(), CVC3::operator<<(), CVC3::TheoryCore::parseExpr(), CVC3::TheoryCore::parseExprOp(), CVC3::Translator::preprocess2Rec(), CVC3::Translator::preprocessRec(), CVC3::TheoryDatatype::print(), LFSCPrinter::print_LFSC(), LFSCPrinter::print_poly_norm(), CVC3::VCCmd::printCounterExample(), CVC3::VCCmd::printModel(), CVC3::VCCmd::printSymbols(), CVC3::TheoryArithNew::processFiniteIntervals(), CVC3::TheoryArith3::processFiniteIntervals(), CVC3::TheoryArithOld::processFiniteIntervals(), CVC3::TheoryArith3::projectInequalities(), CVC3::TheoryArithOld::projectInequalities(), CVC3::ExprTransform::pushNegationRec(), CVC3::TheoryQuant::recMultMatch(), CVC3::TheoryQuant::recMultMatchDebug(), CVC3::TheoryQuant::recMultMatchOldWay(), CVC3::CompleteInstPreProcessor::recRewriteNot(), CVC3::TheoryQuant::registerTrig(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::TheoryBitvector::rewriteBV(), CVC3::CommonTheoremProducer::rewriteOr(), CVC3::BitvectorTheoremProducer::sameKidCheck(), CVC3::TheoryQuant::sendInstNew(), CVC3::TheoryQuant::simplifyExprMap(), CVC3::ExprTransform::simplifyWithCare(), CVC3::ExprTransform::smartSimplify(), CVC3::TheoryArithNew::solvedForm(), CVC3::TheoryArith3::solvedForm(), CVC3::TheoryArithOld::solvedForm(), CVC3::TheoryArithNew::substAndCanonize(), CVC3::TheoryArith3::substAndCanonize(), CVC3::TheoryArithOld::substAndCanonize(), CVC3::ArithTheoremProducerOld::substitute(), CVC3::ArithTheoremProducer3::substitute(), CVC3::ArithTheoremProducer::substitute(), CVC3::TheoryQuant::synNewInst(), CVC3::TheoryArithOld::tryPropagate(), CVC3::TheoryArithOld::updateStats(), CVC3::TheoryArith3::~TheoryArith3(), CVC3::TheoryArithNew::~TheoryArithNew(), and CVC3::TheoryArithOld::~TheoryArithOld().

template<class Data>
const_iterator CVC3::ExprMap< Data >::begin ( ) const
inline

Definition at line 192 of file expr_map.h.

template<class Data>
const_iterator CVC3::ExprMap< Data >::end ( ) const
inline

Definition at line 193 of file expr_map.h.

template<class Data>
iterator CVC3::ExprMap< Data >::find ( const Expr e)
inline

Definition at line 194 of file expr_map.h.

Referenced by CVC3::TheoryQuant::add_parent(), CVC3::TheoryUF::assertFact(), LFSCObj::can_pnorm(), LFSCObj::cascade_expr(), CVC3::TheoryDatatypeLazy::checkSat(), CVC3::TheoryDatatype::checkSat(), CVC3::TheoryQuant::collectChangedTerms(), CVC3::BitvectorTheoremProducer::collectOneTermOfPlus(), CVC3::TheoryQuant::combineOldNewTrigs(), CVC3::BitvectorTheoremProducer::computeCarryPreComputed(), CVC3::TheoryBitvector::computeTCC(), CVC3::TheoryArithOld::computeTermBounds(), CVC3::TheoryArithOld::currentMaxCoefficient(), LFSCConvert::cvc3_to_lfsc(), CVC3::TheoryQuant::enqueueInst(), CVC3::SearchEngineTheoremProducer::findInLocalCache(), CVC3::DecisionEngine::findSplitterRec(), CVC3::TheoryDatatype::getConsForTester(), CVC3::TheoryDatatype::getConsPos(), CVC3::TheoryDatatype::getConstant(), LFSCObj::getNumNodes(), CVC3::TheoryDatatype::getReachablePredicate(), CVC3::TheoryDatatype::getSelectorInfo(), CVC3::TheoryQuant::getSubTerms(), CVC3::Theory::getTCC(), goodMultiTriggers(), CVC3::TheoryDatatypeLazy::initializeLabels(), CVC3::TheoryDatatype::initializeLabels(), CVC3::TheoryDatatypeLazy::instantiate(), CVC3::TheoryDatatype::instantiate(), LFSCObj::isFormula(), LFSCPrinter::make_let_map(), CVC3::TheoryQuant::matchListNew(), CVC3::TheoryQuant::matchListOld(), CVC3::TheoryQuant::multMatchChild(), CVC3::ExprTransform::newPPrec(), CVC3::operator<<(), CVC3::TheoryCore::parseExpr(), CVC3::TheoryCore::parseExprOp(), CVC3::Translator::preprocess2Rec(), CVC3::Translator::preprocessRec(), CVC3::TheoryDatatype::print(), LFSCPrinter::print_poly_norm(), CVC3::VCCmd::printSymbols(), CVC3::TheoryArithNew::processFiniteIntervals(), CVC3::TheoryArith3::processFiniteIntervals(), CVC3::TheoryArithOld::processFiniteIntervals(), CVC3::TheoryArith3::projectInequalities(), CVC3::TheoryArithOld::projectInequalities(), CVC3::ExprTransform::pushNegationRec(), CVC3::TheoryBitvector::pushNegationRec(), CVC3::TheoryQuant::recMultMatch(), CVC3::TheoryQuant::recMultMatchDebug(), CVC3::TheoryQuant::recMultMatchOldWay(), CVC3::CompleteInstPreProcessor::recRewriteNot(), CVC3::TheoryQuant::registerTrig(), CVC3::TheoryBitvector::rewriteBV(), CVC3::BitvectorTheoremProducer::sameKidCheck(), CVC3::TheoryQuant::sendInstNew(), CVC3::ExprTransform::smartSimplify(), CVC3::TheoryArithNew::substAndCanonize(), CVC3::TheoryArith3::substAndCanonize(), CVC3::TheoryArithOld::substAndCanonize(), CVC3::ArithTheoremProducerOld::substitute(), CVC3::ArithTheoremProducer3::substitute(), CVC3::ArithTheoremProducer::substitute(), CVC3::TheoryArithOld::tryPropagate(), CVC3::ExprTransform::updateQueue(), and CVC3::TheoryArithOld::updateStats().

template<class Data>
const_iterator CVC3::ExprMap< Data >::find ( const Expr e) const
inline

Definition at line 195 of file expr_map.h.

Friends And Related Function Documentation

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

Definition at line 197 of file expr_map.h.

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

Definition at line 200 of file expr_map.h.

Member Data Documentation

template<class Data>
ExprMapType CVC3::ExprMap< Data >::d_map
private

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