CVC3
2.4.1
|
#include <hash_map.h>
hash map implementation based on the sgi interface: http://www.sgi.com/tech/stl/hash_map.html
_Key: hash key type _Data: data to store _HashFcn: functional class providing a hash function: size_type (_Key) _EqualKey: functional class providing a comparison function: bool(_Key, _Key) returns true iff two keys are considered to be equal
typedef hash_table<_Key, std::pair<const _Key, _Data>, _HashFcn, _EqualKey, _Select1st<std::pair<const _Key, _Data> > > Hash::hash_map::_hash_table [protected] |
types
Definition at line 93 of file hash_map.h.
Definition at line 97 of file hash_map.h.
Definition at line 98 of file hash_map.h.
typedef _Data Hash::hash_map::data_type |
Definition at line 99 of file hash_map.h.
Definition at line 100 of file hash_map.h.
Definition at line 101 of file hash_map.h.
Definition at line 102 of file hash_map.h.
typedef _hash_table::iterator Hash::hash_map::iterator |
Definition at line 106 of file hash_map.h.
typedef _hash_table::const_iterator Hash::hash_map::const_iterator |
Definition at line 107 of file hash_map.h.
Hash::hash_map::hash_map | ( | ) | [inline] |
Hash::hash_map::hash_map | ( | size_type | initial_capacity | ) | [inline] |
Definition at line 127 of file hash_map.h.
Hash::hash_map::hash_map | ( | size_type | initial_capacity, |
const _HashFcn & | hash | ||
) | [inline] |
Definition at line 132 of file hash_map.h.
Hash::hash_map::hash_map | ( | size_type | initial_capacity, |
const _HashFcn & | hash, | ||
const _EqualKey & | equal | ||
) | [inline] |
Definition at line 137 of file hash_map.h.
Hash::hash_map::hash_map | ( | const hash_map & | other | ) | [inline] |
Definition at line 143 of file hash_map.h.
Definition at line 148 of file hash_map.h.
void Hash::hash_map::swap | ( | hash_map & | other | ) | [inline] |
Definition at line 156 of file hash_map.h.
void Hash::hash_map::clear | ( | ) | [inline] |
Definition at line 161 of file hash_map.h.
Referenced by CVC3::CDMap< Expr, EdgeInfo >::setNull(), CVC3::ExprHashMap< std::vector< Circuit * > >::clear(), and CVC3::TheoremManager::clearAllFlags().
operations
Definition at line 171 of file hash_map.h.
Referenced by CVC3::CDMap< Expr, EdgeInfo >::operator[](), CVC3::CDMap< Expr, EdgeInfo >::insert(), CVC3::CDMap< Expr, EdgeInfo >::find(), SAT::CNF_Formula_Impl::simplify(), CVC3::ExprManager::getKind(), CVC3::ExprHashMap< std::vector< Circuit * > >::find(), MiniSat::Derivation::computeRootReason(), MiniSat::Derivation::checkDerivation(), MiniSat::Derivation::createProof(), MiniSat::Derivation::printDerivation(), CVC3::TheoremManager::getCachedValue(), CVC3::TheoremManager::getExpandFlag(), CVC3::TheoremManager::getLitFlag(), CVC3::Theory::addBoundVar(), CVC3::Theory::resolveID(), CVC3::TheoryArithNew::isBasic(), CVC3::TheoryArithNew::pivot(), CVC3::TheoryArithNew::update(), CVC3::TheoryArithNew::pivotAndUpdate(), CVC3::TheoryArithNew::checkSatSimplex(), CVC3::TheoryArithNew::getVariableIntroThm(), CVC3::TheoryArithNew::substAndCanonizeModTableaux(), CVC3::TheoryArithNew::substAndCanonizeTableaux(), CVC3::TheoryCore::getTheoremForTerm(), CVC3::TheoryCore::registerAtom(), CVC3::TheoryCore::parseExpr(), CVC3::TheoryQuant::enqueueInst(), and CVC3::Translator::fixConstName().
const_iterator Hash::hash_map::find | ( | const key_type & | key | ) | const [inline] |
Definition at line 176 of file hash_map.h.
Definition at line 183 of file hash_map.h.
std::pair<iterator, bool> Hash::hash_map::insert | ( | const value_type & | entry | ) | [inline] |
Definition at line 190 of file hash_map.h.
Referenced by CVC3::ExprHashMap< std::vector< Circuit * > >::insert(), CVC3::TheoryArithNew::updateDependenciesAdd(), and CVC3::TheoryArithNew::updateDependencies().
Definition at line 197 of file hash_map.h.
Referenced by CVC3::CDOmap< Key, Data, HashFcn >::setNull(), CVC3::ExprHashMap< std::vector< Circuit * > >::erase(), CVC3::Theory::unregisterKinds(), CVC3::TheoryArithNew::pivot(), CVC3::TheoryArithNew::updateDependenciesRemove(), CVC3::TheoryArithNew::updateDependencies(), and CVC3::TheoryCore::parseExpr().
const_iterator Hash::hash_map::erase | ( | const const_iterator & | i | ) | [inline] |
Definition at line 203 of file hash_map.h.
bool Hash::hash_map::contains | ( | const key_type & | key | ) | const [inline] |
status
Definition at line 211 of file hash_map.h.
Referenced by MiniSat::Derivation::createProof(), MiniSat::Derivation::registerClause(), and MiniSat::Derivation::registerInference().
size_type Hash::hash_map::count | ( | const _Key & | key | ) | const [inline] |
Definition at line 217 of file hash_map.h.
Referenced by CVC3::CDOmap< Key, Data, HashFcn >::setNull(), CVC3::CDMap< Expr, EdgeInfo >::count(), CVC3::ExprManager::newKind(), CVC3::ExprManager::getKindName(), CVC3::ExprHashMap< std::vector< Circuit * > >::count(), CVC3::TheoremManager::isFlagged(), CVC3::Theory::registerKinds(), CVC3::Theory::hasTheory(), and CVC3::Theory::theoryOf().
bool Hash::hash_map::empty | ( | ) | const [inline] |
Definition at line 222 of file hash_map.h.
Referenced by CVC3::ExprHashMap< std::vector< Circuit * > >::empty(), and CVC3::TheoryArithNew::substAndCanonizeModTableaux().
size_type Hash::hash_map::size | ( | ) | const [inline] |
Definition at line 227 of file hash_map.h.
Referenced by CVC3::CDMap< Expr, EdgeInfo >::size(), CVC3::ExprHashMap< std::vector< Circuit * > >::size(), and CVC3::TheoryArithNew::checkSatSimplex().
size_type Hash::hash_map::bucket_count | ( | ) | const [inline] |
Definition at line 232 of file hash_map.h.
float Hash::hash_map::load_factor | ( | ) | const [inline] |
Definition at line 237 of file hash_map.h.
iterator Hash::hash_map::begin | ( | ) | [inline] |
iterators
Definition at line 246 of file hash_map.h.
Referenced by CVC3::CDMap< Expr, EdgeInfo >::setNull(), CVC3::CDMap< Expr, EdgeInfo >::begin(), CVC3::ExprHashMap< std::vector< Circuit * > >::begin(), MiniSat::Derivation::pop(), CVC3::TheoryArithNew::tableauxAsString(), and CVC3::TheoryArithNew::boundsAsString().
const_iterator Hash::hash_map::begin | ( | ) | const [inline] |
Definition at line 251 of file hash_map.h.
iterator Hash::hash_map::end | ( | ) | [inline] |
Definition at line 257 of file hash_map.h.
Referenced by CVC3::CDMap< Expr, EdgeInfo >::setNull(), CVC3::CDMap< Expr, EdgeInfo >::operator[](), CVC3::CDMap< Expr, EdgeInfo >::insert(), CVC3::CDMap< Expr, EdgeInfo >::end(), SAT::CNF_Formula_Impl::simplify(), CVC3::ExprManager::getKind(), CVC3::ExprHashMap< std::vector< Circuit * > >::end(), CVC3::TheoremManager::getCachedValue(), CVC3::TheoremManager::getExpandFlag(), CVC3::TheoremManager::getLitFlag(), CVC3::Theory::addBoundVar(), CVC3::Theory::resolveID(), CVC3::TheoryArithNew::isBasic(), CVC3::TheoryArithNew::update(), CVC3::TheoryArithNew::pivotAndUpdate(), CVC3::TheoryArithNew::getVariableIntroThm(), CVC3::TheoryArithNew::tableauxAsString(), CVC3::TheoryArithNew::boundsAsString(), CVC3::TheoryArithNew::substAndCanonizeModTableaux(), CVC3::TheoryArithNew::substAndCanonizeTableaux(), CVC3::TheoryCore::getTheoremForTerm(), CVC3::TheoryCore::registerAtom(), CVC3::TheoryCore::parseExpr(), CVC3::TheoryQuant::enqueueInst(), and CVC3::Translator::fixConstName().
const_iterator Hash::hash_map::end | ( | ) | const [inline] |
Definition at line 262 of file hash_map.h.
_hash_table Hash::hash_map::d_table [protected] |
variables
Definition at line 113 of file hash_map.h.
Referenced by Hash::hash_map< long, int >::operator=(), Hash::hash_map< long, int >::swap(), Hash::hash_map< long, int >::clear(), Hash::hash_map< long, int >::find(), Hash::hash_map< long, int >::operator[](), Hash::hash_map< long, int >::insert(), Hash::hash_map< long, int >::erase(), Hash::hash_map< long, int >::contains(), Hash::hash_map< long, int >::count(), Hash::hash_map< long, int >::empty(), Hash::hash_map< long, int >::size(), Hash::hash_map< long, int >::bucket_count(), Hash::hash_map< long, int >::load_factor(), Hash::hash_map< long, int >::begin(), and Hash::hash_map< long, int >::end().