GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/util/statistics_registry.cpp Lines: 9 28 32.1 %
Date: 2021-03-23 Branches: 8 50 16.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file statistics_registry.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Tim King, Mathias Preiner
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing 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
20
#include <cstdlib>
21
#include <iostream>
22
23
#include "base/check.h"
24
#include "lib/clock_gettime.h"
25
#include "util/ostream_util.h"
26
27
#ifdef CVC4_STATISTICS_ON
28
#  define CVC4_USE_STATISTICS true
29
#else
30
#  define CVC4_USE_STATISTICS false
31
#endif
32
33
34
/****************************************************************************/
35
/* Some utility functions for timespec                                    */
36
/****************************************************************************/
37
namespace CVC4 {
38
39
4792214
void StatisticsRegistry::registerStat(Stat* s)
40
{
41
#ifdef CVC4_STATISTICS_ON
42
4792214
  PrettyCheckArgument(
43
      d_stats.find(s) == d_stats.end(),
44
      s,
45
      "Statistic `%s' is already registered with this registry.",
46
      s->getName().c_str());
47
4792214
  d_stats.insert(s);
48
#endif /* CVC4_STATISTICS_ON */
49
4792214
}/* StatisticsRegistry::registerStat_() */
50
51
4771632
void StatisticsRegistry::unregisterStat(Stat* s)
52
{
53
#ifdef CVC4_STATISTICS_ON
54
4771632
  AlwaysAssert(s != nullptr);
55
4771632
  AlwaysAssert(d_stats.erase(s) > 0)
56
      << "Statistic `" << s->getName()
57
      << "' was not registered with this registry.";
58
#endif /* CVC4_STATISTICS_ON */
59
4771632
} /* StatisticsRegistry::unregisterStat() */
60
61
void StatisticsRegistry::flushStat(std::ostream &out) const {
62
#ifdef CVC4_STATISTICS_ON
63
  flushInformation(out);
64
#endif /* CVC4_STATISTICS_ON */
65
}
66
67
void StatisticsRegistry::flushInformation(std::ostream &out) const {
68
#ifdef CVC4_STATISTICS_ON
69
  this->StatisticsBase::flushInformation(out);
70
#endif /* CVC4_STATISTICS_ON */
71
}
72
73
void StatisticsRegistry::safeFlushInformation(int fd) const {
74
#ifdef CVC4_STATISTICS_ON
75
  this->StatisticsBase::safeFlushInformation(fd);
76
#endif /* CVC4_STATISTICS_ON */
77
}
78
79
RegisterStatistic::RegisterStatistic(StatisticsRegistry* reg, Stat* stat)
80
    : d_reg(reg),
81
      d_stat(stat) {
82
  CheckArgument(reg != NULL, reg,
83
                "You need to specify a statistics registry"
84
                "on which to set the statistic");
85
  d_reg->registerStat(d_stat);
86
}
87
88
RegisterStatistic::~RegisterStatistic() {
89
  d_reg->unregisterStat(d_stat);
90
}
91
92
26685
}/* CVC4 namespace */