CVC3::ExprHashMap< Data > Class Template Reference

#include <expr_map.h>

Inheritance diagram for CVC3::ExprHashMap< Data >:

[legend]Collaboration diagram for CVC3::ExprHashMap< Data >:

[legend]List of all members.

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 () const
• iterator end () const
• iterator find (const Expr &e) const

Private Types

• typedef std::hash_map< Expr,
  Data > ExprHashMapType

Private Attributes

• ExprHashMapType d_map

Friends

• bool operator== (const ExprHashMap &m1, const ExprHashMap &m2)
• bool operator!= (const ExprHashMap &m1, const ExprHashMap &m2)

Classes

• class iterator

---

Detailed Description

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

Definition at line 160 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 163 of file expr_map.h.

---

Constructor & Destructor Documentation

template<class Data>

CVC3::ExprHashMap< Data >::ExprHashMap

(

)

[inline]

Default constructor.

Definition at line 220 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 222 of file expr_map.h.

template<class Data>

CVC3::ExprHashMap< Data >::ExprHashMap

(

const ExprHashMap< Data > &

map

)

[inline]

Definition at line 224 of file expr_map.h.

---

Member Function Documentation

template<class Data>

bool CVC3::ExprHashMap< Data >::empty

(

)

const [inline]

Definition at line 227 of file expr_map.h.

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

template<class Data>

size_t CVC3::ExprHashMap< Data >::size

(

)

const [inline]

Definition at line 228 of file expr_map.h.

Referenced by CVC3::TheoryUF::computeModel(), CVC3::TheoryArray::computeModel(), and CVC3::Expr::substExpr().

template<class Data>

size_t CVC3::ExprHashMap< Data >::count

(

const Expr &

e

)

const [inline]

Definition at line 230 of file expr_map.h.

Referenced by CVC3::Expr::recursiveSubst().

template<class Data>

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

(

const Expr &

e

)

[inline]

Definition at line 231 of file expr_map.h.

template<class Data>

void CVC3::ExprHashMap< Data >::clear

(

)

[inline]

Definition at line 232 of file expr_map.h.

Referenced by CVC3::SearchSimple::checkValidMain(), CVC3::SearchEngineFast::checkValidMain(), CVC3::SearchImplBase::processResult(), and CVC3::Expr::recursiveSubst().

template<class Data>

void CVC3::ExprHashMap< Data >::insert	(	const Expr &	e,
		const Data &	d
	)			[inline]

Definition at line 234 of file expr_map.h.

Referenced by CVC3::Expr::recursiveSubst(), CVC3::CoreTheoremProducer::rewriteAndSubterms(), CVC3::CoreTheoremProducer::rewriteOrSubterms(), and CVC3::Expr::substExpr().

template<class Data>

void CVC3::ExprHashMap< Data >::erase

(

const Expr &

e

)

[inline]

Definition at line 235 of file expr_map.h.

Referenced by CVC3::SearchImplBase::processResult(), and CVC3::Expr::recursiveSubst().

template<class Data>

template<class InputIterator>

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

Definition at line 238 of file expr_map.h.

template<class Data>

template<class InputIterator>

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

Definition at line 241 of file expr_map.h.

template<class Data>

iterator CVC3::ExprHashMap< Data >::begin

(

)

const [inline]

Definition at line 247 of file expr_map.h.

Referenced by CVC3::TheoryUF::computeModel(), CVC3::TheoryArray::computeModel(), and CVC3::Expr::recursiveSubst().

template<class Data>

iterator CVC3::ExprHashMap< Data >::end

(

)

const [inline]

Definition at line 248 of file expr_map.h.

Referenced by CVC3::TheoryUF::computeModel(), CVC3::TheoryArray::computeModel(), and CVC3::Expr::recursiveSubst().

template<class Data>

iterator CVC3::ExprHashMap< Data >::find

(

const Expr &

e

)

const [inline]

Definition at line 249 of file expr_map.h.

---

Friends And Related Function Documentation

template<class Data>

bool operator==	(	const ExprHashMap< Data > &	m1,
		const ExprHashMap< Data > &	m2
	)			[friend]

Definition at line 251 of file expr_map.h.

template<class Data>

bool operator!=	(	const ExprHashMap< Data > &	m1,
		const ExprHashMap< Data > &	m2
	)			[friend]

Definition at line 254 of file expr_map.h.

---

Member Data Documentation

template<class Data>

ExprHashMapType CVC3::ExprHashMap< Data >::d_map [private]

Definition at line 165 of file expr_map.h.

Referenced by CVC3::ExprHashMap< std::vector< CVC3::Circuit * > >::begin(), CVC3::ExprHashMap< std::vector< CVC3::Circuit * > >::clear(), CVC3::ExprHashMap< std::vector< CVC3::Circuit * > >::count(), CVC3::ExprHashMap< std::vector< CVC3::Circuit * > >::empty(), CVC3::ExprHashMap< std::vector< CVC3::Circuit * > >::end(), CVC3::ExprHashMap< std::vector< CVC3::Circuit * > >::erase(), CVC3::ExprHashMap< std::vector< CVC3::Circuit * > >::find(), CVC3::ExprHashMap< std::vector< CVC3::Circuit * > >::insert(), CVC3::ExprHashMap< std::vector< CVC3::Circuit * > >::operator[](), and CVC3::ExprHashMap< std::vector< CVC3::Circuit * > >::size().

---

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

• expr_map.h

---