summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/alttheoryskel/theory_DIR.cpp5
-rw-r--r--contrib/theoryskel/theory_DIR.cpp2
-rw-r--r--src/theory/arith/theory_arith_private.cpp1
-rw-r--r--src/theory/arrays/theory_arrays.cpp5
-rw-r--r--src/theory/arrays/theory_arrays.h2
-rw-r--r--src/theory/bv/theory_bv.cpp1
-rw-r--r--src/theory/datatypes/theory_datatypes.cpp2
-rw-r--r--src/theory/example/theory_uf_tim.cpp5
-rw-r--r--src/theory/idl/theory_idl.cpp9
-rw-r--r--src/theory/quantifiers/theory_quantifiers.cpp3
-rw-r--r--src/theory/quantifiers/theory_quantifiers.h2
-rw-r--r--src/theory/sets/theory_sets.cpp1
-rw-r--r--src/theory/sets/theory_sets_private.cpp7
-rw-r--r--src/theory/sets/theory_sets_private.h1
-rw-r--r--src/theory/strings/theory_strings.cpp2
-rw-r--r--src/theory/theory.cpp1
-rw-r--r--src/theory/theory.h8
-rw-r--r--src/theory/uf/theory_uf.cpp2
18 files changed, 36 insertions, 23 deletions
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback