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.

16 files changed, 394 insertions, 23 deletions

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 7fb0d92c9..5c19a995d 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -35,6 +35,7 @@
 #include "util/output.h"
 #include "util/options.h"
 #include "util/result.h"
+#include "util/stats.h"
 
 using namespace std;
 using namespace CVC4;
@@ -85,6 +86,7 @@ int main(int argc, char* argv[]) {
   }
 }
 
+
 int runCvc4(int argc, char* argv[]) {
 
   // Initialize the signal handlers
@@ -183,6 +185,10 @@ int runCvc4(int argc, char* argv[]) {
   // Remove the parser
   delete parser;
 
+  if(options.statistics){
+    StatisticsRegistry::flushStatistics(cerr);
+  }
+
   switch(lastResult.asSatisfiabilityResult().isSAT()) {
 
   case Result::SAT:
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 4adaa1434..c33982ddc 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -90,8 +90,7 @@ public:
    * PropEngine and Theory).  For now, there's nothing to do here in
    * the PropEngine.
    */
-  void shutdown() {
-  }
+  void shutdown() { }
 
   /**
    * Converts the given formula to CNF and assert the CNF to the sat solver.
diff --git a/src/prop/sat.h b/src/prop/sat.h
index e023410c7..f64697d7b 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -26,6 +26,7 @@
 #define __CVC4_USE_MINISAT
 
 #include "util/options.h"
+#include "util/stats.h"
 
 #ifdef __CVC4_USE_MINISAT
 
@@ -132,6 +133,49 @@ class SatSolver : public SatInputInterface {
   /** Minisat solver */
   minisat::SimpSolver* d_minisat;
 
+  class Statistics {
+  private:
+    ReferenceStat<uint64_t> d_statStarts, d_statDecisions;
+    ReferenceStat<uint64_t> d_statRndDecisions, d_statPropagations;
+    ReferenceStat<uint64_t> d_statConflicts, d_statClausesLiterals;
+    ReferenceStat<uint64_t> d_statLearntsLiterals,  d_statMaxLiterals;
+    ReferenceStat<uint64_t> d_statTotLiterals;
+  public:
+    Statistics() :
+      d_statStarts("sat::starts"),
+      d_statDecisions("sat::decisions"),
+      d_statRndDecisions("sat::rnd_decisions"),
+      d_statPropagations("sat::propagations"),
+      d_statConflicts("sat::conflicts"),
+      d_statClausesLiterals("sat::clauses_literals"),
+      d_statLearntsLiterals("sat::learnts_literals"),
+      d_statMaxLiterals("sat::max_literals"),
+      d_statTotLiterals("sat::tot_literals")
+    {
+      StatisticsRegistry::registerStat(&d_statStarts);
+      StatisticsRegistry::registerStat(&d_statDecisions);
+      StatisticsRegistry::registerStat(&d_statRndDecisions);
+      StatisticsRegistry::registerStat(&d_statPropagations);
+      StatisticsRegistry::registerStat(&d_statConflicts);
+      StatisticsRegistry::registerStat(&d_statClausesLiterals);
+      StatisticsRegistry::registerStat(&d_statLearntsLiterals);
+      StatisticsRegistry::registerStat(&d_statMaxLiterals);
+      StatisticsRegistry::registerStat(&d_statTotLiterals);
+    }
+    void init(minisat::SimpSolver* d_minisat){
+      d_statStarts.setData(d_minisat->starts);
+      d_statDecisions.setData(d_minisat->decisions);
+      d_statRndDecisions.setData(d_minisat->rnd_decisions);
+      d_statPropagations.setData(d_minisat->propagations);
+      d_statConflicts.setData(d_minisat->conflicts);
+      d_statClausesLiterals.setData(d_minisat->clauses_literals);
+      d_statLearntsLiterals.setData(d_minisat->learnts_literals);
+      d_statMaxLiterals.setData(d_minisat->max_literals);
+      d_statTotLiterals.setData(d_minisat->tot_literals);
+    }
+  };
+  Statistics d_statistics;
+
 #endif /* __CVC4_USE_MINISAT */
 
 protected:
@@ -150,7 +194,7 @@ public:
   ~SatSolver();
 
   bool solve();
-  
+
   void addClause(SatClause& clause, bool lemma);
 
   SatVariable newVar(bool theoryAtom = false);
@@ -158,7 +202,7 @@ public:
   void theoryCheck(SatClause& conflict);
 
   void enqueueTheoryLiteral(const SatLiteral& l);
-  
+
   void setCnfStream(CnfStream* cnfStream);
 
   SatLiteralValue value(SatLiteral l);
@@ -173,7 +217,8 @@ inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine,
   d_propEngine(propEngine),
   d_cnfStream(NULL),
   d_theoryEngine(theoryEngine),
-  d_context(context)
+  d_context(context),
+  d_statistics()
 {
   // Create the solver
   d_minisat = new minisat::SimpSolver(this, d_context);
@@ -183,6 +228,8 @@ inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine,
   d_minisat->remove_satisfied = false;
   // Make minisat reuse the literal values
   d_minisat->polarity_mode = minisat::SimpSolver::polarity_user;
+
+  d_statistics.init(d_minisat);
 }
 
 inline SatSolver::~SatSolver() {
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 18bea2b8d..c16d8f183 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -54,11 +54,11 @@ TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) :
   d_constants(NodeManager::currentNM()),
   d_partialModel(c),
   d_diseq(c),
-  d_rewriter(&d_constants)
+  d_rewriter(&d_constants),
+  d_statistics()
 {
   uint64_t ass_id = partial_model::Assignment::getId();
   Debug("arithsetup") << "Assignment: " << ass_id << std::endl;
-
 }
 TheoryArith::~TheoryArith(){
   for(vector<Node>::iterator i=d_variables.begin(); i!= d_variables.end(); ++i){
@@ -67,6 +67,20 @@ TheoryArith::~TheoryArith(){
   }
 }
 
+TheoryArith::Statistics::Statistics():
+  d_statPivots("theory::arith::pivots",0),
+  d_statUpdates("theory::arith::updates",0),
+  d_statAssertUpperConflicts("theory::arith::AssertUpperConflicts", 0),
+  d_statAssertLowerConflicts("theory::arith::AssertLowerConflicts", 0),
+  d_statUpdateConflicts("theory::arith::UpdateConflicts", 0)
+{
+  StatisticsRegistry::registerStat(&d_statPivots);
+  StatisticsRegistry::registerStat(&d_statUpdates);
+  StatisticsRegistry::registerStat(&d_statAssertUpperConflicts);
+  StatisticsRegistry::registerStat(&d_statAssertLowerConflicts);
+  StatisticsRegistry::registerStat(&d_statUpdateConflicts);
+}
+
 bool isBasicSum(TNode n){
   if(n.getKind() != kind::PLUS) return false;
 
@@ -260,6 +274,7 @@ bool TheoryArith::AssertUpper(TNode n, TNode original){
     Node lbc = d_partialModel.getLowerConstraint(x_i);
     Node conflict =  NodeManager::currentNM()->mkNode(AND, lbc, original);
     Debug("arith") << "AssertUpper conflict " << conflict << endl;
+    ++(d_statistics.d_statAssertUpperConflicts);
     d_out->conflict(conflict);
     return true;
   }
@@ -294,6 +309,7 @@ bool TheoryArith::AssertLower(TNode n, TNode original){
     Node conflict =  NodeManager::currentNM()->mkNode(AND, ubc, original);
     d_out->conflict(conflict);
     Debug("arith") << "AssertLower conflict " << conflict << endl;
+    ++(d_statistics.d_statAssertLowerConflicts);
     return true;
   }
 
@@ -362,6 +378,7 @@ bool TheoryArith::AssertEquality(TNode n, TNode original){
 void TheoryArith::update(TNode x_i, DeltaRational& v){
   Assert(!isBasic(x_i));
   DeltaRational assignment_x_i = d_partialModel.getAssignment(x_i);
+  ++(d_statistics.d_statUpdates);
 
   Debug("arith") <<"update " << x_i << ": "
                  << assignment_x_i << "|-> " << v << endl;
@@ -422,6 +439,7 @@ void TheoryArith::pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v){
     }
   }
 
+  ++(d_statistics.d_statPivots);
   d_tableau.pivot(x_i, x_j);
 
   checkBasicVariable(x_j);
@@ -507,6 +525,7 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
       DeltaRational l_i = d_partialModel.getLowerBound(x_i);
       TNode x_j = selectSlackBelow(x_i);
       if(x_j == TNode::null() ){
+        ++(d_statistics.d_statUpdateConflicts);
         return generateConflictBelow(x_i); //unsat
       }
       pivotAndUpdate(x_i, x_j, l_i);
@@ -515,6 +534,7 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
       DeltaRational u_i = d_partialModel.getUpperBound(x_i);
       TNode x_j = selectSlackAbove(x_i);
       if(x_j == TNode::null() ){
+        ++(d_statistics.d_statUpdateConflicts);
         return generateConflictAbove(x_i); //unsat
       }
       pivotAndUpdate(x_i, x_j, u_i);
@@ -630,11 +650,6 @@ bool TheoryArith::assertionCases(TNode original, TNode assertion){
     return AssertLower(assertion, original);
   case EQUAL:
     return AssertEquality(assertion,original);
-//     if(AssertUpper(assertion, original)){
-//       return true;
-//     }else{
-//       return AssertLower(assertion, original);
-//     }
   case NOT:
     {
       TNode atom = assertion[0];
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index cb0705f4c..aff60f651 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -31,6 +31,8 @@
 #include "theory/arith/arith_rewriter.h"
 #include "theory/arith/partial_model.h"
 
+#include "util/stats.h"
+
 #include <vector>
 #include <queue>
 
@@ -94,6 +96,7 @@ private:
    */
   ArithRewriter d_rewriter;
 
+
 public:
   TheoryArith(context::Context* c, OutputChannel& out);
   ~TheoryArith();
@@ -115,6 +118,9 @@ public:
   void propagate(Effort e) { Unimplemented(); }
   void explain(TNode n, Effort e) { Unimplemented(); }
 
+  void shutdown(){ }
+
+
 private:
   /**
    * Assert*(n, orig) takes an bound n that is implied by orig.
@@ -228,6 +234,18 @@ private:
   //TODO get rid of this!
   Node simulatePreprocessing(TNode n);
 
+
+  /** These fields are designed to be accessable to TheoryArith methods. */
+  class Statistics {
+  public:
+    IntStat d_statPivots, d_statUpdates, d_statAssertUpperConflicts;
+    IntStat d_statAssertLowerConflicts, d_statUpdateConflicts;
+
+    Statistics();
+  };
+
+  Statistics d_statistics;
+
 };
 
 }/* CVC4::theory::arith namespace */
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 1912cb026..bf4d8d10c 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -32,6 +32,8 @@
 #include "theory/arrays/theory_arrays.h"
 #include "theory/bv/theory_bv.h"
 
+#include "util/stats.h"
+
 namespace CVC4 {
 
 // In terms of abstraction, this is below (and provides services to)
@@ -74,24 +76,31 @@ class TheoryEngine {
     void conflict(TNode conflictNode, bool safe) throw(theory::Interrupted, AssertionException) {
       Debug("theory") << "EngineOutputChannel::conflict(" << conflictNode << ")" << std::endl;
       d_conflictNode = conflictNode;
+      ++(d_engine->d_statistics.d_statConflicts);
       if(safe) {
         throw theory::Interrupted();
       }
     }
 
     void propagate(TNode, bool) throw(theory::Interrupted, AssertionException) {
+      ++(d_engine->d_statistics.d_statPropagate);
     }
 
     void lemma(TNode node, bool) throw(theory::Interrupted, AssertionException) {
+      ++(d_engine->d_statistics.d_statLemma);
       d_engine->newLemma(node);
     }
     void augmentingLemma(TNode node, bool) throw(theory::Interrupted, AssertionException) {
+      ++(d_engine->d_statistics.d_statAugLemma);
       d_engine->newAugmentingLemma(node);
     }
     void explanation(TNode, bool) throw(theory::Interrupted, AssertionException) {
+      ++(d_engine->d_statistics.d_statExplanatation);
     }
   };
 
+
+
   EngineOutputChannel d_theoryOut;
 
   theory::booleans::TheoryBool d_bool;
@@ -100,6 +109,7 @@ class TheoryEngine {
   theory::arrays::TheoryArrays d_arrays;
   theory::bv::TheoryBV d_bv;
 
+
   /**
    * Check whether a node is in the rewrite cache or not.
    */
@@ -190,7 +200,8 @@ public:
     d_uf(ctxt, d_theoryOut),
     d_arith(ctxt, d_theoryOut),
     d_arrays(ctxt, d_theoryOut),
-    d_bv(ctxt, d_theoryOut) {
+    d_bv(ctxt, d_theoryOut),
+    d_statistics() {
 
     d_theoryOfTable.registerTheory(&d_bool);
     d_theoryOfTable.registerTheory(&d_uf);
@@ -319,6 +330,26 @@ public:
     return d_theoryOut.d_conflictNode;
   }
 
+private:
+  class Statistics {
+  public:
+    IntStat d_statConflicts, d_statPropagate, d_statLemma, d_statAugLemma, d_statExplanatation;
+    Statistics():
+      d_statConflicts("theory::conlficts",0),
+      d_statPropagate("theory::propagate",0),
+      d_statLemma("theory::lemma",0),
+      d_statAugLemma("theory::aug_lemma", 0),
+      d_statExplanatation("theory::explanation", 0)
+    {
+      StatisticsRegistry::registerStat(&d_statConflicts);
+      StatisticsRegistry::registerStat(&d_statPropagate);
+      StatisticsRegistry::registerStat(&d_statLemma);
+      StatisticsRegistry::registerStat(&d_statAugLemma);
+      StatisticsRegistry::registerStat(&d_statExplanatation);
+    }
+  };
+  Statistics d_statistics;
+
 };/* class TheoryEngine */
 
 }/* CVC4 namespace */
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 */