diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Makefile.am | 4 | ||||
-rw-r--r-- | src/util/bitvector.cpp | 2 | ||||
-rw-r--r-- | src/util/bitvector.h | 2 | ||||
-rw-r--r-- | src/util/gmp_util.h | 2 | ||||
-rw-r--r-- | src/util/hash.h | 2 | ||||
-rw-r--r-- | src/util/integer.h | 4 | ||||
-rw-r--r-- | src/util/rational.h | 4 | ||||
-rw-r--r-- | src/util/sexpr.h | 2 | ||||
-rw-r--r-- | src/util/stats.cpp | 39 | ||||
-rw-r--r-- | src/util/stats.h | 214 |
10 files changed, 265 insertions, 10 deletions
diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 88d4fc56e..0f6fb5929 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -30,4 +30,6 @@ libutil_la_SOURCES = \ bitvector.h \ bitvector.cpp \ gmp_util.h \ - sexpr.h + sexpr.h \ + stats.h \ + stats.cpp diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp index f789313b8..9440b6df3 100644 --- a/src/util/bitvector.cpp +++ b/src/util/bitvector.cpp @@ -2,7 +2,7 @@ /*! \file bitvector.cpp ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters ** 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) diff --git a/src/util/bitvector.h b/src/util/bitvector.h index e3ba969ec..746d9aaaf 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: dejan ** Major contributors: cconway - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h index de237b793..692d3d742 100644 --- a/src/util/gmp_util.h +++ b/src/util/gmp_util.h @@ -2,7 +2,7 @@ /*! \file gmp_util.h ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters ** 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) diff --git a/src/util/hash.h b/src/util/hash.h index 708628c24..6a6130886 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -2,7 +2,7 @@ /*! \file hash.h ** \verbatim ** Original author: cconway - ** Major contributors: none + ** Major contributors: mdeters ** 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) diff --git a/src/util/integer.h b/src/util/integer.h index d1921f597..f3431334d 100644 --- a/src/util/integer.h +++ b/src/util/integer.h @@ -2,8 +2,8 @@ /*! \file integer.h ** \verbatim ** Original author: taking - ** Major contributors: none - ** Minor contributors (to current version): dejan, cconway, mdeters + ** Major contributors: mdeters + ** Minor contributors (to current version): dejan, cconway ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/util/rational.h b/src/util/rational.h index 81e0f7fbd..feca66da1 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -2,8 +2,8 @@ /*! \file rational.h ** \verbatim ** Original author: taking - ** Major contributors: cconway - ** Minor contributors (to current version): dejan, mdeters + ** Major contributors: none + ** Minor contributors (to current version): dejan, mdeters, cconway ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/util/sexpr.h b/src/util/sexpr.h index f00343729..607075658 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/util/stats.cpp b/src/util/stats.cpp new file mode 100644 index 000000000..cf7b3ad51 --- /dev/null +++ b/src/util/stats.cpp @@ -0,0 +1,39 @@ +/********************* */ +/*! \file stats.cpp + ** \verbatim + ** Original author: taking + ** 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 + ** + ** rief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "util/stats.h" + +using namespace CVC4; + +StatisticsRegistry::StatSet StatisticsRegistry::d_registeredStats; + +std::string Stat::s_delim(","); + + + + +void StatisticsRegistry::flushStatistics(std::ostream& out){ +#ifdef CVC4_STATISTICS_ON + for(StatSet::iterator i=d_registeredStats.begin();i != d_registeredStats.end();++i){ + Stat* s = *i; + s->flushStat(out); + out << std::endl; + } +#endif +} diff --git a/src/util/stats.h b/src/util/stats.h new file mode 100644 index 000000000..b9f0fdf61 --- /dev/null +++ b/src/util/stats.h @@ -0,0 +1,214 @@ +/********************* */ +/*! \file stats.h + ** \verbatim + ** Original author: taking + ** 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 + ** + ** rief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__STATS_H +#define __CVC4__STATS_H + +#include <string> +#include <ostream> +#include <set> +#include "util/Assert.h" + +namespace CVC4 { + + +#ifdef CVC4_STATISTICS_ON +#define USE_STATISTICS true +#else +#define USE_STATISTICS false +#endif + +class CVC4_PUBLIC Stat; + +class CVC4_PUBLIC StatisticsRegistry { +private: + struct StatCmp; + + typedef std::set< Stat*, StatCmp > StatSet; + static StatSet d_registeredStats; + +public: + static void flushStatistics(std::ostream& out); + + static inline void registerStat(Stat* s) throw (AssertionException); +}; /* class StatisticsRegistry */ + + +class CVC4_PUBLIC Stat { +private: + std::string d_name; + + static std::string s_delim; + +public: + + Stat(const std::string& s) throw (CVC4::AssertionException) : d_name(s) + { + if(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){ + out << d_name << s_delim; + flushInformation(out); + } + } + + const std::string& getName() const { + return d_name; + } +}; + +struct StatisticsRegistry::StatCmp { + bool operator()(const Stat* s1, const Stat* s2) const + { + return (s1->getName()) < (s2->getName()); + } +}; + +inline void StatisticsRegistry::registerStat(Stat* s) throw (AssertionException){ + if(USE_STATISTICS){ + AlwaysAssert(d_registeredStats.find(s) == d_registeredStats.end()); + d_registeredStats.insert(s); + } +} + + +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){ + out << getData(); + } + } +}; + +template <class T> +class ReferenceStat: public DataStat<T>{ +private: + const T* d_data; + +public: + ReferenceStat(const std::string& s): DataStat<T>(s), d_data(NULL){} + + ReferenceStat(const std::string& s, const T& data):ReferenceStat<T>(s){ + setData(data); + } + + void setData(const T& t){ + if(USE_STATISTICS){ + d_data = &t; + } + } + const T& getData() const{ + if(USE_STATISTICS){ + return *d_data; + }else{ + Unreachable(); + } + } +}; + +/** T must have an operator=() and a copy constructor. */ +template <class T> +class BackedStat: public DataStat<T>{ +protected: + T d_data; + +public: + + BackedStat(const std::string& s, const T& init): DataStat<T>(s), d_data(init) + {} + + void setData(const T& t) { + if(USE_STATISTICS){ + d_data = t; + } + } + + BackedStat<T>& operator=(const T& t){ + if(USE_STATISTICS){ + d_data = t; + } + return *this; + } + + const T& getData() const{ + if(USE_STATISTICS){ + return d_data; + }else{ + Unreachable(); + } + } +}; + +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){ + ++d_data; + } + return *this; + } + + IntStat& operator+=(int64_t val){ + if(USE_STATISTICS){ + d_data+= val; + } + return *this; + } + + void maxAssign(int64_t val){ + if(USE_STATISTICS){ + if(d_data < val){ + d_data = val; + } + } + } + + void minAssign(int64_t val){ + if(USE_STATISTICS){ + if(d_data > val){ + d_data = val; + } + } + } +}; + +#undef USE_STATISTICS + +}/* CVC4 namespace */ + +#endif /* __CVC4__STATS_H */ |