CVC3
2.4.1
|
#include <expr_map.h>
typedef std::hash_map<Expr, Data> CVC3::ExprHashMap::ExprHashMapType [private] |
Definition at line 209 of file expr_map.h.
CVC3::ExprHashMap::ExprHashMap | ( | ) | [inline] |
Default constructor.
Definition at line 298 of file expr_map.h.
CVC3::ExprHashMap::ExprHashMap | ( | size_t | n | ) | [inline] |
Constructor specifying the initial number of buckets.
Definition at line 300 of file expr_map.h.
CVC3::ExprHashMap::ExprHashMap | ( | const ExprHashMap & | map | ) | [inline] |
Definition at line 302 of file expr_map.h.
bool CVC3::ExprHashMap::empty | ( | ) | const [inline] |
Definition at line 305 of file expr_map.h.
Referenced by CVC3::SearchEngineTheoremProducer::conflictClause().
size_t CVC3::ExprHashMap::size | ( | ) | const [inline] |
Definition at line 306 of file expr_map.h.
Referenced by CVC3::Expr::substExpr(), CVC3::ExprManager::rebuild(), CVC3::TheoryArray::computeModel(), and CVC3::TheoryUF::computeModel().
size_t CVC3::ExprHashMap::count | ( | const Expr & | e | ) | const [inline] |
Definition at line 308 of file expr_map.h.
Referenced by CVC3::Expr::recursiveSubst(), CVC3::TheoryCore::assignValue(), CVC3::TheoryCore::collectBasicVars(), CVC3::TheoryCore::buildModel(), and CVC3::TheoryCore::collectModelValues().
Data& CVC3::ExprHashMap::operator[] | ( | const Expr & | e | ) | [inline] |
Definition at line 309 of file expr_map.h.
void CVC3::ExprHashMap::clear | ( | ) | [inline] |
Definition at line 310 of file expr_map.h.
Referenced by CVC3::ArithTheoremProducerOld::rewriteLeavesConst(), CVC3::Expr::recursiveSubst(), CVC3::ExprManager::rebuild(), CVC3::SearchEngineFast::checkValidMain(), CVC3::SearchImplBase::processResult(), CVC3::SearchSimple::checkValidMain(), CVC3::TheoryCore::print(), and CVC3::TheoryCore::collectBasicVars().
void CVC3::ExprHashMap::insert | ( | const Expr & | e, |
const Data & | d | ||
) | [inline] |
Definition at line 312 of file expr_map.h.
Referenced by CVC3::CoreTheoremProducer::rewriteAndSubterms(), CVC3::CoreTheoremProducer::rewriteOrSubterms(), CVC3::Expr::recursiveSubst(), CVC3::Expr::substExpr(), and CVC3::Expr::substExprQuant().
void CVC3::ExprHashMap::erase | ( | const Expr & | e | ) | [inline] |
Definition at line 313 of file expr_map.h.
Referenced by CVC3::SearchImplBase::processResult().
void CVC3::ExprHashMap::insert | ( | InputIterator | l, |
InputIterator | r | ||
) | [inline] |
Definition at line 316 of file expr_map.h.
void CVC3::ExprHashMap::erase | ( | InputIterator | l, |
InputIterator | r | ||
) | [inline] |
Definition at line 319 of file expr_map.h.
iterator CVC3::ExprHashMap::begin | ( | ) | [inline] |
Definition at line 325 of file expr_map.h.
Referenced by CVC3::Expr::recursiveSubst(), CVC3::Expr::substExpr(), CVC3::TheoryArray::computeModel(), and CVC3::TheoryUF::computeModel().
iterator CVC3::ExprHashMap::end | ( | ) | [inline] |
Definition at line 326 of file expr_map.h.
Referenced by CVC3::ArithTheoremProducerOld::getLeaves(), SAT::CNF_Manager::replaceITErec(), SAT::CNF_Manager::translateExprRec(), SAT::CNF_Manager::getCNFLit(), CVC3::Expr::recursiveSubst(), CVC3::Expr::substExpr(), CVC3::Expr::recursiveQuantSubst(), CVC3::ExprManager::rebuildRec(), CVC3::ExprTransform::specialSimplify(), CVC3::ExprTransform::substitute(), CVC3::TheoryArray::computeModel(), containsRec(), CVC3::TheoryCore::buildModel(), CVC3::TheoryCore::collectModelValues(), and CVC3::TheoryUF::computeModel().
const_iterator CVC3::ExprHashMap::begin | ( | ) | const [inline] |
Definition at line 327 of file expr_map.h.
const_iterator CVC3::ExprHashMap::end | ( | ) | const [inline] |
Definition at line 328 of file expr_map.h.
Definition at line 329 of file expr_map.h.
Referenced by CVC3::ArithTheoremProducerOld::getLeaves(), SAT::CNF_Manager::replaceITErec(), SAT::CNF_Manager::translateExprRec(), SAT::CNF_Manager::getCNFLit(), CVC3::Expr::recursiveQuantSubst(), CVC3::ExprManager::rebuildRec(), CVC3::ExprTransform::specialSimplify(), CVC3::ExprTransform::substitute(), CVC3::TheoryCore::getModelValue(), containsRec(), CVC3::TheoryCore::buildModel(), and CVC3::TheoryCore::collectModelValues().
const_iterator CVC3::ExprHashMap::find | ( | const Expr & | e | ) | const [inline] |
Definition at line 330 of file expr_map.h.
ExprHashMapType CVC3::ExprHashMap::d_map [private] |
Definition at line 211 of file expr_map.h.
Referenced by CVC3::ExprHashMap< std::vector< Circuit * > >::empty(), CVC3::ExprHashMap< std::vector< Circuit * > >::size(), CVC3::ExprHashMap< std::vector< Circuit * > >::count(), CVC3::ExprHashMap< std::vector< Circuit * > >::operator[](), CVC3::ExprHashMap< std::vector< Circuit * > >::clear(), CVC3::ExprHashMap< std::vector< Circuit * > >::insert(), CVC3::ExprHashMap< std::vector< Circuit * > >::erase(), CVC3::ExprHashMap< std::vector< Circuit * > >::begin(), CVC3::ExprHashMap< std::vector< Circuit * > >::end(), and CVC3::ExprHashMap< std::vector< Circuit * > >::find().