diff options
Diffstat (limited to 'src/util')
| -rw-r--r-- | src/util/Makefile.am | 17 | ||||
| -rw-r--r-- | src/util/sexpr.h | 31 | ||||
| -rw-r--r-- | src/util/statistics.cpp | 134 | ||||
| -rw-r--r-- | src/util/statistics.h | 129 | ||||
| -rw-r--r-- | src/util/statistics.i | 6 | ||||
| -rw-r--r-- | src/util/statistics_registry.cpp (renamed from src/util/stats.cpp) | 98 | ||||
| -rw-r--r-- | src/util/statistics_registry.h (renamed from src/util/stats.h) | 253 | ||||
| -rw-r--r-- | src/util/stats.i | 30 |
8 files changed, 504 insertions, 194 deletions
diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 7d3664d47..7d9a055fd 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -3,13 +3,15 @@ AM_CPPFLAGS = \ -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -noinst_LTLIBRARIES = libutil.la libutilcudd.la +noinst_LTLIBRARIES = libutil.la libutilcudd.la libstatistics.la # libutilcudd.la is a separate library so that we can pass separate # compiler flags libutilcudd_la_CPPFLAGS = $(CPPFLAGS) $(AM_CPPFLAGS) @CUDD_CPPFLAGS@ libutilcudd_la_LIBADD = @CUDD_LDFLAGS@ @CUDD_LIBS@ +libstatistics_la_CPPFLAGS = $(CPPFLAGS) $(AM_CPPFLAGS) -D__BUILDING_STATISTICS_FOR_EXPORT + # Do not list built sources (like integer.h, rational.h, and tls.h) here! # Rather, list them under BUILT_SOURCES, and their .in versions under # EXTRA_DIST. Otherwise, they're packaged up in the tarball, which is @@ -44,8 +46,10 @@ libutil_la_SOURCES = \ gmp_util.h \ sexpr.h \ sexpr.cpp \ - stats.h \ - stats.cpp \ + statistics.h \ + statistics.cpp \ + statistics_registry.h \ + statistics_registry.cpp \ dynamic_array.h \ language.h \ lemma_input_channel.h \ @@ -81,6 +85,11 @@ libutil_la_SOURCES = \ libutil_la_LIBADD = \ @builddir@/libutilcudd.la + +libstatistics_la_SOURCES = \ + statistics_registry.h \ + statistics_registry.cpp + libutilcudd_la_SOURCES = \ propositional_query.h \ propositional_query.cpp @@ -110,7 +119,7 @@ EXTRA_DIST = \ integer.h.in \ tls.h.in \ integer.i \ - stats.i \ + statistics.i \ bool.i \ sexpr.i \ datatype.i \ diff --git a/src/util/sexpr.h b/src/util/sexpr.h index 0734dec6c..4feffc18f 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -23,6 +23,8 @@ #include <vector> #include <string> +#include <iomanip> +#include <sstream> #include "util/integer.h" #include "util/rational.h" @@ -151,6 +153,12 @@ public: */ const std::vector<SExpr>& getChildren() const; + /** Is this S-expression equal to another? */ + bool operator==(const SExpr& s) const; + + /** Is this S-expression different from another? */ + bool operator!=(const SExpr& s) const; + };/* class SExpr */ inline bool SExpr::isAtom() const { @@ -178,8 +186,15 @@ inline std::string SExpr::getValue() const { switch(d_sexprType) { case SEXPR_INTEGER: return d_integerValue.toString(); - case SEXPR_RATIONAL: - return d_rationalValue.toString(); + case SEXPR_RATIONAL: { + // We choose to represent rationals as decimal strings rather than + // "numerator/denominator." Perhaps an additional SEXPR_DECIMAL + // could be added if we need both styles, even if it's backed by + // the same Rational object. + std::stringstream ss; + ss << std::fixed << d_rationalValue.getDouble(); + return ss.str(); + } case SEXPR_STRING: case SEXPR_KEYWORD: return d_stringValue; @@ -204,6 +219,18 @@ inline const std::vector<SExpr>& SExpr::getChildren() const { return d_children; } +inline bool SExpr::operator==(const SExpr& s) const { + return d_sexprType == s.d_sexprType && + d_integerValue == s.d_integerValue && + d_rationalValue == s.d_rationalValue && + d_stringValue == s.d_stringValue && + d_children == s.d_children; +} + +inline bool SExpr::operator!=(const SExpr& s) const { + return !(*this == s); +} + std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) CVC4_PUBLIC; }/* CVC4 namespace */ diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp new file mode 100644 index 000000000..bc6bcb53d --- /dev/null +++ b/src/util/statistics.cpp @@ -0,0 +1,134 @@ +/********************* */ +/*! \file statistics.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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 "util/statistics_registry.h" // for details about class Stat + +#include <typeinfo> + +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..e04db5846 --- /dev/null +++ b/src/util/statistics.h @@ -0,0 +1,129 @@ +/********************* */ +/*! \file statistics.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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 "util/sexpr.h" + +#include <string> +#include <ostream> +#include <set> +#include <iterator> +#include <utility> + +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: + 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..7cc737d6c --- /dev/null +++ b/src/util/statistics.i @@ -0,0 +1,6 @@ +%{ +#include "util/statistics.h" +%} + +%include "util/statistics.h" + diff --git a/src/util/stats.cpp b/src/util/statistics_registry.cpp index 7ac430da8..f2a698a48 100644 --- a/src/util/stats.cpp +++ b/src/util/statistics_registry.cpp @@ -1,11 +1,11 @@ /********************* */ -/*! \file stats.cpp +/*! \file statistics_registry.cpp ** \verbatim ** Original author: taking ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -17,7 +17,7 @@ ** \todo document this file **/ -#include "util/stats.h" +#include "util/statistics_registry.h" #include "expr/node_manager.h" #include "expr/expr_manager_scope.h" #include "expr/expr_manager.h" @@ -31,83 +31,70 @@ # define __CVC4_USE_STATISTICS false #endif -using namespace CVC4; +namespace CVC4 { -std::string Stat::s_delim(","); -std::string StatisticsRegistry::s_regDelim("::"); +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; +} + +}/* CVC4::stats namespace */ + +#ifndef __BUILDING_STATISTICS_FOR_EXPORT StatisticsRegistry* StatisticsRegistry::current() { - return smt::currentSmtEngine()->getStatisticsRegistry(); + return stats::getStatisticsRegistry(smt::currentSmtEngine()); } void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) { #ifdef CVC4_STATISTICS_ON - StatSet& registeredStats = current()->d_registeredStats; - AlwaysAssert(registeredStats.find(s) == registeredStats.end(), + StatSet& stats = current()->d_stats; + AlwaysAssert(stats.find(s) == stats.end(), "Statistic `%s' was already registered with this registry.", s->getName().c_str()); - registeredStats.insert(s); + stats.insert(s); #endif /* CVC4_STATISTICS_ON */ }/* StatisticsRegistry::registerStat() */ -void StatisticsRegistry::registerStat_(Stat* s) throw(AssertionException) { -#ifdef CVC4_STATISTICS_ON - AlwaysAssert(d_registeredStats.find(s) == d_registeredStats.end()); - d_registeredStats.insert(s); -#endif /* CVC4_STATISTICS_ON */ -}/* StatisticsRegistry::registerStat_() */ - void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) { #ifdef CVC4_STATISTICS_ON - StatSet& registeredStats = current()->d_registeredStats; - AlwaysAssert(registeredStats.find(s) != registeredStats.end(), + StatSet& stats = current()->d_stats; + AlwaysAssert(stats.find(s) != stats.end(), "Statistic `%s' was not registered with this registry.", s->getName().c_str()); - registeredStats.erase(s); + stats.erase(s); #endif /* CVC4_STATISTICS_ON */ }/* StatisticsRegistry::unregisterStat() */ -void StatisticsRegistry::unregisterStat_(Stat* s) throw(AssertionException) { +#endif /* ! __BUILDING_STATISTICS_FOR_EXPORT */ + +void StatisticsRegistry::registerStat_(Stat* s) throw(AssertionException) { #ifdef CVC4_STATISTICS_ON - AlwaysAssert(d_registeredStats.find(s) != d_registeredStats.end()); - d_registeredStats.erase(s); + AlwaysAssert(d_stats.find(s) == d_stats.end()); + d_stats.insert(s); #endif /* CVC4_STATISTICS_ON */ -}/* StatisticsRegistry::unregisterStat_() */ +}/* StatisticsRegistry::registerStat_() */ -void StatisticsRegistry::flushInformation(std::ostream& out) const { +void StatisticsRegistry::unregisterStat_(Stat* s) throw(AssertionException) { #ifdef CVC4_STATISTICS_ON - for(StatSet::iterator i = d_registeredStats.begin(); - i != d_registeredStats.end(); - ++i) { - Stat* s = *i; - if(d_name != "") { - out << d_name << s_regDelim; - } - s->flushStat(out); - out << std::endl; - } + AlwaysAssert(d_stats.find(s) != d_stats.end()); + d_stats.erase(s); #endif /* CVC4_STATISTICS_ON */ -}/* StatisticsRegistry::flushInformation() */ +}/* StatisticsRegistry::unregisterStat_() */ -void StatisticsRegistry::flushStat(std::ostream &out) const {; +void StatisticsRegistry::flushStat(std::ostream &out) const { #ifdef CVC4_STATISTICS_ON flushInformation(out); #endif /* CVC4_STATISTICS_ON */ } -StatisticsRegistry::const_iterator StatisticsRegistry::begin_() const { - return d_registeredStats.begin(); -}/* StatisticsRegistry::begin() */ - -StatisticsRegistry::const_iterator StatisticsRegistry::begin() { - return current()->d_registeredStats.begin(); -}/* StatisticsRegistry::begin() */ - -StatisticsRegistry::const_iterator StatisticsRegistry::end_() const { - return d_registeredStats.end(); -}/* StatisticsRegistry::end() */ - -StatisticsRegistry::const_iterator StatisticsRegistry::end() { - return current()->d_registeredStats.end(); -}/* StatisticsRegistry::end() */ +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) { @@ -128,14 +115,17 @@ void TimerStat::stop() { }/* TimerStat::stop() */ RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) : - d_reg(em.getStatisticsRegistry()), + d_reg(NodeManager::fromExprManager(&em)->getStatisticsRegistry()), d_stat(stat) { d_reg->registerStat_(d_stat); } RegisterStatistic::RegisterStatistic(SmtEngine& smt, Stat* stat) : - d_reg(smt.getStatisticsRegistry()), + d_reg(stats::getStatisticsRegistry(&smt)), d_stat(stat) { d_reg->registerStat_(d_stat); } +}/* CVC4 namespace */ + +#undef __CVC4_USE_STATISTICS diff --git a/src/util/stats.h b/src/util/statistics_registry.h index 082bdfeaa..b2180ab59 100644 --- a/src/util/stats.h +++ b/src/util/statistics_registry.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file stats.h +/*! \file statistics_registry.h ** \verbatim ** Original author: taking - ** Major contributors: mdeters, kshitij + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -18,16 +18,15 @@ ** classes. **/ -#include "cvc4_public.h" +#include "cvc4_private_library.h" -#ifndef __CVC4__STATS_H -#define __CVC4__STATS_H +#ifndef __CVC4__STATISTICS_REGISTRY_H +#define __CVC4__STATISTICS_REGISTRY_H + +#include "util/statistics.h" -#include <string> -#include <ostream> #include <sstream> #include <iomanip> -#include <set> #include <ctime> #include <vector> #include <stdint.h> @@ -45,8 +44,6 @@ namespace CVC4 { class ExprManager; class SmtEngine; -class CVC4_PUBLIC Stat; - /** * The base class for all statistics. * @@ -57,14 +54,7 @@ class CVC4_PUBLIC Stat; * This class also (statically) maintains the delimiter used to separate * the name and the value when statistics are output. */ -class CVC4_PUBLIC Stat { -private: - /** - * The delimiter between name and value to use when outputting a - * statistic. - */ - static std::string s_delim; - +class Stat { protected: /** The name of this statistic */ std::string d_name; @@ -82,7 +72,7 @@ public: Stat(const std::string& name) throw(CVC4::AssertionException) : d_name(name) { if(__CVC4_USE_STATISTICS) { - AlwaysAssert(d_name.find(s_delim) == std::string::npos); + AlwaysAssert(d_name.find(", ") == std::string::npos); } } @@ -103,7 +93,7 @@ public: */ virtual void flushStat(std::ostream& out) const { if(__CVC4_USE_STATISTICS) { - out << d_name << s_delim; + out << d_name << ", "; flushInformation(out); } } @@ -114,7 +104,7 @@ public: } /** Get the value of this statistic as a string. */ - std::string getValue() const { + virtual SExpr getValue() const { std::stringstream ss; flushInformation(ss); return ss.str(); @@ -122,6 +112,51 @@ public: };/* 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 ss.str(); +} + +template <> +inline SExpr mkSExpr(const uint64_t& x) { + return Integer(x); +} + +template <> +inline SExpr mkSExpr(const int64_t& x) { + return Integer(x); +} + +template <> +inline SExpr mkSExpr(const int& x) { + return Integer(x); +} + +template <> +inline SExpr mkSExpr(const Integer& x) { + return x; +} + +template <> +inline SExpr mkSExpr(const double& x) { + // roundabout way to get a Rational from a double + std::stringstream ss; + ss << std::fixed << x; + return Rational::fromDecimal(ss.str()); +} + +template <> +inline SExpr mkSExpr(const Rational& x) { + return 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 @@ -132,7 +167,7 @@ public: * std::ostream& operator<<(std::ostream&, const T&) */ template <class T> -class CVC4_PUBLIC ReadOnlyDataStat : public Stat { +class ReadOnlyDataStat : public Stat { public: /** The "payload" type of this data statistic (that is, T). */ typedef T payload_t; @@ -152,6 +187,10 @@ public: } } + SExpr getValue() const { + return mkSExpr(getData()); + } + };/* class ReadOnlyDataStat<T> */ @@ -167,7 +206,7 @@ public: * std::ostream& operator<<(std::ostream&, const T&) */ template <class T> -class CVC4_PUBLIC DataStat : public ReadOnlyDataStat<T> { +class DataStat : public ReadOnlyDataStat<T> { public: /** Construct a data statistic with the given name. */ @@ -197,7 +236,7 @@ public: * Template class T must have an assignment operator=(). */ template <class T> -class CVC4_PUBLIC ReferenceStat : public DataStat<T> { +class ReferenceStat : public DataStat<T> { private: /** The referenced data cell */ const T* d_data; @@ -247,7 +286,7 @@ public: * Template class T must have an operator=() and a copy constructor. */ template <class T> -class CVC4_PUBLIC BackedStat : public DataStat<T> { +class BackedStat : public DataStat<T> { protected: /** The internally-kept statistic value */ T d_data; @@ -300,7 +339,7 @@ public: * giving it a globally unique name. */ template <class Stat> -class CVC4_PUBLIC WrappedStat : public ReadOnlyDataStat<typename Stat::payload_t> { +class WrappedStat : public ReadOnlyDataStat<typename Stat::payload_t> { typedef typename Stat::payload_t T; const ReadOnlyDataStat<T>& d_stat; @@ -330,6 +369,10 @@ public: } } + SExpr getValue() const { + return d_stat.getValue(); + } + };/* class WrappedStat<T> */ /** @@ -337,7 +380,7 @@ public: * This doesn't functionally differ from its base class BackedStat<int64_t>, * except for adding convenience functions for dealing with integers. */ -class CVC4_PUBLIC IntStat : public BackedStat<int64_t> { +class IntStat : public BackedStat<int64_t> { public: /** @@ -359,7 +402,7 @@ public: /** Increment the underlying integer statistic by the given amount. */ IntStat& operator+=(int64_t val) { if(__CVC4_USE_STATISTICS) { - d_data+= val; + d_data += val; } return *this; } @@ -382,6 +425,10 @@ public: } } + SExpr getValue() const { + return SExpr(Integer(d_data)); + } + };/* class IntStat */ template <class T> @@ -394,13 +441,13 @@ public: ~SizeStat() {} void flushInformation(std::ostream& out) const { - out<< d_sized.size(); + out << d_sized.size(); } - std::string getValue() const { - std::stringstream ss; - flushInformation(ss); - return ss.str(); + + SExpr getValue() const { + return SExpr(Integer(d_sized.size())); } + };/* class SizeStat */ /** @@ -414,7 +461,7 @@ public: * running count, so should generally be avoided. Call addEntry() to add * an entry to the average calculation. */ -class CVC4_PUBLIC AverageStat : public BackedStat<double> { +class AverageStat : public BackedStat<double> { private: /** * The number of accumulations of the running average that we @@ -438,10 +485,34 @@ public: } } + SExpr getValue() const { + std::stringstream ss; + ss << d_data; + return SExpr(Rational::fromDecimal(ss.str())); + } + };/* class AverageStat */ +/** A statistic that contains a SExpr. */ +class SExprStat : public BackedStat<SExpr> { +public: + + /** + * Construct a SExpr-valued statistic with the given name and + * initial value. + */ + SExprStat(const std::string& name, const SExpr& init) : + BackedStat<SExpr>(name, init) { + } + + SExpr getValue() const { + return d_data; + } + +};/* class SExprStat */ + template <class T> -class CVC4_PUBLIC ListStat : public Stat{ +class ListStat : public Stat { private: typedef std::vector<T> List; List d_list; @@ -486,23 +557,12 @@ public: * 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 Stat { +class StatisticsRegistry : public StatisticsBase, public Stat { private: - /** A helper class for comparing two statistics */ - struct StatCmp { - inline bool operator()(const Stat* s1, const Stat* s2) const; - };/* class StatisticsRegistry::StatCmp */ - - /** A type for a set of statistics */ - typedef std::set< Stat*, StatCmp > StatSet; - - /** The set of currently active statistics */ - StatSet d_registeredStats; /** Private copy constructor undefined (no copy permitted). */ StatisticsRegistry(const StatisticsRegistry&) CVC4_UNDEFINED; - static std::string s_regDelim; public: /** Construct an nameless statistics registry */ @@ -511,82 +571,57 @@ public: /** Construct a statistics registry */ StatisticsRegistry(const std::string& name) throw(CVC4::AssertionException) : Stat(name) { + d_prefix = name; if(__CVC4_USE_STATISTICS) { AlwaysAssert(d_name.find(s_regDelim) == std::string::npos); } } - /** + /** * Set the name of this statistic registry, used as prefix during - * output. - * - * TODO: Get rid of this function once we have ability to set the - * name of StatisticsRegistry at creation time. + * output. (This version overrides StatisticsBase::setPrefix().) */ - void setName(const std::string& name) { - d_name = name; + void setPrefix(const std::string& name) { + d_prefix = d_name = name; } - /** An iterator type over a set of statistics */ - typedef StatSet::const_iterator const_iterator; - +#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && !defined(__BUILDING_STATISTICS_FOR_EXPORT) /** Get a pointer to the current statistics registry */ static StatisticsRegistry* current(); - - /** Flush all statistics to the given output stream. */ - void flushInformation(std::ostream& out) const; - - /** Obsolete flushStatistics -- use flushInformation */ - //void flushStatistics(std::ostream& out) const; +#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) && ! __BUILDING_STATISTICS_FOR_EXPORT */ /** 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((*i)->getName()); + w.push_back((*i)->getValue()); + v.push_back(SExpr(w)); + } + return SExpr(v); + } + +#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && !defined(__BUILDING_STATISTICS_FOR_EXPORT) /** Register a new statistic, making it active. */ static void registerStat(Stat* s) throw(AssertionException); - /** Register a new statistic */ - void registerStat_(Stat* s) throw(AssertionException); - /** Unregister an active statistic, making it inactive. */ static void unregisterStat(Stat* s) throw(AssertionException); +#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB) && ! __BUILDING_STATISTICS_FOR_EXPORT */ + + /** Register a new statistic */ + void registerStat_(Stat* s) throw(AssertionException); /** Unregister a new statistic */ void unregisterStat_(Stat* s) throw(AssertionException); - /** - * Get an iterator to the beginning of the range of the set of active - * (registered) statistics. - */ - const_iterator begin_() const; - - /** - * Get an iterator to the beginning of the range of the set of active - * (registered) statistics. This version uses the "current" - * statistics registry. - */ - static const_iterator begin(); - - /** - * Get an iterator to the end of the range of the set of active - * (registered) statistics. - */ - const_iterator end_() const; - - /** - * Get an iterator to the end of the range of the set of active - * (registered) statistics. This version uses the "current" - * statistics registry. - */ - static const_iterator end(); - };/* class StatisticsRegistry */ -inline bool StatisticsRegistry::StatCmp::operator()(const Stat* s1, - const Stat* s2) const { - return s1->getName() < s2->getName(); -} - /****************************************************************************/ /* Some utility functions for timespec */ /****************************************************************************/ @@ -685,21 +720,20 @@ inline bool operator>=(const timespec& a, const timespec& b) { } /** Output a timespec on an output stream. */ -inline std::ostream& operator<<(std::ostream& os, const timespec& t) CVC4_PUBLIC; 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(8) << std::right << t.tv_nsec; } -class CVC4_PUBLIC CodeTimer; +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> { +class TimerStat : public BackedStat<timespec> { // strange: timespec isn't placed in 'std' namespace ?! /** The last start time of this timer */ @@ -733,6 +767,12 @@ public: */ void stop(); + SExpr getValue() const { + std::stringstream ss; + ss << std::fixed << d_data; + return SExpr(Rational::fromDecimal(ss.str())); + } + };/* class TimerStat */ @@ -741,7 +781,7 @@ public: * code block. When constructed, it starts the timer. When * destructed, it stops the timer. */ -class CVC4_PUBLIC CodeTimer { +class CodeTimer { TimerStat& d_timer; /** Private copy constructor undefined (no copy permitted). */ @@ -796,16 +836,21 @@ public: * registration/unregistration. This RAII class only does * registration and unregistration. */ -class CVC4_PUBLIC RegisterStatistic { +class RegisterStatistic { + StatisticsRegistry* d_reg; Stat* d_stat; + public: + +#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && ! defined(__BUILDING_STATISTICS_FOR_EXPORT) RegisterStatistic(Stat* stat) : d_reg(StatisticsRegistry::current()), d_stat(stat) { Assert(d_reg != NULL, "There is no current statistics registry!"); StatisticsRegistry::registerStat(d_stat); } +#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) && ! __BUILDING_STATISTICS_FOR_EXPORT */ RegisterStatistic(StatisticsRegistry* reg, Stat* stat) : d_reg(reg), @@ -830,4 +875,4 @@ public: }/* CVC4 namespace */ -#endif /* __CVC4__STATS_H */ +#endif /* __CVC4__STATISTICS_REGISTRY_H */ diff --git a/src/util/stats.i b/src/util/stats.i deleted file mode 100644 index 6f1ef5367..000000000 --- a/src/util/stats.i +++ /dev/null @@ -1,30 +0,0 @@ -%{ -#include "util/stats.h" -%} - -namespace CVC4 { - template <class T> class CVC4_PUBLIC BackedStat; - - %template(int64_t_BackedStat) BackedStat<int64_t>; - %template(double_BackedStat) BackedStat<double>; - %template(timespec_BackedStat) BackedStat<timespec>; -}/* CVC4 namespace */ - -%ignore CVC4::operator<<(std::ostream&, const timespec&); - -%rename(increment) CVC4::IntStat::operator++(); -%rename(plusAssign) CVC4::IntStat::operator+=(int64_t); - -%rename(plusAssign) CVC4::operator+=(timespec&, const timespec&); -%rename(minusAssign) CVC4::operator-=(timespec&, const timespec&); -%rename(plus) CVC4::operator+(const timespec&, const timespec&); -%rename(minus) CVC4::operator-(const timespec&, const timespec&); -%rename(equals) CVC4::operator==(const timespec&, const timespec&); -%ignore CVC4::operator!=(const timespec&, const timespec&); -%rename(less) CVC4::operator<(const timespec&, const timespec&); -%rename(lessEqual) CVC4::operator<=(const timespec&, const timespec&); -%rename(greater) CVC4::operator>(const timespec&, const timespec&); -%rename(greaterEqual) CVC4::operator>=(const timespec&, const timespec&); - -%include "util/stats.h" - |