f6a27e20d898a5d62c0062692659b992d418eb3f
1 /********************* */
2 /*! \file statistics_registry.cpp
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
12 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
18 #include "util/statistics_registry.h"
19 #include "expr/expr_manager.h"
20 #include "lib/clock_gettime.h"
21 #include "smt/smt_engine.h"
23 #ifndef __BUILDING_STATISTICS_FOR_EXPORT
24 # include "smt/smt_engine_scope.h"
25 #endif /* ! __BUILDING_STATISTICS_FOR_EXPORT */
27 #ifdef CVC4_STATISTICS_ON
28 # define __CVC4_USE_STATISTICS true
30 # define __CVC4_USE_STATISTICS false
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
40 inline StatisticsRegistry
* getStatisticsRegistry(SmtEngine
* smt
) {
41 return smt
->d_statisticsRegistry
;
44 inline StatisticsRegistry
* getStatisticsRegistry(ExprManager
* em
) {
45 return em
->getStatisticsRegistry();
48 }/* CVC4::stats namespace */
50 #ifndef __BUILDING_STATISTICS_FOR_EXPORT
52 StatisticsRegistry
* StatisticsRegistry::current() {
53 return stats::getStatisticsRegistry(smt::currentSmtEngine());
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());
63 #endif /* CVC4_STATISTICS_ON */
64 }/* StatisticsRegistry::registerStat() */
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());
73 #endif /* CVC4_STATISTICS_ON */
74 }/* StatisticsRegistry::unregisterStat() */
76 #endif /* ! __BUILDING_STATISTICS_FOR_EXPORT */
78 void StatisticsRegistry::registerStat_(Stat
* s
) throw(CVC4::IllegalArgumentException
) {
79 #ifdef CVC4_STATISTICS_ON
80 CheckArgument(d_stats
.find(s
) == d_stats
.end(), s
);
82 #endif /* CVC4_STATISTICS_ON */
83 }/* StatisticsRegistry::registerStat_() */
85 void StatisticsRegistry::unregisterStat_(Stat
* s
) throw(CVC4::IllegalArgumentException
) {
86 #ifdef CVC4_STATISTICS_ON
87 CheckArgument(d_stats
.find(s
) != d_stats
.end(), s
);
89 #endif /* CVC4_STATISTICS_ON */
90 }/* StatisticsRegistry::unregisterStat_() */
92 void StatisticsRegistry::flushStat(std::ostream
&out
) const {
93 #ifdef CVC4_STATISTICS_ON
94 flushInformation(out
);
95 #endif /* CVC4_STATISTICS_ON */
98 void StatisticsRegistry::flushInformation(std::ostream
&out
) const {
99 #ifdef CVC4_STATISTICS_ON
100 this->StatisticsBase::flushInformation(out
);
101 #endif /* CVC4_STATISTICS_ON */
104 void TimerStat::start() {
105 if(__CVC4_USE_STATISTICS
) {
106 CheckArgument(!d_running
, *this, "timer already running");
107 clock_gettime(CLOCK_MONOTONIC
, &d_start
);
110 }/* TimerStat::start() */
112 void TimerStat::stop() {
113 if(__CVC4_USE_STATISTICS
) {
114 CheckArgument(d_running
, *this, "timer not running");
116 clock_gettime(CLOCK_MONOTONIC
, &end
);
117 d_data
+= end
- d_start
;
120 }/* TimerStat::stop() */
122 RegisterStatistic::RegisterStatistic(ExprManager
& em
, Stat
* stat
) :
123 d_reg(stats::getStatisticsRegistry(&em
)),
125 d_reg
->registerStat_(d_stat
);
128 RegisterStatistic::RegisterStatistic(SmtEngine
& smt
, Stat
* stat
) :
129 d_reg(stats::getStatisticsRegistry(&smt
)),
131 d_reg
->registerStat_(d_stat
);
134 }/* CVC4 namespace */
136 #undef __CVC4_USE_STATISTICS