added number of resource units used as a stat

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 74cdee0b793c76a25fdbdc20bd88fc485aa3764d..8f5ba2024041279e3db1d0c48fa7347413b82594 100644 (file)
--- 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));

diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp
index b0fd37fd239f51e094831dc7f1ca43e812ea91c5..7aeb2fc0f09533becdfdf27fc9030344de502c19 100644 (file)
--- a/src/util/resource_manager.cpp
+++ b/src/util/resource_manager.cpp
@@ -172,10 +172,10 @@ unsigned long ResourceManager::getTimeRemaining() const {
 
 void ResourceManager::spendResource() throw (UnsafeInterruptException) {
   ++d_spendResourceCalls;
+  ++d_cumulativeResourceUsed;
   if (!d_on) return;
 
   Debug("limit") << "ResourceManager::spendResource()" << std::endl;
-  ++d_cumulativeResourceUsed;
   ++d_thisCallResourceUsed;
   if(out()) {
     Trace("limit") << "ResourceManager::spendResource: interrupt!" << std::endl;

diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h
index a16f60910ba550724820d7c06a4a2afb320117e9..94e7dbba20c04c00a5dfd9a51b976a78b26fdcf9 100644 (file)
--- a/src/util/resource_manager.h
+++ b/src/util/resource_manager.h
@@ -150,7 +150,7 @@ public:
   void endCall();
 
   static unsigned long getFrequencyCount() { return s_resourceCount; }
-
+  friend class SmtEngine;
 };/* class ResourceManager */
 
 }/* CVC4 namespace */