blob: 11b2d70f7d4681aec3433fbf107d9ca17c9564b5 (
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
|
/********************* */
/*! \file statistics.h
** \verbatim
** Original author: Morgan Deters <mdeters@cs.nyu.edu>
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
** Copyright (c) 2009-2013 New York University and The University of Iowa
** 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 "util/sexpr.h"
#include <string>
#include <ostream>
#include <set>
#include <iterator>
#include <utility>
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;
/** 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 */
|
