diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-11-12 19:42:23 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-11-17 16:21:40 -0500 |
commit | a64af5c3903cbe75214016aef4b5a3994256e6f8 (patch) | |
tree | 1d5d8ee15a53d2576cf61ffbbc3efb2aaf962f53 /src/theory/theory.h | |
parent | 3ba7ed6b1b09739385ae2ffb77a5c7ccd18b40a5 (diff) |
New, uniform checkTime statistic for all theories (as discussed in meeting).
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r-- | src/theory/theory.h | 8 |
1 files changed, 6 insertions, 2 deletions
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); } |