summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
Diffstat (limited to 'src/util')
-rw-r--r--src/util/Makefile.am4
-rw-r--r--src/util/bitvector.cpp2
-rw-r--r--src/util/bitvector.h2
-rw-r--r--src/util/gmp_util.h2
-rw-r--r--src/util/hash.h2
-rw-r--r--src/util/integer.h4
-rw-r--r--src/util/rational.h4
-rw-r--r--src/util/sexpr.h2
-rw-r--r--src/util/stats.cpp39
-rw-r--r--src/util/stats.h214
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback