expr_map.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file expr_map.h
00004  * 
00005  * Author: Sergey Berezin
00006  * 
00007  * Created: Dec 11 01:22:49 GMT 2002
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  * 
00016  * <hr>
00017  * 
00018  */
00019 /*****************************************************************************/
00020 // CLASS: ExprMap<Data>
00021 //
00022 // AUTHOR: Sergey Berezin, 12/10/2002
00023 //
00024 // Abstract:
00025 //
00026 // An abstract interface mapping Expr values to Data.  The
00027 // implementation is a hash table.
00028 //
00029 // Subclassing is NOT allowed; this would lose the iterators (can we
00030 // fix it?  Maybe not worth the trouble.)
00031 //
00032 // Functions follow the style of STL 'map' container.
00033 // 
00034 // ExprMap<Data>()    [Default constructor] Creates an empty map
00035 // int count(Expr e)  Counts the number of elements mapped from e.
00036 //                    Normally, returns 0 or 1.
00037 // Data& operator[](e)  Returns Data associated with e.  If e is not mapped,
00038 //                    insert new Data() into ExprMap.
00039 //                    Can be used to populate ExprMap as follows:
00040 //          ExprMap map;
00041 //          map[e1] = data1; map[e2] = data2; ...
00042 //          Caveat: Data must have a default constructor and be assignable.
00043 // void erase(Expr e)  Erase e->data mapping from ExprMap.
00044 // void insert(Expr e, Data d)  Insert e->d mapping.
00045 // iterator begin()   Return simple "input" iterators for ExprMap
00046 // iterator end()     (as defined in STL)
00047 // size_t size()      Return size of the map
00048 // bool empty()       Check for emptiness     
00049 ///////////////////////////////////////////////////////////////////////////////
00050 #ifndef _cvc3__expr_h_
00051 #include "expr.h"
00052 #endif
00053 
00054 #ifndef _cvc3__expr_map_h_
00055 #define _cvc3__expr_map_h_
00056 
00057 #include "expr_hash.h"
00058 
00059 namespace CVC3 {
00060 
00061   template<class Data>
00062   class ExprMap {
00063   private:
00064 
00065     typedef std::map<Expr, Data> ExprMapType;
00066     // Private members
00067     ExprMapType d_map;
00068 
00069   public:
00070 
00071     //////////////////////////////////////////////////////////////////////////
00072     // Class: ExprMap::iterator
00073     // Author: Sergey Berezin
00074     // Created: Tue Dec 10 16:25:19 2002
00075     // Description: 
00076     //////////////////////////////////////////////////////////////////////////
00077 
00078     class const_iterator: public std::iterator<std::input_iterator_tag, std::pair<Expr,Data>,std::ptrdiff_t> {
00079       friend class ExprMap;
00080     private:
00081       typename ExprMapType::const_iterator d_it;
00082       // Private constructor
00083       const_iterator(const typename ExprMapType::const_iterator& it)
00084   : d_it(it) { }
00085     public:
00086       // Default constructor
00087       const_iterator() { }
00088       // (Dis)equality
00089       bool operator==(const const_iterator& i) const { return d_it == i.d_it; }
00090       bool operator!=(const const_iterator& i) const { return d_it != i.d_it; }
00091       // Dereference operators.
00092       const std::pair<const Expr,Data>& operator*() const { return *d_it; }
00093       const std::pair<const Expr,Data>* operator->() const {
00094   return d_it.operator->();
00095       }
00096       // Prefix increment
00097       const_iterator& operator++() { ++d_it; return *this; }
00098       // Postfix increment: requires a Proxy object to hold the
00099       // intermediate value for dereferencing
00100       class Proxy {
00101   const std::pair<const Expr,Data>& d_pair;
00102       public:
00103   Proxy(const std::pair<Expr,Data>& pair) : d_pair(pair) { }
00104   std::pair<const Expr,Data> operator*() { return d_pair; }
00105       }; // end of class Proxy
00106       // Actual postfix increment: returns Proxy with the old value.
00107       // Now, an expression like *i++ will return the current *i, and
00108       // then advance the iterator.  However, don't try to use Proxy for
00109       // anything else.
00110       Proxy operator++(int) {
00111   Proxy tmp(*(*this));
00112   ++(*this);
00113   return tmp;
00114       }
00115       // Prefix decrement
00116       const_iterator& operator--() { --d_it; return *this; }
00117     }; // end of class const_iterator
00118 
00119     class iterator: public std::iterator<std::input_iterator_tag, std::pair<Expr,Data>,std::ptrdiff_t> {
00120       friend class ExprMap;
00121     private:
00122       typename ExprMapType::iterator d_it;
00123       // Private constructor
00124       iterator(const typename ExprMapType::iterator& it)
00125   : d_it(it) { }
00126     public:
00127       // Default constructor
00128       iterator() { }
00129       // (Dis)equality
00130       bool operator==(const iterator& i) const { return d_it == i.d_it; }
00131       bool operator!=(const iterator& i) const { return d_it != i.d_it; }
00132       // Dereference operators.
00133       std::pair<const Expr,Data>& operator*() const { return *d_it; }
00134       std::pair<const Expr,Data>* operator->() const {
00135   return d_it.operator->();
00136       }
00137       // Prefix increment
00138       iterator& operator++() { ++d_it; return *this; }
00139       // Postfix increment: requires a Proxy object to hold the
00140       // intermediate value for dereferencing
00141       class Proxy {
00142   std::pair<const Expr,Data>& d_pair;
00143       public:
00144   Proxy(std::pair<const Expr,Data>& pair) : d_pair(pair) { }
00145   std::pair<const Expr,Data> operator*() { return d_pair; }
00146       }; // end of class Proxy
00147       // Actual postfix increment: returns Proxy with the old value.
00148       // Now, an expression like *i++ will return the current *i, and
00149       // then advance the iterator.  However, don't try to use Proxy for
00150       // anything else.
00151       Proxy operator++(int) {
00152   Proxy tmp(*(*this));
00153   ++(*this);
00154   return tmp;
00155       }
00156       // Prefix decrement
00157       iterator& operator--() { --d_it; return *this; }
00158     }; // end of class iterator
00159 
00160     //////////////////////////////////////////////////////////////////////////
00161     // Public methods
00162     //////////////////////////////////////////////////////////////////////////
00163 
00164     // Default constructor
00165     ExprMap() { }
00166     // Copy constructor
00167     ExprMap(const ExprMap& map): d_map(map.d_map) { }
00168 
00169     // Other methods
00170     bool empty() const { return d_map.empty(); }
00171     size_t size() const { return d_map.size(); }
00172 
00173     size_t count(const Expr& e) const { return d_map.count(e); }
00174     Data& operator[](const Expr& e) { return d_map[e]; }
00175     void clear() { d_map.clear(); }
00176 
00177     void insert(const Expr& e, const Data& d) { d_map[e] = d; }
00178     void erase(const Expr& e) { d_map.erase(e); }
00179 
00180     template<class InputIterator>
00181       void insert(InputIterator l, InputIterator r) { d_map.insert(l,r); }
00182 
00183     template<class InputIterator>
00184       void erase(InputIterator l, InputIterator r) {
00185       for(; l!=r; ++l) {
00186   d_map.erase((*l).first);
00187       }
00188     }
00189 
00190     iterator begin() { return iterator(d_map.begin()); }
00191     iterator end() { return iterator(d_map.end()); }
00192     const_iterator begin() const { return const_iterator(d_map.begin()); }
00193     const_iterator end() const { return const_iterator(d_map.end()); }
00194     iterator find(const Expr& e) { return iterator(d_map.find(e)); }
00195     const_iterator find(const Expr& e) const { return const_iterator(d_map.find(e)); }
00196 
00197     friend bool operator==(const ExprMap& m1, const ExprMap& m2) {
00198       return m1.d_map == m2.d_map;
00199     }
00200     friend bool operator!=(const ExprMap& m1, const ExprMap& m2) {
00201       return !(m1 == m2);
00202     }
00203   }; // end of class ExprMap
00204 
00205   template<class Data>
00206   class ExprHashMap {
00207   private:
00208 
00209     typedef std::hash_map<Expr, Data> ExprHashMapType;
00210     // Private members
00211     ExprHashMapType d_map;
00212 
00213   public:
00214 
00215     class const_iterator: public std::iterator<std::input_iterator_tag, std::pair<Expr,Data>,std::ptrdiff_t> {
00216       friend class ExprHashMap;
00217     private:
00218       typename ExprHashMapType::const_iterator d_it;
00219       // Private constructor
00220       const_iterator(const typename ExprHashMapType::const_iterator& it)
00221   : d_it(it) { }
00222     public:
00223       // Default constructor
00224       const_iterator() { }
00225       // (Dis)equality
00226       bool operator==(const const_iterator& i) const { return d_it == i.d_it; }
00227       bool operator!=(const const_iterator& i) const { return d_it != i.d_it; }
00228       // Dereference operators.
00229       const std::pair<const Expr,Data>& operator*() const { return *d_it; }
00230       const std::pair<const Expr,Data>* operator->() const {
00231   return d_it.operator->();
00232       }
00233       // Prefix increment
00234       const_iterator& operator++() { ++d_it; return *this; }
00235       // Postfix increment: requires a Proxy object to hold the
00236       // intermediate value for dereferencing
00237       class Proxy {
00238   const std::pair<const Expr,Data>& d_pair;
00239       public:
00240   Proxy(const std::pair<Expr,Data>& pair) : d_pair(pair) { }
00241   std::pair<const Expr,Data> operator*() { return d_pair; }
00242       }; // end of class Proxy
00243       // Actual postfix increment: returns Proxy with the old value.
00244       // Now, an expression like *i++ will return the current *i, and
00245       // then advance the iterator.  However, don't try to use Proxy for
00246       // anything else.
00247       Proxy operator++(int) {
00248   Proxy tmp(*(*this));
00249   ++(*this);
00250   return tmp;
00251       }
00252     }; // end of class const_iterator
00253 
00254     class iterator: public std::iterator<std::input_iterator_tag, std::pair<Expr,Data>,std::ptrdiff_t> {
00255       friend class ExprHashMap;
00256     private:
00257       typename ExprHashMapType::iterator d_it;
00258       // Private constructor
00259       iterator(const typename ExprHashMapType::iterator& it)
00260   : d_it(it) { }
00261     public:
00262       // Default constructor
00263       iterator() { }
00264       // (Dis)equality
00265       bool operator==(const iterator& i) const { return d_it == i.d_it; }
00266       bool operator!=(const iterator& i) const { return d_it != i.d_it; }
00267       // Dereference operators.
00268       std::pair<const Expr,Data>& operator*() const { return *d_it; }
00269       std::pair<const Expr,Data>* operator->() const {
00270   return d_it.operator->();
00271       }
00272       // Prefix increment
00273       iterator& operator++() { ++d_it; return *this; }
00274       // Postfix increment: requires a Proxy object to hold the
00275       // intermediate value for dereferencing
00276       class Proxy {
00277   std::pair<const Expr,Data>& d_pair;
00278       public:
00279   Proxy(std::pair<const Expr,Data>& pair) : d_pair(pair) { }
00280   std::pair<const Expr,Data> operator*() { return d_pair; }
00281       }; // end of class Proxy
00282       // Actual postfix increment: returns Proxy with the old value.
00283       // Now, an expression like *i++ will return the current *i, and
00284       // then advance the iterator.  However, don't try to use Proxy for
00285       // anything else.
00286       Proxy operator++(int) {
00287   Proxy tmp(*(*this));
00288   ++(*this);
00289   return tmp;
00290       }
00291     }; // end of class iterator
00292 
00293     //////////////////////////////////////////////////////////////////////////
00294     // Public methods
00295     //////////////////////////////////////////////////////////////////////////
00296 
00297     //! Default constructor
00298     ExprHashMap() { }
00299     //! Constructor specifying the initial number of buckets
00300     ExprHashMap(size_t n): d_map(n) { }
00301     // Copy constructor
00302     ExprHashMap(const ExprHashMap& map): d_map(map.d_map) { }
00303 
00304     // Other methods
00305     bool empty() const { return d_map.empty(); }
00306     size_t size() const { return d_map.size(); }
00307 
00308     size_t count(const Expr& e) const { return d_map.count(e); }
00309     Data& operator[](const Expr& e) { return d_map[e]; }
00310     void clear() { d_map.clear(); }
00311 
00312     void insert(const Expr& e, const Data& d) { d_map[e] = d; }
00313     void erase(const Expr& e) { d_map.erase(e); }
00314 
00315     template<class InputIterator>
00316       void insert(InputIterator l, InputIterator r) { d_map.insert(l,r); }
00317 
00318     template<class InputIterator>
00319       void erase(InputIterator l, InputIterator r) {
00320       for(; l!=r; ++l) {
00321   d_map.erase((*l).first);
00322       }
00323     }
00324 
00325     iterator begin() { return iterator(d_map.begin()); }
00326     iterator end() { return iterator(d_map.end()); }
00327     const_iterator begin() const { return const_iterator(d_map.begin()); }
00328     const_iterator end() const { return const_iterator(d_map.end()); }
00329     iterator find(const Expr& e) { return iterator(d_map.find(e)); }
00330     const_iterator find(const Expr& e) const { return const_iterator(d_map.find(e)); }
00331 
00332     // These aren't implemented
00333 //     friend bool operator==(const ExprHashMap& m1, const ExprHashMap& m2) {
00334 //       return m1.d_map == m2.d_map;
00335 //     }
00336 //     friend bool operator!=(const ExprHashMap& m1, const ExprHashMap& m2) {
00337 //       return !(m1 == m2);
00338 //     }
00339   }; // end of class ExprHashMap
00340 
00341 } // end of namespace CVC3
00342 
00343 #endif

Generated on Wed Nov 18 16:13:30 2009 for CVC3 by  doxygen 1.5.2