added number of resource units used as a stat

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));