From f4ef7af0a2295691f281ee1604dfeb4082fe229c Mon Sep 17 00:00:00 2001 From: Tim King Date: Fri, 8 Jan 2016 16:44:57 -0800 Subject: 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. --- src/expr/statistics_registry.cpp | 176 --------------------------------------- 1 file changed, 176 deletions(-) delete mode 100644 src/expr/statistics_registry.cpp (limited to 'src/expr/statistics_registry.cpp') 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 -- cgit v1.2.3