diff options
Diffstat (limited to 'src/expr/statistics_registry.cpp')
-rw-r--r-- | src/expr/statistics_registry.cpp | 168 |
1 files changed, 168 insertions, 0 deletions
diff --git a/src/expr/statistics_registry.cpp b/src/expr/statistics_registry.cpp new file mode 100644 index 000000000..c1db992c5 --- /dev/null +++ b/src/expr/statistics_registry.cpp @@ -0,0 +1,168 @@ +/********************* */ +/*! \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 "expr/expr_manager.h" +#include "lib/clock_gettime.h" +#include "smt/smt_engine.h" + +#ifndef __BUILDING_STATISTICS_FOR_EXPORT +# include "smt/smt_engine_scope.h" +#endif /* ! __BUILDING_STATISTICS_FOR_EXPORT */ + +#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 { + +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 */ + +#ifndef __BUILDING_STATISTICS_FOR_EXPORT + +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; + CheckArgument(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; + CheckArgument(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() */ + +#endif /* ! __BUILDING_STATISTICS_FOR_EXPORT */ + +void StatisticsRegistry::registerStat_(Stat* s) throw(CVC4::IllegalArgumentException) { +#ifdef CVC4_STATISTICS_ON + CheckArgument(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 + CheckArgument(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) { + CheckArgument(!d_running, *this, "timer already running"); + clock_gettime(CLOCK_MONOTONIC, &d_start); + d_running = true; + } +}/* TimerStat::start() */ + +void TimerStat::stop() { + if(__CVC4_USE_STATISTICS) { + CheckArgument(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 |