diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/Makefile.am | 14 | ||||
-rw-r--r-- | src/expr/expr_manager_template.cpp | 14 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 13 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 2 | ||||
-rw-r--r-- | src/expr/statistics.cpp | 133 | ||||
-rw-r--r-- | src/expr/statistics.h | 129 | ||||
-rw-r--r-- | src/expr/statistics.i | 79 | ||||
-rw-r--r-- | src/expr/statistics_registry.cpp | 176 | ||||
-rw-r--r-- | src/expr/statistics_registry.h | 924 |
9 files changed, 7 insertions, 1477 deletions
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 5c046c282..4648ed3af 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -3,23 +3,10 @@ AM_CPPFLAGS = \ -I@builddir@/.. -I@srcdir@/../include -I@srcdir@/.. AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -#noinst_LTLIBRARIES = libexpr.la libstatistics.la noinst_LTLIBRARIES = libexpr.la -# libstatistics_la_CPPFLAGS = $(CPPFLAGS) $(AM_CPPFLAGS) -D__BUILDING_STATISTICS_FOR_EXPORT -# libstatistics_la_SOURCES = \ -# statistics_registry.h \ -# statistics_registry.cpp - -# EXTRA_libstatistics_la_DEPENDENCIES = \ -# builts - # For some reason statistics were in libutil. No idea why though. libexpr_la_SOURCES = \ - statistics.cpp \ - statistics.h \ - statistics_registry.cpp \ - statistics_registry.h \ array.h \ array_store_all.cpp \ array_store_all.h \ @@ -102,7 +89,6 @@ EXTRA_DIST = \ expr_stream.i \ expr_manager.i \ symbol_table.i \ - statistics.i \ type.i \ kind.i \ expr.i \ diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 59f423e3c..0b9557cc8 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -19,9 +19,9 @@ #include <map> #include "expr/node_manager.h" -#include "expr/statistics_registry.h" #include "expr/variable_type_map.h" #include "options/options.h" +#include "util/statistics_registry.h" ${includes} @@ -38,7 +38,7 @@ ${includes} stringstream statName; \ statName << "expr::ExprManager::" << kind; \ d_exprStatistics[kind] = new IntStat(statName.str(), 0); \ - d_nodeManager->getStatisticsRegistry()->registerStat_(d_exprStatistics[kind]); \ + d_nodeManager->getStatisticsRegistry()->registerStat(d_exprStatistics[kind]); \ } \ ++ *(d_exprStatistics[kind]); \ } @@ -54,7 +54,7 @@ ${includes} statName << "expr::ExprManager::" << ((bound_var) ? "BOUND_VARIABLE" : "VARIABLE") << ":" << type; \ } \ d_exprStatisticsVars[type] = new IntStat(statName.str(), 0); \ - d_nodeManager->getStatisticsRegistry()->registerStat_(d_exprStatisticsVars[type]); \ + d_nodeManager->getStatisticsRegistry()->registerStat(d_exprStatisticsVars[type]); \ } \ ++ *(d_exprStatisticsVars[type]); \ } @@ -100,14 +100,14 @@ ExprManager::~ExprManager() throw() { #ifdef CVC4_STATISTICS_ON for (unsigned i = 0; i < kind::LAST_KIND; ++ i) { if (d_exprStatistics[i] != NULL) { - d_nodeManager->getStatisticsRegistry()->unregisterStat_(d_exprStatistics[i]); + d_nodeManager->getStatisticsRegistry()->unregisterStat(d_exprStatistics[i]); delete d_exprStatistics[i]; d_exprStatistics[i] = NULL; } } for (unsigned i = 0; i < LAST_TYPE; ++ i) { if (d_exprStatisticsVars[i] != NULL) { - d_nodeManager->getStatisticsRegistry()->unregisterStat_(d_exprStatisticsVars[i]); + d_nodeManager->getStatisticsRegistry()->unregisterStat(d_exprStatisticsVars[i]); delete d_exprStatisticsVars[i]; d_exprStatisticsVars[i] = NULL; } @@ -123,10 +123,6 @@ ExprManager::~ExprManager() throw() { } } -StatisticsRegistry* ExprManager::getStatisticsRegistry() throw() { - return d_nodeManager->getStatisticsRegistry(); -} - const Options& ExprManager::getOptions() const { return d_nodeManager->getOptions(); } diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 31983d5a9..e65cfc358 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -24,7 +24,7 @@ #include "expr/expr.h" #include "expr/kind.h" #include "expr/type.h" -#include "expr/statistics.h" +#include "util/statistics.h" #include "util/subrange_bound.h" ${includes} @@ -43,7 +43,6 @@ class NodeManager; class Options; class IntStat; struct ExprManagerMapCollection; -class StatisticsRegistry; class ResourceManager; namespace expr { @@ -52,10 +51,6 @@ namespace expr { }/* CVC4::expr::pickle namespace */ }/* CVC4::expr namespace */ -namespace stats { - StatisticsRegistry* getStatisticsRegistry(ExprManager*); -}/* CVC4::stats namespace */ - class CVC4_PUBLIC ExprManager { private: /** The internal node manager */ @@ -88,12 +83,6 @@ private: /** NodeManager reaches in to get the NodeManager */ friend class NodeManager; - /** Statistics reach in to get the StatisticsRegistry */ - friend ::CVC4::StatisticsRegistry* ::CVC4::stats::getStatisticsRegistry(ExprManager*); - - /** Get the underlying statistics registry. */ - StatisticsRegistry* getStatisticsRegistry() throw(); - // undefined, private copy constructor and assignment op (disallow copy) ExprManager(const ExprManager&) CVC4_UNDEFINED; ExprManager& operator=(const ExprManager&) CVC4_UNDEFINED; diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index c9e6866d4..4cb75bfc7 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -30,7 +30,7 @@ #include "options/options.h" #include "options/smt_options.h" #include "expr/resource_manager.h" -#include "expr/statistics_registry.h" +#include "util/statistics_registry.h" using namespace std; diff --git a/src/expr/statistics.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 <typeinfo> - -#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 <iterator> -#include <ostream> -#include <set> -#include <string> -#include <utility> - -#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<std::string, SExpr> > { - 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<CVC4::StatisticsBase> iterator() { - return CVC4::JavaIteratorAdapter<CVC4::StatisticsBase>(*$self); - } -} - -// StatisticsBase is "iterable" on the Java side -%typemap(javainterfaces) CVC4::StatisticsBase "java.lang.Iterable<Object[]>"; - -// the JavaIteratorAdapter should not be public, and implements Iterator -%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase> "class"; -%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase> "java.util.Iterator<Object[]>"; -// add some functions to the Java side (do it here because there's no way to do these in C++) -%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase> " - 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<CVC4::StatisticsBase>::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<std::string, SExpr>.) -%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, "<init>", "(JZ)V"); - jenv->SetObjectArrayElement($result, 1, jenv->NewObject(clazz, methodid, reinterpret_cast<long>(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<CVC4::StatisticsBase>; - -#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 <stdint.h> - -#include <cassert> -#include <ctime> -#include <iomanip> -#include <map> -#include <sstream> -#include <vector> - -#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 <class T> -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 T> -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<T> */ - - -/** - * 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 T> -class DataStat : public ReadOnlyDataStat<T> { -public: - - /** Construct a data statistic with the given name. */ - DataStat(const std::string& name) : - ReadOnlyDataStat<T>(name) { - } - - /** Set the data statistic. */ - virtual void setData(const T&) = 0; - -};/* class DataStat<T> */ - - -/** - * 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 T> -class ReferenceStat : public DataStat<T> { -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<T>(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<T>(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<T> */ - - -/** - * 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 T> -class BackedStat : public DataStat<T> { -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<T>(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<T>& 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<T> */ - - -/** - * 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 Stat> -class WrappedStat : public ReadOnlyDataStat<typename Stat::payload_t> { - typedef typename Stat::payload_t T; - - const ReadOnlyDataStat<T>& d_stat; - - /** Private copy constructor undefined (no copy permitted). */ - WrappedStat(const WrappedStat&) CVC4_UNDEFINED; - /** Private assignment operator undefined (no copy permitted). */ - WrappedStat<T>& 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<T>& stat) : - ReadOnlyDataStat<T>(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<T> */ - -/** - * A backed integer-valued (64-bit signed) statistic. - * This doesn't functionally differ from its base class BackedStat<int64_t>, - * except for adding convenience functions for dealing with integers. - */ -class IntStat : public BackedStat<int64_t> { -public: - - /** - * Construct an integer-valued statistic with the given name and - * initial value. - */ - IntStat(const std::string& name, int64_t init) : - BackedStat<int64_t>(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 T> -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<double> { -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<double>(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 T> -class ListStat : public Stat { -private: - typedef std::vector<T> 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 T> -class HistogramStat : public Stat { -private: - typedef std::map<T, unsigned int> 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 << "("<<key<<" : "<<count<< ")"; - ++i; - if(i != end){ - out << ", "; - } - } - out << "]"; - } - } - - HistogramStat& operator<<(const T& val){ - if(__CVC4_USE_STATISTICS) { - if(d_hist.find(val) == d_hist.end()){ - d_hist.insert(std::make_pair(val,0)); - } - d_hist[val]++; - } - return (*this); - } - -};/* class HistogramStat */ - -/****************************************************************************/ -/* Statistics Registry */ -/****************************************************************************/ - -/** - * The main statistics registry. This registry maintains the list of - * currently active statistics and is able to "flush" them all. - */ -class CVC4_PUBLIC StatisticsRegistry : public StatisticsBase, public Stat { -private: - - /** Private copy constructor undefined (no copy permitted). */ - StatisticsRegistry(const StatisticsRegistry&) CVC4_UNDEFINED; - -public: - - /** Construct an nameless statistics registry */ - StatisticsRegistry() {} - - /** Construct a statistics registry */ - StatisticsRegistry(const std::string& name) - throw(CVC4::IllegalArgumentException); - - /** - * Set the name of this statistic registry, used as prefix during - * output. (This version overrides StatisticsBase::setPrefix().) - */ - void setPrefix(const std::string& name) { - d_prefix = d_name = name; - } - -#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) - /** Get a pointer to the current statistics registry */ - static StatisticsRegistry* current(); -#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) */ - - /** Overridden to avoid the name being printed */ - void flushStat(std::ostream &out) const; - - virtual void flushInformation(std::ostream& out) const; - - SExpr getValue() const { - std::vector<SExpr> v; - for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) { - std::vector<SExpr> 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<timespec> { - - // 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 */ |