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.

3 files changed, 72 insertions, 8 deletions

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