CVC3

cvc_util.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file cvc_util.h
00004  *\brief basic helper utilities
00005  *
00006  * Author: Clark Barrett
00007  *
00008  * Created: Thu Dec  1 16:35:52 2005
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  * 
00017  * <hr>
00018  */
00019 /*****************************************************************************/
00020 
00021 #ifndef _cvc3__debug_h
00022 #include "debug.h"
00023 #endif
00024 
00025 #ifndef _cvc3__cvc_util_h
00026 #define _cvc3__cvc_util_h
00027 
00028 namespace CVC3 {
00029 
00030 inline std::string to_upper(const std::string & src){
00031   std::string nameup; 
00032   for(std::string::const_iterator i=src.begin(), iend = src.end(); i!=iend ; i++){
00033     nameup.push_back(toupper(*i));
00034   }
00035   return nameup;
00036 }
00037 
00038 inline std::string to_lower(const std::string & src){
00039   std::string nameup; 
00040   for(std::string::const_iterator i=src.begin(), iend = src.end(); i!=iend ; i++){
00041     nameup.push_back(tolower(*i));
00042   }
00043   return nameup;
00044 }
00045 
00046 inline std::string int2string(int n) {
00047   std::ostringstream ss;
00048   ss << n;
00049   return ss.str();
00050 }
00051 
00052 template<class T>
00053 T abs(T t) { return t < 0 ? -t : t; }
00054 
00055 template<class T>
00056 T max(T a, T b) { return a > b ? a : b; }
00057 
00058 struct ltstr{
00059   bool operator()(const std::string& s1, const std::string& s2) const{
00060     return s1.compare(s2) < 0;
00061   }
00062 };
00063 
00064 template<class T>
00065 class StrPairLess {
00066 public:
00067   bool operator()(const std::pair<std::string,T>& p1,
00068       const std::pair<std::string,T>& p2) const {
00069     return p1.first < p2.first;
00070   }
00071 };
00072 
00073 template<class T>
00074 std::pair<std::string,T> strPair(const std::string& f, const T& t) {
00075   return std::pair<std::string,T>(f, t);
00076 }
00077 
00078 typedef std::pair<std::string,std::string> StrPair;
00079 
00080 //! Sort two vectors based on the first vector
00081 template<class T>
00082 void sort2(std::vector<std::string>& keys, std::vector<T>& vals) {
00083   DebugAssert(keys.size()==vals.size(), "sort2()");
00084   // Create std::vector of pairs
00085   std::vector<std::pair<std::string,T> > pairs;
00086   for(size_t i=0, iend=keys.size(); i<iend; ++i)
00087     pairs.push_back(strPair(keys[i], vals[i]));
00088   // Sort pairs
00089   StrPairLess<T> comp;
00090   sort(pairs.begin(), pairs.end(), comp);
00091   DebugAssert(pairs.size() == keys.size(), "sort2()");
00092   // Split the pairs back into the original vectors
00093   for(size_t i=0, iend=pairs.size(); i<iend; ++i) {
00094     keys[i] = pairs[i].first;
00095     vals[i] = pairs[i].second;
00096   }
00097 }
00098 
00099 /*! @brief A class which sets a boolean value to true when created,
00100  * and resets to false when deleted.
00101  *
00102  * Useful for tracking when the control is within a certain method or
00103  * not.  For example, TheoryCore::addFact() uses d_inAddFact to check
00104  * that certain other methods are only called from within addFact().
00105  * However, when an exception is thrown, this variable is not reset.
00106  * The watcher class will reset the variable even in those cases.
00107  */
00108 class ScopeWatcher {
00109  private:
00110   bool *d_flag;
00111 public:
00112   ScopeWatcher(bool *flag): d_flag(flag) { *d_flag = true; }
00113   ~ScopeWatcher() { *d_flag = false; }
00114 };
00115 
00116 
00117 // For memory calculations
00118 class MemoryTracker {
00119 public:
00120   static void print(std::string name, int verbosity,
00121                     unsigned long memSelf, unsigned long mem)
00122   {
00123     if (verbosity > 0) {
00124       std::cout << name << ": " << memSelf << std::endl;
00125       std::cout << "  Children: " << mem << std::endl;
00126       std::cout << "  Total: " << mem+memSelf << std::endl;
00127     }
00128   }
00129 
00130   template <typename T>
00131   static unsigned long getVec(int verbosity, const std::vector<T>& v)
00132   {
00133     unsigned long memSelf = sizeof(std::vector<T>);
00134     unsigned long mem = 0;
00135     print("vector", verbosity, memSelf, mem);
00136     return memSelf + mem;
00137   }
00138 
00139   template <typename T>
00140   static unsigned long getVecAndData(int verbosity, const std::vector<T>& v)
00141   {
00142     unsigned long memSelf = sizeof(std::vector<T>);
00143     unsigned long mem = 0;
00144     for (unsigned i = 0; i < v.size(); ++i) {
00145       mem += v[i].getMemory(verbosity - 1);
00146     }
00147     print("vector+data", verbosity, memSelf, mem);
00148     return memSelf + mem;
00149   }
00150 
00151   template <typename T>
00152   static unsigned long getVecAndDataP(int verbosity, const std::vector<T>& v)
00153   {
00154     unsigned long memSelf = sizeof(std::vector<T>);
00155     unsigned long mem = 0;
00156     for (unsigned i = 0; i < v.size(); ++i) {
00157       mem += v[i]->getMemory(verbosity - 1);
00158     }
00159     print("vector+data(p)", verbosity, memSelf, mem);
00160     return memSelf + mem;
00161   }
00162 
00163   static unsigned long getString(int verbosity, const std::string& s)
00164   {
00165     unsigned long memSelf = sizeof(std::string);
00166     unsigned long mem = s.capacity() * sizeof(char);
00167     print("string", verbosity, memSelf, mem);
00168     return memSelf + mem;
00169   }
00170 
00171 //   template <class _Key, class _Value,
00172 //      class _HashFcn, class _EqualKey, class _ExtractKey>
00173 //     unsigned long get(int verbosity, const hash_table<_Key, _Value, _HashFcn, 
00174 //         unsigned long memSelf = sizeof(BucketNode);
00175 //         unsigned long mem = 0;
00176 //         BucketNode* node = this;
00177 //         do {
00178 //           if (getMemoryData) {
00179 //             mem += d_value.getMemory(verbosity
00180 //           node = node->d_next;
00181 //         } while (node != NULL)          
00182 //         unsigned long mem = 0;
00183 
00184 //         mem += getMemoryVec(verbosity - 1, d_data, false, true);
00185 //         printMemory("hash_table", verbosity, memSelf, mem);
00186 //         return mem+memSelf;
00187 //       }
00188 
00189 //   unsigned long getMemory(int verbosity, hash_table) {
00190 //       unsigned long memSelf = sizeof(hash_table);
00191 //       unsigned long mem = 0;
00192 //       mem += d_hash.getmemory(verbosity - 1) - sizeof(hasher);
00193 //       mem += d_equal.getmemory(verbosity - 1) - sizeof(key_equal);
00194 //       mem += d_extractKey.getmemory(verbosity - 1) - sizeof(_ExtractKey);
00195 
00196 //       // handle data
00197 //       mem += sizeof(Data);
00198 //       mem += sizeof(Bucket*)*d_data.capacity();
00199 //       for (unsigned i = 0; i < d_data.size(); ++i) {
00200 //         mem += d_data[i]->getMemory(verbosity - 1, getMemoryData, getMemoryDataP);
00201 //       }
00202 
00203 //       printMemory("hash_table", verbosity, memSelf, mem);
00204 //       return mem+memSelf;
00205 //     }
00206   
00207 //     unsigned long getMemory(int verbosity, hash_map) const {
00208 //       unsigned long memSelf = sizeof(hash_map);
00209 //       unsigned long mem = 0;
00210 //       mem += d_table.getMemory(verbosity - 1) - sizeof(_hash_table);
00211 //       MemoryTracker::print("hash_map", verbosity, memSelf, mem);
00212 //       return mem+memSelf;
00213 //     }
00214 
00215 
00216 }; // End of MemoryTracker
00217   
00218 }
00219 
00220 #endif