src/util/statistics_registry.cpp

   1 /*********************                                                        */
   2 /*! \file statistics_registry.cpp
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: Tim King
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief [[ Add one-line brief description here ]]
  13  **
  14  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17
  18 #include "util/statistics_registry.h"
  19 #include "expr/expr_manager.h"
  20 #include "lib/clock_gettime.h"
  21 #include "smt/smt_engine.h"
  22
  23 #ifndef __BUILDING_STATISTICS_FOR_EXPORT
  24 #  include "smt/smt_engine_scope.h"
  25 #endif /* ! __BUILDING_STATISTICS_FOR_EXPORT */
  26
  27 #ifdef CVC4_STATISTICS_ON
  28 #  define __CVC4_USE_STATISTICS true
  29 #else
  30 #  define __CVC4_USE_STATISTICS false
  31 #endif
  32
  33 namespace CVC4 {
  34
  35 namespace stats {
  36
  37 // This is a friend of SmtEngine, just to reach in and get it.
  38 // this isn't a class function because then there's a cyclic
  39 // dependence.
  40 inline StatisticsRegistry* getStatisticsRegistry(SmtEngine* smt) {
  41   return smt->d_statisticsRegistry;
  42 }
  43
  44 inline StatisticsRegistry* getStatisticsRegistry(ExprManager* em) {
  45   return em->getStatisticsRegistry();
  46 }
  47
  48 }/* CVC4::stats namespace */
  49
  50 #ifndef __BUILDING_STATISTICS_FOR_EXPORT
  51
  52 StatisticsRegistry* StatisticsRegistry::current() {
  53   return stats::getStatisticsRegistry(smt::currentSmtEngine());
  54 }
  55
  56 void StatisticsRegistry::registerStat(Stat* s) throw(CVC4::IllegalArgumentException) {
  57 #ifdef CVC4_STATISTICS_ON
  58   StatSet& stats = current()->d_stats;
  59   CheckArgument(stats.find(s) == stats.end(), s,
  60                 "Statistic `%s' was already registered with this registry.",
  61                 s->getName().c_str());
  62   stats.insert(s);
  63 #endif /* CVC4_STATISTICS_ON */
  64 }/* StatisticsRegistry::registerStat() */
  65
  66 void StatisticsRegistry::unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException) {
  67 #ifdef CVC4_STATISTICS_ON
  68   StatSet& stats = current()->d_stats;
  69   CheckArgument(stats.find(s) != stats.end(), s,
  70                 "Statistic `%s' was not registered with this registry.",
  71                 s->getName().c_str());
  72   stats.erase(s);
  73 #endif /* CVC4_STATISTICS_ON */
  74 }/* StatisticsRegistry::unregisterStat() */
  75
  76 #endif /* ! __BUILDING_STATISTICS_FOR_EXPORT */
  77
  78 void StatisticsRegistry::registerStat_(Stat* s) throw(CVC4::IllegalArgumentException) {
  79 #ifdef CVC4_STATISTICS_ON
  80   CheckArgument(d_stats.find(s) == d_stats.end(), s);
  81   d_stats.insert(s);
  82 #endif /* CVC4_STATISTICS_ON */
  83 }/* StatisticsRegistry::registerStat_() */
  84
  85 void StatisticsRegistry::unregisterStat_(Stat* s) throw(CVC4::IllegalArgumentException) {
  86 #ifdef CVC4_STATISTICS_ON
  87   CheckArgument(d_stats.find(s) != d_stats.end(), s);
  88   d_stats.erase(s);
  89 #endif /* CVC4_STATISTICS_ON */
  90 }/* StatisticsRegistry::unregisterStat_() */
  91
  92 void StatisticsRegistry::flushStat(std::ostream &out) const {
  93 #ifdef CVC4_STATISTICS_ON
  94   flushInformation(out);
  95 #endif /* CVC4_STATISTICS_ON */
  96 }
  97
  98 void StatisticsRegistry::flushInformation(std::ostream &out) const {
  99 #ifdef CVC4_STATISTICS_ON
 100   this->StatisticsBase::flushInformation(out);
 101 #endif /* CVC4_STATISTICS_ON */
 102 }
 103
 104 void TimerStat::start() {
 105   if(__CVC4_USE_STATISTICS) {
 106     CheckArgument(!d_running, *this, "timer already running");
 107     clock_gettime(CLOCK_MONOTONIC, &d_start);
 108     d_running = true;
 109   }
 110 }/* TimerStat::start() */
 111
 112 void TimerStat::stop() {
 113   if(__CVC4_USE_STATISTICS) {
 114     CheckArgument(d_running, *this, "timer not running");
 115     ::timespec end;
 116     clock_gettime(CLOCK_MONOTONIC, &end);
 117     d_data += end - d_start;
 118     d_running = false;
 119   }
 120 }/* TimerStat::stop() */
 121
 122 RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) :
 123   d_reg(stats::getStatisticsRegistry(&em)),
 124   d_stat(stat) {
 125   d_reg->registerStat_(d_stat);
 126 }
 127
 128 RegisterStatistic::RegisterStatistic(SmtEngine& smt, Stat* stat) :
 129   d_reg(stats::getStatisticsRegistry(&smt)),
 130   d_stat(stat) {
 131   d_reg->registerStat_(d_stat);
 132 }
 133
 134 }/* CVC4 namespace */
 135
 136 #undef __CVC4_USE_STATISTICS