diff options
51 files changed, 1025 insertions, 1014 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 930ff895c..ebe5de294 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -59,6 +59,7 @@ #include "util/random.h" #include "util/result.h" #include "util/statistics_registry.h" +#include "util/stats_histogram.h" #include "util/utility.h" namespace CVC4 { diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index 1372c302e..6c1ff3378 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -35,6 +35,7 @@ #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 { diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h index fff7def4f..a14247dce 100644 --- a/src/expr/proof_checker.h +++ b/src/expr/proof_checker.h @@ -22,6 +22,7 @@ #include "expr/node.h" #include "expr/proof_rule.h" #include "util/statistics_registry.h" +#include "util/stats_histogram.h" namespace CVC4 { diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index e80ed7749..a343b4a37 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -52,7 +52,7 @@ CommandExecutor::CommandExecutor(Options& options) d_symman(new SymbolManager(d_solver.get())), d_smtEngine(d_solver->getSmtEngine()), d_options(options), - d_stats("driver"), + d_stats(), d_result() { } diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 70e6b7b39..88f23ec36 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -84,7 +84,7 @@ void printUsage(Options& opts, bool full) { 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 @@ -192,7 +192,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { 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 @@ -473,7 +473,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { _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); diff --git a/src/main/main.h b/src/main/main.h index 202c74204..37430b507 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -22,6 +22,7 @@ #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 diff --git a/src/preprocessing/passes/ite_simp.h b/src/preprocessing/passes/ite_simp.h index 2e0c581ab..110ce6057 100644 --- a/src/preprocessing/passes/ite_simp.h +++ b/src/preprocessing/passes/ite_simp.h @@ -19,6 +19,7 @@ #include "preprocessing/preprocessing_pass.h" #include "preprocessing/util/ite_utilities.h" +#include "util/stats_histogram.h" namespace CVC4 { namespace preprocessing { diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h index f866125fb..498c507d0 100644 --- a/src/preprocessing/preprocessing_pass.h +++ b/src/preprocessing/preprocessing_pass.h @@ -34,6 +34,7 @@ #include <string> #include "util/statistics_registry.h" +#include "util/stats_timer.h" namespace CVC4 { namespace preprocessing { diff --git a/src/preprocessing/util/ite_utilities.h b/src/preprocessing/util/ite_utilities.h index 80cc39254..856e3be58 100644 --- a/src/preprocessing/util/ite_utilities.h +++ b/src/preprocessing/util/ite_utilities.h @@ -29,6 +29,7 @@ #include "expr/node.h" #include "util/hash.h" #include "util/statistics_registry.h" +#include "util/stats_histogram.h" namespace CVC4 { namespace preprocessing { diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index e346195b0..0882ee2b6 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -31,6 +31,7 @@ #include "proof/clause_id.h" #include "proof/proof_manager.h" #include "util/statistics_registry.h" +#include "util/stats_histogram.h" // Forward declarations. namespace CVC4 { diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index e3571a868..e58060191 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -285,16 +285,16 @@ void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){ 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 */ diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index 7661cb423..f91ed4d1d 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -26,6 +26,7 @@ #include "prop/sat_solver.h" #include "util/resource_manager.h" #include "util/statistics_registry.h" +#include "util/stats_timer.h" namespace CVC4 { namespace prop { diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index fd2c00fc1..935c08e9b 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -289,15 +289,15 @@ MinisatSatSolver::Statistics::~Statistics() { } 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 */ diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h index 92f3c511c..e045dd2ed 100644 --- a/src/smt/proof_post_processor.h +++ b/src/smt/proof_post_processor.h @@ -23,6 +23,7 @@ #include "expr/proof_node_updater.h" #include "smt/witness_form.h" #include "util/statistics_registry.h" +#include "util/stats_histogram.h" namespace CVC4 { diff --git a/src/smt/smt_engine_stats.h b/src/smt/smt_engine_stats.h index 9fa2f4a4c..0f2e4fd50 100644 --- a/src/smt/smt_engine_stats.h +++ b/src/smt/smt_engine_stats.h @@ -18,6 +18,7 @@ #define CVC4__SMT__SMT_ENGINE_STATS_H #include "util/statistics_registry.h" +#include "util/stats_timer.h" namespace CVC4 { namespace smt { diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp index ed781fd5e..8d98475ce 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/approx_simplex.cpp @@ -3001,7 +3001,7 @@ bool ApproxGLPK::guessCoefficientsConstructTableRow(int nid, int M, const Primit 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; } diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h index 46e252ec7..a9b179e31 100644 --- a/src/theory/arith/approx_simplex.h +++ b/src/theory/arith/approx_simplex.h @@ -26,6 +26,7 @@ #include "util/maybe.h" #include "util/rational.h" #include "util/statistics_registry.h" +#include "util/stats_timer.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h index 3ce7199c0..dc4711800 100644 --- a/src/theory/arith/dio_solver.h +++ b/src/theory/arith/dio_solver.h @@ -31,6 +31,7 @@ #include "theory/arith/normal_form.h" #include "util/rational.h" #include "util/statistics_registry.h" +#include "util/stats_timer.h" namespace CVC4 { namespace context { diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h index 3cfbfe5db..df4e5f30e 100644 --- a/src/theory/arith/linear_equality.h +++ b/src/theory/arith/linear_equality.h @@ -38,6 +38,7 @@ #include "theory/arith/tableau.h" #include "util/maybe.h" #include "util/statistics_registry.h" +#include "util/stats_timer.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index fc3d919c3..df399d686 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -70,7 +70,7 @@ bool SimplexDecisionProcedure::standardProcessSignals(TimerStat &timer, IntStat& Debug("recentlyViolated") << "It worked? " - << conflicts.getData() + << conflicts.get() << " " << curr << " " << checkBasicForConflict(curr) << endl; reportConflict(curr); diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index 110093068..5edfc1608 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -62,6 +62,7 @@ #include "util/dense_map.h" #include "util/result.h" #include "util/statistics_registry.h" +#include "util/stats_timer.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 1cf4a2993..1faad2a7a 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -2457,7 +2457,7 @@ void TheoryArithPrivate::subsumption( 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(); @@ -2892,7 +2892,7 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){ 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++; @@ -3018,7 +3018,7 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){ } } - d_statistics.d_inSolveInteger.setData(0); + d_statistics.d_inSolveInteger.set(0); } SimplexDecisionProcedure& TheoryArithPrivate::selectSimplex(bool pass1){ @@ -3532,7 +3532,7 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) 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(); @@ -4366,7 +4366,7 @@ bool TheoryArithPrivate::unenqueuedVariablesAreConsistent(){ 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(); } diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp index 16126b88c..7919892c6 100644 --- a/src/theory/arrays/array_info.cpp +++ b/src/theory/arrays/array_info.cpp @@ -470,20 +470,20 @@ void ArrayInfo::mergeInfo(const TNode a, const TNode b){ 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; } diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index 499f96bfb..174980474 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -25,6 +25,7 @@ #include "context/cdlist.h" #include "expr/node.h" #include "util/statistics_registry.h" +#include "util/stats_timer.h" namespace CVC4 { namespace theory { diff --git a/src/theory/bags/bags_rewriter.h b/src/theory/bags/bags_rewriter.h index 51b2e5438..309b06009 100644 --- a/src/theory/bags/bags_rewriter.h +++ b/src/theory/bags/bags_rewriter.h @@ -20,6 +20,7 @@ #include "theory/bags/rewrites.h" #include "theory/theory_rewriter.h" #include "util/statistics_registry.h" +#include "util/stats_histogram.h" namespace CVC4 { namespace theory { diff --git a/src/theory/bags/bags_statistics.h b/src/theory/bags/bags_statistics.h index f59c43cb6..c6b6c7e7a 100644 --- a/src/theory/bags/bags_statistics.h +++ b/src/theory/bags/bags_statistics.h @@ -19,6 +19,7 @@ #include "theory/bags/rewrites.h" #include "util/statistics_registry.h" +#include "util/stats_histogram.h" namespace CVC4 { namespace theory { diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp index 157985cf1..3b9df3518 100644 --- a/src/theory/bv/abstraction.cpp +++ b/src/theory/bv/abstraction.cpp @@ -528,7 +528,7 @@ void AbstractionModule::finalizeSignatures() 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"; diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h index 726cfd983..e22e221f2 100644 --- a/src/theory/bv/abstraction.h +++ b/src/theory/bv/abstraction.h @@ -25,6 +25,7 @@ #include "expr/node.h" #include "theory/substitutions.h" #include "util/statistics_registry.h" +#include "util/stats_timer.h" namespace CVC4 { namespace theory { diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp index f9b5e80d2..36e77b0b7 100644 --- a/src/theory/bv/bv_quick_check.cpp +++ b/src/theory/bv/bv_quick_check.cpp @@ -347,7 +347,7 @@ Node QuickXPlain::minimizeConflict(TNode confl) { // 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); } diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h index b10eb2811..f509c3cb4 100644 --- a/src/theory/bv/bv_quick_check.h +++ b/src/theory/bv/bv_quick_check.h @@ -27,6 +27,7 @@ #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 { diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp index 7094c831e..9562b69c7 100644 --- a/src/theory/bv/bv_solver_lazy.cpp +++ b/src/theory/bv/bv_solver_lazy.cpp @@ -198,7 +198,7 @@ void BVSolverLazy::sendConflict() 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(); } } diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index 38d94ea27..8f774e552 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -668,7 +668,7 @@ bool AlgebraicSolver::useHeuristic() { 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; } diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 17081bb7b..0aafbde56 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -2001,7 +2001,7 @@ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e) 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; @@ -2070,7 +2070,7 @@ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e) 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) diff --git a/src/theory/strings/sequences_stats.h b/src/theory/strings/sequences_stats.h index 1597e32a6..e4d122faf 100644 --- a/src/theory/strings/sequences_stats.h +++ b/src/theory/strings/sequences_stats.h @@ -21,6 +21,7 @@ #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 { diff --git a/src/theory/theory.h b/src/theory/theory.h index 68a2e1436..1c23d9041 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -37,6 +37,7 @@ #include "theory/trust_node.h" #include "theory/valuation.h" #include "util/statistics_registry.h" +#include "util/stats_timer.h" namespace CVC4 { diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index a599afa23..549d81c16 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -26,6 +26,7 @@ #include "theory/output_channel.h" #include "theory/trust_node.h" #include "util/statistics_registry.h" +#include "util/stats_histogram.h" namespace CVC4 { diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h index 9b9cc79d0..2a95e5bc7 100644 --- a/src/theory/uf/symmetry_breaker.h +++ b/src/theory/uf/symmetry_breaker.h @@ -55,6 +55,7 @@ #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 { diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 518e08c8b..52a811cb9 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -60,6 +60,13 @@ libcvc4_add_sources( 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 diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp index 38505e5e9..c31300077 100644 --- a/src/util/resource_manager.cpp +++ b/src/util/resource_manager.cpp @@ -185,7 +185,7 @@ ResourceManager::ResourceManager(StatisticsRegistry& stats, Options& options) d_options(options) { - d_statistics->d_resourceUnitsUsed.setData(d_cumulativeResourceUsed); + d_statistics->d_resourceUnitsUsed.set(d_cumulativeResourceUsed); } ResourceManager::~ResourceManager() {} @@ -243,7 +243,7 @@ void ResourceManager::spendResource(unsigned amount) { 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" diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp index 6f7f5c485..d824e0f21 100644 --- a/src/util/statistics.cpp +++ b/src/util/statistics.cpp @@ -23,8 +23,6 @@ namespace CVC4 { -std::string StatisticsBase::s_regDelim("::"); - bool StatisticsBase::StatCmp::operator()(const Stat* s1, const Stat* s2) const { return s1->getName() < s2->getName(); } @@ -34,17 +32,14 @@ StatisticsBase::iterator::value_type StatisticsBase::iterator::operator*() const } 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; } @@ -106,10 +101,8 @@ void StatisticsBase::flushInformation(std::ostream &out) const { 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 */ @@ -119,11 +112,9 @@ void StatisticsBase::safeFlushInformation(int fd) const { #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 */ @@ -140,8 +131,4 @@ SExpr StatisticsBase::getStatistic(std::string name) const { } } -void StatisticsBase::setPrefix(const std::string& prefix) { - d_prefix = prefix; -} - }/* CVC4 namespace */ diff --git a/src/util/statistics.h b/src/util/statistics.h index d2380ea08..ce8f4711f 100644 --- a/src/util/statistics.h +++ b/src/util/statistics.h @@ -35,8 +35,6 @@ 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; @@ -45,8 +43,6 @@ protected: /** 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; @@ -78,9 +74,6 @@ public: /** 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; diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp index e169d8745..b439daba8 100644 --- a/src/util/statistics_registry.cpp +++ b/src/util/statistics_registry.cpp @@ -36,124 +36,6 @@ /****************************************************************************/ 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 @@ -194,51 +76,6 @@ void StatisticsRegistry::safeFlushInformation(int fd) const { #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) { @@ -253,5 +90,3 @@ RegisterStatistic::~RegisterStatistic() { } }/* CVC4 namespace */ - -#undef CVC4_USE_STATISTICS diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index b7f76013a..7382bafa3 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -31,6 +31,55 @@ ** 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 @@ -42,506 +91,18 @@ #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 { @@ -573,175 +134,6 @@ public: };/* 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 */ /****************************************************************************/ @@ -750,7 +142,7 @@ class IntegralHistogramStat : public Stat * 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). */ @@ -761,23 +153,13 @@ public: /** 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) { @@ -797,87 +179,6 @@ public: };/* 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). @@ -894,8 +195,6 @@ private: };/* class RegisterStatistic */ -#undef CVC4_USE_STATISTICS - }/* CVC4 namespace */ #endif /* CVC4__STATISTICS_REGISTRY_H */ diff --git a/src/util/stats_base.cpp b/src/util/stats_base.cpp new file mode 100644 index 000000000..f55e2f5ab --- /dev/null +++ b/src/util/stats_base.cpp @@ -0,0 +1,115 @@ +/********************* */ +/*! \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 diff --git a/src/util/stats_base.h b/src/util/stats_base.h new file mode 100644 index 000000000..c9ff2131f --- /dev/null +++ b/src/util/stats_base.h @@ -0,0 +1,278 @@ +/********************* */ +/*! \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 diff --git a/src/util/stats_histogram.h b/src/util/stats_histogram.h new file mode 100644 index 000000000..5528cf010 --- /dev/null +++ b/src/util/stats_histogram.h @@ -0,0 +1,195 @@ +/********************* */ +/*! \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 diff --git a/src/util/stats_timer.cpp b/src/util/stats_timer.cpp new file mode 100644 index 000000000..63d9914d6 --- /dev/null +++ b/src/util/stats_timer.cpp @@ -0,0 +1,104 @@ +/********************* */ +/*! \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 diff --git a/src/util/stats_timer.h b/src/util/stats_timer.h new file mode 100644 index 000000000..a2dfd626a --- /dev/null +++ b/src/util/stats_timer.h @@ -0,0 +1,112 @@ +/********************* */ +/*! \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 diff --git a/src/util/stats_utils.cpp b/src/util/stats_utils.cpp new file mode 100644 index 000000000..893afcb4c --- /dev/null +++ b/src/util/stats_utils.cpp @@ -0,0 +1,38 @@ +/********************* */ +/*! \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 diff --git a/src/util/stats_utils.h b/src/util/stats_utils.h new file mode 100644 index 000000000..df692af1f --- /dev/null +++ b/src/util/stats_utils.h @@ -0,0 +1,35 @@ +/********************* */ +/*! \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 diff --git a/test/unit/util/stats_black.cpp b/test/unit/util/stats_black.cpp index 336bb33fc..3363ba132 100644 --- a/test/unit/util/stats_black.cpp +++ b/test/unit/util/stats_black.cpp @@ -24,23 +24,12 @@ #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 { }; @@ -84,22 +73,22 @@ TEST_F(TestUtilBlackStats, stats) 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; |