CVC3::ExprMap< Data > Class Template Reference

#include <expr_map.h>

Inheritance diagram for CVC3::ExprMap< Data >:

[legend]Collaboration diagram for CVC3::ExprMap< Data >:

[legend]List of all members.

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 () 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 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 122 of file expr_map.h.

template<class Data>

CVC3::ExprMap< Data >::ExprMap

(

const ExprMap< Data > &

map

)

[inline]

Definition at line 124 of file expr_map.h.

---

Member Function Documentation

template<class Data>

bool CVC3::ExprMap< Data >::empty

(

)

const [inline]

Definition at line 127 of file expr_map.h.

Referenced by CVC3::BitvectorTheoremProducer::collectOneTermOfPlus(), CVC3::TheoryArithOld::substAndCanonize(), and CVC3::TheoryArithNew::substAndCanonize().

template<class Data>

size_t CVC3::ExprMap< Data >::size

(

)

const [inline]

Definition at line 128 of file expr_map.h.

Referenced by CVC3::ExprStream::addLetHeader(), CVC3::TheoryQuant::goodSynMatch(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::CommonTheoremProducer::rewriteOr(), and CVC3::TheoryCore::simplify().

template<class Data>

size_t CVC3::ExprMap< Data >::count

(

const Expr &

e

)

const [inline]

Definition at line 130 of file expr_map.h.

Referenced by CVC3::QuantTheoremProducer::adjustVarUniv(), CVC3::ArithTheoremProducerOld::canonComboLikeTerms(), CVC3::ArithTheoremProducer::canonComboLikeTerms(), CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVC3::ExprStream::collectShared(), CVC3::TheoryArithOld::VarOrderGraph::dfs(), CVC3::TheoryArithNew::VarOrderGraph::dfs(), CVC3::VCCmd::findAxioms(), CVC3::TheoryQuant::findInstAssumptions(), findPolarity(), genPartInstSetThm(), CVC3::DecisionEngineCaching::goalSatisfied(), CVC3::TheoryDatatype::parseExprOp(), CVC3::QuantTheoremProducer::recFindBoundVars(), CVC3::TheoryQuant::recursiveMap(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::CommonTheoremProducer::rewriteOr(), CVC3::TheoryQuant::setupTriggers(), and CVC3::TheoryCore::simplify().

template<class Data>

Data& CVC3::ExprMap< Data >::operator[]

(

const Expr &

e

)

[inline]

Definition at line 131 of file expr_map.h.

template<class Data>

void CVC3::ExprMap< Data >::clear

(

)

[inline]

Definition at line 132 of file expr_map.h.

Referenced by CVC3::ExprStream::addLetHeader(), CVC3::BitvectorTheoremProducer::collectLikeTermsOfPlus(), CVC3::TheoryQuant::goodSynMatch(), CVC3::TheoryArithOld::VarOrderGraph::lessThan(), CVC3::TheoryArithNew::VarOrderGraph::lessThan(), and CVC3::ExprStream::popDag().

template<class Data>

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

Definition at line 134 of file expr_map.h.

Referenced by CVC3::QuantTheoremProducer::adjustVarUniv(), CVC3::VCCmd::findAxioms(), and CVC3::TheoryDatatype::parseExprOp().

template<class Data>

void CVC3::ExprMap< Data >::erase

(

const Expr &

e

)

[inline]

Definition at line 135 of file expr_map.h.

Referenced by CVC3::ExprStream::popDag(), and CVC3::TheoryCore::simplify().

template<class Data>

template<class InputIterator>

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

Definition at line 138 of file expr_map.h.

template<class Data>

template<class InputIterator>

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

Definition at line 141 of file expr_map.h.

template<class Data>

iterator CVC3::ExprMap< Data >::begin

(

)

const [inline]

Definition at line 147 of file expr_map.h.

Referenced by CVC3::ExprStream::addLetHeader(), CVC3::ArithTheoremProducerOld::canonComboLikeTerms(), CVC3::ArithTheoremProducer::canonComboLikeTerms(), CVC3::TheoryQuant::collectChangedTerms(), CVC3::TheoryQuant::combineOldNewTrigs(), CVC3::BitvectorTheoremProducer::createNewPlusCollection(), CVC3::TheoryQuant::delNewTrigs(), CVC3::VCCmd::evaluateCommand(), CVC3::TheoryDatatype::getConstant(), CVC3::TheoryQuant::matchListNew(), CVC3::TheoryQuant::matchListOld(), CVC3::TheoryBitvector::pushNegationRec(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::CommonTheoremProducer::rewriteOr(), CVC3::TheoryArithOld::solvedForm(), and CVC3::TheoryArithNew::solvedForm().

template<class Data>

iterator CVC3::ExprMap< Data >::end

(

)

const [inline]

Definition at line 148 of file expr_map.h.

Referenced by CVC3::ExprStream::addLetHeader(), CVC3::ArithTheoremProducerOld::canonComboLikeTerms(), CVC3::ArithTheoremProducer::canonComboLikeTerms(), CVC3::TheoryQuant::collectChangedTerms(), CVC3::BitvectorTheoremProducer::collectOneTermOfPlus(), CVC3::BitvectorTheoremProducer::createNewPlusCollection(), CVC3::VCCmd::evaluateCommand(), CVC3::SearchEngineTheoremProducer::findInLocalCache(), CVC3::DecisionEngineMBTF::goalSatisfied(), CVC3::DecisionEngineCaching::goalSatisfied(), goodMultiTriggers(), CVC3::TheoryQuant::goodSynMatch(), CVC3::DecisionEngineMBTF::isBetter(), CVC3::DecisionEngineCaching::isBetter(), CVC3::TheoryQuant::matchChild(), CVC3::operator<<(), CVC3::Translator::preprocess2Rec(), CVC3::Translator::preprocessRec(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryQuant::recGeneralTrig(), CVC3::TheoryQuant::recSynMatch(), CVC3::TheoryQuant::registerTrig(), SAT::CNF_Manager::replaceITErec(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::TheoryBitvector::rewriteBV(), CVC3::CommonTheoremProducer::rewriteOr(), CVC3::BitvectorTheoremProducer::sameKidCheck(), CVC3::ExprTransform::smartSimplify(), CVC3::TheoryArithOld::solvedForm(), CVC3::TheoryArithNew::solvedForm(), CVC3::TheoryArithOld::substAndCanonize(), CVC3::TheoryArithNew::substAndCanonize(), CVC3::ArithTheoremProducerOld::substitute(), and CVC3::ArithTheoremProducer::substitute().

template<class Data>

iterator CVC3::ExprMap< Data >::find

(

const Expr &

e

)

const [inline]

Definition at line 149 of file expr_map.h.

Referenced by CVC3::BitvectorTheoremProducer::collectOneTermOfPlus(), CVC3::SearchEngineTheoremProducer::findInLocalCache(), CVC3::DecisionEngineMBTF::goalSatisfied(), CVC3::DecisionEngineCaching::goalSatisfied(), goodMultiTriggers(), CVC3::TheoryQuant::goodSynMatch(), CVC3::DecisionEngineMBTF::isBetter(), CVC3::DecisionEngineCaching::isBetter(), CVC3::TheoryQuant::matchChild(), CVC3::TheoryQuant::matchListNew(), CVC3::TheoryQuant::matchListOld(), CVC3::operator<<(), CVC3::Translator::preprocess2Rec(), CVC3::Translator::preprocessRec(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryQuant::recGeneralTrig(), CVC3::TheoryQuant::recSynMatch(), CVC3::TheoryQuant::registerTrig(), SAT::CNF_Manager::replaceITErec(), CVC3::TheoryBitvector::rewriteBV(), CVC3::BitvectorTheoremProducer::sameKidCheck(), CVC3::ExprTransform::smartSimplify(), CVC3::TheoryArithOld::substAndCanonize(), CVC3::TheoryArithNew::substAndCanonize(), CVC3::ArithTheoremProducerOld::substitute(), and CVC3::ArithTheoremProducer::substitute().

---

Friends And Related Function Documentation

template<class Data>

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

Definition at line 151 of file expr_map.h.

template<class Data>

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

Definition at line 154 of file expr_map.h.

---

Member Data Documentation

template<class Data>

ExprMapType CVC3::ExprMap< Data >::d_map [private]

Definition at line 67 of file expr_map.h.

Referenced by CVC3::ExprMap< CVC3::Op >::begin(), CVC3::ExprMap< CVC3::Op >::clear(), CVC3::ExprMap< CVC3::Op >::count(), CVC3::ExprMap< CVC3::Op >::empty(), CVC3::ExprMap< CVC3::Op >::end(), CVC3::ExprMap< CVC3::Op >::erase(), CVC3::ExprMap< CVC3::Op >::find(), CVC3::ExprMap< CVC3::Op >::insert(), CVC3::ExprMap< CVC3::Op >::operator[](), and CVC3::ExprMap< CVC3::Op >::size().

---

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

• expr_map.h

---