Merging the statistics branch into the main trunk. I'll go over how to use this Tuesd...

diff --git a/configure.ac b/configure.ac
index f805c445c2d4b7c0d018ca67bfa39b0a922dff8b..28a5cca7aa6be8059492217bba624aa3adc1362a 100644 (file)
--- a/configure.ac
+++ b/configure.ac
@@ -71,7 +71,7 @@ AC_ARG_WITH([build],
 if test -z "${with_build+set}" -o "$with_build" = default; then
   with_build=default
 fi
-if test -z "${enable_optimized+set}" -a -z "${enable_debug_symbols+set}" -a -z "${enable_assertions+set}" -a -z "${enable_tracing+set}" -a -z "${enable_muzzle+set}" -a -z "${enable_coverage+set}" -a -z "${enable_profiling+set}"; then
+if test -z "${enable_optimized+set}" -a -z "${enable_debug_symbols+set}" -a -z "${enable_assertions+set}" -a -z "${enable_tracing+set}" -a -z "${enable_muzzle+set}" -a -z "${enable_coverage+set}" -a -z "${enable_profiling+set}" -a -z "${enable_statistics+set}"; then
   custom_build_profile=no
 else
   custom_build_profile=yes
@@ -126,6 +126,13 @@ if test -n "${enable_profiling+set}"; then
     btargs="$btargs noprofiling"
   fi
 fi
+if test -n "${enable_statistics+set}"; then
+  if test "$enable_statistics" = yes; then
+    btargs="$btargs statistics"
+  else
+    btargs="$btargs nostatistics"
+  fi
+fi
 AC_MSG_RESULT([$with_build])
 
 AC_MSG_CHECKING([for appropriate build string])
@@ -199,6 +206,7 @@ case "$with_build" in
     if test -z "${OPTLEVEL+set}"            ; then OPTLEVEL=3                       ; fi
     if test -z "${enable_optimized+set}"    ; then enable_optimized=yes             ; fi
     if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes         ; fi
+    if test -z "${enable_statistics+set}"   ; then enable_statistics=yes            ; fi
     if test -z "${enable_assertions+set}"   ; then enable_assertions=no             ; fi
     if test -z "${enable_tracing+set}"      ; then enable_tracing=no                ; fi
     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
@@ -213,6 +221,7 @@ case "$with_build" in
     if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes         ; fi
     if test -z "${enable_assertions+set}"   ; then enable_assertions=yes            ; fi
     if test -z "${enable_tracing+set}"      ; then enable_tracing=yes               ; fi
+    if test -z "${enable_statistics+set}"   ; then enable_statistics=yes            ; fi
     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
     ;;
   default) # moderately optimized, assertions, tracing
@@ -225,6 +234,7 @@ case "$with_build" in
     if test -z "${enable_optimized+set}"    ; then enable_optimized=yes             ; fi
     if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes         ; fi
     if test -z "${enable_assertions+set}"   ; then enable_assertions=yes            ; fi
+    if test -z "${enable_statistics+set}"   ; then enable_statistics=yes            ; fi
     if test -z "${enable_tracing+set}"      ; then enable_tracing=yes               ; fi
     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
     ;;
@@ -238,6 +248,7 @@ case "$with_build" in
     if test -z "${enable_optimized+set}"    ; then enable_optimized=yes             ; fi
     if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=no          ; fi
     if test -z "${enable_assertions+set}"   ; then enable_assertions=no             ; fi
+    if test -z "${enable_statistics+set}"   ; then enable_statistics=no             ; fi
     if test -z "${enable_tracing+set}"      ; then enable_tracing=no                ; fi
     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=yes                ; fi
     ;;
@@ -302,6 +313,23 @@ if test "$enable_debug_symbols" = yes; then
   CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-ggdb3"
 fi
 
+AC_MSG_CHECKING([whether to include statistics are turned on in libcvc4])
+
+AC_ARG_ENABLE([statistics],
+  [AS_HELP_STRING([--disable-statistics],
+     [do not include statistics in libcvc4])])
+
+if test -z "${enable_statistics+set}"; then
+  enable_statistics=yes
+fi
+
+AC_MSG_RESULT([$enable_statistics])
+
+if test "$enable_statistics" = yes; then
+  CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-DCVC4_STATISTICS_ON"
+  CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-DCVC4_STATISTICS_ON"
+fi
+
 AC_MSG_CHECKING([whether to include assertions in build])
 
 AC_ARG_ENABLE([assertions],
@@ -603,6 +631,7 @@ Muzzle       : $enable_muzzle
 gcov support : $enable_coverage
 gprof support: $enable_profiling
 unit tests   : $support_unit_tests
+statistics   : $enable_statistics
 
 static libs  : $enable_static
 shared libs  : $enable_shared

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 7fb0d92c9819ab35b39e8785d7b068b0e42bb44c..5c19a995ded6a4a87e85622278e6a11cf7a1efd1 100644 (file)
--- 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 4adaa143406d6a6f53a31736d06e639828411cb5..c33982ddca2ce9aa3080c9dee327554eb6bf6632 100644 (file)
--- 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 e023410c73284f3be181dee75d4ba6dd51d0e1a9..f64697d7bcaba8da4ca2d0723eb74d2a809cf6db 100644 (file)
--- 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 18bea2b8d84801d017563d88d5f71cb19a90dd70..c16d8f1830009c837f06534b4088765e7e39017c 100644 (file)
--- 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 cb0705f4c2c23837e67c73b7443f569aa3bd75f7..aff60f651e3955b7b5ae5ae4a7048be94d2e22a7 100644 (file)
--- 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 1912cb0264bece44af6d4f3b4c7434601f44c411..bf4d8d10cc2bc90cdf48f46f1ffdd5d8032c9d25 100644 (file)
--- 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 88d4fc56ebd700f28fa66e119b5f7c3b8c167092..0f6fb592954cd013b82ec0c2bb4621bc9e93e754 100644 (file)
--- 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 f789313b82625fd34206df0b60a5bdc0bd6be456..9440b6df361f7e21c72d380122cbd36722dbcd2e 100644 (file)
--- 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 e3ba969ec2f3644020166fc8c70a19dc21e7e0c4..746d9aaaf3b098c80d9e7dfcdf8fe4ae5e291add 100644 (file)
--- 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 de237b7936447d4a00b4cc2627de1eb6d354ac88..692d3d7421b0cbc8e6fc041bf646ca1a35b61ea4 100644 (file)
--- 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 708628c2448fc790171970e8c450df68778c683a..6a6130886ceb2925fd9048b6e1fffa1b3b07d369 100644 (file)
--- 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 d1921f59778ba26bcc0e95e4ce8911dae18cbdea..f3431334d44699def1241d4573a574754a95d604 100644 (file)
--- 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 81e0f7fbd9ea0eb745188e8367d17fd037ae98d9..feca66da18faa190e414c82e00cfa11372cd608f 100644 (file)
--- 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 f00343729afb8df8d8d8590de9803aa09dcb0598..607075658ae06cdab85490e8b2d05fc366c282eb 100644 (file)
--- 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 (file)
index 0000000..cf7b3ad
--- /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
+ **
+ ** \brief [[ 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 (file)
index 0000000..b9f0fdf
--- /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
+ **
+ ** \brief [[ 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 */