diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 38 |
1 files changed, 33 insertions, 5 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index a55b3a1c9..bcc16c63a 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -49,9 +49,10 @@ using namespace std; -using namespace CVC4; using namespace CVC4::theory; +namespace CVC4 { + void TheoryEngine::finishInit() { PROOF (ProofManager::initTheoryProof(); ); @@ -152,13 +153,13 @@ TheoryEngine::TheoryEngine(context::Context* context, d_curr_model = new theory::TheoryModel(userContext, "DefaultModel", true); d_curr_model_builder = new theory::TheoryEngineModelBuilder(this); - StatisticsRegistry::registerStat(&d_combineTheoriesTime); + smtStatisticsRegistry()->registerStat(&d_combineTheoriesTime); d_true = NodeManager::currentNM()->mkConst<bool>(true); d_false = NodeManager::currentNM()->mkConst<bool>(false); d_iteUtilities = new ITEUtilities(d_iteRemover.getContainsVisitor()); - StatisticsRegistry::registerStat(&d_arithSubstitutionsAdded); + smtStatisticsRegistry()->registerStat(&d_arithSubstitutionsAdded); } TheoryEngine::~TheoryEngine() { @@ -178,13 +179,13 @@ TheoryEngine::~TheoryEngine() { delete d_masterEqualityEngine; - StatisticsRegistry::unregisterStat(&d_combineTheoriesTime); + smtStatisticsRegistry()->unregisterStat(&d_combineTheoriesTime); delete d_unconstrainedSimp; delete d_iteUtilities; - StatisticsRegistry::unregisterStat(&d_arithSubstitutionsAdded); + smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded); } void TheoryEngine::interrupt() throw(ModalException) { @@ -1762,3 +1763,30 @@ std::pair<bool, Node> TheoryEngine::entailmentCheck(theory::TheoryOfMode mode, T void TheoryEngine::spendResource(unsigned ammount) { d_resourceManager->spendResource(ammount); } + +TheoryEngine::Statistics::Statistics(theory::TheoryId theory): + conflicts(mkName("theory<", theory, ">::conflicts"), 0), + propagations(mkName("theory<", theory, ">::propagations"), 0), + lemmas(mkName("theory<", theory, ">::lemmas"), 0), + requirePhase(mkName("theory<", theory, ">::requirePhase"), 0), + flipDecision(mkName("theory<", theory, ">::flipDecision"), 0), + restartDemands(mkName("theory<", theory, ">::restartDemands"), 0) +{ + smtStatisticsRegistry()->registerStat(&conflicts); + smtStatisticsRegistry()->registerStat(&propagations); + smtStatisticsRegistry()->registerStat(&lemmas); + smtStatisticsRegistry()->registerStat(&requirePhase); + smtStatisticsRegistry()->registerStat(&flipDecision); + smtStatisticsRegistry()->registerStat(&restartDemands); +} + +TheoryEngine::Statistics::~Statistics() { + smtStatisticsRegistry()->unregisterStat(&conflicts); + smtStatisticsRegistry()->unregisterStat(&propagations); + smtStatisticsRegistry()->unregisterStat(&lemmas); + smtStatisticsRegistry()->unregisterStat(&requirePhase); + smtStatisticsRegistry()->unregisterStat(&flipDecision); + smtStatisticsRegistry()->unregisterStat(&restartDemands); +} + +}/* CVC4 namespace */ |