From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 13 Nov 2014 00:42:23 +0000 (-0500)
Subject: New, uniform checkTime statistic for all theories (as discussed in meeting).
X-Git-Tag: cvc5-1.0.0~6491
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a64af5c3903cbe75214016aef4b5a3994256e6f8;p=cvc5.git

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 83d837322..ce29fd34d 100644
--- 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 535a54fd7..2130b21f5 100644
--- 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 c657796ee..d6537c562 100644
--- 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 9a661ab0c..8b313e124 100644
--- 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 371b00b0c..b2e039912 100644
--- 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 eddd5017c..08fe5f2e9 100644
--- 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 453f8eb7f..dd56ebba9 100644
--- 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 6963251b8..139a811b8 100644
--- 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 9e402f430..55dec35e9 100644
--- 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 6dac8a72d..5c68e52a7 100644
--- 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 6febc8417..aace13b24 100644
--- 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 106ad6e56..db93c597c 100644
--- 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 87a05bbeb..55bd0eefd 100644
--- 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 536987073..643f2ab7f 100644
--- 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 254aa9138..402a3c731 100644
--- 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 509d7be02..62f2a5ec2 100644
--- 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 867dd7c31..2dab434d1 100644
--- 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 2b9fc3daf..8fa7d2dbc 100644
--- 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