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