diff options
Diffstat (limited to 'src/theory')
110 files changed, 766 insertions, 1261 deletions
diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp index a56835480..f299459f8 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/approx_simplex.cpp @@ -154,29 +154,17 @@ struct CutScratchPad { }; ApproximateStatistics::ApproximateStatistics() - : d_branchMaxDepth("z::approx::branchMaxDepth",0) - , d_branchesMaxOnAVar("z::approx::branchesMaxOnAVar",0) - , d_gaussianElimConstructTime("z::approx::gaussianElimConstruct::time") - , d_gaussianElimConstruct("z::approx::gaussianElimConstruct::calls",0) - , d_averageGuesses("z::approx::averageGuesses") + : d_branchMaxDepth( + smtStatisticsRegistry().registerInt("z::approx::branchMaxDepth")), + d_branchesMaxOnAVar( + smtStatisticsRegistry().registerInt("z::approx::branchesMaxOnAVar")), + d_gaussianElimConstructTime(smtStatisticsRegistry().registerTimer( + "z::approx::gaussianElimConstruct::time")), + d_gaussianElimConstruct(smtStatisticsRegistry().registerInt( + "z::approx::gaussianElimConstruct::calls")), + d_averageGuesses( + smtStatisticsRegistry().registerAverage("z::approx::averageGuesses")) { - smtStatisticsRegistry()->registerStat(&d_branchMaxDepth); - smtStatisticsRegistry()->registerStat(&d_branchesMaxOnAVar); - - smtStatisticsRegistry()->registerStat(&d_gaussianElimConstructTime); - smtStatisticsRegistry()->registerStat(&d_gaussianElimConstruct); - - smtStatisticsRegistry()->registerStat(&d_averageGuesses); -} - -ApproximateStatistics::~ApproximateStatistics(){ - smtStatisticsRegistry()->unregisterStat(&d_branchMaxDepth); - smtStatisticsRegistry()->unregisterStat(&d_branchesMaxOnAVar); - - smtStatisticsRegistry()->unregisterStat(&d_gaussianElimConstructTime); - smtStatisticsRegistry()->unregisterStat(&d_gaussianElimConstruct); - - smtStatisticsRegistry()->unregisterStat(&d_averageGuesses); } Integer ApproximateSimplex::s_defaultMaxDenom(1<<26); diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h index f7266c578..aeced6f10 100644 --- a/src/theory/arith/approx_simplex.h +++ b/src/theory/arith/approx_simplex.h @@ -26,8 +26,7 @@ #include "util/dense_map.h" #include "util/maybe.h" #include "util/rational.h" -#include "util/statistics_registry.h" -#include "util/stats_timer.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { @@ -53,7 +52,6 @@ std::ostream& operator<<(std::ostream& out, MipResult res); class ApproximateStatistics { public: ApproximateStatistics(); - ~ApproximateStatistics(); IntStat d_branchMaxDepth; IntStat d_branchesMaxOnAVar; diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index d434315a3..07582f222 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -45,17 +45,12 @@ ArithStaticLearner::ArithStaticLearner(context::Context* userContext) : ArithStaticLearner::~ArithStaticLearner(){ } -ArithStaticLearner::Statistics::Statistics(): - d_iteMinMaxApplications("theory::arith::iteMinMaxApplications", 0), - d_iteConstantApplications("theory::arith::iteConstantApplications", 0) +ArithStaticLearner::Statistics::Statistics() + : d_iteMinMaxApplications(smtStatisticsRegistry().registerInt( + "theory::arith::iteMinMaxApplications")), + d_iteConstantApplications(smtStatisticsRegistry().registerInt( + "theory::arith::iteConstantApplications")) { - smtStatisticsRegistry()->registerStat(&d_iteMinMaxApplications); - smtStatisticsRegistry()->registerStat(&d_iteConstantApplications); -} - -ArithStaticLearner::Statistics::~Statistics(){ - smtStatisticsRegistry()->unregisterStat(&d_iteMinMaxApplications); - smtStatisticsRegistry()->unregisterStat(&d_iteConstantApplications); } void ArithStaticLearner::staticLearning(TNode n, NodeBuilder& learned) diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h index 053730ec8..7ff674b25 100644 --- a/src/theory/arith/arith_static_learner.h +++ b/src/theory/arith/arith_static_learner.h @@ -24,7 +24,7 @@ #include "context/cdhashmap.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/delta_rational.h" -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace context { @@ -66,7 +66,6 @@ public: IntStat d_iteConstantApplications; Statistics(); - ~Statistics(); }; Statistics d_statistics; diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp index ccad9d866..d74385d3b 100644 --- a/src/theory/arith/attempt_solution_simplex.cpp +++ b/src/theory/arith/attempt_solution_simplex.cpp @@ -36,20 +36,14 @@ AttemptSolutionSDP::AttemptSolutionSDP(LinearEqualityModule& linEq, ErrorSet& er , d_statistics() { } -AttemptSolutionSDP::Statistics::Statistics(): - d_searchTime("theory::arith::attempt::searchTime"), - d_queueTime("theory::arith::attempt::queueTime"), - d_conflicts("theory::arith::attempt::conflicts", 0) +AttemptSolutionSDP::Statistics::Statistics() + : d_searchTime(smtStatisticsRegistry().registerTimer( + "theory::arith::attempt::searchTime")), + d_queueTime(smtStatisticsRegistry().registerTimer( + "theory::arith::attempt::queueTime")), + d_conflicts(smtStatisticsRegistry().registerInt( + "theory::arith::attempt::conflicts")) { - smtStatisticsRegistry()->registerStat(&d_searchTime); - smtStatisticsRegistry()->registerStat(&d_queueTime); - smtStatisticsRegistry()->registerStat(&d_conflicts); -} - -AttemptSolutionSDP::Statistics::~Statistics(){ - smtStatisticsRegistry()->unregisterStat(&d_searchTime); - smtStatisticsRegistry()->unregisterStat(&d_queueTime); - smtStatisticsRegistry()->unregisterStat(&d_conflicts); } bool AttemptSolutionSDP::matchesNewValue(const DenseMap<DeltaRational>& nv, ArithVar v) const{ diff --git a/src/theory/arith/attempt_solution_simplex.h b/src/theory/arith/attempt_solution_simplex.h index 25676a8b6..8c6b28b60 100644 --- a/src/theory/arith/attempt_solution_simplex.h +++ b/src/theory/arith/attempt_solution_simplex.h @@ -55,9 +55,9 @@ #pragma once -#include "theory/arith/simplex.h" #include "theory/arith/approx_simplex.h" -#include "util/statistics_registry.h" +#include "theory/arith/simplex.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { @@ -87,7 +87,6 @@ public: IntStat d_conflicts; Statistics(); - ~Statistics(); } d_statistics; };/* class AttemptSolutionSDP */ diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index ff0b46338..23bdb20f6 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -90,32 +90,22 @@ void ArithCongruenceManager::finishInit(eq::EqualityEngine* ee, d_pfee = pfee; } -ArithCongruenceManager::Statistics::Statistics(): - d_watchedVariables("theory::arith::congruence::watchedVariables", 0), - d_watchedVariableIsZero("theory::arith::congruence::watchedVariableIsZero", 0), - d_watchedVariableIsNotZero("theory::arith::congruence::watchedVariableIsNotZero", 0), - d_equalsConstantCalls("theory::arith::congruence::equalsConstantCalls", 0), - d_propagations("theory::arith::congruence::propagations", 0), - d_propagateConstraints("theory::arith::congruence::propagateConstraints", 0), - d_conflicts("theory::arith::congruence::conflicts", 0) +ArithCongruenceManager::Statistics::Statistics() + : d_watchedVariables(smtStatisticsRegistry().registerInt( + "theory::arith::congruence::watchedVariables")), + d_watchedVariableIsZero(smtStatisticsRegistry().registerInt( + "theory::arith::congruence::watchedVariableIsZero")), + d_watchedVariableIsNotZero(smtStatisticsRegistry().registerInt( + "theory::arith::congruence::watchedVariableIsNotZero")), + d_equalsConstantCalls(smtStatisticsRegistry().registerInt( + "theory::arith::congruence::equalsConstantCalls")), + d_propagations(smtStatisticsRegistry().registerInt( + "theory::arith::congruence::propagations")), + d_propagateConstraints(smtStatisticsRegistry().registerInt( + "theory::arith::congruence::propagateConstraints")), + d_conflicts(smtStatisticsRegistry().registerInt( + "theory::arith::congruence::conflicts")) { - smtStatisticsRegistry()->registerStat(&d_watchedVariables); - smtStatisticsRegistry()->registerStat(&d_watchedVariableIsZero); - smtStatisticsRegistry()->registerStat(&d_watchedVariableIsNotZero); - smtStatisticsRegistry()->registerStat(&d_equalsConstantCalls); - smtStatisticsRegistry()->registerStat(&d_propagations); - smtStatisticsRegistry()->registerStat(&d_propagateConstraints); - smtStatisticsRegistry()->registerStat(&d_conflicts); -} - -ArithCongruenceManager::Statistics::~Statistics(){ - smtStatisticsRegistry()->unregisterStat(&d_watchedVariables); - smtStatisticsRegistry()->unregisterStat(&d_watchedVariableIsZero); - smtStatisticsRegistry()->unregisterStat(&d_watchedVariableIsNotZero); - smtStatisticsRegistry()->unregisterStat(&d_equalsConstantCalls); - smtStatisticsRegistry()->unregisterStat(&d_propagations); - smtStatisticsRegistry()->unregisterStat(&d_propagateConstraints); - smtStatisticsRegistry()->unregisterStat(&d_conflicts); } ArithCongruenceManager::ArithCongruenceNotify::ArithCongruenceNotify(ArithCongruenceManager& acm) diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index c8abba880..6032adcc8 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -24,14 +24,14 @@ #include "context/cdlist.h" #include "context/cdmaybe.h" #include "context/cdtrail_queue.h" -#include "theory/arith/arithvar.h" #include "theory/arith/arith_utilities.h" +#include "theory/arith/arithvar.h" #include "theory/arith/callbacks.h" #include "theory/arith/constraint_forward.h" #include "theory/trust_node.h" #include "theory/uf/equality_engine_notify.h" #include "util/dense_map.h" -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" namespace cvc5 { @@ -291,7 +291,6 @@ private: IntStat d_conflicts; Statistics(); - ~Statistics(); } d_statistics; };/* class ArithCongruenceManager */ diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index eb2078c11..dcd699d88 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -1003,18 +1003,12 @@ ConstraintDatabase::~ConstraintDatabase(){ Assert(d_nodetoConstraintMap.empty()); } -ConstraintDatabase::Statistics::Statistics(): - d_unatePropagateCalls("theory::arith::cd::unatePropagateCalls", 0), - d_unatePropagateImplications("theory::arith::cd::unatePropagateImplications", 0) +ConstraintDatabase::Statistics::Statistics() + : d_unatePropagateCalls(smtStatisticsRegistry().registerInt( + "theory::arith::cd::unatePropagateCalls")), + d_unatePropagateImplications(smtStatisticsRegistry().registerInt( + "theory::arith::cd::unatePropagateImplications")) { - smtStatisticsRegistry()->registerStat(&d_unatePropagateCalls); - smtStatisticsRegistry()->registerStat(&d_unatePropagateImplications); - -} - -ConstraintDatabase::Statistics::~Statistics(){ - smtStatisticsRegistry()->unregisterStat(&d_unatePropagateCalls); - smtStatisticsRegistry()->unregisterStat(&d_unatePropagateImplications); } void ConstraintDatabase::deleteConstraintAndNegation(ConstraintP c){ diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index bd27c6034..ecd5b10fb 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -92,7 +92,7 @@ #include "theory/arith/delta_rational.h" #include "theory/arith/proof_macros.h" #include "theory/trust_node.h" -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" namespace cvc5 { @@ -1270,7 +1270,6 @@ private: IntStat d_unatePropagateImplications; Statistics(); - ~Statistics(); } d_statistics; }; /* ConstraintDatabase */ diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index c54af4eed..1ad23f8ca 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -54,33 +54,19 @@ DioSolver::DioSolver(context::Context* ctxt) d_pureSubstitionIter(ctxt, 0), d_decompositionLemmaQueue(ctxt) {} -DioSolver::Statistics::Statistics() : - d_conflictCalls("theory::arith::dio::conflictCalls",0), - d_cutCalls("theory::arith::dio::cutCalls",0), - d_cuts("theory::arith::dio::cuts",0), - d_conflicts("theory::arith::dio::conflicts",0), - d_conflictTimer("theory::arith::dio::conflictTimer"), - d_cutTimer("theory::arith::dio::cutTimer") +DioSolver::Statistics::Statistics() + : d_conflictCalls(smtStatisticsRegistry().registerInt( + "theory::arith::dio::conflictCalls")), + d_cutCalls( + smtStatisticsRegistry().registerInt("theory::arith::dio::cutCalls")), + d_cuts(smtStatisticsRegistry().registerInt("theory::arith::dio::cuts")), + d_conflicts( + smtStatisticsRegistry().registerInt("theory::arith::dio::conflicts")), + d_conflictTimer(smtStatisticsRegistry().registerTimer( + "theory::arith::dio::conflictTimer")), + d_cutTimer( + smtStatisticsRegistry().registerTimer("theory::arith::dio::cutTimer")) { - smtStatisticsRegistry()->registerStat(&d_conflictCalls); - smtStatisticsRegistry()->registerStat(&d_cutCalls); - - smtStatisticsRegistry()->registerStat(&d_cuts); - smtStatisticsRegistry()->registerStat(&d_conflicts); - - smtStatisticsRegistry()->registerStat(&d_conflictTimer); - smtStatisticsRegistry()->registerStat(&d_cutTimer); -} - -DioSolver::Statistics::~Statistics(){ - smtStatisticsRegistry()->unregisterStat(&d_conflictCalls); - smtStatisticsRegistry()->unregisterStat(&d_cutCalls); - - smtStatisticsRegistry()->unregisterStat(&d_cuts); - smtStatisticsRegistry()->unregisterStat(&d_conflicts); - - smtStatisticsRegistry()->unregisterStat(&d_conflictTimer); - smtStatisticsRegistry()->unregisterStat(&d_cutTimer); } bool DioSolver::queueConditions(TrailIndex t){ diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h index 5e020d66e..0fac563bb 100644 --- a/src/theory/arith/dio_solver.h +++ b/src/theory/arith/dio_solver.h @@ -28,8 +28,7 @@ #include "context/cdqueue.h" #include "theory/arith/normal_form.h" #include "util/rational.h" -#include "util/statistics_registry.h" -#include "util/stats_timer.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace context { @@ -413,7 +412,6 @@ public: TimerStat d_cutTimer; Statistics(); - ~Statistics(); }; Statistics d_statistics; diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp index 26bde0f62..13cc29a58 100644 --- a/src/theory/arith/dual_simplex.cpp +++ b/src/theory/arith/dual_simplex.cpp @@ -35,29 +35,21 @@ DualSimplexDecisionProcedure::DualSimplexDecisionProcedure(LinearEqualityModule& , d_statistics(d_pivots) { } -DualSimplexDecisionProcedure::Statistics::Statistics(uint32_t& pivots): - d_statUpdateConflicts("theory::arith::dual::UpdateConflicts", 0), - d_processSignalsTime("theory::arith::dual::findConflictOnTheQueueTime"), - d_simplexConflicts("theory::arith::dual::simplexConflicts",0), - d_recentViolationCatches("theory::arith::dual::recentViolationCatches",0), - d_searchTime("theory::arith::dual::searchTime"), - d_finalCheckPivotCounter("theory::arith::dual::lastPivots", pivots) +DualSimplexDecisionProcedure::Statistics::Statistics(uint32_t& pivots) + : d_statUpdateConflicts(smtStatisticsRegistry().registerInt( + "theory::arith::dual::UpdateConflicts")), + d_processSignalsTime(smtStatisticsRegistry().registerTimer( + "theory::arith::dual::findConflictOnTheQueueTime")), + d_simplexConflicts(smtStatisticsRegistry().registerInt( + "theory::arith::dual::simplexConflicts")), + d_recentViolationCatches(smtStatisticsRegistry().registerInt( + "theory::arith::dual::recentViolationCatches")), + d_searchTime(smtStatisticsRegistry().registerTimer( + "theory::arith::dual::searchTime")), + d_finalCheckPivotCounter( + smtStatisticsRegistry().registerReference<uint32_t>( + "theory::arith::dual::lastPivots", pivots)) { - smtStatisticsRegistry()->registerStat(&d_statUpdateConflicts); - smtStatisticsRegistry()->registerStat(&d_processSignalsTime); - smtStatisticsRegistry()->registerStat(&d_simplexConflicts); - smtStatisticsRegistry()->registerStat(&d_recentViolationCatches); - smtStatisticsRegistry()->registerStat(&d_searchTime); - smtStatisticsRegistry()->registerStat(&d_finalCheckPivotCounter); -} - -DualSimplexDecisionProcedure::Statistics::~Statistics(){ - smtStatisticsRegistry()->unregisterStat(&d_statUpdateConflicts); - smtStatisticsRegistry()->unregisterStat(&d_processSignalsTime); - smtStatisticsRegistry()->unregisterStat(&d_simplexConflicts); - smtStatisticsRegistry()->unregisterStat(&d_recentViolationCatches); - smtStatisticsRegistry()->unregisterStat(&d_searchTime); - smtStatisticsRegistry()->unregisterStat(&d_finalCheckPivotCounter); } Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){ diff --git a/src/theory/arith/dual_simplex.h b/src/theory/arith/dual_simplex.h index 7113bd329..e1021d2a5 100644 --- a/src/theory/arith/dual_simplex.h +++ b/src/theory/arith/dual_simplex.h @@ -56,7 +56,7 @@ #pragma once #include "theory/arith/simplex.h" -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { @@ -108,7 +108,6 @@ private: ReferenceStat<uint32_t> d_finalCheckPivotCounter; Statistics(uint32_t& pivots); - ~Statistics(); } d_statistics; };/* class DualSimplexDecisionProcedure */ diff --git a/src/theory/arith/error_set.cpp b/src/theory/arith/error_set.cpp index c397efb9a..b7c35a7fd 100644 --- a/src/theory/arith/error_set.cpp +++ b/src/theory/arith/error_set.cpp @@ -128,29 +128,20 @@ void ErrorInformation::setAmount(const DeltaRational& am){ (*d_amount) = am; } -ErrorSet::Statistics::Statistics(): - d_enqueues("theory::arith::pqueue::enqueues", 0), - d_enqueuesCollection("theory::arith::pqueue::enqueuesCollection", 0), - d_enqueuesDiffMode("theory::arith::pqueue::enqueuesDiffMode", 0), - d_enqueuesVarOrderMode("theory::arith::pqueue::enqueuesVarOrderMode", 0), - d_enqueuesCollectionDuplicates("theory::arith::pqueue::enqueuesCollectionDuplicates", 0), - d_enqueuesVarOrderModeDuplicates("theory::arith::pqueue::enqueuesVarOrderModeDuplicates", 0) +ErrorSet::Statistics::Statistics() + : d_enqueues( + smtStatisticsRegistry().registerInt("theory::arith::pqueue::enqueues")), + d_enqueuesCollection(smtStatisticsRegistry().registerInt( + "theory::arith::pqueue::enqueuesCollection")), + d_enqueuesDiffMode(smtStatisticsRegistry().registerInt( + "theory::arith::pqueue::enqueuesDiffMode")), + d_enqueuesVarOrderMode(smtStatisticsRegistry().registerInt( + "theory::arith::pqueue::enqueuesVarOrderMode")), + d_enqueuesCollectionDuplicates(smtStatisticsRegistry().registerInt( + "theory::arith::pqueue::enqueuesCollectionDuplicates")), + d_enqueuesVarOrderModeDuplicates(smtStatisticsRegistry().registerInt( + "theory::arith::pqueue::enqueuesVarOrderModeDuplicates")) { - smtStatisticsRegistry()->registerStat(&d_enqueues); - smtStatisticsRegistry()->registerStat(&d_enqueuesCollection); - smtStatisticsRegistry()->registerStat(&d_enqueuesDiffMode); - smtStatisticsRegistry()->registerStat(&d_enqueuesVarOrderMode); - smtStatisticsRegistry()->registerStat(&d_enqueuesCollectionDuplicates); - smtStatisticsRegistry()->registerStat(&d_enqueuesVarOrderModeDuplicates); -} - -ErrorSet::Statistics::~Statistics(){ - smtStatisticsRegistry()->unregisterStat(&d_enqueues); - smtStatisticsRegistry()->unregisterStat(&d_enqueuesCollection); - smtStatisticsRegistry()->unregisterStat(&d_enqueuesDiffMode); - smtStatisticsRegistry()->unregisterStat(&d_enqueuesVarOrderMode); - smtStatisticsRegistry()->unregisterStat(&d_enqueuesCollectionDuplicates); - smtStatisticsRegistry()->unregisterStat(&d_enqueuesVarOrderModeDuplicates); } ErrorSet::ErrorSet(ArithVariables& vars, diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h index 21cc557b6..5585bf76f 100644 --- a/src/theory/arith/error_set.h +++ b/src/theory/arith/error_set.h @@ -30,7 +30,7 @@ #include "theory/arith/partial_model.h" #include "theory/arith/tableau_sizes.h" #include "util/bin_heap.h" -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { @@ -407,7 +407,6 @@ private: IntStat d_enqueuesVarOrderModeDuplicates; Statistics(); - ~Statistics(); }; Statistics d_statistics; diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp index 6ab5c05d7..de13f4eb9 100644 --- a/src/theory/arith/fc_simplex.cpp +++ b/src/theory/arith/fc_simplex.cpp @@ -20,7 +20,7 @@ #include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" #include "theory/arith/error_set.h" -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" using namespace std; @@ -28,62 +28,42 @@ namespace cvc5 { namespace theory { namespace arith { - -FCSimplexDecisionProcedure::FCSimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc) - : SimplexDecisionProcedure(linEq, errors, conflictChannel, tvmalloc) - , d_focusSize(0) - , d_focusErrorVar(ARITHVAR_SENTINEL) - , d_focusCoefficients() - , d_pivotBudget(0) - , d_prevWitnessImprovement(AntiProductive) - , d_witnessImprovementInARow(0) - , d_sgnDisagreements() - , d_statistics(d_pivots) +FCSimplexDecisionProcedure::FCSimplexDecisionProcedure( + LinearEqualityModule& linEq, + ErrorSet& errors, + RaiseConflict conflictChannel, + TempVarMalloc tvmalloc) + : SimplexDecisionProcedure(linEq, errors, conflictChannel, tvmalloc), + d_focusSize(0), + d_focusErrorVar(ARITHVAR_SENTINEL), + d_focusCoefficients(), + d_pivotBudget(0), + d_prevWitnessImprovement(AntiProductive), + d_witnessImprovementInARow(0), + d_sgnDisagreements(), + d_statistics("theory::arith::FC::", d_pivots) { } -FCSimplexDecisionProcedure::Statistics::Statistics(uint32_t& pivots): - d_initialSignalsTime("theory::arith::FC::initialProcessTime"), - d_initialConflicts("theory::arith::FC::UpdateConflicts", 0), - d_fcFoundUnsat("theory::arith::FC::FoundUnsat", 0), - d_fcFoundSat("theory::arith::FC::FoundSat", 0), - d_fcMissed("theory::arith::FC::Missed", 0), - d_fcTimer("theory::arith::FC::Timer"), - d_fcFocusConstructionTimer("theory::arith::FC::Construction"), - d_selectUpdateForDualLike("theory::arith::FC::selectUpdateForDualLike"), - d_selectUpdateForPrimal("theory::arith::FC::selectUpdateForPrimal"), - d_finalCheckPivotCounter("theory::arith::FC::lastPivots", pivots) +FCSimplexDecisionProcedure::Statistics::Statistics(const std::string& name, + uint32_t& pivots) + : d_initialSignalsTime( + smtStatisticsRegistry().registerTimer(name + "initialProcessTime")), + d_initialConflicts( + smtStatisticsRegistry().registerInt(name + "UpdateConflicts")), + d_fcFoundUnsat(smtStatisticsRegistry().registerInt(name + "FoundUnsat")), + d_fcFoundSat(smtStatisticsRegistry().registerInt(name + "FoundSat")), + d_fcMissed(smtStatisticsRegistry().registerInt(name + "Missed")), + d_fcTimer(smtStatisticsRegistry().registerTimer(name + "Timer")), + d_fcFocusConstructionTimer( + smtStatisticsRegistry().registerTimer(name + "Construction")), + d_selectUpdateForDualLike(smtStatisticsRegistry().registerTimer( + name + "selectUpdateForDualLike")), + d_selectUpdateForPrimal(smtStatisticsRegistry().registerTimer( + name + "selectUpdateForPrimal")), + d_finalCheckPivotCounter( + smtStatisticsRegistry().registerReference<uint32_t>( + name + "lastPivots", pivots)) { - smtStatisticsRegistry()->registerStat(&d_initialSignalsTime); - smtStatisticsRegistry()->registerStat(&d_initialConflicts); - - smtStatisticsRegistry()->registerStat(&d_fcFoundUnsat); - smtStatisticsRegistry()->registerStat(&d_fcFoundSat); - smtStatisticsRegistry()->registerStat(&d_fcMissed); - - smtStatisticsRegistry()->registerStat(&d_fcTimer); - smtStatisticsRegistry()->registerStat(&d_fcFocusConstructionTimer); - - smtStatisticsRegistry()->registerStat(&d_selectUpdateForDualLike); - smtStatisticsRegistry()->registerStat(&d_selectUpdateForPrimal); - - smtStatisticsRegistry()->registerStat(&d_finalCheckPivotCounter); -} - -FCSimplexDecisionProcedure::Statistics::~Statistics(){ - smtStatisticsRegistry()->unregisterStat(&d_initialSignalsTime); - smtStatisticsRegistry()->unregisterStat(&d_initialConflicts); - - smtStatisticsRegistry()->unregisterStat(&d_fcFoundUnsat); - smtStatisticsRegistry()->unregisterStat(&d_fcFoundSat); - smtStatisticsRegistry()->unregisterStat(&d_fcMissed); - - smtStatisticsRegistry()->unregisterStat(&d_fcTimer); - smtStatisticsRegistry()->unregisterStat(&d_fcFocusConstructionTimer); - - smtStatisticsRegistry()->unregisterStat(&d_selectUpdateForDualLike); - smtStatisticsRegistry()->unregisterStat(&d_selectUpdateForPrimal); - - smtStatisticsRegistry()->unregisterStat(&d_finalCheckPivotCounter); } Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){ diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h index 6c391393d..599b324ce 100644 --- a/src/theory/arith/fc_simplex.h +++ b/src/theory/arith/fc_simplex.h @@ -60,7 +60,7 @@ #include "theory/arith/simplex.h" #include "theory/arith/simplex_update.h" #include "util/dense_map.h" -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { @@ -250,8 +250,7 @@ private: ReferenceStat<uint32_t> d_finalCheckPivotCounter; - Statistics(uint32_t& pivots); - ~Statistics(); + Statistics(const std::string& name, uint32_t& pivots); } d_statistics; };/* class FCSimplexDecisionProcedure */ diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp index 25364fc24..90c17be4a 100644 --- a/src/theory/arith/inference_manager.cpp +++ b/src/theory/arith/inference_manager.cpp @@ -27,7 +27,7 @@ namespace arith { InferenceManager::InferenceManager(TheoryArith& ta, ArithState& astate, ProofNodeManager* pnm) - : InferenceManagerBuffered(ta, astate, pnm, "theory::arith") + : InferenceManagerBuffered(ta, astate, pnm, "theory::arith::") { } diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp index c9d65a0fc..57dbdfc82 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear_equality.cpp @@ -65,42 +65,26 @@ LinearEqualityModule::LinearEqualityModule(ArithVariables& vars, Tableau& t, Bou d_trackCallback(this) {} -LinearEqualityModule::Statistics::Statistics(): - d_statPivots("theory::arith::pivots",0), - d_statUpdates("theory::arith::updates",0), - d_pivotTime("theory::arith::pivotTime"), - d_adjTime("theory::arith::adjTime"), - d_weakeningAttempts("theory::arith::weakening::attempts",0), - d_weakeningSuccesses("theory::arith::weakening::success",0), - d_weakenings("theory::arith::weakening::total",0), - d_weakenTime("theory::arith::weakening::time"), - d_forceTime("theory::arith::forcing::time") +LinearEqualityModule::Statistics::Statistics() + : d_statPivots( + smtStatisticsRegistry().registerInt("theory::arith::pivots")), + d_statUpdates( + smtStatisticsRegistry().registerInt("theory::arith::updates")), + d_pivotTime( + smtStatisticsRegistry().registerTimer("theory::arith::pivotTime")), + d_adjTime( + smtStatisticsRegistry().registerTimer("theory::arith::adjTime")), + d_weakeningAttempts(smtStatisticsRegistry().registerInt( + "theory::arith::weakening::attempts")), + d_weakeningSuccesses(smtStatisticsRegistry().registerInt( + "theory::arith::weakening::success")), + d_weakenings(smtStatisticsRegistry().registerInt( + "theory::arith::weakening::total")), + d_weakenTime(smtStatisticsRegistry().registerTimer( + "theory::arith::weakening::time")), + d_forceTime( + smtStatisticsRegistry().registerTimer("theory::arith::forcing::time")) { - smtStatisticsRegistry()->registerStat(&d_statPivots); - smtStatisticsRegistry()->registerStat(&d_statUpdates); - - smtStatisticsRegistry()->registerStat(&d_pivotTime); - smtStatisticsRegistry()->registerStat(&d_adjTime); - - smtStatisticsRegistry()->registerStat(&d_weakeningAttempts); - smtStatisticsRegistry()->registerStat(&d_weakeningSuccesses); - smtStatisticsRegistry()->registerStat(&d_weakenings); - smtStatisticsRegistry()->registerStat(&d_weakenTime); - smtStatisticsRegistry()->registerStat(&d_forceTime); -} - -LinearEqualityModule::Statistics::~Statistics(){ - smtStatisticsRegistry()->unregisterStat(&d_statPivots); - smtStatisticsRegistry()->unregisterStat(&d_statUpdates); - smtStatisticsRegistry()->unregisterStat(&d_pivotTime); - smtStatisticsRegistry()->unregisterStat(&d_adjTime); - - - smtStatisticsRegistry()->unregisterStat(&d_weakeningAttempts); - smtStatisticsRegistry()->unregisterStat(&d_weakeningSuccesses); - smtStatisticsRegistry()->unregisterStat(&d_weakenings); - smtStatisticsRegistry()->unregisterStat(&d_weakenTime); - smtStatisticsRegistry()->unregisterStat(&d_forceTime); } void LinearEqualityModule::includeBoundUpdate(ArithVar v, const BoundsInfo& prev){ diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h index e07ed6051..276c8e63e 100644 --- a/src/theory/arith/linear_equality.h +++ b/src/theory/arith/linear_equality.h @@ -38,8 +38,7 @@ #include "theory/arith/simplex_update.h" #include "theory/arith/tableau.h" #include "util/maybe.h" -#include "util/statistics_registry.h" -#include "util/stats_timer.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { @@ -714,7 +713,6 @@ private: TimerStat d_forceTime; Statistics(); - ~Statistics(); }; mutable Statistics d_statistics; diff --git a/src/theory/arith/nl/stats.cpp b/src/theory/arith/nl/stats.cpp index fa06fa73e..b20214f59 100644 --- a/src/theory/arith/nl/stats.cpp +++ b/src/theory/arith/nl/stats.cpp @@ -23,17 +23,9 @@ namespace arith { namespace nl { NlStats::NlStats() - : d_mbrRuns("nl::mbrRuns", 0), - d_checkRuns("nl::checkRuns", 0) + : d_mbrRuns(smtStatisticsRegistry().registerInt("nl::mbrRuns")), + d_checkRuns(smtStatisticsRegistry().registerInt("nl::checkRuns")) { - smtStatisticsRegistry()->registerStat(&d_mbrRuns); - smtStatisticsRegistry()->registerStat(&d_checkRuns); -} - -NlStats::~NlStats() -{ - smtStatisticsRegistry()->unregisterStat(&d_mbrRuns); - smtStatisticsRegistry()->unregisterStat(&d_checkRuns); } } // namespace nl diff --git a/src/theory/arith/nl/stats.h b/src/theory/arith/nl/stats.h index 988b647a6..4f30031be 100644 --- a/src/theory/arith/nl/stats.h +++ b/src/theory/arith/nl/stats.h @@ -18,7 +18,7 @@ #ifndef CVC5__THEORY__ARITH__NL__STATS_H #define CVC5__THEORY__ARITH__NL__STATS_H -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { @@ -32,7 +32,6 @@ class NlStats { public: NlStats(); - ~NlStats(); /** * Number of calls to NonlinearExtension::modelBasedRefinement. Notice this * may make multiple calls to NonlinearExtension::checkLastCall. diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 88816b311..781f132d7 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -22,6 +22,7 @@ #include "theory/arith/error_set.h" #include "theory/arith/linear_equality.h" #include "theory/arith/tableau.h" +#include "util/statistics_value.h" using namespace std; diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index 9cbb5bac2..fe5b26eaa 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -62,8 +62,7 @@ #include "theory/arith/partial_model.h" #include "util/dense_map.h" #include "util/result.h" -#include "util/statistics_registry.h" -#include "util/stats_timer.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp index fc1e06441..1b22bc81c 100644 --- a/src/theory/arith/soi_simplex.cpp +++ b/src/theory/arith/soi_simplex.cpp @@ -23,7 +23,7 @@ #include "theory/arith/constraint.h" #include "theory/arith/error_set.h" #include "theory/arith/tableau.h" -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" using namespace std; @@ -31,72 +31,45 @@ namespace cvc5 { namespace theory { namespace arith { - -SumOfInfeasibilitiesSPD::SumOfInfeasibilitiesSPD(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc) - : SimplexDecisionProcedure(linEq, errors, conflictChannel, tvmalloc) - , d_soiVar(ARITHVAR_SENTINEL) - , d_pivotBudget(0) - , d_prevWitnessImprovement(AntiProductive) - , d_witnessImprovementInARow(0) - , d_sgnDisagreements() - , d_statistics(d_pivots) +SumOfInfeasibilitiesSPD::SumOfInfeasibilitiesSPD(LinearEqualityModule& linEq, + ErrorSet& errors, + RaiseConflict conflictChannel, + TempVarMalloc tvmalloc) + : SimplexDecisionProcedure(linEq, errors, conflictChannel, tvmalloc), + d_soiVar(ARITHVAR_SENTINEL), + d_pivotBudget(0), + d_prevWitnessImprovement(AntiProductive), + d_witnessImprovementInARow(0), + d_sgnDisagreements(), + d_statistics("theory::arith::SOI", d_pivots) { } -SumOfInfeasibilitiesSPD::Statistics::Statistics(uint32_t& pivots): - d_initialSignalsTime("theory::arith::SOI::initialProcessTime"), - d_initialConflicts("theory::arith::SOI::UpdateConflicts", 0), - d_soiFoundUnsat("theory::arith::SOI::FoundUnsat", 0), - d_soiFoundSat("theory::arith::SOI::FoundSat", 0), - d_soiMissed("theory::arith::SOI::Missed", 0), - d_soiConflicts("theory::arith::SOI::ConfMin::num", 0), - d_hasToBeMinimal("theory::arith::SOI::HasToBeMin", 0), - d_maybeNotMinimal("theory::arith::SOI::MaybeNotMin", 0), - d_soiTimer("theory::arith::SOI::Time"), - d_soiFocusConstructionTimer("theory::arith::SOI::Construction"), - d_soiConflictMinimization("theory::arith::SOI::Conflict::Minimization"), - d_selectUpdateForSOI("theory::arith::SOI::selectSOI"), - d_finalCheckPivotCounter("theory::arith::SOI::lastPivots", pivots) +SumOfInfeasibilitiesSPD::Statistics::Statistics(const std::string& name, + uint32_t& pivots) + : d_initialSignalsTime( + smtStatisticsRegistry().registerTimer(name + "initialProcessTime")), + d_initialConflicts( + smtStatisticsRegistry().registerInt(name + "UpdateConflicts")), + d_soiFoundUnsat(smtStatisticsRegistry().registerInt(name + "FoundUnsat")), + d_soiFoundSat(smtStatisticsRegistry().registerInt(name + "FoundSat")), + d_soiMissed(smtStatisticsRegistry().registerInt(name + "Missed")), + d_soiConflicts( + smtStatisticsRegistry().registerInt(name + "ConfMin::num")), + d_hasToBeMinimal( + smtStatisticsRegistry().registerInt(name + "HasToBeMin")), + d_maybeNotMinimal( + smtStatisticsRegistry().registerInt(name + "MaybeNotMin")), + d_soiTimer(smtStatisticsRegistry().registerTimer(name + "Time")), + d_soiFocusConstructionTimer( + smtStatisticsRegistry().registerTimer(name + "Construction")), + d_soiConflictMinimization(smtStatisticsRegistry().registerTimer( + name + "Conflict::Minimization")), + d_selectUpdateForSOI( + smtStatisticsRegistry().registerTimer(name + "selectSOI")), + d_finalCheckPivotCounter( + smtStatisticsRegistry().registerReference<uint32_t>( + name + "lastPivots", pivots)) { - smtStatisticsRegistry()->registerStat(&d_initialSignalsTime); - smtStatisticsRegistry()->registerStat(&d_initialConflicts); - - smtStatisticsRegistry()->registerStat(&d_soiFoundUnsat); - smtStatisticsRegistry()->registerStat(&d_soiFoundSat); - smtStatisticsRegistry()->registerStat(&d_soiMissed); - - smtStatisticsRegistry()->registerStat(&d_soiConflicts); - smtStatisticsRegistry()->registerStat(&d_hasToBeMinimal); - smtStatisticsRegistry()->registerStat(&d_maybeNotMinimal); - - smtStatisticsRegistry()->registerStat(&d_soiTimer); - smtStatisticsRegistry()->registerStat(&d_soiFocusConstructionTimer); - - smtStatisticsRegistry()->registerStat(&d_soiConflictMinimization); - - smtStatisticsRegistry()->registerStat(&d_selectUpdateForSOI); - - smtStatisticsRegistry()->registerStat(&d_finalCheckPivotCounter); -} - -SumOfInfeasibilitiesSPD::Statistics::~Statistics(){ - smtStatisticsRegistry()->unregisterStat(&d_initialSignalsTime); - smtStatisticsRegistry()->unregisterStat(&d_initialConflicts); - - smtStatisticsRegistry()->unregisterStat(&d_soiFoundUnsat); - smtStatisticsRegistry()->unregisterStat(&d_soiFoundSat); - smtStatisticsRegistry()->unregisterStat(&d_soiMissed); - - smtStatisticsRegistry()->unregisterStat(&d_soiConflicts); - smtStatisticsRegistry()->unregisterStat(&d_hasToBeMinimal); - smtStatisticsRegistry()->unregisterStat(&d_maybeNotMinimal); - - smtStatisticsRegistry()->unregisterStat(&d_soiTimer); - smtStatisticsRegistry()->unregisterStat(&d_soiFocusConstructionTimer); - - smtStatisticsRegistry()->unregisterStat(&d_soiConflictMinimization); - - smtStatisticsRegistry()->unregisterStat(&d_selectUpdateForSOI); - smtStatisticsRegistry()->unregisterStat(&d_finalCheckPivotCounter); } Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){ diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h index 7b2656752..5bff01d99 100644 --- a/src/theory/arith/soi_simplex.h +++ b/src/theory/arith/soi_simplex.h @@ -59,7 +59,7 @@ #include "theory/arith/simplex.h" #include "theory/arith/simplex_update.h" #include "util/dense_map.h" -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { @@ -236,8 +236,7 @@ private: ReferenceStat<uint32_t> d_finalCheckPivotCounter; - Statistics(uint32_t& pivots); - ~Statistics(); + Statistics(const std::string& name, uint32_t& pivots); } d_statistics; };/* class FCSimplexDecisionProcedure */ diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 4232d28dc..181a816c2 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -43,22 +43,20 @@ TheoryArith::TheoryArith(context::Context* c, : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, pnm), d_internal( new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo, pnm)), - d_ppRewriteTimer("theory::arith::ppRewriteTimer"), + d_ppRewriteTimer(smtStatisticsRegistry().registerTimer( + "theory::arith::ppRewriteTimer")), d_ppPfGen(pnm, c, "Arith::ppRewrite"), d_astate(*d_internal, c, u, valuation), d_im(*this, d_astate, pnm), d_nonlinearExtension(nullptr), d_arithPreproc(d_astate, d_im, pnm, logicInfo) { - smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer); - // indicate we are using the theory state object and inference manager d_theoryState = &d_astate; d_inferManager = &d_im; } TheoryArith::~TheoryArith(){ - smtStatisticsRegistry()->unregisterStat(&d_ppRewriteTimer); delete d_internal; } diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 9a13944f3..e7ff27413 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -72,7 +72,7 @@ #include "util/random.h" #include "util/rational.h" #include "util/result.h" -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" using namespace std; using namespace cvc5::kind; @@ -171,7 +171,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, d_solveIntAttempts(0u), d_newFacts(false), d_previousStatus(Result::SAT_UNKNOWN), - d_statistics() + d_statistics("theory::arith::") { } @@ -254,265 +254,154 @@ TheoryArithPrivate::ModelException::ModelException(TNode n, const char* msg) } TheoryArithPrivate::ModelException::~ModelException() {} -TheoryArithPrivate::Statistics::Statistics() - : d_statAssertUpperConflicts("theory::arith::AssertUpperConflicts", 0) - , d_statAssertLowerConflicts("theory::arith::AssertLowerConflicts", 0) - , d_statUserVariables("theory::arith::UserVariables", 0) - , d_statAuxiliaryVariables("theory::arith::AuxiliaryVariables", 0) - , d_statDisequalitySplits("theory::arith::DisequalitySplits", 0) - , d_statDisequalityConflicts("theory::arith::DisequalityConflicts", 0) - , d_simplifyTimer("theory::arith::simplifyTimer") - , d_staticLearningTimer("theory::arith::staticLearningTimer") - , d_presolveTime("theory::arith::presolveTime") - , d_newPropTime("theory::arith::newPropTimer") - , d_externalBranchAndBounds("theory::arith::externalBranchAndBounds",0) - , d_initialTableauSize("theory::arith::initialTableauSize", 0) - , d_currSetToSmaller("theory::arith::currSetToSmaller", 0) - , d_smallerSetToCurr("theory::arith::smallerSetToCurr", 0) - , d_restartTimer("theory::arith::restartTimer") - , d_boundComputationTime("theory::arith::bound::time") - , d_boundComputations("theory::arith::bound::boundComputations",0) - , d_boundPropagations("theory::arith::bound::boundPropagations",0) - , d_unknownChecks("theory::arith::status::unknowns", 0) - , d_maxUnknownsInARow("theory::arith::status::maxUnknownsInARow", 0) - , d_avgUnknownsInARow("theory::arith::status::avgUnknownsInARow") - , d_revertsOnConflicts("theory::arith::status::revertsOnConflicts",0) - , d_commitsOnConflicts("theory::arith::status::commitsOnConflicts",0) - , d_nontrivialSatChecks("theory::arith::status::nontrivialSatChecks",0) - , d_replayLogRecCount("theory::arith::z::approx::replay::rec",0) - , d_replayLogRecConflictEscalation("theory::arith::z::approx::replay::rec::escalation",0) - , d_replayLogRecEarlyExit("theory::arith::z::approx::replay::rec::earlyexit",0) - , d_replayBranchCloseFailures("theory::arith::z::approx::replay::rec::branch::closefailures",0) - , d_replayLeafCloseFailures("theory::arith::z::approx::replay::rec::leaf::closefailures",0) - , d_replayBranchSkips("theory::arith::z::approx::replay::rec::branch::skips",0) - , d_mirCutsAttempted("theory::arith::z::approx::cuts::mir::attempted",0) - , d_gmiCutsAttempted("theory::arith::z::approx::cuts::gmi::attempted",0) - , d_branchCutsAttempted("theory::arith::z::approx::cuts::branch::attempted",0) - , d_cutsReconstructed("theory::arith::z::approx::cuts::reconstructed",0) - , d_cutsReconstructionFailed("theory::arith::z::approx::cuts::reconstructed::failed",0) - , d_cutsProven("theory::arith::z::approx::cuts::proofs",0) - , d_cutsProofFailed("theory::arith::z::approx::cuts::proofs::failed",0) - , d_mipReplayLemmaCalls("theory::arith::z::approx::external::calls",0) - , d_mipExternalCuts("theory::arith::z::approx::external::cuts",0) - , d_mipExternalBranch("theory::arith::z::approx::external::branches",0) - , d_inSolveInteger("theory::arith::z::approx::inSolverInteger",0) - , d_branchesExhausted("theory::arith::z::approx::exhausted::branches",0) - , d_execExhausted("theory::arith::z::approx::exhausted::exec",0) - , d_pivotsExhausted("theory::arith::z::approx::exhausted::pivots",0) - , d_panicBranches("theory::arith::z::arith::paniclemmas",0) - , d_relaxCalls("theory::arith::z::arith::relax::calls",0) - , d_relaxLinFeas("theory::arith::z::arith::relax::feasible::res",0) - , d_relaxLinFeasFailures("theory::arith::z::arith::relax::feasible::failures",0) - , d_relaxLinInfeas("theory::arith::z::arith::relax::infeasible",0) - , d_relaxLinInfeasFailures("theory::arith::z::arith::relax::infeasible::failures",0) - , d_relaxLinExhausted("theory::arith::z::arith::relax::exhausted",0) - , d_relaxOthers("theory::arith::z::arith::relax::other",0) - , d_applyRowsDeleted("theory::arith::z::arith::cuts::applyRowsDeleted",0) - , d_replaySimplexTimer("theory::arith::z::approx::replay::simplex::timer") - , d_replayLogTimer("theory::arith::z::approx::replay::log::timer") - , d_solveIntTimer("theory::arith::z::solveInt::timer") - , d_solveRealRelaxTimer("theory::arith::z::solveRealRelax::timer") - , d_solveIntCalls("theory::arith::z::solveInt::calls", 0) - , d_solveStandardEffort("theory::arith::z::solveInt::calls::standardEffort", 0) - , d_approxDisabled("theory::arith::z::approxDisabled", 0) - , d_replayAttemptFailed("theory::arith::z::replayAttemptFailed",0) - , d_cutsRejectedDuringReplay("theory::arith::z::approx::replay::cuts::rejected", 0) - , d_cutsRejectedDuringLemmas("theory::arith::z::approx::external::cuts::rejected", 0) - , d_satPivots("theory::arith::pivots::sat") - , d_unsatPivots("theory::arith::pivots::unsat") - , d_unknownPivots("theory::arith::pivots::unknown") - , d_solveIntModelsAttempts("theory::arith::z::solveInt::models::attempts", 0) - , d_solveIntModelsSuccessful("theory::arith::zzz::solveInt::models::successful", 0) - , d_mipTimer("theory::arith::z::approx::mip::timer") - , d_lpTimer("theory::arith::z::approx::lp::timer") - , d_mipProofsAttempted("theory::arith::z::mip::proofs::attempted", 0) - , d_mipProofsSuccessful("theory::arith::z::mip::proofs::successful", 0) - , d_numBranchesFailed("theory::arith::z::mip::branch::proof::failed", 0) +TheoryArithPrivate::Statistics::Statistics(const std::string& name) + : d_statAssertUpperConflicts( + smtStatisticsRegistry().registerInt(name + "AssertUpperConflicts")), + d_statAssertLowerConflicts( + smtStatisticsRegistry().registerInt(name + "AssertLowerConflicts")), + d_statUserVariables( + smtStatisticsRegistry().registerInt(name + "UserVariables")), + d_statAuxiliaryVariables( + smtStatisticsRegistry().registerInt(name + "AuxiliaryVariables")), + d_statDisequalitySplits( + smtStatisticsRegistry().registerInt(name + "DisequalitySplits")), + d_statDisequalityConflicts( + smtStatisticsRegistry().registerInt(name + "DisequalityConflicts")), + d_simplifyTimer( + smtStatisticsRegistry().registerTimer(name + "simplifyTimer")), + d_staticLearningTimer( + smtStatisticsRegistry().registerTimer(name + "staticLearningTimer")), + d_presolveTime( + smtStatisticsRegistry().registerTimer(name + "presolveTime")), + d_newPropTime( + smtStatisticsRegistry().registerTimer(name + "newPropTimer")), + d_externalBranchAndBounds(smtStatisticsRegistry().registerInt( + name + "externalBranchAndBounds")), + d_initialTableauSize( + smtStatisticsRegistry().registerInt(name + "initialTableauSize")), + d_currSetToSmaller( + smtStatisticsRegistry().registerInt(name + "currSetToSmaller")), + d_smallerSetToCurr( + smtStatisticsRegistry().registerInt(name + "smallerSetToCurr")), + d_restartTimer( + smtStatisticsRegistry().registerTimer(name + "restartTimer")), + d_boundComputationTime( + smtStatisticsRegistry().registerTimer(name + "bound::time")), + d_boundComputations(smtStatisticsRegistry().registerInt( + name + "bound::boundComputations")), + d_boundPropagations(smtStatisticsRegistry().registerInt( + name + "bound::boundPropagations")), + d_unknownChecks( + smtStatisticsRegistry().registerInt(name + "status::unknowns")), + d_maxUnknownsInARow(smtStatisticsRegistry().registerInt( + name + "status::maxUnknownsInARow")), + d_avgUnknownsInARow(smtStatisticsRegistry().registerAverage( + name + "status::avgUnknownsInARow")), + d_revertsOnConflicts(smtStatisticsRegistry().registerInt( + name + "status::revertsOnConflicts")), + d_commitsOnConflicts(smtStatisticsRegistry().registerInt( + name + "status::commitsOnConflicts")), + d_nontrivialSatChecks(smtStatisticsRegistry().registerInt( + name + "status::nontrivialSatChecks")), + d_replayLogRecCount( + smtStatisticsRegistry().registerInt(name + "z::approx::replay::rec")), + d_replayLogRecConflictEscalation(smtStatisticsRegistry().registerInt( + name + "z::approx::replay::rec::escalation")), + d_replayLogRecEarlyExit(smtStatisticsRegistry().registerInt( + name + "z::approx::replay::rec::earlyexit")), + d_replayBranchCloseFailures(smtStatisticsRegistry().registerInt( + name + "z::approx::replay::rec::branch::closefailures")), + d_replayLeafCloseFailures(smtStatisticsRegistry().registerInt( + name + "z::approx::replay::rec::leaf::closefailures")), + d_replayBranchSkips(smtStatisticsRegistry().registerInt( + name + "z::approx::replay::rec::branch::skips")), + d_mirCutsAttempted(smtStatisticsRegistry().registerInt( + name + "z::approx::cuts::mir::attempted")), + d_gmiCutsAttempted(smtStatisticsRegistry().registerInt( + name + "z::approx::cuts::gmi::attempted")), + d_branchCutsAttempted(smtStatisticsRegistry().registerInt( + name + "z::approx::cuts::branch::attempted")), + d_cutsReconstructed(smtStatisticsRegistry().registerInt( + name + "z::approx::cuts::reconstructed")), + d_cutsReconstructionFailed(smtStatisticsRegistry().registerInt( + name + "z::approx::cuts::reconstructed::failed")), + d_cutsProven(smtStatisticsRegistry().registerInt( + name + "z::approx::cuts::proofs")), + d_cutsProofFailed(smtStatisticsRegistry().registerInt( + name + "z::approx::cuts::proofs::failed")), + d_mipReplayLemmaCalls(smtStatisticsRegistry().registerInt( + name + "z::approx::external::calls")), + d_mipExternalCuts(smtStatisticsRegistry().registerInt( + name + "z::approx::external::cuts")), + d_mipExternalBranch(smtStatisticsRegistry().registerInt( + name + "z::approx::external::branches")), + d_inSolveInteger(smtStatisticsRegistry().registerInt( + name + "z::approx::inSolverInteger")), + d_branchesExhausted(smtStatisticsRegistry().registerInt( + name + "z::approx::exhausted::branches")), + d_execExhausted(smtStatisticsRegistry().registerInt( + name + "z::approx::exhausted::exec")), + d_pivotsExhausted(smtStatisticsRegistry().registerInt( + name + "z::approx::exhausted::pivots")), + d_panicBranches( + smtStatisticsRegistry().registerInt(name + "z::arith::paniclemmas")), + d_relaxCalls( + smtStatisticsRegistry().registerInt(name + "z::arith::relax::calls")), + d_relaxLinFeas(smtStatisticsRegistry().registerInt( + name + "z::arith::relax::feasible::res")), + d_relaxLinFeasFailures(smtStatisticsRegistry().registerInt( + name + "z::arith::relax::feasible::failures")), + d_relaxLinInfeas(smtStatisticsRegistry().registerInt( + name + "z::arith::relax::infeasible")), + d_relaxLinInfeasFailures(smtStatisticsRegistry().registerInt( + name + "z::arith::relax::infeasible::failures")), + d_relaxLinExhausted(smtStatisticsRegistry().registerInt( + name + "z::arith::relax::exhausted")), + d_relaxOthers( + smtStatisticsRegistry().registerInt(name + "z::arith::relax::other")), + d_applyRowsDeleted(smtStatisticsRegistry().registerInt( + name + "z::arith::cuts::applyRowsDeleted")), + d_replaySimplexTimer(smtStatisticsRegistry().registerTimer( + name + "z::approx::replay::simplex::timer")), + d_replayLogTimer(smtStatisticsRegistry().registerTimer( + name + "z::approx::replay::log::timer")), + d_solveIntTimer( + smtStatisticsRegistry().registerTimer(name + "z::solveInt::timer")), + d_solveRealRelaxTimer(smtStatisticsRegistry().registerTimer( + name + "z::solveRealRelax::timer")), + d_solveIntCalls( + smtStatisticsRegistry().registerInt(name + "z::solveInt::calls")), + d_solveStandardEffort(smtStatisticsRegistry().registerInt( + name + "z::solveInt::calls::standardEffort")), + d_approxDisabled( + smtStatisticsRegistry().registerInt(name + "z::approxDisabled")), + d_replayAttemptFailed( + smtStatisticsRegistry().registerInt(name + "z::replayAttemptFailed")), + d_cutsRejectedDuringReplay(smtStatisticsRegistry().registerInt( + name + "z::approx::replay::cuts::rejected")), + d_cutsRejectedDuringLemmas(smtStatisticsRegistry().registerInt( + name + "z::approx::external::cuts::rejected")), + d_satPivots(smtStatisticsRegistry().registerHistogram<uint32_t>( + name + "pivots::sat")), + d_unsatPivots(smtStatisticsRegistry().registerHistogram<uint32_t>( + name + "pivots::unsat")), + d_unknownPivots(smtStatisticsRegistry().registerHistogram<uint32_t>( + name + "pivots::unknown")), + d_solveIntModelsAttempts(smtStatisticsRegistry().registerInt( + name + "z::solveInt::models::attempts")), + d_solveIntModelsSuccessful(smtStatisticsRegistry().registerInt( + name + "zzz::solveInt::models::successful")), + d_mipTimer(smtStatisticsRegistry().registerTimer( + name + "z::approx::mip::timer")), + d_lpTimer( + smtStatisticsRegistry().registerTimer(name + "z::approx::lp::timer")), + d_mipProofsAttempted(smtStatisticsRegistry().registerInt( + name + "z::mip::proofs::attempted")), + d_mipProofsSuccessful(smtStatisticsRegistry().registerInt( + name + "z::mip::proofs::successful")), + d_numBranchesFailed(smtStatisticsRegistry().registerInt( + name + "z::mip::branch::proof::failed")) { - smtStatisticsRegistry()->registerStat(&d_statAssertUpperConflicts); - smtStatisticsRegistry()->registerStat(&d_statAssertLowerConflicts); - - smtStatisticsRegistry()->registerStat(&d_statUserVariables); - smtStatisticsRegistry()->registerStat(&d_statAuxiliaryVariables); - smtStatisticsRegistry()->registerStat(&d_statDisequalitySplits); - smtStatisticsRegistry()->registerStat(&d_statDisequalityConflicts); - smtStatisticsRegistry()->registerStat(&d_simplifyTimer); - smtStatisticsRegistry()->registerStat(&d_staticLearningTimer); - - smtStatisticsRegistry()->registerStat(&d_presolveTime); - smtStatisticsRegistry()->registerStat(&d_newPropTime); - - smtStatisticsRegistry()->registerStat(&d_externalBranchAndBounds); - - smtStatisticsRegistry()->registerStat(&d_initialTableauSize); - smtStatisticsRegistry()->registerStat(&d_currSetToSmaller); - smtStatisticsRegistry()->registerStat(&d_smallerSetToCurr); - smtStatisticsRegistry()->registerStat(&d_restartTimer); - - smtStatisticsRegistry()->registerStat(&d_boundComputationTime); - smtStatisticsRegistry()->registerStat(&d_boundComputations); - smtStatisticsRegistry()->registerStat(&d_boundPropagations); - - smtStatisticsRegistry()->registerStat(&d_unknownChecks); - smtStatisticsRegistry()->registerStat(&d_maxUnknownsInARow); - smtStatisticsRegistry()->registerStat(&d_avgUnknownsInARow); - smtStatisticsRegistry()->registerStat(&d_revertsOnConflicts); - smtStatisticsRegistry()->registerStat(&d_commitsOnConflicts); - smtStatisticsRegistry()->registerStat(&d_nontrivialSatChecks); - - - smtStatisticsRegistry()->registerStat(&d_satPivots); - smtStatisticsRegistry()->registerStat(&d_unsatPivots); - smtStatisticsRegistry()->registerStat(&d_unknownPivots); - - smtStatisticsRegistry()->registerStat(&d_replayLogRecCount); - smtStatisticsRegistry()->registerStat(&d_replayLogRecConflictEscalation); - smtStatisticsRegistry()->registerStat(&d_replayLogRecEarlyExit); - smtStatisticsRegistry()->registerStat(&d_replayBranchCloseFailures); - smtStatisticsRegistry()->registerStat(&d_replayLeafCloseFailures); - smtStatisticsRegistry()->registerStat(&d_replayBranchSkips); - smtStatisticsRegistry()->registerStat(&d_mirCutsAttempted); - smtStatisticsRegistry()->registerStat(&d_gmiCutsAttempted); - smtStatisticsRegistry()->registerStat(&d_branchCutsAttempted); - smtStatisticsRegistry()->registerStat(&d_cutsReconstructed); - smtStatisticsRegistry()->registerStat(&d_cutsProven); - smtStatisticsRegistry()->registerStat(&d_cutsProofFailed); - smtStatisticsRegistry()->registerStat(&d_cutsReconstructionFailed); - smtStatisticsRegistry()->registerStat(&d_mipReplayLemmaCalls); - smtStatisticsRegistry()->registerStat(&d_mipExternalCuts); - smtStatisticsRegistry()->registerStat(&d_mipExternalBranch); - - smtStatisticsRegistry()->registerStat(&d_inSolveInteger); - smtStatisticsRegistry()->registerStat(&d_branchesExhausted); - smtStatisticsRegistry()->registerStat(&d_execExhausted); - smtStatisticsRegistry()->registerStat(&d_pivotsExhausted); - smtStatisticsRegistry()->registerStat(&d_panicBranches); - smtStatisticsRegistry()->registerStat(&d_relaxCalls); - smtStatisticsRegistry()->registerStat(&d_relaxLinFeas); - smtStatisticsRegistry()->registerStat(&d_relaxLinFeasFailures); - smtStatisticsRegistry()->registerStat(&d_relaxLinInfeas); - smtStatisticsRegistry()->registerStat(&d_relaxLinInfeasFailures); - smtStatisticsRegistry()->registerStat(&d_relaxLinExhausted); - smtStatisticsRegistry()->registerStat(&d_relaxOthers); - - smtStatisticsRegistry()->registerStat(&d_applyRowsDeleted); - - smtStatisticsRegistry()->registerStat(&d_replaySimplexTimer); - smtStatisticsRegistry()->registerStat(&d_replayLogTimer); - smtStatisticsRegistry()->registerStat(&d_solveIntTimer); - smtStatisticsRegistry()->registerStat(&d_solveRealRelaxTimer); - - smtStatisticsRegistry()->registerStat(&d_solveIntCalls); - smtStatisticsRegistry()->registerStat(&d_solveStandardEffort); - - smtStatisticsRegistry()->registerStat(&d_approxDisabled); - - smtStatisticsRegistry()->registerStat(&d_replayAttemptFailed); - - smtStatisticsRegistry()->registerStat(&d_cutsRejectedDuringReplay); - smtStatisticsRegistry()->registerStat(&d_cutsRejectedDuringLemmas); - - smtStatisticsRegistry()->registerStat(&d_solveIntModelsAttempts); - smtStatisticsRegistry()->registerStat(&d_solveIntModelsSuccessful); - smtStatisticsRegistry()->registerStat(&d_mipTimer); - smtStatisticsRegistry()->registerStat(&d_lpTimer); - smtStatisticsRegistry()->registerStat(&d_mipProofsAttempted); - smtStatisticsRegistry()->registerStat(&d_mipProofsSuccessful); - smtStatisticsRegistry()->registerStat(&d_numBranchesFailed); -} - -TheoryArithPrivate::Statistics::~Statistics(){ - smtStatisticsRegistry()->unregisterStat(&d_statAssertUpperConflicts); - smtStatisticsRegistry()->unregisterStat(&d_statAssertLowerConflicts); - - smtStatisticsRegistry()->unregisterStat(&d_statUserVariables); - smtStatisticsRegistry()->unregisterStat(&d_statAuxiliaryVariables); - smtStatisticsRegistry()->unregisterStat(&d_statDisequalitySplits); - smtStatisticsRegistry()->unregisterStat(&d_statDisequalityConflicts); - smtStatisticsRegistry()->unregisterStat(&d_simplifyTimer); - smtStatisticsRegistry()->unregisterStat(&d_staticLearningTimer); - - smtStatisticsRegistry()->unregisterStat(&d_presolveTime); - smtStatisticsRegistry()->unregisterStat(&d_newPropTime); - - smtStatisticsRegistry()->unregisterStat(&d_externalBranchAndBounds); - - smtStatisticsRegistry()->unregisterStat(&d_initialTableauSize); - smtStatisticsRegistry()->unregisterStat(&d_currSetToSmaller); - smtStatisticsRegistry()->unregisterStat(&d_smallerSetToCurr); - smtStatisticsRegistry()->unregisterStat(&d_restartTimer); - - smtStatisticsRegistry()->unregisterStat(&d_boundComputationTime); - smtStatisticsRegistry()->unregisterStat(&d_boundComputations); - smtStatisticsRegistry()->unregisterStat(&d_boundPropagations); - - smtStatisticsRegistry()->unregisterStat(&d_unknownChecks); - smtStatisticsRegistry()->unregisterStat(&d_maxUnknownsInARow); - smtStatisticsRegistry()->unregisterStat(&d_avgUnknownsInARow); - smtStatisticsRegistry()->unregisterStat(&d_revertsOnConflicts); - smtStatisticsRegistry()->unregisterStat(&d_commitsOnConflicts); - smtStatisticsRegistry()->unregisterStat(&d_nontrivialSatChecks); - - smtStatisticsRegistry()->unregisterStat(&d_satPivots); - smtStatisticsRegistry()->unregisterStat(&d_unsatPivots); - smtStatisticsRegistry()->unregisterStat(&d_unknownPivots); - - smtStatisticsRegistry()->unregisterStat(&d_replayLogRecCount); - smtStatisticsRegistry()->unregisterStat(&d_replayLogRecConflictEscalation); - smtStatisticsRegistry()->unregisterStat(&d_replayLogRecEarlyExit); - smtStatisticsRegistry()->unregisterStat(&d_replayBranchCloseFailures); - smtStatisticsRegistry()->unregisterStat(&d_replayLeafCloseFailures); - smtStatisticsRegistry()->unregisterStat(&d_replayBranchSkips); - smtStatisticsRegistry()->unregisterStat(&d_mirCutsAttempted); - smtStatisticsRegistry()->unregisterStat(&d_gmiCutsAttempted); - smtStatisticsRegistry()->unregisterStat(&d_branchCutsAttempted); - smtStatisticsRegistry()->unregisterStat(&d_cutsReconstructed); - smtStatisticsRegistry()->unregisterStat(&d_cutsProven); - smtStatisticsRegistry()->unregisterStat(&d_cutsProofFailed); - smtStatisticsRegistry()->unregisterStat(&d_cutsReconstructionFailed); - smtStatisticsRegistry()->unregisterStat(&d_mipReplayLemmaCalls); - smtStatisticsRegistry()->unregisterStat(&d_mipExternalCuts); - smtStatisticsRegistry()->unregisterStat(&d_mipExternalBranch); - - - smtStatisticsRegistry()->unregisterStat(&d_inSolveInteger); - smtStatisticsRegistry()->unregisterStat(&d_branchesExhausted); - smtStatisticsRegistry()->unregisterStat(&d_execExhausted); - smtStatisticsRegistry()->unregisterStat(&d_pivotsExhausted); - smtStatisticsRegistry()->unregisterStat(&d_panicBranches); - smtStatisticsRegistry()->unregisterStat(&d_relaxCalls); - smtStatisticsRegistry()->unregisterStat(&d_relaxLinFeas); - smtStatisticsRegistry()->unregisterStat(&d_relaxLinFeasFailures); - smtStatisticsRegistry()->unregisterStat(&d_relaxLinInfeas); - smtStatisticsRegistry()->unregisterStat(&d_relaxLinInfeasFailures); - smtStatisticsRegistry()->unregisterStat(&d_relaxLinExhausted); - smtStatisticsRegistry()->unregisterStat(&d_relaxOthers); - - smtStatisticsRegistry()->unregisterStat(&d_applyRowsDeleted); - - smtStatisticsRegistry()->unregisterStat(&d_replaySimplexTimer); - smtStatisticsRegistry()->unregisterStat(&d_replayLogTimer); - smtStatisticsRegistry()->unregisterStat(&d_solveIntTimer); - smtStatisticsRegistry()->unregisterStat(&d_solveRealRelaxTimer); - - smtStatisticsRegistry()->unregisterStat(&d_solveIntCalls); - smtStatisticsRegistry()->unregisterStat(&d_solveStandardEffort); - - smtStatisticsRegistry()->unregisterStat(&d_approxDisabled); - - smtStatisticsRegistry()->unregisterStat(&d_replayAttemptFailed); - - smtStatisticsRegistry()->unregisterStat(&d_cutsRejectedDuringReplay); - smtStatisticsRegistry()->unregisterStat(&d_cutsRejectedDuringLemmas); - - - smtStatisticsRegistry()->unregisterStat(&d_solveIntModelsAttempts); - smtStatisticsRegistry()->unregisterStat(&d_solveIntModelsSuccessful); - smtStatisticsRegistry()->unregisterStat(&d_mipTimer); - smtStatisticsRegistry()->unregisterStat(&d_lpTimer); - smtStatisticsRegistry()->unregisterStat(&d_mipProofsAttempted); - smtStatisticsRegistry()->unregisterStat(&d_mipProofsSuccessful); - smtStatisticsRegistry()->unregisterStat(&d_numBranchesFailed); } bool complexityBelow(const DenseMap<Rational>& row, uint32_t cap){ @@ -2406,8 +2295,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.get() << std::endl; + Debug("approx::replayLogRec") << "replayLogRec()" << std::endl; size_t rpvars_size = d_replayVariables.size(); size_t rpcons_size = d_replayConstraints.size(); @@ -2842,7 +2730,7 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){ TimerStat::CodeTimer codeTimer0(d_statistics.d_solveIntTimer); ++(d_statistics.d_solveIntCalls); - d_statistics.d_inSolveInteger.set(1); + d_statistics.d_inSolveInteger = 1; if(!Theory::fullEffort(effortLevel)){ d_solveIntAttempts++; @@ -2971,7 +2859,7 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){ } } - d_statistics.d_inSolveInteger.set(0); + d_statistics.d_inSolveInteger = 0; } SimplexDecisionProcedure& TheoryArithPrivate::selectSimplex(bool pass1){ @@ -4324,7 +4212,7 @@ bool TheoryArithPrivate::unenqueuedVariablesAreConsistent(){ void TheoryArithPrivate::presolve(){ TimerStat::CodeTimer codeTimer(d_statistics.d_presolveTime); - d_statistics.d_initialTableauSize.set(d_tableau.size()); + d_statistics.d_initialTableauSize = d_tableau.size(); if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); } diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 408d94397..e23451167 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -53,7 +53,7 @@ #include "util/integer.h" #include "util/rational.h" #include "util/result.h" -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { @@ -856,10 +856,9 @@ private: IntStat d_cutsRejectedDuringReplay; IntStat d_cutsRejectedDuringLemmas; - IntegralHistogramStat<uint32_t> d_satPivots; - IntegralHistogramStat<uint32_t> d_unsatPivots; - IntegralHistogramStat<uint32_t> d_unknownPivots; - + HistogramStat<uint32_t> d_satPivots; + HistogramStat<uint32_t> d_unsatPivots; + HistogramStat<uint32_t> d_unknownPivots; IntStat d_solveIntModelsAttempts; IntStat d_solveIntModelsSuccessful; @@ -871,10 +870,7 @@ private: IntStat d_numBranchesFailed; - - - Statistics(); - ~Statistics(); + Statistics(const std::string& name); }; diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp index 164b9b058..4dc7201fb 100644 --- a/src/theory/arrays/array_info.cpp +++ b/src/theory/arrays/array_info.cpp @@ -43,26 +43,31 @@ Info::~Info() { in_stores->deleteSelf(); } -ArrayInfo::ArrayInfo(context::Context* c, Backtracker<TNode>* b, std::string statisticsPrefix) - : ct(c), bck(b), info_map(), - d_mergeInfoTimer(statisticsPrefix + "theory::arrays::mergeInfoTimer"), - d_avgIndexListLength(statisticsPrefix + "theory::arrays::avgIndexListLength"), - d_avgStoresListLength(statisticsPrefix + "theory::arrays::avgStoresListLength"), - d_avgInStoresListLength(statisticsPrefix + "theory::arrays::avgInStoresListLength"), - d_listsCount(statisticsPrefix + "theory::arrays::listsCount",0), - d_callsMergeInfo(statisticsPrefix + "theory::arrays::callsMergeInfo",0), - d_maxList(statisticsPrefix + "theory::arrays::maxList",0), - d_tableSize(statisticsPrefix + "theory::arrays::infoTableSize", info_map) { +ArrayInfo::ArrayInfo(context::Context* c, + Backtracker<TNode>* b, + std::string statisticsPrefix) + : ct(c), + bck(b), + info_map(), + d_mergeInfoTimer(smtStatisticsRegistry().registerTimer( + statisticsPrefix + "mergeInfoTimer")), + d_avgIndexListLength(smtStatisticsRegistry().registerAverage( + statisticsPrefix + "avgIndexListLength")), + d_avgStoresListLength(smtStatisticsRegistry().registerAverage( + statisticsPrefix + "avgStoresListLength")), + d_avgInStoresListLength(smtStatisticsRegistry().registerAverage( + statisticsPrefix + "avgInStoresListLength")), + d_listsCount( + smtStatisticsRegistry().registerInt(statisticsPrefix + "listsCount")), + d_callsMergeInfo(smtStatisticsRegistry().registerInt(statisticsPrefix + + "callsMergeInfo")), + d_maxList( + smtStatisticsRegistry().registerInt(statisticsPrefix + "maxList")), + d_tableSize(smtStatisticsRegistry().registerSize<CNodeInfoMap>( + statisticsPrefix + "infoTableSize", info_map)) +{ emptyList = new(true) CTNodeList(ct); emptyInfo = new Info(ct, bck); - smtStatisticsRegistry()->registerStat(&d_mergeInfoTimer); - smtStatisticsRegistry()->registerStat(&d_avgIndexListLength); - smtStatisticsRegistry()->registerStat(&d_avgStoresListLength); - smtStatisticsRegistry()->registerStat(&d_avgInStoresListLength); - smtStatisticsRegistry()->registerStat(&d_listsCount); - smtStatisticsRegistry()->registerStat(&d_callsMergeInfo); - smtStatisticsRegistry()->registerStat(&d_maxList); - smtStatisticsRegistry()->registerStat(&d_tableSize); } ArrayInfo::~ArrayInfo() { @@ -75,14 +80,6 @@ ArrayInfo::~ArrayInfo() { } emptyList->deleteSelf(); delete emptyInfo; - smtStatisticsRegistry()->unregisterStat(&d_mergeInfoTimer); - smtStatisticsRegistry()->unregisterStat(&d_avgIndexListLength); - smtStatisticsRegistry()->unregisterStat(&d_avgStoresListLength); - smtStatisticsRegistry()->unregisterStat(&d_avgInStoresListLength); - smtStatisticsRegistry()->unregisterStat(&d_listsCount); - smtStatisticsRegistry()->unregisterStat(&d_callsMergeInfo); - smtStatisticsRegistry()->unregisterStat(&d_maxList); - smtStatisticsRegistry()->unregisterStat(&d_tableSize); } bool inList(const CTNodeList* l, const TNode el) { diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index bbb9e8c62..15f27eb96 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -25,8 +25,7 @@ #include "context/backtrackable.h" #include "context/cdlist.h" #include "expr/node.h" -#include "util/statistics_registry.h" -#include "util/stats_timer.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { @@ -117,7 +116,7 @@ private: IntStat d_listsCount; IntStat d_callsMergeInfo; IntStat d_maxList; - SizeStat<CNodeInfoMap > d_tableSize; + SizeStat<CNodeInfoMap> d_tableSize; /** * checks if a certain element is in the list l diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp index 48755b7ea..fc3f67cf0 100644 --- a/src/theory/arrays/inference_manager.cpp +++ b/src/theory/arrays/inference_manager.cpp @@ -29,10 +29,9 @@ namespace arrays { InferenceManager::InferenceManager(Theory& t, TheoryState& state, ProofNodeManager* pnm) - : TheoryInferenceManager(t, state, pnm, "theory::arrays", false), - d_lemmaPg(pnm ? new EagerProofGenerator(pnm, - state.getUserContext(), - "ArrayLemmaProofGenerator") + : TheoryInferenceManager(t, state, pnm, "theory::arrays::", false), + d_lemmaPg(pnm ? new EagerProofGenerator( + pnm, state.getUserContext(), "ArrayLemmaProofGenerator") : nullptr) { } diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index ee95b3c82..1a1090f68 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -62,30 +62,34 @@ TheoryArrays::TheoryArrays(context::Context* c, ProofNodeManager* pnm, std::string name) : Theory(THEORY_ARRAYS, c, u, out, valuation, logicInfo, pnm, name), - d_numRow(name + "theory::arrays::number of Row lemmas", 0), - d_numExt(name + "theory::arrays::number of Ext lemmas", 0), - d_numProp(name + "theory::arrays::number of propagations", 0), - d_numExplain(name + "theory::arrays::number of explanations", 0), - d_numNonLinear(name + "theory::arrays::number of calls to setNonLinear", - 0), - d_numSharedArrayVarSplits( - name + "theory::arrays::number of shared array var splits", 0), - d_numGetModelValSplits( - name + "theory::arrays::number of getModelVal splits", 0), - d_numGetModelValConflicts( - name + "theory::arrays::number of getModelVal conflicts", 0), - d_numSetModelValSplits( - name + "theory::arrays::number of setModelVal splits", 0), - d_numSetModelValConflicts( - name + "theory::arrays::number of setModelVal conflicts", 0), - d_ppEqualityEngine(u, name + "theory::arrays::pp", true), + d_numRow( + smtStatisticsRegistry().registerInt(name + "number of Row lemmas")), + d_numExt( + smtStatisticsRegistry().registerInt(name + "number of Ext lemmas")), + d_numProp( + smtStatisticsRegistry().registerInt(name + "number of propagations")), + d_numExplain( + smtStatisticsRegistry().registerInt(name + "number of explanations")), + d_numNonLinear(smtStatisticsRegistry().registerInt( + name + "number of calls to setNonLinear")), + d_numSharedArrayVarSplits(smtStatisticsRegistry().registerInt( + name + "number of shared array var splits")), + d_numGetModelValSplits(smtStatisticsRegistry().registerInt( + name + "number of getModelVal splits")), + d_numGetModelValConflicts(smtStatisticsRegistry().registerInt( + name + "number of getModelVal conflicts")), + d_numSetModelValSplits(smtStatisticsRegistry().registerInt( + name + "number of setModelVal splits")), + d_numSetModelValConflicts(smtStatisticsRegistry().registerInt( + name + "number of setModelVal conflicts")), + d_ppEqualityEngine(u, name + "pp", true), d_ppFacts(u), d_state(c, u, valuation), d_im(*this, d_state, pnm), d_literalsToPropagate(c), d_literalsToPropagateIndex(c, 0), d_isPreRegistered(c), - d_mayEqualEqualityEngine(c, name + "theory::arrays::mayEqual", true), + d_mayEqualEqualityEngine(c, name + "mayEqual", true), d_notify(*this), d_backtracker(c), d_infoMap(c, &d_backtracker, name), @@ -112,17 +116,6 @@ TheoryArrays::TheoryArrays(context::Context* c, d_dstrat(new TheoryArraysDecisionStrategy(this)), d_dstratInit(false) { - smtStatisticsRegistry()->registerStat(&d_numRow); - smtStatisticsRegistry()->registerStat(&d_numExt); - smtStatisticsRegistry()->registerStat(&d_numProp); - smtStatisticsRegistry()->registerStat(&d_numExplain); - smtStatisticsRegistry()->registerStat(&d_numNonLinear); - smtStatisticsRegistry()->registerStat(&d_numSharedArrayVarSplits); - smtStatisticsRegistry()->registerStat(&d_numGetModelValSplits); - smtStatisticsRegistry()->registerStat(&d_numGetModelValConflicts); - smtStatisticsRegistry()->registerStat(&d_numSetModelValSplits); - smtStatisticsRegistry()->registerStat(&d_numSetModelValConflicts); - d_true = NodeManager::currentNM()->mkConst<bool>(true); d_false = NodeManager::currentNM()->mkConst<bool>(false); @@ -147,16 +140,6 @@ TheoryArrays::~TheoryArrays() { it2->second->deleteSelf(); } delete d_constReadsContext; - smtStatisticsRegistry()->unregisterStat(&d_numRow); - smtStatisticsRegistry()->unregisterStat(&d_numExt); - smtStatisticsRegistry()->unregisterStat(&d_numProp); - smtStatisticsRegistry()->unregisterStat(&d_numExplain); - smtStatisticsRegistry()->unregisterStat(&d_numNonLinear); - smtStatisticsRegistry()->unregisterStat(&d_numSharedArrayVarSplits); - smtStatisticsRegistry()->unregisterStat(&d_numGetModelValSplits); - smtStatisticsRegistry()->unregisterStat(&d_numGetModelValConflicts); - smtStatisticsRegistry()->unregisterStat(&d_numSetModelValSplits); - smtStatisticsRegistry()->unregisterStat(&d_numSetModelValConflicts); } TheoryRewriter* TheoryArrays::getTheoryRewriter() { return &d_rewriter; } @@ -166,7 +149,7 @@ ProofRuleChecker* TheoryArrays::getProofChecker() { return &d_checker; } bool TheoryArrays::needsEqualityEngine(EeSetupInfo& esi) { esi.d_notify = &d_notify; - esi.d_name = d_instanceName + "theory::arrays::ee"; + esi.d_name = d_instanceName + "ee"; return true; } diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 188573152..7cf8d52e3 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -32,7 +32,7 @@ #include "theory/theory.h" #include "theory/theory_state.h" #include "theory/uf/equality_engine.h" -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { @@ -138,7 +138,7 @@ class TheoryArrays : public Theory { Valuation valuation, const LogicInfo& logicInfo, ProofNodeManager* pnm = nullptr, - std::string name = ""); + std::string name = "theory::arrays::"); ~TheoryArrays(); //--------------------------------- initialization diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp index 6e3b38d8d..3d1a94f22 100644 --- a/src/theory/bags/bags_rewriter.cpp +++ b/src/theory/bags/bags_rewriter.cpp @@ -16,6 +16,7 @@ #include "theory/bags/bags_rewriter.h" #include "theory/bags/normal_form.h" +#include "util/statistics_registry.h" using namespace cvc5::kind; @@ -38,7 +39,7 @@ BagsRewriteResponse::BagsRewriteResponse(const BagsRewriteResponse& r) { } -BagsRewriter::BagsRewriter(IntegralHistogramStat<Rewrite>* statistics) +BagsRewriter::BagsRewriter(HistogramStat<Rewrite>* statistics) : d_statistics(statistics) { d_nm = NodeManager::currentNM(); diff --git a/src/theory/bags/bags_rewriter.h b/src/theory/bags/bags_rewriter.h index 10fa65aa5..54c1d7253 100644 --- a/src/theory/bags/bags_rewriter.h +++ b/src/theory/bags/bags_rewriter.h @@ -20,8 +20,7 @@ #include "theory/bags/rewrites.h" #include "theory/theory_rewriter.h" -#include "util/statistics_registry.h" -#include "util/stats_histogram.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { @@ -43,7 +42,7 @@ struct BagsRewriteResponse class BagsRewriter : public TheoryRewriter { public: - BagsRewriter(IntegralHistogramStat<Rewrite>* statistics = nullptr); + BagsRewriter(HistogramStat<Rewrite>* statistics = nullptr); /** * postRewrite nodes with kinds: MK_BAG, BAG_COUNT, UNION_MAX, UNION_DISJOINT, @@ -219,7 +218,7 @@ class BagsRewriter : public TheoryRewriter Node d_zero; Node d_one; /** Reference to the rewriter statistics. */ - IntegralHistogramStat<Rewrite>* d_statistics; + HistogramStat<Rewrite>* d_statistics; }; /* class TheoryBagsRewriter */ } // namespace bags diff --git a/src/theory/bags/bags_statistics.cpp b/src/theory/bags/bags_statistics.cpp index 018dbb231..5c351f0ac 100644 --- a/src/theory/bags/bags_statistics.cpp +++ b/src/theory/bags/bags_statistics.cpp @@ -21,14 +21,10 @@ namespace cvc5 { namespace theory { namespace bags { -BagsStatistics::BagsStatistics() : d_rewrites("theory::bags::rewrites") +BagsStatistics::BagsStatistics() + : d_rewrites(smtStatisticsRegistry().registerHistogram<Rewrite>( + "theory::bags::rewrites")) { - smtStatisticsRegistry()->registerStat(&d_rewrites); -} - -BagsStatistics::~BagsStatistics() -{ - smtStatisticsRegistry()->unregisterStat(&d_rewrites); } } // namespace bags diff --git a/src/theory/bags/bags_statistics.h b/src/theory/bags/bags_statistics.h index c0bca3444..d2eb33dbe 100644 --- a/src/theory/bags/bags_statistics.h +++ b/src/theory/bags/bags_statistics.h @@ -19,8 +19,7 @@ #define CVC5__THEORY__BAGS_STATISTICS_H #include "theory/bags/rewrites.h" -#include "util/statistics_registry.h" -#include "util/stats_histogram.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { @@ -33,10 +32,9 @@ class BagsStatistics { public: BagsStatistics(); - ~BagsStatistics(); /** Counts the number of applications of each type of rewrite rule */ - IntegralHistogramStat<Rewrite> d_rewrites; + HistogramStat<Rewrite> d_rewrites; }; } // namespace bags diff --git a/src/theory/bags/inference_manager.cpp b/src/theory/bags/inference_manager.cpp index 797ec0f4d..cc163e6cf 100644 --- a/src/theory/bags/inference_manager.cpp +++ b/src/theory/bags/inference_manager.cpp @@ -27,7 +27,7 @@ namespace bags { InferenceManager::InferenceManager(Theory& t, SolverState& s, ProofNodeManager* pnm) - : InferenceManagerBuffered(t, s, pnm, "theory::bags"), d_state(s) + : InferenceManagerBuffered(t, s, pnm, "theory::bags::"), d_state(s) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp index bded82b4b..e6080ed4f 100644 --- a/src/theory/bv/abstraction.cpp +++ b/src/theory/bv/abstraction.cpp @@ -532,8 +532,6 @@ void AbstractionModule::finalizeSignatures() d_funcToSignature[abs_func] = signature; } - d_statistics.d_numFunctionsAbstracted.set(d_signatureToFunc.size()); - Debug("bv-abstraction") << "AbstractionModule::finalizeSignatures abstracted " << d_signatureToFunc.size() << " signatures. \n"; } @@ -1090,19 +1088,14 @@ AbstractionModule::ArgsTableEntry& AbstractionModule::ArgsTable::getEntry(TNode return d_data.find(signature)->second; } -AbstractionModule::Statistics::Statistics(const std::string& name) - : d_numFunctionsAbstracted(name + "::abstraction::NumFunctionsAbstracted", - 0), - d_numArgsSkolemized(name + "::abstraction::NumArgsSkolemized", 0), - d_abstractionTime(name + "::abstraction::AbstractionTime") +AbstractionModule::Statistics::Statistics( + const std::string& name, const NodeNodeMap& functionsAbstracted) + : d_numFunctionsAbstracted( + smtStatisticsRegistry().registerSize<NodeNodeMap>( + name + "NumFunctionsAbstracted", functionsAbstracted)), + d_numArgsSkolemized( + smtStatisticsRegistry().registerInt(name + "NumArgsSkolemized")), + d_abstractionTime( + smtStatisticsRegistry().registerTimer(name + "AbstractionTime")) { - smtStatisticsRegistry()->registerStat(&d_numFunctionsAbstracted); - smtStatisticsRegistry()->registerStat(&d_numArgsSkolemized); - smtStatisticsRegistry()->registerStat(&d_abstractionTime); -} - -AbstractionModule::Statistics::~Statistics() { - smtStatisticsRegistry()->unregisterStat(&d_numFunctionsAbstracted); - smtStatisticsRegistry()->unregisterStat(&d_numArgsSkolemized); - smtStatisticsRegistry()->unregisterStat(&d_abstractionTime); } diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h index b099a33cd..67a04bfea 100644 --- a/src/theory/bv/abstraction.h +++ b/src/theory/bv/abstraction.h @@ -23,8 +23,7 @@ #include "expr/node.h" #include "theory/substitutions.h" -#include "util/statistics_registry.h" -#include "util/stats_timer.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { @@ -33,13 +32,23 @@ namespace bv { typedef std::vector<TNode> ArgsVec; class AbstractionModule { + using NodeVecMap = + std::unordered_map<Node, std::vector<Node>, NodeHashFunction>; + using NodeTNodeMap = std::unordered_map<Node, TNode, NodeHashFunction>; + using TNodeTNodeMap = std::unordered_map<TNode, TNode, TNodeHashFunction>; + using NodeNodeMap = std::unordered_map<Node, Node, NodeHashFunction>; + using TNodeNodeMap = std::unordered_map<Node, TNode, NodeHashFunction>; + using TNodeSet = std::unordered_set<TNode, TNodeHashFunction>; + using IntNodeMap = std::unordered_map<unsigned, Node>; + using IndexMap = std::unordered_map<unsigned, unsigned>; + using SkolemMap = std::unordered_map<unsigned, std::vector<Node> >; + using SignatureMap = std::unordered_map<TNode, unsigned, TNodeHashFunction>; struct Statistics { - IntStat d_numFunctionsAbstracted; + SizeStat<NodeNodeMap> d_numFunctionsAbstracted; IntStat d_numArgsSkolemized; TimerStat d_abstractionTime; - Statistics(const std::string& name); - ~Statistics(); + Statistics(const std::string& name, const NodeNodeMap& functionsAbstracted); }; @@ -126,17 +135,6 @@ class AbstractionModule { }; - typedef std::unordered_map<Node, std::vector<Node>, NodeHashFunction> NodeVecMap; - typedef std::unordered_map<Node, TNode, NodeHashFunction> NodeTNodeMap; - typedef std::unordered_map<TNode, TNode, TNodeHashFunction> TNodeTNodeMap; - typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap; - typedef std::unordered_map<Node, TNode, NodeHashFunction> TNodeNodeMap; - typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; - typedef std::unordered_map<unsigned, Node> IntNodeMap; - typedef std::unordered_map<unsigned, unsigned> IndexMap; - typedef std::unordered_map<unsigned, std::vector<Node> > SkolemMap; - typedef std::unordered_map<TNode, unsigned, TNodeHashFunction > SignatureMap; - ArgsTable d_argsTable; // mapping between signature and uninterpreted function symbol used to @@ -197,21 +195,22 @@ class AbstractionModule { Statistics d_statistics; public: - AbstractionModule(const std::string& name) - : d_argsTable() - , d_signatureToFunc() - , d_funcToSignature() - , d_assertionToSignature() - , d_signatures() - , d_sigToGeneralization() - , d_skolems() - , d_signatureIndices() - , d_signatureSkolems() - , d_addedLemmas() - , d_lemmaAtoms() - , d_inputAtoms() - , d_statistics(name) - {} + AbstractionModule(const std::string& name) + : d_argsTable(), + d_signatureToFunc(), + d_funcToSignature(), + d_assertionToSignature(), + d_signatures(), + d_sigToGeneralization(), + d_skolems(), + d_signatureIndices(), + d_signatureSkolems(), + d_addedLemmas(), + d_lemmaAtoms(), + d_inputAtoms(), + d_statistics(name + "abstraction::", d_signatureToFunc) + { + } /** * returns true if there are new uninterepreted functions symbols in the output * diff --git a/src/theory/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp index 8c80f9d19..0907e8005 100644 --- a/src/theory/bv/bitblast/aig_bitblaster.cpp +++ b/src/theory/bv/bitblast/aig_bitblaster.cpp @@ -148,24 +148,25 @@ AigBitblaster::AigBitblaster() case options::SatSolverMode::MINISAT: { prop::BVSatSolverInterface* minisat = - prop::SatSolverFactory::createMinisat( - d_nullContext.get(), smtStatisticsRegistry(), "AigBitblaster"); + prop::SatSolverFactory::createMinisat(d_nullContext.get(), + smtStatisticsRegistry(), + "theory::bv::AigBitblaster::"); d_notify.reset(new MinisatEmptyNotify()); minisat->setNotify(d_notify.get()); solver = minisat; break; } case options::SatSolverMode::CADICAL: - solver = prop::SatSolverFactory::createCadical(smtStatisticsRegistry(), - "AigBitblaster"); + solver = prop::SatSolverFactory::createCadical( + smtStatisticsRegistry(), "theory::bv::AigBitblaster::"); break; case options::SatSolverMode::CRYPTOMINISAT: solver = prop::SatSolverFactory::createCryptoMinisat( - smtStatisticsRegistry(), "AigBitblaster"); + smtStatisticsRegistry(), "theory::bv::AigBitblaster::"); break; case options::SatSolverMode::KISSAT: - solver = prop::SatSolverFactory::createKissat(smtStatisticsRegistry(), - "AigBitblaster"); + solver = prop::SatSolverFactory::createKissat( + smtStatisticsRegistry(), "theory::bv::AigBitblaster::"); break; default: CVC5_FATAL() << "Unknown SAT solver type"; } diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp index fcd33e775..9871f2a92 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.cpp +++ b/src/theory/bv/bitblast/eager_bitblaster.cpp @@ -47,23 +47,25 @@ EagerBitblaster::EagerBitblaster(BVSolverLazy* theory_bv, context::Context* c) { prop::BVSatSolverInterface* minisat = prop::SatSolverFactory::createMinisat( - d_nullContext.get(), smtStatisticsRegistry(), "EagerBitblaster"); + d_nullContext.get(), + smtStatisticsRegistry(), + "theory::bv::EagerBitblaster::"); d_notify.reset(new MinisatEmptyNotify()); minisat->setNotify(d_notify.get()); solver = minisat; break; } case options::SatSolverMode::CADICAL: - solver = prop::SatSolverFactory::createCadical(smtStatisticsRegistry(), - "EagerBitblaster"); + solver = prop::SatSolverFactory::createCadical( + smtStatisticsRegistry(), "theory::bv::EagerBitblaster::"); break; case options::SatSolverMode::CRYPTOMINISAT: solver = prop::SatSolverFactory::createCryptoMinisat( - smtStatisticsRegistry(), "EagerBitblaster"); + smtStatisticsRegistry(), "theory::bv::EagerBitblaster::"); break; case options::SatSolverMode::KISSAT: - solver = prop::SatSolverFactory::createKissat(smtStatisticsRegistry(), - "EagerBitblaster"); + solver = prop::SatSolverFactory::createKissat( + smtStatisticsRegistry(), "theory::bv::EagerBitblaster::"); break; default: Unreachable() << "Unknown SAT solver type"; } diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp index 12f584442..6a5372e04 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.cpp +++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp @@ -73,10 +73,10 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, d_emptyNotify(emptyNotify), d_fullModelAssertionLevel(c, 0), d_name(name), - d_statistics(name) + d_statistics(name + "::") { - d_satSolver.reset( - prop::SatSolverFactory::createMinisat(c, smtStatisticsRegistry(), name)); + d_satSolver.reset(prop::SatSolverFactory::createMinisat( + c, smtStatisticsRegistry(), name + "::")); ResourceManager* rm = smt::currentResourceManager(); d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(), @@ -362,33 +362,22 @@ void TLazyBitblaster::getConflict(std::vector<TNode>& conflict) } } -TLazyBitblaster::Statistics::Statistics(const std::string& prefix) : - d_numTermClauses(prefix + "::NumTermSatClauses", 0), - d_numAtomClauses(prefix + "::NumAtomSatClauses", 0), - d_numTerms(prefix + "::NumBitblastedTerms", 0), - d_numAtoms(prefix + "::NumBitblastedAtoms", 0), - d_numExplainedPropagations(prefix + "::NumExplainedPropagations", 0), - d_numBitblastingPropagations(prefix + "::NumBitblastingPropagations", 0), - d_bitblastTimer(prefix + "::BitblastTimer") +TLazyBitblaster::Statistics::Statistics(const std::string& prefix) + : d_numTermClauses( + smtStatisticsRegistry().registerInt(prefix + "NumTermSatClauses")), + d_numAtomClauses( + smtStatisticsRegistry().registerInt(prefix + "NumAtomSatClauses")), + d_numTerms( + smtStatisticsRegistry().registerInt(prefix + "NumBitblastedTerms")), + d_numAtoms( + smtStatisticsRegistry().registerInt(prefix + "NumBitblastedAtoms")), + d_numExplainedPropagations(smtStatisticsRegistry().registerInt( + prefix + "NumExplainedPropagations")), + d_numBitblastingPropagations(smtStatisticsRegistry().registerInt( + prefix + "NumBitblastingPropagations")), + d_bitblastTimer( + smtStatisticsRegistry().registerTimer(prefix + "BitblastTimer")) { - smtStatisticsRegistry()->registerStat(&d_numTermClauses); - smtStatisticsRegistry()->registerStat(&d_numAtomClauses); - smtStatisticsRegistry()->registerStat(&d_numTerms); - smtStatisticsRegistry()->registerStat(&d_numAtoms); - smtStatisticsRegistry()->registerStat(&d_numExplainedPropagations); - smtStatisticsRegistry()->registerStat(&d_numBitblastingPropagations); - smtStatisticsRegistry()->registerStat(&d_bitblastTimer); -} - - -TLazyBitblaster::Statistics::~Statistics() { - smtStatisticsRegistry()->unregisterStat(&d_numTermClauses); - smtStatisticsRegistry()->unregisterStat(&d_numAtomClauses); - smtStatisticsRegistry()->unregisterStat(&d_numTerms); - smtStatisticsRegistry()->unregisterStat(&d_numAtoms); - smtStatisticsRegistry()->unregisterStat(&d_numExplainedPropagations); - smtStatisticsRegistry()->unregisterStat(&d_numBitblastingPropagations); - smtStatisticsRegistry()->unregisterStat(&d_bitblastTimer); } bool TLazyBitblaster::MinisatNotify::notify(prop::SatLiteral lit) { diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h index 7ca2063a3..15cbe1558 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.h +++ b/src/theory/bv/bitblast/lazy_bitblaster.h @@ -161,7 +161,6 @@ class TLazyBitblaster : public TBitblaster<Node> IntStat d_numBitblastingPropagations; TimerStat d_bitblastTimer; Statistics(const std::string& name); - ~Statistics(); }; std::string d_name; diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp index f3d2a0832..5d3e99253 100644 --- a/src/theory/bv/bv_quick_check.cpp +++ b/src/theory/bv/bv_quick_check.cpp @@ -351,31 +351,21 @@ Node QuickXPlain::minimizeConflict(TNode confl) { } QuickXPlain::Statistics::Statistics(const std::string& name) - : d_xplainTime(name + "::QuickXplain::Time") - , d_numSolved(name + "::QuickXplain::NumSolved", 0) - , d_numUnknown(name + "::QuickXplain::NumUnknown", 0) - , d_numUnknownWasUnsat(name + "::QuickXplain::NumUnknownWasUnsat", 0) - , d_numConflictsMinimized(name + "::QuickXplain::NumConflictsMinimized", 0) - , d_finalPeriod(name + "::QuickXplain::FinalPeriod", 0) - , d_avgMinimizationRatio(name + "::QuickXplain::AvgMinRatio") + : d_xplainTime( + smtStatisticsRegistry().registerTimer(name + "QuickXplain::Time")), + d_numSolved( + smtStatisticsRegistry().registerInt(name + "QuickXplain::NumSolved")), + d_numUnknown(smtStatisticsRegistry().registerInt( + name + "QuickXplain::NumUnknown")), + d_numUnknownWasUnsat(smtStatisticsRegistry().registerInt( + name + "QuickXplain::NumUnknownWasUnsat")), + d_numConflictsMinimized(smtStatisticsRegistry().registerInt( + name + "QuickXplain::NumConflictsMinimized")), + d_finalPeriod(smtStatisticsRegistry().registerInt( + name + "QuickXplain::FinalPeriod")), + d_avgMinimizationRatio(smtStatisticsRegistry().registerAverage( + name + "QuickXplain::AvgMinRatio")) { - smtStatisticsRegistry()->registerStat(&d_xplainTime); - smtStatisticsRegistry()->registerStat(&d_numSolved); - smtStatisticsRegistry()->registerStat(&d_numUnknown); - smtStatisticsRegistry()->registerStat(&d_numUnknownWasUnsat); - smtStatisticsRegistry()->registerStat(&d_numConflictsMinimized); - smtStatisticsRegistry()->registerStat(&d_finalPeriod); - smtStatisticsRegistry()->registerStat(&d_avgMinimizationRatio); -} - -QuickXPlain::Statistics::~Statistics() { - smtStatisticsRegistry()->unregisterStat(&d_xplainTime); - smtStatisticsRegistry()->unregisterStat(&d_numSolved); - smtStatisticsRegistry()->unregisterStat(&d_numUnknown); - smtStatisticsRegistry()->unregisterStat(&d_numUnknownWasUnsat); - smtStatisticsRegistry()->unregisterStat(&d_numConflictsMinimized); - smtStatisticsRegistry()->unregisterStat(&d_finalPeriod); - smtStatisticsRegistry()->unregisterStat(&d_avgMinimizationRatio); } } // namespace bv diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h index 57bcca261..f22f298ac 100644 --- a/src/theory/bv/bv_quick_check.h +++ b/src/theory/bv/bv_quick_check.h @@ -25,8 +25,7 @@ #include "expr/node.h" #include "prop/sat_solver_types.h" #include "theory/bv/theory_bv_utils.h" -#include "util/statistics_registry.h" -#include "util/stats_timer.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { @@ -121,7 +120,6 @@ class QuickXPlain IntStat d_finalPeriod; AverageStat d_avgMinimizationRatio; Statistics(const std::string& name); - ~Statistics(); }; BVQuickCheck* d_solver; unsigned long d_budget; diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp index 1a3eb0a4b..a9d46f068 100644 --- a/src/theory/bv/bv_solver_bitblast.cpp +++ b/src/theory/bv/bv_solver_bitblast.cpp @@ -52,11 +52,11 @@ BVSolverBitblast::BVSolverBitblast(TheoryState* s, { case options::SatSolverMode::CRYPTOMINISAT: d_satSolver.reset(prop::SatSolverFactory::createCryptoMinisat( - smtStatisticsRegistry(), "BVSolverBitblast")); + smtStatisticsRegistry(), "theory::bv::BVSolverBitblast")); break; default: d_satSolver.reset(prop::SatSolverFactory::createCadical( - smtStatisticsRegistry(), "BVSolverBitblast")); + smtStatisticsRegistry(), "theory::bv::BVSolverBitblast")); } d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(), d_nullRegistrar.get(), diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp index a36c4d4fb..a8670e1a6 100644 --- a/src/theory/bv/bv_solver_lazy.cpp +++ b/src/theory/bv/bv_solver_lazy.cpp @@ -124,33 +124,21 @@ void BVSolverLazy::spendResource(Resource r) } BVSolverLazy::Statistics::Statistics() - : d_avgConflictSize("theory::bv::lazy::AvgBVConflictSize"), - d_solveSubstitutions("theory::bv::lazy::NumSolveSubstitutions", 0), - d_solveTimer("theory::bv::lazy::solveTimer"), - d_numCallsToCheckFullEffort("theory::bv::lazy::NumFullCheckCalls", 0), - d_numCallsToCheckStandardEffort("theory::bv::lazy::NumStandardCheckCalls", - 0), - d_weightComputationTimer("theory::bv::lazy::weightComputationTimer"), - d_numMultSlice("theory::bv::lazy::NumMultSliceApplied", 0) + : d_avgConflictSize(smtStatisticsRegistry().registerAverage( + "theory::bv::lazy::AvgBVConflictSize")), + d_solveSubstitutions(smtStatisticsRegistry().registerInt( + "theory::bv::lazy::NumSolveSubstitutions")), + d_solveTimer(smtStatisticsRegistry().registerTimer( + "theory::bv::lazy::solveTimer")), + d_numCallsToCheckFullEffort(smtStatisticsRegistry().registerInt( + "theory::bv::lazy::NumFullCheckCalls")), + d_numCallsToCheckStandardEffort(smtStatisticsRegistry().registerInt( + "theory::bv::lazy::NumStandardCheckCalls")), + d_weightComputationTimer(smtStatisticsRegistry().registerTimer( + "theory::bv::lazy::weightComputationTimer")), + d_numMultSlice(smtStatisticsRegistry().registerInt( + "theory::bv::lazy::NumMultSliceApplied")) { - smtStatisticsRegistry()->registerStat(&d_avgConflictSize); - smtStatisticsRegistry()->registerStat(&d_solveSubstitutions); - smtStatisticsRegistry()->registerStat(&d_solveTimer); - smtStatisticsRegistry()->registerStat(&d_numCallsToCheckFullEffort); - smtStatisticsRegistry()->registerStat(&d_numCallsToCheckStandardEffort); - smtStatisticsRegistry()->registerStat(&d_weightComputationTimer); - smtStatisticsRegistry()->registerStat(&d_numMultSlice); -} - -BVSolverLazy::Statistics::~Statistics() -{ - smtStatisticsRegistry()->unregisterStat(&d_avgConflictSize); - smtStatisticsRegistry()->unregisterStat(&d_solveSubstitutions); - smtStatisticsRegistry()->unregisterStat(&d_solveTimer); - smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckFullEffort); - smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckStandardEffort); - smtStatisticsRegistry()->unregisterStat(&d_weightComputationTimer); - smtStatisticsRegistry()->unregisterStat(&d_numMultSlice); } void BVSolverLazy::preRegisterTerm(TNode node) diff --git a/src/theory/bv/bv_solver_lazy.h b/src/theory/bv/bv_solver_lazy.h index 42f59eda4..e11f525f3 100644 --- a/src/theory/bv/bv_solver_lazy.h +++ b/src/theory/bv/bv_solver_lazy.h @@ -119,7 +119,6 @@ class BVSolverLazy : public BVSolver TimerStat d_weightComputationTimer; IntStat d_numMultSlice; Statistics(); - ~Statistics(); }; Statistics d_statistics; diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index 254a9b13e..4c050b3f0 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -750,34 +750,23 @@ Node AlgebraicSolver::getModelValue(TNode node) { } AlgebraicSolver::Statistics::Statistics() - : d_numCallstoCheck("theory::bv::algebraic::NumCallsToCheck", 0) - , d_numSimplifiesToTrue("theory::bv::algebraic::NumSimplifiesToTrue", 0) - , d_numSimplifiesToFalse("theory::bv::algebraic::NumSimplifiesToFalse", 0) - , d_numUnsat("theory::bv::algebraic::NumUnsat", 0) - , d_numSat("theory::bv::algebraic::NumSat", 0) - , d_numUnknown("theory::bv::algebraic::NumUnknown", 0) - , d_solveTime("theory::bv::algebraic::SolveTime") - , d_useHeuristic("theory::bv::algebraic::UseHeuristic", 0.2) + : d_numCallstoCheck(smtStatisticsRegistry().registerInt( + "theory::bv::algebraic::NumCallsToCheck")), + d_numSimplifiesToTrue(smtStatisticsRegistry().registerInt( + "theory::bv::algebraic::NumSimplifiesToTrue")), + d_numSimplifiesToFalse(smtStatisticsRegistry().registerInt( + "theory::bv::algebraic::NumSimplifiesToFalse")), + d_numUnsat(smtStatisticsRegistry().registerInt( + "theory::bv::algebraic::NumUnsat")), + d_numSat( + smtStatisticsRegistry().registerInt("theory::bv::algebraic::NumSat")), + d_numUnknown(smtStatisticsRegistry().registerInt( + "theory::bv::algebraic::NumUnknown")), + d_solveTime(smtStatisticsRegistry().registerTimer( + "theory::bv::algebraic::SolveTime")), + d_useHeuristic(smtStatisticsRegistry().registerValue<double>( + "theory::bv::algebraic::UseHeuristic", 0.2)) { - smtStatisticsRegistry()->registerStat(&d_numCallstoCheck); - smtStatisticsRegistry()->registerStat(&d_numSimplifiesToTrue); - smtStatisticsRegistry()->registerStat(&d_numSimplifiesToFalse); - smtStatisticsRegistry()->registerStat(&d_numUnsat); - smtStatisticsRegistry()->registerStat(&d_numSat); - smtStatisticsRegistry()->registerStat(&d_numUnknown); - smtStatisticsRegistry()->registerStat(&d_solveTime); - smtStatisticsRegistry()->registerStat(&d_useHeuristic); -} - -AlgebraicSolver::Statistics::~Statistics() { - smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck); - smtStatisticsRegistry()->unregisterStat(&d_numSimplifiesToTrue); - smtStatisticsRegistry()->unregisterStat(&d_numSimplifiesToFalse); - smtStatisticsRegistry()->unregisterStat(&d_numUnsat); - smtStatisticsRegistry()->unregisterStat(&d_numSat); - smtStatisticsRegistry()->unregisterStat(&d_numUnknown); - smtStatisticsRegistry()->unregisterStat(&d_solveTime); - smtStatisticsRegistry()->unregisterStat(&d_useHeuristic); } bool hasExpensiveBVOperatorsRec(TNode fact, TNodeSet& seen) { diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h index 93fe9d21d..670adafa3 100644 --- a/src/theory/bv/bv_subtheory_algebraic.h +++ b/src/theory/bv/bv_subtheory_algebraic.h @@ -163,9 +163,8 @@ class AlgebraicSolver : public SubtheorySolver IntStat d_numSat; IntStat d_numUnknown; TimerStat d_solveTime; - BackedStat<double> d_useHeuristic; + ValueStat<double> d_useHeuristic; Statistics(); - ~Statistics(); }; std::unique_ptr<SubstitutionMap> d_modelMap; diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index 70c9d9de6..b86809a91 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -54,15 +54,11 @@ BitblastSolver::BitblastSolver(context::Context* c, BVSolverLazy* bv) BitblastSolver::~BitblastSolver() {} BitblastSolver::Statistics::Statistics() - : d_numCallstoCheck("theory::bv::BitblastSolver::NumCallsToCheck", 0) - , d_numBBLemmas("theory::bv::BitblastSolver::NumTimesLemmasBB", 0) + : d_numCallstoCheck(smtStatisticsRegistry().registerInt( + "theory::bv::BitblastSolver::NumCallsToCheck")), + d_numBBLemmas(smtStatisticsRegistry().registerInt( + "theory::bv::BitblastSolver::NumTimesLemmasBB")) { - smtStatisticsRegistry()->registerStat(&d_numCallstoCheck); - smtStatisticsRegistry()->registerStat(&d_numBBLemmas); -} -BitblastSolver::Statistics::~Statistics() { - smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck); - smtStatisticsRegistry()->unregisterStat(&d_numBBLemmas); } void BitblastSolver::setAbstraction(AbstractionModule* abs) { diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index a3238ae61..903a5136e 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -41,7 +41,6 @@ class BitblastSolver : public SubtheorySolver IntStat d_numCallstoCheck; IntStat d_numBBLemmas; Statistics(); - ~Statistics(); }; /** Bitblaster */ std::unique_ptr<TLazyBitblaster> d_bitblaster; diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index 0a391f474..7f3099f8c 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -484,12 +484,9 @@ void CoreSolver::addTermToEqualityEngine(TNode node) } CoreSolver::Statistics::Statistics() - : d_numCallstoCheck("theory::bv::CoreSolver::NumCallsToCheck", 0) + : d_numCallstoCheck(smtStatisticsRegistry().registerInt( + "theory::bv::CoreSolver::NumCallsToCheck")) { - smtStatisticsRegistry()->registerStat(&d_numCallstoCheck); -} -CoreSolver::Statistics::~Statistics() { - smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck); } void CoreSolver::checkExtf(Theory::Effort e) diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h index 2400eb31b..52d9e739a 100644 --- a/src/theory/bv/bv_subtheory_core.h +++ b/src/theory/bv/bv_subtheory_core.h @@ -58,7 +58,6 @@ class CoreSolver : public SubtheorySolver { struct Statistics { IntStat d_numCallstoCheck; Statistics(); - ~Statistics(); }; // NotifyClass: handles call-back from congruence closure module diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index 3613584fe..10b9a346e 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -246,15 +246,9 @@ bool InequalitySolver::addInequality(TNode a, TNode b, bool strict, TNode fact) } InequalitySolver::Statistics::Statistics() - : d_numCallstoCheck("theory::bv::inequality::NumCallsToCheck", 0), - d_solveTime("theory::bv::inequality::SolveTime") + : d_numCallstoCheck(smtStatisticsRegistry().registerInt( + "theory::bv::inequality::NumCallsToCheck")), + d_solveTime(smtStatisticsRegistry().registerTimer( + "theory::bv::inequality::SolveTime")) { - smtStatisticsRegistry()->registerStat(&d_numCallstoCheck); - smtStatisticsRegistry()->registerStat(&d_solveTime); -} - -InequalitySolver::Statistics::~Statistics() -{ - smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck); - smtStatisticsRegistry()->unregisterStat(&d_solveTime); } diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h index b554062c0..65eee95e1 100644 --- a/src/theory/bv/bv_subtheory_inequality.h +++ b/src/theory/bv/bv_subtheory_inequality.h @@ -49,7 +49,6 @@ class InequalitySolver : public SubtheorySolver IntStat d_numCallstoCheck; TimerStat d_solveTime; Statistics(); - ~Statistics(); }; context::CDHashSet<Node, NodeHashFunction> d_assertionSet; diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 107d6313c..06f837c7f 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -39,7 +39,7 @@ TheoryBV::TheoryBV(context::Context* c, d_internal(nullptr), d_rewriter(), d_state(c, u, valuation), - d_im(*this, d_state, nullptr, "theory::bv"), + d_im(*this, d_state, nullptr, "theory::bv::"), d_notify(d_im) { switch (options::bvSolver()) diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index 412c824aa..72906929b 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -29,7 +29,7 @@ #include "smt/smt_engine_scope.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory.h" -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp index e459ec05b..393813590 100644 --- a/src/theory/datatypes/inference_manager.cpp +++ b/src/theory/datatypes/inference_manager.cpp @@ -33,7 +33,7 @@ namespace datatypes { InferenceManager::InferenceManager(Theory& t, TheoryState& state, ProofNodeManager* pnm) - : InferenceManagerBuffered(t, state, pnm, "theory::datatypes"), + : InferenceManagerBuffered(t, state, pnm, "theory::datatypes::"), d_pnm(pnm), d_ipc(pnm == nullptr ? nullptr : new InferProofCons(state.getSatContext(), pnm)), diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp index d5ce5ab79..b1f35821f 100644 --- a/src/theory/engine_output_channel.cpp +++ b/src/theory/engine_output_channel.cpp @@ -26,32 +26,21 @@ namespace cvc5 { namespace theory { EngineOutputChannel::Statistics::Statistics(theory::TheoryId theory) - : conflicts(getStatsPrefix(theory) + "::conflicts", 0), - propagations(getStatsPrefix(theory) + "::propagations", 0), - lemmas(getStatsPrefix(theory) + "::lemmas", 0), - requirePhase(getStatsPrefix(theory) + "::requirePhase", 0), - restartDemands(getStatsPrefix(theory) + "::restartDemands", 0), - trustedConflicts(getStatsPrefix(theory) + "::trustedConflicts", 0), - trustedLemmas(getStatsPrefix(theory) + "::trustedLemmas", 0) + : conflicts(smtStatisticsRegistry().registerInt(getStatsPrefix(theory) + + "conflicts")), + propagations(smtStatisticsRegistry().registerInt(getStatsPrefix(theory) + + "propagations")), + lemmas(smtStatisticsRegistry().registerInt(getStatsPrefix(theory) + + "lemmas")), + requirePhase(smtStatisticsRegistry().registerInt(getStatsPrefix(theory) + + "requirePhase")), + restartDemands(smtStatisticsRegistry().registerInt(getStatsPrefix(theory) + + "restartDemands")), + trustedConflicts(smtStatisticsRegistry().registerInt( + getStatsPrefix(theory) + "trustedConflicts")), + trustedLemmas(smtStatisticsRegistry().registerInt(getStatsPrefix(theory) + + "trustedLemmas")) { - smtStatisticsRegistry()->registerStat(&conflicts); - smtStatisticsRegistry()->registerStat(&propagations); - smtStatisticsRegistry()->registerStat(&lemmas); - smtStatisticsRegistry()->registerStat(&requirePhase); - smtStatisticsRegistry()->registerStat(&restartDemands); - smtStatisticsRegistry()->registerStat(&trustedConflicts); - smtStatisticsRegistry()->registerStat(&trustedLemmas); -} - -EngineOutputChannel::Statistics::~Statistics() -{ - smtStatisticsRegistry()->unregisterStat(&conflicts); - smtStatisticsRegistry()->unregisterStat(&propagations); - smtStatisticsRegistry()->unregisterStat(&lemmas); - smtStatisticsRegistry()->unregisterStat(&requirePhase); - smtStatisticsRegistry()->unregisterStat(&restartDemands); - smtStatisticsRegistry()->unregisterStat(&trustedConflicts); - smtStatisticsRegistry()->unregisterStat(&trustedLemmas); } EngineOutputChannel::EngineOutputChannel(TheoryEngine* engine, diff --git a/src/theory/engine_output_channel.h b/src/theory/engine_output_channel.h index ff9bdfa64..dcf8fba55 100644 --- a/src/theory/engine_output_channel.h +++ b/src/theory/engine_output_channel.h @@ -21,7 +21,7 @@ #include "expr/node.h" #include "theory/output_channel.h" #include "theory/theory_id.h" -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" namespace cvc5 { @@ -89,7 +89,6 @@ class EngineOutputChannel : public theory::OutputChannel { public: Statistics(theory::TheoryId theory); - ~Statistics(); /** Number of calls to conflict, propagate, lemma, requirePhase, * restartDemands */ IntStat conflicts, propagations, lemmas, requirePhase, restartDemands, diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 80a5c539b..4bcb761a5 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -122,7 +122,7 @@ TheoryFp::TheoryFp(context::Context* c, d_floatToRealMap(u), d_abstractionMap(u), d_state(c, u, valuation), - d_im(*this, d_state, pnm, "theory::fp", false) + d_im(*this, d_state, pnm, "theory::fp::", false) { // indicate we are using the default theory state and inference manager d_theoryState = &d_state; diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp index 42fe40faf..534d59aeb 100644 --- a/src/theory/inference_manager_buffered.cpp +++ b/src/theory/inference_manager_buffered.cpp @@ -27,9 +27,9 @@ namespace theory { InferenceManagerBuffered::InferenceManagerBuffered(Theory& t, TheoryState& state, ProofNodeManager* pnm, - const std::string& name, + const std::string& statsName, bool cacheLemmas) - : TheoryInferenceManager(t, state, pnm, name, cacheLemmas), + : TheoryInferenceManager(t, state, pnm, statsName, cacheLemmas), d_processingPendingLemmas(false) { } diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h index 5dd01b802..080033562 100644 --- a/src/theory/inference_manager_buffered.h +++ b/src/theory/inference_manager_buffered.h @@ -35,7 +35,7 @@ class InferenceManagerBuffered : public TheoryInferenceManager InferenceManagerBuffered(Theory& t, TheoryState& state, ProofNodeManager* pnm, - const std::string& name, + const std::string& statsName, bool cacheLemmas = true); virtual ~InferenceManagerBuffered() {} /** diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h index 2264127cf..0279a72ca 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h @@ -22,7 +22,7 @@ #include "expr/node.h" #include "theory/inference_id.h" -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index 7ab0f1b8f..266de9a53 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -25,7 +25,7 @@ #include "theory/quantifiers/cegqi/vts_term_cache.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quant_module.h" -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 5f83578df..0415d4271 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -742,23 +742,15 @@ InstLemmaList* Instantiate::getOrMkInstLemmaList(TNode q) } Instantiate::Statistics::Statistics() - : d_instantiations("Instantiate::Instantiations_Total", 0), - d_inst_duplicate("Instantiate::Duplicate_Inst", 0), - d_inst_duplicate_eq("Instantiate::Duplicate_Inst_Eq", 0), - d_inst_duplicate_ent("Instantiate::Duplicate_Inst_Entailed", 0) + : d_instantiations(smtStatisticsRegistry().registerInt( + "Instantiate::Instantiations_Total")), + d_inst_duplicate( + smtStatisticsRegistry().registerInt("Instantiate::Duplicate_Inst")), + d_inst_duplicate_eq(smtStatisticsRegistry().registerInt( + "Instantiate::Duplicate_Inst_Eq")), + d_inst_duplicate_ent(smtStatisticsRegistry().registerInt( + "Instantiate::Duplicate_Inst_Entailed")) { - smtStatisticsRegistry()->registerStat(&d_instantiations); - smtStatisticsRegistry()->registerStat(&d_inst_duplicate); - smtStatisticsRegistry()->registerStat(&d_inst_duplicate_eq); - smtStatisticsRegistry()->registerStat(&d_inst_duplicate_ent); -} - -Instantiate::Statistics::~Statistics() -{ - smtStatisticsRegistry()->unregisterStat(&d_instantiations); - smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate); - smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_eq); - smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_ent); } } // namespace quantifiers diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index f420c0f62..42bff316a 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -26,7 +26,7 @@ #include "theory/inference_id.h" #include "theory/quantifiers/inst_match_trie.h" #include "theory/quantifiers/quant_util.h" -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" namespace cvc5 { @@ -290,7 +290,6 @@ class Instantiate : public QuantifiersUtil IntStat d_inst_duplicate_eq; IntStat d_inst_duplicate_ent; Statistics(); - ~Statistics(); }; /* class Instantiate::Statistics */ Statistics d_statistics; diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 791f843fa..cff9fde0b 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -2270,17 +2270,12 @@ void QuantConflictFind::debugPrintQuantBody( const char * c, Node q, Node n, boo } } -QuantConflictFind::Statistics::Statistics(): - d_inst_rounds("QuantConflictFind::Inst_Rounds", 0), - d_entailment_checks("QuantConflictFind::Entailment_Checks",0) +QuantConflictFind::Statistics::Statistics() + : d_inst_rounds( + smtStatisticsRegistry().registerInt("QuantConflictFind::Inst_Rounds")), + d_entailment_checks(smtStatisticsRegistry().registerInt( + "QuantConflictFind::Entailment_Checks")) { - smtStatisticsRegistry()->registerStat(&d_inst_rounds); - smtStatisticsRegistry()->registerStat(&d_entailment_checks); -} - -QuantConflictFind::Statistics::~Statistics(){ - smtStatisticsRegistry()->unregisterStat(&d_inst_rounds); - smtStatisticsRegistry()->unregisterStat(&d_entailment_checks); } TNode QuantConflictFind::getZero( Kind k ) { diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index b533a3f12..5a36452fe 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -287,7 +287,6 @@ public: IntStat d_inst_rounds; IntStat d_entailment_checks; Statistics(); - ~Statistics(); }; Statistics d_statistics; /** Identify this module */ diff --git a/src/theory/quantifiers/quantifiers_inference_manager.cpp b/src/theory/quantifiers/quantifiers_inference_manager.cpp index 0f7c65924..67f8f6f8e 100644 --- a/src/theory/quantifiers/quantifiers_inference_manager.cpp +++ b/src/theory/quantifiers/quantifiers_inference_manager.cpp @@ -28,7 +28,7 @@ QuantifiersInferenceManager::QuantifiersInferenceManager( QuantifiersRegistry& qr, TermRegistry& tr, ProofNodeManager* pnm) - : InferenceManagerBuffered(t, state, pnm, "theory::quantifiers"), + : InferenceManagerBuffered(t, state, pnm, "theory::quantifiers::"), d_instantiate(new Instantiate(state, *this, qr, tr, pnm)), d_skolemize(new Skolemize(state, tr, pnm)) { diff --git a/src/theory/quantifiers/quantifiers_statistics.cpp b/src/theory/quantifiers/quantifiers_statistics.cpp index e3c17fd77..59fdb1808 100644 --- a/src/theory/quantifiers/quantifiers_statistics.cpp +++ b/src/theory/quantifiers/quantifiers_statistics.cpp @@ -22,42 +22,27 @@ namespace theory { namespace quantifiers { QuantifiersStatistics::QuantifiersStatistics() - : d_time("theory::QuantifiersEngine::time"), - d_qcf_time("theory::QuantifiersEngine::time_qcf"), - d_ematching_time("theory::QuantifiersEngine::time_ematching"), - d_num_quant("QuantifiersEngine::Num_Quantifiers", 0), - d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0), - d_instantiation_rounds_lc( - "QuantifiersEngine::Rounds_Instantiation_Last_Call", 0), - d_triggers("QuantifiersEngine::Triggers", 0), - d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0), - d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0), - d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0) + : d_time(smtStatisticsRegistry().registerTimer( + "theory::QuantifiersEngine::time")), + d_qcf_time(smtStatisticsRegistry().registerTimer( + "theory::QuantifiersEngine::time_qcf")), + d_ematching_time(smtStatisticsRegistry().registerTimer( + "theory::QuantifiersEngine::time_ematching")), + d_num_quant(smtStatisticsRegistry().registerInt( + "QuantifiersEngine::Num_Quantifiers")), + d_instantiation_rounds(smtStatisticsRegistry().registerInt( + "QuantifiersEngine::Rounds_Instantiation_Full")), + d_instantiation_rounds_lc(smtStatisticsRegistry().registerInt( + "QuantifiersEngine::Rounds_Instantiation_Last_Call")), + d_triggers( + smtStatisticsRegistry().registerInt("QuantifiersEngine::Triggers")), + d_simple_triggers(smtStatisticsRegistry().registerInt( + "QuantifiersEngine::Triggers_Simple")), + d_multi_triggers(smtStatisticsRegistry().registerInt( + "QuantifiersEngine::Triggers_Multi")), + d_red_alpha_equiv(smtStatisticsRegistry().registerInt( + "QuantifiersEngine::Reductions_Alpha_Equivalence")) { - smtStatisticsRegistry()->registerStat(&d_time); - smtStatisticsRegistry()->registerStat(&d_qcf_time); - smtStatisticsRegistry()->registerStat(&d_ematching_time); - smtStatisticsRegistry()->registerStat(&d_num_quant); - smtStatisticsRegistry()->registerStat(&d_instantiation_rounds); - smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc); - smtStatisticsRegistry()->registerStat(&d_triggers); - smtStatisticsRegistry()->registerStat(&d_simple_triggers); - smtStatisticsRegistry()->registerStat(&d_multi_triggers); - smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv); -} - -QuantifiersStatistics::~QuantifiersStatistics() -{ - smtStatisticsRegistry()->unregisterStat(&d_time); - smtStatisticsRegistry()->unregisterStat(&d_qcf_time); - smtStatisticsRegistry()->unregisterStat(&d_ematching_time); - smtStatisticsRegistry()->unregisterStat(&d_num_quant); - smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds); - smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc); - smtStatisticsRegistry()->unregisterStat(&d_triggers); - smtStatisticsRegistry()->unregisterStat(&d_simple_triggers); - smtStatisticsRegistry()->unregisterStat(&d_multi_triggers); - smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv); } } // namespace quantifiers diff --git a/src/theory/quantifiers/quantifiers_statistics.h b/src/theory/quantifiers/quantifiers_statistics.h index f03d27ee3..438efd30f 100644 --- a/src/theory/quantifiers/quantifiers_statistics.h +++ b/src/theory/quantifiers/quantifiers_statistics.h @@ -18,8 +18,7 @@ #ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H #define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H -#include "util/statistics_registry.h" -#include "util/stats_timer.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { @@ -33,7 +32,6 @@ class QuantifiersStatistics { public: QuantifiersStatistics(); - ~QuantifiersStatistics(); TimerStat d_time; TimerStat d_qcf_time; TimerStat d_ematching_time; diff --git a/src/theory/quantifiers/sygus/sygus_stats.cpp b/src/theory/quantifiers/sygus/sygus_stats.cpp index 4fe0e9bbc..19d799eb3 100644 --- a/src/theory/quantifiers/sygus/sygus_stats.cpp +++ b/src/theory/quantifiers/sygus/sygus_stats.cpp @@ -22,40 +22,26 @@ namespace theory { namespace quantifiers { SygusStatistics::SygusStatistics() - : d_cegqi_lemmas_ce("SynthEngine::cegqi_lemmas_ce", 0), - d_cegqi_lemmas_refine("SynthEngine::cegqi_lemmas_refine", 0), - d_cegqi_si_lemmas("SynthEngine::cegqi_lemmas_si", 0), - d_solutions("SynthConjecture::solutions", 0), - d_filtered_solutions("SynthConjecture::filtered_solutions", 0), - d_candidate_rewrites_print("SynthConjecture::candidate_rewrites_print", - 0), - d_enumTermsRewrite("SygusEnumerator::enumTermsRewrite", 0), - d_enumTermsExampleEval("SygusEnumerator::enumTermsEvalExamples", 0), - d_enumTerms("SygusEnumerator::enumTerms", 0) + : d_cegqi_lemmas_ce( + smtStatisticsRegistry().registerInt("SynthEngine::cegqi_lemmas_ce")), + d_cegqi_lemmas_refine(smtStatisticsRegistry().registerInt( + "SynthEngine::cegqi_lemmas_refine")), + d_cegqi_si_lemmas( + smtStatisticsRegistry().registerInt("SynthEngine::cegqi_lemmas_si")), + d_solutions( + smtStatisticsRegistry().registerInt("SynthConjecture::solutions")), + d_filtered_solutions(smtStatisticsRegistry().registerInt( + "SynthConjecture::filtered_solutions")), + d_candidate_rewrites_print(smtStatisticsRegistry().registerInt( + "SynthConjecture::candidate_rewrites_print")), + d_enumTermsRewrite(smtStatisticsRegistry().registerInt( + "SygusEnumerator::enumTermsRewrite")), + d_enumTermsExampleEval(smtStatisticsRegistry().registerInt( + "SygusEnumerator::enumTermsEvalExamples")), + d_enumTerms( + smtStatisticsRegistry().registerInt("SygusEnumerator::enumTerms")) { - smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_ce); - smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_refine); - smtStatisticsRegistry()->registerStat(&d_cegqi_si_lemmas); - smtStatisticsRegistry()->registerStat(&d_solutions); - smtStatisticsRegistry()->registerStat(&d_filtered_solutions); - smtStatisticsRegistry()->registerStat(&d_candidate_rewrites_print); - smtStatisticsRegistry()->registerStat(&d_enumTermsRewrite); - smtStatisticsRegistry()->registerStat(&d_enumTermsExampleEval); - smtStatisticsRegistry()->registerStat(&d_enumTerms); -} - -SygusStatistics::~SygusStatistics() -{ - smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_ce); - smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_refine); - smtStatisticsRegistry()->unregisterStat(&d_cegqi_si_lemmas); - smtStatisticsRegistry()->unregisterStat(&d_solutions); - smtStatisticsRegistry()->unregisterStat(&d_filtered_solutions); - smtStatisticsRegistry()->unregisterStat(&d_candidate_rewrites_print); - smtStatisticsRegistry()->unregisterStat(&d_enumTermsRewrite); - smtStatisticsRegistry()->unregisterStat(&d_enumTermsExampleEval); - smtStatisticsRegistry()->unregisterStat(&d_enumTerms); } } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/sygus_stats.h b/src/theory/quantifiers/sygus/sygus_stats.h index 20b0633aa..6236547f9 100644 --- a/src/theory/quantifiers/sygus/sygus_stats.h +++ b/src/theory/quantifiers/sygus/sygus_stats.h @@ -18,7 +18,7 @@ #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_STATS_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_STATS_H -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { @@ -31,7 +31,6 @@ class SygusStatistics { public: SygusStatistics(); - ~SygusStatistics(); /** Number of counterexample lemmas */ IntStat d_cegqi_lemmas_ce; /** Number of refinement lemmas */ diff --git a/src/theory/quantifiers/term_tuple_enumerator.cpp b/src/theory/quantifiers/term_tuple_enumerator.cpp index 4b714419f..2f21a50e1 100644 --- a/src/theory/quantifiers/term_tuple_enumerator.cpp +++ b/src/theory/quantifiers/term_tuple_enumerator.cpp @@ -31,7 +31,7 @@ #include "theory/quantifiers/term_pools.h" #include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" namespace cvc5 { diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 301299f11..22b77c4fb 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -50,7 +50,7 @@ TheorySep::TheorySep(context::Context* c, d_lemmas_produced_c(u), d_bounds_init(false), d_state(c, u, valuation), - d_im(*this, d_state, nullptr, "theory::sep"), + d_im(*this, d_state, nullptr, "theory::sep::"), d_notify(*this), d_reduce(u), d_spatial_assertions(c) diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index 2b90a46a3..3b8ec8b6b 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -28,7 +28,7 @@ #include "theory/theory.h" #include "theory/theory_state.h" #include "theory/uf/equality_engine.h" -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp index a2d7b33a5..73c6db35f 100644 --- a/src/theory/sets/inference_manager.cpp +++ b/src/theory/sets/inference_manager.cpp @@ -28,7 +28,7 @@ namespace sets { InferenceManager::InferenceManager(Theory& t, SolverState& s, ProofNodeManager* pnm) - : InferenceManagerBuffered(t, s, pnm, "theory::sets"), d_state(s) + : InferenceManagerBuffered(t, s, pnm, "theory::sets::"), d_state(s) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index 9e87e17a5..b9c331acc 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -29,7 +29,8 @@ SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine, context::UserContext* userContext, ProofNodeManager* pnm) : ContextNotifyObj(context), - d_statSharedTerms("theory::shared_terms", 0), + d_statSharedTerms( + smtStatisticsRegistry().registerInt("theory::shared_terms")), d_addedSharedTermsSize(context, 0), d_termsToTheories(context), d_alreadyNotifiedMap(context), @@ -44,12 +45,6 @@ SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine, d_pfee(nullptr), d_pnm(pnm) { - smtStatisticsRegistry()->registerStat(&d_statSharedTerms); -} - -SharedTermsDatabase::~SharedTermsDatabase() -{ - smtStatisticsRegistry()->unregisterStat(&d_statSharedTerms); } void SharedTermsDatabase::setEqualityEngine(eq::EqualityEngine* ee) diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index efc2b2154..655c2aa88 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -28,7 +28,7 @@ #include "theory/trust_node.h" #include "theory/uf/equality_engine.h" #include "theory/uf/proof_equality_engine.h" -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" namespace cvc5 { @@ -163,7 +163,6 @@ class SharedTermsDatabase : public context::ContextNotifyObj { context::Context* context, context::UserContext* userContext, ProofNodeManager* pnm); - ~SharedTermsDatabase(); //-------------------------------------------- initialization /** Called to set the equality engine. */ diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index 7bb8bd3c1..e00668997 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -19,6 +19,7 @@ #include "theory/strings/sequences_rewriter.h" #include "theory/strings/theory_strings_preprocess.h" #include "theory/strings/theory_strings_utils.h" +#include "util/statistics_registry.h" using namespace std; using namespace cvc5::context; diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index 8797e3fcd..2351e7bf3 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -23,6 +23,7 @@ #include "theory/rewriter.h" #include "theory/strings/regexp_operation.h" #include "theory/strings/theory_strings_utils.h" +#include "util/statistics_registry.h" using namespace cvc5::kind; diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 06bd4acc2..3dbb6b89b 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -35,7 +35,7 @@ InferenceManager::InferenceManager(Theory& t, ExtTheory& e, SequencesStatistics& statistics, ProofNodeManager* pnm) - : InferenceManagerBuffered(t, s, pnm, "theory::strings", false), + : InferenceManagerBuffered(t, s, pnm, "theory::strings::", false), d_state(s), d_termReg(tr), d_extt(e), diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 05c218fa4..38fc6fc8f 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -22,6 +22,7 @@ #include "theory/ext_theory.h" #include "theory/strings/theory_strings_utils.h" #include "theory/theory_model.h" +#include "util/statistics_value.h" using namespace std; using namespace cvc5::context; diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index fa372771b..431f488a5 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -24,6 +24,7 @@ #include "theory/strings/strings_rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/statistics_registry.h" using namespace std; using namespace cvc5::kind; @@ -32,7 +33,7 @@ namespace cvc5 { namespace theory { namespace strings { -SequencesRewriter::SequencesRewriter(IntegralHistogramStat<Rewrite>* statistics) +SequencesRewriter::SequencesRewriter(HistogramStat<Rewrite>* statistics) : d_statistics(statistics), d_stringsEntail(*this) { } diff --git a/src/theory/strings/sequences_rewriter.h b/src/theory/strings/sequences_rewriter.h index 1564a5ebc..97db2c7f4 100644 --- a/src/theory/strings/sequences_rewriter.h +++ b/src/theory/strings/sequences_rewriter.h @@ -33,7 +33,7 @@ namespace strings { class SequencesRewriter : public TheoryRewriter { public: - SequencesRewriter(IntegralHistogramStat<Rewrite>* statistics); + SequencesRewriter(HistogramStat<Rewrite>* statistics); protected: /** rewrite regular expression concatenation @@ -288,7 +288,7 @@ class SequencesRewriter : public TheoryRewriter static Node canonicalStrForSymbolicLength(Node n, TypeNode stype); /** Reference to the rewriter statistics. */ - IntegralHistogramStat<Rewrite>* d_statistics; + HistogramStat<Rewrite>* d_statistics; /** Instance of the entailment checker for strings. */ StringsEntail d_stringsEntail; diff --git a/src/theory/strings/sequences_stats.cpp b/src/theory/strings/sequences_stats.cpp index b27df959e..2c4834de2 100644 --- a/src/theory/strings/sequences_stats.cpp +++ b/src/theory/strings/sequences_stats.cpp @@ -22,44 +22,29 @@ namespace theory { namespace strings { SequencesStatistics::SequencesStatistics() - : d_checkRuns("theory::strings::checkRuns", 0), - d_strategyRuns("theory::strings::strategyRuns", 0), - d_inferencesNoPf("theory::strings::inferencesNoPf"), - d_cdSimplifications("theory::strings::cdSimplifications"), - d_reductions("theory::strings::reductions"), - d_regexpUnfoldingsPos("theory::strings::regexpUnfoldingsPos"), - d_regexpUnfoldingsNeg("theory::strings::regexpUnfoldingsNeg"), - d_rewrites("theory::strings::rewrites"), - d_conflictsEqEngine("theory::strings::conflictsEqEngine", 0), - d_conflictsEager("theory::strings::conflictsEager", 0), - d_conflictsInfer("theory::strings::conflictsInfer", 0) + : d_checkRuns( + smtStatisticsRegistry().registerInt("theory::strings::checkRuns")), + d_strategyRuns( + smtStatisticsRegistry().registerInt("theory::strings::strategyRuns")), + d_inferencesNoPf(smtStatisticsRegistry().registerHistogram<InferenceId>( + "theory::strings::inferencesNoPf")), + d_cdSimplifications(smtStatisticsRegistry().registerHistogram<Kind>( + "theory::strings::cdSimplifications")), + d_reductions(smtStatisticsRegistry().registerHistogram<Kind>( + "theory::strings::reductions")), + d_regexpUnfoldingsPos(smtStatisticsRegistry().registerHistogram<Kind>( + "theory::strings::regexpUnfoldingsPos")), + d_regexpUnfoldingsNeg(smtStatisticsRegistry().registerHistogram<Kind>( + "theory::strings::regexpUnfoldingsNeg")), + d_rewrites(smtStatisticsRegistry().registerHistogram<Rewrite>( + "theory::strings::rewrites")), + d_conflictsEqEngine(smtStatisticsRegistry().registerInt( + "theory::strings::conflictsEqEngine")), + d_conflictsEager(smtStatisticsRegistry().registerInt( + "theory::strings::conflictsEager")), + d_conflictsInfer(smtStatisticsRegistry().registerInt( + "theory::strings::conflictsInfer")) { - smtStatisticsRegistry()->registerStat(&d_checkRuns); - smtStatisticsRegistry()->registerStat(&d_strategyRuns); - smtStatisticsRegistry()->registerStat(&d_inferencesNoPf); - smtStatisticsRegistry()->registerStat(&d_cdSimplifications); - smtStatisticsRegistry()->registerStat(&d_reductions); - smtStatisticsRegistry()->registerStat(&d_regexpUnfoldingsPos); - smtStatisticsRegistry()->registerStat(&d_regexpUnfoldingsNeg); - smtStatisticsRegistry()->registerStat(&d_rewrites); - smtStatisticsRegistry()->registerStat(&d_conflictsEqEngine); - smtStatisticsRegistry()->registerStat(&d_conflictsEager); - smtStatisticsRegistry()->registerStat(&d_conflictsInfer); -} - -SequencesStatistics::~SequencesStatistics() -{ - smtStatisticsRegistry()->unregisterStat(&d_checkRuns); - smtStatisticsRegistry()->unregisterStat(&d_strategyRuns); - smtStatisticsRegistry()->unregisterStat(&d_inferencesNoPf); - smtStatisticsRegistry()->unregisterStat(&d_cdSimplifications); - smtStatisticsRegistry()->unregisterStat(&d_reductions); - smtStatisticsRegistry()->unregisterStat(&d_regexpUnfoldingsPos); - smtStatisticsRegistry()->unregisterStat(&d_regexpUnfoldingsNeg); - smtStatisticsRegistry()->unregisterStat(&d_rewrites); - smtStatisticsRegistry()->unregisterStat(&d_conflictsEqEngine); - smtStatisticsRegistry()->unregisterStat(&d_conflictsEager); - smtStatisticsRegistry()->unregisterStat(&d_conflictsInfer); } } diff --git a/src/theory/strings/sequences_stats.h b/src/theory/strings/sequences_stats.h index e442fcc0c..398b8894d 100644 --- a/src/theory/strings/sequences_stats.h +++ b/src/theory/strings/sequences_stats.h @@ -21,8 +21,7 @@ #include "expr/kind.h" #include "theory/strings/infer_info.h" #include "theory/strings/rewrites.h" -#include "util/statistics_registry.h" -#include "util/stats_histogram.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { @@ -53,7 +52,6 @@ class SequencesStatistics { public: SequencesStatistics(); - ~SequencesStatistics(); /** Number of calls to run a check where strategy is present */ IntStat d_checkRuns; /** Number of calls to run the strategy */ @@ -65,29 +63,29 @@ class SequencesStatistics * TheoryInferenceManager, i.e. * (theory::strings::inferences{Facts,Lemmas,Conflicts}). */ - IntegralHistogramStat<InferenceId> d_inferencesNoPf; + HistogramStat<InferenceId> d_inferencesNoPf; /** * Counts the number of applications of each type of context-dependent * simplification. The sum of this map is equal to the number of EXTF or * EXTF_N inferences. */ - IntegralHistogramStat<Kind> d_cdSimplifications; + HistogramStat<Kind> d_cdSimplifications; /** * Counts the number of applications of each type of reduction. The sum of * this map is equal to the number of REDUCTION inferences (when * options::stringLazyPreproc is true). */ - IntegralHistogramStat<Kind> d_reductions; + HistogramStat<Kind> d_reductions; /** * Counts the number of applications of each type of regular expression * positive (resp. negative) unfoldings. The sum of this map is equal to the * number of RE_UNFOLD_POS (resp. RE_UNFOLD_NEG) inferences. */ - IntegralHistogramStat<Kind> d_regexpUnfoldingsPos; - IntegralHistogramStat<Kind> d_regexpUnfoldingsNeg; + HistogramStat<Kind> d_regexpUnfoldingsPos; + HistogramStat<Kind> d_regexpUnfoldingsNeg; //--------------- end of inferences /** Counts the number of applications of each type of rewrite rule */ - IntegralHistogramStat<Rewrite> d_rewrites; + HistogramStat<Rewrite> d_rewrites; //--------------- conflicts, partition of calls to OutputChannel::conflict /** Number of equality engine conflicts */ IntStat d_conflictsEqEngine; diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp index 4ef3f7c96..41a8ac448 100644 --- a/src/theory/strings/strings_rewriter.cpp +++ b/src/theory/strings/strings_rewriter.cpp @@ -26,7 +26,7 @@ namespace cvc5 { namespace theory { namespace strings { -StringsRewriter::StringsRewriter(IntegralHistogramStat<Rewrite>* statistics) +StringsRewriter::StringsRewriter(HistogramStat<Rewrite>* statistics) : SequencesRewriter(statistics) { } diff --git a/src/theory/strings/strings_rewriter.h b/src/theory/strings/strings_rewriter.h index bfe780535..70a1cccf0 100644 --- a/src/theory/strings/strings_rewriter.h +++ b/src/theory/strings/strings_rewriter.h @@ -32,7 +32,7 @@ namespace strings { class StringsRewriter : public SequencesRewriter { public: - StringsRewriter(IntegralHistogramStat<Rewrite>* statistics); + StringsRewriter(HistogramStat<Rewrite>* statistics); RewriteResponse postRewrite(TNode node) override; diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 5e6b27e1b..1cc0736fb 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -25,6 +25,7 @@ #include "theory/strings/arith_entail.h" #include "theory/strings/sequences_rewriter.h" #include "theory/strings/word.h" +#include "util/statistics_registry.h" using namespace cvc5; using namespace cvc5::kind; @@ -41,7 +42,7 @@ struct QInternalVarAttributeId typedef expr::Attribute<QInternalVarAttributeId, Node> QInternalVarAttribute; StringsPreprocess::StringsPreprocess(SkolemCache* sc, - IntegralHistogramStat<Kind>* statReductions) + HistogramStat<Kind>* statReductions) : d_sc(sc), d_statReductions(statReductions) { } diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index fe190532d..7f0efe50f 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -40,7 +40,7 @@ namespace strings { class StringsPreprocess { public: StringsPreprocess(SkolemCache* sc, - IntegralHistogramStat<Kind>* statReductions = nullptr); + HistogramStat<Kind>* statReductions = nullptr); ~StringsPreprocess(); /** The reduce routine * @@ -82,7 +82,7 @@ class StringsPreprocess { /** pointer to the skolem cache used by this class */ SkolemCache* d_sc; /** Reference to the statistics for the theory of strings/sequences. */ - IntegralHistogramStat<Kind>* d_statReductions; + HistogramStat<Kind>* d_statReductions; /** visited cache */ std::map<Node, Node> d_visited; /** diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 78a83c4da..859356341 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -75,9 +75,10 @@ Theory::Theory(TheoryId id, d_sharedTermsIndex(satContext, 0), d_careGraph(nullptr), d_instanceName(name), - d_checkTime(getStatsPrefix(id) + name + "::checkTime"), - d_computeCareGraphTime(getStatsPrefix(id) + name - + "::computeCareGraphTime"), + d_checkTime(smtStatisticsRegistry().registerTimer(getStatsPrefix(id) + + name + "checkTime")), + d_computeCareGraphTime(smtStatisticsRegistry().registerTimer( + getStatsPrefix(id) + name + "computeCareGraphTime")), d_sharedTerms(satContext), d_out(&out), d_valuation(valuation), @@ -88,13 +89,9 @@ Theory::Theory(TheoryId id, d_quantEngine(nullptr), d_pnm(pnm) { - smtStatisticsRegistry()->registerStat(&d_checkTime); - smtStatisticsRegistry()->registerStat(&d_computeCareGraphTime); } Theory::~Theory() { - smtStatisticsRegistry()->unregisterStat(&d_checkTime); - smtStatisticsRegistry()->unregisterStat(&d_computeCareGraphTime); } bool Theory::needsEqualityEngine(EeSetupInfo& esi) diff --git a/src/theory/theory.h b/src/theory/theory.h index 3d3ec0627..247ebcf46 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -35,8 +35,7 @@ #include "theory/theory_id.h" #include "theory/trust_node.h" #include "theory/valuation.h" -#include "util/statistics_registry.h" -#include "util/stats_timer.h" +#include "util/statistics_stats.h" namespace cvc5 { diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 79f9c660f..b4ad09d77 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -218,10 +218,9 @@ TheoryEngine::TheoryEngine(context::Context* context, d_outMgr(outMgr), d_pnm(pnm), d_lazyProof( - d_pnm != nullptr - ? new LazyCDProof( - d_pnm, nullptr, d_userContext, "TheoryEngine::LazyCDProof") - : nullptr), + d_pnm != nullptr ? new LazyCDProof( + d_pnm, nullptr, d_userContext, "TheoryEngine::LazyCDProof") + : nullptr), d_tepg(new TheoryEngineProofGenerator(d_pnm, d_userContext)), d_tc(nullptr), d_sharedSolver(nullptr), @@ -240,7 +239,8 @@ TheoryEngine::TheoryEngine(context::Context* context, d_propagatedLiterals(context), d_propagatedLiteralsIndex(context, 0), d_atomRequests(context), - d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"), + d_combineTheoriesTime(smtStatisticsRegistry().registerTimer( + "TheoryEngine::combineTheoriesTime")), d_true(), d_false(), d_interrupted(false), @@ -261,7 +261,6 @@ TheoryEngine::TheoryEngine(context::Context* context, d_sortInfer.reset(new SortInference); } - smtStatisticsRegistry()->registerStat(&d_combineTheoriesTime); d_true = NodeManager::currentNM()->mkConst<bool>(true); d_false = NodeManager::currentNM()->mkConst<bool>(false); } @@ -275,8 +274,6 @@ TheoryEngine::~TheoryEngine() { delete d_theoryOut[theoryId]; } } - - smtStatisticsRegistry()->unregisterStat(&d_combineTheoriesTime); } void TheoryEngine::interrupt() { d_interrupted = true; } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index dcf4ff2c8..3eacdaa20 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -37,7 +37,7 @@ #include "theory/uf/equality_engine.h" #include "theory/valuation.h" #include "util/hash.h" -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" #include "util/unsafe_interrupt_exception.h" namespace cvc5 { diff --git a/src/theory/theory_id.cpp b/src/theory/theory_id.cpp index d3f225f79..d9b25bf98 100644 --- a/src/theory/theory_id.cpp +++ b/src/theory/theory_id.cpp @@ -59,23 +59,23 @@ std::string getStatsPrefix(TheoryId theoryId) { switch (theoryId) { - case THEORY_BUILTIN: return "theory::builtin"; break; - case THEORY_BOOL: return "theory::bool"; break; - case THEORY_UF: return "theory::uf"; break; - case THEORY_ARITH: return "theory::arith"; break; - case THEORY_BV: return "theory::bv"; break; - case THEORY_FP: return "theory::fp"; break; - case THEORY_ARRAYS: return "theory::arrays"; break; - case THEORY_DATATYPES: return "theory::datatypes"; break; - case THEORY_SEP: return "theory::sep"; break; - case THEORY_SETS: return "theory::sets"; break; - case THEORY_BAGS: return "theory::bags"; break; - case THEORY_STRINGS: return "theory::strings"; break; - case THEORY_QUANTIFIERS: return "theory::quantifiers"; break; + case THEORY_BUILTIN: return "theory::builtin::"; break; + case THEORY_BOOL: return "theory::bool::"; break; + case THEORY_UF: return "theory::uf::"; break; + case THEORY_ARITH: return "theory::arith::"; break; + case THEORY_BV: return "theory::bv::"; break; + case THEORY_FP: return "theory::fp::"; break; + case THEORY_ARRAYS: return "theory::arrays::"; break; + case THEORY_DATATYPES: return "theory::datatypes::"; break; + case THEORY_SEP: return "theory::sep::"; break; + case THEORY_SETS: return "theory::sets::"; break; + case THEORY_BAGS: return "theory::bags::"; break; + case THEORY_STRINGS: return "theory::strings::"; break; + case THEORY_QUANTIFIERS: return "theory::quantifiers::"; break; default: break; } - return "unknown"; + return "unknown::"; } TheoryId TheoryIdSetUtil::setPop(TheoryIdSet& set) diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index e52321c49..3bc7351fe 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -31,7 +31,7 @@ namespace theory { TheoryInferenceManager::TheoryInferenceManager(Theory& t, TheoryState& state, ProofNodeManager* pnm, - const std::string& name, + const std::string& statsName, bool cacheLemmas) : d_theory(t), d_theoryState(state), @@ -45,23 +45,20 @@ TheoryInferenceManager::TheoryInferenceManager(Theory& t, d_numConflicts(0), d_numCurrentLemmas(0), d_numCurrentFacts(0), - d_conflictIdStats(name + "::inferencesConflict"), - d_factIdStats(name + "::inferencesFact"), - d_lemmaIdStats(name + "::inferencesLemma") + d_conflictIdStats(smtStatisticsRegistry().registerHistogram<InferenceId>( + statsName + "inferencesConflict")), + d_factIdStats(smtStatisticsRegistry().registerHistogram<InferenceId>( + statsName + "inferencesFact")), + d_lemmaIdStats(smtStatisticsRegistry().registerHistogram<InferenceId>( + statsName + "inferencesLemma")) { // don't add true lemma Node truen = NodeManager::currentNM()->mkConst(true); d_lemmasSent.insert(truen); - smtStatisticsRegistry()->registerStat(&d_conflictIdStats); - smtStatisticsRegistry()->registerStat(&d_factIdStats); - smtStatisticsRegistry()->registerStat(&d_lemmaIdStats); } TheoryInferenceManager::~TheoryInferenceManager() { - smtStatisticsRegistry()->unregisterStat(&d_conflictIdStats); - smtStatisticsRegistry()->unregisterStat(&d_factIdStats); - smtStatisticsRegistry()->unregisterStat(&d_lemmaIdStats); } void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee) diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index 89c4aec3f..a785af186 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -26,8 +26,7 @@ #include "theory/inference_id.h" #include "theory/output_channel.h" #include "theory/trust_node.h" -#include "util/statistics_registry.h" -#include "util/stats_histogram.h" +#include "util/statistics_stats.h" namespace cvc5 { @@ -79,8 +78,8 @@ class TheoryInferenceManager * @param state The state of the theory * @param pnm The proof node manager, which if non-null, enables proofs for * this inference manager - * @param name The name of the inference manager, which is used for giving - * unique names for statistics, + * @param statsName The name of the inference manager, which is used for + * giving unique names for statistics, * @param cacheLemmas Whether all lemmas sent using this theory inference * manager are added to a user-context dependent cache. This means that * only lemmas that are unique after rewriting are sent to the theory engine @@ -89,7 +88,7 @@ class TheoryInferenceManager TheoryInferenceManager(Theory& t, TheoryState& state, ProofNodeManager* pnm, - const std::string& name, + const std::string& statsName, bool cacheLemmas = true); virtual ~TheoryInferenceManager(); //--------------------------------------- initialization @@ -454,11 +453,11 @@ class TheoryInferenceManager /** The number of internal facts added since the last call to reset. */ uint32_t d_numCurrentFacts; /** Statistics for conflicts sent via this inference manager. */ - IntegralHistogramStat<InferenceId> d_conflictIdStats; + HistogramStat<InferenceId> d_conflictIdStats; /** Statistics for facts sent via this inference manager. */ - IntegralHistogramStat<InferenceId> d_factIdStats; + HistogramStat<InferenceId> d_factIdStats; /** Statistics for lemmas sent via this inference manager. */ - IntegralHistogramStat<InferenceId> d_lemmaIdStats; + HistogramStat<InferenceId> d_lemmaIdStats; }; } // namespace theory diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp index b45ccbac3..25f87de2c 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -1748,23 +1748,16 @@ void CardinalityExtension::checkCombinedCardinality() } CardinalityExtension::Statistics::Statistics() - : d_clique_conflicts("CardinalityExtension::Clique_Conflicts", 0), - d_clique_lemmas("CardinalityExtension::Clique_Lemmas", 0), - d_split_lemmas("CardinalityExtension::Split_Lemmas", 0), - d_max_model_size("CardinalityExtension::Max_Model_Size", 1) + : d_clique_conflicts(smtStatisticsRegistry().registerInt( + "CardinalityExtension::Clique_Conflicts")), + d_clique_lemmas(smtStatisticsRegistry().registerInt( + "CardinalityExtension::Clique_Lemmas")), + d_split_lemmas(smtStatisticsRegistry().registerInt( + "CardinalityExtension::Split_Lemmas")), + d_max_model_size(smtStatisticsRegistry().registerInt( + "CardinalityExtension::Max_Model_Size")) { - smtStatisticsRegistry()->registerStat(&d_clique_conflicts); - smtStatisticsRegistry()->registerStat(&d_clique_lemmas); - smtStatisticsRegistry()->registerStat(&d_split_lemmas); - smtStatisticsRegistry()->registerStat(&d_max_model_size); -} - -CardinalityExtension::Statistics::~Statistics() -{ - smtStatisticsRegistry()->unregisterStat(&d_clique_conflicts); - smtStatisticsRegistry()->unregisterStat(&d_clique_lemmas); - smtStatisticsRegistry()->unregisterStat(&d_split_lemmas); - smtStatisticsRegistry()->unregisterStat(&d_max_model_size); + d_max_model_size.maxAssign(1); } } // namespace uf diff --git a/src/theory/uf/cardinality_extension.h b/src/theory/uf/cardinality_extension.h index 53c850897..70db9257f 100644 --- a/src/theory/uf/cardinality_extension.h +++ b/src/theory/uf/cardinality_extension.h @@ -22,7 +22,7 @@ #include "context/context.h" #include "theory/decision_strategy.h" #include "theory/theory.h" -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { @@ -397,7 +397,6 @@ class CardinalityExtension IntStat d_split_lemmas; IntStat d_max_model_size; Statistics(); - ~Statistics(); }; /** statistics class */ Statistics d_statistics; diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index fe7b0ab84..7124a8890 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -29,23 +29,14 @@ namespace cvc5 { namespace theory { namespace eq { -EqualityEngine::Statistics::Statistics(std::string name) - : d_mergesCount(name + "::mergesCount", 0), - d_termsCount(name + "::termsCount", 0), - d_functionTermsCount(name + "::functionTermsCount", 0), - d_constantTermsCount(name + "::constantTermsCount", 0) +EqualityEngine::Statistics::Statistics(const std::string& name) + : d_mergesCount(smtStatisticsRegistry().registerInt(name + "mergesCount")), + d_termsCount(smtStatisticsRegistry().registerInt(name + "termsCount")), + d_functionTermsCount( + smtStatisticsRegistry().registerInt(name + "functionTermsCount")), + d_constantTermsCount( + smtStatisticsRegistry().registerInt(name + "constantTermsCount")) { - smtStatisticsRegistry()->registerStat(&d_mergesCount); - smtStatisticsRegistry()->registerStat(&d_termsCount); - smtStatisticsRegistry()->registerStat(&d_functionTermsCount); - smtStatisticsRegistry()->registerStat(&d_constantTermsCount); -} - -EqualityEngine::Statistics::~Statistics() { - smtStatisticsRegistry()->unregisterStat(&d_mergesCount); - smtStatisticsRegistry()->unregisterStat(&d_termsCount); - smtStatisticsRegistry()->unregisterStat(&d_functionTermsCount); - smtStatisticsRegistry()->unregisterStat(&d_constantTermsCount); } /** @@ -128,7 +119,7 @@ EqualityEngine::EqualityEngine(context::Context* context, d_assertedEqualitiesCount(context, 0), d_equalityTriggersCount(context, 0), d_subtermEvaluatesSize(context, 0), - d_stats(name), + d_stats(name + "::"), d_inPropagate(false), d_constantsAreTriggers(constantsAreTriggers), d_anyTermsAreTriggers(anyTermTriggers), @@ -158,7 +149,7 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, d_assertedEqualitiesCount(context, 0), d_equalityTriggersCount(context, 0), d_subtermEvaluatesSize(context, 0), - d_stats(name), + d_stats(name + "::"), d_inPropagate(false), d_constantsAreTriggers(constantsAreTriggers), d_anyTermsAreTriggers(anyTermTriggers), diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index d8a8f3916..8676e446e 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -34,7 +34,7 @@ #include "theory/uf/equality_engine_iterator.h" #include "theory/uf/equality_engine_notify.h" #include "theory/uf/equality_engine_types.h" -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { @@ -109,9 +109,7 @@ class EqualityEngine : public context::ContextNotifyObj { /** Number of constant terms managed by the system */ IntStat d_constantTermsCount; - Statistics(std::string name); - - ~Statistics(); + Statistics(const std::string& name); };/* struct EqualityEngine::statistics */ private: diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index 49b056f5a..65ed4d542 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -164,21 +164,20 @@ void SymmetryBreaker::Template::reset() { d_reps.clear(); } -SymmetryBreaker::SymmetryBreaker(context::Context* context, - std::string name) : - ContextNotifyObj(context), - d_assertionsToRerun(context), - d_rerunningAssertions(false), - d_phi(), - d_phiSet(), - d_permutations(), - d_terms(), - d_template(), - d_normalizationCache(), - d_termEqs(), - d_termEqsOnly(), - d_name(name), - d_stats(d_name) +SymmetryBreaker::SymmetryBreaker(context::Context* context, std::string name) + : ContextNotifyObj(context), + d_assertionsToRerun(context), + d_rerunningAssertions(false), + d_phi(), + d_phiSet(), + d_permutations(), + d_terms(), + d_template(), + d_normalizationCache(), + d_termEqs(), + d_termEqsOnly(), + d_name(name), + d_stats(d_name + "theory::uf::symmetry_breaker::") { } @@ -750,33 +749,20 @@ void SymmetryBreaker::selectTerms(const Permutation& p) { } } -SymmetryBreaker::Statistics::Statistics(std::string name) - : d_clauses(name + "theory::uf::symmetry_breaker::clauses", 0) - , d_units(name + "theory::uf::symmetry_breaker::units", 0) - , d_permutationSetsConsidered(name + "theory::uf::symmetry_breaker::permutationSetsConsidered", 0) - , d_permutationSetsInvariant(name + "theory::uf::symmetry_breaker::permutationSetsInvariant", 0) - , d_invariantByPermutationsTimer(name + "theory::uf::symmetry_breaker::timers::invariantByPermutations") - , d_selectTermsTimer(name + "theory::uf::symmetry_breaker::timers::selectTerms") - , d_initNormalizationTimer(name + "theory::uf::symmetry_breaker::timers::initNormalization") -{ - smtStatisticsRegistry()->registerStat(&d_clauses); - smtStatisticsRegistry()->registerStat(&d_units); - smtStatisticsRegistry()->registerStat(&d_permutationSetsConsidered); - smtStatisticsRegistry()->registerStat(&d_permutationSetsInvariant); - smtStatisticsRegistry()->registerStat(&d_invariantByPermutationsTimer); - smtStatisticsRegistry()->registerStat(&d_selectTermsTimer); - smtStatisticsRegistry()->registerStat(&d_initNormalizationTimer); -} - -SymmetryBreaker::Statistics::~Statistics() +SymmetryBreaker::Statistics::Statistics(const std::string& name) + : d_clauses(smtStatisticsRegistry().registerInt(name + "clauses")), + d_units(smtStatisticsRegistry().registerInt(name + "units")), + d_permutationSetsConsidered(smtStatisticsRegistry().registerInt( + name + "permutationSetsConsidered")), + d_permutationSetsInvariant(smtStatisticsRegistry().registerInt( + name + "permutationSetsInvariant")), + d_invariantByPermutationsTimer(smtStatisticsRegistry().registerTimer( + name + "timers::invariantByPermutations")), + d_selectTermsTimer( + smtStatisticsRegistry().registerTimer(name + "timers::selectTerms")), + d_initNormalizationTimer(smtStatisticsRegistry().registerTimer( + name + "timers::initNormalization")) { - smtStatisticsRegistry()->unregisterStat(&d_clauses); - smtStatisticsRegistry()->unregisterStat(&d_units); - smtStatisticsRegistry()->unregisterStat(&d_permutationSetsConsidered); - smtStatisticsRegistry()->unregisterStat(&d_permutationSetsInvariant); - smtStatisticsRegistry()->unregisterStat(&d_invariantByPermutationsTimer); - smtStatisticsRegistry()->unregisterStat(&d_selectTermsTimer); - smtStatisticsRegistry()->unregisterStat(&d_initNormalizationTimer); } SymmetryBreaker::Terms::iterator diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h index eb78f9101..b5d0fbdf9 100644 --- a/src/theory/uf/symmetry_breaker.h +++ b/src/theory/uf/symmetry_breaker.h @@ -52,8 +52,7 @@ #include "expr/node.h" #include "expr/node_builder.h" #include "smt/smt_statistics_registry.h" -#include "util/statistics_registry.h" -#include "util/stats_timer.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { @@ -147,8 +146,7 @@ private: /** time spent in initial round of normalization */ TimerStat d_initNormalizationTimer; - Statistics(std::string name); - ~Statistics(); + Statistics(const std::string& name); }; Statistics d_stats; diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 9fa86f402..5d91faa87 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -53,7 +53,7 @@ TheoryUF::TheoryUF(context::Context* c, d_functionsTerms(c), d_symb(u, instanceName), d_state(c, u, valuation), - d_im(*this, d_state, pnm, "theory::uf", false), + d_im(*this, d_state, pnm, "theory::uf::" + instanceName, false), d_notify(d_im, *this) { d_true = NodeManager::currentNM()->mkConst( true ); |