diff options
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 33 |
1 files changed, 32 insertions, 1 deletions
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 */ |