diff options
Diffstat (limited to 'src/theory/arith')
30 files changed, 352 insertions, 626 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); }; |