diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-09 09:49:35 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-09 09:49:35 +0000 |
commit | 0131e18b811bdf2825a1cde5a6d68d523b19aacc (patch) | |
tree | 9c4dcb4c1bf355b943926a5df85d3c3446750878 /src/util | |
parent | ec86769172d29ff7f5ed959866ecef339264552b (diff) |
support for SMT-LIBv2 :named attributes, and attributes in general; zero-ary define-fun; several set-info, set-option, get-option, get-info improvementss
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/configuration.cpp | 7 | ||||
-rw-r--r-- | src/util/configuration.h | 2 | ||||
-rw-r--r-- | src/util/stats.h | 74 |
3 files changed, 59 insertions, 24 deletions
diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp index 403f6f84b..9b463f797 100644 --- a/src/util/configuration.cpp +++ b/src/util/configuration.cpp @@ -18,13 +18,20 @@ ** configuration information about the CVC4 library. **/ +#include <string> + #include "util/configuration.h" #include "util/configuration_private.h" +#include "cvc4autoconfig.h" using namespace std; namespace CVC4 { +string Configuration::getName() { + return PACKAGE_NAME; +} + bool Configuration::isDebugBuild() { return IS_DEBUG_BUILD; } diff --git a/src/util/configuration.h b/src/util/configuration.h index 907cd1d31..33c0a7407 100644 --- a/src/util/configuration.h +++ b/src/util/configuration.h @@ -37,6 +37,8 @@ class CVC4_PUBLIC Configuration { public: + static std::string getName(); + static bool isDebugBuild(); static bool isTracingBuild(); diff --git a/src/util/stats.h b/src/util/stats.h index 43b48140e..d6b463e65 100644 --- a/src/util/stats.h +++ b/src/util/stats.h @@ -24,6 +24,7 @@ #include <string> #include <ostream> +#include <sstream> #include <iomanip> #include <set> #include <ctime> @@ -44,16 +45,28 @@ class CVC4_PUBLIC Stat; class CVC4_PUBLIC StatisticsRegistry { private: - struct StatCmp; + struct StatCmp { + inline bool operator()(const Stat* s1, const Stat* s2) const; + };/* class StatisticsRegistry::StatCmp */ typedef std::set< Stat*, StatCmp > StatSet; static StatSet d_registeredStats; public: + + typedef StatSet::const_iterator const_iterator; + static void flushStatistics(std::ostream& out); static inline void registerStat(Stat* s) throw(AssertionException); static inline void unregisterStat(Stat* s) throw(AssertionException); + + static inline const_iterator begin() { + return d_registeredStats.begin(); + } + static inline const_iterator end() { + return d_registeredStats.end(); + } };/* class StatisticsRegistry */ @@ -65,8 +78,8 @@ private: public: - Stat(const std::string& s) throw(CVC4::AssertionException) : d_name(s) - { + Stat(const std::string& s) throw(CVC4::AssertionException) : + d_name(s) { if(__CVC4_USE_STATISTICS) { AlwaysAssert(d_name.find(s_delim) == std::string::npos); } @@ -85,18 +98,17 @@ public: const std::string& getName() const { return d_name; } -};/* class Stat */ - -struct StatisticsRegistry::StatCmp { - bool operator()(const Stat* s1, const Stat* s2) const - { - return (s1->getName()) < (s2->getName()); - } -};/* class StatCmp */ + virtual std::string getValue() const = 0; +};/* class Stat */ +inline bool StatisticsRegistry::StatCmp::operator()(const Stat* s1, + const Stat* s2) const { + return s1->getName() < s2->getName(); +} -inline void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) { +inline void StatisticsRegistry::registerStat(Stat* s) + throw(AssertionException) { if(__CVC4_USE_STATISTICS) { AlwaysAssert(d_registeredStats.find(s) == d_registeredStats.end()); d_registeredStats.insert(s); @@ -104,7 +116,8 @@ inline void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) }/* StatisticsRegistry::registerStat */ -inline void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) { +inline void StatisticsRegistry::unregisterStat(Stat* s) + throw(AssertionException) { if(__CVC4_USE_STATISTICS) { AlwaysAssert(d_registeredStats.find(s) != d_registeredStats.end()); d_registeredStats.erase(s); @@ -120,7 +133,9 @@ inline void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException template <class T> class DataStat : public Stat { public: - DataStat(const std::string& s) : Stat(s) {} + DataStat(const std::string& s) : + Stat(s) { + } virtual const T& getData() const = 0; virtual void setData(const T&) = 0; @@ -130,6 +145,12 @@ public: out << getData(); } } + + std::string getValue() const { + std::stringstream ss; + ss << getData(); + return ss.str(); + } };/* class DataStat */ @@ -140,13 +161,14 @@ private: const T* d_data; public: - ReferenceStat(const std::string& s): - DataStat<T>(s), d_data(NULL) - {} + ReferenceStat(const std::string& s) : + DataStat<T>(s), + d_data(NULL) { + } - ReferenceStat(const std::string& s, const T& data): - DataStat<T>(s), d_data(NULL) - { + ReferenceStat(const std::string& s, const T& data) : + DataStat<T>(s), + d_data(NULL) { setData(data); } @@ -155,6 +177,7 @@ public: d_data = &t; } } + const T& getData() const { if(__CVC4_USE_STATISTICS) { return *d_data; @@ -173,8 +196,10 @@ protected: public: - BackedStat(const std::string& s, const T& init): DataStat<T>(s), d_data(init) - {} + BackedStat(const std::string& s, const T& init) : + DataStat<T>(s), + d_data(init) { + } void setData(const T& t) { if(__CVC4_USE_STATISTICS) { @@ -202,8 +227,9 @@ public: class IntStat : public BackedStat<int64_t> { public: - IntStat(const std::string& s, int64_t init): BackedStat<int64_t>(s, init) - {} + IntStat(const std::string& s, int64_t init) : + BackedStat<int64_t>(s, init) { + } IntStat& operator++() { if(__CVC4_USE_STATISTICS) { |