diff options
119 files changed, 1523 insertions, 1428 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index f16c5408b..ec6464cdb 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -105,10 +105,12 @@ libcvc4_la_SOURCES = \ smt/smt_globals.h \ smt/model_postprocessor.cpp \ smt/model_postprocessor.h \ - smt/smt_options_handler.cpp \ - smt/smt_options_handler.h \ smt/smt_engine_scope.cpp \ smt/smt_engine_scope.h \ + smt/smt_options_handler.cpp \ + smt/smt_options_handler.h \ + smt/smt_statistics_registry.cpp \ + smt/smt_statistics_registry.h \ smt/command_list.cpp \ smt/command_list.h \ smt/boolean_terms.h \ diff --git a/src/cvc4.i b/src/cvc4.i index b0fad9f2e..b5ce4a5fa 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -324,12 +324,12 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters; %include "util/regexp.i" %include "util/result.i" %include "util/sexpr.i" +%include "util/statistics.i" %include "util/subrange_bound.i" %include "util/tuple.i" %include "util/unsafe_interrupt_exception.i" %include "expr/uninterpreted_constant.i" -%include "expr/statistics.i" %include "expr/array_store_all.i" %include "expr/ascription_type.i" %include "expr/emptyset.i" diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index 68c7379ce..e9f4997b7 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -23,7 +23,7 @@ #include "options/decision_options.h" #include "theory/rewriter.h" #include "smt_util/ite_removal.h" - +#include "smt/smt_statistics_registry.h" namespace CVC4 { @@ -48,16 +48,16 @@ JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de, d_childCache(uc), d_weightCache(uc), d_startIndexCache(c) { - StatisticsRegistry::registerStat(&d_helfulness); - StatisticsRegistry::registerStat(&d_giveup); - StatisticsRegistry::registerStat(&d_timestat); + smtStatisticsRegistry()->registerStat(&d_helfulness); + smtStatisticsRegistry()->registerStat(&d_giveup); + smtStatisticsRegistry()->registerStat(&d_timestat); Trace("decision") << "Justification heuristic enabled" << std::endl; } JustificationHeuristic::~JustificationHeuristic() throw() { - StatisticsRegistry::unregisterStat(&d_helfulness); - StatisticsRegistry::unregisterStat(&d_giveup); - StatisticsRegistry::unregisterStat(&d_timestat); + smtStatisticsRegistry()->unregisterStat(&d_helfulness); + smtStatisticsRegistry()->unregisterStat(&d_giveup); + smtStatisticsRegistry()->unregisterStat(&d_timestat); } CVC4::prop::SatLiteral JustificationHeuristic::getNext(bool &stopSearch) diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 5c046c282..4648ed3af 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -3,23 +3,10 @@ AM_CPPFLAGS = \ -I@builddir@/.. -I@srcdir@/../include -I@srcdir@/.. AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -#noinst_LTLIBRARIES = libexpr.la libstatistics.la noinst_LTLIBRARIES = libexpr.la -# libstatistics_la_CPPFLAGS = $(CPPFLAGS) $(AM_CPPFLAGS) -D__BUILDING_STATISTICS_FOR_EXPORT -# libstatistics_la_SOURCES = \ -# statistics_registry.h \ -# statistics_registry.cpp - -# EXTRA_libstatistics_la_DEPENDENCIES = \ -# builts - # For some reason statistics were in libutil. No idea why though. libexpr_la_SOURCES = \ - statistics.cpp \ - statistics.h \ - statistics_registry.cpp \ - statistics_registry.h \ array.h \ array_store_all.cpp \ array_store_all.h \ @@ -102,7 +89,6 @@ EXTRA_DIST = \ expr_stream.i \ expr_manager.i \ symbol_table.i \ - statistics.i \ type.i \ kind.i \ expr.i \ diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 59f423e3c..0b9557cc8 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -19,9 +19,9 @@ #include <map> #include "expr/node_manager.h" -#include "expr/statistics_registry.h" #include "expr/variable_type_map.h" #include "options/options.h" +#include "util/statistics_registry.h" ${includes} @@ -38,7 +38,7 @@ ${includes} stringstream statName; \ statName << "expr::ExprManager::" << kind; \ d_exprStatistics[kind] = new IntStat(statName.str(), 0); \ - d_nodeManager->getStatisticsRegistry()->registerStat_(d_exprStatistics[kind]); \ + d_nodeManager->getStatisticsRegistry()->registerStat(d_exprStatistics[kind]); \ } \ ++ *(d_exprStatistics[kind]); \ } @@ -54,7 +54,7 @@ ${includes} statName << "expr::ExprManager::" << ((bound_var) ? "BOUND_VARIABLE" : "VARIABLE") << ":" << type; \ } \ d_exprStatisticsVars[type] = new IntStat(statName.str(), 0); \ - d_nodeManager->getStatisticsRegistry()->registerStat_(d_exprStatisticsVars[type]); \ + d_nodeManager->getStatisticsRegistry()->registerStat(d_exprStatisticsVars[type]); \ } \ ++ *(d_exprStatisticsVars[type]); \ } @@ -100,14 +100,14 @@ ExprManager::~ExprManager() throw() { #ifdef CVC4_STATISTICS_ON for (unsigned i = 0; i < kind::LAST_KIND; ++ i) { if (d_exprStatistics[i] != NULL) { - d_nodeManager->getStatisticsRegistry()->unregisterStat_(d_exprStatistics[i]); + d_nodeManager->getStatisticsRegistry()->unregisterStat(d_exprStatistics[i]); delete d_exprStatistics[i]; d_exprStatistics[i] = NULL; } } for (unsigned i = 0; i < LAST_TYPE; ++ i) { if (d_exprStatisticsVars[i] != NULL) { - d_nodeManager->getStatisticsRegistry()->unregisterStat_(d_exprStatisticsVars[i]); + d_nodeManager->getStatisticsRegistry()->unregisterStat(d_exprStatisticsVars[i]); delete d_exprStatisticsVars[i]; d_exprStatisticsVars[i] = NULL; } @@ -123,10 +123,6 @@ ExprManager::~ExprManager() throw() { } } -StatisticsRegistry* ExprManager::getStatisticsRegistry() throw() { - return d_nodeManager->getStatisticsRegistry(); -} - const Options& ExprManager::getOptions() const { return d_nodeManager->getOptions(); } diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 31983d5a9..e65cfc358 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -24,7 +24,7 @@ #include "expr/expr.h" #include "expr/kind.h" #include "expr/type.h" -#include "expr/statistics.h" +#include "util/statistics.h" #include "util/subrange_bound.h" ${includes} @@ -43,7 +43,6 @@ class NodeManager; class Options; class IntStat; struct ExprManagerMapCollection; -class StatisticsRegistry; class ResourceManager; namespace expr { @@ -52,10 +51,6 @@ namespace expr { }/* CVC4::expr::pickle namespace */ }/* CVC4::expr namespace */ -namespace stats { - StatisticsRegistry* getStatisticsRegistry(ExprManager*); -}/* CVC4::stats namespace */ - class CVC4_PUBLIC ExprManager { private: /** The internal node manager */ @@ -88,12 +83,6 @@ private: /** NodeManager reaches in to get the NodeManager */ friend class NodeManager; - /** Statistics reach in to get the StatisticsRegistry */ - friend ::CVC4::StatisticsRegistry* ::CVC4::stats::getStatisticsRegistry(ExprManager*); - - /** Get the underlying statistics registry. */ - StatisticsRegistry* getStatisticsRegistry() throw(); - // undefined, private copy constructor and assignment op (disallow copy) ExprManager(const ExprManager&) CVC4_UNDEFINED; ExprManager& operator=(const ExprManager&) CVC4_UNDEFINED; diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index c9e6866d4..4cb75bfc7 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -30,7 +30,7 @@ #include "options/options.h" #include "options/smt_options.h" #include "expr/resource_manager.h" -#include "expr/statistics_registry.h" +#include "util/statistics_registry.h" using namespace std; diff --git a/src/expr/statistics_registry.cpp b/src/expr/statistics_registry.cpp deleted file mode 100644 index 3f9124a2f..000000000 --- a/src/expr/statistics_registry.cpp +++ /dev/null @@ -1,176 +0,0 @@ -/********************* */ -/*! \file statistics_registry.cpp - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Kshitij Bansal, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "expr/statistics_registry.h" - -#include "base/cvc4_assert.h" -#include "expr/expr_manager.h" -#include "lib/clock_gettime.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" - - -#ifdef CVC4_STATISTICS_ON -# define __CVC4_USE_STATISTICS true -#else -# define __CVC4_USE_STATISTICS false -#endif - -#warning "TODO: Make StatisticsRegistry non-public again." -#warning "TODO: Make TimerStat non-public again." - -namespace CVC4 { - -/** Construct a statistics registry */ -StatisticsRegistry::StatisticsRegistry(const std::string& name) - throw(CVC4::IllegalArgumentException) : - Stat(name) { - - d_prefix = name; - if(__CVC4_USE_STATISTICS) { - PrettyCheckArgument(d_name.find(s_regDelim) == std::string::npos, name, - "StatisticsRegistry names cannot contain the string \"%s\"", - s_regDelim.c_str()); - } -} - -namespace stats { - -// This is a friend of SmtEngine, just to reach in and get it. -// this isn't a class function because then there's a cyclic -// dependence. -inline StatisticsRegistry* getStatisticsRegistry(SmtEngine* smt) { - return smt->d_statisticsRegistry; -} - -inline StatisticsRegistry* getStatisticsRegistry(ExprManager* em) { - return em->getStatisticsRegistry(); -} - -}/* CVC4::stats namespace */ - -StatisticsRegistry* StatisticsRegistry::current() { - return stats::getStatisticsRegistry(smt::currentSmtEngine()); -} - -void StatisticsRegistry::registerStat(Stat* s) throw(CVC4::IllegalArgumentException) { -#ifdef CVC4_STATISTICS_ON - StatSet& stats = current()->d_stats; - PrettyCheckArgument(stats.find(s) == stats.end(), s, - "Statistic `%s' was already registered with this registry.", - s->getName().c_str()); - stats.insert(s); -#endif /* CVC4_STATISTICS_ON */ -}/* StatisticsRegistry::registerStat() */ - -void StatisticsRegistry::unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException) { -#ifdef CVC4_STATISTICS_ON - StatSet& stats = current()->d_stats; - PrettyCheckArgument(stats.find(s) != stats.end(), s, - "Statistic `%s' was not registered with this registry.", - s->getName().c_str()); - stats.erase(s); -#endif /* CVC4_STATISTICS_ON */ -}/* StatisticsRegistry::unregisterStat() */ - -void StatisticsRegistry::registerStat_(Stat* s) throw(CVC4::IllegalArgumentException) { -#ifdef CVC4_STATISTICS_ON - PrettyCheckArgument(d_stats.find(s) == d_stats.end(), s); - d_stats.insert(s); -#endif /* CVC4_STATISTICS_ON */ -}/* StatisticsRegistry::registerStat_() */ - -void StatisticsRegistry::unregisterStat_(Stat* s) throw(CVC4::IllegalArgumentException) { -#ifdef CVC4_STATISTICS_ON - PrettyCheckArgument(d_stats.find(s) != d_stats.end(), s); - d_stats.erase(s); -#endif /* CVC4_STATISTICS_ON */ -}/* StatisticsRegistry::unregisterStat_() */ - -void StatisticsRegistry::flushStat(std::ostream &out) const { -#ifdef CVC4_STATISTICS_ON - flushInformation(out); -#endif /* CVC4_STATISTICS_ON */ -} - -void StatisticsRegistry::flushInformation(std::ostream &out) const { -#ifdef CVC4_STATISTICS_ON - this->StatisticsBase::flushInformation(out); -#endif /* CVC4_STATISTICS_ON */ -} - -void TimerStat::start() { - if(__CVC4_USE_STATISTICS) { - PrettyCheckArgument(!d_running, *this, "timer already running"); - clock_gettime(CLOCK_MONOTONIC, &d_start); - d_running = true; - } -}/* TimerStat::start() */ - -void TimerStat::stop() { - if(__CVC4_USE_STATISTICS) { - PrettyCheckArgument(d_running, *this, "timer not running"); - ::timespec end; - clock_gettime(CLOCK_MONOTONIC, &end); - d_data += end - d_start; - d_running = false; - } -}/* TimerStat::stop() */ - -bool TimerStat::running() const { - return d_running; -}/* TimerStat::running() */ - -timespec TimerStat::getData() const { - ::timespec data = d_data; - if(__CVC4_USE_STATISTICS && d_running) { - ::timespec end; - clock_gettime(CLOCK_MONOTONIC, &end); - data += end - d_start; - } - return data; -} - -SExpr TimerStat::getValue() const { - ::timespec data = d_data; - if(__CVC4_USE_STATISTICS && d_running) { - ::timespec end; - clock_gettime(CLOCK_MONOTONIC, &end); - data += end - d_start; - } - std::stringstream ss; - ss << std::fixed << std::setprecision(8) << data; - return SExpr(Rational::fromDecimal(ss.str())); -}/* TimerStat::getValue() */ - -RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) : - d_reg(stats::getStatisticsRegistry(&em)), - d_stat(stat) { - d_reg->registerStat_(d_stat); -} - -RegisterStatistic::RegisterStatistic(SmtEngine& smt, Stat* stat) : - d_reg(stats::getStatisticsRegistry(&smt)), - d_stat(stat) { - d_reg->registerStat_(d_stat); -} - - - -}/* CVC4 namespace */ - -#undef __CVC4_USE_STATISTICS diff --git a/src/main/command_executor.h b/src/main/command_executor.h index df9c9e19f..7b6c2fab5 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -19,10 +19,10 @@ #include <string> #include "expr/expr_manager.h" -#include "expr/statistics_registry.h" #include "options/options.h" #include "smt/smt_engine.h" #include "smt_util/command.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace main { diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index cdd20c05a..9d0042694 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -63,8 +63,8 @@ CommandExecutorPortfolio::CommandExecutorPortfolio assert(d_threadOptions.size() == d_numThreads); d_statLastWinner.setData(d_lastWinner); - d_stats.registerStat_(&d_statLastWinner); - d_stats.registerStat_(&d_statWaitTime); + d_stats.registerStat(&d_statLastWinner); + d_stats.registerStat(&d_statWaitTime); /* Duplication, individualization */ d_exprMgrs.push_back(&d_exprMgr); @@ -99,8 +99,8 @@ CommandExecutorPortfolio::~CommandExecutorPortfolio() d_exprMgrs.clear(); d_smts.clear(); - d_stats.unregisterStat_(&d_statLastWinner); - d_stats.unregisterStat_(&d_statWaitTime); + d_stats.unregisterStat(&d_statLastWinner); + d_stats.unregisterStat(&d_statWaitTime); } void CommandExecutorPortfolio::lemmaSharingInit() diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index c110ffa4f..71f47906d 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -28,7 +28,6 @@ #include "base/output.h" #include "expr/expr_iomanip.h" #include "expr/expr_manager.h" -#include "expr/statistics_registry.h" #include "main/command_executor.h" #ifdef PORTFOLIO_BUILD @@ -50,6 +49,7 @@ #include "smt_util/command.h" #include "util/configuration.h" #include "util/result.h" +#include "util/statistics_registry.h" using namespace std; using namespace CVC4; diff --git a/src/main/main.cpp b/src/main/main.cpp index f8cb0677c..92902ac11 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -24,7 +24,6 @@ #include "base/output.h" #include "expr/expr_manager.h" -#include "expr/statistics.h" #include "main/command_executor.h" #include "main/interactive_shell.h" #include "options/base_options.h" @@ -37,6 +36,7 @@ #include "smt_util/command.h" #include "util/configuration.h" #include "util/result.h" +#include "util/statistics.h" using namespace std; using namespace CVC4; diff --git a/src/main/main.h b/src/main/main.h index 7dda429af..2ba688a98 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -21,10 +21,10 @@ #include "base/tls.h" #include "cvc4autoconfig.h" #include "expr/expr_manager.h" -#include "expr/statistics.h" -#include "expr/statistics_registry.h" #include "options/options.h" #include "smt/smt_engine.h" +#include "util/statistics.h" +#include "util/statistics_registry.h" #ifndef __CVC4__MAIN__MAIN_H #define __CVC4__MAIN__MAIN_H diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp index ea7e3d458..22f3a67ae 100644 --- a/src/main/portfolio.cpp +++ b/src/main/portfolio.cpp @@ -20,11 +20,10 @@ #include <boost/exception_ptr.hpp> #include "base/output.h" -#include "expr/statistics_registry.h" #include "options/options.h" #include "smt/smt_engine.h" #include "util/result.h" - +#include "util/statistics_registry.h" namespace CVC4 { diff --git a/src/main/portfolio.h b/src/main/portfolio.h index 5a730c005..cab8bda3c 100644 --- a/src/main/portfolio.h +++ b/src/main/portfolio.h @@ -19,10 +19,10 @@ #include <boost/function.hpp> #include <utility> -#include "expr/statistics_registry.h" #include "options/options.h" #include "smt/smt_engine.h" #include "smt_util/command.h" +#include "util/statistics_registry.h" namespace CVC4 { diff --git a/src/main/util.cpp b/src/main/util.cpp index bc3d45287..abcdcc7c5 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -31,12 +31,12 @@ #include "base/exception.h" #include "base/tls.h" #include "cvc4autoconfig.h" -#include "expr/statistics.h" #include "main/command_executor.h" #include "main/main.h" #include "options/base_options.h" #include "options/options.h" #include "smt/smt_engine.h" +#include "util/statistics.h" using CVC4::Exception; using namespace std; diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index ab157844a..be266b6d8 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -17,21 +17,23 @@ **/ #include "prop/bvminisat/bvminisat.h" + #include "prop/bvminisat/simp/SimpSolver.h" +#include "util/statistics_registry.h" -using namespace CVC4; -using namespace prop; +namespace CVC4 { +namespace prop { -BVMinisatSatSolver::BVMinisatSatSolver(context::Context* mainSatContext, const std::string& name) +BVMinisatSatSolver::BVMinisatSatSolver(StatisticsRegistry* registry, context::Context* mainSatContext, const std::string& name) : context::ContextNotifyObj(mainSatContext, false), d_minisat(new BVMinisat::SimpSolver(mainSatContext)), d_minisatNotify(0), d_assertionsCount(0), d_assertionsRealCount(mainSatContext, 0), d_lastPropagation(mainSatContext, 0), - d_statistics(name) + d_statistics(registry, name) { - d_statistics.init(d_minisat); + d_statistics.init(d_minisat); } @@ -208,59 +210,63 @@ void BVMinisatSatSolver::toSatClause(BVMinisat::vec<BVMinisat::Lit>& clause, // Satistics for BVMinisatSatSolver -BVMinisatSatSolver::Statistics::Statistics(const std::string& prefix) : - d_statStarts("theory::bv::"+prefix+"bvminisat::starts"), - d_statDecisions("theory::bv::"+prefix+"bvminisat::decisions"), - d_statRndDecisions("theory::bv::"+prefix+"bvminisat::rnd_decisions"), - d_statPropagations("theory::bv::"+prefix+"bvminisat::propagations"), - d_statConflicts("theory::bv::"+prefix+"bvminisat::conflicts"), - d_statClausesLiterals("theory::bv::"+prefix+"bvminisat::clauses_literals"), - d_statLearntsLiterals("theory::bv::"+prefix+"bvminisat::learnts_literals"), - d_statMaxLiterals("theory::bv::"+prefix+"bvminisat::max_literals"), - d_statTotLiterals("theory::bv::"+prefix+"bvminisat::tot_literals"), - d_statEliminatedVars("theory::bv::"+prefix+"bvminisat::eliminated_vars"), - d_statCallsToSolve("theory::bv::"+prefix+"bvminisat::calls_to_solve", 0), - d_statSolveTime("theory::bv::"+prefix+"bvminisat::solve_time", 0), - d_registerStats(!prefix.empty()) +BVMinisatSatSolver::Statistics::Statistics(StatisticsRegistry* registry, const std::string& prefix) + : d_registry(registry), + d_statStarts("theory::bv::"+prefix+"bvminisat::starts"), + d_statDecisions("theory::bv::"+prefix+"bvminisat::decisions"), + d_statRndDecisions("theory::bv::"+prefix+"bvminisat::rnd_decisions"), + d_statPropagations("theory::bv::"+prefix+"bvminisat::propagations"), + d_statConflicts("theory::bv::"+prefix+"bvminisat::conflicts"), + d_statClausesLiterals("theory::bv::"+prefix+"bvminisat::clauses_literals"), + d_statLearntsLiterals("theory::bv::"+prefix+"bvminisat::learnts_literals"), + d_statMaxLiterals("theory::bv::"+prefix+"bvminisat::max_literals"), + d_statTotLiterals("theory::bv::"+prefix+"bvminisat::tot_literals"), + d_statEliminatedVars("theory::bv::"+prefix+"bvminisat::eliminated_vars"), + d_statCallsToSolve("theory::bv::"+prefix+"bvminisat::calls_to_solve", 0), + d_statSolveTime("theory::bv::"+prefix+"bvminisat::solve_time", 0), + d_registerStats(!prefix.empty()) { - if (!d_registerStats) + if (!d_registerStats){ return; + } - StatisticsRegistry::registerStat(&d_statStarts); - StatisticsRegistry::registerStat(&d_statDecisions); - StatisticsRegistry::registerStat(&d_statRndDecisions); - StatisticsRegistry::registerStat(&d_statPropagations); - StatisticsRegistry::registerStat(&d_statConflicts); - StatisticsRegistry::registerStat(&d_statClausesLiterals); - StatisticsRegistry::registerStat(&d_statLearntsLiterals); - StatisticsRegistry::registerStat(&d_statMaxLiterals); - StatisticsRegistry::registerStat(&d_statTotLiterals); - StatisticsRegistry::registerStat(&d_statEliminatedVars); - StatisticsRegistry::registerStat(&d_statCallsToSolve); - StatisticsRegistry::registerStat(&d_statSolveTime); + d_registry->registerStat(&d_statStarts); + d_registry->registerStat(&d_statDecisions); + d_registry->registerStat(&d_statRndDecisions); + d_registry->registerStat(&d_statPropagations); + d_registry->registerStat(&d_statConflicts); + d_registry->registerStat(&d_statClausesLiterals); + d_registry->registerStat(&d_statLearntsLiterals); + d_registry->registerStat(&d_statMaxLiterals); + d_registry->registerStat(&d_statTotLiterals); + d_registry->registerStat(&d_statEliminatedVars); + d_registry->registerStat(&d_statCallsToSolve); + d_registry->registerStat(&d_statSolveTime); } BVMinisatSatSolver::Statistics::~Statistics() { - if (!d_registerStats) + if (!d_registerStats){ return; - StatisticsRegistry::unregisterStat(&d_statStarts); - StatisticsRegistry::unregisterStat(&d_statDecisions); - StatisticsRegistry::unregisterStat(&d_statRndDecisions); - StatisticsRegistry::unregisterStat(&d_statPropagations); - StatisticsRegistry::unregisterStat(&d_statConflicts); - StatisticsRegistry::unregisterStat(&d_statClausesLiterals); - StatisticsRegistry::unregisterStat(&d_statLearntsLiterals); - StatisticsRegistry::unregisterStat(&d_statMaxLiterals); - StatisticsRegistry::unregisterStat(&d_statTotLiterals); - StatisticsRegistry::unregisterStat(&d_statEliminatedVars); - StatisticsRegistry::unregisterStat(&d_statCallsToSolve); - StatisticsRegistry::unregisterStat(&d_statSolveTime); + } + d_registry->unregisterStat(&d_statStarts); + d_registry->unregisterStat(&d_statDecisions); + d_registry->unregisterStat(&d_statRndDecisions); + d_registry->unregisterStat(&d_statPropagations); + d_registry->unregisterStat(&d_statConflicts); + d_registry->unregisterStat(&d_statClausesLiterals); + d_registry->unregisterStat(&d_statLearntsLiterals); + d_registry->unregisterStat(&d_statMaxLiterals); + d_registry->unregisterStat(&d_statTotLiterals); + d_registry->unregisterStat(&d_statEliminatedVars); + d_registry->unregisterStat(&d_statCallsToSolve); + d_registry->unregisterStat(&d_statSolveTime); } void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){ - if (!d_registerStats) + if (!d_registerStats){ return; - + } + d_statStarts.setData(minisat->starts); d_statDecisions.setData(minisat->decisions); d_statRndDecisions.setData(minisat->rnd_decisions); @@ -272,3 +278,6 @@ void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){ d_statTotLiterals.setData(minisat->tot_literals); d_statEliminatedVars.setData(minisat->eliminated_vars); } + +} /* namespace CVC4::prop */ +} /* namespace CVC4 */ diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index fc5b29e89..986fbf339 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -20,9 +20,10 @@ #pragma once -#include "prop/sat_solver.h" -#include "prop/bvminisat/simp/SimpSolver.h" #include "context/cdo.h" +#include "prop/bvminisat/simp/SimpSolver.h" +#include "prop/sat_solver.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace prop { @@ -67,13 +68,7 @@ protected: public: - BVMinisatSatSolver() : - ContextNotifyObj(NULL, false), - d_assertionsRealCount(NULL, (unsigned)0), - d_lastPropagation(NULL, (unsigned)0), - d_statistics("") - { Unreachable(); } - BVMinisatSatSolver(context::Context* mainSatContext, const std::string& name = ""); + BVMinisatSatSolver(StatisticsRegistry* registry, context::Context* mainSatContext, const std::string& name = ""); ~BVMinisatSatSolver() throw(AssertionException); void setNotify(Notify* notify); @@ -90,7 +85,7 @@ public: void markUnremovable(SatLiteral lit); void interrupt(); - + SatValue solve(); SatValue solve(long unsigned int&); void getUnsatCore(SatClause& unsatCore); @@ -117,11 +112,16 @@ public: void explain(SatLiteral lit, std::vector<SatLiteral>& explanation); SatValue assertAssumption(SatLiteral lit, bool propagate); - + void popAssumption(); +private: + /* Disable the default constructor. */ + BVMinisatSatSolver() CVC4_UNUSED; + class Statistics { public: + StatisticsRegistry* d_registry; ReferenceStat<uint64_t> d_statStarts, d_statDecisions; ReferenceStat<uint64_t> d_statRndDecisions, d_statPropagations; ReferenceStat<uint64_t> d_statConflicts, d_statClausesLiterals; @@ -131,7 +131,7 @@ public: IntStat d_statCallsToSolve; BackedStat<double> d_statSolveTime; bool d_registerStats; - Statistics(const std::string& prefix); + Statistics(StatisticsRegistry* registry, const std::string& prefix); ~Statistics(); void init(BVMinisat::SimpSolver* minisat); }; diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h index bef8e0a70..85556e935 100644 --- a/src/prop/bvminisat/simp/SimpSolver.h +++ b/src/prop/bvminisat/simp/SimpSolver.h @@ -22,9 +22,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #define BVMinisat_SimpSolver_h #include "context/context.h" -#include "expr/statistics_registry.h" #include "prop/bvminisat/core/Solver.h" #include "prop/bvminisat/mtl/Queue.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace BVMinisat { diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index d9b8bb4f8..ce5c1eb92 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -23,15 +23,17 @@ #include "options/prop_options.h" #include "options/smt_options.h" #include "prop/minisat/simp/SimpSolver.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace prop { //// DPllMinisatSatSolver -MinisatSatSolver::MinisatSatSolver() : +MinisatSatSolver::MinisatSatSolver(StatisticsRegistry* registry) : d_minisat(NULL), - d_context(NULL) + d_context(NULL), + d_statistics(registry) {} MinisatSatSolver::~MinisatSatSolver() throw() @@ -229,38 +231,41 @@ void MinisatSatSolver::pop() { /// Statistics for MinisatSatSolver -MinisatSatSolver::Statistics::Statistics() : - d_statStarts("sat::starts"), - d_statDecisions("sat::decisions"), - d_statRndDecisions("sat::rnd_decisions"), - d_statPropagations("sat::propagations"), - d_statConflicts("sat::conflicts"), - d_statClausesLiterals("sat::clauses_literals"), - d_statLearntsLiterals("sat::learnts_literals"), - d_statMaxLiterals("sat::max_literals"), - d_statTotLiterals("sat::tot_literals") +MinisatSatSolver::Statistics::Statistics(StatisticsRegistry* registry) : + d_registry(registry), + d_statStarts("sat::starts"), + d_statDecisions("sat::decisions"), + d_statRndDecisions("sat::rnd_decisions"), + d_statPropagations("sat::propagations"), + d_statConflicts("sat::conflicts"), + d_statClausesLiterals("sat::clauses_literals"), + d_statLearntsLiterals("sat::learnts_literals"), + d_statMaxLiterals("sat::max_literals"), + d_statTotLiterals("sat::tot_literals") { - StatisticsRegistry::registerStat(&d_statStarts); - StatisticsRegistry::registerStat(&d_statDecisions); - StatisticsRegistry::registerStat(&d_statRndDecisions); - StatisticsRegistry::registerStat(&d_statPropagations); - StatisticsRegistry::registerStat(&d_statConflicts); - StatisticsRegistry::registerStat(&d_statClausesLiterals); - StatisticsRegistry::registerStat(&d_statLearntsLiterals); - StatisticsRegistry::registerStat(&d_statMaxLiterals); - StatisticsRegistry::registerStat(&d_statTotLiterals); + d_registry->registerStat(&d_statStarts); + d_registry->registerStat(&d_statDecisions); + d_registry->registerStat(&d_statRndDecisions); + d_registry->registerStat(&d_statPropagations); + d_registry->registerStat(&d_statConflicts); + d_registry->registerStat(&d_statClausesLiterals); + d_registry->registerStat(&d_statLearntsLiterals); + d_registry->registerStat(&d_statMaxLiterals); + d_registry->registerStat(&d_statTotLiterals); } + MinisatSatSolver::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_statStarts); - StatisticsRegistry::unregisterStat(&d_statDecisions); - StatisticsRegistry::unregisterStat(&d_statRndDecisions); - StatisticsRegistry::unregisterStat(&d_statPropagations); - StatisticsRegistry::unregisterStat(&d_statConflicts); - StatisticsRegistry::unregisterStat(&d_statClausesLiterals); - StatisticsRegistry::unregisterStat(&d_statLearntsLiterals); - StatisticsRegistry::unregisterStat(&d_statMaxLiterals); - StatisticsRegistry::unregisterStat(&d_statTotLiterals); + d_registry->unregisterStat(&d_statStarts); + d_registry->unregisterStat(&d_statDecisions); + d_registry->unregisterStat(&d_statRndDecisions); + d_registry->unregisterStat(&d_statPropagations); + d_registry->unregisterStat(&d_statConflicts); + d_registry->unregisterStat(&d_statClausesLiterals); + d_registry->unregisterStat(&d_statLearntsLiterals); + d_registry->unregisterStat(&d_statMaxLiterals); + d_registry->unregisterStat(&d_statTotLiterals); } + void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* d_minisat){ d_statStarts.setData(d_minisat->starts); d_statDecisions.setData(d_minisat->decisions); diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index 2564572c2..f279b3a5b 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -20,23 +20,15 @@ #include "prop/sat_solver.h" #include "prop/minisat/simp/SimpSolver.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace prop { class MinisatSatSolver : public DPLLSatSolverInterface { - - /** The SatSolver used */ - Minisat::SimpSolver* d_minisat; - - /** Context we will be using to synchronize the sat solver */ - context::Context* d_context; - - void setupOptions(); - public: - MinisatSatSolver(); + MinisatSatSolver(StatisticsRegistry* registry); ~MinisatSatSolver() throw(); ; @@ -83,15 +75,26 @@ public: bool isDecision(SatVariable decn) const; +private: + + /** The SatSolver used */ + Minisat::SimpSolver* d_minisat; + + /** Context we will be using to synchronize the sat solver */ + context::Context* d_context; + + void setupOptions(); + class Statistics { private: + StatisticsRegistry* d_registry; ReferenceStat<uint64_t> d_statStarts, d_statDecisions; ReferenceStat<uint64_t> d_statRndDecisions, d_statPropagations; ReferenceStat<uint64_t> d_statConflicts, d_statClausesLiterals; ReferenceStat<uint64_t> d_statLearntsLiterals, d_statMaxLiterals; ReferenceStat<uint64_t> d_statTotLiterals; public: - Statistics(); + Statistics(StatisticsRegistry* registry); ~Statistics(); void init(Minisat::SimpSolver* d_minisat); };/* class MinisatSatSolver::Statistics */ diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 96ca7480f..630825103 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -36,6 +36,7 @@ #include "prop/sat_solver.h" #include "prop/sat_solver_factory.h" #include "prop/theory_proxy.h" +#include "smt/smt_statistics_registry.h" #include "smt_util/command.h" #include "theory/theory_engine.h" #include "theory/theory_registrar.h" @@ -83,7 +84,7 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext Debug("prop") << "Constructing the PropEngine" << endl; - d_satSolver = SatSolverFactory::createDPLLMinisat(); + d_satSolver = SatSolverFactory::createDPLLMinisat(smtStatisticsRegistry()); d_registrar = new theory::TheoryRegistrar(d_theoryEngine); d_cnfStream = new CVC4::prop::TseitinCnfStream diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 960881844..1c1dae410 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -24,9 +24,10 @@ #include <string> #include "context/cdlist.h" +#include "context/context.h" #include "expr/node.h" -#include "expr/statistics_registry.h" #include "prop/sat_solver_types.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace prop { @@ -101,7 +102,7 @@ public: virtual void notify(SatClause& clause) = 0; virtual void spendResource(unsigned ammount) = 0; virtual void safePoint(unsigned ammount) = 0; - + };/* class BVSatSolverInterface::Notify */ virtual void setNotify(Notify* notify) = 0; diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp index 98b8fce47..c131ca475 100644 --- a/src/prop/sat_solver_factory.cpp +++ b/src/prop/sat_solver_factory.cpp @@ -15,18 +15,19 @@ **/ #include "prop/sat_solver_factory.h" + #include "prop/minisat/minisat.h" #include "prop/bvminisat/bvminisat.h" namespace CVC4 { namespace prop { -BVSatSolverInterface* SatSolverFactory::createMinisat(context::Context* mainSatContext, const std::string& name) { - return new BVMinisatSatSolver(mainSatContext, name); +BVSatSolverInterface* SatSolverFactory::createMinisat(context::Context* mainSatContext, StatisticsRegistry* registry, const std::string& name) { + return new BVMinisatSatSolver(registry, mainSatContext, name); } -DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat() { - return new MinisatSatSolver(); +DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat(StatisticsRegistry* registry) { + return new MinisatSatSolver(registry); } } /* CVC4::prop namespace */ diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h index e0446eb4a..434bf849d 100644 --- a/src/prop/sat_solver_factory.h +++ b/src/prop/sat_solver_factory.h @@ -21,7 +21,9 @@ #include <string> #include <vector> +#include "context/context.h" #include "prop/sat_solver.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace prop { @@ -29,8 +31,8 @@ namespace prop { class SatSolverFactory { public: - static BVSatSolverInterface* createMinisat(context::Context* mainSatContext, const std::string& name = ""); - static DPLLSatSolverInterface* createDPLLMinisat(); + static BVSatSolverInterface* createMinisat(context::Context* mainSatContext, StatisticsRegistry* registry, const std::string& name = ""); + static DPLLSatSolverInterface* createDPLLMinisat(StatisticsRegistry* registry); };/* class SatSolverFactory */ diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index d0830b9a5..e87046ad5 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -19,14 +19,15 @@ #include "context/context.h" #include "decision/decision_engine.h" #include "expr/expr_stream.h" -#include "expr/statistics_registry.h" #include "options/decision_options.h" #include "prop/cnf_stream.h" #include "prop/prop_engine.h" #include "smt_util/lemma_input_channel.h" #include "smt_util/lemma_output_channel.h" +#include "smt/smt_statistics_registry.h" #include "theory/rewriter.h" #include "theory/theory_engine.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace prop { @@ -42,11 +43,15 @@ TheoryProxy::TheoryProxy(PropEngine* propEngine, d_decisionEngine(decisionEngine), d_theoryEngine(theoryEngine), d_globals(globals), - d_queue(context) -{} + d_queue(context), + d_replayedDecisions("prop::theoryproxy::replayedDecisions", 0) +{ + smtStatisticsRegistry()->registerStat(&d_replayedDecisions); +} TheoryProxy::~TheoryProxy() { /* nothing to do for now */ + smtStatisticsRegistry()->unregisterStat(&d_replayedDecisions); } /** The lemma input channel we are using. */ diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 59bc859cb..261db8c87 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -27,12 +27,12 @@ #include "context/cdqueue.h" #include "expr/node.h" -#include "expr/statistics_registry.h" #include "prop/sat_solver.h" #include "smt/smt_globals.h" #include "smt_util/lemma_output_channel.h" #include "smt_util/lemma_input_channel.h" #include "theory/theory.h" +#include "util/statistics_registry.h" namespace CVC4 { @@ -137,8 +137,8 @@ public: /** * Statistic: the number of replayed decisions (via --replay). */ - KEEP_STATISTIC(IntStat, d_replayedDecisions, - "prop::theoryproxy::replayedDecisions", 0); + IntStat d_replayedDecisions; + };/* class SatSolver */ }/* CVC4::prop namespace */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3571ae0cb..1999930d1 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -244,55 +244,55 @@ struct SmtEngineStatistics { d_resourceUnitsUsed("smt::SmtEngine::resourceUnitsUsed") { - StatisticsRegistry::registerStat(&d_definitionExpansionTime); - StatisticsRegistry::registerStat(&d_rewriteBooleanTermsTime); - StatisticsRegistry::registerStat(&d_nonclausalSimplificationTime); - StatisticsRegistry::registerStat(&d_miplibPassTime); - StatisticsRegistry::registerStat(&d_numMiplibAssertionsRemoved); - StatisticsRegistry::registerStat(&d_numConstantProps); - StatisticsRegistry::registerStat(&d_staticLearningTime); - StatisticsRegistry::registerStat(&d_simpITETime); - StatisticsRegistry::registerStat(&d_unconstrainedSimpTime); - StatisticsRegistry::registerStat(&d_iteRemovalTime); - StatisticsRegistry::registerStat(&d_theoryPreprocessTime); - StatisticsRegistry::registerStat(&d_rewriteApplyToConstTime); - StatisticsRegistry::registerStat(&d_cnfConversionTime); - StatisticsRegistry::registerStat(&d_numAssertionsPre); - StatisticsRegistry::registerStat(&d_numAssertionsPost); - StatisticsRegistry::registerStat(&d_checkModelTime); - StatisticsRegistry::registerStat(&d_checkProofTime); - StatisticsRegistry::registerStat(&d_checkUnsatCoreTime); - StatisticsRegistry::registerStat(&d_solveTime); - StatisticsRegistry::registerStat(&d_pushPopTime); - StatisticsRegistry::registerStat(&d_processAssertionsTime); - StatisticsRegistry::registerStat(&d_simplifiedToFalse); - StatisticsRegistry::registerStat(&d_resourceUnitsUsed); + smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime); + smtStatisticsRegistry()->registerStat(&d_rewriteBooleanTermsTime); + smtStatisticsRegistry()->registerStat(&d_nonclausalSimplificationTime); + smtStatisticsRegistry()->registerStat(&d_miplibPassTime); + smtStatisticsRegistry()->registerStat(&d_numMiplibAssertionsRemoved); + smtStatisticsRegistry()->registerStat(&d_numConstantProps); + smtStatisticsRegistry()->registerStat(&d_staticLearningTime); + smtStatisticsRegistry()->registerStat(&d_simpITETime); + smtStatisticsRegistry()->registerStat(&d_unconstrainedSimpTime); + smtStatisticsRegistry()->registerStat(&d_iteRemovalTime); + smtStatisticsRegistry()->registerStat(&d_theoryPreprocessTime); + smtStatisticsRegistry()->registerStat(&d_rewriteApplyToConstTime); + smtStatisticsRegistry()->registerStat(&d_cnfConversionTime); + smtStatisticsRegistry()->registerStat(&d_numAssertionsPre); + smtStatisticsRegistry()->registerStat(&d_numAssertionsPost); + smtStatisticsRegistry()->registerStat(&d_checkModelTime); + smtStatisticsRegistry()->registerStat(&d_checkProofTime); + smtStatisticsRegistry()->registerStat(&d_checkUnsatCoreTime); + smtStatisticsRegistry()->registerStat(&d_solveTime); + smtStatisticsRegistry()->registerStat(&d_pushPopTime); + smtStatisticsRegistry()->registerStat(&d_processAssertionsTime); + smtStatisticsRegistry()->registerStat(&d_simplifiedToFalse); + smtStatisticsRegistry()->registerStat(&d_resourceUnitsUsed); } ~SmtEngineStatistics() { - StatisticsRegistry::unregisterStat(&d_definitionExpansionTime); - StatisticsRegistry::unregisterStat(&d_rewriteBooleanTermsTime); - StatisticsRegistry::unregisterStat(&d_nonclausalSimplificationTime); - StatisticsRegistry::unregisterStat(&d_miplibPassTime); - StatisticsRegistry::unregisterStat(&d_numMiplibAssertionsRemoved); - StatisticsRegistry::unregisterStat(&d_numConstantProps); - StatisticsRegistry::unregisterStat(&d_staticLearningTime); - StatisticsRegistry::unregisterStat(&d_simpITETime); - StatisticsRegistry::unregisterStat(&d_unconstrainedSimpTime); - StatisticsRegistry::unregisterStat(&d_iteRemovalTime); - StatisticsRegistry::unregisterStat(&d_theoryPreprocessTime); - StatisticsRegistry::unregisterStat(&d_rewriteApplyToConstTime); - StatisticsRegistry::unregisterStat(&d_cnfConversionTime); - StatisticsRegistry::unregisterStat(&d_numAssertionsPre); - StatisticsRegistry::unregisterStat(&d_numAssertionsPost); - StatisticsRegistry::unregisterStat(&d_checkModelTime); - StatisticsRegistry::unregisterStat(&d_checkProofTime); - StatisticsRegistry::unregisterStat(&d_checkUnsatCoreTime); - StatisticsRegistry::unregisterStat(&d_solveTime); - StatisticsRegistry::unregisterStat(&d_pushPopTime); - StatisticsRegistry::unregisterStat(&d_processAssertionsTime); - StatisticsRegistry::unregisterStat(&d_simplifiedToFalse); - StatisticsRegistry::unregisterStat(&d_resourceUnitsUsed); + smtStatisticsRegistry()->unregisterStat(&d_definitionExpansionTime); + smtStatisticsRegistry()->unregisterStat(&d_rewriteBooleanTermsTime); + smtStatisticsRegistry()->unregisterStat(&d_nonclausalSimplificationTime); + smtStatisticsRegistry()->unregisterStat(&d_miplibPassTime); + smtStatisticsRegistry()->unregisterStat(&d_numMiplibAssertionsRemoved); + smtStatisticsRegistry()->unregisterStat(&d_numConstantProps); + smtStatisticsRegistry()->unregisterStat(&d_staticLearningTime); + smtStatisticsRegistry()->unregisterStat(&d_simpITETime); + smtStatisticsRegistry()->unregisterStat(&d_unconstrainedSimpTime); + smtStatisticsRegistry()->unregisterStat(&d_iteRemovalTime); + smtStatisticsRegistry()->unregisterStat(&d_theoryPreprocessTime); + smtStatisticsRegistry()->unregisterStat(&d_rewriteApplyToConstTime); + smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime); + smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPre); + smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPost); + smtStatisticsRegistry()->unregisterStat(&d_checkModelTime); + smtStatisticsRegistry()->unregisterStat(&d_checkProofTime); + smtStatisticsRegistry()->unregisterStat(&d_checkUnsatCoreTime); + smtStatisticsRegistry()->unregisterStat(&d_solveTime); + smtStatisticsRegistry()->unregisterStat(&d_pushPopTime); + smtStatisticsRegistry()->unregisterStat(&d_processAssertionsTime); + smtStatisticsRegistry()->unregisterStat(&d_simplifiedToFalse); + smtStatisticsRegistry()->unregisterStat(&d_resourceUnitsUsed); } };/* struct SmtEngineStatistics */ diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 531b499ac..2f222790c 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -28,7 +28,6 @@ #include "context/cdlist_forward.h" #include "expr/expr.h" #include "expr/expr_manager.h" -#include "expr/statistics.h" #include "options/options.h" #include "proof/unsat_core.h" #include "smt/logic_exception.h" @@ -38,6 +37,7 @@ #include "util/proof.h" #include "util/result.h" #include "util/sexpr.h" +#include "util/statistics.h" #include "util/unsafe_interrupt_exception.h" // In terms of abstraction, this is below (and provides services to) diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp index da01b9863..c4747d724 100644 --- a/src/smt/smt_engine_check_proof.cpp +++ b/src/smt/smt_engine_check_proof.cpp @@ -27,9 +27,9 @@ #include "base/cvc4_assert.h" #include "base/output.h" -#include "expr/statistics_registry.h" #include "smt/smt_engine.h" #include "util/configuration_private.h" +#include "util/statistics_registry.h" using namespace CVC4; using namespace std; diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h index 1dd69abc9..83da5a159 100644 --- a/src/smt/smt_engine_scope.h +++ b/src/smt/smt_engine_scope.h @@ -73,7 +73,18 @@ public: s_smtEngine_current = d_oldSmtEngine; Debug("current") << "smt scope: returning to " << s_smtEngine_current << std::endl; } + + /** + * This returns the StatisticsRegistry attached to the currently in scope + * SmtEngine. + */ + static StatisticsRegistry* currentStatisticsRegistry() { + Assert(smtEngineInScope()); + return s_smtEngine_current->d_statisticsRegistry; + } + };/* class SmtScope */ + }/* CVC4::smt namespace */ }/* CVC4 namespace */ diff --git a/src/smt/smt_statistics_registry.cpp b/src/smt/smt_statistics_registry.cpp new file mode 100644 index 000000000..5aa9085f5 --- /dev/null +++ b/src/smt/smt_statistics_registry.cpp @@ -0,0 +1,29 @@ +/********************* */ +/*! \file smt_statistic_registry.cpp + ** \verbatim + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Accessor for the SmtEngine's StatisticsRegistry. + ** + ** Accessor for the SmtEngine's StatisticsRegistry. + **/ + + +#include "smt/smt_statistics_registry.h" + +#include "smt/smt_engine_scope.h" +#include "util/statistics_registry.h" + +namespace CVC4 { + +StatisticsRegistry* smtStatisticsRegistry() { + return smt::SmtScope::currentStatisticsRegistry(); +} + +}/* CVC4 namespace */ diff --git a/src/smt/smt_statistics_registry.h b/src/smt/smt_statistics_registry.h new file mode 100644 index 000000000..60a5e7c53 --- /dev/null +++ b/src/smt/smt_statistics_registry.h @@ -0,0 +1,61 @@ +/********************* */ +/*! \file smt_statistic_registry.h + ** \verbatim + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Accessor for the SmtEngine's StatisticsRegistry. + ** + ** Accessor for the SmtEngine's StatisticsRegistry. + **/ + +#include "cvc4_private.h" + +#pragma once + +#include "util/statistics_registry.h" + +namespace CVC4 { + +/** + * This returns the StatisticsRegistry attached to the currently in scope + * SmtEngine. This is a synonym for smt::SmtScope::currentStatisticsRegistry(). + */ +StatisticsRegistry* smtStatisticsRegistry(); + + +/** + * To use a statistic, you need to declare it, initialize it in your + * constructor, register it in your constructor, and deregister it in + * your destructor. Instead, this macro does it all for you (and + * therefore also keeps the statistic type, field name, and output + * string all in the same place in your class's header. Its use is + * like in this example, which takes the place of the declaration of a + * statistics field "d_checkTimer": + * + * KEEP_STATISTIC(TimerStat, d_checkTimer, "theory::uf::checkTime"); + * + * If any args need to be passed to the constructor, you can specify + * them after the string. + * + * The macro works by creating a nested class type, derived from the + * statistic type you give it, which declares a registry-aware + * constructor/destructor pair. + */ +#define KEEP_STATISTIC(_StatType, _StatField, _StatName, _CtorArgs...) \ + struct Statistic_##_StatField : public _StatType { \ + Statistic_##_StatField() : _StatType(_StatName, ## _CtorArgs) { \ + smtStatisticsRegistry()->registerStat(this); \ + } \ + ~Statistic_##_StatField() { \ + smtStatisticsRegistry()->unregisterStat(this); \ + } \ + } _StatField + + +}/* CVC4 namespace */ diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp index 71ac18e84..5bbe29bc5 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/approx_simplex.cpp @@ -14,6 +14,7 @@ ** [[ Add lengthier description here ]] ** \todo document this file **/ +#include "theory/arith/approx_simplex.h" #include <cfloat> #include <cmath> @@ -22,7 +23,7 @@ #include "base/output.h" #include "cvc4autoconfig.h" -#include "theory/arith/approx_simplex.h" +#include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" #include "theory/arith/cut_log.h" #include "theory/arith/matrix.h" @@ -169,67 +170,67 @@ ApproximateStatistics::ApproximateStatistics() , d_gaussianElimConstruct("z::approx::gaussianElimConstruct::calls",0) , d_averageGuesses("z::approx::averageGuesses") { - // StatisticsRegistry::registerStat(&d_relaxCalls); - // StatisticsRegistry::registerStat(&d_relaxUnknowns); - // StatisticsRegistry::registerStat(&d_relaxFeasible); - // StatisticsRegistry::registerStat(&d_relaxInfeasible); - // StatisticsRegistry::registerStat(&d_relaxPivotsExhausted); - - // StatisticsRegistry::registerStat(&d_mipCalls); - // StatisticsRegistry::registerStat(&d_mipUnknowns); - // StatisticsRegistry::registerStat(&d_mipBingo); - // StatisticsRegistry::registerStat(&d_mipClosed); - // StatisticsRegistry::registerStat(&d_mipBranchesExhausted); - // StatisticsRegistry::registerStat(&d_mipPivotsExhausted); - // StatisticsRegistry::registerStat(&d_mipExecExhausted); - - - // StatisticsRegistry::registerStat(&d_gmiGen); - // StatisticsRegistry::registerStat(&d_gmiReplay); - // StatisticsRegistry::registerStat(&d_mipGen); - // StatisticsRegistry::registerStat(&d_mipReplay); - - StatisticsRegistry::registerStat(&d_branchMaxDepth); - //StatisticsRegistry::registerStat(&d_branchTotal); - //StatisticsRegistry::registerStat(&d_branchCuts); - StatisticsRegistry::registerStat(&d_branchesMaxOnAVar); - - StatisticsRegistry::registerStat(&d_gaussianElimConstructTime); - StatisticsRegistry::registerStat(&d_gaussianElimConstruct); - - StatisticsRegistry::registerStat(&d_averageGuesses); + // smtStatisticsRegistry()->registerStat(&d_relaxCalls); + // smtStatisticsRegistry()->registerStat(&d_relaxUnknowns); + // smtStatisticsRegistry()->registerStat(&d_relaxFeasible); + // smtStatisticsRegistry()->registerStat(&d_relaxInfeasible); + // smtStatisticsRegistry()->registerStat(&d_relaxPivotsExhausted); + + // smtStatisticsRegistry()->registerStat(&d_mipCalls); + // smtStatisticsRegistry()->registerStat(&d_mipUnknowns); + // smtStatisticsRegistry()->registerStat(&d_mipBingo); + // smtStatisticsRegistry()->registerStat(&d_mipClosed); + // smtStatisticsRegistry()->registerStat(&d_mipBranchesExhausted); + // smtStatisticsRegistry()->registerStat(&d_mipPivotsExhausted); + // smtStatisticsRegistry()->registerStat(&d_mipExecExhausted); + + + // smtStatisticsRegistry()->registerStat(&d_gmiGen); + // smtStatisticsRegistry()->registerStat(&d_gmiReplay); + // smtStatisticsRegistry()->registerStat(&d_mipGen); + // smtStatisticsRegistry()->registerStat(&d_mipReplay); + + smtStatisticsRegistry()->registerStat(&d_branchMaxDepth); + //smtStatisticsRegistry()->registerStat(&d_branchTotal); + //smtStatisticsRegistry()->registerStat(&d_branchCuts); + smtStatisticsRegistry()->registerStat(&d_branchesMaxOnAVar); + + smtStatisticsRegistry()->registerStat(&d_gaussianElimConstructTime); + smtStatisticsRegistry()->registerStat(&d_gaussianElimConstruct); + + smtStatisticsRegistry()->registerStat(&d_averageGuesses); } ApproximateStatistics::~ApproximateStatistics(){ - // StatisticsRegistry::unregisterStat(&d_relaxCalls); - // StatisticsRegistry::unregisterStat(&d_relaxUnknowns); - // StatisticsRegistry::unregisterStat(&d_relaxFeasible); - // StatisticsRegistry::unregisterStat(&d_relaxInfeasible); - // StatisticsRegistry::unregisterStat(&d_relaxPivotsExhausted); - - // StatisticsRegistry::unregisterStat(&d_mipCalls); - // StatisticsRegistry::unregisterStat(&d_mipUnknowns); - // StatisticsRegistry::unregisterStat(&d_mipBingo); - // StatisticsRegistry::unregisterStat(&d_mipClosed); - // StatisticsRegistry::unregisterStat(&d_mipBranchesExhausted); - // StatisticsRegistry::unregisterStat(&d_mipPivotsExhausted); - // StatisticsRegistry::unregisterStat(&d_mipExecExhausted); - - - // StatisticsRegistry::unregisterStat(&d_gmiGen); - // StatisticsRegistry::unregisterStat(&d_gmiReplay); - // StatisticsRegistry::unregisterStat(&d_mipGen); - // StatisticsRegistry::unregisterStat(&d_mipReplay); - - StatisticsRegistry::unregisterStat(&d_branchMaxDepth); - //StatisticsRegistry::unregisterStat(&d_branchTotal); - //StatisticsRegistry::unregisterStat(&d_branchCuts); - StatisticsRegistry::unregisterStat(&d_branchesMaxOnAVar); - - StatisticsRegistry::unregisterStat(&d_gaussianElimConstructTime); - StatisticsRegistry::unregisterStat(&d_gaussianElimConstruct); - - StatisticsRegistry::unregisterStat(&d_averageGuesses); + // smtStatisticsRegistry()->unregisterStat(&d_relaxCalls); + // smtStatisticsRegistry()->unregisterStat(&d_relaxUnknowns); + // smtStatisticsRegistry()->unregisterStat(&d_relaxFeasible); + // smtStatisticsRegistry()->unregisterStat(&d_relaxInfeasible); + // smtStatisticsRegistry()->unregisterStat(&d_relaxPivotsExhausted); + + // smtStatisticsRegistry()->unregisterStat(&d_mipCalls); + // smtStatisticsRegistry()->unregisterStat(&d_mipUnknowns); + // smtStatisticsRegistry()->unregisterStat(&d_mipBingo); + // smtStatisticsRegistry()->unregisterStat(&d_mipClosed); + // smtStatisticsRegistry()->unregisterStat(&d_mipBranchesExhausted); + // smtStatisticsRegistry()->unregisterStat(&d_mipPivotsExhausted); + // smtStatisticsRegistry()->unregisterStat(&d_mipExecExhausted); + + + // smtStatisticsRegistry()->unregisterStat(&d_gmiGen); + // smtStatisticsRegistry()->unregisterStat(&d_gmiReplay); + // smtStatisticsRegistry()->unregisterStat(&d_mipGen); + // smtStatisticsRegistry()->unregisterStat(&d_mipReplay); + + smtStatisticsRegistry()->unregisterStat(&d_branchMaxDepth); + //smtStatisticsRegistry()->unregisterStat(&d_branchTotal); + //smtStatisticsRegistry()->unregisterStat(&d_branchCuts); + smtStatisticsRegistry()->unregisterStat(&d_branchesMaxOnAVar); + + smtStatisticsRegistry()->unregisterStat(&d_gaussianElimConstructTime); + smtStatisticsRegistry()->unregisterStat(&d_gaussianElimConstruct); + + smtStatisticsRegistry()->unregisterStat(&d_averageGuesses); } Integer ApproximateSimplex::s_defaultMaxDenom(1<<26); diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h index 064887787..97e6d6b3e 100644 --- a/src/theory/arith/approx_simplex.h +++ b/src/theory/arith/approx_simplex.h @@ -21,11 +21,11 @@ #pragma once #include <vector> -#include "expr/statistics_registry.h" #include "theory/arith/arithvar.h" #include "theory/arith/delta_rational.h" #include "util/dense_map.h" #include "util/rational.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index 383c6b418..aac792377 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -21,6 +21,7 @@ #include "expr/convenience_node_builders.h" #include "expr/expr.h" #include "options/arith_options.h" +#include "smt/smt_statistics_registry.h" #include "theory/arith/arith_static_learner.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/normal_form.h" @@ -48,13 +49,13 @@ ArithStaticLearner::Statistics::Statistics(): d_iteMinMaxApplications("theory::arith::iteMinMaxApplications", 0), d_iteConstantApplications("theory::arith::iteConstantApplications", 0) { - StatisticsRegistry::registerStat(&d_iteMinMaxApplications); - StatisticsRegistry::registerStat(&d_iteConstantApplications); + smtStatisticsRegistry()->registerStat(&d_iteMinMaxApplications); + smtStatisticsRegistry()->registerStat(&d_iteConstantApplications); } ArithStaticLearner::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_iteMinMaxApplications); - StatisticsRegistry::unregisterStat(&d_iteConstantApplications); + smtStatisticsRegistry()->unregisterStat(&d_iteMinMaxApplications); + smtStatisticsRegistry()->unregisterStat(&d_iteConstantApplications); } void ArithStaticLearner::staticLearning(TNode n, NodeBuilder<>& learned){ diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h index 2b0ee9dad..2aa9c9332 100644 --- a/src/theory/arith/arith_static_learner.h +++ b/src/theory/arith/arith_static_learner.h @@ -24,8 +24,8 @@ #include "context/cdtrail_hashmap.h" #include "context/context.h" -#include "expr/statistics_registry.h" #include "theory/arith/arith_utilities.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp index 737cc9e7b..d7b31e2e2 100644 --- a/src/theory/arith/attempt_solution_simplex.cpp +++ b/src/theory/arith/attempt_solution_simplex.cpp @@ -14,10 +14,11 @@ ** [[ Add lengthier description here ]] ** \todo document this file **/ +#include "theory/arith/attempt_solution_simplex.h" #include "base/output.h" #include "options/arith_options.h" -#include "theory/arith/attempt_solution_simplex.h" +#include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" using namespace std; @@ -36,15 +37,15 @@ AttemptSolutionSDP::Statistics::Statistics(): d_queueTime("theory::arith::attempt::queueTime"), d_conflicts("theory::arith::attempt::conflicts", 0) { - StatisticsRegistry::registerStat(&d_searchTime); - StatisticsRegistry::registerStat(&d_queueTime); - StatisticsRegistry::registerStat(&d_conflicts); + smtStatisticsRegistry()->registerStat(&d_searchTime); + smtStatisticsRegistry()->registerStat(&d_queueTime); + smtStatisticsRegistry()->registerStat(&d_conflicts); } AttemptSolutionSDP::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_searchTime); - StatisticsRegistry::unregisterStat(&d_queueTime); - StatisticsRegistry::unregisterStat(&d_conflicts); + smtStatisticsRegistry()->unregisterStat(&d_searchTime); + smtStatisticsRegistry()->unregisterStat(&d_queueTime); + smtStatisticsRegistry()->unregisterStat(&d_conflicts); } bool AttemptSolutionSDP::matchesNewValue(const DenseMap<DeltaRational>& nv, ArithVar v) const{ diff --git a/src/theory/arith/attempt_solution_simplex.h b/src/theory/arith/attempt_solution_simplex.h index 88d29f6b0..49a2dda29 100644 --- a/src/theory/arith/attempt_solution_simplex.h +++ b/src/theory/arith/attempt_solution_simplex.h @@ -53,9 +53,9 @@ #pragma once -#include "expr/statistics_registry.h" #include "theory/arith/simplex.h" #include "theory/arith/approx_simplex.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { @@ -94,4 +94,3 @@ private: }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ - diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index 964c92eb5..746121b70 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -13,10 +13,11 @@ ** [[ Add lengthier description here ]] ** \todo document this file **/ +#include "theory/arith/congruence_manager.h" #include "base/output.h" +#include "smt/smt_statistics_registry.h" #include "theory/arith/arith_utilities.h" -#include "theory/arith/congruence_manager.h" #include "theory/arith/constraint.h" namespace CVC4 { @@ -45,23 +46,23 @@ ArithCongruenceManager::Statistics::Statistics(): d_propagateConstraints("theory::arith::congruence::propagateConstraints", 0), d_conflicts("theory::arith::congruence::conflicts", 0) { - StatisticsRegistry::registerStat(&d_watchedVariables); - StatisticsRegistry::registerStat(&d_watchedVariableIsZero); - StatisticsRegistry::registerStat(&d_watchedVariableIsNotZero); - StatisticsRegistry::registerStat(&d_equalsConstantCalls); - StatisticsRegistry::registerStat(&d_propagations); - StatisticsRegistry::registerStat(&d_propagateConstraints); - StatisticsRegistry::registerStat(&d_conflicts); + smtStatisticsRegistry()->registerStat(&d_watchedVariables); + smtStatisticsRegistry()->registerStat(&d_watchedVariableIsZero); + smtStatisticsRegistry()->registerStat(&d_watchedVariableIsNotZero); + smtStatisticsRegistry()->registerStat(&d_equalsConstantCalls); + smtStatisticsRegistry()->registerStat(&d_propagations); + smtStatisticsRegistry()->registerStat(&d_propagateConstraints); + smtStatisticsRegistry()->registerStat(&d_conflicts); } ArithCongruenceManager::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_watchedVariables); - StatisticsRegistry::unregisterStat(&d_watchedVariableIsZero); - StatisticsRegistry::unregisterStat(&d_watchedVariableIsNotZero); - StatisticsRegistry::unregisterStat(&d_equalsConstantCalls); - StatisticsRegistry::unregisterStat(&d_propagations); - StatisticsRegistry::unregisterStat(&d_propagateConstraints); - StatisticsRegistry::unregisterStat(&d_conflicts); + smtStatisticsRegistry()->unregisterStat(&d_watchedVariables); + smtStatisticsRegistry()->unregisterStat(&d_watchedVariableIsZero); + smtStatisticsRegistry()->unregisterStat(&d_watchedVariableIsNotZero); + smtStatisticsRegistry()->unregisterStat(&d_equalsConstantCalls); + smtStatisticsRegistry()->unregisterStat(&d_propagations); + smtStatisticsRegistry()->unregisterStat(&d_propagateConstraints); + smtStatisticsRegistry()->unregisterStat(&d_conflicts); } ArithCongruenceManager::ArithCongruenceNotify::ArithCongruenceNotify(ArithCongruenceManager& acm) diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 2fc9c47ed..138805b6e 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -24,12 +24,12 @@ #include "context/cdo.h" #include "context/cdtrail_queue.h" #include "context/context.h" -#include "expr/statistics_registry.h" #include "theory/arith/arithvar.h" #include "theory/arith/constraint_forward.h" #include "theory/arith/partial_model.h" #include "theory/uf/equality_engine.h" #include "util/dense_map.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index f13565a7f..5dc0ba1ac 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -14,14 +14,15 @@ ** [[ Add lengthier description here ]] ** \todo document this file **/ +#include "theory/arith/constraint.h" #include <ostream> #include <algorithm> #include "base/output.h" #include "proof/proof.h" +#include "smt/smt_statistics_registry.h" #include "theory/arith/arith_utilities.h" -#include "theory/arith/constraint.h" #include "theory/arith/normal_form.h" @@ -893,13 +894,14 @@ ConstraintDatabase::Statistics::Statistics(): d_unatePropagateCalls("theory::arith::cd::unatePropagateCalls", 0), d_unatePropagateImplications("theory::arith::cd::unatePropagateImplications", 0) { - StatisticsRegistry::registerStat(&d_unatePropagateCalls); - StatisticsRegistry::registerStat(&d_unatePropagateImplications); + smtStatisticsRegistry()->registerStat(&d_unatePropagateCalls); + smtStatisticsRegistry()->registerStat(&d_unatePropagateImplications); } + ConstraintDatabase::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_unatePropagateCalls); - StatisticsRegistry::unregisterStat(&d_unatePropagateImplications); + smtStatisticsRegistry()->unregisterStat(&d_unatePropagateCalls); + smtStatisticsRegistry()->unregisterStat(&d_unatePropagateImplications); } void ConstraintDatabase::deleteConstraintAndNegation(ConstraintP c){ diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h index f4d392995..054ab01e7 100644 --- a/src/theory/arith/cut_log.h +++ b/src/theory/arith/cut_log.h @@ -26,10 +26,10 @@ #include <vector> #include "expr/kind.h" -#include "expr/statistics_registry.h" #include "theory/arith/arithvar.h" #include "theory/arith/constraint_forward.h" #include "util/dense_map.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index f8b8e0e7b..71ad6de45 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -13,12 +13,13 @@ ** ** A Diophantine equation solver for the theory of arithmetic. **/ +#include "theory/arith/dio_solver.h" #include <iostream> #include "base/output.h" #include "options/arith_options.h" -#include "theory/arith/dio_solver.h" +#include "smt/smt_statistics_registry.h" using namespace std; @@ -56,25 +57,25 @@ DioSolver::Statistics::Statistics() : d_conflictTimer("theory::arith::dio::conflictTimer"), d_cutTimer("theory::arith::dio::cutTimer") { - StatisticsRegistry::registerStat(&d_conflictCalls); - StatisticsRegistry::registerStat(&d_cutCalls); + smtStatisticsRegistry()->registerStat(&d_conflictCalls); + smtStatisticsRegistry()->registerStat(&d_cutCalls); - StatisticsRegistry::registerStat(&d_cuts); - StatisticsRegistry::registerStat(&d_conflicts); + smtStatisticsRegistry()->registerStat(&d_cuts); + smtStatisticsRegistry()->registerStat(&d_conflicts); - StatisticsRegistry::registerStat(&d_conflictTimer); - StatisticsRegistry::registerStat(&d_cutTimer); + smtStatisticsRegistry()->registerStat(&d_conflictTimer); + smtStatisticsRegistry()->registerStat(&d_cutTimer); } DioSolver::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_conflictCalls); - StatisticsRegistry::unregisterStat(&d_cutCalls); + smtStatisticsRegistry()->unregisterStat(&d_conflictCalls); + smtStatisticsRegistry()->unregisterStat(&d_cutCalls); - StatisticsRegistry::unregisterStat(&d_cuts); - StatisticsRegistry::unregisterStat(&d_conflicts); + smtStatisticsRegistry()->unregisterStat(&d_cuts); + smtStatisticsRegistry()->unregisterStat(&d_conflicts); - StatisticsRegistry::unregisterStat(&d_conflictTimer); - StatisticsRegistry::unregisterStat(&d_cutTimer); + smtStatisticsRegistry()->unregisterStat(&d_conflictTimer); + smtStatisticsRegistry()->unregisterStat(&d_cutTimer); } bool DioSolver::queueConditions(TrailIndex t){ diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h index 626160b03..ccaff47c7 100644 --- a/src/theory/arith/dio_solver.h +++ b/src/theory/arith/dio_solver.h @@ -28,10 +28,10 @@ #include "context/cdo.h" #include "context/cdqueue.h" #include "context/context.h" -#include "expr/statistics_registry.h" #include "theory/arith/normal_form.h" #include "theory/arith/partial_model.h" #include "util/rational.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp index 32f81ded8..907d5eefb 100644 --- a/src/theory/arith/dual_simplex.cpp +++ b/src/theory/arith/dual_simplex.cpp @@ -14,11 +14,13 @@ ** [[ Add lengthier description here ]] ** \todo document this file **/ +#include "theory/arith/dual_simplex.h" #include "base/output.h" #include "options/arith_options.h" +#include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" -#include "theory/arith/dual_simplex.h" + using namespace std; @@ -40,21 +42,21 @@ DualSimplexDecisionProcedure::Statistics::Statistics(uint32_t& pivots): d_searchTime("theory::arith::dual::searchTime"), d_finalCheckPivotCounter("theory::arith::dual::lastPivots", pivots) { - StatisticsRegistry::registerStat(&d_statUpdateConflicts); - StatisticsRegistry::registerStat(&d_processSignalsTime); - StatisticsRegistry::registerStat(&d_simplexConflicts); - StatisticsRegistry::registerStat(&d_recentViolationCatches); - StatisticsRegistry::registerStat(&d_searchTime); - StatisticsRegistry::registerStat(&d_finalCheckPivotCounter); + smtStatisticsRegistry()->registerStat(&d_statUpdateConflicts); + smtStatisticsRegistry()->registerStat(&d_processSignalsTime); + smtStatisticsRegistry()->registerStat(&d_simplexConflicts); + smtStatisticsRegistry()->registerStat(&d_recentViolationCatches); + smtStatisticsRegistry()->registerStat(&d_searchTime); + smtStatisticsRegistry()->registerStat(&d_finalCheckPivotCounter); } DualSimplexDecisionProcedure::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_statUpdateConflicts); - StatisticsRegistry::unregisterStat(&d_processSignalsTime); - StatisticsRegistry::unregisterStat(&d_simplexConflicts); - StatisticsRegistry::unregisterStat(&d_recentViolationCatches); - StatisticsRegistry::unregisterStat(&d_searchTime); - StatisticsRegistry::unregisterStat(&d_finalCheckPivotCounter); + smtStatisticsRegistry()->unregisterStat(&d_statUpdateConflicts); + smtStatisticsRegistry()->unregisterStat(&d_processSignalsTime); + smtStatisticsRegistry()->unregisterStat(&d_simplexConflicts); + smtStatisticsRegistry()->unregisterStat(&d_recentViolationCatches); + smtStatisticsRegistry()->unregisterStat(&d_searchTime); + smtStatisticsRegistry()->unregisterStat(&d_finalCheckPivotCounter); } Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){ diff --git a/src/theory/arith/dual_simplex.h b/src/theory/arith/dual_simplex.h index d6bf57bb0..e5ab76da8 100644 --- a/src/theory/arith/dual_simplex.h +++ b/src/theory/arith/dual_simplex.h @@ -52,8 +52,8 @@ #pragma once -#include "expr/statistics_registry.h" #include "theory/arith/simplex.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { @@ -111,4 +111,3 @@ private: }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ - diff --git a/src/theory/arith/error_set.cpp b/src/theory/arith/error_set.cpp index 14da973d8..e918f4c7d 100644 --- a/src/theory/arith/error_set.cpp +++ b/src/theory/arith/error_set.cpp @@ -15,8 +15,9 @@ ** \todo document this file **/ - #include "theory/arith/error_set.h" + +#include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" using namespace std; @@ -134,21 +135,21 @@ ErrorSet::Statistics::Statistics(): d_enqueuesCollectionDuplicates("theory::arith::pqueue::enqueuesCollectionDuplicates", 0), d_enqueuesVarOrderModeDuplicates("theory::arith::pqueue::enqueuesVarOrderModeDuplicates", 0) { - StatisticsRegistry::registerStat(&d_enqueues); - StatisticsRegistry::registerStat(&d_enqueuesCollection); - StatisticsRegistry::registerStat(&d_enqueuesDiffMode); - StatisticsRegistry::registerStat(&d_enqueuesVarOrderMode); - StatisticsRegistry::registerStat(&d_enqueuesCollectionDuplicates); - StatisticsRegistry::registerStat(&d_enqueuesVarOrderModeDuplicates); + smtStatisticsRegistry()->registerStat(&d_enqueues); + smtStatisticsRegistry()->registerStat(&d_enqueuesCollection); + smtStatisticsRegistry()->registerStat(&d_enqueuesDiffMode); + smtStatisticsRegistry()->registerStat(&d_enqueuesVarOrderMode); + smtStatisticsRegistry()->registerStat(&d_enqueuesCollectionDuplicates); + smtStatisticsRegistry()->registerStat(&d_enqueuesVarOrderModeDuplicates); } ErrorSet::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_enqueues); - StatisticsRegistry::unregisterStat(&d_enqueuesCollection); - StatisticsRegistry::unregisterStat(&d_enqueuesDiffMode); - StatisticsRegistry::unregisterStat(&d_enqueuesVarOrderMode); - StatisticsRegistry::unregisterStat(&d_enqueuesCollectionDuplicates); - StatisticsRegistry::unregisterStat(&d_enqueuesVarOrderModeDuplicates); + smtStatisticsRegistry()->unregisterStat(&d_enqueues); + smtStatisticsRegistry()->unregisterStat(&d_enqueuesCollection); + smtStatisticsRegistry()->unregisterStat(&d_enqueuesDiffMode); + smtStatisticsRegistry()->unregisterStat(&d_enqueuesVarOrderMode); + smtStatisticsRegistry()->unregisterStat(&d_enqueuesCollectionDuplicates); + smtStatisticsRegistry()->unregisterStat(&d_enqueuesVarOrderModeDuplicates); } ErrorSet::ErrorSet(ArithVariables& vars, TableauSizes tabSizes, BoundCountingLookup lookups): diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h index f12e38c12..fb3117a98 100644 --- a/src/theory/arith/error_set.h +++ b/src/theory/arith/error_set.h @@ -22,7 +22,6 @@ #include <vector> -#include "expr/statistics_registry.h" #include "options/arith_heuristic_pivot_rule.h" #include "theory/arith/arithvar.h" #include "theory/arith/bound_counts.h" @@ -31,6 +30,7 @@ #include "theory/arith/partial_model.h" #include "theory/arith/tableau_sizes.h" #include "util/bin_heap.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp index 229dc379c..888e29732 100644 --- a/src/theory/arith/fc_simplex.cpp +++ b/src/theory/arith/fc_simplex.cpp @@ -17,9 +17,10 @@ #include "theory/arith/fc_simplex.h" #include "base/output.h" -#include "expr/statistics_registry.h" #include "options/arith_options.h" +#include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" +#include "util/statistics_registry.h" using namespace std; @@ -52,37 +53,37 @@ FCSimplexDecisionProcedure::Statistics::Statistics(uint32_t& pivots): d_selectUpdateForPrimal("theory::arith::FC::selectUpdateForPrimal"), d_finalCheckPivotCounter("theory::arith::FC::lastPivots", pivots) { - StatisticsRegistry::registerStat(&d_initialSignalsTime); - StatisticsRegistry::registerStat(&d_initialConflicts); + smtStatisticsRegistry()->registerStat(&d_initialSignalsTime); + smtStatisticsRegistry()->registerStat(&d_initialConflicts); - StatisticsRegistry::registerStat(&d_fcFoundUnsat); - StatisticsRegistry::registerStat(&d_fcFoundSat); - StatisticsRegistry::registerStat(&d_fcMissed); + smtStatisticsRegistry()->registerStat(&d_fcFoundUnsat); + smtStatisticsRegistry()->registerStat(&d_fcFoundSat); + smtStatisticsRegistry()->registerStat(&d_fcMissed); - StatisticsRegistry::registerStat(&d_fcTimer); - StatisticsRegistry::registerStat(&d_fcFocusConstructionTimer); + smtStatisticsRegistry()->registerStat(&d_fcTimer); + smtStatisticsRegistry()->registerStat(&d_fcFocusConstructionTimer); - StatisticsRegistry::registerStat(&d_selectUpdateForDualLike); - StatisticsRegistry::registerStat(&d_selectUpdateForPrimal); + smtStatisticsRegistry()->registerStat(&d_selectUpdateForDualLike); + smtStatisticsRegistry()->registerStat(&d_selectUpdateForPrimal); - StatisticsRegistry::registerStat(&d_finalCheckPivotCounter); + smtStatisticsRegistry()->registerStat(&d_finalCheckPivotCounter); } FCSimplexDecisionProcedure::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_initialSignalsTime); - StatisticsRegistry::unregisterStat(&d_initialConflicts); + smtStatisticsRegistry()->unregisterStat(&d_initialSignalsTime); + smtStatisticsRegistry()->unregisterStat(&d_initialConflicts); - StatisticsRegistry::unregisterStat(&d_fcFoundUnsat); - StatisticsRegistry::unregisterStat(&d_fcFoundSat); - StatisticsRegistry::unregisterStat(&d_fcMissed); + smtStatisticsRegistry()->unregisterStat(&d_fcFoundUnsat); + smtStatisticsRegistry()->unregisterStat(&d_fcFoundSat); + smtStatisticsRegistry()->unregisterStat(&d_fcMissed); - StatisticsRegistry::unregisterStat(&d_fcTimer); - StatisticsRegistry::unregisterStat(&d_fcFocusConstructionTimer); + smtStatisticsRegistry()->unregisterStat(&d_fcTimer); + smtStatisticsRegistry()->unregisterStat(&d_fcFocusConstructionTimer); - StatisticsRegistry::unregisterStat(&d_selectUpdateForDualLike); - StatisticsRegistry::unregisterStat(&d_selectUpdateForPrimal); + smtStatisticsRegistry()->unregisterStat(&d_selectUpdateForDualLike); + smtStatisticsRegistry()->unregisterStat(&d_selectUpdateForPrimal); - StatisticsRegistry::unregisterStat(&d_finalCheckPivotCounter); + smtStatisticsRegistry()->unregisterStat(&d_finalCheckPivotCounter); } Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){ diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h index 471804003..c416af1c6 100644 --- a/src/theory/arith/fc_simplex.h +++ b/src/theory/arith/fc_simplex.h @@ -54,9 +54,9 @@ #include <stdint.h> -#include "expr/statistics_registry.h" #include "theory/arith/simplex.h" #include "util/dense_map.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { @@ -255,4 +255,3 @@ private: }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ - diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp index d8888bd75..6d86a1ab1 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear_equality.cpp @@ -13,11 +13,12 @@ ** ** This implements the LinearEqualityModule. **/ - +#include "theory/arith/linear_equality.h" #include "base/output.h" +#include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" -#include "theory/arith/linear_equality.h" + using namespace std; @@ -76,31 +77,31 @@ LinearEqualityModule::Statistics::Statistics(): d_weakenTime("theory::arith::weakening::time"), d_forceTime("theory::arith::forcing::time") { - StatisticsRegistry::registerStat(&d_statPivots); - StatisticsRegistry::registerStat(&d_statUpdates); + smtStatisticsRegistry()->registerStat(&d_statPivots); + smtStatisticsRegistry()->registerStat(&d_statUpdates); - StatisticsRegistry::registerStat(&d_pivotTime); - StatisticsRegistry::registerStat(&d_adjTime); + smtStatisticsRegistry()->registerStat(&d_pivotTime); + smtStatisticsRegistry()->registerStat(&d_adjTime); - StatisticsRegistry::registerStat(&d_weakeningAttempts); - StatisticsRegistry::registerStat(&d_weakeningSuccesses); - StatisticsRegistry::registerStat(&d_weakenings); - StatisticsRegistry::registerStat(&d_weakenTime); - StatisticsRegistry::registerStat(&d_forceTime); + smtStatisticsRegistry()->registerStat(&d_weakeningAttempts); + smtStatisticsRegistry()->registerStat(&d_weakeningSuccesses); + smtStatisticsRegistry()->registerStat(&d_weakenings); + smtStatisticsRegistry()->registerStat(&d_weakenTime); + smtStatisticsRegistry()->registerStat(&d_forceTime); } LinearEqualityModule::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_statPivots); - StatisticsRegistry::unregisterStat(&d_statUpdates); - StatisticsRegistry::unregisterStat(&d_pivotTime); - StatisticsRegistry::unregisterStat(&d_adjTime); + smtStatisticsRegistry()->unregisterStat(&d_statPivots); + smtStatisticsRegistry()->unregisterStat(&d_statUpdates); + smtStatisticsRegistry()->unregisterStat(&d_pivotTime); + smtStatisticsRegistry()->unregisterStat(&d_adjTime); - StatisticsRegistry::unregisterStat(&d_weakeningAttempts); - StatisticsRegistry::unregisterStat(&d_weakeningSuccesses); - StatisticsRegistry::unregisterStat(&d_weakenings); - StatisticsRegistry::unregisterStat(&d_weakenTime); - StatisticsRegistry::unregisterStat(&d_forceTime); + smtStatisticsRegistry()->unregisterStat(&d_weakeningAttempts); + smtStatisticsRegistry()->unregisterStat(&d_weakeningSuccesses); + smtStatisticsRegistry()->unregisterStat(&d_weakenings); + smtStatisticsRegistry()->unregisterStat(&d_weakenTime); + smtStatisticsRegistry()->unregisterStat(&d_forceTime); } void LinearEqualityModule::includeBoundUpdate(ArithVar v, const BoundsInfo& prev){ diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h index d7c9c038c..f3cf17d81 100644 --- a/src/theory/arith/linear_equality.h +++ b/src/theory/arith/linear_equality.h @@ -29,7 +29,6 @@ #pragma once -#include "expr/statistics_registry.h" #include "options/arith_options.h" #include "theory/arith/arithvar.h" #include "theory/arith/constraint_forward.h" @@ -38,6 +37,7 @@ #include "theory/arith/simplex_update.h" #include "theory/arith/tableau.h" #include "util/maybe.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp index 765e6a00d..df32ec8a4 100644 --- a/src/theory/arith/soi_simplex.cpp +++ b/src/theory/arith/soi_simplex.cpp @@ -19,10 +19,10 @@ #include <algorithm> #include "base/output.h" -#include "expr/statistics_registry.h" #include "options/arith_options.h" +#include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" - +#include "util/statistics_registry.h" using namespace std; @@ -56,46 +56,46 @@ SumOfInfeasibilitiesSPD::Statistics::Statistics(uint32_t& pivots): d_selectUpdateForSOI("theory::arith::SOI::selectSOI"), d_finalCheckPivotCounter("theory::arith::SOI::lastPivots", pivots) { - StatisticsRegistry::registerStat(&d_initialSignalsTime); - StatisticsRegistry::registerStat(&d_initialConflicts); + smtStatisticsRegistry()->registerStat(&d_initialSignalsTime); + smtStatisticsRegistry()->registerStat(&d_initialConflicts); - StatisticsRegistry::registerStat(&d_soiFoundUnsat); - StatisticsRegistry::registerStat(&d_soiFoundSat); - StatisticsRegistry::registerStat(&d_soiMissed); + smtStatisticsRegistry()->registerStat(&d_soiFoundUnsat); + smtStatisticsRegistry()->registerStat(&d_soiFoundSat); + smtStatisticsRegistry()->registerStat(&d_soiMissed); - StatisticsRegistry::registerStat(&d_soiConflicts); - StatisticsRegistry::registerStat(&d_hasToBeMinimal); - StatisticsRegistry::registerStat(&d_maybeNotMinimal); + smtStatisticsRegistry()->registerStat(&d_soiConflicts); + smtStatisticsRegistry()->registerStat(&d_hasToBeMinimal); + smtStatisticsRegistry()->registerStat(&d_maybeNotMinimal); - StatisticsRegistry::registerStat(&d_soiTimer); - StatisticsRegistry::registerStat(&d_soiFocusConstructionTimer); + smtStatisticsRegistry()->registerStat(&d_soiTimer); + smtStatisticsRegistry()->registerStat(&d_soiFocusConstructionTimer); - StatisticsRegistry::registerStat(&d_soiConflictMinimization); + smtStatisticsRegistry()->registerStat(&d_soiConflictMinimization); - StatisticsRegistry::registerStat(&d_selectUpdateForSOI); + smtStatisticsRegistry()->registerStat(&d_selectUpdateForSOI); - StatisticsRegistry::registerStat(&d_finalCheckPivotCounter); + smtStatisticsRegistry()->registerStat(&d_finalCheckPivotCounter); } SumOfInfeasibilitiesSPD::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_initialSignalsTime); - StatisticsRegistry::unregisterStat(&d_initialConflicts); + smtStatisticsRegistry()->unregisterStat(&d_initialSignalsTime); + smtStatisticsRegistry()->unregisterStat(&d_initialConflicts); - StatisticsRegistry::unregisterStat(&d_soiFoundUnsat); - StatisticsRegistry::unregisterStat(&d_soiFoundSat); - StatisticsRegistry::unregisterStat(&d_soiMissed); + smtStatisticsRegistry()->unregisterStat(&d_soiFoundUnsat); + smtStatisticsRegistry()->unregisterStat(&d_soiFoundSat); + smtStatisticsRegistry()->unregisterStat(&d_soiMissed); - StatisticsRegistry::unregisterStat(&d_soiConflicts); - StatisticsRegistry::unregisterStat(&d_hasToBeMinimal); - StatisticsRegistry::unregisterStat(&d_maybeNotMinimal); + smtStatisticsRegistry()->unregisterStat(&d_soiConflicts); + smtStatisticsRegistry()->unregisterStat(&d_hasToBeMinimal); + smtStatisticsRegistry()->unregisterStat(&d_maybeNotMinimal); - StatisticsRegistry::unregisterStat(&d_soiTimer); - StatisticsRegistry::unregisterStat(&d_soiFocusConstructionTimer); + smtStatisticsRegistry()->unregisterStat(&d_soiTimer); + smtStatisticsRegistry()->unregisterStat(&d_soiFocusConstructionTimer); - StatisticsRegistry::unregisterStat(&d_soiConflictMinimization); + smtStatisticsRegistry()->unregisterStat(&d_soiConflictMinimization); - StatisticsRegistry::unregisterStat(&d_selectUpdateForSOI); - StatisticsRegistry::unregisterStat(&d_finalCheckPivotCounter); + smtStatisticsRegistry()->unregisterStat(&d_selectUpdateForSOI); + smtStatisticsRegistry()->unregisterStat(&d_finalCheckPivotCounter); } Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){ diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h index b08d7794b..73a2330a3 100644 --- a/src/theory/arith/soi_simplex.h +++ b/src/theory/arith/soi_simplex.h @@ -54,9 +54,9 @@ #include <stdint.h> -#include "expr/statistics_registry.h" #include "theory/arith/simplex.h" #include "util/dense_map.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { @@ -241,4 +241,3 @@ private: }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ - diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 3c5c1c414..843feed01 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -18,6 +18,7 @@ #include "theory/arith/theory_arith.h" #include "options/smt_options.h" +#include "smt/smt_statistics_registry.h" #include "theory/arith/infer_bounds.h" #include "theory/arith/theory_arith_private.h" @@ -33,9 +34,13 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, const LogicInfo& logicInfo, SmtGlobals* globals) : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, globals) , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo)) -{} + , d_ppRewriteTimer("theory::arith::ppRewriteTimer") +{ + smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer); +} TheoryArith::~TheoryArith(){ + smtStatisticsRegistry()->unregisterStat(&d_ppRewriteTimer); delete d_internal; } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index d26a120ae..c54414109 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -43,7 +43,7 @@ private: TheoryArithPrivate* d_internal; - KEEP_STATISTIC(TimerStat, d_ppRewriteTimer, "theory::arith::ppRewriteTimer"); + TimerStat d_ppRewriteTimer; public: TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index bf1810331..e6b14d2b1 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -33,11 +33,11 @@ #include "expr/metakind.h" #include "expr/node.h" #include "expr/node_builder.h" -#include "expr/statistics_registry.h" #include "options/arith_options.h" #include "options/smt_options.h" // for incrementalSolving() #include "smt/logic_exception.h" #include "smt/logic_request.h" +#include "smt/smt_statistics_registry.h" #include "smt_util/boolean_simplification.h" #include "theory/arith/approx_simplex.h" #include "theory/arith/arith_ite_utils.h" @@ -70,6 +70,7 @@ #include "util/integer.h" #include "util/rational.h" #include "util/result.h" +#include "util/statistics_registry.h" using namespace std; using namespace CVC4::kind; @@ -328,190 +329,190 @@ TheoryArithPrivate::Statistics::Statistics() , d_mipProofsSuccessful("theory::arith::z::mip::proofs::successful", 0) , d_numBranchesFailed("theory::arith::z::mip::branch::proof::failed", 0) { - StatisticsRegistry::registerStat(&d_statAssertUpperConflicts); - StatisticsRegistry::registerStat(&d_statAssertLowerConflicts); - - StatisticsRegistry::registerStat(&d_statUserVariables); - StatisticsRegistry::registerStat(&d_statAuxiliaryVariables); - StatisticsRegistry::registerStat(&d_statDisequalitySplits); - StatisticsRegistry::registerStat(&d_statDisequalityConflicts); - StatisticsRegistry::registerStat(&d_simplifyTimer); - StatisticsRegistry::registerStat(&d_staticLearningTimer); - - StatisticsRegistry::registerStat(&d_presolveTime); - StatisticsRegistry::registerStat(&d_newPropTime); - - StatisticsRegistry::registerStat(&d_externalBranchAndBounds); - - StatisticsRegistry::registerStat(&d_initialTableauSize); - StatisticsRegistry::registerStat(&d_currSetToSmaller); - StatisticsRegistry::registerStat(&d_smallerSetToCurr); - StatisticsRegistry::registerStat(&d_restartTimer); - - StatisticsRegistry::registerStat(&d_boundComputationTime); - StatisticsRegistry::registerStat(&d_boundComputations); - StatisticsRegistry::registerStat(&d_boundPropagations); - - StatisticsRegistry::registerStat(&d_unknownChecks); - StatisticsRegistry::registerStat(&d_maxUnknownsInARow); - StatisticsRegistry::registerStat(&d_avgUnknownsInARow); - StatisticsRegistry::registerStat(&d_revertsOnConflicts); - StatisticsRegistry::registerStat(&d_commitsOnConflicts); - StatisticsRegistry::registerStat(&d_nontrivialSatChecks); - - - StatisticsRegistry::registerStat(&d_satPivots); - StatisticsRegistry::registerStat(&d_unsatPivots); - StatisticsRegistry::registerStat(&d_unknownPivots); - - StatisticsRegistry::registerStat(&d_replayLogRecCount); - StatisticsRegistry::registerStat(&d_replayLogRecConflictEscalation); - StatisticsRegistry::registerStat(&d_replayLogRecEarlyExit); - StatisticsRegistry::registerStat(&d_replayBranchCloseFailures); - StatisticsRegistry::registerStat(&d_replayLeafCloseFailures); - StatisticsRegistry::registerStat(&d_replayBranchSkips); - StatisticsRegistry::registerStat(&d_mirCutsAttempted); - StatisticsRegistry::registerStat(&d_gmiCutsAttempted); - StatisticsRegistry::registerStat(&d_branchCutsAttempted); - StatisticsRegistry::registerStat(&d_cutsReconstructed); - StatisticsRegistry::registerStat(&d_cutsProven); - StatisticsRegistry::registerStat(&d_cutsProofFailed); - StatisticsRegistry::registerStat(&d_cutsReconstructionFailed); - StatisticsRegistry::registerStat(&d_mipReplayLemmaCalls); - StatisticsRegistry::registerStat(&d_mipExternalCuts); - StatisticsRegistry::registerStat(&d_mipExternalBranch); - - StatisticsRegistry::registerStat(&d_inSolveInteger); - StatisticsRegistry::registerStat(&d_branchesExhausted); - StatisticsRegistry::registerStat(&d_execExhausted); - StatisticsRegistry::registerStat(&d_pivotsExhausted); - StatisticsRegistry::registerStat(&d_panicBranches); - StatisticsRegistry::registerStat(&d_relaxCalls); - StatisticsRegistry::registerStat(&d_relaxLinFeas); - StatisticsRegistry::registerStat(&d_relaxLinFeasFailures); - StatisticsRegistry::registerStat(&d_relaxLinInfeas); - StatisticsRegistry::registerStat(&d_relaxLinInfeasFailures); - StatisticsRegistry::registerStat(&d_relaxLinExhausted); - StatisticsRegistry::registerStat(&d_relaxOthers); - - StatisticsRegistry::registerStat(&d_applyRowsDeleted); - - StatisticsRegistry::registerStat(&d_replaySimplexTimer); - StatisticsRegistry::registerStat(&d_replayLogTimer); - StatisticsRegistry::registerStat(&d_solveIntTimer); - StatisticsRegistry::registerStat(&d_solveRealRelaxTimer); - - StatisticsRegistry::registerStat(&d_solveIntCalls); - StatisticsRegistry::registerStat(&d_solveStandardEffort); - - StatisticsRegistry::registerStat(&d_approxDisabled); - - StatisticsRegistry::registerStat(&d_replayAttemptFailed); - - StatisticsRegistry::registerStat(&d_cutsRejectedDuringReplay); - StatisticsRegistry::registerStat(&d_cutsRejectedDuringLemmas); - - StatisticsRegistry::registerStat(&d_solveIntModelsAttempts); - StatisticsRegistry::registerStat(&d_solveIntModelsSuccessful); - StatisticsRegistry::registerStat(&d_mipTimer); - StatisticsRegistry::registerStat(&d_lpTimer); - StatisticsRegistry::registerStat(&d_mipProofsAttempted); - StatisticsRegistry::registerStat(&d_mipProofsSuccessful); - StatisticsRegistry::registerStat(&d_numBranchesFailed); + smtStatisticsRegistry()->registerStat(&d_statAssertUpperConflicts); + smtStatisticsRegistry()->registerStat(&d_statAssertLowerConflicts); + + smtStatisticsRegistry()->registerStat(&d_statUserVariables); + smtStatisticsRegistry()->registerStat(&d_statAuxiliaryVariables); + smtStatisticsRegistry()->registerStat(&d_statDisequalitySplits); + smtStatisticsRegistry()->registerStat(&d_statDisequalityConflicts); + smtStatisticsRegistry()->registerStat(&d_simplifyTimer); + smtStatisticsRegistry()->registerStat(&d_staticLearningTimer); + + smtStatisticsRegistry()->registerStat(&d_presolveTime); + smtStatisticsRegistry()->registerStat(&d_newPropTime); + + smtStatisticsRegistry()->registerStat(&d_externalBranchAndBounds); + + smtStatisticsRegistry()->registerStat(&d_initialTableauSize); + smtStatisticsRegistry()->registerStat(&d_currSetToSmaller); + smtStatisticsRegistry()->registerStat(&d_smallerSetToCurr); + smtStatisticsRegistry()->registerStat(&d_restartTimer); + + smtStatisticsRegistry()->registerStat(&d_boundComputationTime); + smtStatisticsRegistry()->registerStat(&d_boundComputations); + smtStatisticsRegistry()->registerStat(&d_boundPropagations); + + smtStatisticsRegistry()->registerStat(&d_unknownChecks); + smtStatisticsRegistry()->registerStat(&d_maxUnknownsInARow); + smtStatisticsRegistry()->registerStat(&d_avgUnknownsInARow); + smtStatisticsRegistry()->registerStat(&d_revertsOnConflicts); + smtStatisticsRegistry()->registerStat(&d_commitsOnConflicts); + smtStatisticsRegistry()->registerStat(&d_nontrivialSatChecks); + + + smtStatisticsRegistry()->registerStat(&d_satPivots); + smtStatisticsRegistry()->registerStat(&d_unsatPivots); + smtStatisticsRegistry()->registerStat(&d_unknownPivots); + + smtStatisticsRegistry()->registerStat(&d_replayLogRecCount); + smtStatisticsRegistry()->registerStat(&d_replayLogRecConflictEscalation); + smtStatisticsRegistry()->registerStat(&d_replayLogRecEarlyExit); + smtStatisticsRegistry()->registerStat(&d_replayBranchCloseFailures); + smtStatisticsRegistry()->registerStat(&d_replayLeafCloseFailures); + smtStatisticsRegistry()->registerStat(&d_replayBranchSkips); + smtStatisticsRegistry()->registerStat(&d_mirCutsAttempted); + smtStatisticsRegistry()->registerStat(&d_gmiCutsAttempted); + smtStatisticsRegistry()->registerStat(&d_branchCutsAttempted); + smtStatisticsRegistry()->registerStat(&d_cutsReconstructed); + smtStatisticsRegistry()->registerStat(&d_cutsProven); + smtStatisticsRegistry()->registerStat(&d_cutsProofFailed); + smtStatisticsRegistry()->registerStat(&d_cutsReconstructionFailed); + smtStatisticsRegistry()->registerStat(&d_mipReplayLemmaCalls); + smtStatisticsRegistry()->registerStat(&d_mipExternalCuts); + smtStatisticsRegistry()->registerStat(&d_mipExternalBranch); + + smtStatisticsRegistry()->registerStat(&d_inSolveInteger); + smtStatisticsRegistry()->registerStat(&d_branchesExhausted); + smtStatisticsRegistry()->registerStat(&d_execExhausted); + smtStatisticsRegistry()->registerStat(&d_pivotsExhausted); + smtStatisticsRegistry()->registerStat(&d_panicBranches); + smtStatisticsRegistry()->registerStat(&d_relaxCalls); + smtStatisticsRegistry()->registerStat(&d_relaxLinFeas); + smtStatisticsRegistry()->registerStat(&d_relaxLinFeasFailures); + smtStatisticsRegistry()->registerStat(&d_relaxLinInfeas); + smtStatisticsRegistry()->registerStat(&d_relaxLinInfeasFailures); + smtStatisticsRegistry()->registerStat(&d_relaxLinExhausted); + smtStatisticsRegistry()->registerStat(&d_relaxOthers); + + smtStatisticsRegistry()->registerStat(&d_applyRowsDeleted); + + smtStatisticsRegistry()->registerStat(&d_replaySimplexTimer); + smtStatisticsRegistry()->registerStat(&d_replayLogTimer); + smtStatisticsRegistry()->registerStat(&d_solveIntTimer); + smtStatisticsRegistry()->registerStat(&d_solveRealRelaxTimer); + + smtStatisticsRegistry()->registerStat(&d_solveIntCalls); + smtStatisticsRegistry()->registerStat(&d_solveStandardEffort); + + smtStatisticsRegistry()->registerStat(&d_approxDisabled); + + smtStatisticsRegistry()->registerStat(&d_replayAttemptFailed); + + smtStatisticsRegistry()->registerStat(&d_cutsRejectedDuringReplay); + smtStatisticsRegistry()->registerStat(&d_cutsRejectedDuringLemmas); + + smtStatisticsRegistry()->registerStat(&d_solveIntModelsAttempts); + smtStatisticsRegistry()->registerStat(&d_solveIntModelsSuccessful); + smtStatisticsRegistry()->registerStat(&d_mipTimer); + smtStatisticsRegistry()->registerStat(&d_lpTimer); + smtStatisticsRegistry()->registerStat(&d_mipProofsAttempted); + smtStatisticsRegistry()->registerStat(&d_mipProofsSuccessful); + smtStatisticsRegistry()->registerStat(&d_numBranchesFailed); } TheoryArithPrivate::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_statAssertUpperConflicts); - StatisticsRegistry::unregisterStat(&d_statAssertLowerConflicts); - - StatisticsRegistry::unregisterStat(&d_statUserVariables); - StatisticsRegistry::unregisterStat(&d_statAuxiliaryVariables); - StatisticsRegistry::unregisterStat(&d_statDisequalitySplits); - StatisticsRegistry::unregisterStat(&d_statDisequalityConflicts); - StatisticsRegistry::unregisterStat(&d_simplifyTimer); - StatisticsRegistry::unregisterStat(&d_staticLearningTimer); - - StatisticsRegistry::unregisterStat(&d_presolveTime); - StatisticsRegistry::unregisterStat(&d_newPropTime); - - StatisticsRegistry::unregisterStat(&d_externalBranchAndBounds); - - StatisticsRegistry::unregisterStat(&d_initialTableauSize); - StatisticsRegistry::unregisterStat(&d_currSetToSmaller); - StatisticsRegistry::unregisterStat(&d_smallerSetToCurr); - StatisticsRegistry::unregisterStat(&d_restartTimer); - - StatisticsRegistry::unregisterStat(&d_boundComputationTime); - StatisticsRegistry::unregisterStat(&d_boundComputations); - StatisticsRegistry::unregisterStat(&d_boundPropagations); - - StatisticsRegistry::unregisterStat(&d_unknownChecks); - StatisticsRegistry::unregisterStat(&d_maxUnknownsInARow); - StatisticsRegistry::unregisterStat(&d_avgUnknownsInARow); - StatisticsRegistry::unregisterStat(&d_revertsOnConflicts); - StatisticsRegistry::unregisterStat(&d_commitsOnConflicts); - StatisticsRegistry::unregisterStat(&d_nontrivialSatChecks); - - StatisticsRegistry::unregisterStat(&d_satPivots); - StatisticsRegistry::unregisterStat(&d_unsatPivots); - StatisticsRegistry::unregisterStat(&d_unknownPivots); - - StatisticsRegistry::unregisterStat(&d_replayLogRecCount); - StatisticsRegistry::unregisterStat(&d_replayLogRecConflictEscalation); - StatisticsRegistry::unregisterStat(&d_replayLogRecEarlyExit); - StatisticsRegistry::unregisterStat(&d_replayBranchCloseFailures); - StatisticsRegistry::unregisterStat(&d_replayLeafCloseFailures); - StatisticsRegistry::unregisterStat(&d_replayBranchSkips); - StatisticsRegistry::unregisterStat(&d_mirCutsAttempted); - StatisticsRegistry::unregisterStat(&d_gmiCutsAttempted); - StatisticsRegistry::unregisterStat(&d_branchCutsAttempted); - StatisticsRegistry::unregisterStat(&d_cutsReconstructed); - StatisticsRegistry::unregisterStat(&d_cutsProven); - StatisticsRegistry::unregisterStat(&d_cutsProofFailed); - StatisticsRegistry::unregisterStat(&d_cutsReconstructionFailed); - StatisticsRegistry::unregisterStat(&d_mipReplayLemmaCalls); - StatisticsRegistry::unregisterStat(&d_mipExternalCuts); - StatisticsRegistry::unregisterStat(&d_mipExternalBranch); - - - StatisticsRegistry::unregisterStat(&d_inSolveInteger); - StatisticsRegistry::unregisterStat(&d_branchesExhausted); - StatisticsRegistry::unregisterStat(&d_execExhausted); - StatisticsRegistry::unregisterStat(&d_pivotsExhausted); - StatisticsRegistry::unregisterStat(&d_panicBranches); - StatisticsRegistry::unregisterStat(&d_relaxCalls); - StatisticsRegistry::unregisterStat(&d_relaxLinFeas); - StatisticsRegistry::unregisterStat(&d_relaxLinFeasFailures); - StatisticsRegistry::unregisterStat(&d_relaxLinInfeas); - StatisticsRegistry::unregisterStat(&d_relaxLinInfeasFailures); - StatisticsRegistry::unregisterStat(&d_relaxLinExhausted); - StatisticsRegistry::unregisterStat(&d_relaxOthers); - - StatisticsRegistry::unregisterStat(&d_applyRowsDeleted); - - StatisticsRegistry::unregisterStat(&d_replaySimplexTimer); - StatisticsRegistry::unregisterStat(&d_replayLogTimer); - StatisticsRegistry::unregisterStat(&d_solveIntTimer); - StatisticsRegistry::unregisterStat(&d_solveRealRelaxTimer); - - StatisticsRegistry::unregisterStat(&d_solveIntCalls); - StatisticsRegistry::unregisterStat(&d_solveStandardEffort); - - StatisticsRegistry::unregisterStat(&d_approxDisabled); - - StatisticsRegistry::unregisterStat(&d_replayAttemptFailed); - - StatisticsRegistry::unregisterStat(&d_cutsRejectedDuringReplay); - StatisticsRegistry::unregisterStat(&d_cutsRejectedDuringLemmas); - - - StatisticsRegistry::unregisterStat(&d_solveIntModelsAttempts); - StatisticsRegistry::unregisterStat(&d_solveIntModelsSuccessful); - StatisticsRegistry::unregisterStat(&d_mipTimer); - StatisticsRegistry::unregisterStat(&d_lpTimer); - StatisticsRegistry::unregisterStat(&d_mipProofsAttempted); - StatisticsRegistry::unregisterStat(&d_mipProofsSuccessful); - StatisticsRegistry::unregisterStat(&d_numBranchesFailed); + smtStatisticsRegistry()->unregisterStat(&d_statAssertUpperConflicts); + smtStatisticsRegistry()->unregisterStat(&d_statAssertLowerConflicts); + + smtStatisticsRegistry()->unregisterStat(&d_statUserVariables); + smtStatisticsRegistry()->unregisterStat(&d_statAuxiliaryVariables); + smtStatisticsRegistry()->unregisterStat(&d_statDisequalitySplits); + smtStatisticsRegistry()->unregisterStat(&d_statDisequalityConflicts); + smtStatisticsRegistry()->unregisterStat(&d_simplifyTimer); + smtStatisticsRegistry()->unregisterStat(&d_staticLearningTimer); + + smtStatisticsRegistry()->unregisterStat(&d_presolveTime); + smtStatisticsRegistry()->unregisterStat(&d_newPropTime); + + smtStatisticsRegistry()->unregisterStat(&d_externalBranchAndBounds); + + smtStatisticsRegistry()->unregisterStat(&d_initialTableauSize); + smtStatisticsRegistry()->unregisterStat(&d_currSetToSmaller); + smtStatisticsRegistry()->unregisterStat(&d_smallerSetToCurr); + smtStatisticsRegistry()->unregisterStat(&d_restartTimer); + + smtStatisticsRegistry()->unregisterStat(&d_boundComputationTime); + smtStatisticsRegistry()->unregisterStat(&d_boundComputations); + smtStatisticsRegistry()->unregisterStat(&d_boundPropagations); + + smtStatisticsRegistry()->unregisterStat(&d_unknownChecks); + smtStatisticsRegistry()->unregisterStat(&d_maxUnknownsInARow); + smtStatisticsRegistry()->unregisterStat(&d_avgUnknownsInARow); + smtStatisticsRegistry()->unregisterStat(&d_revertsOnConflicts); + smtStatisticsRegistry()->unregisterStat(&d_commitsOnConflicts); + smtStatisticsRegistry()->unregisterStat(&d_nontrivialSatChecks); + + smtStatisticsRegistry()->unregisterStat(&d_satPivots); + smtStatisticsRegistry()->unregisterStat(&d_unsatPivots); + smtStatisticsRegistry()->unregisterStat(&d_unknownPivots); + + smtStatisticsRegistry()->unregisterStat(&d_replayLogRecCount); + smtStatisticsRegistry()->unregisterStat(&d_replayLogRecConflictEscalation); + smtStatisticsRegistry()->unregisterStat(&d_replayLogRecEarlyExit); + smtStatisticsRegistry()->unregisterStat(&d_replayBranchCloseFailures); + smtStatisticsRegistry()->unregisterStat(&d_replayLeafCloseFailures); + smtStatisticsRegistry()->unregisterStat(&d_replayBranchSkips); + smtStatisticsRegistry()->unregisterStat(&d_mirCutsAttempted); + smtStatisticsRegistry()->unregisterStat(&d_gmiCutsAttempted); + smtStatisticsRegistry()->unregisterStat(&d_branchCutsAttempted); + smtStatisticsRegistry()->unregisterStat(&d_cutsReconstructed); + smtStatisticsRegistry()->unregisterStat(&d_cutsProven); + smtStatisticsRegistry()->unregisterStat(&d_cutsProofFailed); + smtStatisticsRegistry()->unregisterStat(&d_cutsReconstructionFailed); + smtStatisticsRegistry()->unregisterStat(&d_mipReplayLemmaCalls); + smtStatisticsRegistry()->unregisterStat(&d_mipExternalCuts); + smtStatisticsRegistry()->unregisterStat(&d_mipExternalBranch); + + + smtStatisticsRegistry()->unregisterStat(&d_inSolveInteger); + smtStatisticsRegistry()->unregisterStat(&d_branchesExhausted); + smtStatisticsRegistry()->unregisterStat(&d_execExhausted); + smtStatisticsRegistry()->unregisterStat(&d_pivotsExhausted); + smtStatisticsRegistry()->unregisterStat(&d_panicBranches); + smtStatisticsRegistry()->unregisterStat(&d_relaxCalls); + smtStatisticsRegistry()->unregisterStat(&d_relaxLinFeas); + smtStatisticsRegistry()->unregisterStat(&d_relaxLinFeasFailures); + smtStatisticsRegistry()->unregisterStat(&d_relaxLinInfeas); + smtStatisticsRegistry()->unregisterStat(&d_relaxLinInfeasFailures); + smtStatisticsRegistry()->unregisterStat(&d_relaxLinExhausted); + smtStatisticsRegistry()->unregisterStat(&d_relaxOthers); + + smtStatisticsRegistry()->unregisterStat(&d_applyRowsDeleted); + + smtStatisticsRegistry()->unregisterStat(&d_replaySimplexTimer); + smtStatisticsRegistry()->unregisterStat(&d_replayLogTimer); + smtStatisticsRegistry()->unregisterStat(&d_solveIntTimer); + smtStatisticsRegistry()->unregisterStat(&d_solveRealRelaxTimer); + + smtStatisticsRegistry()->unregisterStat(&d_solveIntCalls); + smtStatisticsRegistry()->unregisterStat(&d_solveStandardEffort); + + smtStatisticsRegistry()->unregisterStat(&d_approxDisabled); + + smtStatisticsRegistry()->unregisterStat(&d_replayAttemptFailed); + + smtStatisticsRegistry()->unregisterStat(&d_cutsRejectedDuringReplay); + smtStatisticsRegistry()->unregisterStat(&d_cutsRejectedDuringLemmas); + + + smtStatisticsRegistry()->unregisterStat(&d_solveIntModelsAttempts); + smtStatisticsRegistry()->unregisterStat(&d_solveIntModelsSuccessful); + smtStatisticsRegistry()->unregisterStat(&d_mipTimer); + smtStatisticsRegistry()->unregisterStat(&d_lpTimer); + smtStatisticsRegistry()->unregisterStat(&d_mipProofsAttempted); + smtStatisticsRegistry()->unregisterStat(&d_mipProofsSuccessful); + smtStatisticsRegistry()->unregisterStat(&d_numBranchesFailed); } bool complexityBelow(const DenseMap<Rational>& row, uint32_t cap){ diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 32c12eba7..1009dceb8 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -31,7 +31,6 @@ #include "expr/metakind.h" #include "expr/node.h" #include "expr/node_builder.h" -#include "expr/statistics_registry.h" #include "options/arith_options.h" #include "smt/logic_exception.h" #include "smt_util/boolean_simplification.h" @@ -67,6 +66,7 @@ #include "util/integer.h" #include "util/rational.h" #include "util/result.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp index cd0025fe2..e94abe9cb 100644 --- a/src/theory/arrays/array_info.cpp +++ b/src/theory/arrays/array_info.cpp @@ -17,10 +17,53 @@ #include "theory/arrays/array_info.h" +#include "smt/smt_statistics_registry.h" + namespace CVC4 { namespace theory { namespace arrays { +ArrayInfo::ArrayInfo(context::Context* c, Backtracker<TNode>* b) + : ct(c), bck(b), info_map(), + d_mergeInfoTimer("theory::arrays::mergeInfoTimer"), + d_avgIndexListLength("theory::arrays::avgIndexListLength"), + d_avgStoresListLength("theory::arrays::avgStoresListLength"), + d_avgInStoresListLength("theory::arrays::avgInStoresListLength"), + d_listsCount("theory::arrays::listsCount",0), + d_callsMergeInfo("theory::arrays::callsMergeInfo",0), + d_maxList("theory::arrays::maxList",0), + d_tableSize("theory::arrays::infoTableSize", info_map) { + emptyList = new(true) CTNodeList(ct); + emptyInfo = new Info(ct, bck); + smtStatisticsRegistry()->registerStat(&d_mergeInfoTimer); + smtStatisticsRegistry()->registerStat(&d_avgIndexListLength); + smtStatisticsRegistry()->registerStat(&d_avgStoresListLength); + smtStatisticsRegistry()->registerStat(&d_avgInStoresListLength); + smtStatisticsRegistry()->registerStat(&d_listsCount); + smtStatisticsRegistry()->registerStat(&d_callsMergeInfo); + smtStatisticsRegistry()->registerStat(&d_maxList); + smtStatisticsRegistry()->registerStat(&d_tableSize); +} + +ArrayInfo::~ArrayInfo() { + CNodeInfoMap::iterator it = info_map.begin(); + for( ; it != info_map.end(); it++ ) { + if((*it).second!= emptyInfo) { + delete (*it).second; + } + } + emptyList->deleteSelf(); + delete emptyInfo; + smtStatisticsRegistry()->unregisterStat(&d_mergeInfoTimer); + smtStatisticsRegistry()->unregisterStat(&d_avgIndexListLength); + smtStatisticsRegistry()->unregisterStat(&d_avgStoresListLength); + smtStatisticsRegistry()->unregisterStat(&d_avgInStoresListLength); + smtStatisticsRegistry()->unregisterStat(&d_listsCount); + smtStatisticsRegistry()->unregisterStat(&d_callsMergeInfo); + smtStatisticsRegistry()->unregisterStat(&d_maxList); + smtStatisticsRegistry()->unregisterStat(&d_tableSize); +} + bool inList(const CTNodeList* l, const TNode el) { CTNodeList::const_iterator it = l->begin(); for ( ; it!= l->end(); it ++) { diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index f14788ed5..3e479e0f9 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -27,8 +27,8 @@ #include "context/cdlist.h" #include "context/cdhashmap.h" #include "expr/node.h" -#include "expr/statistics_registry.h" #include "util/ntuple.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { @@ -163,54 +163,18 @@ public: d_callsMergeInfo("theory::arrays::callsMergeInfo",0), d_maxList("theory::arrays::maxList",0), d_tableSize("theory::arrays::infoTableSize", info_map) { - StatisticsRegistry::registerStat(&d_mergeInfoTimer); - StatisticsRegistry::registerStat(&d_avgIndexListLength); - StatisticsRegistry::registerStat(&d_avgStoresListLength); - StatisticsRegistry::registerStat(&d_avgInStoresListLength); - StatisticsRegistry::registerStat(&d_listsCount); - StatisticsRegistry::registerStat(&d_callsMergeInfo); - StatisticsRegistry::registerStat(&d_maxList); - StatisticsRegistry::registerStat(&d_tableSize); + currentStatisticsRegistry()->registerStat(&d_mergeInfoTimer); + currentStatisticsRegistry()->registerStat(&d_avgIndexListLength); + currentStatisticsRegistry()->registerStat(&d_avgStoresListLength); + currentStatisticsRegistry()->registerStat(&d_avgInStoresListLength); + currentStatisticsRegistry()->registerStat(&d_listsCount); + currentStatisticsRegistry()->registerStat(&d_callsMergeInfo); + currentStatisticsRegistry()->registerStat(&d_maxList); + currentStatisticsRegistry()->registerStat(&d_tableSize); }*/ - ArrayInfo(context::Context* c, Backtracker<TNode>* b): ct(c), bck(b), info_map(), - d_mergeInfoTimer("theory::arrays::mergeInfoTimer"), - d_avgIndexListLength("theory::arrays::avgIndexListLength"), - d_avgStoresListLength("theory::arrays::avgStoresListLength"), - d_avgInStoresListLength("theory::arrays::avgInStoresListLength"), - d_listsCount("theory::arrays::listsCount",0), - d_callsMergeInfo("theory::arrays::callsMergeInfo",0), - d_maxList("theory::arrays::maxList",0), - d_tableSize("theory::arrays::infoTableSize", info_map) { - emptyList = new(true) CTNodeList(ct); - emptyInfo = new Info(ct, bck); - StatisticsRegistry::registerStat(&d_mergeInfoTimer); - StatisticsRegistry::registerStat(&d_avgIndexListLength); - StatisticsRegistry::registerStat(&d_avgStoresListLength); - StatisticsRegistry::registerStat(&d_avgInStoresListLength); - StatisticsRegistry::registerStat(&d_listsCount); - StatisticsRegistry::registerStat(&d_callsMergeInfo); - StatisticsRegistry::registerStat(&d_maxList); - StatisticsRegistry::registerStat(&d_tableSize); - } + ArrayInfo(context::Context* c, Backtracker<TNode>* b); - ~ArrayInfo() { - CNodeInfoMap::iterator it = info_map.begin(); - for( ; it != info_map.end(); it++ ) { - if((*it).second!= emptyInfo) { - delete (*it).second; - } - } - emptyList->deleteSelf(); - delete emptyInfo; - StatisticsRegistry::unregisterStat(&d_mergeInfoTimer); - StatisticsRegistry::unregisterStat(&d_avgIndexListLength); - StatisticsRegistry::unregisterStat(&d_avgStoresListLength); - StatisticsRegistry::unregisterStat(&d_avgInStoresListLength); - StatisticsRegistry::unregisterStat(&d_listsCount); - StatisticsRegistry::unregisterStat(&d_callsMergeInfo); - StatisticsRegistry::unregisterStat(&d_maxList); - StatisticsRegistry::unregisterStat(&d_tableSize); - }; + ~ArrayInfo(); /** * adds the node a to the map if it does not exist diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index ab57eb260..508a4b323 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -22,6 +22,7 @@ #include "options/arrays_options.h" #include "options/smt_options.h" #include "smt/logic_exception.h" +#include "smt/smt_statistics_registry.h" #include "smt_util/command.h" #include "theory/rewriter.h" #include "theory/theory_model.h" @@ -98,16 +99,16 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, d_arrayMerges(c), d_inCheckModel(false) { - StatisticsRegistry::registerStat(&d_numRow); - StatisticsRegistry::registerStat(&d_numExt); - StatisticsRegistry::registerStat(&d_numProp); - StatisticsRegistry::registerStat(&d_numExplain); - StatisticsRegistry::registerStat(&d_numNonLinear); - StatisticsRegistry::registerStat(&d_numSharedArrayVarSplits); - StatisticsRegistry::registerStat(&d_numGetModelValSplits); - StatisticsRegistry::registerStat(&d_numGetModelValConflicts); - StatisticsRegistry::registerStat(&d_numSetModelValSplits); - StatisticsRegistry::registerStat(&d_numSetModelValConflicts); + smtStatisticsRegistry()->registerStat(&d_numRow); + smtStatisticsRegistry()->registerStat(&d_numExt); + smtStatisticsRegistry()->registerStat(&d_numProp); + smtStatisticsRegistry()->registerStat(&d_numExplain); + smtStatisticsRegistry()->registerStat(&d_numNonLinear); + smtStatisticsRegistry()->registerStat(&d_numSharedArrayVarSplits); + smtStatisticsRegistry()->registerStat(&d_numGetModelValSplits); + smtStatisticsRegistry()->registerStat(&d_numGetModelValConflicts); + smtStatisticsRegistry()->registerStat(&d_numSetModelValSplits); + smtStatisticsRegistry()->registerStat(&d_numSetModelValConflicts); d_true = NodeManager::currentNM()->mkConst<bool>(true); d_false = NodeManager::currentNM()->mkConst<bool>(false); @@ -137,16 +138,16 @@ TheoryArrays::~TheoryArrays() { it2->second->deleteSelf(); } delete d_constReadsContext; - StatisticsRegistry::unregisterStat(&d_numRow); - StatisticsRegistry::unregisterStat(&d_numExt); - StatisticsRegistry::unregisterStat(&d_numProp); - StatisticsRegistry::unregisterStat(&d_numExplain); - StatisticsRegistry::unregisterStat(&d_numNonLinear); - StatisticsRegistry::unregisterStat(&d_numSharedArrayVarSplits); - StatisticsRegistry::unregisterStat(&d_numGetModelValSplits); - StatisticsRegistry::unregisterStat(&d_numGetModelValConflicts); - StatisticsRegistry::unregisterStat(&d_numSetModelValSplits); - StatisticsRegistry::unregisterStat(&d_numSetModelValConflicts); + smtStatisticsRegistry()->unregisterStat(&d_numRow); + smtStatisticsRegistry()->unregisterStat(&d_numExt); + smtStatisticsRegistry()->unregisterStat(&d_numProp); + smtStatisticsRegistry()->unregisterStat(&d_numExplain); + smtStatisticsRegistry()->unregisterStat(&d_numNonLinear); + smtStatisticsRegistry()->unregisterStat(&d_numSharedArrayVarSplits); + smtStatisticsRegistry()->unregisterStat(&d_numGetModelValSplits); + smtStatisticsRegistry()->unregisterStat(&d_numGetModelValConflicts); + smtStatisticsRegistry()->unregisterStat(&d_numSetModelValSplits); + smtStatisticsRegistry()->unregisterStat(&d_numSetModelValConflicts); } void TheoryArrays::setMasterEqualityEngine(eq::EqualityEngine* eq) { diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 98cba0420..f1b02d99e 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -22,10 +22,10 @@ #include "context/cdhashmap.h" #include "context/cdhashset.h" #include "context/cdqueue.h" -#include "expr/statistics_registry.h" #include "theory/arrays/array_info.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp index f05520306..842ff60b1 100644 --- a/src/theory/bv/abstraction.cpp +++ b/src/theory/bv/abstraction.cpp @@ -16,6 +16,7 @@ #include "options/bv_options.h" #include "smt_util/dump.h" +#include "smt/smt_statistics_registry.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" @@ -1047,13 +1048,13 @@ AbstractionModule::Statistics::Statistics() , d_numArgsSkolemized("theory::bv::AbstractioModule::NumArgsSkolemized", 0) , d_abstractionTime("theory::bv::AbstractioModule::AbstractionTime") { - StatisticsRegistry::registerStat(&d_numFunctionsAbstracted); - StatisticsRegistry::registerStat(&d_numArgsSkolemized); - StatisticsRegistry::registerStat(&d_abstractionTime); + smtStatisticsRegistry()->registerStat(&d_numFunctionsAbstracted); + smtStatisticsRegistry()->registerStat(&d_numArgsSkolemized); + smtStatisticsRegistry()->registerStat(&d_abstractionTime); } AbstractionModule::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_numFunctionsAbstracted); - StatisticsRegistry::unregisterStat(&d_numArgsSkolemized); - StatisticsRegistry::unregisterStat(&d_abstractionTime); + smtStatisticsRegistry()->unregisterStat(&d_numFunctionsAbstracted); + smtStatisticsRegistry()->unregisterStat(&d_numArgsSkolemized); + smtStatisticsRegistry()->unregisterStat(&d_abstractionTime); } diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h index 6b4d5a7dc..cba170d76 100644 --- a/src/theory/bv/abstraction.h +++ b/src/theory/bv/abstraction.h @@ -23,8 +23,8 @@ #include <ext/hash_set> #include "expr/node.h" -#include "expr/statistics_registry.h" #include "theory/substitutions.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp index f07bd49f7..d84493daf 100644 --- a/src/theory/bv/aig_bitblaster.cpp +++ b/src/theory/bv/aig_bitblaster.cpp @@ -455,19 +455,19 @@ AigBitblaster::Statistics::Statistics() , d_cnfConversionTime("theory::bv::AigBitblaster::cnfConversionTime") , d_solveTime("theory::bv::AigBitblaster::solveTime") { - StatisticsRegistry::registerStat(&d_numClauses); - StatisticsRegistry::registerStat(&d_numVariables); - StatisticsRegistry::registerStat(&d_simplificationTime); - StatisticsRegistry::registerStat(&d_cnfConversionTime); - StatisticsRegistry::registerStat(&d_solveTime); + smtStatisticsRegistry()->registerStat(&d_numClauses); + smtStatisticsRegistry()->registerStat(&d_numVariables); + smtStatisticsRegistry()->registerStat(&d_simplificationTime); + smtStatisticsRegistry()->registerStat(&d_cnfConversionTime); + smtStatisticsRegistry()->registerStat(&d_solveTime); } AigBitblaster::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_numClauses); - StatisticsRegistry::unregisterStat(&d_numVariables); - StatisticsRegistry::unregisterStat(&d_simplificationTime); - StatisticsRegistry::unregisterStat(&d_cnfConversionTime); - StatisticsRegistry::unregisterStat(&d_solveTime); + smtStatisticsRegistry()->unregisterStat(&d_numClauses); + smtStatisticsRegistry()->unregisterStat(&d_numVariables); + smtStatisticsRegistry()->unregisterStat(&d_simplificationTime); + smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime); + smtStatisticsRegistry()->unregisterStat(&d_solveTime); } #else // CVC4_USE_ABC diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp index 6231b8e46..40ac3d560 100644 --- a/src/theory/bv/bv_quick_check.cpp +++ b/src/theory/bv/bv_quick_check.cpp @@ -15,9 +15,10 @@ **/ #include "theory/bv/bv_quick_check.h" -#include "theory/bv/theory_bv_utils.h" +#include "smt/smt_statistics_registry.h" #include "theory/bv/bitblaster_template.h" +#include "theory/bv/theory_bv_utils.h" using namespace CVC4; using namespace CVC4::theory; @@ -357,22 +358,21 @@ QuickXPlain::Statistics::Statistics(const std::string& name) , d_finalPeriod("theory::bv::"+name+"::QuickXplain::FinalPeriod", 0) , d_avgMinimizationRatio("theory::bv::"+name+"::QuickXplain::AvgMinRatio") { - StatisticsRegistry::registerStat(&d_xplainTime); - StatisticsRegistry::registerStat(&d_numSolved); - StatisticsRegistry::registerStat(&d_numUnknown); - StatisticsRegistry::registerStat(&d_numUnknownWasUnsat); - StatisticsRegistry::registerStat(&d_numConflictsMinimized); - StatisticsRegistry::registerStat(&d_finalPeriod); - StatisticsRegistry::registerStat(&d_avgMinimizationRatio); + smtStatisticsRegistry()->registerStat(&d_xplainTime); + smtStatisticsRegistry()->registerStat(&d_numSolved); + smtStatisticsRegistry()->registerStat(&d_numUnknown); + smtStatisticsRegistry()->registerStat(&d_numUnknownWasUnsat); + smtStatisticsRegistry()->registerStat(&d_numConflictsMinimized); + smtStatisticsRegistry()->registerStat(&d_finalPeriod); + smtStatisticsRegistry()->registerStat(&d_avgMinimizationRatio); } QuickXPlain::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_xplainTime); - StatisticsRegistry::unregisterStat(&d_numSolved); - StatisticsRegistry::unregisterStat(&d_numUnknown); - StatisticsRegistry::unregisterStat(&d_numUnknownWasUnsat); - StatisticsRegistry::unregisterStat(&d_numConflictsMinimized); - StatisticsRegistry::unregisterStat(&d_finalPeriod); - StatisticsRegistry::unregisterStat(&d_avgMinimizationRatio); + smtStatisticsRegistry()->unregisterStat(&d_xplainTime); + smtStatisticsRegistry()->unregisterStat(&d_numSolved); + smtStatisticsRegistry()->unregisterStat(&d_numUnknown); + smtStatisticsRegistry()->unregisterStat(&d_numUnknownWasUnsat); + smtStatisticsRegistry()->unregisterStat(&d_numConflictsMinimized); + smtStatisticsRegistry()->unregisterStat(&d_finalPeriod); + smtStatisticsRegistry()->unregisterStat(&d_avgMinimizationRatio); } - diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h index 8ef49f786..8d2a62287 100644 --- a/src/theory/bv/bv_quick_check.h +++ b/src/theory/bv/bv_quick_check.h @@ -24,9 +24,9 @@ #include "context/cdo.h" #include "expr/node.h" -#include "expr/statistics_registry.h" #include "prop/sat_solver_types.h" #include "theory/bv/theory_bv_utils.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index 4531be040..fc9d67cb4 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -13,11 +13,12 @@ ** ** Algebraic solver. **/ +#include "theory/bv/bv_subtheory_algebraic.h" #include "options/bv_options.h" #include "smt_util/boolean_simplification.h" +#include "smt/smt_statistics_registry.h" #include "theory/bv/bv_quick_check.h" -#include "theory/bv/bv_subtheory_algebraic.h" #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory_model.h" @@ -734,25 +735,25 @@ AlgebraicSolver::Statistics::Statistics() , d_solveTime("theory::bv::AlgebraicSolver::SolveTime") , d_useHeuristic("theory::bv::AlgebraicSolver::UseHeuristic", 0.2) { - StatisticsRegistry::registerStat(&d_numCallstoCheck); - StatisticsRegistry::registerStat(&d_numSimplifiesToTrue); - StatisticsRegistry::registerStat(&d_numSimplifiesToFalse); - StatisticsRegistry::registerStat(&d_numUnsat); - StatisticsRegistry::registerStat(&d_numSat); - StatisticsRegistry::registerStat(&d_numUnknown); - StatisticsRegistry::registerStat(&d_solveTime); - StatisticsRegistry::registerStat(&d_useHeuristic); + smtStatisticsRegistry()->registerStat(&d_numCallstoCheck); + smtStatisticsRegistry()->registerStat(&d_numSimplifiesToTrue); + smtStatisticsRegistry()->registerStat(&d_numSimplifiesToFalse); + smtStatisticsRegistry()->registerStat(&d_numUnsat); + smtStatisticsRegistry()->registerStat(&d_numSat); + smtStatisticsRegistry()->registerStat(&d_numUnknown); + smtStatisticsRegistry()->registerStat(&d_solveTime); + smtStatisticsRegistry()->registerStat(&d_useHeuristic); } AlgebraicSolver::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_numCallstoCheck); - StatisticsRegistry::unregisterStat(&d_numSimplifiesToTrue); - StatisticsRegistry::unregisterStat(&d_numSimplifiesToFalse); - StatisticsRegistry::unregisterStat(&d_numUnsat); - StatisticsRegistry::unregisterStat(&d_numSat); - StatisticsRegistry::unregisterStat(&d_numUnknown); - StatisticsRegistry::unregisterStat(&d_solveTime); - StatisticsRegistry::unregisterStat(&d_useHeuristic); + smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck); + smtStatisticsRegistry()->unregisterStat(&d_numSimplifiesToTrue); + smtStatisticsRegistry()->unregisterStat(&d_numSimplifiesToFalse); + smtStatisticsRegistry()->unregisterStat(&d_numUnsat); + smtStatisticsRegistry()->unregisterStat(&d_numSat); + smtStatisticsRegistry()->unregisterStat(&d_numUnknown); + smtStatisticsRegistry()->unregisterStat(&d_solveTime); + smtStatisticsRegistry()->unregisterStat(&d_useHeuristic); } bool hasExpensiveBVOperatorsRec(TNode fact, TNodeSet& seen) { diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index 1d0342c08..9f8cb580c 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -17,6 +17,7 @@ #include "decision/decision_attributes.h" #include "options/decision_options.h" #include "options/bv_options.h" +#include "smt/smt_statistics_registry.h" #include "theory/bv/abstraction.h" #include "theory/bv/bitblaster_template.h" #include "theory/bv/bv_quick_check.h" @@ -55,12 +56,12 @@ BitblastSolver::Statistics::Statistics() : d_numCallstoCheck("theory::bv::BitblastSolver::NumCallsToCheck", 0) , d_numBBLemmas("theory::bv::BitblastSolver::NumTimesLemmasBB", 0) { - StatisticsRegistry::registerStat(&d_numCallstoCheck); - StatisticsRegistry::registerStat(&d_numBBLemmas); + smtStatisticsRegistry()->registerStat(&d_numCallstoCheck); + smtStatisticsRegistry()->registerStat(&d_numBBLemmas); } BitblastSolver::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_numCallstoCheck); - StatisticsRegistry::unregisterStat(&d_numBBLemmas); + smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck); + smtStatisticsRegistry()->unregisterStat(&d_numBBLemmas); } void BitblastSolver::setAbstraction(AbstractionModule* abs) { diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index ef4d24e82..ec257468e 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -18,6 +18,7 @@ #include "options/bv_options.h" #include "options/smt_options.h" +#include "smt/smt_statistics_registry.h" #include "theory/bv/slicer.h" #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" @@ -438,10 +439,10 @@ CoreSolver::Statistics::Statistics() : d_numCallstoCheck("theory::bv::CoreSolver::NumCallsToCheck", 0) , d_slicerEnabled("theory::bv::CoreSolver::SlicerEnabled", false) { - StatisticsRegistry::registerStat(&d_numCallstoCheck); - StatisticsRegistry::registerStat(&d_slicerEnabled); + smtStatisticsRegistry()->registerStat(&d_numCallstoCheck); + smtStatisticsRegistry()->registerStat(&d_slicerEnabled); } CoreSolver::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_numCallstoCheck); - StatisticsRegistry::unregisterStat(&d_slicerEnabled); + smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck); + smtStatisticsRegistry()->unregisterStat(&d_slicerEnabled); } diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index 054e43b7c..7916d941e 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -17,6 +17,7 @@ #include "theory/bv/bv_subtheory_inequality.h" #include "options/smt_options.h" +#include "smt/smt_statistics_registry.h" #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory_model.h" @@ -228,8 +229,8 @@ bool InequalitySolver::addInequality(TNode a, TNode b, bool strict, TNode fact) InequalitySolver::Statistics::Statistics() : d_numCallstoCheck("theory::bv::InequalitySolver::NumCallsToCheck", 0) { - StatisticsRegistry::registerStat(&d_numCallstoCheck); + smtStatisticsRegistry()->registerStat(&d_numCallstoCheck); } InequalitySolver::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_numCallstoCheck); + smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck); } diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp index 00e6f9ff8..66ad4fec0 100644 --- a/src/theory/bv/bv_to_bool.cpp +++ b/src/theory/bv/bv_to_bool.cpp @@ -11,11 +11,12 @@ ** ** \brief Preprocessing pass that lifts bit-vectors of size 1 to booleans. ** - ** Preprocessing pass that lifts bit-vectors of size 1 to booleans. + ** Preprocessing pass that lifts bit-vectors of size 1 to booleans. **/ #include "theory/bv/bv_to_bool.h" #include "smt_util/node_visitor.h" +#include "smt/smt_statistics_registry.h" using namespace std; using namespace CVC4; @@ -31,7 +32,7 @@ BvToBoolPreprocessor::BvToBoolPreprocessor() {} void BvToBoolPreprocessor::addToLiftCache(TNode term, Node new_term) { - Assert (new_term != Node()); + Assert (new_term != Node()); Assert (!hasLiftCache(term)); Assert (term.getType() == new_term.getType()); d_liftCache[term] = new_term; @@ -239,13 +240,13 @@ BvToBoolPreprocessor::Statistics::Statistics() , d_numAtomsLifted("theory::bv::BvToBoolPreprocess::NumberOfAtomsLifted", 0) , d_numTermsForcedLifted("theory::bv::BvToBoolPreprocess::NumberOfTermsForcedLifted", 0) { - StatisticsRegistry::registerStat(&d_numTermsLifted); - StatisticsRegistry::registerStat(&d_numAtomsLifted); - StatisticsRegistry::registerStat(&d_numTermsForcedLifted); + smtStatisticsRegistry()->registerStat(&d_numTermsLifted); + smtStatisticsRegistry()->registerStat(&d_numAtomsLifted); + smtStatisticsRegistry()->registerStat(&d_numTermsForcedLifted); } BvToBoolPreprocessor::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_numTermsLifted); - StatisticsRegistry::unregisterStat(&d_numAtomsLifted); - StatisticsRegistry::unregisterStat(&d_numTermsForcedLifted); + smtStatisticsRegistry()->unregisterStat(&d_numTermsLifted); + smtStatisticsRegistry()->unregisterStat(&d_numAtomsLifted); + smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLifted); } diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h index 46b2d5c6e..e6c126440 100644 --- a/src/theory/bv/bv_to_bool.h +++ b/src/theory/bv/bv_to_bool.h @@ -11,7 +11,7 @@ ** ** \brief Preprocessing pass that lifts bit-vectors of size 1 to booleans. ** - ** Preprocessing pass that lifts bit-vectors of size 1 to booleans. + ** Preprocessing pass that lifts bit-vectors of size 1 to booleans. **/ #include "cvc4_private.h" @@ -19,14 +19,14 @@ #ifndef __CVC4__THEORY__BV__BV_TO_BOOL_H #define __CVC4__THEORY__BV__BV_TO_BOOL_H -#include "expr/statistics_registry.h" #include "theory/bv/theory_bv_utils.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { namespace bv { -typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap; +typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap; class BvToBoolPreprocessor { diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp index 39606ca7c..000abe62b 100644 --- a/src/theory/bv/eager_bitblaster.cpp +++ b/src/theory/bv/eager_bitblaster.cpp @@ -19,6 +19,7 @@ #include "options/bv_options.h" #include "prop/cnf_stream.h" #include "prop/sat_solver_factory.h" +#include "smt/smt_statistics_registry.h" #include "theory/bv/bitblaster_template.h" #include "theory/bv/theory_bv.h" #include "theory/theory_model.h" @@ -45,7 +46,8 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv) d_bitblastingRegistrar = new BitblastingRegistrar(this); d_nullContext = new context::Context(); - d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, "EagerBitblaster"); + d_satSolver = prop::SatSolverFactory::createMinisat( + d_nullContext, smtStatisticsRegistry(), "EagerBitblaster"); d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar, d_nullContext, d_bv->globals()); diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp index b8173cb8b..34a9418dd 100644 --- a/src/theory/bv/lazy_bitblaster.cpp +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -20,6 +20,7 @@ #include "prop/cnf_stream.h" #include "prop/sat_solver.h" #include "prop/sat_solver_factory.h" +#include "smt/smt_statistics_registry.h" #include "theory/bv/abstraction.h" #include "theory/bv/theory_bv.h" #include "theory/rewriter.h" @@ -46,7 +47,8 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, , d_name(name) , d_statistics(name) { - d_satSolver = prop::SatSolverFactory::createMinisat(c, name); + d_satSolver = prop::SatSolverFactory::createMinisat( + c, smtStatisticsRegistry(), name); d_nullRegistrar = new prop::NullRegistrar(); d_nullContext = new context::Context(); d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar, @@ -307,24 +309,24 @@ TLazyBitblaster::Statistics::Statistics(const std::string& prefix) : d_numBitblastingPropagations("theory::bv::"+prefix+"::NumberOfBitblastingPropagations", 0), d_bitblastTimer("theory::bv::"+prefix+"::BitblastTimer") { - StatisticsRegistry::registerStat(&d_numTermClauses); - StatisticsRegistry::registerStat(&d_numAtomClauses); - StatisticsRegistry::registerStat(&d_numTerms); - StatisticsRegistry::registerStat(&d_numAtoms); - StatisticsRegistry::registerStat(&d_numExplainedPropagations); - StatisticsRegistry::registerStat(&d_numBitblastingPropagations); - StatisticsRegistry::registerStat(&d_bitblastTimer); + smtStatisticsRegistry()->registerStat(&d_numTermClauses); + smtStatisticsRegistry()->registerStat(&d_numAtomClauses); + smtStatisticsRegistry()->registerStat(&d_numTerms); + smtStatisticsRegistry()->registerStat(&d_numAtoms); + smtStatisticsRegistry()->registerStat(&d_numExplainedPropagations); + smtStatisticsRegistry()->registerStat(&d_numBitblastingPropagations); + smtStatisticsRegistry()->registerStat(&d_bitblastTimer); } TLazyBitblaster::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_numTermClauses); - StatisticsRegistry::unregisterStat(&d_numAtomClauses); - StatisticsRegistry::unregisterStat(&d_numTerms); - StatisticsRegistry::unregisterStat(&d_numAtoms); - StatisticsRegistry::unregisterStat(&d_numExplainedPropagations); - StatisticsRegistry::unregisterStat(&d_numBitblastingPropagations); - StatisticsRegistry::unregisterStat(&d_bitblastTimer); + smtStatisticsRegistry()->unregisterStat(&d_numTermClauses); + smtStatisticsRegistry()->unregisterStat(&d_numAtomClauses); + smtStatisticsRegistry()->unregisterStat(&d_numTerms); + smtStatisticsRegistry()->unregisterStat(&d_numAtoms); + smtStatisticsRegistry()->unregisterStat(&d_numExplainedPropagations); + smtStatisticsRegistry()->unregisterStat(&d_numBitblastingPropagations); + smtStatisticsRegistry()->unregisterStat(&d_bitblastTimer); } bool TLazyBitblaster::MinisatNotify::notify(prop::SatLiteral lit) { @@ -496,7 +498,8 @@ void TLazyBitblaster::clearSolver() { invalidateModelCache(); // recreate sat solver - d_satSolver = prop::SatSolverFactory::createMinisat(d_ctx); + d_satSolver = prop::SatSolverFactory::createMinisat( + d_ctx, smtStatisticsRegistry()); d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar, d_nullContext, d_bv->globals()); diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp index d31ff50d1..0e6815f47 100644 --- a/src/theory/bv/slicer.cpp +++ b/src/theory/bv/slicer.cpp @@ -13,9 +13,10 @@ ** ** Bitvector theory. **/ +#include "theory/bv/slicer.h" #include "options/bv_options.h" -#include "theory/bv/slicer.h" +#include "smt/smt_statistics_registry.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" @@ -598,17 +599,17 @@ UnionFind::Statistics::Statistics(): d_avgFindDepth("theory::bv::slicer::AverageFindDepth"), d_numAddedEqualities("theory::bv::slicer::NumberOfEqualitiesAdded", Slicer::d_numAddedEqualities) { - StatisticsRegistry::registerStat(&d_numRepresentatives); - StatisticsRegistry::registerStat(&d_numSplits); - StatisticsRegistry::registerStat(&d_numMerges); - StatisticsRegistry::registerStat(&d_avgFindDepth); - StatisticsRegistry::registerStat(&d_numAddedEqualities); + smtStatisticsRegistry()->registerStat(&d_numRepresentatives); + smtStatisticsRegistry()->registerStat(&d_numSplits); + smtStatisticsRegistry()->registerStat(&d_numMerges); + smtStatisticsRegistry()->registerStat(&d_avgFindDepth); + smtStatisticsRegistry()->registerStat(&d_numAddedEqualities); } UnionFind::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_numRepresentatives); - StatisticsRegistry::unregisterStat(&d_numSplits); - StatisticsRegistry::unregisterStat(&d_numMerges); - StatisticsRegistry::unregisterStat(&d_avgFindDepth); - StatisticsRegistry::unregisterStat(&d_numAddedEqualities); + smtStatisticsRegistry()->unregisterStat(&d_numRepresentatives); + smtStatisticsRegistry()->unregisterStat(&d_numSplits); + smtStatisticsRegistry()->unregisterStat(&d_numMerges); + smtStatisticsRegistry()->unregisterStat(&d_avgFindDepth); + smtStatisticsRegistry()->unregisterStat(&d_numAddedEqualities); } diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h index 5ecc2a788..68642784f 100644 --- a/src/theory/bv/slicer.h +++ b/src/theory/bv/slicer.h @@ -23,11 +23,10 @@ #include <ext/hash_map> #include "expr/node.h" -#include "expr/statistics_registry.h" #include "theory/bv/theory_bv_utils.h" #include "util/bitvector.h" #include "util/index.h" - +#include "util/statistics_registry.h" #ifndef __CVC4__THEORY__BV__SLICER_BV_H #define __CVC4__THEORY__BV__SLICER_BV_H diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 0505035c7..4acd1b847 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -17,6 +17,7 @@ #include "options/bv_options.h" #include "options/smt_options.h" +#include "smt/smt_statistics_registry.h" #include "theory/bv/abstraction.h" #include "theory/bv/bv_eager_solver.h" #include "theory/bv/bv_subtheory_algebraic.h" @@ -123,23 +124,23 @@ TheoryBV::Statistics::Statistics(): d_weightComputationTimer("theory::bv::weightComputationTimer"), d_numMultSlice("theory::bv::NumMultSliceApplied", 0) { - StatisticsRegistry::registerStat(&d_avgConflictSize); - StatisticsRegistry::registerStat(&d_solveSubstitutions); - StatisticsRegistry::registerStat(&d_solveTimer); - StatisticsRegistry::registerStat(&d_numCallsToCheckFullEffort); - StatisticsRegistry::registerStat(&d_numCallsToCheckStandardEffort); - StatisticsRegistry::registerStat(&d_weightComputationTimer); - StatisticsRegistry::registerStat(&d_numMultSlice); + smtStatisticsRegistry()->registerStat(&d_avgConflictSize); + smtStatisticsRegistry()->registerStat(&d_solveSubstitutions); + smtStatisticsRegistry()->registerStat(&d_solveTimer); + smtStatisticsRegistry()->registerStat(&d_numCallsToCheckFullEffort); + smtStatisticsRegistry()->registerStat(&d_numCallsToCheckStandardEffort); + smtStatisticsRegistry()->registerStat(&d_weightComputationTimer); + smtStatisticsRegistry()->registerStat(&d_numMultSlice); } TheoryBV::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_avgConflictSize); - StatisticsRegistry::unregisterStat(&d_solveSubstitutions); - StatisticsRegistry::unregisterStat(&d_solveTimer); - StatisticsRegistry::unregisterStat(&d_numCallsToCheckFullEffort); - StatisticsRegistry::unregisterStat(&d_numCallsToCheckStandardEffort); - StatisticsRegistry::unregisterStat(&d_weightComputationTimer); - StatisticsRegistry::unregisterStat(&d_numMultSlice); + smtStatisticsRegistry()->unregisterStat(&d_avgConflictSize); + smtStatisticsRegistry()->unregisterStat(&d_solveSubstitutions); + smtStatisticsRegistry()->unregisterStat(&d_solveTimer); + smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckFullEffort); + smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckStandardEffort); + smtStatisticsRegistry()->unregisterStat(&d_weightComputationTimer); + smtStatisticsRegistry()->unregisterStat(&d_numMultSlice); } Node TheoryBV::getBVDivByZero(Kind k, unsigned width) { diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 8ded63c28..e7e4d464f 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -22,12 +22,12 @@ #include "context/cdhashset.h" #include "context/cdlist.h" #include "context/context.h" -#include "expr/statistics_registry.h" #include "smt/smt_globals.h" #include "theory/bv/bv_subtheory.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory.h" #include "util/hash.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index f5e2a2077..af080a970 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -22,10 +22,10 @@ #include <sstream> #include "context/context.h" -#include "expr/statistics_registry.h" #include "smt_util/command.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { @@ -328,7 +328,7 @@ class RewriteRule { // /** Constructor */ // RuleStatistics() // : d_ruleApplications(getStatName("theory::bv::RewriteRules::count"), 0) { - // StatisticsRegistry::registerStat(&d_ruleApplications); + // currentStatisticsRegistry()->registerStat(&d_ruleApplications); // } // /** Destructor */ diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 2c82943ce..6e2fdf58e 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -36,14 +36,14 @@ RewriteFunction TheoryBVRewriter::d_rewriteTable[kind::LAST_KIND]; void TheoryBVRewriter::init() { // s_allRules = new AllRewriteRules; // d_rewriteTimer = new TimerStat("theory::bv::rewriteTimer"); - // StatisticsRegistry::registerStat(d_rewriteTimer); + // smtStatisticsRegistry()->registerStat(d_rewriteTimer); initializeRewrites(); } void TheoryBVRewriter::shutdown() { // delete s_allRules; - // StatisticsRegistry::unregisterStat(d_rewriteTimer); + // smtStatisticsRegistry()->unregisterStat(d_rewriteTimer); //delete d_rewriteTimer; } diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index 7e5d429fd..3f0fa8194 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -20,8 +20,8 @@ #ifndef __CVC4__THEORY__BV__THEORY_BV_REWRITER_H #define __CVC4__THEORY__BV__THEORY_BV_REWRITER_H -#include "expr/statistics_registry.h" #include "theory/rewriter.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/ite_utilities.cpp b/src/theory/ite_utilities.cpp index 20464b14e..2791a9555 100644 --- a/src/theory/ite_utilities.cpp +++ b/src/theory/ite_utilities.cpp @@ -16,10 +16,11 @@ ** Kim, Somenzi, Jin. Efficient Term-ITE Conversion for SMT. FMCAD 2009. ** Burch, Jerry. Techniques for Verifying Superscalar Microprocessors. DAC '96 **/ - - #include "theory/ite_utilities.h" + #include <utility> + +#include "smt/smt_statistics_registry.h" #include "theory/rewriter.h" #include "theory/theory.h" @@ -276,13 +277,13 @@ ITECompressor::Statistics::Statistics(): d_compressCalls("ite-simp::compressCalls", 0), d_skolemsAdded("ite-simp::skolems", 0) { - StatisticsRegistry::registerStat(&d_compressCalls); - StatisticsRegistry::registerStat(&d_skolemsAdded); + smtStatisticsRegistry()->registerStat(&d_compressCalls); + smtStatisticsRegistry()->registerStat(&d_skolemsAdded); } ITECompressor::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_compressCalls); - StatisticsRegistry::unregisterStat(&d_skolemsAdded); + smtStatisticsRegistry()->unregisterStat(&d_compressCalls); + smtStatisticsRegistry()->unregisterStat(&d_skolemsAdded); } Node ITECompressor::push_back_boolean(Node original, Node compressed){ @@ -611,25 +612,25 @@ ITESimplifier::Statistics::Statistics(): d_simpITEVisits("ite-simp::simpITE.visits", 0), d_inSmaller("ite-simp::inSmaller") { - StatisticsRegistry::registerStat(&d_maxNonConstantsFolded); - StatisticsRegistry::registerStat(&d_unexpected); - StatisticsRegistry::registerStat(&d_unsimplified); - StatisticsRegistry::registerStat(&d_exactMatchFold); - StatisticsRegistry::registerStat(&d_binaryPredFold); - StatisticsRegistry::registerStat(&d_specialEqualityFolds); - StatisticsRegistry::registerStat(&d_simpITEVisits); - StatisticsRegistry::registerStat(&d_inSmaller); + smtStatisticsRegistry()->registerStat(&d_maxNonConstantsFolded); + smtStatisticsRegistry()->registerStat(&d_unexpected); + smtStatisticsRegistry()->registerStat(&d_unsimplified); + smtStatisticsRegistry()->registerStat(&d_exactMatchFold); + smtStatisticsRegistry()->registerStat(&d_binaryPredFold); + smtStatisticsRegistry()->registerStat(&d_specialEqualityFolds); + smtStatisticsRegistry()->registerStat(&d_simpITEVisits); + smtStatisticsRegistry()->registerStat(&d_inSmaller); } ITESimplifier::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_maxNonConstantsFolded); - StatisticsRegistry::unregisterStat(&d_unexpected); - StatisticsRegistry::unregisterStat(&d_unsimplified); - StatisticsRegistry::unregisterStat(&d_exactMatchFold); - StatisticsRegistry::unregisterStat(&d_binaryPredFold); - StatisticsRegistry::unregisterStat(&d_specialEqualityFolds); - StatisticsRegistry::unregisterStat(&d_simpITEVisits); - StatisticsRegistry::unregisterStat(&d_inSmaller); + smtStatisticsRegistry()->unregisterStat(&d_maxNonConstantsFolded); + smtStatisticsRegistry()->unregisterStat(&d_unexpected); + smtStatisticsRegistry()->unregisterStat(&d_unsimplified); + smtStatisticsRegistry()->unregisterStat(&d_exactMatchFold); + smtStatisticsRegistry()->unregisterStat(&d_binaryPredFold); + smtStatisticsRegistry()->unregisterStat(&d_specialEqualityFolds); + smtStatisticsRegistry()->unregisterStat(&d_simpITEVisits); + smtStatisticsRegistry()->unregisterStat(&d_inSmaller); } bool ITESimplifier::isConstantIte(TNode e){ diff --git a/src/theory/ite_utilities.h b/src/theory/ite_utilities.h index 27fce3071..10fe2853b 100644 --- a/src/theory/ite_utilities.h +++ b/src/theory/ite_utilities.h @@ -27,7 +27,7 @@ #include <vector> #include "expr/node.h" -#include "expr/statistics_registry.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 81fe00674..cc0b18ffe 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -16,6 +16,7 @@ #include "expr/datatype.h" #include "options/quantifiers_options.h" +#include "smt/smt_statistics_registry.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" @@ -696,15 +697,15 @@ CegInstantiation::Statistics::Statistics(): d_cegqi_lemmas_refine("CegInstantiation::cegqi_lemmas_refine", 0), d_cegqi_si_lemmas("CegInstantiation::cegqi_lemmas_si", 0) { - StatisticsRegistry::registerStat(&d_cegqi_lemmas_ce); - StatisticsRegistry::registerStat(&d_cegqi_lemmas_refine); - StatisticsRegistry::registerStat(&d_cegqi_si_lemmas); + smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_ce); + smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_refine); + smtStatisticsRegistry()->registerStat(&d_cegqi_si_lemmas); } CegInstantiation::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_cegqi_lemmas_ce); - StatisticsRegistry::unregisterStat(&d_cegqi_lemmas_refine); - StatisticsRegistry::unregisterStat(&d_cegqi_si_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_ce); + smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_refine); + smtStatisticsRegistry()->unregisterStat(&d_cegqi_si_lemmas); } diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h index 5b3c5263f..9504bd407 100644 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -18,8 +18,8 @@ #ifndef __CVC4__CEG_INSTANTIATOR_H #define __CVC4__CEG_INSTANTIATOR_H -#include "expr/statistics_registry.h" #include "theory/quantifiers_engine.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 2105007e2..5511af209 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -18,10 +18,10 @@ #ifndef __CVC4__INST_STRATEGY_CBQI_H #define __CVC4__INST_STRATEGY_CBQI_H -#include "expr/statistics_registry.h" #include "theory/arith/arithvar.h" #include "theory/quantifiers/ceg_instantiator.h" #include "theory/quantifiers/instantiation_engine.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h index a19bcca76..4e7afad5d 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/inst_strategy_e_matching.h @@ -19,10 +19,10 @@ #include "context/context.h" #include "context/context_mm.h" -#include "expr/statistics_registry.h" #include "theory/quantifiers/instantiation_engine.h" #include "theory/quantifiers/trigger.h" #include "theory/quantifiers_engine.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index dc18548a5..95b674cca 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -352,25 +352,25 @@ QModelBuilderIG::Statistics::Statistics(): d_eval_lits("QModelBuilderIG::Eval_Lits", 0 ), d_eval_lits_unknown("QModelBuilderIG::Eval_Lits_Unknown", 0 ) { - StatisticsRegistry::registerStat(&d_num_quants_init); - StatisticsRegistry::registerStat(&d_num_partial_quants_init); - StatisticsRegistry::registerStat(&d_init_inst_gen_lemmas); - StatisticsRegistry::registerStat(&d_inst_gen_lemmas); - StatisticsRegistry::registerStat(&d_eval_formulas); - StatisticsRegistry::registerStat(&d_eval_uf_terms); - StatisticsRegistry::registerStat(&d_eval_lits); - StatisticsRegistry::registerStat(&d_eval_lits_unknown); + smtStatisticsRegistry()->registerStat(&d_num_quants_init); + smtStatisticsRegistry()->registerStat(&d_num_partial_quants_init); + smtStatisticsRegistry()->registerStat(&d_init_inst_gen_lemmas); + smtStatisticsRegistry()->registerStat(&d_inst_gen_lemmas); + smtStatisticsRegistry()->registerStat(&d_eval_formulas); + smtStatisticsRegistry()->registerStat(&d_eval_uf_terms); + smtStatisticsRegistry()->registerStat(&d_eval_lits); + smtStatisticsRegistry()->registerStat(&d_eval_lits_unknown); } QModelBuilderIG::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_num_quants_init); - StatisticsRegistry::unregisterStat(&d_num_partial_quants_init); - StatisticsRegistry::unregisterStat(&d_init_inst_gen_lemmas); - StatisticsRegistry::unregisterStat(&d_inst_gen_lemmas); - StatisticsRegistry::unregisterStat(&d_eval_formulas); - StatisticsRegistry::unregisterStat(&d_eval_uf_terms); - StatisticsRegistry::unregisterStat(&d_eval_lits); - StatisticsRegistry::unregisterStat(&d_eval_lits_unknown); + smtStatisticsRegistry()->unregisterStat(&d_num_quants_init); + smtStatisticsRegistry()->unregisterStat(&d_num_partial_quants_init); + smtStatisticsRegistry()->unregisterStat(&d_init_inst_gen_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_inst_gen_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_eval_formulas); + smtStatisticsRegistry()->unregisterStat(&d_eval_uf_terms); + smtStatisticsRegistry()->unregisterStat(&d_eval_lits); + smtStatisticsRegistry()->unregisterStat(&d_eval_lits_unknown); } bool QModelBuilderIG::isQuantifierActive( Node f ){ diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 6a21a50e5..eb827edc3 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -326,13 +326,13 @@ ModelEngine::Statistics::Statistics(): d_exh_inst_lemmas("ModelEngine::Instantiations_Exhaustive", 0 ), d_mbqi_inst_lemmas("ModelEngine::Instantiations_Mbqi", 0 ) { - StatisticsRegistry::registerStat(&d_inst_rounds); - StatisticsRegistry::registerStat(&d_exh_inst_lemmas); - StatisticsRegistry::registerStat(&d_mbqi_inst_lemmas); + smtStatisticsRegistry()->registerStat(&d_inst_rounds); + smtStatisticsRegistry()->registerStat(&d_exh_inst_lemmas); + smtStatisticsRegistry()->registerStat(&d_mbqi_inst_lemmas); } ModelEngine::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_inst_rounds); - StatisticsRegistry::unregisterStat(&d_exh_inst_lemmas); - StatisticsRegistry::unregisterStat(&d_mbqi_inst_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_inst_rounds); + smtStatisticsRegistry()->unregisterStat(&d_exh_inst_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_mbqi_inst_lemmas); } diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index b6256980a..a890276f7 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -18,6 +18,7 @@ #include <vector> #include "options/quantifiers_options.h" +#include "smt/smt_statistics_registry.h" #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/trigger.h" @@ -2227,17 +2228,17 @@ QuantConflictFind::Statistics::Statistics(): d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 ), d_entailment_checks("QuantConflictFind::Entailment_Checks",0) { - StatisticsRegistry::registerStat(&d_inst_rounds); - StatisticsRegistry::registerStat(&d_conflict_inst); - StatisticsRegistry::registerStat(&d_prop_inst); - StatisticsRegistry::registerStat(&d_entailment_checks); + smtStatisticsRegistry()->registerStat(&d_inst_rounds); + smtStatisticsRegistry()->registerStat(&d_conflict_inst); + smtStatisticsRegistry()->registerStat(&d_prop_inst); + smtStatisticsRegistry()->registerStat(&d_entailment_checks); } QuantConflictFind::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_inst_rounds); - StatisticsRegistry::unregisterStat(&d_conflict_inst); - StatisticsRegistry::unregisterStat(&d_prop_inst); - StatisticsRegistry::unregisterStat(&d_entailment_checks); + smtStatisticsRegistry()->unregisterStat(&d_inst_rounds); + smtStatisticsRegistry()->unregisterStat(&d_conflict_inst); + smtStatisticsRegistry()->unregisterStat(&d_prop_inst); + smtStatisticsRegistry()->unregisterStat(&d_entailment_checks); } TNode QuantConflictFind::getZero( Kind k ) { diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index f24c10fc0..63f3379b8 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -24,9 +24,9 @@ #include <map> #include "context/cdhashmap.h" -#include "expr/statistics_registry.h" #include "theory/theory.h" #include "util/hash.h" +#include "util/statistics_registry.h" namespace CVC4 { class TheoryEngine; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index e46c59dc0..3813d7cd2 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -16,6 +16,7 @@ #include "options/quantifiers_options.h" #include "options/uf_options.h" +#include "smt/smt_statistics_registry.h" #include "theory/arrays/theory_arrays.h" #include "theory/datatypes/theory_datatypes.h" #include "theory/quantifiers/alpha_equivalence.h" @@ -82,14 +83,14 @@ quantifiers::TermDb * QuantifiersModule::getTermDatabase() { } QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te): -d_te( te ), -d_lemmas_produced_c(u), -d_skolemized(u), -d_presolve(u, true), -d_presolve_in(u), -d_presolve_cache(u), -d_presolve_cache_wq(u), -d_presolve_cache_wic(u){ + d_te( te ), + d_lemmas_produced_c(u), + d_skolemized(u), + d_presolve(u, true), + d_presolve_in(u), + d_presolve_cache(u), + d_presolve_cache_wq(u), + d_presolve_cache_wic(u){ d_eq_query = new EqualityQueryQuantifiersEngine( this ); d_term_db = new quantifiers::TermDb( c, u, this ); d_tr_trie = new inst::TriggerTrie; @@ -315,7 +316,7 @@ void QuantifiersEngine::presolve() { } void QuantifiersEngine::check( Theory::Effort e ){ - CodeTimer codeTimer(d_time); + CodeTimer codeTimer(d_statistics.d_time); if( !getMasterEqualityEngine()->consistent() ){ Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl; return; @@ -621,7 +622,7 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){ } void QuantifiersEngine::propagate( Theory::Effort level ){ - CodeTimer codeTimer(d_time); + CodeTimer codeTimer(d_statistics.d_time); for( int i=0; i<(int)d_modules.size(); i++ ){ d_modules[i]->propagate( level ); @@ -1098,59 +1099,62 @@ void QuantifiersEngine::printSynthSolution( std::ostream& out ) { } } -QuantifiersEngine::Statistics::Statistics(): - d_num_quant("QuantifiersEngine::Num_Quantifiers", 0), - d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0), - d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0), - d_instantiations("QuantifiersEngine::Instantiations_Total", 0), - d_inst_duplicate("QuantifiersEngine::Duplicate_Inst", 0), - d_inst_duplicate_eq("QuantifiersEngine::Duplicate_Inst_Eq", 0), - d_triggers("QuantifiersEngine::Triggers", 0), - d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0), - d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0), - d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0), - d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0), - d_red_lte_partial_inst("QuantifiersEngine::Reductions_Lte_Partial_Inst", 0), - d_instantiations_user_patterns("QuantifiersEngine::Instantiations_User_Patterns", 0), - d_instantiations_auto_gen("QuantifiersEngine::Instantiations_Auto_Gen", 0), - d_instantiations_guess("QuantifiersEngine::Instantiations_Guess", 0), - d_instantiations_cbqi_arith("QuantifiersEngine::Instantiations_Cbqi_Arith", 0) +QuantifiersEngine::Statistics::Statistics() + : d_time("theory::QuantifiersEngine::time"), + d_num_quant("QuantifiersEngine::Num_Quantifiers", 0), + d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0), + d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0), + d_instantiations("QuantifiersEngine::Instantiations_Total", 0), + d_inst_duplicate("QuantifiersEngine::Duplicate_Inst", 0), + d_inst_duplicate_eq("QuantifiersEngine::Duplicate_Inst_Eq", 0), + d_triggers("QuantifiersEngine::Triggers", 0), + d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0), + d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0), + d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0), + d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0), + d_red_lte_partial_inst("QuantifiersEngine::Reductions_Lte_Partial_Inst", 0), + d_instantiations_user_patterns("QuantifiersEngine::Instantiations_User_Patterns", 0), + d_instantiations_auto_gen("QuantifiersEngine::Instantiations_Auto_Gen", 0), + d_instantiations_guess("QuantifiersEngine::Instantiations_Guess", 0), + d_instantiations_cbqi_arith("QuantifiersEngine::Instantiations_Cbqi_Arith", 0) { - StatisticsRegistry::registerStat(&d_num_quant); - StatisticsRegistry::registerStat(&d_instantiation_rounds); - StatisticsRegistry::registerStat(&d_instantiation_rounds_lc); - StatisticsRegistry::registerStat(&d_instantiations); - StatisticsRegistry::registerStat(&d_inst_duplicate); - StatisticsRegistry::registerStat(&d_inst_duplicate_eq); - StatisticsRegistry::registerStat(&d_triggers); - StatisticsRegistry::registerStat(&d_simple_triggers); - StatisticsRegistry::registerStat(&d_multi_triggers); - StatisticsRegistry::registerStat(&d_multi_trigger_instantiations); - StatisticsRegistry::registerStat(&d_red_alpha_equiv); - StatisticsRegistry::registerStat(&d_red_lte_partial_inst); - StatisticsRegistry::registerStat(&d_instantiations_user_patterns); - StatisticsRegistry::registerStat(&d_instantiations_auto_gen); - StatisticsRegistry::registerStat(&d_instantiations_guess); - StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith); + smtStatisticsRegistry()->registerStat(&d_time); + smtStatisticsRegistry()->registerStat(&d_num_quant); + smtStatisticsRegistry()->registerStat(&d_instantiation_rounds); + smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc); + smtStatisticsRegistry()->registerStat(&d_instantiations); + smtStatisticsRegistry()->registerStat(&d_inst_duplicate); + smtStatisticsRegistry()->registerStat(&d_inst_duplicate_eq); + smtStatisticsRegistry()->registerStat(&d_triggers); + smtStatisticsRegistry()->registerStat(&d_simple_triggers); + smtStatisticsRegistry()->registerStat(&d_multi_triggers); + smtStatisticsRegistry()->registerStat(&d_multi_trigger_instantiations); + smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv); + smtStatisticsRegistry()->registerStat(&d_red_lte_partial_inst); + smtStatisticsRegistry()->registerStat(&d_instantiations_user_patterns); + smtStatisticsRegistry()->registerStat(&d_instantiations_auto_gen); + smtStatisticsRegistry()->registerStat(&d_instantiations_guess); + smtStatisticsRegistry()->registerStat(&d_instantiations_cbqi_arith); } QuantifiersEngine::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_num_quant); - StatisticsRegistry::unregisterStat(&d_instantiation_rounds); - StatisticsRegistry::unregisterStat(&d_instantiation_rounds_lc); - StatisticsRegistry::unregisterStat(&d_instantiations); - StatisticsRegistry::unregisterStat(&d_inst_duplicate); - StatisticsRegistry::unregisterStat(&d_inst_duplicate_eq); - StatisticsRegistry::unregisterStat(&d_triggers); - StatisticsRegistry::unregisterStat(&d_simple_triggers); - StatisticsRegistry::unregisterStat(&d_multi_triggers); - StatisticsRegistry::unregisterStat(&d_multi_trigger_instantiations); - StatisticsRegistry::unregisterStat(&d_red_alpha_equiv); - StatisticsRegistry::unregisterStat(&d_red_lte_partial_inst); - StatisticsRegistry::unregisterStat(&d_instantiations_user_patterns); - StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen); - StatisticsRegistry::unregisterStat(&d_instantiations_guess); - StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith); + smtStatisticsRegistry()->unregisterStat(&d_time); + smtStatisticsRegistry()->unregisterStat(&d_num_quant); + smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds); + smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc); + smtStatisticsRegistry()->unregisterStat(&d_instantiations); + smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate); + smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_eq); + smtStatisticsRegistry()->unregisterStat(&d_triggers); + smtStatisticsRegistry()->unregisterStat(&d_simple_triggers); + smtStatisticsRegistry()->unregisterStat(&d_multi_triggers); + smtStatisticsRegistry()->unregisterStat(&d_multi_trigger_instantiations); + smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv); + smtStatisticsRegistry()->unregisterStat(&d_red_lte_partial_inst); + smtStatisticsRegistry()->unregisterStat(&d_instantiations_user_patterns); + smtStatisticsRegistry()->unregisterStat(&d_instantiations_auto_gen); + smtStatisticsRegistry()->unregisterStat(&d_instantiations_guess); + smtStatisticsRegistry()->unregisterStat(&d_instantiations_cbqi_arith); } eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){ diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index ba41b2ca3..aa770ad67 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -24,12 +24,12 @@ #include "context/cdchunk_list.h" #include "context/cdhashset.h" #include "expr/attribute.h" -#include "expr/statistics_registry.h" #include "options/quantifiers_modes.h" #include "theory/quantifiers/inst_match.h" #include "theory/quantifiers/quant_util.h" #include "theory/theory.h" #include "util/hash.h" +#include "util/statistics_registry.h" namespace CVC4 { @@ -206,8 +206,7 @@ private: NodeList d_presolve_cache; BoolList d_presolve_cache_wq; BoolList d_presolve_cache_wic; -private: - KEEP_STATISTIC(TimerStat, d_time, "theory::QuantifiersEngine::time"); + public: QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te); ~QuantifiersEngine(); @@ -346,6 +345,7 @@ public: /** statistics class */ class Statistics { public: + TimerStat d_time; IntStat d_num_quant; IntStat d_instantiation_rounds; IntStat d_instantiation_rounds_lc; @@ -382,7 +382,7 @@ private: std::map< Node, int > d_rep_score; /** reset count */ int d_reset_count; -private: + /** node contains */ Node getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache ); /** get score */ diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 758f4a913..697736ebf 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -19,8 +19,10 @@ #include "expr/resource_manager.h" #include "theory/theory.h" -#include "theory/rewriter_tables.h" #include "smt/smt_engine_scope.h" +#include "smt/smt_statistics_registry.h" +#include "theory/rewriter_tables.h" + using namespace std; diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 0c3171065..d0866e537 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -20,6 +20,7 @@ #include "expr/emptyset.h" #include "options/sets_options.h" +#include "smt/smt_statistics_registry.h" #include "theory/sets/expr_patterns.h" // ONLY included here #include "theory/sets/scrutinize.h" #include "theory/sets/theory_sets.h" @@ -924,16 +925,16 @@ TheorySetsPrivate::Statistics::Statistics() : , d_memberLemmas("theory::sets::lemmas::member", 0) , d_disequalityLemmas("theory::sets::lemmas::disequality", 0) { - StatisticsRegistry::registerStat(&d_getModelValueTime); - StatisticsRegistry::registerStat(&d_memberLemmas); - StatisticsRegistry::registerStat(&d_disequalityLemmas); + smtStatisticsRegistry()->registerStat(&d_getModelValueTime); + smtStatisticsRegistry()->registerStat(&d_memberLemmas); + smtStatisticsRegistry()->registerStat(&d_disequalityLemmas); } TheorySetsPrivate::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_getModelValueTime); - StatisticsRegistry::unregisterStat(&d_memberLemmas); - StatisticsRegistry::unregisterStat(&d_disequalityLemmas); + smtStatisticsRegistry()->unregisterStat(&d_getModelValueTime); + smtStatisticsRegistry()->unregisterStat(&d_memberLemmas); + smtStatisticsRegistry()->unregisterStat(&d_disequalityLemmas); } diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index a41326350..89cba3ae4 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -13,8 +13,9 @@ ** \todo document this file **/ - #include "theory/shared_terms_database.h" + +#include "smt/smt_statistics_registry.h" #include "theory/theory_engine.h" using namespace std; @@ -33,12 +34,12 @@ SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine, context::Co , d_theoryEngine(theoryEngine) , d_inConflict(context, false) { - StatisticsRegistry::registerStat(&d_statSharedTerms); + smtStatisticsRegistry()->registerStat(&d_statSharedTerms); } SharedTermsDatabase::~SharedTermsDatabase() throw(AssertionException) { - StatisticsRegistry::unregisterStat(&d_statSharedTerms); + smtStatisticsRegistry()->unregisterStat(&d_statSharedTerms); } void SharedTermsDatabase::addEqualityToPropagate(TNode equality) { diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index fd45cca15..c15336e29 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -19,9 +19,9 @@ #include "context/cdhashset.h" #include "expr/node.h" -#include "expr/statistics_registry.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" +#include "util/statistics_registry.h" namespace CVC4 { diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index b68687d54..4405fe406 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -21,6 +21,7 @@ #include "expr/kind.h" #include "options/strings_options.h" #include "smt/logic_exception.h" +#include "smt/smt_statistics_registry.h" #include "smt_util/command.h" #include "theory/rewriter.h" #include "theory/strings/theory_strings_rewriter.h" @@ -4416,19 +4417,19 @@ TheoryStrings::Statistics::Statistics(): d_loop_lemmas("TheoryStrings::NumOfLoops", 0), d_new_skolems("TheoryStrings::NumOfNewSkolems", 0) { - StatisticsRegistry::registerStat(&d_splits); - StatisticsRegistry::registerStat(&d_eq_splits); - StatisticsRegistry::registerStat(&d_deq_splits); - StatisticsRegistry::registerStat(&d_loop_lemmas); - StatisticsRegistry::registerStat(&d_new_skolems); + smtStatisticsRegistry()->registerStat(&d_splits); + smtStatisticsRegistry()->registerStat(&d_eq_splits); + smtStatisticsRegistry()->registerStat(&d_deq_splits); + smtStatisticsRegistry()->registerStat(&d_loop_lemmas); + smtStatisticsRegistry()->registerStat(&d_new_skolems); } TheoryStrings::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_splits); - StatisticsRegistry::unregisterStat(&d_eq_splits); - StatisticsRegistry::unregisterStat(&d_deq_splits); - StatisticsRegistry::unregisterStat(&d_loop_lemmas); - StatisticsRegistry::unregisterStat(&d_new_skolems); + smtStatisticsRegistry()->unregisterStat(&d_splits); + smtStatisticsRegistry()->unregisterStat(&d_eq_splits); + smtStatisticsRegistry()->unregisterStat(&d_deq_splits); + smtStatisticsRegistry()->unregisterStat(&d_loop_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_new_skolems); } }/* CVC4::theory::strings namespace */ diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 05795ca8f..9e946f8d7 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -19,6 +19,7 @@ #include <vector> #include "base/cvc4_assert.h" +#include "smt/smt_statistics_registry.h" #include "theory/substitutions.h" #include "theory/quantifiers_engine.h" @@ -47,9 +48,33 @@ std::ostream& operator<<(std::ostream& os, Theory::Effort level){ return os; }/* ostream& operator<<(ostream&, Theory::Effort) */ +Theory::Theory(TheoryId id, context::Context* satContext, context::UserContext* userContext, + OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, + SmtGlobals* globals) throw() + : d_id(id) + , d_satContext(satContext) + , d_userContext(userContext) + , d_logicInfo(logicInfo) + , d_facts(satContext) + , d_factsHead(satContext, 0) + , d_sharedTermsIndex(satContext, 0) + , d_careGraph(NULL) + , d_quantEngine(NULL) + , d_checkTime(statName(id, "checkTime")) + , d_computeCareGraphTime(statName(id, "computeCareGraphTime")) + , d_sharedTerms(satContext) + , d_out(&out) + , d_valuation(valuation) + , d_proofEnabled(false) + , d_globals(globals) +{ + smtStatisticsRegistry()->registerStat(&d_checkTime); + smtStatisticsRegistry()->registerStat(&d_computeCareGraphTime); +} + Theory::~Theory() { - StatisticsRegistry::unregisterStat(&d_checkTime); - StatisticsRegistry::unregisterStat(&d_computeCareGraphTime); + smtStatisticsRegistry()->unregisterStat(&d_checkTime); + smtStatisticsRegistry()->unregisterStat(&d_computeCareGraphTime); } TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) { diff --git a/src/theory/theory.h b/src/theory/theory.h index d17d97f97..f7d9ee6a0 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -28,7 +28,6 @@ #include "context/cdo.h" #include "context/context.h" #include "expr/node.h" -#include "expr/statistics_registry.h" #include "lib/ffs.h" #include "options/options.h" #include "options/theory_options.h" @@ -40,6 +39,7 @@ #include "theory/logic_info.h" #include "theory/output_channel.h" #include "theory/valuation.h" +#include "util/statistics_registry.h" namespace CVC4 { @@ -247,27 +247,7 @@ protected: */ Theory(TheoryId id, context::Context* satContext, context::UserContext* userContext, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, - SmtGlobals* globals) throw() - : d_id(id) - , d_satContext(satContext) - , d_userContext(userContext) - , d_logicInfo(logicInfo) - , d_facts(satContext) - , d_factsHead(satContext, 0) - , d_sharedTermsIndex(satContext, 0) - , d_careGraph(NULL) - , d_quantEngine(NULL) - , d_checkTime(statName(id, "checkTime")) - , d_computeCareGraphTime(statName(id, "computeCareGraphTime")) - , d_sharedTerms(satContext) - , d_out(&out) - , d_valuation(valuation) - , d_proofEnabled(false) - , d_globals(globals) - { - StatisticsRegistry::registerStat(&d_checkTime); - StatisticsRegistry::registerStat(&d_computeCareGraphTime); - } + SmtGlobals* globals) throw(); /** * This is called at shutdown time by the TheoryEngine, just before 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 */ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index adc4daeee..7cb15ca97 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -26,7 +26,6 @@ #include "base/cvc4_assert.h" #include "context/cdhashset.h" #include "expr/node.h" -#include "expr/statistics_registry.h" #include "options/options.h" #include "options/smt_options.h" #include "prop/prop_engine.h" @@ -44,6 +43,7 @@ #include "theory/theory.h" #include "theory/uf/equality_engine.h" #include "theory/valuation.h" +#include "util/statistics_registry.h" #include "util/unsafe_interrupt_exception.h" namespace CVC4 { @@ -225,30 +225,8 @@ class TheoryEngine { IntStat conflicts, propagations, lemmas, requirePhase, flipDecision, restartDemands; - 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) - { - StatisticsRegistry::registerStat(&conflicts); - StatisticsRegistry::registerStat(&propagations); - StatisticsRegistry::registerStat(&lemmas); - StatisticsRegistry::registerStat(&requirePhase); - StatisticsRegistry::registerStat(&flipDecision); - StatisticsRegistry::registerStat(&restartDemands); - } - - ~Statistics() { - StatisticsRegistry::unregisterStat(&conflicts); - StatisticsRegistry::unregisterStat(&propagations); - StatisticsRegistry::unregisterStat(&lemmas); - StatisticsRegistry::unregisterStat(&requirePhase); - StatisticsRegistry::unregisterStat(&flipDecision); - StatisticsRegistry::unregisterStat(&restartDemands); - } + Statistics(theory::TheoryId theory); + ~Statistics(); };/* class TheoryEngine::Statistics */ @@ -764,7 +742,7 @@ public: inline bool isTheoryEnabled(theory::TheoryId theoryId) const { return d_logicInfo.isTheoryEnabled(theoryId); } - + /** * Returns the equality status of the two terms, from the theory * that owns the domain type. The types of a and b must be the same. @@ -791,7 +769,7 @@ public: * Print solution for synthesis conjectures found by ce_guided_instantiation module */ void printSynthSolution( std::ostream& out ); - + /** * Forwards an entailment check according to the given theoryOfMode. * See theory.h for documentation on entailmentCheck(). @@ -835,11 +813,11 @@ public: SharedTermsDatabase* getSharedTermsDatabase() { return &d_sharedTerms; } theory::eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; } - + RemoveITE* getIteRemover() { return &d_iteRemover; } SortInference* getSortInference() { return &d_sortInfer; } - + /** Prints the assertions to the debug stream */ void printAssertions(const char* tag); diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index cd6459a3c..828d53144 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -17,10 +17,32 @@ #include "theory/uf/equality_engine.h" +#include "smt/smt_statistics_registry.h" + namespace CVC4 { namespace theory { namespace eq { +EqualityEngine::Statistics::Statistics(std::string name) + : mergesCount(name + "::mergesCount", 0), + termsCount(name + "::termsCount", 0), + functionTermsCount(name + "::functionTermsCount", 0), + constantTermsCount(name + "::constantTermsCount", 0) +{ + smtStatisticsRegistry()->registerStat(&mergesCount); + smtStatisticsRegistry()->registerStat(&termsCount); + smtStatisticsRegistry()->registerStat(&functionTermsCount); + smtStatisticsRegistry()->registerStat(&constantTermsCount); +} + +EqualityEngine::Statistics::~Statistics() { + smtStatisticsRegistry()->unregisterStat(&mergesCount); + smtStatisticsRegistry()->unregisterStat(&termsCount); + smtStatisticsRegistry()->unregisterStat(&functionTermsCount); + smtStatisticsRegistry()->unregisterStat(&constantTermsCount); +} + + /** * Data used in the BFS search through the equality graph. */ @@ -2058,4 +2080,3 @@ void EqProof::debug_print( const char * c, unsigned tb ){ } // Namespace uf } // Namespace theory } // Namespace CVC4 - diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index f7f7f9ddd..87074aebc 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -29,10 +29,10 @@ #include "context/cdo.h" #include "expr/kind_map.h" #include "expr/node.h" -#include "expr/statistics_registry.h" #include "theory/rewriter.h" #include "theory/theory.h" #include "theory/uf/equality_engine_types.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { @@ -193,24 +193,9 @@ public: /** Number of constant terms managed by the system */ IntStat constantTermsCount; - Statistics(std::string name) - : mergesCount(name + "::mergesCount", 0), - termsCount(name + "::termsCount", 0), - functionTermsCount(name + "::functionTermsCount", 0), - constantTermsCount(name + "::constantTermsCount", 0) - { - StatisticsRegistry::registerStat(&mergesCount); - StatisticsRegistry::registerStat(&termsCount); - StatisticsRegistry::registerStat(&functionTermsCount); - StatisticsRegistry::registerStat(&constantTermsCount); - } + Statistics(std::string name); - ~Statistics() { - StatisticsRegistry::unregisterStat(&mergesCount); - StatisticsRegistry::unregisterStat(&termsCount); - StatisticsRegistry::unregisterStat(&functionTermsCount); - StatisticsRegistry::unregisterStat(&constantTermsCount); - } + ~Statistics(); };/* struct EqualityEngine::statistics */ private: @@ -900,4 +885,3 @@ public: } // Namespace eq } // Namespace theory } // Namespace CVC4 - diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h index e49b4652a..763ced650 100644 --- a/src/theory/uf/symmetry_breaker.h +++ b/src/theory/uf/symmetry_breaker.h @@ -52,7 +52,8 @@ #include "context/context.h" #include "expr/node.h" #include "expr/node_builder.h" -#include "expr/statistics_registry.h" +#include "smt/smt_statistics_registry.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 0f8ccf49a..9fceedc96 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -2058,23 +2058,23 @@ StrongSolverTheoryUF::Statistics::Statistics(): d_totality_lemmas("StrongSolverTheoryUF::Totality_Lemmas", 0), d_max_model_size("StrongSolverTheoryUF::Max_Model_Size", 1) { - StatisticsRegistry::registerStat(&d_clique_conflicts); - StatisticsRegistry::registerStat(&d_clique_lemmas); - StatisticsRegistry::registerStat(&d_split_lemmas); - StatisticsRegistry::registerStat(&d_disamb_term_lemmas); - StatisticsRegistry::registerStat(&d_sym_break_lemmas); - StatisticsRegistry::registerStat(&d_totality_lemmas); - StatisticsRegistry::registerStat(&d_max_model_size); + smtStatisticsRegistry()->registerStat(&d_clique_conflicts); + smtStatisticsRegistry()->registerStat(&d_clique_lemmas); + smtStatisticsRegistry()->registerStat(&d_split_lemmas); + smtStatisticsRegistry()->registerStat(&d_disamb_term_lemmas); + smtStatisticsRegistry()->registerStat(&d_sym_break_lemmas); + smtStatisticsRegistry()->registerStat(&d_totality_lemmas); + smtStatisticsRegistry()->registerStat(&d_max_model_size); } StrongSolverTheoryUF::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_clique_conflicts); - StatisticsRegistry::unregisterStat(&d_clique_lemmas); - StatisticsRegistry::unregisterStat(&d_split_lemmas); - StatisticsRegistry::unregisterStat(&d_disamb_term_lemmas); - StatisticsRegistry::unregisterStat(&d_sym_break_lemmas); - StatisticsRegistry::unregisterStat(&d_totality_lemmas); - StatisticsRegistry::unregisterStat(&d_max_model_size); + smtStatisticsRegistry()->unregisterStat(&d_clique_conflicts); + smtStatisticsRegistry()->unregisterStat(&d_clique_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_split_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_disamb_term_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_sym_break_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_totality_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_max_model_size); } @@ -2141,9 +2141,9 @@ void DisequalityPropagator::assertPredicate( Node p, bool polarity ) { DisequalityPropagator::Statistics::Statistics(): d_propagations("StrongSolverTheoryUF::Disequality_Propagations", 0) { - StatisticsRegistry::registerStat(& d_propagations); + smtStatisticsRegistry()->registerStat(& d_propagations); } DisequalityPropagator::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(& d_propagations); + smtStatisticsRegistry()->unregisterStat(& d_propagations); } diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index 45d7fc3cc..24d7f840f 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -21,8 +21,8 @@ #include "context/cdhashmap.h" #include "context/context.h" #include "context/context_mm.h" -#include "expr/statistics_registry.h" #include "theory/theory.h" +#include "util/statistics_registry.h" namespace CVC4 { diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp index 997c998e6..dda73c1d9 100644 --- a/src/theory/unconstrained_simplifier.cpp +++ b/src/theory/unconstrained_simplifier.cpp @@ -17,8 +17,10 @@ #include "theory/unconstrained_simplifier.h" + #include "theory/rewriter.h" #include "theory/logic_info.h" +#include "smt/smt_statistics_registry.h" using namespace std; using namespace CVC4; @@ -30,13 +32,13 @@ UnconstrainedSimplifier::UnconstrainedSimplifier(context::Context* context, : d_numUnconstrainedElim("preprocessor::number of unconstrained elims", 0), d_context(context), d_substitutions(context), d_logicInfo(logicInfo) { - StatisticsRegistry::registerStat(&d_numUnconstrainedElim); + smtStatisticsRegistry()->registerStat(&d_numUnconstrainedElim); } UnconstrainedSimplifier::~UnconstrainedSimplifier() { - StatisticsRegistry::unregisterStat(&d_numUnconstrainedElim); + smtStatisticsRegistry()->unregisterStat(&d_numUnconstrainedElim); } diff --git a/src/theory/unconstrained_simplifier.h b/src/theory/unconstrained_simplifier.h index 6c04d66e7..e23c4853d 100644 --- a/src/theory/unconstrained_simplifier.h +++ b/src/theory/unconstrained_simplifier.h @@ -24,8 +24,8 @@ #include <utility> #include "expr/node.h" -#include "expr/statistics_registry.h" #include "theory/substitutions.h" +#include "util/statistics_registry.h" namespace CVC4 { diff --git a/src/util/Makefile.am b/src/util/Makefile.am index d086e3068..e1c593243 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -49,6 +49,10 @@ libutil_la_SOURCES = \ sexpr.h \ smt2_quote_string.cpp \ smt2_quote_string.h \ + statistics.cpp \ + statistics.h \ + statistics_registry.cpp \ + statistics_registry.h \ subrange_bound.cpp \ subrange_bound.h \ tuple.h \ @@ -95,6 +99,7 @@ EXTRA_DIST = \ regexp.i \ result.i \ sexpr.i \ + statistics.i \ subrange_bound.i \ tuple.i \ unsafe_interrupt_exception.i diff --git a/src/expr/statistics.cpp b/src/util/statistics.cpp index e5d3f6e69..371872454 100644 --- a/src/expr/statistics.cpp +++ b/src/util/statistics.cpp @@ -15,10 +15,11 @@ ** \todo document this file **/ +#include "util/statistics.h" + #include <typeinfo> -#include "expr/statistics.h" -#include "expr/statistics_registry.h" // for details about class Stat +#include "util/statistics_registry.h" // for details about class Stat namespace CVC4 { diff --git a/src/expr/statistics.h b/src/util/statistics.h index a0b6ed083..a0b6ed083 100644 --- a/src/expr/statistics.h +++ b/src/util/statistics.h diff --git a/src/expr/statistics.i b/src/util/statistics.i index 990f465f5..bd3a4eeb9 100644 --- a/src/expr/statistics.i +++ b/src/util/statistics.i @@ -1,5 +1,5 @@ %{ -#include "expr/statistics.h" +#include "util/statistics.h" #ifdef SWIGJAVA @@ -67,7 +67,7 @@ #endif /* SWIGJAVA */ -%include "expr/statistics.h" +%include "util/statistics.h" #ifdef SWIGJAVA diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp new file mode 100644 index 000000000..c9051cc0e --- /dev/null +++ b/src/util/statistics_registry.cpp @@ -0,0 +1,245 @@ +/********************* */ +/*! \file statistics_registry.cpp + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): Kshitij Bansal, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "util/statistics_registry.h" + +#include "base/cvc4_assert.h" +#include "lib/clock_gettime.h" + + +#ifdef CVC4_STATISTICS_ON +# define __CVC4_USE_STATISTICS true +#else +# define __CVC4_USE_STATISTICS false +#endif + + +/****************************************************************************/ +/* Some utility functions for timespec */ +/****************************************************************************/ +namespace CVC4 { + +/** Compute the sum of two timespecs. */ +inline timespec& operator+=(timespec& a, const timespec& b) { + using namespace CVC4; + // assumes a.tv_nsec and b.tv_nsec are in range + const long nsec_per_sec = 1000000000L; // one thousand million + CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a); + CheckArgument(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec, b); + a.tv_sec += b.tv_sec; + long nsec = a.tv_nsec + b.tv_nsec; + assert(nsec >= 0); + if(nsec < 0) { + nsec += nsec_per_sec; + --a.tv_sec; + } + if(nsec >= nsec_per_sec) { + nsec -= nsec_per_sec; + ++a.tv_sec; + } + assert(nsec >= 0 && nsec < nsec_per_sec); + a.tv_nsec = nsec; + return a; +} + +/** Compute the difference of two timespecs. */ +inline timespec& operator-=(timespec& a, const timespec& b) { + using namespace CVC4; + // assumes a.tv_nsec and b.tv_nsec are in range + const long nsec_per_sec = 1000000000L; // one thousand million + CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a); + CheckArgument(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec, b); + a.tv_sec -= b.tv_sec; + long nsec = a.tv_nsec - b.tv_nsec; + if(nsec < 0) { + nsec += nsec_per_sec; + --a.tv_sec; + } + if(nsec >= nsec_per_sec) { + nsec -= nsec_per_sec; + ++a.tv_sec; + } + assert(nsec >= 0 && nsec < nsec_per_sec); + a.tv_nsec = nsec; + return a; +} + +/** Add two timespecs. */ +inline timespec operator+(const timespec& a, const timespec& b) { + timespec result = a; + return result += b; +} + +/** Subtract two timespecs. */ +inline timespec operator-(const timespec& a, const timespec& b) { + timespec result = a; + return result -= b; +} + +/** + * Compare two timespecs for equality. + * This must be kept in sync with the copy in test/util/stats_black.h + */ +inline bool operator==(const timespec& a, const timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return a.tv_sec == b.tv_sec && a.tv_nsec == b.tv_nsec; +} + +/** Compare two timespecs for disequality. */ +inline bool operator!=(const timespec& a, const timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return !(a == b); +} + +/** Compare two timespecs, returning true iff a < b. */ +inline bool operator<(const timespec& a, const timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return a.tv_sec < b.tv_sec || + (a.tv_sec == b.tv_sec && a.tv_nsec < b.tv_nsec); +} + +/** Compare two timespecs, returning true iff a > b. */ +inline bool operator>(const timespec& a, const timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return a.tv_sec > b.tv_sec || + (a.tv_sec == b.tv_sec && a.tv_nsec > b.tv_nsec); +} + +/** Compare two timespecs, returning true iff a <= b. */ +inline bool operator<=(const timespec& a, const timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return !(a > b); +} + +/** Compare two timespecs, returning true iff a >= b. */ +inline bool operator>=(const timespec& a, const timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return !(a < b); +} + +/** Output a timespec on an output stream. */ +std::ostream& operator<<(std::ostream& os, const timespec& t) { + // assumes t.tv_nsec is in range + return os << t.tv_sec << "." + << std::setfill('0') << std::setw(9) << std::right << t.tv_nsec; +} + + +/** Construct a statistics registry */ +StatisticsRegistry::StatisticsRegistry(const std::string& name) + throw(CVC4::IllegalArgumentException) : + Stat(name) { + + d_prefix = name; + if(__CVC4_USE_STATISTICS) { + PrettyCheckArgument(d_name.find(s_regDelim) == std::string::npos, name, + "StatisticsRegistry names cannot contain the string \"%s\"", + s_regDelim.c_str()); + } +} + +void StatisticsRegistry::registerStat(Stat* s) throw(CVC4::IllegalArgumentException) { +#ifdef CVC4_STATISTICS_ON + PrettyCheckArgument(d_stats.find(s) == d_stats.end(), s, + "Statistic `%s' was not registered with this registry.", + s->getName().c_str()); + d_stats.insert(s); +#endif /* CVC4_STATISTICS_ON */ +}/* StatisticsRegistry::registerStat_() */ + +void StatisticsRegistry::unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException) { +#ifdef CVC4_STATISTICS_ON + PrettyCheckArgument(d_stats.find(s) != d_stats.end(), s, + "Statistic `%s' was not registered with this registry.", + s->getName().c_str()); + d_stats.erase(s); +#endif /* CVC4_STATISTICS_ON */ +}/* StatisticsRegistry::unregisterStat_() */ + +void StatisticsRegistry::flushStat(std::ostream &out) const { +#ifdef CVC4_STATISTICS_ON + flushInformation(out); +#endif /* CVC4_STATISTICS_ON */ +} + +void StatisticsRegistry::flushInformation(std::ostream &out) const { +#ifdef CVC4_STATISTICS_ON + this->StatisticsBase::flushInformation(out); +#endif /* CVC4_STATISTICS_ON */ +} + +void TimerStat::start() { + if(__CVC4_USE_STATISTICS) { + PrettyCheckArgument(!d_running, *this, "timer already running"); + clock_gettime(CLOCK_MONOTONIC, &d_start); + d_running = true; + } +}/* TimerStat::start() */ + +void TimerStat::stop() { + if(__CVC4_USE_STATISTICS) { + PrettyCheckArgument(d_running, *this, "timer not running"); + ::timespec end; + clock_gettime(CLOCK_MONOTONIC, &end); + d_data += end - d_start; + d_running = false; + } +}/* TimerStat::stop() */ + +bool TimerStat::running() const { + return d_running; +}/* TimerStat::running() */ + +timespec TimerStat::getData() const { + ::timespec data = d_data; + if(__CVC4_USE_STATISTICS && d_running) { + ::timespec end; + clock_gettime(CLOCK_MONOTONIC, &end); + data += end - d_start; + } + return data; +} + +SExpr TimerStat::getValue() const { + ::timespec data = d_data; + if(__CVC4_USE_STATISTICS && d_running) { + ::timespec end; + clock_gettime(CLOCK_MONOTONIC, &end); + data += end - d_start; + } + std::stringstream ss; + ss << std::fixed << std::setprecision(8) << data; + return SExpr(Rational::fromDecimal(ss.str())); +}/* TimerStat::getValue() */ + + +RegisterStatistic::RegisterStatistic(StatisticsRegistry* reg, Stat* stat) + : d_reg(reg), + d_stat(stat) { + CheckArgument(reg != NULL, reg, + "You need to specify a statistics registry" + "on which to set the statistic"); + d_reg->registerStat(d_stat); +} + +RegisterStatistic::~RegisterStatistic() { + d_reg->unregisterStat(d_stat); +} + +}/* CVC4 namespace */ + +#undef __CVC4_USE_STATISTICS diff --git a/src/expr/statistics_registry.h b/src/util/statistics_registry.h index 3225f6672..f4f00e444 100644 --- a/src/expr/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -14,6 +14,21 @@ ** Statistics utility classes, including classes for holding (and referring ** to) statistics, the statistics registry, and some other associated ** classes. + ** + ** This file is somewhat unique in that it is a "cvc4_private_library.h" + ** header. Because of this, most classes need to be marked as CVC4_PUBLIC. + ** This is because CVC4_PUBLIC is connected to the visibility of the linkage + ** in the object files for the class. It does not dictate what headers are + ** installed. + ** Because the StatisticsRegistry and associated classes are built into + ** libutil, which is used by libcvc4, and then later used by the libmain + ** without referring to libutil as well. Thus the without marking these as + ** CVC4_PUBLIC the symbols would be external in libutil, internal in libcvc4, + ** and not be visible to libmain and linking would fail. + ** You can debug this using "nm" on the .so and .o files in the builds/ + ** directory. See + ** http://eli.thegreenplace.net/2013/07/09/library-order-in-static-linking + ** for a longer discussion on symbol visibility. **/ #include "cvc4_private_library.h" @@ -31,19 +46,25 @@ #include <vector> #include "base/exception.h" -#include "expr/statistics.h" #include "lib/clock_gettime.h" +#include "util/statistics.h" namespace CVC4 { +/** + * Prints a timespec. + * + * This is used in the implementation of TimerStat. This needs to be available + * before Stat due to ordering constraints in clang for TimerStat. + */ +std::ostream& operator<<(std::ostream& os, const timespec& t) CVC4_PUBLIC; + #ifdef CVC4_STATISTICS_ON # define __CVC4_USE_STATISTICS true #else # define __CVC4_USE_STATISTICS false #endif -class ExprManager; -class SmtEngine; /** * The base class for all statistics. @@ -617,11 +638,6 @@ public: d_prefix = d_name = name; } -#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) - /** Get a pointer to the current statistics registry */ - static StatisticsRegistry* current(); -#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) */ - /** Overridden to avoid the name being printed */ void flushStat(std::ostream &out) const; @@ -638,134 +654,14 @@ public: return SExpr(v); } -#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) - /** Register a new statistic, making it active. */ - static void registerStat(Stat* s) throw(CVC4::IllegalArgumentException); - - /** Unregister an active statistic, making it inactive. */ - static void unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException); -#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB) */ - /** Register a new statistic */ - void registerStat_(Stat* s) throw(CVC4::IllegalArgumentException); + void registerStat(Stat* s) throw(CVC4::IllegalArgumentException); /** Unregister a new statistic */ - void unregisterStat_(Stat* s) throw(CVC4::IllegalArgumentException); + void unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException); };/* class StatisticsRegistry */ -}/* CVC4 namespace */ - -/****************************************************************************/ -/* Some utility functions for timespec */ -/****************************************************************************/ - -inline std::ostream& operator<<(std::ostream& os, const timespec& t); - -/** Compute the sum of two timespecs. */ -inline timespec& operator+=(timespec& a, const timespec& b) { - using namespace CVC4; - // assumes a.tv_nsec and b.tv_nsec are in range - const long nsec_per_sec = 1000000000L; // one thousand million - CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a); - CheckArgument(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec, b); - a.tv_sec += b.tv_sec; - long nsec = a.tv_nsec + b.tv_nsec; - assert(nsec >= 0); - if(nsec < 0) { - nsec += nsec_per_sec; - --a.tv_sec; - } - if(nsec >= nsec_per_sec) { - nsec -= nsec_per_sec; - ++a.tv_sec; - } - assert(nsec >= 0 && nsec < nsec_per_sec); - a.tv_nsec = nsec; - return a; -} - -/** Compute the difference of two timespecs. */ -inline timespec& operator-=(timespec& a, const timespec& b) { - using namespace CVC4; - // assumes a.tv_nsec and b.tv_nsec are in range - const long nsec_per_sec = 1000000000L; // one thousand million - CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a); - CheckArgument(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec, b); - a.tv_sec -= b.tv_sec; - long nsec = a.tv_nsec - b.tv_nsec; - if(nsec < 0) { - nsec += nsec_per_sec; - --a.tv_sec; - } - if(nsec >= nsec_per_sec) { - nsec -= nsec_per_sec; - ++a.tv_sec; - } - assert(nsec >= 0 && nsec < nsec_per_sec); - a.tv_nsec = nsec; - return a; -} - -/** Add two timespecs. */ -inline timespec operator+(const timespec& a, const timespec& b) { - timespec result = a; - return result += b; -} - -/** Subtract two timespecs. */ -inline timespec operator-(const timespec& a, const timespec& b) { - timespec result = a; - return result -= b; -} - -/** Compare two timespecs for equality. */ -inline bool operator==(const timespec& a, const timespec& b) { - // assumes a.tv_nsec and b.tv_nsec are in range - return a.tv_sec == b.tv_sec && a.tv_nsec == b.tv_nsec; -} - -/** Compare two timespecs for disequality. */ -inline bool operator!=(const timespec& a, const timespec& b) { - // assumes a.tv_nsec and b.tv_nsec are in range - return !(a == b); -} - -/** Compare two timespecs, returning true iff a < b. */ -inline bool operator<(const timespec& a, const timespec& b) { - // assumes a.tv_nsec and b.tv_nsec are in range - return a.tv_sec < b.tv_sec || - (a.tv_sec == b.tv_sec && a.tv_nsec < b.tv_nsec); -} - -/** Compare two timespecs, returning true iff a > b. */ -inline bool operator>(const timespec& a, const timespec& b) { - // assumes a.tv_nsec and b.tv_nsec are in range - return a.tv_sec > b.tv_sec || - (a.tv_sec == b.tv_sec && a.tv_nsec > b.tv_nsec); -} - -/** Compare two timespecs, returning true iff a <= b. */ -inline bool operator<=(const timespec& a, const timespec& b) { - // assumes a.tv_nsec and b.tv_nsec are in range - return !(a > b); -} - -/** Compare two timespecs, returning true iff a >= b. */ -inline bool operator>=(const timespec& a, const timespec& b) { - // assumes a.tv_nsec and b.tv_nsec are in range - return !(a < b); -} - -/** Output a timespec on an output stream. */ -inline std::ostream& operator<<(std::ostream& os, const timespec& t) { - // assumes t.tv_nsec is in range - return os << t.tv_sec << "." - << std::setfill('0') << std::setw(9) << std::right << t.tv_nsec; -} - -namespace CVC4 { - class CodeTimer; /** @@ -844,34 +740,6 @@ public: };/* class CodeTimer */ /** - * To use a statistic, you need to declare it, initialize it in your - * constructor, register it in your constructor, and deregister it in - * your destructor. Instead, this macro does it all for you (and - * therefore also keeps the statistic type, field name, and output - * string all in the same place in your class's header. Its use is - * like in this example, which takes the place of the declaration of a - * statistics field "d_checkTimer": - * - * KEEP_STATISTIC(TimerStat, d_checkTimer, "theory::uf::checkTime"); - * - * If any args need to be passed to the constructor, you can specify - * them after the string. - * - * The macro works by creating a nested class type, derived from the - * statistic type you give it, which declares a registry-aware - * constructor/destructor pair. - */ -#define KEEP_STATISTIC(_StatType, _StatField, _StatName, _CtorArgs...) \ - struct Statistic_##_StatField : public _StatType { \ - Statistic_##_StatField() : _StatType(_StatName, ## _CtorArgs) { \ - StatisticsRegistry::registerStat(this); \ - } \ - ~Statistic_##_StatField() { \ - StatisticsRegistry::unregisterStat(this); \ - } \ - } _StatField - -/** * Resource-acquisition-is-initialization idiom for statistics * registry. Useful for stack-based statistics (like in the driver). * Generally, for statistics kept in a member field of class, it's @@ -880,41 +748,15 @@ public: * registration/unregistration. This RAII class only does * registration and unregistration. */ -class RegisterStatistic { +class CVC4_PUBLIC RegisterStatistic { +public: + RegisterStatistic(StatisticsRegistry* reg, Stat* stat); + ~RegisterStatistic(); +private: StatisticsRegistry* d_reg; Stat* d_stat; -public: - -#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) - RegisterStatistic(Stat* stat) : - d_reg(StatisticsRegistry::current()), - d_stat(stat) { - if(d_reg != NULL) { - throw CVC4::Exception("There is no current statistics registry!"); - } - StatisticsRegistry::registerStat(d_stat); - } -#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) */ - - RegisterStatistic(StatisticsRegistry* reg, Stat* stat) : - d_reg(reg), - d_stat(stat) { - CheckArgument(reg != NULL, reg, - "You need to specify a statistics registry" - "on which to set the statistic"); - d_reg->registerStat_(d_stat); - } - - RegisterStatistic(ExprManager& em, Stat* stat); - - RegisterStatistic(SmtEngine& smt, Stat* stat); - - ~RegisterStatistic() { - d_reg->unregisterStat_(d_stat); - } - };/* class RegisterStatistic */ #undef __CVC4_USE_STATISTICS diff --git a/test/system/statistics.cpp b/test/system/statistics.cpp index 884ffb8a6..18b1e5937 100644 --- a/test/system/statistics.cpp +++ b/test/system/statistics.cpp @@ -19,9 +19,9 @@ #include <sstream> #include "expr/expr.h" -#include "expr/statistics.h" #include "smt/smt_engine.h" #include "util/sexpr.h" +#include "util/statistics.h" using namespace CVC4; using namespace std; diff --git a/test/unit/util/stats_black.h b/test/unit/util/stats_black.h index c0e1ea7fd..dd67429cf 100644 --- a/test/unit/util/stats_black.h +++ b/test/unit/util/stats_black.h @@ -19,11 +19,24 @@ #include <string> #include <ctime> -#include "expr/statistics_registry.h" +#include "lib/clock_gettime.h" +#include "util/statistics_registry.h" using namespace CVC4; using namespace std; +/** + * This is a duplicate of operator== in statistics_registry.h. + * This is duplicated here to try to avoid polluting top namepsace. + * + * If operator== is in the CVC4 namespace, there are some circumstances + * where clang does not find this operator. + */ +bool operator==(const timespec& a, const timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return a.tv_sec == b.tv_sec && a.tv_nsec == b.tv_nsec; +} + class StatsBlack : public CxxTest::TestSuite { public: |