Merging the statistics branch into the main trunk. I'll go over how to use this Tuesday during the meeting. You'll need to run autogen and receonfigure after updating.

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 */