00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00029
00030
00031
00032
00033
00034
00035
00036
00037
00038
00039
00040
00041
00042
00043
00044
00045
00046
00047
00048
00049
00050
00051
00052
00053
00054
00055
00056
00057
00058 #ifndef _CVC_lite__expr_h_
00059 #include "expr.h"
00060 #endif
00061
00062 #ifndef _CVC_lite__expr_map_h_
00063 #define _CVC_lite__expr_map_h_
00064
00065 #include "expr_hash.h"
00066
00067 namespace CVCL {
00068
00069 template<class Data>
00070 class ExprMap {
00071 private:
00072
00073 typedef std::map<Expr, Data> ExprMapType;
00074
00075 ExprMapType d_map;
00076
00077 public:
00078
00079
00080
00081
00082
00083
00084
00085
00086 class iterator: public std::iterator<std::input_iterator_tag, std::pair<Expr,Data>,std::ptrdiff_t> {
00087 friend class ExprMap;
00088 private:
00089 typename ExprMapType::const_iterator d_it;
00090
00091 iterator(const typename ExprMapType::const_iterator& it)
00092 : d_it(it) { }
00093 public:
00094
00095 iterator() { }
00096
00097 bool operator==(const iterator& i) const { return d_it == i.d_it; }
00098 bool operator!=(const iterator& i) const { return d_it != i.d_it; }
00099
00100 const std::pair<const Expr,Data>& operator*() const { return *d_it; }
00101 const std::pair<const Expr,Data>* operator->() const {
00102 return d_it.operator->();
00103 }
00104
00105 iterator& operator++() { ++d_it; return *this; }
00106
00107
00108 class Proxy {
00109 const std::pair<const Expr,Data>& d_pair;
00110 public:
00111 Proxy(const std::pair<Expr,Data>& pair) : d_pair(pair) { }
00112 std::pair<const Expr,Data> operator*() { return d_pair; }
00113 };
00114
00115
00116
00117
00118 Proxy operator++(int) {
00119 Proxy tmp(*(*this));
00120 ++(*this);
00121 return tmp;
00122 }
00123 };
00124
00125
00126
00127
00128
00129
00130 ExprMap() { }
00131
00132 ExprMap(const ExprMap& map): d_map(map.d_map) { }
00133
00134
00135 bool empty() const { return d_map.empty(); }
00136 size_t size() const { return d_map.size(); }
00137
00138 int count(const Expr& e) const { return d_map.count(e); }
00139 Data& operator[](const Expr& e) { return d_map[e]; }
00140 void clear() { d_map.clear(); }
00141
00142 void insert(const Expr& e, const Data& d) { d_map[e] = d; }
00143 void erase(const Expr& e) { d_map.erase(e); }
00144
00145 template<class InputIterator>
00146 void insert(InputIterator l, InputIterator r) { d_map.insert(l,r); }
00147
00148 template<class InputIterator>
00149 void erase(InputIterator l, InputIterator r) {
00150 for(; l!=r; ++l) {
00151 d_map.erase((*l).first);
00152 }
00153 }
00154
00155 iterator begin() const { return iterator(d_map.begin()); }
00156 iterator end() const { return iterator(d_map.end()); }
00157 iterator find(const Expr& e) const { return iterator(d_map.find(e)); }
00158
00159 friend bool operator==(const ExprMap& m1, const ExprMap& m2) {
00160 return m1.d_map == m2.d_map;
00161 }
00162 friend bool operator!=(const ExprMap& m1, const ExprMap& m2) {
00163 return !(m1 == m2);
00164 }
00165 };
00166
00167 template<class Data>
00168 class ExprHashMap {
00169 private:
00170
00171 typedef std::hash_map<Expr, Data> ExprHashMapType;
00172
00173 ExprHashMapType d_map;
00174
00175 public:
00176
00177
00178
00179
00180
00181
00182
00183
00184 class iterator: public std::iterator<std::input_iterator_tag, std::pair<Expr,Data>,std::ptrdiff_t> {
00185 friend class ExprHashMap;
00186 private:
00187 typename ExprHashMapType::const_iterator d_it;
00188
00189 iterator(const typename ExprHashMapType::const_iterator& it)
00190 : d_it(it) { }
00191 public:
00192
00193 iterator() { }
00194
00195 bool operator==(const iterator& i) const { return d_it == i.d_it; }
00196 bool operator!=(const iterator& i) const { return d_it != i.d_it; }
00197
00198 const std::pair<const Expr,Data>& operator*() const { return *d_it; }
00199 const std::pair<const Expr,Data>* operator->() const {
00200 return d_it.operator->();
00201 }
00202
00203 iterator& operator++() { ++d_it; return *this; }
00204
00205
00206 class Proxy {
00207 const std::pair<const Expr,Data>& d_pair;
00208 public:
00209 Proxy(const std::pair<Expr,Data>& pair) : d_pair(pair) { }
00210 std::pair<const Expr,Data> operator*() { return d_pair; }
00211 };
00212
00213
00214
00215
00216 Proxy operator++(int) {
00217 Proxy tmp(*(*this));
00218 ++(*this);
00219 return tmp;
00220 }
00221 };
00222
00223
00224
00225
00226
00227
00228 ExprHashMap() { }
00229
00230 ExprHashMap(size_t n): d_map(n) { }
00231
00232 ExprHashMap(const ExprHashMap& map): d_map(map.d_map) { }
00233
00234
00235 bool empty() const { return d_map.empty(); }
00236 size_t size() const { return d_map.size(); }
00237
00238 int count(const Expr& e) const { return d_map.count(e); }
00239 Data& operator[](const Expr& e) { return d_map[e]; }
00240 void clear() { d_map.clear(); }
00241
00242 void insert(const Expr& e, const Data& d) { d_map[e] = d; }
00243 void erase(const Expr& e) { d_map.erase(e); }
00244
00245 template<class InputIterator>
00246 void insert(InputIterator l, InputIterator r) { d_map.insert(l,r); }
00247
00248 template<class InputIterator>
00249 void erase(InputIterator l, InputIterator r) {
00250 for(; l!=r; ++l) {
00251 d_map.erase((*l).first);
00252 }
00253 }
00254
00255 iterator begin() const { return iterator(d_map.begin()); }
00256 iterator end() const { return iterator(d_map.end()); }
00257 iterator find(const Expr& e) const { return iterator(d_map.find(e)); }
00258
00259 friend bool operator==(const ExprHashMap& m1, const ExprHashMap& m2) {
00260 return m1.d_map == m2.d_map;
00261 }
00262 friend bool operator!=(const ExprHashMap& m1, const ExprHashMap& m2) {
00263 return !(m1 == m2);
00264 }
00265 };
00266
00267 }
00268
00269 #endif