This PR does a first round of refactoring on the statistics, in particular the Stat class and derived classes.
It significantly shrinks the class hierarchy, modernizes some code (e.g. use std::chrono instead of clock_gettime), removes unused features (e.g. nesting of statistics) and does some general cleanup and consolidation.
Subsequent PRs are planned to change the ownership model (right now every module owns the Stat object) which makes the whole register / unregister mechanism obsolete.
#include "util/random.h"
#include "util/result.h"
#include "util/statistics_registry.h"
+#include "util/stats_histogram.h"
#include "util/utility.h"
namespace CVC4 {
#include "options/decision_weight.h"
#include "prop/sat_solver_types.h"
#include "util/statistics_registry.h"
+#include "util/stats_timer.h"
namespace CVC4 {
namespace decision {
#include "expr/node.h"
#include "expr/proof_rule.h"
#include "util/statistics_registry.h"
+#include "util/stats_histogram.h"
namespace CVC4 {
d_symman(new SymbolManager(d_solver.get())),
d_smtEngine(d_solver->getSmtEngine()),
d_options(options),
- d_stats("driver"),
+ d_stats(),
d_result()
{
}
int runCvc4(int argc, char* argv[], Options& opts) {
// Timer statistic
- pTotalTime = new TimerStat("totalTime");
+ pTotalTime = new TimerStat("driver::totalTime");
pTotalTime->start();
// For the signal handlers' benefit
pTotalTime);
// Filename statistics
- ReferenceStat<std::string> s_statFilename("filename", filenameStr);
+ ReferenceStat<std::string> s_statFilename("driver::filename", filenameStr);
RegisterStatistic statFilenameReg(&pExecutor->getStatisticsRegistry(),
&s_statFilename);
// notify SmtEngine that we are starting to parse
_exit(returnValue);
#endif /* CVC4_COMPETITION_MODE */
- ReferenceStat<api::Result> s_statSatResult("sat/unsat", result);
+ ReferenceStat<api::Result> s_statSatResult("driver::sat/unsat", result);
RegisterStatistic statSatResultReg(&pExecutor->getStatisticsRegistry(),
&s_statSatResult);
#include "options/options.h"
#include "util/statistics.h"
#include "util/statistics_registry.h"
+#include "util/stats_timer.h"
#ifndef CVC4__MAIN__MAIN_H
#define CVC4__MAIN__MAIN_H
#include "preprocessing/preprocessing_pass.h"
#include "preprocessing/util/ite_utilities.h"
+#include "util/stats_histogram.h"
namespace CVC4 {
namespace preprocessing {
#include <string>
#include "util/statistics_registry.h"
+#include "util/stats_timer.h"
namespace CVC4 {
namespace preprocessing {
#include "expr/node.h"
#include "util/hash.h"
#include "util/statistics_registry.h"
+#include "util/stats_histogram.h"
namespace CVC4 {
namespace preprocessing {
#include "proof/clause_id.h"
#include "proof/proof_manager.h"
#include "util/statistics_registry.h"
+#include "util/stats_histogram.h"
// Forward declarations.
namespace CVC4 {
return;
}
- d_statStarts.setData(minisat->starts);
- d_statDecisions.setData(minisat->decisions);
- d_statRndDecisions.setData(minisat->rnd_decisions);
- d_statPropagations.setData(minisat->propagations);
- d_statConflicts.setData(minisat->conflicts);
- d_statClausesLiterals.setData(minisat->clauses_literals);
- d_statLearntsLiterals.setData(minisat->learnts_literals);
- d_statMaxLiterals.setData(minisat->max_literals);
- d_statTotLiterals.setData(minisat->tot_literals);
- d_statEliminatedVars.setData(minisat->eliminated_vars);
+ d_statStarts.set(minisat->starts);
+ d_statDecisions.set(minisat->decisions);
+ d_statRndDecisions.set(minisat->rnd_decisions);
+ d_statPropagations.set(minisat->propagations);
+ d_statConflicts.set(minisat->conflicts);
+ d_statClausesLiterals.set(minisat->clauses_literals);
+ d_statLearntsLiterals.set(minisat->learnts_literals);
+ d_statMaxLiterals.set(minisat->max_literals);
+ d_statTotLiterals.set(minisat->tot_literals);
+ d_statEliminatedVars.set(minisat->eliminated_vars);
}
} /* namespace CVC4::prop */
#include "prop/sat_solver.h"
#include "util/resource_manager.h"
#include "util/statistics_registry.h"
+#include "util/stats_timer.h"
namespace CVC4 {
namespace prop {
}
void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* minisat){
- d_statStarts.setData(minisat->starts);
- d_statDecisions.setData(minisat->decisions);
- d_statRndDecisions.setData(minisat->rnd_decisions);
- d_statPropagations.setData(minisat->propagations);
- d_statConflicts.setData(minisat->conflicts);
- d_statClausesLiterals.setData(minisat->clauses_literals);
- d_statLearntsLiterals.setData(minisat->learnts_literals);
- d_statMaxLiterals.setData(minisat->max_literals);
- d_statTotLiterals.setData(minisat->tot_literals);
+ d_statStarts.set(minisat->starts);
+ d_statDecisions.set(minisat->decisions);
+ d_statRndDecisions.set(minisat->rnd_decisions);
+ d_statPropagations.set(minisat->propagations);
+ d_statConflicts.set(minisat->conflicts);
+ d_statClausesLiterals.set(minisat->clauses_literals);
+ d_statLearntsLiterals.set(minisat->learnts_literals);
+ d_statMaxLiterals.set(minisat->max_literals);
+ d_statTotLiterals.set(minisat->tot_literals);
}
} /* namespace CVC4::prop */
#include "expr/proof_node_updater.h"
#include "smt/witness_form.h"
#include "util/statistics_registry.h"
+#include "util/stats_histogram.h"
namespace CVC4 {
#define CVC4__SMT__SMT_ENGINE_STATS_H
#include "util/statistics_registry.h"
+#include "util/stats_timer.h"
namespace CVC4 {
namespace smt {
for(size_t i=0; i < d_denomGuesses.size(); ++i){
const Integer& D = d_denomGuesses[i];
if(!guessCoefficientsConstructTableRow(nid, M, vec, D)){
- d_stats.d_averageGuesses.addEntry(i+1);
+ d_stats.d_averageGuesses << i+1;
Debug("approx::gmi") << "guesseditat " << i << " D=" << D << endl;
return false;
}
#include "util/maybe.h"
#include "util/rational.h"
#include "util/statistics_registry.h"
+#include "util/stats_timer.h"
namespace CVC4 {
namespace theory {
#include "theory/arith/normal_form.h"
#include "util/rational.h"
#include "util/statistics_registry.h"
+#include "util/stats_timer.h"
namespace CVC4 {
namespace context {
#include "theory/arith/tableau.h"
#include "util/maybe.h"
#include "util/statistics_registry.h"
+#include "util/stats_timer.h"
namespace CVC4 {
namespace theory {
Debug("recentlyViolated")
<< "It worked? "
- << conflicts.getData()
+ << conflicts.get()
<< " " << curr
<< " " << checkBasicForConflict(curr) << endl;
reportConflict(curr);
#include "util/dense_map.h"
#include "util/result.h"
#include "util/statistics_registry.h"
+#include "util/stats_timer.h"
namespace CVC4 {
namespace theory {
std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex* approx, int nid, ConstraintP bc, int depth){
++(d_statistics.d_replayLogRecCount);
Debug("approx::replayLogRec") << "replayLogRec()"
- << d_statistics.d_replayLogRecCount.getData() << std::endl;
+ << d_statistics.d_replayLogRecCount.get() << std::endl;
size_t rpvars_size = d_replayVariables.size();
size_t rpcons_size = d_replayConstraints.size();
TimerStat::CodeTimer codeTimer0(d_statistics.d_solveIntTimer);
++(d_statistics.d_solveIntCalls);
- d_statistics.d_inSolveInteger.setData(1);
+ d_statistics.d_inSolveInteger.set(1);
if(!Theory::fullEffort(effortLevel)){
d_solveIntAttempts++;
}
}
- d_statistics.d_inSolveInteger.setData(0);
+ d_statistics.d_inSolveInteger.set(0);
}
SimplexDecisionProcedure& TheoryArithPrivate::selectSimplex(bool pass1){
default:
Unimplemented();
}
- d_statistics.d_avgUnknownsInARow.addEntry(d_unknownsInARow);
+ d_statistics.d_avgUnknownsInARow << d_unknownsInARow;
size_t nPivots =
options::useFC() ? d_fcSimplex.getPivots() : d_dualSimplex.getPivots();
void TheoryArithPrivate::presolve(){
TimerStat::CodeTimer codeTimer(d_statistics.d_presolveTime);
- d_statistics.d_initialTableauSize.setData(d_tableau.size());
+ d_statistics.d_initialTableauSize.set(d_tableau.size());
if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
if(s!= 0) {
- d_avgIndexListLength.addEntry(s);
+ d_avgIndexListLength << s;
++d_listsCount;
}
s = lista_st->size();
d_maxList.maxAssign(s);
if(s!= 0) {
- d_avgStoresListLength.addEntry(s);
+ d_avgStoresListLength << s;
++d_listsCount;
}
s = lista_inst->size();
d_maxList.maxAssign(s);
if(s!=0) {
- d_avgInStoresListLength.addEntry(s);
+ d_avgInStoresListLength << s;
++d_listsCount;
}
#include "context/cdlist.h"
#include "expr/node.h"
#include "util/statistics_registry.h"
+#include "util/stats_timer.h"
namespace CVC4 {
namespace theory {
#include "theory/bags/rewrites.h"
#include "theory/theory_rewriter.h"
#include "util/statistics_registry.h"
+#include "util/stats_histogram.h"
namespace CVC4 {
namespace theory {
#include "theory/bags/rewrites.h"
#include "util/statistics_registry.h"
+#include "util/stats_histogram.h"
namespace CVC4 {
namespace theory {
d_funcToSignature[abs_func] = signature;
}
- d_statistics.d_numFunctionsAbstracted.setData(d_signatureToFunc.size());
+ d_statistics.d_numFunctionsAbstracted.set(d_signatureToFunc.size());
Debug("bv-abstraction") << "AbstractionModule::finalizeSignatures abstracted "
<< d_signatureToFunc.size() << " signatures. \n";
#include "expr/node.h"
#include "theory/substitutions.h"
#include "util/statistics_registry.h"
+#include "util/stats_timer.h"
namespace CVC4 {
namespace theory {
// if (1.5* d_statistics.d_numUnknown.getData() > d_statistics.d_numSolved.getData()) {
// d_period = d_period * 2;
// }
- d_statistics.d_avgMinimizationRatio.addEntry(minimization_ratio);
+ d_statistics.d_avgMinimizationRatio << minimization_ratio;
return utils::mkAnd(minimized);
}
#include "prop/sat_solver_types.h"
#include "theory/bv/theory_bv_utils.h"
#include "util/statistics_registry.h"
+#include "util/stats_timer.h"
namespace CVC4 {
namespace theory {
Debug("bitvector") << indent() << "BVSolverLazy::check(): conflict "
<< d_conflictNode << std::endl;
d_im.conflict(d_conflictNode, InferenceId::BV_LAZY_CONFLICT);
- d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren());
+ d_statistics.d_avgConflictSize << d_conflictNode.getNumChildren();
d_conflictNode = Node::null();
}
}
return true;
double success_rate = double(d_numSolved)/double(d_numCalls);
- d_statistics.d_useHeuristic.setData(success_rate);
+ d_statistics.d_useHeuristic.set(success_rate);
return success_rate > 0.8;
}
int prevEt = 0;
if (Trace.isOn("qcf-engine"))
{
- prevEt = d_statistics.d_entailment_checks.getData();
+ prevEt = d_statistics.d_entailment_checks.get();
clSet = double(clock()) / double(CLOCKS_PER_SEC);
Trace("qcf-engine") << "---Conflict Find Engine Round, effort = " << level
<< "---" << std::endl;
Trace("qcf-engine") << ", addedLemmas = " << addedLemmas;
}
Trace("qcf-engine") << std::endl;
- int currEt = d_statistics.d_entailment_checks.getData();
+ int currEt = d_statistics.d_entailment_checks.get();
if (currEt != prevEt)
{
Trace("qcf-engine") << " Entailment checks = " << (currEt - prevEt)
#include "theory/strings/infer_info.h"
#include "theory/strings/rewrites.h"
#include "util/statistics_registry.h"
+#include "util/stats_histogram.h"
namespace CVC4 {
namespace theory {
#include "theory/trust_node.h"
#include "theory/valuation.h"
#include "util/statistics_registry.h"
+#include "util/stats_timer.h"
namespace CVC4 {
#include "theory/output_channel.h"
#include "theory/trust_node.h"
#include "util/statistics_registry.h"
+#include "util/stats_histogram.h"
namespace CVC4 {
#include "expr/node_builder.h"
#include "smt/smt_statistics_registry.h"
#include "util/statistics_registry.h"
+#include "util/stats_timer.h"
namespace CVC4 {
namespace theory {
statistics.h
statistics_registry.cpp
statistics_registry.h
+ stats_base.cpp
+ stats_base.h
+ stats_histogram.h
+ stats_timer.cpp
+ stats_timer.h
+ stats_utils.cpp
+ stats_utils.h
string.cpp
string.h
floatingpoint_literal_symfpu.cpp
d_options(options)
{
- d_statistics->d_resourceUnitsUsed.setData(d_cumulativeResourceUsed);
+ d_statistics->d_resourceUnitsUsed.set(d_cumulativeResourceUsed);
}
ResourceManager::~ResourceManager() {}
{
Trace("limit") << "ResourceManager::spendResource: interrupt!" << std::endl;
Trace("limit") << " on call "
- << d_statistics->d_spendResourceCalls.getData() << std::endl;
+ << d_statistics->d_spendResourceCalls.get() << std::endl;
if (outOfTime())
{
Trace("limit") << "ResourceManager::spendResource: elapsed time"
namespace CVC4 {
-std::string StatisticsBase::s_regDelim("::");
-
bool StatisticsBase::StatCmp::operator()(const Stat* s1, const Stat* s2) const {
return s1->getName() < s2->getName();
}
}
StatisticsBase::StatisticsBase() :
- d_prefix(),
d_stats() {
}
StatisticsBase::StatisticsBase(const StatisticsBase& stats) :
- d_prefix(stats.d_prefix),
d_stats() {
}
StatisticsBase& StatisticsBase::operator=(const StatisticsBase& stats) {
- d_prefix = stats.d_prefix;
return *this;
}
i != d_stats.end();
++i) {
Stat* s = *i;
- if(d_prefix != "") {
- out << d_prefix << s_regDelim;
- }
- s->flushStat(out);
+ out << s->getName() << ", ";
+ s->flushInformation(out);
out << std::endl;
}
#endif /* CVC4_STATISTICS_ON */
#ifdef CVC4_STATISTICS_ON
for (StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) {
Stat* s = *i;
- if (d_prefix.size() != 0) {
- safe_print(fd, d_prefix);
- safe_print(fd, s_regDelim);
- }
- s->safeFlushStat(fd);
+ safe_print(fd, s->getName());
+ safe_print(fd, ", ");
+ s->safeFlushInformation(fd);
safe_print(fd, "\n");
}
#endif /* CVC4_STATISTICS_ON */
}
}
-void StatisticsBase::setPrefix(const std::string& prefix) {
- d_prefix = prefix;
-}
-
}/* CVC4 namespace */
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;
/** 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;
/** 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;
/****************************************************************************/
namespace CVC4 {
-/** Compute the sum of two timespecs. */
-inline timespec& operator+=(timespec& a, const timespec& b) {
- using namespace CVC4;
- // assumes a.tv_nsec and b.tv_nsec are in range
- const long nsec_per_sec = 1000000000L; // one thousand million
- CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a);
- CheckArgument(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec, b);
- a.tv_sec += b.tv_sec;
- long nsec = a.tv_nsec + b.tv_nsec;
- Assert(nsec >= 0);
- if(nsec < 0) {
- nsec += nsec_per_sec;
- --a.tv_sec;
- }
- if(nsec >= nsec_per_sec) {
- nsec -= nsec_per_sec;
- ++a.tv_sec;
- }
- Assert(nsec >= 0 && nsec < nsec_per_sec);
- a.tv_nsec = nsec;
- return a;
-}
-
-/** Compute the difference of two timespecs. */
-inline timespec& operator-=(timespec& a, const timespec& b) {
- using namespace CVC4;
- // assumes a.tv_nsec and b.tv_nsec are in range
- const long nsec_per_sec = 1000000000L; // one thousand million
- CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a);
- CheckArgument(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec, b);
- a.tv_sec -= b.tv_sec;
- long nsec = a.tv_nsec - b.tv_nsec;
- if(nsec < 0) {
- nsec += nsec_per_sec;
- --a.tv_sec;
- }
- if(nsec >= nsec_per_sec) {
- nsec -= nsec_per_sec;
- ++a.tv_sec;
- }
- Assert(nsec >= 0 && nsec < nsec_per_sec);
- a.tv_nsec = nsec;
- return a;
-}
-
-/** Add two timespecs. */
-inline timespec operator+(const timespec& a, const timespec& b) {
- timespec result = a;
- return result += b;
-}
-
-/** Subtract two timespecs. */
-inline timespec operator-(const timespec& a, const timespec& b) {
- timespec result = a;
- return result -= b;
-}
-
-/**
- * Compare two timespecs for equality.
- * This must be kept in sync with the copy in test/util/stats_black.h
- */
-inline bool operator==(const timespec& a, const timespec& b) {
- // assumes a.tv_nsec and b.tv_nsec are in range
- return a.tv_sec == b.tv_sec && a.tv_nsec == b.tv_nsec;
-}
-
-/** Compare two timespecs for disequality. */
-inline bool operator!=(const timespec& a, const timespec& b) {
- // assumes a.tv_nsec and b.tv_nsec are in range
- return !(a == b);
-}
-
-/** Compare two timespecs, returning true iff a < b. */
-inline bool operator<(const timespec& a, const timespec& b) {
- // assumes a.tv_nsec and b.tv_nsec are in range
- return a.tv_sec < b.tv_sec ||
- (a.tv_sec == b.tv_sec && a.tv_nsec < b.tv_nsec);
-}
-
-/** Compare two timespecs, returning true iff a > b. */
-inline bool operator>(const timespec& a, const timespec& b) {
- // assumes a.tv_nsec and b.tv_nsec are in range
- return a.tv_sec > b.tv_sec ||
- (a.tv_sec == b.tv_sec && a.tv_nsec > b.tv_nsec);
-}
-
-/** Compare two timespecs, returning true iff a <= b. */
-inline bool operator<=(const timespec& a, const timespec& b) {
- // assumes a.tv_nsec and b.tv_nsec are in range
- return !(a > b);
-}
-
-/** Compare two timespecs, returning true iff a >= b. */
-inline bool operator>=(const timespec& a, const timespec& b) {
- // assumes a.tv_nsec and b.tv_nsec are in range
- return !(a < b);
-}
-
-/** Output a timespec on an output stream. */
-std::ostream& operator<<(std::ostream& os, const timespec& t) {
- // assumes t.tv_nsec is in range
- StreamFormatScope format_scope(os);
- return os << t.tv_sec << "."
- << std::setfill('0') << std::setw(9) << std::right << t.tv_nsec;
-}
-
-
-/** Construct a statistics registry */
-StatisticsRegistry::StatisticsRegistry(const std::string& name) : Stat(name)
-{
- d_prefix = name;
- if(CVC4_USE_STATISTICS) {
- PrettyCheckArgument(d_name.find(s_regDelim) == std::string::npos, name,
- "StatisticsRegistry names cannot contain the string \"%s\"",
- s_regDelim.c_str());
- }
-}
-
void StatisticsRegistry::registerStat(Stat* s)
{
#ifdef CVC4_STATISTICS_ON
#endif /* CVC4_STATISTICS_ON */
}
-void TimerStat::start() {
- if(CVC4_USE_STATISTICS) {
- PrettyCheckArgument(!d_running, *this, "timer already running");
- clock_gettime(CLOCK_MONOTONIC, &d_start);
- d_running = true;
- }
-}/* TimerStat::start() */
-
-void TimerStat::stop() {
- if(CVC4_USE_STATISTICS) {
- AlwaysAssert(d_running) << "timer not running";
- ::timespec end;
- clock_gettime(CLOCK_MONOTONIC, &end);
- d_data += end - d_start;
- d_running = false;
- }
-}/* TimerStat::stop() */
-
-bool TimerStat::running() const {
- return d_running;
-}/* TimerStat::running() */
-
-timespec TimerStat::getData() const {
- ::timespec data = d_data;
- if(CVC4_USE_STATISTICS && d_running) {
- ::timespec end;
- clock_gettime(CLOCK_MONOTONIC, &end);
- data += end - d_start;
- }
- return data;
-}
-
-SExpr TimerStat::getValue() const {
- ::timespec data = d_data;
- if(CVC4_USE_STATISTICS && d_running) {
- ::timespec end;
- clock_gettime(CLOCK_MONOTONIC, &end);
- data += end - d_start;
- }
- std::stringstream ss;
- ss << std::fixed << std::setprecision(8) << data;
- return SExpr(Rational::fromDecimal(ss.str()));
-}/* TimerStat::getValue() */
-
-
RegisterStatistic::RegisterStatistic(StatisticsRegistry* reg, Stat* stat)
: d_reg(reg),
d_stat(stat) {
}
}/* CVC4 namespace */
-
-#undef CVC4_USE_STATISTICS
** for a longer discussion on symbol visibility.
**/
+
+/**
+ * On the design of the statistics:
+ *
+ * Stat is the abstract base class for all statistic values.
+ * It stores the name and provides (fully virtual) methods
+ * flushInformation() and safeFlushInformation().
+ *
+ * BackedStat is an abstract templated base class for statistic values
+ * that store the data themselves. It takes care of printing them already
+ * and derived classes usually only need to provide methods to set the
+ * value.
+ *
+ * ReferenceStat holds a reference (conceptually, it is implemented as a
+ * const pointer) to some data that is stored outside of the statistic.
+ *
+ * IntStat is a BackedStat<std::int64_t>.
+ *
+ * SizeStat holds a const reference to some container and provides the
+ * size of this container.
+ *
+ * AverageStat is a BackedStat<double>.
+ *
+ * HistogramStat counts instances of some type T. It is implemented as a
+ * std::map<T, std::uint64_t>.
+ *
+ * IntegralHistogramStat is a (conceptual) specialization of HistogramStat
+ * for types that are (convertible to) integral. This allows to use a
+ * std::vector<std::uint64_t> instead of a std::map.
+ *
+ * TimerStat uses std::chrono to collect timing information. It is
+ * implemented as BackedStat<std::chrono::duration> and provides methods
+ * start() and stop(), accumulating times it was activated. It provides
+ * the convenience class CodeTimer to allow for RAII-style usage.
+ *
+ *
+ * All statistic classes should protect their custom methods using
+ * if (CVC4_USE_STATISTICS) { ... }
+ * Output methods (flushInformation() and safeFlushInformation()) are only
+ * called when statistics are enabled and need no protection.
+ *
+ *
+ * The statistic classes try to implement a consistent interface:
+ * - if we store some generic data, we implement set()
+ * - if we (conceptually) store a set of values, we implement operator<<()
+ * - if there are standard operations for the stored data, we implement these
+ * (like operator++() or operator+=())
+ */
+
#include "cvc4_private_library.h"
#ifndef CVC4__STATISTICS_REGISTRY_H
#include <sstream>
#include <vector>
-#include "base/exception.h"
-#include "util/safe_print.h"
-#include "util/statistics.h"
-
-namespace CVC4 {
-
-/**
- * Prints a timespec.
- *
- * This is used in the implementation of TimerStat. This needs to be available
- * before Stat due to ordering constraints in clang for TimerStat.
- */
-std::ostream& operator<<(std::ostream& os, const timespec& t) CVC4_PUBLIC;
-
#ifdef CVC4_STATISTICS_ON
# define CVC4_USE_STATISTICS true
#else
# define CVC4_USE_STATISTICS false
#endif
+#include "base/exception.h"
+#include "util/safe_print.h"
+#include "util/stats_base.h"
+#include "util/statistics.h"
-/**
- * The base class for all statistics.
- *
- * This base class keeps the name of the statistic and declares the (pure)
- * virtual function flushInformation(). Derived classes must implement
- * this function and pass their name to the base class constructor.
- *
- * This class also (statically) maintains the delimiter used to separate
- * the name and the value when statistics are output.
- */
-class Stat {
-protected:
- /** The name of this statistic */
- std::string d_name;
-
-public:
-
- /** Nullary constructor, does nothing */
- Stat() { }
-
- /**
- * Construct a statistic with the given name. Debug builds of CVC4
- * will throw an assertion exception if the given name contains the
- * statistic delimiter string.
- */
- Stat(const std::string& name) : d_name(name)
- {
- if(CVC4_USE_STATISTICS) {
- CheckArgument(d_name.find(", ") == std::string::npos, name,
- "Statistics names cannot include a comma (',')");
- }
- }
-
- /** Destruct a statistic. This base-class version does nothing. */
- virtual ~Stat() {}
-
- /**
- * Flush the value of this statistic to an output stream. Should
- * finish the output with an end-of-line character.
- */
- virtual void flushInformation(std::ostream& out) const = 0;
-
- /**
- * Flush the value of this statistic to a file descriptor. Should finish the
- * output with an end-of-line character. Should be safe to use in a signal
- * handler.
- */
- virtual void safeFlushInformation(int fd) const = 0;
-
- /**
- * Flush the name,value pair of this statistic to an output stream.
- * Uses the statistic delimiter string between name and value.
- *
- * May be redefined by a child class
- */
- virtual void flushStat(std::ostream& out) const {
- if(CVC4_USE_STATISTICS) {
- out << d_name << ", ";
- flushInformation(out);
- }
- }
-
- /**
- * Flush the name,value pair of this statistic to a file descriptor. Uses the
- * statistic delimiter string between name and value.
- *
- * May be redefined by a child class
- */
- virtual void safeFlushStat(int fd) const {
- if (CVC4_USE_STATISTICS) {
- safe_print(fd, d_name);
- safe_print(fd, ", ");
- safeFlushInformation(fd);
- }
- }
-
- /** Get the name of this statistic. */
- const std::string& getName() const {
- return d_name;
- }
-
- /** Get the value of this statistic as a string. */
- virtual SExpr getValue() const {
- std::stringstream ss;
- flushInformation(ss);
- return SExpr(ss.str());
- }
-
-};/* class Stat */
-
-// A generic way of making a SExpr from templated stats code.
-// for example, the uint64_t version ensures that we create
-// Integer-SExprs for ReadOnlyDataStats (like those inside
-// Minisat) without having to specialize the entire
-// ReadOnlyDataStat class template.
-template <class T>
-inline SExpr mkSExpr(const T& x) {
- std::stringstream ss;
- ss << x;
- return SExpr(ss.str());
-}
-
-template <>
-inline SExpr mkSExpr(const uint64_t& x) {
- return SExpr(Integer(x));
-}
-
-template <>
-inline SExpr mkSExpr(const int64_t& x) {
- return SExpr(Integer(x));
-}
-
-template <>
-inline SExpr mkSExpr(const int& x) {
- return SExpr(Integer(x));
-}
-
-template <>
-inline SExpr mkSExpr(const Integer& x) {
- return SExpr(x);
-}
-
-template <>
-inline SExpr mkSExpr(const double& x) {
- // roundabout way to get a Rational from a double
- std::stringstream ss;
- ss << std::fixed << std::setprecision(8) << x;
- return SExpr(Rational::fromDecimal(ss.str()));
-}
-
-template <>
-inline SExpr mkSExpr(const Rational& x) {
- return SExpr(x);
-}
-
-/**
- * A class to represent a "read-only" data statistic of type T. Adds to
- * the Stat base class the pure virtual function getData(), which returns
- * type T, and flushInformation(), which outputs the statistic value to an
- * output stream (using the same existing stream insertion operator).
- *
- * Template class T must have stream insertion operation defined:
- * std::ostream& operator<<(std::ostream&, const T&)
- */
-template <class T>
-class ReadOnlyDataStat : public Stat {
-public:
- /** The "payload" type of this data statistic (that is, T). */
- typedef T payload_t;
-
- /** Construct a read-only data statistic with the given name. */
- ReadOnlyDataStat(const std::string& name) :
- Stat(name) {
- }
-
- /** Get the value of the statistic. */
- virtual T getData() const = 0;
-
- /** Get a reference to the data value of the statistic. */
- virtual const T& getDataRef() const = 0;
-
- /** Flush the value of the statistic to the given output stream. */
- void flushInformation(std::ostream& out) const override
- {
- if(CVC4_USE_STATISTICS) {
- out << getData();
- }
- }
-
- void safeFlushInformation(int fd) const override
- {
- if (CVC4_USE_STATISTICS) {
- safe_print<T>(fd, getDataRef());
- }
- }
-
- SExpr getValue() const override { return mkSExpr(getData()); }
-
-};/* class ReadOnlyDataStat<T> */
-
-
-/**
- * A data statistic class. This class extends a read-only data statistic
- * with assignment (the statistic can be set as well as read). This class
- * adds to the read-only case a pure virtual function setData(), thus
- * providing the basic interface for a data statistic: getData() to get the
- * statistic value, and setData() to set it.
- *
- * As with the read-only data statistic class, template class T must have
- * stream insertion operation defined:
- * std::ostream& operator<<(std::ostream&, const T&)
- */
-template <class T>
-class DataStat : public ReadOnlyDataStat<T> {
-public:
-
- /** Construct a data statistic with the given name. */
- DataStat(const std::string& name) :
- ReadOnlyDataStat<T>(name) {
- }
-
- /** Set the data statistic. */
- virtual void setData(const T&) = 0;
-
-};/* class DataStat<T> */
-
-
-/**
- * A data statistic that references a data cell of type T,
- * implementing getData() by referencing that memory cell, and
- * setData() by reassigning the statistic to point to the new
- * data cell. The referenced data cell is kept as a const
- * reference, meaning the referenced data is never actually
- * modified by this class (it must be externally modified for
- * a reference statistic to make sense). A common use for
- * this type of statistic is to output a statistic that is kept
- * outside the statistics package (for example, one that's kept
- * by a theory implementation for internal heuristic purposes,
- * which is important to keep even if statistics are turned off).
- *
- * Template class T must have an assignment operator=().
- */
-template <class T>
-class ReferenceStat : public DataStat<T> {
-private:
- /** The referenced data cell */
- const T* d_data;
-
-public:
- /**
- * Construct a reference stat with the given name and a reference
- * to NULL.
- */
- ReferenceStat(const std::string& name) :
- DataStat<T>(name),
- d_data(NULL) {
- }
-
- /**
- * Construct a reference stat with the given name and a reference to
- * the given data.
- */
- ReferenceStat(const std::string& name, const T& data) :
- DataStat<T>(name),
- d_data(NULL) {
- setData(data);
- }
-
- /** Set this reference statistic to refer to the given data cell. */
- void setData(const T& t) override
- {
- if(CVC4_USE_STATISTICS) {
- d_data = &t;
- }
- }
-
- /** Get the value of the referenced data cell. */
- T getData() const override { return *d_data; }
-
- /** Get a reference to the value of the referenced data cell. */
- const T& getDataRef() const override { return *d_data; }
-
-};/* class ReferenceStat<T> */
-
-/**
- * A data statistic that keeps a T and sets it with setData().
- *
- * Template class T must have an operator=() and a copy constructor.
- */
-template <class T>
-class BackedStat : public DataStat<T> {
-protected:
- /** The internally-kept statistic value */
- T d_data;
-
-public:
-
- /** Construct a backed statistic with the given name and initial value. */
- BackedStat(const std::string& name, const T& init) :
- DataStat<T>(name),
- d_data(init) {
- }
-
- /** Set the underlying data value to the given value. */
- void setData(const T& t) override
- {
- if(CVC4_USE_STATISTICS) {
- d_data = t;
- }
- }
-
- /** Identical to setData(). */
- BackedStat<T>& operator=(const T& t) {
- if(CVC4_USE_STATISTICS) {
- d_data = t;
- }
- return *this;
- }
-
- /** Get the underlying data value. */
- T getData() const override { return d_data; }
-
- /** Get a reference to the underlying data value. */
- const T& getDataRef() const override { return d_data; }
-
-};/* class BackedStat<T> */
-
-/**
- * A wrapper Stat for another Stat.
- *
- * This type of Stat is useful in cases where a module (like the
- * CongruenceClosure module) might keep its own statistics, but might
- * be instantiated in many contexts by many clients. This makes such
- * a statistic inappopriate to register with the StatisticsRegistry
- * directly, as all would be output with the same name (and may be
- * unregistered too quickly anyway). A WrappedStat allows the calling
- * client (say, TheoryUF) to wrap the Stat from the client module,
- * giving it a globally unique name.
- */
-template <class Stat>
-class WrappedStat : public ReadOnlyDataStat<typename Stat::payload_t> {
- typedef typename Stat::payload_t T;
-
- const ReadOnlyDataStat<T>& d_stat;
-
- /** Private copy constructor undefined (no copy permitted). */
- WrappedStat(const WrappedStat&) = delete;
- /** Private assignment operator undefined (no copy permitted). */
- WrappedStat<T>& operator=(const WrappedStat&) = delete;
-
-public:
-
- /**
- * Construct a wrapped statistic with the given name that wraps the
- * given statistic.
- */
- WrappedStat(const std::string& name, const ReadOnlyDataStat<T>& stat) :
- ReadOnlyDataStat<T>(name),
- d_stat(stat) {
- }
-
- /** Get the data of the underlying (wrapped) statistic. */
- T getData() const override { return d_stat.getData(); }
-
- /** Get a reference to the data of the underlying (wrapped) statistic. */
- const T& getDataRef() const override { return d_stat.getDataRef(); }
-
- void safeFlushInformation(int fd) const override
- {
- // ReadOnlyDataStat uses getDataRef() to get the information to print,
- // which might not be appropriate for all wrapped statistics. Delegate the
- // printing to the wrapped statistic instead.
- d_stat.safeFlushInformation(fd);
- }
-
- SExpr getValue() const override { return d_stat.getValue(); }
-
-};/* class WrappedStat<T> */
-
-/**
- * A backed integer-valued (64-bit signed) statistic.
- * This doesn't functionally differ from its base class BackedStat<int64_t>,
- * except for adding convenience functions for dealing with integers.
- */
-class IntStat : public BackedStat<int64_t> {
-public:
-
- /**
- * Construct an integer-valued statistic with the given name and
- * initial value.
- */
- IntStat(const std::string& name, int64_t init) :
- BackedStat<int64_t>(name, init) {
- }
-
- /** Increment the underlying integer statistic. */
- IntStat& operator++() {
- if(CVC4_USE_STATISTICS) {
- ++d_data;
- }
- return *this;
- }
-
- /** Increment the underlying integer statistic by the given amount. */
- IntStat& operator+=(int64_t val) {
- if(CVC4_USE_STATISTICS) {
- d_data += val;
- }
- return *this;
- }
-
- /** Keep the maximum of the current statistic value and the given one. */
- void maxAssign(int64_t val) {
- if(CVC4_USE_STATISTICS) {
- if(d_data < val) {
- d_data = val;
- }
- }
- }
-
- /** Keep the minimum of the current statistic value and the given one. */
- void minAssign(int64_t val) {
- if(CVC4_USE_STATISTICS) {
- if(d_data > val) {
- d_data = val;
- }
- }
- }
-
- SExpr getValue() const override { return SExpr(Integer(d_data)); }
-
-};/* class IntStat */
-
-template <class T>
-class SizeStat : public Stat {
-private:
- const T& d_sized;
-public:
- SizeStat(const std::string&name, const T& sized) :
- Stat(name), d_sized(sized) {}
- ~SizeStat() {}
-
- void flushInformation(std::ostream& out) const override
- {
- out << d_sized.size();
- }
-
- void safeFlushInformation(int fd) const override
- {
- safe_print<uint64_t>(fd, d_sized.size());
- }
-
- SExpr getValue() const override { return SExpr(Integer(d_sized.size())); }
-
-};/* class SizeStat */
-
-/**
- * The value for an AverageStat is the running average of (e1, e_2, ..., e_n),
- * (e1 + e_2 + ... + e_n)/n,
- * where e_i is an entry added by an addEntry(e_i) call.
- * The value is initially always 0.
- * (This is to avoid making parsers confused.)
- *
- * A call to setData() will change the running average but not reset the
- * running count, so should generally be avoided. Call addEntry() to add
- * an entry to the average calculation.
- */
-class AverageStat : public BackedStat<double> {
-private:
- /**
- * The number of accumulations of the running average that we
- * have seen so far.
- */
- uint32_t d_count;
- double d_sum;
-
-public:
- /** Construct an average statistic with the given name. */
- AverageStat(const std::string& name) :
- BackedStat<double>(name, 0.0), d_count(0), d_sum(0.0) {
- }
-
- /** Add an entry to the running-average calculation. */
- void addEntry(double e) {
- if(CVC4_USE_STATISTICS) {
- ++d_count;
- d_sum += e;
- setData(d_sum / d_count);
- }
- }
-
- SExpr getValue() const override
- {
- std::stringstream ss;
- ss << std::fixed << std::setprecision(8) << d_data;
- return SExpr(Rational::fromDecimal(ss.str()));
- }
-
-};/* class AverageStat */
+namespace CVC4 {
/** A statistic that contains a SExpr. */
class SExprStat : public Stat {
};/* class SExprStat */
-template <class T>
-class HistogramStat : public Stat {
-private:
- typedef std::map<T, unsigned int> Histogram;
- Histogram d_hist;
-public:
-
- /** Construct a histogram of a stream of entries. */
- HistogramStat(const std::string& name) : Stat(name) {}
- ~HistogramStat() {}
-
- void flushInformation(std::ostream& out) const override
- {
- if(CVC4_USE_STATISTICS) {
- typename Histogram::const_iterator i = d_hist.begin();
- typename Histogram::const_iterator end = d_hist.end();
- out << "[";
- while(i != end){
- const T& key = (*i).first;
- unsigned int count = (*i).second;
- out << "("<<key<<" : "<<count<< ")";
- ++i;
- if(i != end){
- out << ", ";
- }
- }
- out << "]";
- }
- }
-
- void safeFlushInformation(int fd) const override
- {
- if (CVC4_USE_STATISTICS) {
- typename Histogram::const_iterator i = d_hist.begin();
- typename Histogram::const_iterator end = d_hist.end();
- safe_print(fd, "[");
- while (i != end) {
- const T& key = (*i).first;
- unsigned int count = (*i).second;
- safe_print(fd, "(");
- safe_print<T>(fd, key);
- safe_print(fd, " : ");
- safe_print<uint64_t>(fd, count);
- safe_print(fd, ")");
- ++i;
- if (i != end) {
- safe_print(fd, ", ");
- }
- }
- safe_print(fd, "]");
- }
- }
-
- HistogramStat& operator<<(const T& val){
- if(CVC4_USE_STATISTICS) {
- if(d_hist.find(val) == d_hist.end()){
- d_hist.insert(std::make_pair(val,0));
- }
- d_hist[val]++;
- }
- return (*this);
- }
-
-};/* class HistogramStat */
-
-/**
- * A histogram statistic class for integral types.
- * Avoids using an std::map (like the generic HistogramStat) in favor of a
- * faster std::vector by casting the integral values to indices into the
- * vector. Requires the type to be an integral type that is convertible to
- * std::int64_t, also supporting appropriate enum types.
- * The vector is resized on demand to grow as necessary and supports negative
- * values as well.
- */
-template <typename Integral>
-class IntegralHistogramStat : public Stat
-{
- static_assert(std::is_integral<Integral>::value
- || std::is_enum<Integral>::value,
- "Type should be a fundamental integral type.");
-
- private:
- std::vector<std::uint64_t> d_hist;
- std::int64_t d_offset;
-
- public:
- /** Construct a histogram of a stream of entries. */
- IntegralHistogramStat(const std::string& name) : Stat(name) {}
- ~IntegralHistogramStat() {}
-
- void flushInformation(std::ostream& out) const override
- {
- if (CVC4_USE_STATISTICS)
- {
- out << "[";
- bool first = true;
- for (std::size_t i = 0, n = d_hist.size(); i < n; ++i)
- {
- if (d_hist[i] > 0)
- {
- if (first)
- {
- first = false;
- }
- else
- {
- out << ", ";
- }
- out << "(" << static_cast<Integral>(i + d_offset) << " : "
- << d_hist[i] << ")";
- }
- }
- out << "]";
- }
- }
-
- void safeFlushInformation(int fd) const override
- {
- if (CVC4_USE_STATISTICS)
- {
- safe_print(fd, "[");
- bool first = true;
- for (std::size_t i = 0, n = d_hist.size(); i < n; ++i)
- {
- if (d_hist[i] > 0)
- {
- if (first)
- {
- first = false;
- }
- else
- {
- safe_print(fd, ", ");
- }
- safe_print(fd, "(");
- safe_print<Integral>(fd, static_cast<Integral>(i + d_offset));
- safe_print(fd, " : ");
- safe_print<std::uint64_t>(fd, d_hist[i]);
- safe_print(fd, ")");
- }
- }
- safe_print(fd, "]");
- }
- }
-
- IntegralHistogramStat& operator<<(Integral val)
- {
- if (CVC4_USE_STATISTICS)
- {
- std::int64_t v = static_cast<std::int64_t>(val);
- if (d_hist.empty())
- {
- d_offset = v;
- }
- if (v < d_offset)
- {
- d_hist.insert(d_hist.begin(), d_offset - v, 0);
- d_offset = v;
- }
- if (static_cast<std::size_t>(v - d_offset) >= d_hist.size())
- {
- d_hist.resize(v - d_offset + 1);
- }
- d_hist[v - d_offset]++;
- }
- return (*this);
- }
-}; /* class IntegralHistogramStat */
-
/****************************************************************************/
/* Statistics Registry */
/****************************************************************************/
* The main statistics registry. This registry maintains the list of
* currently active statistics and is able to "flush" them all.
*/
-class CVC4_PUBLIC StatisticsRegistry : public StatisticsBase, public Stat {
+class CVC4_PUBLIC StatisticsRegistry : public StatisticsBase {
private:
/** Private copy constructor undefined (no copy permitted). */
/** Construct an nameless statistics registry */
StatisticsRegistry() {}
- /** Construct a statistics registry */
- StatisticsRegistry(const std::string& name);
-
- /**
- * Set the name of this statistic registry, used as prefix during
- * output. (This version overrides StatisticsBase::setPrefix().)
- */
- void setPrefix(const std::string& name) override { d_prefix = d_name = name; }
-
- /** Overridden to avoid the name being printed */
- void flushStat(std::ostream& out) const override;
+ void flushStat(std::ostream& out) const;
- void flushInformation(std::ostream& out) const override;
+ void flushInformation(std::ostream& out) const;
- void safeFlushInformation(int fd) const override;
+ void safeFlushInformation(int fd) const;
- SExpr getValue() const override
+ SExpr getValue() const
{
std::vector<SExpr> v;
for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) {
};/* class StatisticsRegistry */
-class CodeTimer;
-
-/**
- * A timer statistic. The timer can be started and stopped
- * arbitrarily, like a stopwatch; the value of the statistic at the
- * end is the accumulated time over all (start,stop) pairs.
- */
-class CVC4_PUBLIC TimerStat : public BackedStat<timespec> {
-
- // strange: timespec isn't placed in 'std' namespace ?!
- /** The last start time of this timer */
- timespec d_start;
-
- /** Whether this timer is currently running */
- bool d_running;
-
-public:
-
- typedef CVC4::CodeTimer CodeTimer;
-
- /**
- * Construct a timer statistic with the given name. Newly-constructed
- * timers have a 0.0 value and are not running.
- */
- TimerStat(const std::string& name)
- : BackedStat<timespec>(name, {0, 0}), d_start{0, 0}, d_running(false) {}
-
- /** Start the timer. */
- void start();
-
- /**
- * Stop the timer and update the statistic value with the
- * accumulated time.
- */
- void stop();
-
- /** If the timer is currently running */
- bool running() const;
-
- timespec getData() const override;
-
- void safeFlushInformation(int fd) const override
- {
- // Overwrite the implementation in the superclass because we cannot use
- // getDataRef(): it might return stale data if the timer is currently
- // running.
- ::timespec data = getData();
- safe_print<timespec>(fd, data);
- }
-
- SExpr getValue() const override;
-
-};/* class TimerStat */
-
-/**
- * Utility class to make it easier to call stop() at the end of a
- * code block. When constructed, it starts the timer. When
- * destructed, it stops the timer.
- */
-class CodeTimer {
- TimerStat& d_timer;
- bool d_reentrant;
-
- /** Private copy constructor undefined (no copy permitted). */
- CodeTimer(const CodeTimer& timer) = delete;
- /** Private assignment operator undefined (no copy permitted). */
- CodeTimer& operator=(const CodeTimer& timer) = delete;
-
-public:
- CodeTimer(TimerStat& timer, bool allow_reentrant = false) : d_timer(timer), d_reentrant(false) {
- if(!allow_reentrant || !(d_reentrant = d_timer.running())) {
- d_timer.start();
- }
- }
- ~CodeTimer() {
- if(!d_reentrant) {
- d_timer.stop();
- }
- }
-};/* class CodeTimer */
-
/**
* Resource-acquisition-is-initialization idiom for statistics
* registry. Useful for stack-based statistics (like in the driver).
};/* class RegisterStatistic */
-#undef CVC4_USE_STATISTICS
-
}/* CVC4 namespace */
#endif /* CVC4__STATISTICS_REGISTRY_H */
--- /dev/null
+/********************* */
+/*! \file stats_base.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 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 Base statistic classes
+ **
+ ** Base statistic classes
+ **/
+
+#include "util/stats_base.h"
+
+#include "util/statistics_registry.h"
+
+namespace CVC4 {
+
+Stat::Stat(const std::string& name) : d_name(name)
+{
+ if (CVC4_USE_STATISTICS)
+ {
+ CheckArgument(d_name.find(", ") == std::string::npos,
+ name,
+ "Statistics names cannot include a comma (',')");
+ }
+}
+
+IntStat::IntStat(const std::string& name, int64_t init)
+ : BackedStat<int64_t>(name, init)
+{
+}
+
+/** Increment the underlying integer statistic. */
+IntStat& IntStat::operator++()
+{
+ if (CVC4_USE_STATISTICS)
+ {
+ ++d_data;
+ }
+ return *this;
+}
+/** Increment the underlying integer statistic. */
+IntStat& IntStat::operator++(int)
+{
+ if (CVC4_USE_STATISTICS)
+ {
+ ++d_data;
+ }
+ return *this;
+}
+
+/** Increment the underlying integer statistic by the given amount. */
+IntStat& IntStat::operator+=(int64_t val)
+{
+ if (CVC4_USE_STATISTICS)
+ {
+ d_data += val;
+ }
+ return *this;
+}
+
+/** Keep the maximum of the current statistic value and the given one. */
+void IntStat::maxAssign(int64_t val)
+{
+ if (CVC4_USE_STATISTICS)
+ {
+ if (d_data < val)
+ {
+ d_data = val;
+ }
+ }
+}
+
+/** Keep the minimum of the current statistic value and the given one. */
+void IntStat::minAssign(int64_t val)
+{
+ if (CVC4_USE_STATISTICS)
+ {
+ if (d_data > val)
+ {
+ d_data = val;
+ }
+ }
+}
+
+AverageStat::AverageStat(const std::string& name)
+ : BackedStat<double>(name, 0.0)
+{
+}
+
+/** Add an entry to the running-average calculation. */
+AverageStat& AverageStat::operator<<(double e)
+{
+ if (CVC4_USE_STATISTICS)
+ {
+ ++d_count;
+ d_sum += e;
+ set(d_sum / d_count);
+ }
+ return *this;
+}
+
+SExpr AverageStat::getValue() const
+{
+ std::stringstream ss;
+ ss << std::fixed << std::setprecision(8) << d_data;
+ return SExpr(Rational::fromDecimal(ss.str()));
+}
+
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file stats_base.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 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 Base statistic classes
+ **
+ ** Base statistic classes
+ **/
+
+#include "cvc4_private_library.h"
+
+#ifndef CVC4__UTIL__STATS_BASE_H
+#define CVC4__UTIL__STATS_BASE_H
+
+#include <iomanip>
+#include <sstream>
+#include <string>
+
+#include "util/safe_print.h"
+#include "util/sexpr.h"
+#include "util/stats_utils.h"
+
+#ifdef CVC4_STATISTICS_ON
+#define CVC4_USE_STATISTICS true
+#else
+#define CVC4_USE_STATISTICS false
+#endif
+
+namespace CVC4 {
+
+/**
+ * The base class for all statistics.
+ *
+ * This base class keeps the name of the statistic and declares the (pure)
+ * virtual functions flushInformation() and safeFlushInformation().
+ * Derived classes must implement these function and pass their name to
+ * the base class constructor.
+ */
+class Stat
+{
+ public:
+ /**
+ * Construct a statistic with the given name. Debug builds of CVC4
+ * will throw an assertion exception if the given name contains the
+ * statistic delimiter string.
+ */
+ Stat(const std::string& name);
+
+ /** Destruct a statistic. This base-class version does nothing. */
+ virtual ~Stat() = default;
+
+ /**
+ * Flush the value of this statistic to an output stream. Should
+ * finish the output with an end-of-line character.
+ */
+ virtual void flushInformation(std::ostream& out) const = 0;
+
+ /**
+ * Flush the value of this statistic to a file descriptor. Should finish the
+ * output with an end-of-line character. Should be safe to use in a signal
+ * handler.
+ */
+ virtual void safeFlushInformation(int fd) const = 0;
+
+ /** Get the name of this statistic. */
+ const std::string& getName() const { return d_name; }
+
+ /** Get the value of this statistic as a string. */
+ virtual SExpr getValue() const
+ {
+ std::stringstream ss;
+ flushInformation(ss);
+ return SExpr(ss.str());
+ }
+
+ protected:
+ /** The name of this statistic */
+ std::string d_name;
+}; /* class Stat */
+
+/**
+ * A data statistic that keeps a T and sets it with setData().
+ *
+ * Template class T must have an operator=() and a copy constructor.
+ */
+template <class T>
+class BackedStat : public Stat
+{
+ public:
+ /** Construct a backed statistic with the given name and initial value. */
+ BackedStat(const std::string& name, const T& init) : Stat(name), d_data(init)
+ {
+ }
+
+ /** Set the underlying data value to the given value. */
+ void set(const T& t)
+ {
+ if (CVC4_USE_STATISTICS)
+ {
+ d_data = t;
+ }
+ }
+
+ const T& get() const { return d_data; }
+
+ /** Flush the value of the statistic to the given output stream. */
+ virtual void flushInformation(std::ostream& out) const override
+ {
+ out << d_data;
+ }
+
+ virtual void safeFlushInformation(int fd) const override
+ {
+ safe_print<T>(fd, d_data);
+ }
+
+ protected:
+ /** The internally-kept statistic value */
+ T d_data;
+}; /* class BackedStat<T> */
+
+/**
+ * A data statistic that references a data cell of type T,
+ * implementing get() by referencing that memory cell, and
+ * setData() by reassigning the statistic to point to the new
+ * data cell. The referenced data cell is kept as a const
+ * reference, meaning the referenced data is never actually
+ * modified by this class (it must be externally modified for
+ * a reference statistic to make sense). A common use for
+ * this type of statistic is to output a statistic that is kept
+ * outside the statistics package (for example, one that's kept
+ * by a theory implementation for internal heuristic purposes,
+ * which is important to keep even if statistics are turned off).
+ *
+ * Template class T must have an assignment operator=().
+ */
+template <class T>
+class ReferenceStat : public Stat
+{
+ public:
+ /**
+ * Construct a reference stat with the given name and a reference
+ * to nullptr.
+ */
+ ReferenceStat(const std::string& name) : Stat(name) {}
+
+ /**
+ * Construct a reference stat with the given name and a reference to
+ * the given data.
+ */
+ ReferenceStat(const std::string& name, const T& data) : Stat(name)
+ {
+ set(data);
+ }
+
+ /** Set this reference statistic to refer to the given data cell. */
+ void set(const T& t)
+ {
+ if (CVC4_USE_STATISTICS)
+ {
+ d_data = &t;
+ }
+ }
+ const T& get() const { return *d_data; }
+
+ /** Flush the value of the statistic to the given output stream. */
+ virtual void flushInformation(std::ostream& out) const override
+ {
+ out << *d_data;
+ }
+
+ virtual void safeFlushInformation(int fd) const override
+ {
+ safe_print<T>(fd, *d_data);
+ }
+
+ private:
+ /** The referenced data cell */
+ const T* d_data = nullptr;
+}; /* class ReferenceStat<T> */
+
+/**
+ * A backed integer-valued (64-bit signed) statistic.
+ * This doesn't functionally differ from its base class BackedStat<int64_t>,
+ * except for adding convenience functions for dealing with integers.
+ */
+class IntStat : public BackedStat<int64_t>
+{
+ public:
+ /**
+ * Construct an integer-valued statistic with the given name and
+ * initial value.
+ */
+ IntStat(const std::string& name, int64_t init);
+
+ /** Increment the underlying integer statistic. */
+ IntStat& operator++();
+ /** Increment the underlying integer statistic. */
+ IntStat& operator++(int);
+
+ /** Increment the underlying integer statistic by the given amount. */
+ IntStat& operator+=(int64_t val);
+
+ /** Keep the maximum of the current statistic value and the given one. */
+ void maxAssign(int64_t val);
+
+ /** Keep the minimum of the current statistic value and the given one. */
+ void minAssign(int64_t val);
+
+ SExpr getValue() const override { return SExpr(Integer(d_data)); }
+
+}; /* class IntStat */
+
+/**
+ * The value for an AverageStat is the running average of (e1, e_2, ..., e_n),
+ * (e1 + e_2 + ... + e_n)/n,
+ * where e_i is an entry added by an addEntry(e_i) call.
+ * The value is initially always 0.
+ * (This is to avoid making parsers confused.)
+ *
+ * A call to setData() will change the running average but not reset the
+ * running count, so should generally be avoided. Call addEntry() to add
+ * an entry to the average calculation.
+ */
+class AverageStat : public BackedStat<double>
+{
+ public:
+ /** Construct an average statistic with the given name. */
+ AverageStat(const std::string& name);
+
+ /** Add an entry to the running-average calculation. */
+ AverageStat& operator<<(double e);
+
+ SExpr getValue() const override;
+
+ private:
+ /**
+ * The number of accumulations of the running average that we
+ * have seen so far.
+ */
+ uint32_t d_count = 0;
+ double d_sum = 0;
+}; /* class AverageStat */
+
+template <class T>
+class SizeStat : public Stat
+{
+ public:
+ SizeStat(const std::string& name, const T& sized) : Stat(name), d_sized(sized)
+ {
+ }
+ ~SizeStat() {}
+
+ /** Flush the value of the statistic to the given output stream. */
+ void flushInformation(std::ostream& out) const override
+ {
+ out << d_sized.size();
+ }
+
+ void safeFlushInformation(int fd) const override
+ {
+ safe_print(fd, d_sized.size());
+ }
+
+ private:
+ const T& d_sized;
+}; /* class SizeStat */
+
+} // namespace CVC4
+
+#endif
--- /dev/null
+/********************* */
+/*! \file stats_histogram.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 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 Histogram statistics
+ **
+ ** Stat classes that represent histograms
+ **/
+
+#include "cvc4_private_library.h"
+
+#ifndef CVC4__UTIL__STATS_HISTOGRAM_H
+#define CVC4__UTIL__STATS_HISTOGRAM_H
+
+#include <map>
+#include <vector>
+
+#include "util/stats_base.h"
+
+namespace CVC4 {
+
+template <class T>
+class HistogramStat : public Stat
+{
+ using Histogram = std::map<T, uint64_t>;
+ public:
+ /** Construct a histogram of a stream of entries. */
+ HistogramStat(const std::string& name) : Stat(name) {}
+
+ void flushInformation(std::ostream& out) const override
+ {
+ auto i = d_hist.begin();
+ auto end = d_hist.end();
+ out << "[";
+ while (i != end)
+ {
+ const T& key = (*i).first;
+ uint64_t count = (*i).second;
+ out << "(" << key << " : " << count << ")";
+ ++i;
+ if (i != end)
+ {
+ out << ", ";
+ }
+ }
+ out << "]";
+ }
+
+ void safeFlushInformation(int fd) const override
+ {
+ auto i = d_hist.begin();
+ auto end = d_hist.end();
+ safe_print(fd, "[");
+ while (i != end)
+ {
+ const T& key = (*i).first;
+ uint64_t count = (*i).second;
+ safe_print(fd, "(");
+ safe_print<T>(fd, key);
+ safe_print(fd, " : ");
+ safe_print<uint64_t>(fd, count);
+ safe_print(fd, ")");
+ ++i;
+ if (i != end)
+ {
+ safe_print(fd, ", ");
+ }
+ }
+ safe_print(fd, "]");
+ }
+
+ HistogramStat& operator<<(const T& val)
+ {
+ if (CVC4_USE_STATISTICS)
+ {
+ if (d_hist.find(val) == d_hist.end())
+ {
+ d_hist.insert(std::make_pair(val, 0));
+ }
+ d_hist[val]++;
+ }
+ return (*this);
+ }
+
+ private:
+ Histogram d_hist;
+}; /* class HistogramStat */
+
+/**
+ * A histogram statistic class for integral types.
+ * Avoids using an std::map (like the generic HistogramStat) in favor of a
+ * faster std::vector by casting the integral values to indices into the
+ * vector. Requires the type to be an integral type that is convertible to
+ * int64_t, also supporting appropriate enum types.
+ * The vector is resized on demand to grow as necessary and supports negative
+ * values as well.
+ */
+template <typename Integral>
+class IntegralHistogramStat : public Stat
+{
+ static_assert(std::is_integral<Integral>::value
+ || std::is_enum<Integral>::value,
+ "Type should be a fundamental integral type.");
+
+ public:
+ /** Construct a histogram of a stream of entries. */
+ IntegralHistogramStat(const std::string& name) : Stat(name) {}
+
+ void flushInformation(std::ostream& out) const override
+ {
+ out << "[";
+ bool first = true;
+ for (size_t i = 0, n = d_hist.size(); i < n; ++i)
+ {
+ if (d_hist[i] > 0)
+ {
+ if (first)
+ {
+ first = false;
+ }
+ else
+ {
+ out << ", ";
+ }
+ out << "(" << static_cast<Integral>(i + d_offset) << " : "
+ << d_hist[i] << ")";
+ }
+ }
+ out << "]";
+ }
+
+ void safeFlushInformation(int fd) const override
+ {
+ safe_print(fd, "[");
+ bool first = true;
+ for (size_t i = 0, n = d_hist.size(); i < n; ++i)
+ {
+ if (d_hist[i] > 0)
+ {
+ if (first)
+ {
+ first = false;
+ }
+ else
+ {
+ safe_print(fd, ", ");
+ }
+ safe_print(fd, "(");
+ safe_print<Integral>(fd, static_cast<Integral>(i + d_offset));
+ safe_print(fd, " : ");
+ safe_print<uint64_t>(fd, d_hist[i]);
+ safe_print(fd, ")");
+ }
+ }
+ safe_print(fd, "]");
+ }
+
+ IntegralHistogramStat& operator<<(Integral val)
+ {
+ if (CVC4_USE_STATISTICS)
+ {
+ int64_t v = static_cast<int64_t>(val);
+ if (d_hist.empty())
+ {
+ d_offset = v;
+ }
+ if (v < d_offset)
+ {
+ d_hist.insert(d_hist.begin(), d_offset - v, 0);
+ d_offset = v;
+ }
+ if (static_cast<size_t>(v - d_offset) >= d_hist.size())
+ {
+ d_hist.resize(v - d_offset + 1);
+ }
+ d_hist[v - d_offset]++;
+ }
+ return (*this);
+ }
+
+ private:
+ std::vector<uint64_t> d_hist;
+ int64_t d_offset;
+}; /* class IntegralHistogramStat */
+
+} // namespace CVC4
+
+#endif
--- /dev/null
+/********************* */
+/*! \file stats_timer.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 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 Timer statistics
+ **
+ ** Stat classes that hold timers
+ **/
+
+#include "util/stats_timer.h"
+
+#include <iostream>
+
+#include "base/check.h"
+#include "util/ostream_util.h"
+
+namespace CVC4 {
+
+template <>
+void safe_print(int fd, const timer_stat_detail::duration& t)
+{
+ safe_print<uint64_t>(fd, t / std::chrono::seconds(1));
+ safe_print(fd, ".");
+ safe_print_right_aligned(fd, (t % std::chrono::seconds(1)).count(), 9);
+}
+
+void TimerStat::start()
+{
+ if (CVC4_USE_STATISTICS)
+ {
+ PrettyCheckArgument(!d_running, *this, "timer already running");
+ d_start = timer_stat_detail::clock::now();
+ d_running = true;
+ }
+}
+
+void TimerStat::stop()
+{
+ if (CVC4_USE_STATISTICS)
+ {
+ AlwaysAssert(d_running) << "timer not running";
+ d_data += timer_stat_detail::clock::now() - d_start;
+ d_running = false;
+ }
+}
+
+bool TimerStat::running() const { return d_running; }
+
+timer_stat_detail::duration TimerStat::get() const
+{
+ auto data = d_data;
+ if (CVC4_USE_STATISTICS && d_running)
+ {
+ data += timer_stat_detail::clock::now() - d_start;
+ }
+ return data;
+}
+
+SExpr TimerStat::getValue() const
+{
+ auto data = d_data;
+ if (CVC4_USE_STATISTICS && d_running)
+ {
+ data += timer_stat_detail::clock::now() - d_start;
+ }
+ std::stringstream ss;
+ ss << std::fixed << std::setprecision(8) << data;
+ return SExpr(Rational::fromDecimal(ss.str()));
+}
+
+void TimerStat::flushInformation(std::ostream& out) const { out << get(); }
+
+void TimerStat::safeFlushInformation(int fd) const
+{
+ // Overwrite the implementation in the superclass because we cannot use
+ // getDataRef(): it might return stale data if the timer is currently
+ // running.
+ safe_print<timer_stat_detail::duration>(fd, get());
+}
+
+CodeTimer::CodeTimer(TimerStat& timer, bool allow_reentrant)
+ : d_timer(timer), d_reentrant(false)
+{
+ if (!allow_reentrant || !(d_reentrant = d_timer.running()))
+ {
+ d_timer.start();
+ }
+}
+CodeTimer::~CodeTimer()
+{
+ if (!d_reentrant)
+ {
+ d_timer.stop();
+ }
+}
+
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file stats_timer.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 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 Timer statistics
+ **
+ ** Stat classes that hold timers
+ **/
+
+#include "cvc4_private_library.h"
+
+#ifndef CVC4__UTIL__STATS_TIMER_H
+#define CVC4__UTIL__STATS_TIMER_H
+
+#include <chrono>
+
+#include "util/stats_base.h"
+
+namespace CVC4 {
+namespace timer_stat_detail {
+using clock = std::chrono::steady_clock;
+using time_point = clock::time_point;
+struct duration : public std::chrono::nanoseconds
+{
+};
+} // namespace timer_stat_detail
+
+template <>
+void CVC4_PUBLIC safe_print(int fd, const timer_stat_detail::duration& t);
+
+class CodeTimer;
+
+/**
+ * A timer statistic. The timer can be started and stopped
+ * arbitrarily, like a stopwatch; the value of the statistic at the
+ * end is the accumulated time over all (start,stop) pairs.
+ */
+class CVC4_PUBLIC TimerStat : public BackedStat<timer_stat_detail::duration>
+{
+ public:
+ typedef CVC4::CodeTimer CodeTimer;
+
+ /**
+ * Construct a timer statistic with the given name. Newly-constructed
+ * timers have a 0.0 value and are not running.
+ */
+ TimerStat(const std::string& name)
+ : BackedStat<timer_stat_detail::duration>(name,
+ timer_stat_detail::duration()),
+ d_start(),
+ d_running(false)
+ {
+ }
+
+ /** Start the timer. */
+ void start();
+
+ /**
+ * Stop the timer and update the statistic value with the
+ * accumulated time.
+ */
+ void stop();
+
+ /** If the timer is currently running */
+ bool running() const;
+
+ timer_stat_detail::duration get() const;
+
+ void flushInformation(std::ostream& out) const override;
+ void safeFlushInformation(int fd) const override;
+
+ SExpr getValue() const override;
+
+ private:
+ /** The last start time of this timer */
+ timer_stat_detail::time_point d_start;
+
+ /** Whether this timer is currently running */
+ bool d_running;
+}; /* class TimerStat */
+
+/**
+ * Utility class to make it easier to call stop() at the end of a
+ * code block. When constructed, it starts the timer. When
+ * destructed, it stops the timer.
+ */
+class CodeTimer
+{
+ public:
+ CodeTimer(TimerStat& timer, bool allow_reentrant = false);
+ ~CodeTimer();
+
+private:
+ TimerStat& d_timer;
+ bool d_reentrant;
+
+ /** Private copy constructor undefined (no copy permitted). */
+ CodeTimer(const CodeTimer& timer) = delete;
+ /** Private assignment operator undefined (no copy permitted). */
+ CodeTimer& operator=(const CodeTimer& timer) = delete;
+}; /* class CodeTimer */
+
+} // namespace CVC4
+
+#endif
--- /dev/null
+/********************* */
+/*! \file stats_utils.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 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 Statistic utilities
+ **
+ ** Statistic utilities
+ **/
+
+#include "util/stats_utils.h"
+
+#include <chrono>
+#include <iomanip>
+#include <iostream>
+
+#include "util/ostream_util.h"
+#include "util/stats_timer.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& os,
+ const timer_stat_detail::duration& dur)
+{
+ StreamFormatScope format_scope(os);
+
+ return os << (dur / std::chrono::seconds(1)) << "." << std::setfill('0')
+ << std::setw(9) << std::right
+ << (dur % std::chrono::seconds(1)).count();
+}
+
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file stats_utils.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 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 Statistic utilities
+ **
+ ** Statistic utilities
+ **/
+
+#include "cvc4_private_library.h"
+
+#ifndef CVC4__UTIL__STATS_UTILS_H
+#define CVC4__UTIL__STATS_UTILS_H
+
+#include <iosfwd>
+
+namespace CVC4 {
+
+namespace timer_stat_detail {
+struct duration;
+}
+
+std::ostream& operator<<(std::ostream& os,
+ const timer_stat_detail::duration& dur) CVC4_PUBLIC;
+
+} // namespace CVC4
+
+#endif
#include "lib/clock_gettime.h"
#include "test.h"
#include "util/statistics_registry.h"
+#include "util/stats_histogram.h"
+#include "util/stats_timer.h"
namespace CVC4 {
namespace test {
-/**
- * This is a duplicate of operator== in statistics_registry.h.
- * This is duplicated here to try to avoid polluting top namepsace.
- *
- * If operator== is in the CVC4 namespace, there are some circumstances
- * where clang does not find this operator.
- */
-bool operator==(const timespec& a, const timespec& b)
-{
- // assumes a.tv_nsec and b.tv_nsec are in range
- return a.tv_sec == b.tv_sec && a.tv_nsec == b.tv_nsec;
-}
-
class TestUtilBlackStats : public TestInternal
{
};
ASSERT_EQ(histIntStat.getName(), "hist-int");
ASSERT_EQ(histPfRuleStat.getName(), "hist-pfrule");
- ASSERT_EQ(refStr.getData(), empty);
- ASSERT_EQ(refStr2.getData(), bar);
+ ASSERT_EQ(refStr.get(), empty);
+ ASSERT_EQ(refStr2.get(), bar);
empty = "a different string";
bar += " and with an addition";
- ASSERT_EQ(refStr.getData(), empty);
- ASSERT_EQ(refStr2.getData(), bar);
+ ASSERT_EQ(refStr.get(), empty);
+ ASSERT_EQ(refStr2.get(), bar);
- ASSERT_EQ(backedStr.getData(), "baz");
+ ASSERT_EQ(backedStr.get(), "baz");
baz = "something else";
- ASSERT_EQ(backedStr.getData(), "baz");
+ ASSERT_EQ(backedStr.get(), "baz");
- ASSERT_EQ(sInt.getData(), 10);
- sInt.setData(100);
- ASSERT_EQ(sInt.getData(), 100);
+ ASSERT_EQ(sInt.get(), 10);
+ sInt.set(100);
+ ASSERT_EQ(sInt.get(), 100);
- ASSERT_TRUE(sTimer.getData() == timespec());
+ ASSERT_TRUE(sTimer.get() == std::chrono::nanoseconds());
std::stringstream sstr;
projects / cvc5.git / commitdiff