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.

1 files changed, 32 insertions, 1 deletions

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