blob: e77b480906118130022061d79e24d260b9712fdf (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
|
/********************* */
/*! \file statistics.h
** \verbatim
** Top contributors (to current version):
** Morgan Deters, Andres Noetzli, Mathias Preiner
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. 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 "cvc4_public.h"
#ifndef CVC4__STATISTICS_H
#define CVC4__STATISTICS_H
#include <iterator>
#include <ostream>
#include <set>
#include <string>
#include <utility>
#include "util/sexpr.h"
namespace CVC4 {
class Stat;
class CVC4_PUBLIC StatisticsBase {
protected:
static std::string s_regDelim;
/** A helper class for comparing two statistics */
struct StatCmp {
bool operator()(const Stat* s1, const Stat* s2) const;
};/* struct StatisticsRegistry::StatCmp */
/** A type for a set of statistics */
typedef std::set< Stat*, StatCmp > StatSet;
std::string d_prefix;
/** The set of statistics in this object */
StatSet d_stats;
StatisticsBase();
StatisticsBase(const StatisticsBase& stats);
StatisticsBase& operator=(const StatisticsBase& stats);
public:
virtual ~StatisticsBase() { }
class CVC4_PUBLIC iterator : public std::iterator< std::input_iterator_tag, std::pair<std::string, SExpr> > {
StatSet::iterator d_it;
iterator(StatSet::iterator it) : d_it(it) { }
friend class StatisticsBase;
public:
iterator() : d_it() { }
iterator(const iterator& it) : d_it(it.d_it) { }
value_type operator*() const;
iterator& operator++() { ++d_it; return *this; }
iterator operator++(int) { iterator old = *this; ++d_it; return old; }
bool operator==(const iterator& i) const { return d_it == i.d_it; }
bool operator!=(const iterator& i) const { return d_it != i.d_it; }
};/* class StatisticsBase::iterator */
/** An iterator type over a set of statistics. */
typedef iterator const_iterator;
/** Set the output prefix for this set of statistics. */
virtual void setPrefix(const std::string& prefix);
/** Flush all statistics to the given output stream. */
void flushInformation(std::ostream& out) const;
/**
* Flush all statistics to the given file descriptor. Safe to use in a signal
* handler.
*/
void safeFlushInformation(int fd) const;
/** Get the value of a named statistic. */
SExpr getStatistic(std::string name) const;
/**
* Get an iterator to the beginning of the range of the set of
* statistics.
*/
const_iterator begin() const;
/**
* Get an iterator to the end of the range of the set of statistics.
*/
const_iterator end() const;
};/* class StatisticsBase */
class CVC4_PUBLIC Statistics : public StatisticsBase {
void clear();
void copyFrom(const StatisticsBase&);
public:
/**
* Override the copy constructor to do a "deep" copy of statistics
* values.
*/
Statistics(const StatisticsBase& stats);
Statistics(const Statistics& stats);
~Statistics();
/**
* Override the assignment operator to do a "deep" copy of statistics
* values.
*/
Statistics& operator=(const StatisticsBase& stats);
Statistics& operator=(const Statistics& stats);
};/* class Statistics */
}/* CVC4 namespace */
#endif /* CVC4__STATISTICS_H */
|
