#include <string>
#include <ostream>
+#include <iomanip>
#include <set>
+#include <ctime>
+
#include "util/Assert.h"
namespace CVC4 {
#ifdef CVC4_STATISTICS_ON
-# define USE_STATISTICS true
+# define __CVC4_USE_STATISTICS true
#else
-# define USE_STATISTICS false
+# define __CVC4_USE_STATISTICS false
#endif
class CVC4_PUBLIC Stat;
public:
static void flushStatistics(std::ostream& out);
- static inline void registerStat(Stat* s) throw (AssertionException);
- static inline void unregisterStat(Stat* s) throw (AssertionException);
+ static inline void registerStat(Stat* s) throw(AssertionException);
+ static inline void unregisterStat(Stat* s) throw(AssertionException);
};/* class StatisticsRegistry */
public:
- Stat(const std::string& s) throw (CVC4::AssertionException) : d_name(s)
+ Stat(const std::string& s) throw(CVC4::AssertionException) : d_name(s)
{
- if(USE_STATISTICS){
+ if(__CVC4_USE_STATISTICS) {
AlwaysAssert(d_name.find(s_delim) == std::string::npos);
}
}
virtual void flushInformation(std::ostream& out) const = 0;
- void flushStat(std::ostream& out) const{
- if(USE_STATISTICS){
+ void flushStat(std::ostream& out) const {
+ if(__CVC4_USE_STATISTICS) {
out << d_name << s_delim;
flushInformation(out);
}
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 */
+
-inline void StatisticsRegistry::registerStat(Stat* s) throw (AssertionException){
- if(USE_STATISTICS){
+inline void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) {
+ if(__CVC4_USE_STATISTICS) {
AlwaysAssert(d_registeredStats.find(s) == d_registeredStats.end());
d_registeredStats.insert(s);
}
-}
-inline void StatisticsRegistry::unregisterStat(Stat* s) throw (AssertionException){
- if(USE_STATISTICS){
+}/* StatisticsRegistry::registerStat */
+
+
+inline void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) {
+ if(__CVC4_USE_STATISTICS) {
AlwaysAssert(d_registeredStats.find(s) != d_registeredStats.end());
d_registeredStats.erase(s);
}
-}
+}/* StatisticsRegistry::unregisterStat */
* class T must have stream insertion operation defined.
* std::ostream& operator<<(std::ostream&, const T&);
*/
-template<class T>
-class DataStat : public Stat{
+template <class T>
+class DataStat : public Stat {
public:
DataStat(const std::string& s) : Stat(s) {}
virtual const T& getData() const = 0;
virtual void setData(const T&) = 0;
- void flushInformation(std::ostream& out) const{
- if(USE_STATISTICS){
+ void flushInformation(std::ostream& out) const {
+ if(__CVC4_USE_STATISTICS) {
out << getData();
}
}
-};
+};/* class DataStat */
+
/** T must have an assignment operator=(). */
template <class T>
-class ReferenceStat: public DataStat<T>{
+class ReferenceStat : public DataStat<T> {
private:
const T* d_data;
{}
ReferenceStat(const std::string& s, const T& data):
- DataStat<T>(s),d_data(NULL)
+ DataStat<T>(s), d_data(NULL)
{
setData(data);
}
- void setData(const T& t){
- if(USE_STATISTICS){
+ void setData(const T& t) {
+ if(__CVC4_USE_STATISTICS) {
d_data = &t;
}
}
- const T& getData() const{
- if(USE_STATISTICS){
+ const T& getData() const {
+ if(__CVC4_USE_STATISTICS) {
return *d_data;
- }else{
+ } else {
Unreachable();
}
}
-};
+};/* class ReferenceStat */
+
/** T must have an operator=() and a copy constructor. */
template <class T>
-class BackedStat: public DataStat<T>{
+class BackedStat : public DataStat<T> {
protected:
T d_data;
{}
void setData(const T& t) {
- if(USE_STATISTICS){
+ if(__CVC4_USE_STATISTICS) {
d_data = t;
}
}
- BackedStat<T>& operator=(const T& t){
- if(USE_STATISTICS){
+ BackedStat<T>& operator=(const T& t) {
+ if(__CVC4_USE_STATISTICS) {
d_data = t;
}
return *this;
}
- const T& getData() const{
- if(USE_STATISTICS){
+ const T& getData() const {
+ if(__CVC4_USE_STATISTICS) {
return d_data;
- }else{
+ } else {
Unreachable();
}
}
-};
+};/* class BackedStat */
+
-class IntStat : public BackedStat<int64_t>{
+class IntStat : public BackedStat<int64_t> {
public:
IntStat(const std::string& s, int64_t init): BackedStat<int64_t>(s, init)
{}
- IntStat& operator++(){
- if(USE_STATISTICS){
+ IntStat& operator++() {
+ if(__CVC4_USE_STATISTICS) {
++d_data;
}
return *this;
}
- IntStat& operator+=(int64_t val){
- if(USE_STATISTICS){
+ IntStat& operator+=(int64_t val) {
+ if(__CVC4_USE_STATISTICS) {
d_data+= val;
}
return *this;
}
- void maxAssign(int64_t val){
- if(USE_STATISTICS){
- if(d_data < val){
+ void maxAssign(int64_t val) {
+ if(__CVC4_USE_STATISTICS) {
+ if(d_data < val) {
d_data = val;
}
}
}
- void minAssign(int64_t val){
- if(USE_STATISTICS){
- if(d_data > val){
+ void minAssign(int64_t val) {
+ if(__CVC4_USE_STATISTICS) {
+ if(d_data > val) {
d_data = val;
}
}
}
-};
+};/* class IntStat */
+
+
+// some utility functions for ::timespec
+inline ::timespec& operator+=(::timespec& a, const ::timespec& b) {
+ // assumes a.tv_nsec and b.tv_nsec are in range
+ const long nsec_per_sec = 1000000000L; // one thousand million
+ a.tv_sec += b.tv_sec;
+ long nsec = a.tv_nsec + b.tv_nsec;
+ while(nsec < 0) {
+ nsec += nsec_per_sec;
+ ++a.tv_sec;
+ }
+ while(nsec >= nsec_per_sec) {
+ nsec -= nsec_per_sec;
+ --a.tv_sec;
+ }
+ a.tv_nsec = nsec;
+ return a;
+}
+inline ::timespec& operator-=(::timespec& a, const ::timespec& b) {
+ // assumes a.tv_nsec and b.tv_nsec are in range
+ const long nsec_per_sec = 1000000000L; // one thousand million
+ a.tv_sec -= b.tv_sec;
+ long nsec = a.tv_nsec - b.tv_nsec;
+ while(nsec < 0) {
+ nsec += nsec_per_sec;
+ ++a.tv_sec;
+ }
+ while(nsec >= nsec_per_sec) {
+ nsec -= nsec_per_sec;
+ --a.tv_sec;
+ }
+ a.tv_nsec = nsec;
+ return a;
+}
+inline ::timespec operator+(const ::timespec& a, const ::timespec& b) {
+ ::timespec result = a;
+ return result += b;
+}
+inline ::timespec operator-(const ::timespec& a, const ::timespec& b) {
+ ::timespec result = a;
+ return result -= b;
+}
+inline bool operator==(const ::timespec& a, const ::timespec& b) {
+ // assumes a.tv_nsec and b.tv_nsec are in range
+ return a.tv_sec == b.tv_sec && a.tv_nsec == b.tv_nsec;
+}
+inline bool operator!=(const ::timespec& a, const ::timespec& b) {
+ // assumes a.tv_nsec and b.tv_nsec are in range
+ return !(a == b);
+}
+inline bool operator<(const ::timespec& a, const ::timespec& b) {
+ // assumes a.tv_nsec and b.tv_nsec are in range
+ return a.tv_sec < b.tv_sec ||
+ (a.tv_sec == b.tv_sec && a.tv_nsec < b.tv_nsec);
+}
+inline bool operator>(const ::timespec& a, const ::timespec& b) {
+ // assumes a.tv_nsec and b.tv_nsec are in range
+ return a.tv_sec > b.tv_sec ||
+ (a.tv_sec == b.tv_sec && a.tv_nsec > b.tv_nsec);
+}
+inline bool operator<=(const ::timespec& a, const ::timespec& b) {
+ // assumes a.tv_nsec and b.tv_nsec are in range
+ return !(a > b);
+}
+inline bool operator>=(const ::timespec& a, const ::timespec& b) {
+ // assumes a.tv_nsec and b.tv_nsec are in range
+ return !(a < b);
+}
+inline std::ostream& operator<<(std::ostream& os, const ::timespec& t) {
+ // assumes t.tv_nsec is in range
+ return os << t.tv_sec << "."
+ << std::setfill('0') << std::setw(8) << std::right << t.tv_nsec;
+}
+
+
+class TimerStat : public BackedStat< ::timespec > {
+ // strange: timespec isn't placed in 'std' namespace ?!
+ ::timespec d_start;
+ bool d_running;
+
+public:
+
+ TimerStat(const std::string& s) :
+ BackedStat< ::timespec >(s, ::timespec()),
+ d_running(false) {
+ }
+
+ void start() {
+ if(__CVC4_USE_STATISTICS) {
+ AlwaysAssert(!d_running);
+ clock_gettime(CLOCK_REALTIME, &d_start);
+ }
+ }
+
+ void stop() {
+ if(__CVC4_USE_STATISTICS) {
+ AlwaysAssert(d_running);
+ ::timespec end;
+ clock_gettime(CLOCK_REALTIME, &end);
+ d_data += end - d_start;
+ }
+ }
+};/* class TimerStat */
+
-#undef USE_STATISTICS
+#undef __CVC4_USE_STATISTICS
}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file stats_black.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::Stat and associated classes
+ **
+ ** Black box testing of CVC4::Stat and associated classes.
+ **/
+
+#include <cxxtest/TestSuite.h>
+#include <sstream>
+#include <string>
+#include <ctime>
+
+#include "util/stats.h"
+
+using namespace CVC4;
+using namespace std;
+
+class StatsBlack : public CxxTest::TestSuite {
+public:
+
+ void testStats() {
+
+ // StatisticsRegistry
+ //static void flushStatistics(std::ostream& out);
+
+ //static inline void registerStat(Stat* s) throw (AssertionException);
+ //static inline void unregisterStat(Stat* s) throw (AssertionException);
+
+ string empty, bar = "bar", baz = "baz";
+ ReferenceStat<string> refStr("stat #1", empty);
+ ReferenceStat<string> refStr2("refStr2", bar);
+ // setData
+ // getData
+
+ // flushInformation
+ // flushStat
+
+ BackedStat<string> backedStr("backed", baz);
+ // setData
+ // getData
+ // operator=
+
+ IntStat sInt("my int", 10);
+ TimerStat sTimer("a timer ! for measuring time");
+
+ TS_ASSERT_EQUALS(refStr.getName(), "stat #1");
+ TS_ASSERT_EQUALS(refStr2.getName(), "refStr2");
+ TS_ASSERT_EQUALS(backedStr.getName(), "backed");
+ TS_ASSERT_EQUALS(sInt.getName(), "my int");
+ TS_ASSERT_EQUALS(sTimer.getName(), "a timer ! for measuring time");
+
+ TS_ASSERT_EQUALS(refStr.getData(), empty);
+ TS_ASSERT_EQUALS(refStr2.getData(), bar);
+ empty = "a different string";
+ bar += " and with an addition";
+ TS_ASSERT_EQUALS(refStr.getData(), empty);
+ TS_ASSERT_EQUALS(refStr2.getData(), bar);
+
+ TS_ASSERT_EQUALS(backedStr.getData(), "baz");
+ baz = "something else";
+ TS_ASSERT_EQUALS(backedStr.getData(), "baz");
+
+ TS_ASSERT_EQUALS(sInt.getData(), 10);
+ sInt.setData(100);
+ TS_ASSERT_EQUALS(sInt.getData(), 100);
+
+ TS_ASSERT_EQUALS(sTimer.getData(), timespec());
+
+ stringstream sstr;
+
+ refStr.flushInformation(sstr);
+ TS_ASSERT_EQUALS(sstr.str(), empty);
+ sstr.str("");
+ refStr2.flushInformation(sstr);
+ TS_ASSERT_EQUALS(sstr.str(), bar);
+ sstr.str("");
+ backedStr.flushInformation(sstr);
+ TS_ASSERT_EQUALS(sstr.str(), "baz");
+ sstr.str("");
+ sInt.flushInformation(sstr);
+ TS_ASSERT_EQUALS(sstr.str(), "100");
+ sstr.str("");
+ sTimer.flushInformation(sstr);
+ TS_ASSERT_EQUALS(sstr.str(), "0.00000000");
+
+ sTimer.start();
+ TS_ASSERT_EQUALS(timespec(), sTimer.getData());
+ sTimer.stop();
+ TS_ASSERT_LESS_THAN(timespec(), sTimer.getData());
+ }
+
+};
projects / cvc5.git / commitdiff