diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-07-16 15:53:22 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-07-16 15:53:22 +0000 |
commit | 36615c5e7332e26645b33ce9b6bab25439a5108e (patch) | |
tree | 166efefced107009f4a68ff3d0c6623540dfa435 /src/util | |
parent | 25396f93b7df85c80a39ed207483e28a8c86ff26 (diff) |
Support for having two SmtEngines with the same ExprManager.
Basically, this involves creating a separate StatisticsRegistry for the
ExprManager and for the SmtEngine. Otherwise, theories register the
same statistic twice. This is a larger problem, though, for creating
multiple instances of theories, and that is unaddressed. Still,
separating out the expr statistics into a separate registry is probably
a good idea, since the expr package is somewhat separate anyway (and in
the short term it allows two SmtEngines to co-exist).
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/stats.cpp | 24 | ||||
-rw-r--r-- | src/util/stats.h | 3 |
2 files changed, 19 insertions, 8 deletions
diff --git a/src/util/stats.cpp b/src/util/stats.cpp index b030495c5..96e300197 100644 --- a/src/util/stats.cpp +++ b/src/util/stats.cpp @@ -20,7 +20,10 @@ #include "util/stats.h" #include "expr/node_manager.h" #include "expr/expr_manager_scope.h" +#include "expr/expr_manager.h" #include "lib/clock_gettime.h" +#include "smt/smt_engine_scope.h" +#include "smt/smt_engine.h" #ifdef CVC4_STATISTICS_ON # define __CVC4_USE_STATISTICS true @@ -34,12 +37,12 @@ std::string Stat::s_delim(","); std::string StatisticsRegistry::s_regDelim("::"); StatisticsRegistry* StatisticsRegistry::current() { - return NodeManager::currentNM()->getStatisticsRegistry(); + return smt::currentSmtEngine()->getStatisticsRegistry(); } void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) { #ifdef CVC4_STATISTICS_ON - StatSet& registeredStats = NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats; + StatSet& registeredStats = current()->d_registeredStats; AlwaysAssert(registeredStats.find(s) == registeredStats.end(), "Statistic `%s' was already registered with this registry.", s->getName().c_str()); registeredStats.insert(s); @@ -55,7 +58,7 @@ void StatisticsRegistry::registerStat_(Stat* s) throw(AssertionException) { void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) { #ifdef CVC4_STATISTICS_ON - StatSet& registeredStats = NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats; + StatSet& registeredStats = current()->d_registeredStats; AlwaysAssert(registeredStats.find(s) != registeredStats.end(), "Statistic `%s' was not registered with this registry.", s->getName().c_str()); registeredStats.erase(s); @@ -91,11 +94,11 @@ void StatisticsRegistry::flushStat(std::ostream &out) const {; } StatisticsRegistry::const_iterator StatisticsRegistry::begin() { - return NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats.begin(); + return current()->d_registeredStats.begin(); }/* StatisticsRegistry::begin() */ StatisticsRegistry::const_iterator StatisticsRegistry::end() { - return NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats.end(); + return current()->d_registeredStats.end(); }/* StatisticsRegistry::end() */ void TimerStat::start() { @@ -117,9 +120,14 @@ void TimerStat::stop() { }/* TimerStat::stop() */ RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) : - d_reg(NULL), + d_reg(em.getStatisticsRegistry()), d_stat(stat) { - ExprManagerScope ems(em); - d_reg = StatisticsRegistry::current(); d_reg->registerStat_(d_stat); } + +RegisterStatistic::RegisterStatistic(SmtEngine& smt, Stat* stat) : + d_reg(smt.getStatisticsRegistry()), + d_stat(stat) { + d_reg->registerStat_(d_stat); +} + diff --git a/src/util/stats.h b/src/util/stats.h index 63e732305..aabf04dc0 100644 --- a/src/util/stats.h +++ b/src/util/stats.h @@ -43,6 +43,7 @@ namespace CVC4 { #endif class ExprManager; +class SmtEngine; class CVC4_PUBLIC Stat; @@ -803,6 +804,8 @@ public: RegisterStatistic(ExprManager& em, Stat* stat); + RegisterStatistic(SmtEngine& smt, Stat* stat); + ~RegisterStatistic() { d_reg->unregisterStat_(d_stat); } |