diff options
Diffstat (limited to 'src/smt/smt_statistics_registry.h')
-rw-r--r-- | src/smt/smt_statistics_registry.h | 30 |
1 files changed, 0 insertions, 30 deletions
diff --git a/src/smt/smt_statistics_registry.h b/src/smt/smt_statistics_registry.h index e6932a084..1a0993d1d 100644 --- a/src/smt/smt_statistics_registry.h +++ b/src/smt/smt_statistics_registry.h @@ -28,34 +28,4 @@ namespace CVC4 { */ StatisticsRegistry* smtStatisticsRegistry(); - -/** - * To use a statistic, you need to declare it, initialize it in your - * constructor, register it in your constructor, and deregister it in - * your destructor. Instead, this macro does it all for you (and - * therefore also keeps the statistic type, field name, and output - * string all in the same place in your class's header. Its use is - * like in this example, which takes the place of the declaration of a - * statistics field "d_checkTimer": - * - * KEEP_STATISTIC(TimerStat, d_checkTimer, "theory::uf::checkTime"); - * - * If any args need to be passed to the constructor, you can specify - * them after the string. - * - * The macro works by creating a nested class type, derived from the - * statistic type you give it, which declares a registry-aware - * constructor/destructor pair. - */ -#define KEEP_STATISTIC(_StatType, _StatField, _StatName, _CtorArgs...) \ - struct Statistic_##_StatField : public _StatType { \ - Statistic_##_StatField() : _StatType(_StatName, ## _CtorArgs) { \ - smtStatisticsRegistry()->registerStat(this); \ - } \ - ~Statistic_##_StatField() { \ - smtStatisticsRegistry()->unregisterStat(this); \ - } \ - } _StatField - - }/* CVC4 namespace */ |