CVC3
cvc_util.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file cvc_util.h
4  *\brief basic helper utilities
5  *
6  * Author: Clark Barrett
7  *
8  * Created: Thu Dec 1 16:35:52 2005
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  */
19 /*****************************************************************************/
20 
21 #ifndef _cvc3__debug_h
22 #include "debug.h"
23 #endif
24 
25 #ifndef _cvc3__cvc_util_h
26 #define _cvc3__cvc_util_h
27 
28 namespace CVC3 {
29 
30 inline std::string to_upper(const std::string & src){
31  std::string nameup;
32  for(std::string::const_iterator i=src.begin(), iend = src.end(); i!=iend ; i++){
33  nameup.push_back(toupper(*i));
34  }
35  return nameup;
36 }
37 
38 inline std::string to_lower(const std::string & src){
39  std::string nameup;
40  for(std::string::const_iterator i=src.begin(), iend = src.end(); i!=iend ; i++){
41  nameup.push_back(tolower(*i));
42  }
43  return nameup;
44 }
45 
46 inline std::string int2string(int n) {
47  std::ostringstream ss;
48  ss << n;
49  return ss.str();
50 }
51 
52 template<class T>
53 T abs(T t) { return t < 0 ? -t : t; }
54 
55 template<class T>
56 T max(T a, T b) { return a > b ? a : b; }
57 
58 struct ltstr{
59  bool operator()(const std::string& s1, const std::string& s2) const{
60  return s1.compare(s2) < 0;
61  }
62 };
63 
64 template<class T>
65 class StrPairLess {
66 public:
67  bool operator()(const std::pair<std::string,T>& p1,
68  const std::pair<std::string,T>& p2) const {
69  return p1.first < p2.first;
70  }
71 };
72 
73 template<class T>
74 std::pair<std::string,T> strPair(const std::string& f, const T& t) {
75  return std::pair<std::string,T>(f, t);
76 }
77 
78 typedef std::pair<std::string,std::string> StrPair;
79 
80 //! Sort two vectors based on the first vector
81 template<class T>
82 void sort2(std::vector<std::string>& keys, std::vector<T>& vals) {
83  DebugAssert(keys.size()==vals.size(), "sort2()");
84  // Create std::vector of pairs
85  std::vector<std::pair<std::string,T> > pairs;
86  for(size_t i=0, iend=keys.size(); i<iend; ++i)
87  pairs.push_back(strPair(keys[i], vals[i]));
88  // Sort pairs
89  StrPairLess<T> comp;
90  sort(pairs.begin(), pairs.end(), comp);
91  DebugAssert(pairs.size() == keys.size(), "sort2()");
92  // Split the pairs back into the original vectors
93  for(size_t i=0, iend=pairs.size(); i<iend; ++i) {
94  keys[i] = pairs[i].first;
95  vals[i] = pairs[i].second;
96  }
97 }
98 
99 /*! @brief A class which sets a boolean value to true when created,
100  * and resets to false when deleted.
101  *
102  * Useful for tracking when the control is within a certain method or
103  * not. For example, TheoryCore::addFact() uses d_inAddFact to check
104  * that certain other methods are only called from within addFact().
105  * However, when an exception is thrown, this variable is not reset.
106  * The watcher class will reset the variable even in those cases.
107  */
109  private:
110  bool *d_flag;
111 public:
112  ScopeWatcher(bool *flag): d_flag(flag) { *d_flag = true; }
113  ~ScopeWatcher() { *d_flag = false; }
114 };
115 
116 
117 // For memory calculations
119 public:
120  static void print(std::string name, int verbosity,
121  unsigned long memSelf, unsigned long mem)
122  {
123  if (verbosity > 0) {
124  std::cout << name << ": " << memSelf << std::endl;
125  std::cout << " Children: " << mem << std::endl;
126  std::cout << " Total: " << mem+memSelf << std::endl;
127  }
128  }
129 
130  template <typename T>
131  static unsigned long getVec(int verbosity, const std::vector<T>& v)
132  {
133  unsigned long memSelf = sizeof(std::vector<T>);
134  unsigned long mem = 0;
135  print("vector", verbosity, memSelf, mem);
136  return memSelf + mem;
137  }
138 
139  template <typename T>
140  static unsigned long getVecAndData(int verbosity, const std::vector<T>& v)
141  {
142  unsigned long memSelf = sizeof(std::vector<T>);
143  unsigned long mem = 0;
144  for (unsigned i = 0; i < v.size(); ++i) {
145  mem += v[i].getMemory(verbosity - 1);
146  }
147  print("vector+data", verbosity, memSelf, mem);
148  return memSelf + mem;
149  }
150 
151  template <typename T>
152  static unsigned long getVecAndDataP(int verbosity, const std::vector<T>& v)
153  {
154  unsigned long memSelf = sizeof(std::vector<T>);
155  unsigned long mem = 0;
156  for (unsigned i = 0; i < v.size(); ++i) {
157  mem += v[i]->getMemory(verbosity - 1);
158  }
159  print("vector+data(p)", verbosity, memSelf, mem);
160  return memSelf + mem;
161  }
162 
163  static unsigned long getString(int verbosity, const std::string& s)
164  {
165  unsigned long memSelf = sizeof(std::string);
166  unsigned long mem = s.capacity() * sizeof(char);
167  print("string", verbosity, memSelf, mem);
168  return memSelf + mem;
169  }
170 
171 // template <class _Key, class _Value,
172 // class _HashFcn, class _EqualKey, class _ExtractKey>
173 // unsigned long get(int verbosity, const hash_table<_Key, _Value, _HashFcn,
174 // unsigned long memSelf = sizeof(BucketNode);
175 // unsigned long mem = 0;
176 // BucketNode* node = this;
177 // do {
178 // if (getMemoryData) {
179 // mem += d_value.getMemory(verbosity
180 // node = node->d_next;
181 // } while (node != NULL)
182 // unsigned long mem = 0;
183 
184 // mem += getMemoryVec(verbosity - 1, d_data, false, true);
185 // printMemory("hash_table", verbosity, memSelf, mem);
186 // return mem+memSelf;
187 // }
188 
189 // unsigned long getMemory(int verbosity, hash_table) {
190 // unsigned long memSelf = sizeof(hash_table);
191 // unsigned long mem = 0;
192 // mem += d_hash.getmemory(verbosity - 1) - sizeof(hasher);
193 // mem += d_equal.getmemory(verbosity - 1) - sizeof(key_equal);
194 // mem += d_extractKey.getmemory(verbosity - 1) - sizeof(_ExtractKey);
195 
196 // // handle data
197 // mem += sizeof(Data);
198 // mem += sizeof(Bucket*)*d_data.capacity();
199 // for (unsigned i = 0; i < d_data.size(); ++i) {
200 // mem += d_data[i]->getMemory(verbosity - 1, getMemoryData, getMemoryDataP);
201 // }
202 
203 // printMemory("hash_table", verbosity, memSelf, mem);
204 // return mem+memSelf;
205 // }
206 
207 // unsigned long getMemory(int verbosity, hash_map) const {
208 // unsigned long memSelf = sizeof(hash_map);
209 // unsigned long mem = 0;
210 // mem += d_table.getMemory(verbosity - 1) - sizeof(_hash_table);
211 // MemoryTracker::print("hash_map", verbosity, memSelf, mem);
212 // return mem+memSelf;
213 // }
214 
215 
216 }; // End of MemoryTracker
217 
218 }
219 
220 #endif