CVC3
2.4.1
|
#include <expr_map.h>
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) |
Definition at line 62 of file expr_map.h.
|
private |
Definition at line 65 of file expr_map.h.
|
inline |
Definition at line 165 of file expr_map.h.
|
inline |
Definition at line 167 of file expr_map.h.
|
inline |
Definition at line 170 of file expr_map.h.
Referenced by CVC3::Theory::addBoundVar(), CVC3::BitvectorTheoremProducer::collectOneTermOfPlus(), LFSCConvert::make_let_proof(), LFSCPrinter::print_LFSC(), CVC3::ExprTransform::simplifyWithCare(), CVC3::TheoryArithNew::substAndCanonize(), CVC3::TheoryArith3::substAndCanonize(), and CVC3::TheoryArithOld::substAndCanonize().
|
inline |
Definition at line 171 of file expr_map.h.
Referenced by CVC3::ExprStream::addLetHeader(), CVC3::TheoryQuant::checkSat(), CVC3::TheoryDatatype::getConstant(), CVC3::CommonTheoremProducer::rewriteAnd(), and CVC3::CommonTheoremProducer::rewriteOr().
|
inline |
Definition at line 173 of file expr_map.h.
Referenced by CVC3::QuantTheoremProducer::adjustVarUniv(), CVC3::TheoryQuant::backList(), CVC3::QuantTheoremProducer::boundVarElim(), CVC3::BitvectorTheoremProducer::BVMult_order_subterms(), CVC3::ArithTheoremProducer3::canonComboLikeTerms(), CVC3::ArithTheoremProducerOld::canonComboLikeTerms(), CVC3::ArithTheoremProducer::canonComboLikeTerms(), CVC3::TheoryQuant::checkSat(), CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVC3::ExprStream::collectShared(), CVC3::VCCmd::findAxioms(), CVC3::TheoryQuant::findInstAssumptions(), findPolarity(), findPolarityAtomic(), CVC3::DecisionEngine::findSplitterRec(), CVC3::TheoryDatatype::finiteTypeInfo(), CVC3::TheoryQuant::forwList(), CVC3::TheoryDatatype::getConstant(), CVC3::CompleteInstPreProcessor::inst(), CVC3::CompleteInstPreProcessor::isMacro(), CVC3::TheoryDatatype::parseExprOp(), CVC3::TheoryQuant::pushBackList(), CVC3::TheoryQuant::pushForwList(), CVC3::QuantTheoremProducer::recFindBoundVars(), CVC3::CompleteInstPreProcessor::recInstMacros(), CVC3::TheoryQuant::recMultMatchDebug(), CVC3::TheoryQuant::recMultMatchOldWay(), CVC3::TheoryQuant::recursiveMap(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::CommonTheoremProducer::rewriteOr(), CVC3::TheoryQuant::setupTriggers(), and CVC3::CompleteInstPreProcessor::substMacro().
|
inline |
Definition at line 174 of file expr_map.h.
|
inline |
Definition at line 175 of file expr_map.h.
Referenced by CVC3::Theory::addBoundVar(), CVC3::ExprStream::addLetHeader(), CVC3::BitvectorTheoremProducer::collectLikeTermsOfPlus(), CVC3::TheoryQuant::delNewTrigs(), CVC3::DecisionEngineDFS::findSplitter(), CVC3::TheoryCore::parseExpr(), and CVC3::ExprStream::popDag().
|
inline |
Definition at line 177 of file expr_map.h.
Referenced by CVC3::BitvectorTheoremProducer::computeCarryPreComputed(), CVC3::VCCmd::findAxioms(), CVC3::TheoryDatatype::parseExprOp(), and CVC3::TheoryArithOld::registerAtom().
|
inline |
Definition at line 178 of file expr_map.h.
Referenced by CVC3::BitvectorTheoremProducer::bitwiseFlatten(), CVC3::TheoryDatatype::finiteTypeInfo(), CVC3::ExprStream::popDag(), and CVC3::ExprTransform::simplifyWithCare().
|
inline |
Definition at line 181 of file expr_map.h.
|
inline |
Definition at line 184 of file expr_map.h.
|
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(), and CVC3::TheoryArithOld::DifferenceLogicGraph::~DifferenceLogicGraph().
|
inline |
Definition at line 191 of file expr_map.h.
Referenced by CVC3::TheoryQuant::add_parent(), CVC3::ExprStream::addLetHeader(), 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::TheoryArray::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::BitvectorTheoremProducer::createNewPlusCollection(), LFSCConvert::cvc3_to_lfsc(), CVC3::TheoryDatatype::dataType(), CVC3::TheoryQuant::delNewTrigs(), CVC3::VCCmd::evaluateCommand(), CVC3::SearchEngineTheoremProducer::findInLocalCache(), CVC3::DecisionEngine::findSplitterRec(), CVC3::TheoryDatatype::finiteTypeInfo(), CVC3::TheoryDatatype::getConsForTester(), LFSCObj::getNumNodes(), CVC3::Theory::getTCC(), CVC3::TheoryArithOld::VarOrderGraph::getVerticesTopological(), goodMultiTriggers(), LFSCObj::isFormula(), CVC3::CompleteInstPreProcessor::isGood(), CVC3::CompleteInstPreProcessor::isGoodQuant(), LFSCPrinter::make_let_map(), LFSCConvert::make_let_proof(), CVC3::TheoryQuant::matchListNew(), CVC3::TheoryQuant::multMatchChild(), CVC3::operator<<(), CVC3::TheoryCore::parseExpr(), CVC3::TheoryCore::parseExprOp(), CVC3::Translator::preprocess2Rec(), CVC3::Translator::preprocessRec(), LFSCPrinter::print_LFSC(), LFSCPrinter::print_poly_norm(), CVC3::VCCmd::printCounterExample(), CVC3::VCCmd::printModel(), CVC3::VCCmd::printSymbols(), CVC3::TheoryArith3::projectInequalities(), CVC3::TheoryArithOld::projectInequalities(), 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::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::ArithTheoremProducer::substitute(), CVC3::ArithTheoremProducer3::substitute(), CVC3::TheoryQuant::synNewInst(), and CVC3::TheoryArithOld::tryPropagate().
|
inline |
Definition at line 192 of file expr_map.h.
|
inline |
Definition at line 193 of file expr_map.h.
|
inline |
Definition at line 194 of file expr_map.h.
Referenced by CVC3::TheoryQuant::add_parent(), LFSCObj::can_pnorm(), LFSCObj::cascade_expr(), CVC3::TheoryQuant::collectChangedTerms(), CVC3::BitvectorTheoremProducer::collectOneTermOfPlus(), CVC3::BitvectorTheoremProducer::computeCarryPreComputed(), CVC3::TheoryBitvector::computeTCC(), LFSCConvert::cvc3_to_lfsc(), CVC3::SearchEngineTheoremProducer::findInLocalCache(), CVC3::DecisionEngine::findSplitterRec(), CVC3::TheoryDatatype::getConsForTester(), LFSCObj::getNumNodes(), CVC3::Theory::getTCC(), goodMultiTriggers(), LFSCObj::isFormula(), LFSCPrinter::make_let_map(), CVC3::TheoryQuant::matchListNew(), CVC3::TheoryQuant::matchListOld(), CVC3::TheoryQuant::multMatchChild(), CVC3::operator<<(), CVC3::TheoryCore::parseExpr(), CVC3::TheoryCore::parseExprOp(), CVC3::Translator::preprocess2Rec(), CVC3::Translator::preprocessRec(), LFSCPrinter::print_poly_norm(), CVC3::VCCmd::printSymbols(), CVC3::TheoryArith3::projectInequalities(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryQuant::recMultMatch(), CVC3::TheoryQuant::recMultMatchDebug(), CVC3::TheoryQuant::recMultMatchOldWay(), CVC3::CompleteInstPreProcessor::recRewriteNot(), CVC3::TheoryQuant::registerTrig(), CVC3::TheoryBitvector::rewriteBV(), CVC3::BitvectorTheoremProducer::sameKidCheck(), CVC3::ExprTransform::smartSimplify(), CVC3::TheoryArithNew::substAndCanonize(), CVC3::TheoryArith3::substAndCanonize(), CVC3::TheoryArithOld::substAndCanonize(), CVC3::ArithTheoremProducerOld::substitute(), CVC3::ArithTheoremProducer3::substitute(), CVC3::ArithTheoremProducer::substitute(), CVC3::TheoryArithOld::tryPropagate(), and CVC3::ExprTransform::updateQueue().
|
inline |
Definition at line 195 of file expr_map.h.
|
friend |
Definition at line 197 of file expr_map.h.
|
friend |
Definition at line 200 of file expr_map.h.
|
private |
Definition at line 67 of file expr_map.h.