New, uniform checkTime statistic for all theories (as discussed in meeting).

diff --git a/contrib/alttheoryskel/theory_DIR.cpp b/contrib/alttheoryskel/theory_DIR.cpp
index 83d837322bf0862ebb48c34bfef5bc6221a1e1dc..ce29fd34dfbdd947f0ed8e487fbba795103f2af1 100644 (file)
--- a/contrib/alttheoryskel/theory_DIR.cpp
+++ b/contrib/alttheoryskel/theory_DIR.cpp
@@ -16,6 +16,11 @@ Theory$camel::Theory$camel(context::Context* c,
 }/* Theory$camel::Theory$camel() */
 
 void Theory$camel::check(Effort level) {
+  if (done() && !fullEffort(level)) {
+    return;
+  }
+
+  TimerStat::CodeTimer checkTimer(d_checkTime);
 
   while(!done()) {
     // Get all the assertions

diff --git a/contrib/theoryskel/theory_DIR.cpp b/contrib/theoryskel/theory_DIR.cpp
index 535a54fd7ae8b9b2b259ab033ecdc4d24b8dbb4f..2130b21f55db7471c9aaded8b2adb1fc70087d84 100644 (file)
--- a/contrib/theoryskel/theory_DIR.cpp
+++ b/contrib/theoryskel/theory_DIR.cpp
@@ -20,6 +20,8 @@ void Theory$camel::check(Effort level) {
     return;
   }
 
+  TimerStat::CodeTimer checkTimer(d_checkTime);
+
   while(!done()) {
     // Get all the assertions
     Assertion assertion = get();

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index c657796ee8a8f95ef6d3c33de4f305103a18f322..d6537c56200a877d3e5ac7a638eb20f6fd6e4ed0 100644 (file)
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -3346,6 +3346,7 @@ bool TheoryArithPrivate::hasFreshArithLiteral(Node n) const{
 
 void TheoryArithPrivate::check(Theory::Effort effortLevel){
   Assert(d_currentPropagationList.empty());
+  TimerStat::CodeTimer checkTimer(d_containing.d_checkTime);
   //cout << "TheoryArithPrivate::check " << effortLevel << std::endl;
   Debug("effortlevel") << "TheoryArithPrivate::check " << effortLevel << std::endl;
   Debug("arith") << "TheoryArithPrivate::check begun " << effortLevel << std::endl;

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 9a661ab0cd9bb50bc19d96ecf2d815d4cf65998a..8b313e124dd9e5867dc55e4966c1b83565a91531 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -61,7 +61,6 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC
   d_numGetModelValConflicts("theory::arrays::number of getModelVal conflicts", 0),
   d_numSetModelValSplits("theory::arrays::number of setModelVal splits", 0),
   d_numSetModelValConflicts("theory::arrays::number of setModelVal conflicts", 0),
-  d_checkTimer("theory::arrays::checkTime"),
   d_ppEqualityEngine(u, "theory::arrays::TheoryArraysPP"),
   d_ppFacts(u),
   //  d_ppCache(u),
@@ -103,7 +102,6 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC
   StatisticsRegistry::registerStat(&d_numGetModelValConflicts);
   StatisticsRegistry::registerStat(&d_numSetModelValSplits);
   StatisticsRegistry::registerStat(&d_numSetModelValConflicts);
-  StatisticsRegistry::registerStat(&d_checkTimer);
 
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
@@ -142,7 +140,6 @@ TheoryArrays::~TheoryArrays() {
   StatisticsRegistry::unregisterStat(&d_numGetModelValConflicts);
   StatisticsRegistry::unregisterStat(&d_numSetModelValSplits);
   StatisticsRegistry::unregisterStat(&d_numSetModelValConflicts);
-  StatisticsRegistry::unregisterStat(&d_checkTimer);
 }
 
 void TheoryArrays::setMasterEqualityEngine(eq::EqualityEngine* eq) {
@@ -1034,7 +1031,7 @@ void TheoryArrays::check(Effort e) {
   if (done() && !fullEffort(e)) {
     return;
   }
-  TimerStat::CodeTimer codeTimer(d_checkTimer);
+  TimerStat::CodeTimer checkTimer(d_checkTime);
 
   while (!done() && !d_conflict)
   {

diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 371b00b0c276c86a46c40c73dec040c2210085e3..b2e039912f58db6814747e3fbb89a4faba63aadd 100644 (file)
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -123,8 +123,6 @@ class TheoryArrays : public Theory {
   IntStat d_numSetModelValSplits;
   /** conflicts in setModelVal */
   IntStat d_numSetModelValConflicts;
-  /** time spent in check() */
-  TimerStat d_checkTimer;
 
   public:
 

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index eddd5017c78555c0549d394f2ce9169c8de9f857..08fe5f2e99cc648b5a1252ce5c3f442a3d2b1784 100644 (file)
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -365,6 +365,7 @@ void TheoryBV::check(Effort e)
   if (done() && !fullEffort(e)) {
     return;
   }
+  TimerStat::CodeTimer checkTimer(d_checkTime);
   Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
   TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer);
   // we may be getting new assertions so the model cache may not be sound

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 453f8eb7f2fd873c2504ddeb1b6d692ddca8aa68..dd56ebba98f61078935c56c3ee0232882b20eace 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -124,6 +124,8 @@ void TheoryDatatypes::check(Effort e) {
     return;
   }
 
+  TimerStat::CodeTimer checkTimer(d_checkTime);
+
   Trace("datatypes-debug") << "Check effort " << e << std::endl;
   while(!done() && !d_conflict) {
     // Get all the assertions

diff --git a/src/theory/example/theory_uf_tim.cpp b/src/theory/example/theory_uf_tim.cpp
index 6963251b8fa5195ba39b9e2d0b9a1560b9993cbf..139a811b80f8a72628c1d821607483c45c5b907d 100644 (file)
--- a/src/theory/example/theory_uf_tim.cpp
+++ b/src/theory/example/theory_uf_tim.cpp
@@ -271,6 +271,11 @@ Node TheoryUFTim::constructConflict(TNode diseq) {
 }
 
 void TheoryUFTim::check(Effort level) {
+  if (done() && !fullEffort(level)) {
+    return;
+  }
+
+  TimerStat::CodeTimer checkTimer(d_checkTime);
 
   Debug("uf") << "uf: begin check(" << level << ")" << std::endl;
 

diff --git a/src/theory/idl/theory_idl.cpp b/src/theory/idl/theory_idl.cpp
index 9e402f4306a68c571dd00bcd1ec4f2d889c82705..55dec35e9430620cb31064a0f0e56e24759f66b0 100644 (file)
--- a/src/theory/idl/theory_idl.cpp
+++ b/src/theory/idl/theory_idl.cpp
@@ -49,10 +49,11 @@ Node TheoryIdl::ppRewrite(TNode atom) {
 }
 
 void TheoryIdl::check(Effort level) {
-  //// Not needed for now, as no code outside while() loop below.
-  // if (done() && !fullEffort(e)) {
-  //   return;
-  // }
+  if (done() && !fullEffort(level)) {
+    return;
+  }
+
+  TimerStat::CodeTimer checkTimer(d_checkTime);
 
   while(!done()) {
 

diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 6dac8a72d0c1cfffb75f2e8079a2483da3736f15..5c68e52a7ed5855302f49f214a76640884c018ed 100644 (file)
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -116,7 +116,7 @@ void TheoryQuantifiers::check(Effort e) {
     return;
   }
 
-  CodeTimer codeTimer(d_theoryTime);
+  TimerStat::CodeTimer checkTimer(d_checkTime);
 
   Trace("quantifiers-check") << "quantifiers::check(" << e << ")" << std::endl;
   while(!done()) {
@@ -148,7 +148,6 @@ void TheoryQuantifiers::check(Effort e) {
 }
 
 void TheoryQuantifiers::propagate(Effort level){
-  //CodeTimer codeTimer(d_theoryTime);
   //getQuantifiersEngine()->propagate( level );
 }
 

diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 6febc84178e0110efe8ad16e3b8464fbb34a0f8d..aace13b241177cef4b4769b11448d794495b4bd8 100644 (file)
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -47,8 +47,6 @@ private:
   /** number of restarts */
   int d_numRestarts;
 
-  KEEP_STATISTIC(TimerStat, d_theoryTime, "theory::quantifiers::theoryTime");
-
   eq::EqualityEngine* d_masterEqualityEngine;
 
 public:

diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 106ad6e5627ae2130c0ad3df9eb2780e7ebcd02e..db93c597c96a78442dfae1799f828fd2385c198b 100644 (file)
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -42,6 +42,7 @@ void TheorySets::check(Effort e) {
   if (done() && !fullEffort(e)) {
     return;
   }
+  TimerStat::CodeTimer checkTimer(d_checkTime);
   d_internal->check(e);
 }
 

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 87a05bbeb079fdba2c18a6384f125ce2cb4da819..55bd0eefdf85a1d3ad7fc7287b73be8d21440cf4 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -42,8 +42,6 @@ const char* element_of_str = " \u2208 ";
 
 void TheorySetsPrivate::check(Theory::Effort level) {
 
-  CodeTimer checkCodeTimer(d_statistics.d_checkTime);
-
   while(!d_external.done() && !d_conflict) {
     // Get all the assertions
     Assertion assertion = d_external.get();
@@ -916,12 +914,10 @@ Node mkAnd(const std::vector<TNode>& conjunctions) {
 
 
 TheorySetsPrivate::Statistics::Statistics() :
-  d_checkTime("theory::sets::time")
-  , d_getModelValueTime("theory::sets::getModelValueTime")
+    d_getModelValueTime("theory::sets::getModelValueTime")
   , d_memberLemmas("theory::sets::lemmas::member", 0)
   , d_disequalityLemmas("theory::sets::lemmas::disequality", 0)
 {
-  StatisticsRegistry::registerStat(&d_checkTime);
   StatisticsRegistry::registerStat(&d_getModelValueTime);
   StatisticsRegistry::registerStat(&d_memberLemmas);
   StatisticsRegistry::registerStat(&d_disequalityLemmas);
@@ -929,7 +925,6 @@ TheorySetsPrivate::Statistics::Statistics() :
 
 
 TheorySetsPrivate::Statistics::~Statistics() {
-  StatisticsRegistry::unregisterStat(&d_checkTime);
   StatisticsRegistry::unregisterStat(&d_getModelValueTime);
   StatisticsRegistry::unregisterStat(&d_memberLemmas);
   StatisticsRegistry::unregisterStat(&d_disequalityLemmas);

diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 5369870737ddccef34f641b8c2665532a245e86d..643f2ab7f1ebf051f0133ae6cde495cb2f4819ae 100644 (file)
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -73,7 +73,6 @@ private:
 
   class Statistics {
   public:
-    TimerStat d_checkTime;
     TimerStat d_getModelValueTime;
     IntStat d_memberLemmas;
     IntStat d_disequalityLemmas;

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 254aa9138c939a735596e010dc014f5d46cf5d01..402a3c731e8f3a5bca3ad7ffd4c5c7621340731b 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -558,6 +558,8 @@ void TheoryStrings::check(Effort e) {
     return;
   }
 
+  TimerStat::CodeTimer checkTimer(d_checkTime);
+
   bool polarity;
   TNode atom;
 

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 509d7be02f42ea7eebaa72f9dd292d3d82a93fd7..62f2a5ec2d2ff22c8b34db9df919e80a212dd81e 100644 (file)
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -46,6 +46,7 @@ std::ostream& operator<<(std::ostream& os, Theory::Effort level){
 }/* ostream& operator<<(ostream&, Theory::Effort) */
 
 Theory::~Theory() {
+  StatisticsRegistry::unregisterStat(&d_checkTime);
   StatisticsRegistry::unregisterStat(&d_computeCareGraphTime);
 }
 

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 867dd7c31a2ed0b854a4cb69526c6d3b0ef0ae16..2dab434d1e1f76ef5a5435d8301f0955935213a8 100644 (file)
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -197,7 +197,11 @@ private:
    */
   QuantifiersEngine* d_quantEngine;
 
+protected:
+
   // === STATISTICS ===
+  /** time spent in check calls */
+  TimerStat d_checkTime;
   /** time spent in theory combination */
   TimerStat d_computeCareGraphTime;
 
@@ -207,8 +211,6 @@ private:
     return ss.str();
   }
 
-protected:
-
   /**
    * The only method to add suff to the care graph.
    */
@@ -255,12 +257,14 @@ protected:
   , d_sharedTermsIndex(satContext, 0)
   , d_careGraph(NULL)
   , d_quantEngine(NULL)
+  , d_checkTime(statName(id, "checkTime"))
   , d_computeCareGraphTime(statName(id, "computeCareGraphTime"))
   , d_sharedTerms(satContext)
   , d_out(&out)
   , d_valuation(valuation)
   , d_proofEnabled(false)
   {
+    StatisticsRegistry::registerStat(&d_checkTime);
     StatisticsRegistry::registerStat(&d_computeCareGraphTime);
   }
 

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 2b9fc3daf8ce98f902914606ad25d36fdfc2d6d2..8fa7d2dbc8aa6da8c5a034254659d8823c5c80e1 100644 (file)
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -93,6 +93,8 @@ void TheoryUF::check(Effort level) {
     return;
   }
 
+  TimerStat::CodeTimer checkTimer(d_checkTime);
+
   while (!done() && !d_conflict)
   {
     // Get all the assertions