From: Tim King Date: Sat, 9 Jan 2016 00:44:57 +0000 (-0800) Subject: Removing StatisticsRegistry's static functions current() and registerStat(). X-Git-Tag: cvc5-1.0.0~6113 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f4ef7af0a2295691f281ee1604dfeb4082fe229c;p=cvc5.git Removing StatisticsRegistry's static functions current() and registerStat(). - The functionality the get the StatisticsRegistry attached to the SmtEngine was previously through StatisticsRegistry::current(). This is the dominant StatisticsRegistry in the code. (There is another StatisticsRegistry attached to the NodeManager.) Having this be a static function on StatisticsRegistry requires the use of an SmtEngine in the wrong compilation unit. - Usages of StatisticsRegistry::current() that were visible in prop/{bvminisat,minisat} has been removed. A pointer to the relevant StatisticsRegistry should be passed instead into the constructor. - The function StatisticsRegistry::current() has been replaced by SmtScope::currentStatisticsRegistry(). SmtScope is in the libcvc4 package, where SmtEngine is available in the compilation unit. - The function smtStatisticsRegistry() is a synonym for SmtScope::currentStatisticsRegistry() in smt/smt_statistics_registry.h. This header has fewer include dependencies than the one for SmtScope. - Correspondingly, the static functions StatisticsRegistry::{registerStat, unregisterStat} have been removed. One should instead use smtStatisticsRegistry()->{registerStat,unregisterStat} instead. - The KEEP_STATISTIC macro has been moved into smt/smt_statistics_registry.h. - Documents the reason StatisticsRegistry is CVC4_PUBLIC. This lets me remove the warning I added. - Removing most operators for timespec from statistics_registry.h file. These a bit error prone in clang. - Most of the really confusing ifdef's in util/statistics_registry.h are gone. --- 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 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 #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.cpp b/src/expr/statistics.cpp deleted file mode 100644 index e5d3f6e69..000000000 --- a/src/expr/statistics.cpp +++ /dev/null @@ -1,133 +0,0 @@ -/********************* */ -/*! \file statistics.cpp - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none - ** 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 - -#include "expr/statistics.h" -#include "expr/statistics_registry.h" // for details about class Stat - - -namespace CVC4 { - -std::string StatisticsBase::s_regDelim("::"); - -bool StatisticsBase::StatCmp::operator()(const Stat* s1, const Stat* s2) const { - return s1->getName() < s2->getName(); -} - -StatisticsBase::iterator::value_type StatisticsBase::iterator::operator*() const { - return std::make_pair((*d_it)->getName(), (*d_it)->getValue()); -} - -StatisticsBase::StatisticsBase() : - d_prefix(), - d_stats() { -} - -StatisticsBase::StatisticsBase(const StatisticsBase& stats) : - d_prefix(stats.d_prefix), - d_stats() { -} - -StatisticsBase& StatisticsBase::operator=(const StatisticsBase& stats) { - d_prefix = stats.d_prefix; - return *this; -} - -void Statistics::copyFrom(const StatisticsBase& stats) { - // This is ugly, but otherwise we have to introduce a "friend" relation for - // Base to its derived class (really obnoxious). - StatSet::const_iterator i_begin = ((const Statistics*) &stats)->d_stats.begin(); - StatSet::const_iterator i_end = ((const Statistics*) &stats)->d_stats.end(); - for(StatSet::const_iterator i = i_begin; i != i_end; ++i) { - SExprStat* p = new SExprStat((*i)->getName(), (*i)->getValue()); - d_stats.insert(p); - } -} - -void Statistics::clear() { - for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) { - delete *i; - } - d_stats.clear(); -} - -Statistics::Statistics(const StatisticsBase& stats) : - StatisticsBase(stats) { - copyFrom(stats); -} - -Statistics::Statistics(const Statistics& stats) : - StatisticsBase(stats) { - copyFrom(stats); -} - -Statistics::~Statistics() { - clear(); -} - -Statistics& Statistics::operator=(const StatisticsBase& stats) { - clear(); - this->StatisticsBase::operator=(stats); - copyFrom(stats); - - return *this; -} - -Statistics& Statistics::operator=(const Statistics& stats) { - return this->operator=((const StatisticsBase&)stats); -} - -StatisticsBase::const_iterator StatisticsBase::begin() const { - return iterator(d_stats.begin()); -} - -StatisticsBase::const_iterator StatisticsBase::end() const { - return iterator(d_stats.end()); -} - -void StatisticsBase::flushInformation(std::ostream &out) const { -#ifdef CVC4_STATISTICS_ON - for(StatSet::iterator i = d_stats.begin(); - i != d_stats.end(); - ++i) { - Stat* s = *i; - if(d_prefix != "") { - out << d_prefix << s_regDelim; - } - s->flushStat(out); - out << std::endl; - } -#endif /* CVC4_STATISTICS_ON */ -} - -SExpr StatisticsBase::getStatistic(std::string name) const { - SExpr value; - IntStat s(name, 0); - StatSet::iterator i = d_stats.find(&s); - if(i != d_stats.end()) { - return (*i)->getValue(); - } else { - return SExpr(); - } -} - -void StatisticsBase::setPrefix(const std::string& prefix) { - d_prefix = prefix; -} - -}/* CVC4 namespace */ diff --git a/src/expr/statistics.h b/src/expr/statistics.h deleted file mode 100644 index a0b6ed083..000000000 --- a/src/expr/statistics.h +++ /dev/null @@ -1,129 +0,0 @@ -/********************* */ -/*! \file statistics.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none - ** 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 "cvc4_public.h" - -#ifndef __CVC4__STATISTICS_H -#define __CVC4__STATISTICS_H - -#include -#include -#include -#include -#include - -#include "util/sexpr.h" - -namespace CVC4 { - -class Stat; - -class CVC4_PUBLIC StatisticsBase { -protected: - - static std::string s_regDelim; - - /** A helper class for comparing two statistics */ - struct StatCmp { - bool operator()(const Stat* s1, const Stat* s2) const; - };/* struct StatisticsRegistry::StatCmp */ - - /** A type for a set of statistics */ - typedef std::set< Stat*, StatCmp > StatSet; - - std::string d_prefix; - - /** The set of statistics in this object */ - StatSet d_stats; - - StatisticsBase(); - StatisticsBase(const StatisticsBase& stats); - StatisticsBase& operator=(const StatisticsBase& stats); - -public: - - virtual ~StatisticsBase() { } - - class CVC4_PUBLIC iterator : public std::iterator< std::input_iterator_tag, std::pair > { - StatSet::iterator d_it; - - iterator(StatSet::iterator it) : d_it(it) { } - - friend class StatisticsBase; - - public: - iterator() : d_it() { } - iterator(const iterator& it) : d_it(it.d_it) { } - value_type operator*() const; - iterator& operator++() { ++d_it; return *this; } - iterator operator++(int) { iterator old = *this; ++d_it; return old; } - bool operator==(const iterator& i) const { return d_it == i.d_it; } - bool operator!=(const iterator& i) const { return d_it != i.d_it; } - };/* class StatisticsBase::iterator */ - - /** An iterator type over a set of statistics. */ - typedef iterator const_iterator; - - /** Set the output prefix for this set of statistics. */ - virtual void setPrefix(const std::string& prefix); - - /** Flush all statistics to the given output stream. */ - void flushInformation(std::ostream& out) const; - - /** Get the value of a named statistic. */ - SExpr getStatistic(std::string name) const; - - /** - * Get an iterator to the beginning of the range of the set of - * statistics. - */ - const_iterator begin() const; - - /** - * Get an iterator to the end of the range of the set of statistics. - */ - const_iterator end() const; - -};/* class StatisticsBase */ - -class CVC4_PUBLIC Statistics : public StatisticsBase { - void clear(); - void copyFrom(const StatisticsBase&); - -public: - - /** - * Override the copy constructor to do a "deep" copy of statistics - * values. - */ - Statistics(const StatisticsBase& stats); - Statistics(const Statistics& stats); - - ~Statistics(); - - /** - * Override the assignment operator to do a "deep" copy of statistics - * values. - */ - Statistics& operator=(const StatisticsBase& stats); - Statistics& operator=(const Statistics& stats); - -};/* class Statistics */ - -}/* CVC4 namespace */ - -#endif /* __CVC4__STATISTICS_H */ diff --git a/src/expr/statistics.i b/src/expr/statistics.i deleted file mode 100644 index 990f465f5..000000000 --- a/src/expr/statistics.i +++ /dev/null @@ -1,79 +0,0 @@ -%{ -#include "expr/statistics.h" - -#ifdef SWIGJAVA - -#include "bindings/java_iterator_adapter.h" -#include "bindings/java_stream_adapters.h" - -#endif /* SWIGJAVA */ -%} - -%rename(assign) CVC4::Statistics::operator=(const StatisticsBase&); -%rename(assign) CVC4::Statistics::operator=(const Statistics& stats); - -#ifdef SWIGJAVA - -// Instead of StatisticsBase::begin() and end(), create an -// iterator() method on the Java side that returns a Java-style -// Iterator. -%ignore CVC4::StatisticsBase::begin(); -%ignore CVC4::StatisticsBase::end(); -%ignore CVC4::StatisticsBase::begin() const; -%ignore CVC4::StatisticsBase::end() const; -%extend CVC4::StatisticsBase { - CVC4::JavaIteratorAdapter iterator() { - return CVC4::JavaIteratorAdapter(*$self); - } -} - -// StatisticsBase is "iterable" on the Java side -%typemap(javainterfaces) CVC4::StatisticsBase "java.lang.Iterable"; - -// the JavaIteratorAdapter should not be public, and implements Iterator -%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter "class"; -%typemap(javainterfaces) CVC4::JavaIteratorAdapter "java.util.Iterator"; -// add some functions to the Java side (do it here because there's no way to do these in C++) -%typemap(javacode) CVC4::JavaIteratorAdapter " - public void remove() { - throw new java.lang.UnsupportedOperationException(); - } - - public Object[] next() { - if(hasNext()) { - return getNext(); - } else { - throw new java.util.NoSuchElementException(); - } - } -" -// getNext() just allows C++ iterator access from Java-side next(), make it private -%javamethodmodifiers CVC4::JavaIteratorAdapter::getNext() "private"; - -// map the types appropriately. for statistics, the "payload" of the iterator is an Object[]. -// These Object arrays are always of two elements, the first is a String and the second an -// SExpr. (On the C++ side, it is a std::pair.) -%typemap(jni) CVC4::StatisticsBase::const_iterator::value_type "jobjectArray"; -%typemap(jtype) CVC4::StatisticsBase::const_iterator::value_type "java.lang.Object[]"; -%typemap(jstype) CVC4::StatisticsBase::const_iterator::value_type "java.lang.Object[]"; -%typemap(javaout) CVC4::StatisticsBase::const_iterator::value_type { return $jnicall; } -%typemap(out) CVC4::StatisticsBase::const_iterator::value_type { - $result = jenv->NewObjectArray(2, jenv->FindClass("java/lang/Object"), $null); - jenv->SetObjectArrayElement($result, 0, jenv->NewStringUTF($1.first.c_str())); - jclass clazz = jenv->FindClass("edu/nyu/acsys/CVC4/SExpr"); - jmethodID methodid = jenv->GetMethodID(clazz, "", "(JZ)V"); - jenv->SetObjectArrayElement($result, 1, jenv->NewObject(clazz, methodid, reinterpret_cast(new CVC4::SExpr($1.second)), true)); - }; - -#endif /* SWIGJAVA */ - -%include "expr/statistics.h" - -#ifdef SWIGJAVA - -%include "bindings/java_iterator_adapter.h" -%include "bindings/java_stream_adapters.h" - -%template(JavaIteratorAdapter_StatisticsBase) CVC4::JavaIteratorAdapter; - -#endif /* SWIGJAVA */ 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/expr/statistics_registry.h b/src/expr/statistics_registry.h deleted file mode 100644 index 3225f6672..000000000 --- a/src/expr/statistics_registry.h +++ /dev/null @@ -1,924 +0,0 @@ -/********************* */ -/*! \file statistics_registry.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Tim King - ** Minor contributors (to current version): Kshitij Bansal - ** 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 Statistics utility classes - ** - ** Statistics utility classes, including classes for holding (and referring - ** to) statistics, the statistics registry, and some other associated - ** classes. - **/ - -#include "cvc4_private_library.h" - -#ifndef __CVC4__STATISTICS_REGISTRY_H -#define __CVC4__STATISTICS_REGISTRY_H - -#include - -#include -#include -#include -#include -#include -#include - -#include "base/exception.h" -#include "expr/statistics.h" -#include "lib/clock_gettime.h" - -namespace CVC4 { - -#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. - * - * This base class keeps the name of the statistic and declares the (pure) - * virtual function flushInformation(). Derived classes must implement - * this function and pass their name to the base class constructor. - * - * This class also (statically) maintains the delimiter used to separate - * the name and the value when statistics are output. - */ -class Stat { -protected: - /** The name of this statistic */ - std::string d_name; - -public: - - /** Nullary constructor, does nothing */ - Stat() { } - - /** - * Construct a statistic with the given name. Debug builds of CVC4 - * will throw an assertion exception if the given name contains the - * statistic delimiter string. - */ - Stat(const std::string& name) throw(CVC4::IllegalArgumentException) : - d_name(name) { - if(__CVC4_USE_STATISTICS) { - CheckArgument(d_name.find(", ") == std::string::npos, name, - "Statistics names cannot include a comma (',')"); - } - } - - /** Destruct a statistic. This base-class version does nothing. */ - virtual ~Stat() {} - - /** - * Flush the value of this statistic to an output stream. Should - * finish the output with an end-of-line character. - */ - virtual void flushInformation(std::ostream& out) const = 0; - - /** - * Flush the name,value pair of this statistic to an output stream. - * Uses the statistic delimiter string between name and value. - * - * May be redefined by a child class - */ - virtual void flushStat(std::ostream& out) const { - if(__CVC4_USE_STATISTICS) { - out << d_name << ", "; - flushInformation(out); - } - } - - /** Get the name of this statistic. */ - const std::string& getName() const { - return d_name; - } - - /** Get the value of this statistic as a string. */ - virtual SExpr getValue() const { - std::stringstream ss; - flushInformation(ss); - return SExpr(ss.str()); - } - -};/* class Stat */ - -// A generic way of making a SExpr from templated stats code. -// for example, the uint64_t version ensures that we create -// Integer-SExprs for ReadOnlyDataStats (like those inside -// Minisat) without having to specialize the entire -// ReadOnlyDataStat class template. -template -inline SExpr mkSExpr(const T& x) { - std::stringstream ss; - ss << x; - return SExpr(ss.str()); -} - -template <> -inline SExpr mkSExpr(const uint64_t& x) { - return SExpr(Integer(x)); -} - -template <> -inline SExpr mkSExpr(const int64_t& x) { - return SExpr(Integer(x)); -} - -template <> -inline SExpr mkSExpr(const int& x) { - return SExpr(Integer(x)); -} - -template <> -inline SExpr mkSExpr(const Integer& x) { - return SExpr(x); -} - -template <> -inline SExpr mkSExpr(const double& x) { - // roundabout way to get a Rational from a double - std::stringstream ss; - ss << std::fixed << std::setprecision(8) << x; - return SExpr(Rational::fromDecimal(ss.str())); -} - -template <> -inline SExpr mkSExpr(const Rational& x) { - return SExpr(x); -} - -/** - * A class to represent a "read-only" data statistic of type T. Adds to - * the Stat base class the pure virtual function getData(), which returns - * type T, and flushInformation(), which outputs the statistic value to an - * output stream (using the same existing stream insertion operator). - * - * Template class T must have stream insertion operation defined: - * std::ostream& operator<<(std::ostream&, const T&) - */ -template -class ReadOnlyDataStat : public Stat { -public: - /** The "payload" type of this data statistic (that is, T). */ - typedef T payload_t; - - /** Construct a read-only data statistic with the given name. */ - ReadOnlyDataStat(const std::string& name) : - Stat(name) { - } - - /** Get the value of the statistic. */ - virtual T getData() const = 0; - - /** Flush the value of the statistic to the given output stream. */ - void flushInformation(std::ostream& out) const { - if(__CVC4_USE_STATISTICS) { - out << getData(); - } - } - - SExpr getValue() const { - return mkSExpr(getData()); - } - -};/* class ReadOnlyDataStat */ - - -/** - * A data statistic class. This class extends a read-only data statistic - * with assignment (the statistic can be set as well as read). This class - * adds to the read-only case a pure virtual function setData(), thus - * providing the basic interface for a data statistic: getData() to get the - * statistic value, and setData() to set it. - * - * As with the read-only data statistic class, template class T must have - * stream insertion operation defined: - * std::ostream& operator<<(std::ostream&, const T&) - */ -template -class DataStat : public ReadOnlyDataStat { -public: - - /** Construct a data statistic with the given name. */ - DataStat(const std::string& name) : - ReadOnlyDataStat(name) { - } - - /** Set the data statistic. */ - virtual void setData(const T&) = 0; - -};/* class DataStat */ - - -/** - * A data statistic that references a data cell of type T, - * implementing getData() by referencing that memory cell, and - * setData() by reassigning the statistic to point to the new - * data cell. The referenced data cell is kept as a const - * reference, meaning the referenced data is never actually - * modified by this class (it must be externally modified for - * a reference statistic to make sense). A common use for - * this type of statistic is to output a statistic that is kept - * outside the statistics package (for example, one that's kept - * by a theory implementation for internal heuristic purposes, - * which is important to keep even if statistics are turned off). - * - * Template class T must have an assignment operator=(). - */ -template -class ReferenceStat : public DataStat { -private: - /** The referenced data cell */ - const T* d_data; - -public: - /** - * Construct a reference stat with the given name and a reference - * to NULL. - */ - ReferenceStat(const std::string& name) : - DataStat(name), - d_data(NULL) { - } - - /** - * Construct a reference stat with the given name and a reference to - * the given data. - */ - ReferenceStat(const std::string& name, const T& data) : - DataStat(name), - d_data(NULL) { - setData(data); - } - - /** Set this reference statistic to refer to the given data cell. */ - void setData(const T& t) { - if(__CVC4_USE_STATISTICS) { - d_data = &t; - } - } - - /** Get the value of the referenced data cell. */ - T getData() const { - return *d_data; - } - -};/* class ReferenceStat */ - - -/** - * A data statistic that keeps a T and sets it with setData(). - * - * Template class T must have an operator=() and a copy constructor. - */ -template -class BackedStat : public DataStat { -protected: - /** The internally-kept statistic value */ - T d_data; - -public: - - /** Construct a backed statistic with the given name and initial value. */ - BackedStat(const std::string& name, const T& init) : - DataStat(name), - d_data(init) { - } - - /** Set the underlying data value to the given value. */ - void setData(const T& t) { - if(__CVC4_USE_STATISTICS) { - d_data = t; - } - } - - /** Identical to setData(). */ - BackedStat& operator=(const T& t) { - if(__CVC4_USE_STATISTICS) { - d_data = t; - } - return *this; - } - - /** Get the underlying data value. */ - T getData() const { - return d_data; - } - -};/* class BackedStat */ - - -/** - * A wrapper Stat for another Stat. - * - * This type of Stat is useful in cases where a module (like the - * CongruenceClosure module) might keep its own statistics, but might - * be instantiated in many contexts by many clients. This makes such - * a statistic inappopriate to register with the StatisticsRegistry - * directly, as all would be output with the same name (and may be - * unregistered too quickly anyway). A WrappedStat allows the calling - * client (say, TheoryUF) to wrap the Stat from the client module, - * giving it a globally unique name. - */ -template -class WrappedStat : public ReadOnlyDataStat { - typedef typename Stat::payload_t T; - - const ReadOnlyDataStat& d_stat; - - /** Private copy constructor undefined (no copy permitted). */ - WrappedStat(const WrappedStat&) CVC4_UNDEFINED; - /** Private assignment operator undefined (no copy permitted). */ - WrappedStat& operator=(const WrappedStat&) CVC4_UNDEFINED; - -public: - - /** - * Construct a wrapped statistic with the given name that wraps the - * given statistic. - */ - WrappedStat(const std::string& name, const ReadOnlyDataStat& stat) : - ReadOnlyDataStat(name), - d_stat(stat) { - } - - /** Get the data of the underlying (wrapped) statistic. */ - T getData() const { - return d_stat.getData(); - } - - SExpr getValue() const { - return d_stat.getValue(); - } - -};/* class WrappedStat */ - -/** - * A backed integer-valued (64-bit signed) statistic. - * This doesn't functionally differ from its base class BackedStat, - * except for adding convenience functions for dealing with integers. - */ -class IntStat : public BackedStat { -public: - - /** - * Construct an integer-valued statistic with the given name and - * initial value. - */ - IntStat(const std::string& name, int64_t init) : - BackedStat(name, init) { - } - - /** Increment the underlying integer statistic. */ - IntStat& operator++() { - if(__CVC4_USE_STATISTICS) { - ++d_data; - } - return *this; - } - - /** Increment the underlying integer statistic by the given amount. */ - IntStat& operator+=(int64_t val) { - if(__CVC4_USE_STATISTICS) { - d_data += val; - } - return *this; - } - - /** Keep the maximum of the current statistic value and the given one. */ - void maxAssign(int64_t val) { - if(__CVC4_USE_STATISTICS) { - if(d_data < val) { - d_data = val; - } - } - } - - /** Keep the minimum of the current statistic value and the given one. */ - void minAssign(int64_t val) { - if(__CVC4_USE_STATISTICS) { - if(d_data > val) { - d_data = val; - } - } - } - - SExpr getValue() const { - return SExpr(Integer(d_data)); - } - -};/* class IntStat */ - -template -class SizeStat : public Stat { -private: - const T& d_sized; -public: - SizeStat(const std::string&name, const T& sized) : - Stat(name), d_sized(sized) {} - ~SizeStat() {} - - void flushInformation(std::ostream& out) const { - out << d_sized.size(); - } - - SExpr getValue() const { - return SExpr(Integer(d_sized.size())); - } - -};/* class SizeStat */ - -/** - * The value for an AverageStat is the running average of (e1, e_2, ..., e_n), - * (e1 + e_2 + ... + e_n)/n, - * where e_i is an entry added by an addEntry(e_i) call. - * The value is initially always 0. - * (This is to avoid making parsers confused.) - * - * A call to setData() will change the running average but not reset the - * running count, so should generally be avoided. Call addEntry() to add - * an entry to the average calculation. - */ -class AverageStat : public BackedStat { -private: - /** - * The number of accumulations of the running average that we - * have seen so far. - */ - uint32_t d_count; - double d_sum; - -public: - /** Construct an average statistic with the given name. */ - AverageStat(const std::string& name) : - BackedStat(name, 0.0), d_count(0), d_sum(0.0) { - } - - /** Add an entry to the running-average calculation. */ - void addEntry(double e) { - if(__CVC4_USE_STATISTICS) { - ++d_count; - d_sum += e; - setData(d_sum / d_count); - } - } - - SExpr getValue() const { - std::stringstream ss; - ss << std::fixed << std::setprecision(8) << d_data; - return SExpr(Rational::fromDecimal(ss.str())); - } - -};/* class AverageStat */ - -/** A statistic that contains a SExpr. */ -class SExprStat : public Stat { -private: - SExpr d_data; - -public: - - /** - * Construct a SExpr-valued statistic with the given name and - * initial value. - */ - SExprStat(const std::string& name, const SExpr& init) : - Stat(name), d_data(init){} - - virtual void flushInformation(std::ostream& out) const { - out << d_data << std::endl; - } - - SExpr getValue() const { - return d_data; - } - -};/* class SExprStat */ - -template -class ListStat : public Stat { -private: - typedef std::vector List; - List d_list; -public: - - /** - * Construct an integer-valued statistic with the given name and - * initial value. - */ - ListStat(const std::string& name) : Stat(name) {} - ~ListStat() {} - - void flushInformation(std::ostream& out) const{ - if(__CVC4_USE_STATISTICS) { - typename List::const_iterator i = d_list.begin(), end = d_list.end(); - out << "["; - if(i != end){ - out << *i; - ++i; - for(; i != end; ++i){ - out << ", " << *i; - } - } - out << "]"; - } - } - - ListStat& operator<<(const T& val){ - if(__CVC4_USE_STATISTICS) { - d_list.push_back(val); - } - return (*this); - } - -};/* class ListStat */ - -template -class HistogramStat : public Stat { -private: - typedef std::map Histogram; - Histogram d_hist; -public: - - /** Construct a histogram of a stream of entries. */ - HistogramStat(const std::string& name) : Stat(name) {} - ~HistogramStat() {} - - void flushInformation(std::ostream& out) const{ - if(__CVC4_USE_STATISTICS) { - typename Histogram::const_iterator i = d_hist.begin(); - typename Histogram::const_iterator end = d_hist.end(); - out << "["; - while(i != end){ - const T& key = (*i).first; - unsigned int count = (*i).second; - out << "("< v; - for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) { - std::vector w; - w.push_back(SExpr((*i)->getName())); - w.push_back((*i)->getValue()); - v.push_back(SExpr(w)); - } - 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); - - /** Unregister a new statistic */ - 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; - -/** - * A timer statistic. The timer can be started and stopped - * arbitrarily, like a stopwatch; the value of the statistic at the - * end is the accumulated time over all (start,stop) pairs. - */ -class CVC4_PUBLIC TimerStat : public BackedStat { - - // strange: timespec isn't placed in 'std' namespace ?! - /** The last start time of this timer */ - timespec d_start; - - /** Whether this timer is currently running */ - bool d_running; - -public: - - typedef CVC4::CodeTimer CodeTimer; - - /** - * Construct a timer statistic with the given name. Newly-constructed - * timers have a 0.0 value and are not running. - */ - TimerStat(const std::string& name) : - BackedStat< timespec >(name, timespec()), - d_running(false) { - /* timespec is POD and so may not be initialized to zero; - * here, ensure it is */ - d_data.tv_sec = d_data.tv_nsec = 0; - } - - /** Start the timer. */ - void start(); - - /** - * Stop the timer and update the statistic value with the - * accumulated time. - */ - void stop(); - - /** If the timer is currently running */ - bool running() const; - - timespec getData() const; - - SExpr getValue() const; - -};/* class TimerStat */ - -/** - * Utility class to make it easier to call stop() at the end of a - * code block. When constructed, it starts the timer. When - * destructed, it stops the timer. - */ -class CodeTimer { - TimerStat& d_timer; - bool d_reentrant; - - /** Private copy constructor undefined (no copy permitted). */ - CodeTimer(const CodeTimer& timer) CVC4_UNDEFINED; - /** Private assignment operator undefined (no copy permitted). */ - CodeTimer& operator=(const CodeTimer& timer) CVC4_UNDEFINED; - -public: - CodeTimer(TimerStat& timer, bool allow_reentrant = false) : d_timer(timer), d_reentrant(false) { - if(!allow_reentrant || !(d_reentrant = d_timer.running())) { - d_timer.start(); - } - } - ~CodeTimer() { - if(!d_reentrant) { - d_timer.stop(); - } - } -};/* 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 - * better to use the above KEEP_STATISTIC(), which does declaration of - * the member, construction of the statistic, and - * registration/unregistration. This RAII class only does - * registration and unregistration. - */ -class RegisterStatistic { - - 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 - -}/* CVC4 namespace */ - -#endif /* __CVC4__STATISTICS_REGISTRY_H */ 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 #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 #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 #include -#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& 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& explanation); SatValue assertAssumption(SatLiteral lit, bool propagate); - + void popAssumption(); +private: + /* Disable the default constructor. */ + BVMinisatSatSolver() CVC4_UNUSED; + class Statistics { public: + StatisticsRegistry* d_registry; ReferenceStat d_statStarts, d_statDecisions; ReferenceStat d_statRndDecisions, d_statPropagations; ReferenceStat d_statConflicts, d_statClausesLiterals; @@ -131,7 +131,7 @@ public: IntStat d_statCallsToSolve; BackedStat 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 d_statStarts, d_statDecisions; ReferenceStat d_statRndDecisions, d_statPropagations; ReferenceStat d_statConflicts, d_statClausesLiterals; ReferenceStat d_statLearntsLiterals, d_statMaxLiterals; ReferenceStat 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 #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 #include +#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 #include @@ -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 -#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& 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 #include #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 #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 #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 -#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 -#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 #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 -#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& 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* 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* 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* 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(true); d_false = NodeManager::currentNM()->mkConst(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 #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 NodeNodeMap; +typedef __gnu_cxx::hash_map 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 #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 #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 + +#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 #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 #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 #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& 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 #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(true); d_false = NodeManager::currentNM()->mkConst(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 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 #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/util/statistics.cpp b/src/util/statistics.cpp new file mode 100644 index 000000000..371872454 --- /dev/null +++ b/src/util/statistics.cpp @@ -0,0 +1,134 @@ +/********************* */ +/*! \file statistics.cpp + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** 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.h" + +#include + +#include "util/statistics_registry.h" // for details about class Stat + + +namespace CVC4 { + +std::string StatisticsBase::s_regDelim("::"); + +bool StatisticsBase::StatCmp::operator()(const Stat* s1, const Stat* s2) const { + return s1->getName() < s2->getName(); +} + +StatisticsBase::iterator::value_type StatisticsBase::iterator::operator*() const { + return std::make_pair((*d_it)->getName(), (*d_it)->getValue()); +} + +StatisticsBase::StatisticsBase() : + d_prefix(), + d_stats() { +} + +StatisticsBase::StatisticsBase(const StatisticsBase& stats) : + d_prefix(stats.d_prefix), + d_stats() { +} + +StatisticsBase& StatisticsBase::operator=(const StatisticsBase& stats) { + d_prefix = stats.d_prefix; + return *this; +} + +void Statistics::copyFrom(const StatisticsBase& stats) { + // This is ugly, but otherwise we have to introduce a "friend" relation for + // Base to its derived class (really obnoxious). + StatSet::const_iterator i_begin = ((const Statistics*) &stats)->d_stats.begin(); + StatSet::const_iterator i_end = ((const Statistics*) &stats)->d_stats.end(); + for(StatSet::const_iterator i = i_begin; i != i_end; ++i) { + SExprStat* p = new SExprStat((*i)->getName(), (*i)->getValue()); + d_stats.insert(p); + } +} + +void Statistics::clear() { + for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) { + delete *i; + } + d_stats.clear(); +} + +Statistics::Statistics(const StatisticsBase& stats) : + StatisticsBase(stats) { + copyFrom(stats); +} + +Statistics::Statistics(const Statistics& stats) : + StatisticsBase(stats) { + copyFrom(stats); +} + +Statistics::~Statistics() { + clear(); +} + +Statistics& Statistics::operator=(const StatisticsBase& stats) { + clear(); + this->StatisticsBase::operator=(stats); + copyFrom(stats); + + return *this; +} + +Statistics& Statistics::operator=(const Statistics& stats) { + return this->operator=((const StatisticsBase&)stats); +} + +StatisticsBase::const_iterator StatisticsBase::begin() const { + return iterator(d_stats.begin()); +} + +StatisticsBase::const_iterator StatisticsBase::end() const { + return iterator(d_stats.end()); +} + +void StatisticsBase::flushInformation(std::ostream &out) const { +#ifdef CVC4_STATISTICS_ON + for(StatSet::iterator i = d_stats.begin(); + i != d_stats.end(); + ++i) { + Stat* s = *i; + if(d_prefix != "") { + out << d_prefix << s_regDelim; + } + s->flushStat(out); + out << std::endl; + } +#endif /* CVC4_STATISTICS_ON */ +} + +SExpr StatisticsBase::getStatistic(std::string name) const { + SExpr value; + IntStat s(name, 0); + StatSet::iterator i = d_stats.find(&s); + if(i != d_stats.end()) { + return (*i)->getValue(); + } else { + return SExpr(); + } +} + +void StatisticsBase::setPrefix(const std::string& prefix) { + d_prefix = prefix; +} + +}/* CVC4 namespace */ diff --git a/src/util/statistics.h b/src/util/statistics.h new file mode 100644 index 000000000..a0b6ed083 --- /dev/null +++ b/src/util/statistics.h @@ -0,0 +1,129 @@ +/********************* */ +/*! \file statistics.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** 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 "cvc4_public.h" + +#ifndef __CVC4__STATISTICS_H +#define __CVC4__STATISTICS_H + +#include +#include +#include +#include +#include + +#include "util/sexpr.h" + +namespace CVC4 { + +class Stat; + +class CVC4_PUBLIC StatisticsBase { +protected: + + static std::string s_regDelim; + + /** A helper class for comparing two statistics */ + struct StatCmp { + bool operator()(const Stat* s1, const Stat* s2) const; + };/* struct StatisticsRegistry::StatCmp */ + + /** A type for a set of statistics */ + typedef std::set< Stat*, StatCmp > StatSet; + + std::string d_prefix; + + /** The set of statistics in this object */ + StatSet d_stats; + + StatisticsBase(); + StatisticsBase(const StatisticsBase& stats); + StatisticsBase& operator=(const StatisticsBase& stats); + +public: + + virtual ~StatisticsBase() { } + + class CVC4_PUBLIC iterator : public std::iterator< std::input_iterator_tag, std::pair > { + StatSet::iterator d_it; + + iterator(StatSet::iterator it) : d_it(it) { } + + friend class StatisticsBase; + + public: + iterator() : d_it() { } + iterator(const iterator& it) : d_it(it.d_it) { } + value_type operator*() const; + iterator& operator++() { ++d_it; return *this; } + iterator operator++(int) { iterator old = *this; ++d_it; return old; } + bool operator==(const iterator& i) const { return d_it == i.d_it; } + bool operator!=(const iterator& i) const { return d_it != i.d_it; } + };/* class StatisticsBase::iterator */ + + /** An iterator type over a set of statistics. */ + typedef iterator const_iterator; + + /** Set the output prefix for this set of statistics. */ + virtual void setPrefix(const std::string& prefix); + + /** Flush all statistics to the given output stream. */ + void flushInformation(std::ostream& out) const; + + /** Get the value of a named statistic. */ + SExpr getStatistic(std::string name) const; + + /** + * Get an iterator to the beginning of the range of the set of + * statistics. + */ + const_iterator begin() const; + + /** + * Get an iterator to the end of the range of the set of statistics. + */ + const_iterator end() const; + +};/* class StatisticsBase */ + +class CVC4_PUBLIC Statistics : public StatisticsBase { + void clear(); + void copyFrom(const StatisticsBase&); + +public: + + /** + * Override the copy constructor to do a "deep" copy of statistics + * values. + */ + Statistics(const StatisticsBase& stats); + Statistics(const Statistics& stats); + + ~Statistics(); + + /** + * Override the assignment operator to do a "deep" copy of statistics + * values. + */ + Statistics& operator=(const StatisticsBase& stats); + Statistics& operator=(const Statistics& stats); + +};/* class Statistics */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__STATISTICS_H */ diff --git a/src/util/statistics.i b/src/util/statistics.i new file mode 100644 index 000000000..bd3a4eeb9 --- /dev/null +++ b/src/util/statistics.i @@ -0,0 +1,79 @@ +%{ +#include "util/statistics.h" + +#ifdef SWIGJAVA + +#include "bindings/java_iterator_adapter.h" +#include "bindings/java_stream_adapters.h" + +#endif /* SWIGJAVA */ +%} + +%rename(assign) CVC4::Statistics::operator=(const StatisticsBase&); +%rename(assign) CVC4::Statistics::operator=(const Statistics& stats); + +#ifdef SWIGJAVA + +// Instead of StatisticsBase::begin() and end(), create an +// iterator() method on the Java side that returns a Java-style +// Iterator. +%ignore CVC4::StatisticsBase::begin(); +%ignore CVC4::StatisticsBase::end(); +%ignore CVC4::StatisticsBase::begin() const; +%ignore CVC4::StatisticsBase::end() const; +%extend CVC4::StatisticsBase { + CVC4::JavaIteratorAdapter iterator() { + return CVC4::JavaIteratorAdapter(*$self); + } +} + +// StatisticsBase is "iterable" on the Java side +%typemap(javainterfaces) CVC4::StatisticsBase "java.lang.Iterable"; + +// the JavaIteratorAdapter should not be public, and implements Iterator +%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter "class"; +%typemap(javainterfaces) CVC4::JavaIteratorAdapter "java.util.Iterator"; +// add some functions to the Java side (do it here because there's no way to do these in C++) +%typemap(javacode) CVC4::JavaIteratorAdapter " + public void remove() { + throw new java.lang.UnsupportedOperationException(); + } + + public Object[] next() { + if(hasNext()) { + return getNext(); + } else { + throw new java.util.NoSuchElementException(); + } + } +" +// getNext() just allows C++ iterator access from Java-side next(), make it private +%javamethodmodifiers CVC4::JavaIteratorAdapter::getNext() "private"; + +// map the types appropriately. for statistics, the "payload" of the iterator is an Object[]. +// These Object arrays are always of two elements, the first is a String and the second an +// SExpr. (On the C++ side, it is a std::pair.) +%typemap(jni) CVC4::StatisticsBase::const_iterator::value_type "jobjectArray"; +%typemap(jtype) CVC4::StatisticsBase::const_iterator::value_type "java.lang.Object[]"; +%typemap(jstype) CVC4::StatisticsBase::const_iterator::value_type "java.lang.Object[]"; +%typemap(javaout) CVC4::StatisticsBase::const_iterator::value_type { return $jnicall; } +%typemap(out) CVC4::StatisticsBase::const_iterator::value_type { + $result = jenv->NewObjectArray(2, jenv->FindClass("java/lang/Object"), $null); + jenv->SetObjectArrayElement($result, 0, jenv->NewStringUTF($1.first.c_str())); + jclass clazz = jenv->FindClass("edu/nyu/acsys/CVC4/SExpr"); + jmethodID methodid = jenv->GetMethodID(clazz, "", "(JZ)V"); + jenv->SetObjectArrayElement($result, 1, jenv->NewObject(clazz, methodid, reinterpret_cast(new CVC4::SExpr($1.second)), true)); + }; + +#endif /* SWIGJAVA */ + +%include "util/statistics.h" + +#ifdef SWIGJAVA + +%include "bindings/java_iterator_adapter.h" +%include "bindings/java_stream_adapters.h" + +%template(JavaIteratorAdapter_StatisticsBase) CVC4::JavaIteratorAdapter; + +#endif /* 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/util/statistics_registry.h b/src/util/statistics_registry.h new file mode 100644 index 000000000..f4f00e444 --- /dev/null +++ b/src/util/statistics_registry.h @@ -0,0 +1,766 @@ +/********************* */ +/*! \file statistics_registry.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: Tim King + ** Minor contributors (to current version): Kshitij Bansal + ** 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 Statistics utility classes + ** + ** 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" + +#ifndef __CVC4__STATISTICS_REGISTRY_H +#define __CVC4__STATISTICS_REGISTRY_H + +#include + +#include +#include +#include +#include +#include +#include + +#include "base/exception.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 + + +/** + * The base class for all statistics. + * + * This base class keeps the name of the statistic and declares the (pure) + * virtual function flushInformation(). Derived classes must implement + * this function and pass their name to the base class constructor. + * + * This class also (statically) maintains the delimiter used to separate + * the name and the value when statistics are output. + */ +class Stat { +protected: + /** The name of this statistic */ + std::string d_name; + +public: + + /** Nullary constructor, does nothing */ + Stat() { } + + /** + * Construct a statistic with the given name. Debug builds of CVC4 + * will throw an assertion exception if the given name contains the + * statistic delimiter string. + */ + Stat(const std::string& name) throw(CVC4::IllegalArgumentException) : + d_name(name) { + if(__CVC4_USE_STATISTICS) { + CheckArgument(d_name.find(", ") == std::string::npos, name, + "Statistics names cannot include a comma (',')"); + } + } + + /** Destruct a statistic. This base-class version does nothing. */ + virtual ~Stat() {} + + /** + * Flush the value of this statistic to an output stream. Should + * finish the output with an end-of-line character. + */ + virtual void flushInformation(std::ostream& out) const = 0; + + /** + * Flush the name,value pair of this statistic to an output stream. + * Uses the statistic delimiter string between name and value. + * + * May be redefined by a child class + */ + virtual void flushStat(std::ostream& out) const { + if(__CVC4_USE_STATISTICS) { + out << d_name << ", "; + flushInformation(out); + } + } + + /** Get the name of this statistic. */ + const std::string& getName() const { + return d_name; + } + + /** Get the value of this statistic as a string. */ + virtual SExpr getValue() const { + std::stringstream ss; + flushInformation(ss); + return SExpr(ss.str()); + } + +};/* class Stat */ + +// A generic way of making a SExpr from templated stats code. +// for example, the uint64_t version ensures that we create +// Integer-SExprs for ReadOnlyDataStats (like those inside +// Minisat) without having to specialize the entire +// ReadOnlyDataStat class template. +template +inline SExpr mkSExpr(const T& x) { + std::stringstream ss; + ss << x; + return SExpr(ss.str()); +} + +template <> +inline SExpr mkSExpr(const uint64_t& x) { + return SExpr(Integer(x)); +} + +template <> +inline SExpr mkSExpr(const int64_t& x) { + return SExpr(Integer(x)); +} + +template <> +inline SExpr mkSExpr(const int& x) { + return SExpr(Integer(x)); +} + +template <> +inline SExpr mkSExpr(const Integer& x) { + return SExpr(x); +} + +template <> +inline SExpr mkSExpr(const double& x) { + // roundabout way to get a Rational from a double + std::stringstream ss; + ss << std::fixed << std::setprecision(8) << x; + return SExpr(Rational::fromDecimal(ss.str())); +} + +template <> +inline SExpr mkSExpr(const Rational& x) { + return SExpr(x); +} + +/** + * A class to represent a "read-only" data statistic of type T. Adds to + * the Stat base class the pure virtual function getData(), which returns + * type T, and flushInformation(), which outputs the statistic value to an + * output stream (using the same existing stream insertion operator). + * + * Template class T must have stream insertion operation defined: + * std::ostream& operator<<(std::ostream&, const T&) + */ +template +class ReadOnlyDataStat : public Stat { +public: + /** The "payload" type of this data statistic (that is, T). */ + typedef T payload_t; + + /** Construct a read-only data statistic with the given name. */ + ReadOnlyDataStat(const std::string& name) : + Stat(name) { + } + + /** Get the value of the statistic. */ + virtual T getData() const = 0; + + /** Flush the value of the statistic to the given output stream. */ + void flushInformation(std::ostream& out) const { + if(__CVC4_USE_STATISTICS) { + out << getData(); + } + } + + SExpr getValue() const { + return mkSExpr(getData()); + } + +};/* class ReadOnlyDataStat */ + + +/** + * A data statistic class. This class extends a read-only data statistic + * with assignment (the statistic can be set as well as read). This class + * adds to the read-only case a pure virtual function setData(), thus + * providing the basic interface for a data statistic: getData() to get the + * statistic value, and setData() to set it. + * + * As with the read-only data statistic class, template class T must have + * stream insertion operation defined: + * std::ostream& operator<<(std::ostream&, const T&) + */ +template +class DataStat : public ReadOnlyDataStat { +public: + + /** Construct a data statistic with the given name. */ + DataStat(const std::string& name) : + ReadOnlyDataStat(name) { + } + + /** Set the data statistic. */ + virtual void setData(const T&) = 0; + +};/* class DataStat */ + + +/** + * A data statistic that references a data cell of type T, + * implementing getData() by referencing that memory cell, and + * setData() by reassigning the statistic to point to the new + * data cell. The referenced data cell is kept as a const + * reference, meaning the referenced data is never actually + * modified by this class (it must be externally modified for + * a reference statistic to make sense). A common use for + * this type of statistic is to output a statistic that is kept + * outside the statistics package (for example, one that's kept + * by a theory implementation for internal heuristic purposes, + * which is important to keep even if statistics are turned off). + * + * Template class T must have an assignment operator=(). + */ +template +class ReferenceStat : public DataStat { +private: + /** The referenced data cell */ + const T* d_data; + +public: + /** + * Construct a reference stat with the given name and a reference + * to NULL. + */ + ReferenceStat(const std::string& name) : + DataStat(name), + d_data(NULL) { + } + + /** + * Construct a reference stat with the given name and a reference to + * the given data. + */ + ReferenceStat(const std::string& name, const T& data) : + DataStat(name), + d_data(NULL) { + setData(data); + } + + /** Set this reference statistic to refer to the given data cell. */ + void setData(const T& t) { + if(__CVC4_USE_STATISTICS) { + d_data = &t; + } + } + + /** Get the value of the referenced data cell. */ + T getData() const { + return *d_data; + } + +};/* class ReferenceStat */ + + +/** + * A data statistic that keeps a T and sets it with setData(). + * + * Template class T must have an operator=() and a copy constructor. + */ +template +class BackedStat : public DataStat { +protected: + /** The internally-kept statistic value */ + T d_data; + +public: + + /** Construct a backed statistic with the given name and initial value. */ + BackedStat(const std::string& name, const T& init) : + DataStat(name), + d_data(init) { + } + + /** Set the underlying data value to the given value. */ + void setData(const T& t) { + if(__CVC4_USE_STATISTICS) { + d_data = t; + } + } + + /** Identical to setData(). */ + BackedStat& operator=(const T& t) { + if(__CVC4_USE_STATISTICS) { + d_data = t; + } + return *this; + } + + /** Get the underlying data value. */ + T getData() const { + return d_data; + } + +};/* class BackedStat */ + + +/** + * A wrapper Stat for another Stat. + * + * This type of Stat is useful in cases where a module (like the + * CongruenceClosure module) might keep its own statistics, but might + * be instantiated in many contexts by many clients. This makes such + * a statistic inappopriate to register with the StatisticsRegistry + * directly, as all would be output with the same name (and may be + * unregistered too quickly anyway). A WrappedStat allows the calling + * client (say, TheoryUF) to wrap the Stat from the client module, + * giving it a globally unique name. + */ +template +class WrappedStat : public ReadOnlyDataStat { + typedef typename Stat::payload_t T; + + const ReadOnlyDataStat& d_stat; + + /** Private copy constructor undefined (no copy permitted). */ + WrappedStat(const WrappedStat&) CVC4_UNDEFINED; + /** Private assignment operator undefined (no copy permitted). */ + WrappedStat& operator=(const WrappedStat&) CVC4_UNDEFINED; + +public: + + /** + * Construct a wrapped statistic with the given name that wraps the + * given statistic. + */ + WrappedStat(const std::string& name, const ReadOnlyDataStat& stat) : + ReadOnlyDataStat(name), + d_stat(stat) { + } + + /** Get the data of the underlying (wrapped) statistic. */ + T getData() const { + return d_stat.getData(); + } + + SExpr getValue() const { + return d_stat.getValue(); + } + +};/* class WrappedStat */ + +/** + * A backed integer-valued (64-bit signed) statistic. + * This doesn't functionally differ from its base class BackedStat, + * except for adding convenience functions for dealing with integers. + */ +class IntStat : public BackedStat { +public: + + /** + * Construct an integer-valued statistic with the given name and + * initial value. + */ + IntStat(const std::string& name, int64_t init) : + BackedStat(name, init) { + } + + /** Increment the underlying integer statistic. */ + IntStat& operator++() { + if(__CVC4_USE_STATISTICS) { + ++d_data; + } + return *this; + } + + /** Increment the underlying integer statistic by the given amount. */ + IntStat& operator+=(int64_t val) { + if(__CVC4_USE_STATISTICS) { + d_data += val; + } + return *this; + } + + /** Keep the maximum of the current statistic value and the given one. */ + void maxAssign(int64_t val) { + if(__CVC4_USE_STATISTICS) { + if(d_data < val) { + d_data = val; + } + } + } + + /** Keep the minimum of the current statistic value and the given one. */ + void minAssign(int64_t val) { + if(__CVC4_USE_STATISTICS) { + if(d_data > val) { + d_data = val; + } + } + } + + SExpr getValue() const { + return SExpr(Integer(d_data)); + } + +};/* class IntStat */ + +template +class SizeStat : public Stat { +private: + const T& d_sized; +public: + SizeStat(const std::string&name, const T& sized) : + Stat(name), d_sized(sized) {} + ~SizeStat() {} + + void flushInformation(std::ostream& out) const { + out << d_sized.size(); + } + + SExpr getValue() const { + return SExpr(Integer(d_sized.size())); + } + +};/* class SizeStat */ + +/** + * The value for an AverageStat is the running average of (e1, e_2, ..., e_n), + * (e1 + e_2 + ... + e_n)/n, + * where e_i is an entry added by an addEntry(e_i) call. + * The value is initially always 0. + * (This is to avoid making parsers confused.) + * + * A call to setData() will change the running average but not reset the + * running count, so should generally be avoided. Call addEntry() to add + * an entry to the average calculation. + */ +class AverageStat : public BackedStat { +private: + /** + * The number of accumulations of the running average that we + * have seen so far. + */ + uint32_t d_count; + double d_sum; + +public: + /** Construct an average statistic with the given name. */ + AverageStat(const std::string& name) : + BackedStat(name, 0.0), d_count(0), d_sum(0.0) { + } + + /** Add an entry to the running-average calculation. */ + void addEntry(double e) { + if(__CVC4_USE_STATISTICS) { + ++d_count; + d_sum += e; + setData(d_sum / d_count); + } + } + + SExpr getValue() const { + std::stringstream ss; + ss << std::fixed << std::setprecision(8) << d_data; + return SExpr(Rational::fromDecimal(ss.str())); + } + +};/* class AverageStat */ + +/** A statistic that contains a SExpr. */ +class SExprStat : public Stat { +private: + SExpr d_data; + +public: + + /** + * Construct a SExpr-valued statistic with the given name and + * initial value. + */ + SExprStat(const std::string& name, const SExpr& init) : + Stat(name), d_data(init){} + + virtual void flushInformation(std::ostream& out) const { + out << d_data << std::endl; + } + + SExpr getValue() const { + return d_data; + } + +};/* class SExprStat */ + +template +class ListStat : public Stat { +private: + typedef std::vector List; + List d_list; +public: + + /** + * Construct an integer-valued statistic with the given name and + * initial value. + */ + ListStat(const std::string& name) : Stat(name) {} + ~ListStat() {} + + void flushInformation(std::ostream& out) const{ + if(__CVC4_USE_STATISTICS) { + typename List::const_iterator i = d_list.begin(), end = d_list.end(); + out << "["; + if(i != end){ + out << *i; + ++i; + for(; i != end; ++i){ + out << ", " << *i; + } + } + out << "]"; + } + } + + ListStat& operator<<(const T& val){ + if(__CVC4_USE_STATISTICS) { + d_list.push_back(val); + } + return (*this); + } + +};/* class ListStat */ + +template +class HistogramStat : public Stat { +private: + typedef std::map Histogram; + Histogram d_hist; +public: + + /** Construct a histogram of a stream of entries. */ + HistogramStat(const std::string& name) : Stat(name) {} + ~HistogramStat() {} + + void flushInformation(std::ostream& out) const{ + if(__CVC4_USE_STATISTICS) { + typename Histogram::const_iterator i = d_hist.begin(); + typename Histogram::const_iterator end = d_hist.end(); + out << "["; + while(i != end){ + const T& key = (*i).first; + unsigned int count = (*i).second; + out << "("< v; + for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) { + std::vector w; + w.push_back(SExpr((*i)->getName())); + w.push_back((*i)->getValue()); + v.push_back(SExpr(w)); + } + return SExpr(v); + } + + /** Register a new statistic */ + void registerStat(Stat* s) throw(CVC4::IllegalArgumentException); + + /** Unregister a new statistic */ + void unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException); + +};/* class StatisticsRegistry */ + +class CodeTimer; + +/** + * A timer statistic. The timer can be started and stopped + * arbitrarily, like a stopwatch; the value of the statistic at the + * end is the accumulated time over all (start,stop) pairs. + */ +class CVC4_PUBLIC TimerStat : public BackedStat { + + // strange: timespec isn't placed in 'std' namespace ?! + /** The last start time of this timer */ + timespec d_start; + + /** Whether this timer is currently running */ + bool d_running; + +public: + + typedef CVC4::CodeTimer CodeTimer; + + /** + * Construct a timer statistic with the given name. Newly-constructed + * timers have a 0.0 value and are not running. + */ + TimerStat(const std::string& name) : + BackedStat< timespec >(name, timespec()), + d_running(false) { + /* timespec is POD and so may not be initialized to zero; + * here, ensure it is */ + d_data.tv_sec = d_data.tv_nsec = 0; + } + + /** Start the timer. */ + void start(); + + /** + * Stop the timer and update the statistic value with the + * accumulated time. + */ + void stop(); + + /** If the timer is currently running */ + bool running() const; + + timespec getData() const; + + SExpr getValue() const; + +};/* class TimerStat */ + +/** + * Utility class to make it easier to call stop() at the end of a + * code block. When constructed, it starts the timer. When + * destructed, it stops the timer. + */ +class CodeTimer { + TimerStat& d_timer; + bool d_reentrant; + + /** Private copy constructor undefined (no copy permitted). */ + CodeTimer(const CodeTimer& timer) CVC4_UNDEFINED; + /** Private assignment operator undefined (no copy permitted). */ + CodeTimer& operator=(const CodeTimer& timer) CVC4_UNDEFINED; + +public: + CodeTimer(TimerStat& timer, bool allow_reentrant = false) : d_timer(timer), d_reentrant(false) { + if(!allow_reentrant || !(d_reentrant = d_timer.running())) { + d_timer.start(); + } + } + ~CodeTimer() { + if(!d_reentrant) { + d_timer.stop(); + } + } +};/* class CodeTimer */ + +/** + * 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 + * better to use the above KEEP_STATISTIC(), which does declaration of + * the member, construction of the statistic, and + * registration/unregistration. This RAII class only does + * registration and unregistration. + */ +class CVC4_PUBLIC RegisterStatistic { +public: + RegisterStatistic(StatisticsRegistry* reg, Stat* stat); + ~RegisterStatistic(); + +private: + StatisticsRegistry* d_reg; + Stat* d_stat; + +};/* class RegisterStatistic */ + +#undef __CVC4_USE_STATISTICS + +}/* CVC4 namespace */ + +#endif /* __CVC4__STATISTICS_REGISTRY_H */ 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 #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 #include -#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: