CVC3
expr_map.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file expr_map.h
4  *
5  * Author: Sergey Berezin
6  *
7  * Created: Dec 11 01:22:49 GMT 2002
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 // CLASS: ExprMap<Data>
21 //
22 // AUTHOR: Sergey Berezin, 12/10/2002
23 //
24 // Abstract:
25 //
26 // An abstract interface mapping Expr values to Data. The
27 // implementation is a hash table.
28 //
29 // Subclassing is NOT allowed; this would lose the iterators (can we
30 // fix it? Maybe not worth the trouble.)
31 //
32 // Functions follow the style of STL 'map' container.
33 //
34 // ExprMap<Data>() [Default constructor] Creates an empty map
35 // int count(Expr e) Counts the number of elements mapped from e.
36 // Normally, returns 0 or 1.
37 // Data& operator[](e) Returns Data associated with e. If e is not mapped,
38 // insert new Data() into ExprMap.
39 // Can be used to populate ExprMap as follows:
40 // ExprMap map;
41 // map[e1] = data1; map[e2] = data2; ...
42 // Caveat: Data must have a default constructor and be assignable.
43 // void erase(Expr e) Erase e->data mapping from ExprMap.
44 // void insert(Expr e, Data d) Insert e->d mapping.
45 // iterator begin() Return simple "input" iterators for ExprMap
46 // iterator end() (as defined in STL)
47 // size_t size() Return size of the map
48 // bool empty() Check for emptiness
49 ///////////////////////////////////////////////////////////////////////////////
50 #ifndef _cvc3__expr_h_
51 #include "expr.h"
52 #endif
53 
54 #ifndef _cvc3__expr_map_h_
55 #define _cvc3__expr_map_h_
56 
57 #include "expr_hash.h"
58 
59 namespace CVC3 {
60 
61  template<class Data>
62  class ExprMap {
63  private:
64 
65  typedef std::map<Expr, Data> ExprMapType;
66  // Private members
68 
69  public:
70 
71  //////////////////////////////////////////////////////////////////////////
72  // Class: ExprMap::iterator
73  // Author: Sergey Berezin
74  // Created: Tue Dec 10 16:25:19 2002
75  // Description:
76  //////////////////////////////////////////////////////////////////////////
77 
78  class const_iterator: public std::iterator<std::input_iterator_tag, std::pair<Expr,Data>,std::ptrdiff_t> {
79  friend class ExprMap;
80  private:
81  typename ExprMapType::const_iterator d_it;
82  // Private constructor
83  const_iterator(const typename ExprMapType::const_iterator& it)
84  : d_it(it) { }
85  public:
86  // Default constructor
88  // (Dis)equality
89  bool operator==(const const_iterator& i) const { return d_it == i.d_it; }
90  bool operator!=(const const_iterator& i) const { return d_it != i.d_it; }
91  // Dereference operators.
92  const std::pair<const Expr,Data>& operator*() const { return *d_it; }
93  const std::pair<const Expr,Data>* operator->() const {
94  return d_it.operator->();
95  }
96  // Prefix increment
97  const_iterator& operator++() { ++d_it; return *this; }
98  // Postfix increment: requires a Proxy object to hold the
99  // intermediate value for dereferencing
100  class Proxy {
101  const std::pair<const Expr,Data>& d_pair;
102  public:
103  Proxy(const std::pair<Expr,Data>& pair) : d_pair(pair) { }
104  std::pair<const Expr,Data> operator*() { return d_pair; }
105  }; // end of class Proxy
106  // Actual postfix increment: returns Proxy with the old value.
107  // Now, an expression like *i++ will return the current *i, and
108  // then advance the iterator. However, don't try to use Proxy for
109  // anything else.
111  Proxy tmp(*(*this));
112  ++(*this);
113  return tmp;
114  }
115  // Prefix decrement
116  const_iterator& operator--() { --d_it; return *this; }
117  }; // end of class const_iterator
118 
119  class iterator: public std::iterator<std::input_iterator_tag, std::pair<Expr,Data>,std::ptrdiff_t> {
120  friend class ExprMap;
121  private:
122  typename ExprMapType::iterator d_it;
123  // Private constructor
124  iterator(const typename ExprMapType::iterator& it)
125  : d_it(it) { }
126  public:
127  // Default constructor
128  iterator() { }
129  // (Dis)equality
130  bool operator==(const iterator& i) const { return d_it == i.d_it; }
131  bool operator!=(const iterator& i) const { return d_it != i.d_it; }
132  // Dereference operators.
133  std::pair<const Expr,Data>& operator*() const { return *d_it; }
134  std::pair<const Expr,Data>* operator->() const {
135  return d_it.operator->();
136  }
137  // Prefix increment
138  iterator& operator++() { ++d_it; return *this; }
139  // Postfix increment: requires a Proxy object to hold the
140  // intermediate value for dereferencing
141  class Proxy {
142  std::pair<const Expr,Data>& d_pair;
143  public:
144  Proxy(std::pair<const Expr,Data>& pair) : d_pair(pair) { }
145  std::pair<const Expr,Data> operator*() { return d_pair; }
146  }; // end of class Proxy
147  // Actual postfix increment: returns Proxy with the old value.
148  // Now, an expression like *i++ will return the current *i, and
149  // then advance the iterator. However, don't try to use Proxy for
150  // anything else.
152  Proxy tmp(*(*this));
153  ++(*this);
154  return tmp;
155  }
156  // Prefix decrement
157  iterator& operator--() { --d_it; return *this; }
158  }; // end of class iterator
159 
160  //////////////////////////////////////////////////////////////////////////
161  // Public methods
162  //////////////////////////////////////////////////////////////////////////
163 
164  // Default constructor
165  ExprMap() { }
166  // Copy constructor
167  ExprMap(const ExprMap& map): d_map(map.d_map) { }
168 
169  // Other methods
170  bool empty() const { return d_map.empty(); }
171  size_t size() const { return d_map.size(); }
172 
173  size_t count(const Expr& e) const { return d_map.count(e); }
174  Data& operator[](const Expr& e) { return d_map[e]; }
175  void clear() { d_map.clear(); }
176 
177  void insert(const Expr& e, const Data& d) { d_map[e] = d; }
178  void erase(const Expr& e) { d_map.erase(e); }
179 
180  template<class InputIterator>
181  void insert(InputIterator l, InputIterator r) { d_map.insert(l,r); }
182 
183  template<class InputIterator>
184  void erase(InputIterator l, InputIterator r) {
185  for(; l!=r; ++l) {
186  d_map.erase((*l).first);
187  }
188  }
189 
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)); }
196 
197  friend bool operator==(const ExprMap& m1, const ExprMap& m2) {
198  return m1.d_map == m2.d_map;
199  }
200  friend bool operator!=(const ExprMap& m1, const ExprMap& m2) {
201  return !(m1 == m2);
202  }
203  }; // end of class ExprMap
204 
205  template<class Data>
206  class ExprHashMap {
207  private:
208 
210  // Private members
212 
213  public:
214 
215  class const_iterator: public std::iterator<std::input_iterator_tag, std::pair<Expr,Data>,std::ptrdiff_t> {
216  friend class ExprHashMap;
217  private:
219  // Private constructor
221  : d_it(it) { }
222  public:
223  // Default constructor
225  // (Dis)equality
226  bool operator==(const const_iterator& i) const { return d_it == i.d_it; }
227  bool operator!=(const const_iterator& i) const { return d_it != i.d_it; }
228  // Dereference operators.
229  const std::pair<const Expr,Data>& operator*() const { return *d_it; }
230  const std::pair<const Expr,Data>* operator->() const {
231  return d_it.operator->();
232  }
233  // Prefix increment
234  const_iterator& operator++() { ++d_it; return *this; }
235  // Postfix increment: requires a Proxy object to hold the
236  // intermediate value for dereferencing
237  class Proxy {
238  const std::pair<const Expr,Data>& d_pair;
239  public:
240  Proxy(const std::pair<Expr,Data>& pair) : d_pair(pair) { }
241  std::pair<const Expr,Data> operator*() { return d_pair; }
242  }; // end of class Proxy
243  // Actual postfix increment: returns Proxy with the old value.
244  // Now, an expression like *i++ will return the current *i, and
245  // then advance the iterator. However, don't try to use Proxy for
246  // anything else.
248  Proxy tmp(*(*this));
249  ++(*this);
250  return tmp;
251  }
252  }; // end of class const_iterator
253 
254  class iterator: public std::iterator<std::input_iterator_tag, std::pair<Expr,Data>,std::ptrdiff_t> {
255  friend class ExprHashMap;
256  private:
258  // Private constructor
260  : d_it(it) { }
261  public:
262  // Default constructor
263  iterator() { }
264  // (Dis)equality
265  bool operator==(const iterator& i) const { return d_it == i.d_it; }
266  bool operator!=(const iterator& i) const { return d_it != i.d_it; }
267  // Dereference operators.
268  std::pair<const Expr,Data>& operator*() const { return *d_it; }
269  std::pair<const Expr,Data>* operator->() const {
270  return d_it.operator->();
271  }
272  // Prefix increment
273  iterator& operator++() { ++d_it; return *this; }
274  // Postfix increment: requires a Proxy object to hold the
275  // intermediate value for dereferencing
276  class Proxy {
277  std::pair<const Expr,Data>& d_pair;
278  public:
279  Proxy(std::pair<const Expr,Data>& pair) : d_pair(pair) { }
280  std::pair<const Expr,Data> operator*() { return d_pair; }
281  }; // end of class Proxy
282  // Actual postfix increment: returns Proxy with the old value.
283  // Now, an expression like *i++ will return the current *i, and
284  // then advance the iterator. However, don't try to use Proxy for
285  // anything else.
287  Proxy tmp(*(*this));
288  ++(*this);
289  return tmp;
290  }
291  }; // end of class iterator
292 
293  //////////////////////////////////////////////////////////////////////////
294  // Public methods
295  //////////////////////////////////////////////////////////////////////////
296 
297  //! Default constructor
299  //! Constructor specifying the initial number of buckets
300  ExprHashMap(size_t n): d_map(n) { }
301  // Copy constructor
302  ExprHashMap(const ExprHashMap& map): d_map(map.d_map) { }
303 
304  // Other methods
305  bool empty() const { return d_map.empty(); }
306  size_t size() const { return d_map.size(); }
307 
308  size_t count(const Expr& e) const { return d_map.count(e); }
309  Data& operator[](const Expr& e) { return d_map[e]; }
310  void clear() { d_map.clear(); }
311 
312  void insert(const Expr& e, const Data& d) { d_map[e] = d; }
313  void erase(const Expr& e) { d_map.erase(e); }
314 
315  template<class InputIterator>
316  void insert(InputIterator l, InputIterator r) { d_map.insert(l,r); }
317 
318  template<class InputIterator>
319  void erase(InputIterator l, InputIterator r) {
320  for(; l!=r; ++l) {
321  d_map.erase((*l).first);
322  }
323  }
324 
325  iterator begin() { return iterator(d_map.begin()); }
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()); }
329  iterator find(const Expr& e) { return iterator(d_map.find(e)); }
330  const_iterator find(const Expr& e) const { return const_iterator(d_map.find(e)); }
331 
332  // These aren't implemented
333 // friend bool operator==(const ExprHashMap& m1, const ExprHashMap& m2) {
334 // return m1.d_map == m2.d_map;
335 // }
336 // friend bool operator!=(const ExprHashMap& m1, const ExprHashMap& m2) {
337 // return !(m1 == m2);
338 // }
339  }; // end of class ExprHashMap
340 
341 } // end of namespace CVC3
342 
343 #endif