#include <expr_map.h>
Inheritance diagram for CVC3::ExprMap< Data >:
Definition at line 62 of file expr_map.h.
typedef std::map<Expr, Data> CVC3::ExprMap< Data >::ExprMapType [private] |
Definition at line 65 of file expr_map.h.
CVC3::ExprMap< Data >::ExprMap | ( | ) | [inline] |
Definition at line 122 of file expr_map.h.
CVC3::ExprMap< Data >::ExprMap | ( | const ExprMap< Data > & | map | ) | [inline] |
Definition at line 124 of file expr_map.h.
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().
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().
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().
Data& CVC3::ExprMap< Data >::operator[] | ( | const Expr & | e | ) | [inline] |
Definition at line 131 of file expr_map.h.
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().
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().
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().
void CVC3::ExprMap< Data >::insert | ( | InputIterator | l, | |
InputIterator | r | |||
) | [inline] |
Definition at line 138 of file expr_map.h.
void CVC3::ExprMap< Data >::erase | ( | InputIterator | l, | |
InputIterator | r | |||
) | [inline] |
Definition at line 141 of file expr_map.h.
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().
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().
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().
bool operator== | ( | const ExprMap< Data > & | m1, | |
const ExprMap< Data > & | m2 | |||
) | [friend] |
Definition at line 151 of file expr_map.h.
bool operator!= | ( | const ExprMap< Data > & | m1, | |
const ExprMap< Data > & | m2 | |||
) | [friend] |
Definition at line 154 of file expr_map.h.
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().