CVC3::ExprHashMap< Data > Class Template Reference

#include <expr_map.h>

Collaboration diagram for CVC3::ExprHashMap< Data >:

List of all members.

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

---

Detailed Description

template<class Data>
class CVC3::ExprHashMap< Data >

Definition at line 206 of file expr_map.h.

---

Member Typedef Documentation

template<class Data>

typedef std::hash_map<Expr, Data> CVC3::ExprHashMap< Data >::ExprHashMapType [private]

Definition at line 209 of file expr_map.h.

---

Constructor & Destructor Documentation

template<class Data>

CVC3::ExprHashMap< Data >::ExprHashMap

(

)

[inline]

Default constructor.

Definition at line 298 of file expr_map.h.

template<class Data>

CVC3::ExprHashMap< Data >::ExprHashMap

(

size_t

n

)

[inline]

Constructor specifying the initial number of buckets.

Definition at line 300 of file expr_map.h.

template<class Data>

CVC3::ExprHashMap< Data >::ExprHashMap

(

const ExprHashMap< Data > &

map

)

[inline]

Definition at line 302 of file expr_map.h.

---

Member Function Documentation

template<class Data>

bool CVC3::ExprHashMap< Data >::empty

(

)

const [inline]

Definition at line 305 of file expr_map.h.

Referenced by CVC3::SearchEngineTheoremProducer::conflictClause().

template<class Data>

size_t CVC3::ExprHashMap< Data >::size

(

)

const [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().

template<class Data>

size_t CVC3::ExprHashMap< Data >::count

(

const Expr &

e

)

const [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().

template<class Data>

Data& CVC3::ExprHashMap< Data >::operator[]

(

const Expr &

e

)

[inline]

Definition at line 309 of file expr_map.h.

template<class Data>

void CVC3::ExprHashMap< Data >::clear

(

)

[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().

template<class Data>

void CVC3::ExprHashMap< Data >::insert	(	const Expr &	e,
		const Data &	d
	)		[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().

template<class Data>

void CVC3::ExprHashMap< Data >::erase

(

const Expr &

e

)

[inline]

Definition at line 313 of file expr_map.h.

Referenced by CVC3::SearchImplBase::processResult().

template<class Data>

template<class InputIterator >

void CVC3::ExprHashMap< Data >::insert	(	InputIterator	l,
		InputIterator	r
	)		[inline]

Definition at line 316 of file expr_map.h.

template<class Data>

template<class InputIterator >

void CVC3::ExprHashMap< Data >::erase	(	InputIterator	l,
		InputIterator	r
	)		[inline]

Definition at line 319 of file expr_map.h.

template<class Data>

iterator CVC3::ExprHashMap< Data >::begin

(

)

[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().

template<class Data>

iterator CVC3::ExprHashMap< Data >::end

(

)

[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().

template<class Data>

const_iterator CVC3::ExprHashMap< Data >::begin

(

)

const [inline]

Definition at line 327 of file expr_map.h.

template<class Data>

const_iterator CVC3::ExprHashMap< Data >::end

(

)

const [inline]

Definition at line 328 of file expr_map.h.

template<class Data>

iterator CVC3::ExprHashMap< Data >::find

(

const Expr &

e

)

[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().

template<class Data>

const_iterator CVC3::ExprHashMap< Data >::find

(

const Expr &

e

)

const [inline]

Definition at line 330 of file expr_map.h.

---

Member Data Documentation

template<class Data>

ExprHashMapType CVC3::ExprHashMap< Data >::d_map [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().

---

The documentation for this class was generated from the following file:

• expr_map.h