diff options
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 74cdee0b7..8f5ba2024 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -209,6 +209,8 @@ struct SmtEngineStatistics { /** Has something simplified to false? */ IntStat d_simplifiedToFalse; + /** Number of resource units spent. */ + ReferenceStat<uint64_t> d_resourceUnitsUsed; SmtEngineStatistics() : d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"), @@ -231,7 +233,8 @@ struct SmtEngineStatistics { d_solveTime("smt::SmtEngine::solveTime"), d_pushPopTime("smt::SmtEngine::pushPopTime"), d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"), - d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0) + d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0), + d_resourceUnitsUsed("smt::SmtEngine::resourceUnitsUsed") { StatisticsRegistry::registerStat(&d_definitionExpansionTime); @@ -255,6 +258,7 @@ struct SmtEngineStatistics { StatisticsRegistry::registerStat(&d_pushPopTime); StatisticsRegistry::registerStat(&d_processAssertionsTime); StatisticsRegistry::registerStat(&d_simplifiedToFalse); + StatisticsRegistry::registerStat(&d_resourceUnitsUsed); } ~SmtEngineStatistics() { @@ -279,6 +283,7 @@ struct SmtEngineStatistics { StatisticsRegistry::unregisterStat(&d_pushPopTime); StatisticsRegistry::unregisterStat(&d_processAssertionsTime); StatisticsRegistry::unregisterStat(&d_simplifiedToFalse); + StatisticsRegistry::unregisterStat(&d_resourceUnitsUsed); } };/* struct SmtEngineStatistics */ @@ -708,7 +713,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_private = new smt::SmtEnginePrivate(*this); d_statisticsRegistry = new StatisticsRegistry(); d_stats = new SmtEngineStatistics(); - + d_stats->d_resourceUnitsUsed.setData(d_private->getResourceManager()->d_cumulativeResourceUsed); // We have mutual dependency here, so we add the prop engine to the theory // engine later (it is non-essential there) d_theoryEngine = new TheoryEngine(d_context, d_userContext, d_private->d_iteRemover, const_cast<const LogicInfo&>(d_logic)); |