50 #ifndef _cvc3__expr_h_
54 #ifndef _cvc3__expr_map_h_
55 #define _cvc3__expr_map_h_
78 class const_iterator:
public std::iterator<std::input_iterator_tag, std::pair<Expr,Data>,std::ptrdiff_t> {
81 typename ExprMapType::const_iterator
d_it;
94 return d_it.operator->();
101 const std::pair<const Expr,Data>&
d_pair;
103 Proxy(
const std::pair<Expr,Data>& pair) : d_pair(pair) { }
119 class iterator:
public std::iterator<std::input_iterator_tag, std::pair<Expr,Data>,std::ptrdiff_t> {
122 typename ExprMapType::iterator
d_it;
135 return d_it.operator->();
144 Proxy(std::pair<const Expr,Data>& pair) : d_pair(pair) { }
170 bool empty()
const {
return d_map.empty(); }
171 size_t size()
const {
return d_map.size(); }
173 size_t count(
const Expr& e)
const {
return d_map.count(e); }
180 template<
class InputIterator>
181 void insert(InputIterator l, InputIterator r) { d_map.insert(l,r); }
183 template<
class InputIterator>
184 void erase(InputIterator l, InputIterator r) {
186 d_map.erase((*l).first);
190 iterator
begin() {
return iterator(d_map.begin()); }
191 iterator
end() {
return iterator(d_map.end()); }
192 const_iterator
begin()
const {
return const_iterator(d_map.begin()); }
193 const_iterator
end()
const {
return const_iterator(d_map.end()); }
194 iterator
find(
const Expr& e) {
return iterator(d_map.find(e)); }
195 const_iterator
find(
const Expr& e)
const {
return const_iterator(d_map.find(e)); }
215 class const_iterator:
public std::iterator<std::input_iterator_tag, std::pair<Expr,Data>,std::ptrdiff_t> {
231 return d_it.operator->();
238 const std::pair<const Expr,Data>&
d_pair;
240 Proxy(
const std::pair<Expr,Data>& pair) : d_pair(pair) { }
254 class iterator:
public std::iterator<std::input_iterator_tag, std::pair<Expr,Data>,std::ptrdiff_t> {
270 return d_it.operator->();
279 Proxy(std::pair<const Expr,Data>& pair) : d_pair(pair) { }
315 template<
class InputIterator>
318 template<
class InputIterator>
319 void erase(InputIterator l, InputIterator r) {
321 d_map.
erase((*l).first);
326 iterator
end() {
return iterator(d_map.
end()); }
327 const_iterator
begin()
const {
return const_iterator(d_map.
begin()); }
328 const_iterator
end()
const {
return const_iterator(d_map.
end()); }
330 const_iterator
find(
const Expr& e)
const {
return const_iterator(d_map.
find(e)); }
Proxy(const std::pair< Expr, Data > &pair)
const std::pair< const Expr, Data > & d_pair
const_iterator & operator++()
_hash_table::iterator iterator
ExprHashMapType::const_iterator d_it
size_type count(const _Key &key) const
const std::pair< const Expr, Data > & operator*() const
Data structure of expressions in CVC3.
const_iterator & operator--()
std::pair< const Expr, Data > operator*()
std::pair< const Expr, Data > operator*()
Data & operator[](const Expr &e)
bool operator!=(const iterator &i) const
void erase(const Expr &e)
ExprHashMapType::iterator d_it
void insert(const Expr &e, const Data &d)
const_iterator find(const Expr &e) const
iterator find(const Expr &e)
void erase(InputIterator l, InputIterator r)
ExprHashMap(size_t n)
Constructor specifying the initial number of buckets.
iterator(const typename ExprMapType::iterator &it)
ExprMapType::const_iterator d_it
bool operator!=(const const_iterator &i) const
_hash_table::const_iterator const_iterator
std::pair< const Expr, Data > * operator->() const
void insert(InputIterator l, InputIterator r)
void insert(const Expr &e, const Data &d)
iterator(const typename ExprHashMapType::iterator &it)
iterator find(const key_type &key)
operations
bool operator==(const const_iterator &i) const
ExprHashMap(const ExprHashMap &map)
size_type erase(const key_type &key)
friend bool operator==(const ExprMap &m1, const ExprMap &m2)
const_iterator find(const Expr &e) const
size_t count(const Expr &e) const
const_iterator begin() const
const std::pair< const Expr, Data > & operator*() const
const_iterator end() const
std::hash_map< Expr, Data > ExprHashMapType
Definition of the API to expression package. See class Expr for details.
const_iterator(const typename ExprHashMapType::const_iterator &it)
Proxy(const std::pair< Expr, Data > &pair)
iterator begin()
iterators
const_iterator begin() const
friend bool operator!=(const ExprMap &m1, const ExprMap &m2)
Data & operator[](const Expr &e)
const_iterator(const typename ExprMapType::const_iterator &it)
void insert(InputIterator l, InputIterator r)
const std::pair< const Expr, Data > * operator->() const
std::pair< iterator, bool > insert(const value_type &entry)
size_t count(const Expr &e) const
std::pair< const Expr, Data > operator*()
bool operator==(const iterator &i) const
ExprMap(const ExprMap &map)
const std::pair< const Expr, Data > * operator->() const
bool operator!=(const const_iterator &i) const
const_iterator end() const
Proxy(std::pair< const Expr, Data > &pair)
std::pair< const Expr, Data > operator*()
std::map< Expr, Data > ExprMapType
std::pair< const Expr, Data > & d_pair
ExprHashMap()
Default constructor.
iterator find(const Expr &e)
Definition of the API to expression package. See class Expr for details.
std::pair< const Expr, Data > * operator->() const
std::pair< const Expr, Data > & d_pair
Proxy(std::pair< const Expr, Data > &pair)
bool operator!=(const iterator &i) const
ExprMapType::iterator d_it
std::pair< const Expr, Data > & operator*() const
bool operator==(const const_iterator &i) const
const std::pair< const Expr, Data > & d_pair
void erase(const Expr &e)
bool operator==(const iterator &i) const
void erase(InputIterator l, InputIterator r)
std::pair< const Expr, Data > & operator*() const
const_iterator & operator++()