diff options
author | Tim King <taking@google.com> | 2016-01-08 16:44:57 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-01-08 16:44:57 -0800 |
commit | f4ef7af0a2295691f281ee1604dfeb4082fe229c (patch) | |
tree | 995e512e5669cec6bbc9447d00ec912d5e4c19e3 /src/theory/arith | |
parent | def0a07f9676a292a849d7fc8269ffd0901ce156 (diff) |
Removing StatisticsRegistry's static functions current() and registerStat().
- The functionality the get the StatisticsRegistry attached to the SmtEngine was previously through StatisticsRegistry::current(). This is the dominant StatisticsRegistry in the code. (There is another StatisticsRegistry attached to the NodeManager.) Having this be a static function on StatisticsRegistry requires the use of an SmtEngine in the wrong compilation unit.
- Usages of StatisticsRegistry::current() that were visible in prop/{bvminisat,minisat} has been removed. A pointer to the relevant StatisticsRegistry should be passed instead into the constructor.
- The function StatisticsRegistry::current() has been replaced by SmtScope::currentStatisticsRegistry(). SmtScope is in the libcvc4 package, where SmtEngine is available in the compilation unit.
- The function smtStatisticsRegistry() is a synonym for SmtScope::currentStatisticsRegistry() in smt/smt_statistics_registry.h. This header has fewer include dependencies than the one for SmtScope.
- Correspondingly, the static functions StatisticsRegistry::{registerStat, unregisterStat} have been removed. One should instead use smtStatisticsRegistry()->{registerStat,unregisterStat} instead.
- The KEEP_STATISTIC macro has been moved into smt/smt_statistics_registry.h.
- Documents the reason StatisticsRegistry is CVC4_PUBLIC. This lets me remove the warning I added.
- Removing most operators for timespec from statistics_registry.h file. These a bit error prone in clang.
- Most of the really confusing ifdef's in util/statistics_registry.h are gone.
Diffstat (limited to 'src/theory/arith')
26 files changed, 412 insertions, 398 deletions
diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp index 71ac18e84..5bbe29bc5 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/approx_simplex.cpp @@ -14,6 +14,7 @@ ** [[ Add lengthier description here ]] ** \todo document this file **/ +#include "theory/arith/approx_simplex.h" #include <cfloat> #include <cmath> @@ -22,7 +23,7 @@ #include "base/output.h" #include "cvc4autoconfig.h" -#include "theory/arith/approx_simplex.h" +#include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" #include "theory/arith/cut_log.h" #include "theory/arith/matrix.h" @@ -169,67 +170,67 @@ ApproximateStatistics::ApproximateStatistics() , d_gaussianElimConstruct("z::approx::gaussianElimConstruct::calls",0) , d_averageGuesses("z::approx::averageGuesses") { - // StatisticsRegistry::registerStat(&d_relaxCalls); - // StatisticsRegistry::registerStat(&d_relaxUnknowns); - // StatisticsRegistry::registerStat(&d_relaxFeasible); - // StatisticsRegistry::registerStat(&d_relaxInfeasible); - // StatisticsRegistry::registerStat(&d_relaxPivotsExhausted); - - // StatisticsRegistry::registerStat(&d_mipCalls); - // StatisticsRegistry::registerStat(&d_mipUnknowns); - // StatisticsRegistry::registerStat(&d_mipBingo); - // StatisticsRegistry::registerStat(&d_mipClosed); - // StatisticsRegistry::registerStat(&d_mipBranchesExhausted); - // StatisticsRegistry::registerStat(&d_mipPivotsExhausted); - // StatisticsRegistry::registerStat(&d_mipExecExhausted); - - - // StatisticsRegistry::registerStat(&d_gmiGen); - // StatisticsRegistry::registerStat(&d_gmiReplay); - // StatisticsRegistry::registerStat(&d_mipGen); - // StatisticsRegistry::registerStat(&d_mipReplay); - - StatisticsRegistry::registerStat(&d_branchMaxDepth); - //StatisticsRegistry::registerStat(&d_branchTotal); - //StatisticsRegistry::registerStat(&d_branchCuts); - StatisticsRegistry::registerStat(&d_branchesMaxOnAVar); - - StatisticsRegistry::registerStat(&d_gaussianElimConstructTime); - StatisticsRegistry::registerStat(&d_gaussianElimConstruct); - - StatisticsRegistry::registerStat(&d_averageGuesses); + // smtStatisticsRegistry()->registerStat(&d_relaxCalls); + // smtStatisticsRegistry()->registerStat(&d_relaxUnknowns); + // smtStatisticsRegistry()->registerStat(&d_relaxFeasible); + // smtStatisticsRegistry()->registerStat(&d_relaxInfeasible); + // smtStatisticsRegistry()->registerStat(&d_relaxPivotsExhausted); + + // smtStatisticsRegistry()->registerStat(&d_mipCalls); + // smtStatisticsRegistry()->registerStat(&d_mipUnknowns); + // smtStatisticsRegistry()->registerStat(&d_mipBingo); + // smtStatisticsRegistry()->registerStat(&d_mipClosed); + // smtStatisticsRegistry()->registerStat(&d_mipBranchesExhausted); + // smtStatisticsRegistry()->registerStat(&d_mipPivotsExhausted); + // smtStatisticsRegistry()->registerStat(&d_mipExecExhausted); + + + // smtStatisticsRegistry()->registerStat(&d_gmiGen); + // smtStatisticsRegistry()->registerStat(&d_gmiReplay); + // smtStatisticsRegistry()->registerStat(&d_mipGen); + // smtStatisticsRegistry()->registerStat(&d_mipReplay); + + smtStatisticsRegistry()->registerStat(&d_branchMaxDepth); + //smtStatisticsRegistry()->registerStat(&d_branchTotal); + //smtStatisticsRegistry()->registerStat(&d_branchCuts); + smtStatisticsRegistry()->registerStat(&d_branchesMaxOnAVar); + + smtStatisticsRegistry()->registerStat(&d_gaussianElimConstructTime); + smtStatisticsRegistry()->registerStat(&d_gaussianElimConstruct); + + smtStatisticsRegistry()->registerStat(&d_averageGuesses); } ApproximateStatistics::~ApproximateStatistics(){ - // StatisticsRegistry::unregisterStat(&d_relaxCalls); - // StatisticsRegistry::unregisterStat(&d_relaxUnknowns); - // StatisticsRegistry::unregisterStat(&d_relaxFeasible); - // StatisticsRegistry::unregisterStat(&d_relaxInfeasible); - // StatisticsRegistry::unregisterStat(&d_relaxPivotsExhausted); - - // StatisticsRegistry::unregisterStat(&d_mipCalls); - // StatisticsRegistry::unregisterStat(&d_mipUnknowns); - // StatisticsRegistry::unregisterStat(&d_mipBingo); - // StatisticsRegistry::unregisterStat(&d_mipClosed); - // StatisticsRegistry::unregisterStat(&d_mipBranchesExhausted); - // StatisticsRegistry::unregisterStat(&d_mipPivotsExhausted); - // StatisticsRegistry::unregisterStat(&d_mipExecExhausted); - - - // StatisticsRegistry::unregisterStat(&d_gmiGen); - // StatisticsRegistry::unregisterStat(&d_gmiReplay); - // StatisticsRegistry::unregisterStat(&d_mipGen); - // StatisticsRegistry::unregisterStat(&d_mipReplay); - - StatisticsRegistry::unregisterStat(&d_branchMaxDepth); - //StatisticsRegistry::unregisterStat(&d_branchTotal); - //StatisticsRegistry::unregisterStat(&d_branchCuts); - StatisticsRegistry::unregisterStat(&d_branchesMaxOnAVar); - - StatisticsRegistry::unregisterStat(&d_gaussianElimConstructTime); - StatisticsRegistry::unregisterStat(&d_gaussianElimConstruct); - - StatisticsRegistry::unregisterStat(&d_averageGuesses); + // smtStatisticsRegistry()->unregisterStat(&d_relaxCalls); + // smtStatisticsRegistry()->unregisterStat(&d_relaxUnknowns); + // smtStatisticsRegistry()->unregisterStat(&d_relaxFeasible); + // smtStatisticsRegistry()->unregisterStat(&d_relaxInfeasible); + // smtStatisticsRegistry()->unregisterStat(&d_relaxPivotsExhausted); + + // smtStatisticsRegistry()->unregisterStat(&d_mipCalls); + // smtStatisticsRegistry()->unregisterStat(&d_mipUnknowns); + // smtStatisticsRegistry()->unregisterStat(&d_mipBingo); + // smtStatisticsRegistry()->unregisterStat(&d_mipClosed); + // smtStatisticsRegistry()->unregisterStat(&d_mipBranchesExhausted); + // smtStatisticsRegistry()->unregisterStat(&d_mipPivotsExhausted); + // smtStatisticsRegistry()->unregisterStat(&d_mipExecExhausted); + + + // smtStatisticsRegistry()->unregisterStat(&d_gmiGen); + // smtStatisticsRegistry()->unregisterStat(&d_gmiReplay); + // smtStatisticsRegistry()->unregisterStat(&d_mipGen); + // smtStatisticsRegistry()->unregisterStat(&d_mipReplay); + + smtStatisticsRegistry()->unregisterStat(&d_branchMaxDepth); + //smtStatisticsRegistry()->unregisterStat(&d_branchTotal); + //smtStatisticsRegistry()->unregisterStat(&d_branchCuts); + 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 064887787..97e6d6b3e 100644 --- a/src/theory/arith/approx_simplex.h +++ b/src/theory/arith/approx_simplex.h @@ -21,11 +21,11 @@ #pragma once #include <vector> -#include "expr/statistics_registry.h" #include "theory/arith/arithvar.h" #include "theory/arith/delta_rational.h" #include "util/dense_map.h" #include "util/rational.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index 383c6b418..aac792377 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -21,6 +21,7 @@ #include "expr/convenience_node_builders.h" #include "expr/expr.h" #include "options/arith_options.h" +#include "smt/smt_statistics_registry.h" #include "theory/arith/arith_static_learner.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/normal_form.h" @@ -48,13 +49,13 @@ ArithStaticLearner::Statistics::Statistics(): d_iteMinMaxApplications("theory::arith::iteMinMaxApplications", 0), d_iteConstantApplications("theory::arith::iteConstantApplications", 0) { - StatisticsRegistry::registerStat(&d_iteMinMaxApplications); - StatisticsRegistry::registerStat(&d_iteConstantApplications); + smtStatisticsRegistry()->registerStat(&d_iteMinMaxApplications); + smtStatisticsRegistry()->registerStat(&d_iteConstantApplications); } ArithStaticLearner::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_iteMinMaxApplications); - StatisticsRegistry::unregisterStat(&d_iteConstantApplications); + 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 2b0ee9dad..2aa9c9332 100644 --- a/src/theory/arith/arith_static_learner.h +++ b/src/theory/arith/arith_static_learner.h @@ -24,8 +24,8 @@ #include "context/cdtrail_hashmap.h" #include "context/context.h" -#include "expr/statistics_registry.h" #include "theory/arith/arith_utilities.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp index 737cc9e7b..d7b31e2e2 100644 --- a/src/theory/arith/attempt_solution_simplex.cpp +++ b/src/theory/arith/attempt_solution_simplex.cpp @@ -14,10 +14,11 @@ ** [[ Add lengthier description here ]] ** \todo document this file **/ +#include "theory/arith/attempt_solution_simplex.h" #include "base/output.h" #include "options/arith_options.h" -#include "theory/arith/attempt_solution_simplex.h" +#include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" using namespace std; @@ -36,15 +37,15 @@ AttemptSolutionSDP::Statistics::Statistics(): d_queueTime("theory::arith::attempt::queueTime"), d_conflicts("theory::arith::attempt::conflicts", 0) { - StatisticsRegistry::registerStat(&d_searchTime); - StatisticsRegistry::registerStat(&d_queueTime); - StatisticsRegistry::registerStat(&d_conflicts); + smtStatisticsRegistry()->registerStat(&d_searchTime); + smtStatisticsRegistry()->registerStat(&d_queueTime); + smtStatisticsRegistry()->registerStat(&d_conflicts); } AttemptSolutionSDP::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_searchTime); - StatisticsRegistry::unregisterStat(&d_queueTime); - StatisticsRegistry::unregisterStat(&d_conflicts); + 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 88d29f6b0..49a2dda29 100644 --- a/src/theory/arith/attempt_solution_simplex.h +++ b/src/theory/arith/attempt_solution_simplex.h @@ -53,9 +53,9 @@ #pragma once -#include "expr/statistics_registry.h" #include "theory/arith/simplex.h" #include "theory/arith/approx_simplex.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { @@ -94,4 +94,3 @@ private: }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ - diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index 964c92eb5..746121b70 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -13,10 +13,11 @@ ** [[ Add lengthier description here ]] ** \todo document this file **/ +#include "theory/arith/congruence_manager.h" #include "base/output.h" +#include "smt/smt_statistics_registry.h" #include "theory/arith/arith_utilities.h" -#include "theory/arith/congruence_manager.h" #include "theory/arith/constraint.h" namespace CVC4 { @@ -45,23 +46,23 @@ ArithCongruenceManager::Statistics::Statistics(): d_propagateConstraints("theory::arith::congruence::propagateConstraints", 0), d_conflicts("theory::arith::congruence::conflicts", 0) { - StatisticsRegistry::registerStat(&d_watchedVariables); - StatisticsRegistry::registerStat(&d_watchedVariableIsZero); - StatisticsRegistry::registerStat(&d_watchedVariableIsNotZero); - StatisticsRegistry::registerStat(&d_equalsConstantCalls); - StatisticsRegistry::registerStat(&d_propagations); - StatisticsRegistry::registerStat(&d_propagateConstraints); - StatisticsRegistry::registerStat(&d_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(){ - StatisticsRegistry::unregisterStat(&d_watchedVariables); - StatisticsRegistry::unregisterStat(&d_watchedVariableIsZero); - StatisticsRegistry::unregisterStat(&d_watchedVariableIsNotZero); - StatisticsRegistry::unregisterStat(&d_equalsConstantCalls); - StatisticsRegistry::unregisterStat(&d_propagations); - StatisticsRegistry::unregisterStat(&d_propagateConstraints); - StatisticsRegistry::unregisterStat(&d_conflicts); + 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 2fc9c47ed..138805b6e 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -24,12 +24,12 @@ #include "context/cdo.h" #include "context/cdtrail_queue.h" #include "context/context.h" -#include "expr/statistics_registry.h" #include "theory/arith/arithvar.h" #include "theory/arith/constraint_forward.h" #include "theory/arith/partial_model.h" #include "theory/uf/equality_engine.h" #include "util/dense_map.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index f13565a7f..5dc0ba1ac 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -14,14 +14,15 @@ ** [[ Add lengthier description here ]] ** \todo document this file **/ +#include "theory/arith/constraint.h" #include <ostream> #include <algorithm> #include "base/output.h" #include "proof/proof.h" +#include "smt/smt_statistics_registry.h" #include "theory/arith/arith_utilities.h" -#include "theory/arith/constraint.h" #include "theory/arith/normal_form.h" @@ -893,13 +894,14 @@ ConstraintDatabase::Statistics::Statistics(): d_unatePropagateCalls("theory::arith::cd::unatePropagateCalls", 0), d_unatePropagateImplications("theory::arith::cd::unatePropagateImplications", 0) { - StatisticsRegistry::registerStat(&d_unatePropagateCalls); - StatisticsRegistry::registerStat(&d_unatePropagateImplications); + smtStatisticsRegistry()->registerStat(&d_unatePropagateCalls); + smtStatisticsRegistry()->registerStat(&d_unatePropagateImplications); } + ConstraintDatabase::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_unatePropagateCalls); - StatisticsRegistry::unregisterStat(&d_unatePropagateImplications); + smtStatisticsRegistry()->unregisterStat(&d_unatePropagateCalls); + smtStatisticsRegistry()->unregisterStat(&d_unatePropagateImplications); } void ConstraintDatabase::deleteConstraintAndNegation(ConstraintP c){ diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h index f4d392995..054ab01e7 100644 --- a/src/theory/arith/cut_log.h +++ b/src/theory/arith/cut_log.h @@ -26,10 +26,10 @@ #include <vector> #include "expr/kind.h" -#include "expr/statistics_registry.h" #include "theory/arith/arithvar.h" #include "theory/arith/constraint_forward.h" #include "util/dense_map.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index f8b8e0e7b..71ad6de45 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -13,12 +13,13 @@ ** ** A Diophantine equation solver for the theory of arithmetic. **/ +#include "theory/arith/dio_solver.h" #include <iostream> #include "base/output.h" #include "options/arith_options.h" -#include "theory/arith/dio_solver.h" +#include "smt/smt_statistics_registry.h" using namespace std; @@ -56,25 +57,25 @@ DioSolver::Statistics::Statistics() : d_conflictTimer("theory::arith::dio::conflictTimer"), d_cutTimer("theory::arith::dio::cutTimer") { - StatisticsRegistry::registerStat(&d_conflictCalls); - StatisticsRegistry::registerStat(&d_cutCalls); + smtStatisticsRegistry()->registerStat(&d_conflictCalls); + smtStatisticsRegistry()->registerStat(&d_cutCalls); - StatisticsRegistry::registerStat(&d_cuts); - StatisticsRegistry::registerStat(&d_conflicts); + smtStatisticsRegistry()->registerStat(&d_cuts); + smtStatisticsRegistry()->registerStat(&d_conflicts); - StatisticsRegistry::registerStat(&d_conflictTimer); - StatisticsRegistry::registerStat(&d_cutTimer); + smtStatisticsRegistry()->registerStat(&d_conflictTimer); + smtStatisticsRegistry()->registerStat(&d_cutTimer); } DioSolver::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_conflictCalls); - StatisticsRegistry::unregisterStat(&d_cutCalls); + smtStatisticsRegistry()->unregisterStat(&d_conflictCalls); + smtStatisticsRegistry()->unregisterStat(&d_cutCalls); - StatisticsRegistry::unregisterStat(&d_cuts); - StatisticsRegistry::unregisterStat(&d_conflicts); + smtStatisticsRegistry()->unregisterStat(&d_cuts); + smtStatisticsRegistry()->unregisterStat(&d_conflicts); - StatisticsRegistry::unregisterStat(&d_conflictTimer); - StatisticsRegistry::unregisterStat(&d_cutTimer); + 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 626160b03..ccaff47c7 100644 --- a/src/theory/arith/dio_solver.h +++ b/src/theory/arith/dio_solver.h @@ -28,10 +28,10 @@ #include "context/cdo.h" #include "context/cdqueue.h" #include "context/context.h" -#include "expr/statistics_registry.h" #include "theory/arith/normal_form.h" #include "theory/arith/partial_model.h" #include "util/rational.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp index 32f81ded8..907d5eefb 100644 --- a/src/theory/arith/dual_simplex.cpp +++ b/src/theory/arith/dual_simplex.cpp @@ -14,11 +14,13 @@ ** [[ Add lengthier description here ]] ** \todo document this file **/ +#include "theory/arith/dual_simplex.h" #include "base/output.h" #include "options/arith_options.h" +#include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" -#include "theory/arith/dual_simplex.h" + using namespace std; @@ -40,21 +42,21 @@ DualSimplexDecisionProcedure::Statistics::Statistics(uint32_t& pivots): d_searchTime("theory::arith::dual::searchTime"), d_finalCheckPivotCounter("theory::arith::dual::lastPivots", pivots) { - StatisticsRegistry::registerStat(&d_statUpdateConflicts); - StatisticsRegistry::registerStat(&d_processSignalsTime); - StatisticsRegistry::registerStat(&d_simplexConflicts); - StatisticsRegistry::registerStat(&d_recentViolationCatches); - StatisticsRegistry::registerStat(&d_searchTime); - StatisticsRegistry::registerStat(&d_finalCheckPivotCounter); + 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(){ - StatisticsRegistry::unregisterStat(&d_statUpdateConflicts); - StatisticsRegistry::unregisterStat(&d_processSignalsTime); - StatisticsRegistry::unregisterStat(&d_simplexConflicts); - StatisticsRegistry::unregisterStat(&d_recentViolationCatches); - StatisticsRegistry::unregisterStat(&d_searchTime); - StatisticsRegistry::unregisterStat(&d_finalCheckPivotCounter); + 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 d6bf57bb0..e5ab76da8 100644 --- a/src/theory/arith/dual_simplex.h +++ b/src/theory/arith/dual_simplex.h @@ -52,8 +52,8 @@ #pragma once -#include "expr/statistics_registry.h" #include "theory/arith/simplex.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { @@ -111,4 +111,3 @@ private: }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ - diff --git a/src/theory/arith/error_set.cpp b/src/theory/arith/error_set.cpp index 14da973d8..e918f4c7d 100644 --- a/src/theory/arith/error_set.cpp +++ b/src/theory/arith/error_set.cpp @@ -15,8 +15,9 @@ ** \todo document this file **/ - #include "theory/arith/error_set.h" + +#include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" using namespace std; @@ -134,21 +135,21 @@ ErrorSet::Statistics::Statistics(): d_enqueuesCollectionDuplicates("theory::arith::pqueue::enqueuesCollectionDuplicates", 0), d_enqueuesVarOrderModeDuplicates("theory::arith::pqueue::enqueuesVarOrderModeDuplicates", 0) { - StatisticsRegistry::registerStat(&d_enqueues); - StatisticsRegistry::registerStat(&d_enqueuesCollection); - StatisticsRegistry::registerStat(&d_enqueuesDiffMode); - StatisticsRegistry::registerStat(&d_enqueuesVarOrderMode); - StatisticsRegistry::registerStat(&d_enqueuesCollectionDuplicates); - StatisticsRegistry::registerStat(&d_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(){ - StatisticsRegistry::unregisterStat(&d_enqueues); - StatisticsRegistry::unregisterStat(&d_enqueuesCollection); - StatisticsRegistry::unregisterStat(&d_enqueuesDiffMode); - StatisticsRegistry::unregisterStat(&d_enqueuesVarOrderMode); - StatisticsRegistry::unregisterStat(&d_enqueuesCollectionDuplicates); - StatisticsRegistry::unregisterStat(&d_enqueuesVarOrderModeDuplicates); + 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, TableauSizes tabSizes, BoundCountingLookup lookups): diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h index f12e38c12..fb3117a98 100644 --- a/src/theory/arith/error_set.h +++ b/src/theory/arith/error_set.h @@ -22,7 +22,6 @@ #include <vector> -#include "expr/statistics_registry.h" #include "options/arith_heuristic_pivot_rule.h" #include "theory/arith/arithvar.h" #include "theory/arith/bound_counts.h" @@ -31,6 +30,7 @@ #include "theory/arith/partial_model.h" #include "theory/arith/tableau_sizes.h" #include "util/bin_heap.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp index 229dc379c..888e29732 100644 --- a/src/theory/arith/fc_simplex.cpp +++ b/src/theory/arith/fc_simplex.cpp @@ -17,9 +17,10 @@ #include "theory/arith/fc_simplex.h" #include "base/output.h" -#include "expr/statistics_registry.h" #include "options/arith_options.h" +#include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" +#include "util/statistics_registry.h" using namespace std; @@ -52,37 +53,37 @@ FCSimplexDecisionProcedure::Statistics::Statistics(uint32_t& pivots): d_selectUpdateForPrimal("theory::arith::FC::selectUpdateForPrimal"), d_finalCheckPivotCounter("theory::arith::FC::lastPivots", pivots) { - StatisticsRegistry::registerStat(&d_initialSignalsTime); - StatisticsRegistry::registerStat(&d_initialConflicts); + smtStatisticsRegistry()->registerStat(&d_initialSignalsTime); + smtStatisticsRegistry()->registerStat(&d_initialConflicts); - StatisticsRegistry::registerStat(&d_fcFoundUnsat); - StatisticsRegistry::registerStat(&d_fcFoundSat); - StatisticsRegistry::registerStat(&d_fcMissed); + smtStatisticsRegistry()->registerStat(&d_fcFoundUnsat); + smtStatisticsRegistry()->registerStat(&d_fcFoundSat); + smtStatisticsRegistry()->registerStat(&d_fcMissed); - StatisticsRegistry::registerStat(&d_fcTimer); - StatisticsRegistry::registerStat(&d_fcFocusConstructionTimer); + smtStatisticsRegistry()->registerStat(&d_fcTimer); + smtStatisticsRegistry()->registerStat(&d_fcFocusConstructionTimer); - StatisticsRegistry::registerStat(&d_selectUpdateForDualLike); - StatisticsRegistry::registerStat(&d_selectUpdateForPrimal); + smtStatisticsRegistry()->registerStat(&d_selectUpdateForDualLike); + smtStatisticsRegistry()->registerStat(&d_selectUpdateForPrimal); - StatisticsRegistry::registerStat(&d_finalCheckPivotCounter); + smtStatisticsRegistry()->registerStat(&d_finalCheckPivotCounter); } FCSimplexDecisionProcedure::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_initialSignalsTime); - StatisticsRegistry::unregisterStat(&d_initialConflicts); + smtStatisticsRegistry()->unregisterStat(&d_initialSignalsTime); + smtStatisticsRegistry()->unregisterStat(&d_initialConflicts); - StatisticsRegistry::unregisterStat(&d_fcFoundUnsat); - StatisticsRegistry::unregisterStat(&d_fcFoundSat); - StatisticsRegistry::unregisterStat(&d_fcMissed); + smtStatisticsRegistry()->unregisterStat(&d_fcFoundUnsat); + smtStatisticsRegistry()->unregisterStat(&d_fcFoundSat); + smtStatisticsRegistry()->unregisterStat(&d_fcMissed); - StatisticsRegistry::unregisterStat(&d_fcTimer); - StatisticsRegistry::unregisterStat(&d_fcFocusConstructionTimer); + smtStatisticsRegistry()->unregisterStat(&d_fcTimer); + smtStatisticsRegistry()->unregisterStat(&d_fcFocusConstructionTimer); - StatisticsRegistry::unregisterStat(&d_selectUpdateForDualLike); - StatisticsRegistry::unregisterStat(&d_selectUpdateForPrimal); + smtStatisticsRegistry()->unregisterStat(&d_selectUpdateForDualLike); + smtStatisticsRegistry()->unregisterStat(&d_selectUpdateForPrimal); - StatisticsRegistry::unregisterStat(&d_finalCheckPivotCounter); + 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 471804003..c416af1c6 100644 --- a/src/theory/arith/fc_simplex.h +++ b/src/theory/arith/fc_simplex.h @@ -54,9 +54,9 @@ #include <stdint.h> -#include "expr/statistics_registry.h" #include "theory/arith/simplex.h" #include "util/dense_map.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { @@ -255,4 +255,3 @@ private: }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ - diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp index d8888bd75..6d86a1ab1 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear_equality.cpp @@ -13,11 +13,12 @@ ** ** This implements the LinearEqualityModule. **/ - +#include "theory/arith/linear_equality.h" #include "base/output.h" +#include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" -#include "theory/arith/linear_equality.h" + using namespace std; @@ -76,31 +77,31 @@ LinearEqualityModule::Statistics::Statistics(): d_weakenTime("theory::arith::weakening::time"), d_forceTime("theory::arith::forcing::time") { - StatisticsRegistry::registerStat(&d_statPivots); - StatisticsRegistry::registerStat(&d_statUpdates); + smtStatisticsRegistry()->registerStat(&d_statPivots); + smtStatisticsRegistry()->registerStat(&d_statUpdates); - StatisticsRegistry::registerStat(&d_pivotTime); - StatisticsRegistry::registerStat(&d_adjTime); + smtStatisticsRegistry()->registerStat(&d_pivotTime); + smtStatisticsRegistry()->registerStat(&d_adjTime); - StatisticsRegistry::registerStat(&d_weakeningAttempts); - StatisticsRegistry::registerStat(&d_weakeningSuccesses); - StatisticsRegistry::registerStat(&d_weakenings); - StatisticsRegistry::registerStat(&d_weakenTime); - StatisticsRegistry::registerStat(&d_forceTime); + smtStatisticsRegistry()->registerStat(&d_weakeningAttempts); + smtStatisticsRegistry()->registerStat(&d_weakeningSuccesses); + smtStatisticsRegistry()->registerStat(&d_weakenings); + smtStatisticsRegistry()->registerStat(&d_weakenTime); + smtStatisticsRegistry()->registerStat(&d_forceTime); } LinearEqualityModule::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_statPivots); - StatisticsRegistry::unregisterStat(&d_statUpdates); - StatisticsRegistry::unregisterStat(&d_pivotTime); - StatisticsRegistry::unregisterStat(&d_adjTime); + smtStatisticsRegistry()->unregisterStat(&d_statPivots); + smtStatisticsRegistry()->unregisterStat(&d_statUpdates); + smtStatisticsRegistry()->unregisterStat(&d_pivotTime); + smtStatisticsRegistry()->unregisterStat(&d_adjTime); - StatisticsRegistry::unregisterStat(&d_weakeningAttempts); - StatisticsRegistry::unregisterStat(&d_weakeningSuccesses); - StatisticsRegistry::unregisterStat(&d_weakenings); - StatisticsRegistry::unregisterStat(&d_weakenTime); - StatisticsRegistry::unregisterStat(&d_forceTime); + 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 d7c9c038c..f3cf17d81 100644 --- a/src/theory/arith/linear_equality.h +++ b/src/theory/arith/linear_equality.h @@ -29,7 +29,6 @@ #pragma once -#include "expr/statistics_registry.h" #include "options/arith_options.h" #include "theory/arith/arithvar.h" #include "theory/arith/constraint_forward.h" @@ -38,6 +37,7 @@ #include "theory/arith/simplex_update.h" #include "theory/arith/tableau.h" #include "util/maybe.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp index 765e6a00d..df32ec8a4 100644 --- a/src/theory/arith/soi_simplex.cpp +++ b/src/theory/arith/soi_simplex.cpp @@ -19,10 +19,10 @@ #include <algorithm> #include "base/output.h" -#include "expr/statistics_registry.h" #include "options/arith_options.h" +#include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" - +#include "util/statistics_registry.h" using namespace std; @@ -56,46 +56,46 @@ SumOfInfeasibilitiesSPD::Statistics::Statistics(uint32_t& pivots): d_selectUpdateForSOI("theory::arith::SOI::selectSOI"), d_finalCheckPivotCounter("theory::arith::SOI::lastPivots", pivots) { - StatisticsRegistry::registerStat(&d_initialSignalsTime); - StatisticsRegistry::registerStat(&d_initialConflicts); + smtStatisticsRegistry()->registerStat(&d_initialSignalsTime); + smtStatisticsRegistry()->registerStat(&d_initialConflicts); - StatisticsRegistry::registerStat(&d_soiFoundUnsat); - StatisticsRegistry::registerStat(&d_soiFoundSat); - StatisticsRegistry::registerStat(&d_soiMissed); + smtStatisticsRegistry()->registerStat(&d_soiFoundUnsat); + smtStatisticsRegistry()->registerStat(&d_soiFoundSat); + smtStatisticsRegistry()->registerStat(&d_soiMissed); - StatisticsRegistry::registerStat(&d_soiConflicts); - StatisticsRegistry::registerStat(&d_hasToBeMinimal); - StatisticsRegistry::registerStat(&d_maybeNotMinimal); + smtStatisticsRegistry()->registerStat(&d_soiConflicts); + smtStatisticsRegistry()->registerStat(&d_hasToBeMinimal); + smtStatisticsRegistry()->registerStat(&d_maybeNotMinimal); - StatisticsRegistry::registerStat(&d_soiTimer); - StatisticsRegistry::registerStat(&d_soiFocusConstructionTimer); + smtStatisticsRegistry()->registerStat(&d_soiTimer); + smtStatisticsRegistry()->registerStat(&d_soiFocusConstructionTimer); - StatisticsRegistry::registerStat(&d_soiConflictMinimization); + smtStatisticsRegistry()->registerStat(&d_soiConflictMinimization); - StatisticsRegistry::registerStat(&d_selectUpdateForSOI); + smtStatisticsRegistry()->registerStat(&d_selectUpdateForSOI); - StatisticsRegistry::registerStat(&d_finalCheckPivotCounter); + smtStatisticsRegistry()->registerStat(&d_finalCheckPivotCounter); } SumOfInfeasibilitiesSPD::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_initialSignalsTime); - StatisticsRegistry::unregisterStat(&d_initialConflicts); + smtStatisticsRegistry()->unregisterStat(&d_initialSignalsTime); + smtStatisticsRegistry()->unregisterStat(&d_initialConflicts); - StatisticsRegistry::unregisterStat(&d_soiFoundUnsat); - StatisticsRegistry::unregisterStat(&d_soiFoundSat); - StatisticsRegistry::unregisterStat(&d_soiMissed); + smtStatisticsRegistry()->unregisterStat(&d_soiFoundUnsat); + smtStatisticsRegistry()->unregisterStat(&d_soiFoundSat); + smtStatisticsRegistry()->unregisterStat(&d_soiMissed); - StatisticsRegistry::unregisterStat(&d_soiConflicts); - StatisticsRegistry::unregisterStat(&d_hasToBeMinimal); - StatisticsRegistry::unregisterStat(&d_maybeNotMinimal); + smtStatisticsRegistry()->unregisterStat(&d_soiConflicts); + smtStatisticsRegistry()->unregisterStat(&d_hasToBeMinimal); + smtStatisticsRegistry()->unregisterStat(&d_maybeNotMinimal); - StatisticsRegistry::unregisterStat(&d_soiTimer); - StatisticsRegistry::unregisterStat(&d_soiFocusConstructionTimer); + smtStatisticsRegistry()->unregisterStat(&d_soiTimer); + smtStatisticsRegistry()->unregisterStat(&d_soiFocusConstructionTimer); - StatisticsRegistry::unregisterStat(&d_soiConflictMinimization); + smtStatisticsRegistry()->unregisterStat(&d_soiConflictMinimization); - StatisticsRegistry::unregisterStat(&d_selectUpdateForSOI); - StatisticsRegistry::unregisterStat(&d_finalCheckPivotCounter); + 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 b08d7794b..73a2330a3 100644 --- a/src/theory/arith/soi_simplex.h +++ b/src/theory/arith/soi_simplex.h @@ -54,9 +54,9 @@ #include <stdint.h> -#include "expr/statistics_registry.h" #include "theory/arith/simplex.h" #include "util/dense_map.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { @@ -241,4 +241,3 @@ private: }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ - diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 3c5c1c414..843feed01 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -18,6 +18,7 @@ #include "theory/arith/theory_arith.h" #include "options/smt_options.h" +#include "smt/smt_statistics_registry.h" #include "theory/arith/infer_bounds.h" #include "theory/arith/theory_arith_private.h" @@ -33,9 +34,13 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, const LogicInfo& logicInfo, SmtGlobals* globals) : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, globals) , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo)) -{} + , d_ppRewriteTimer("theory::arith::ppRewriteTimer") +{ + smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer); +} TheoryArith::~TheoryArith(){ + smtStatisticsRegistry()->unregisterStat(&d_ppRewriteTimer); delete d_internal; } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index d26a120ae..c54414109 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -43,7 +43,7 @@ private: TheoryArithPrivate* d_internal; - KEEP_STATISTIC(TimerStat, d_ppRewriteTimer, "theory::arith::ppRewriteTimer"); + TimerStat d_ppRewriteTimer; public: TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index bf1810331..e6b14d2b1 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -33,11 +33,11 @@ #include "expr/metakind.h" #include "expr/node.h" #include "expr/node_builder.h" -#include "expr/statistics_registry.h" #include "options/arith_options.h" #include "options/smt_options.h" // for incrementalSolving() #include "smt/logic_exception.h" #include "smt/logic_request.h" +#include "smt/smt_statistics_registry.h" #include "smt_util/boolean_simplification.h" #include "theory/arith/approx_simplex.h" #include "theory/arith/arith_ite_utils.h" @@ -70,6 +70,7 @@ #include "util/integer.h" #include "util/rational.h" #include "util/result.h" +#include "util/statistics_registry.h" using namespace std; using namespace CVC4::kind; @@ -328,190 +329,190 @@ TheoryArithPrivate::Statistics::Statistics() , d_mipProofsSuccessful("theory::arith::z::mip::proofs::successful", 0) , d_numBranchesFailed("theory::arith::z::mip::branch::proof::failed", 0) { - StatisticsRegistry::registerStat(&d_statAssertUpperConflicts); - StatisticsRegistry::registerStat(&d_statAssertLowerConflicts); - - StatisticsRegistry::registerStat(&d_statUserVariables); - StatisticsRegistry::registerStat(&d_statAuxiliaryVariables); - StatisticsRegistry::registerStat(&d_statDisequalitySplits); - StatisticsRegistry::registerStat(&d_statDisequalityConflicts); - StatisticsRegistry::registerStat(&d_simplifyTimer); - StatisticsRegistry::registerStat(&d_staticLearningTimer); - - StatisticsRegistry::registerStat(&d_presolveTime); - StatisticsRegistry::registerStat(&d_newPropTime); - - StatisticsRegistry::registerStat(&d_externalBranchAndBounds); - - StatisticsRegistry::registerStat(&d_initialTableauSize); - StatisticsRegistry::registerStat(&d_currSetToSmaller); - StatisticsRegistry::registerStat(&d_smallerSetToCurr); - StatisticsRegistry::registerStat(&d_restartTimer); - - StatisticsRegistry::registerStat(&d_boundComputationTime); - StatisticsRegistry::registerStat(&d_boundComputations); - StatisticsRegistry::registerStat(&d_boundPropagations); - - StatisticsRegistry::registerStat(&d_unknownChecks); - StatisticsRegistry::registerStat(&d_maxUnknownsInARow); - StatisticsRegistry::registerStat(&d_avgUnknownsInARow); - StatisticsRegistry::registerStat(&d_revertsOnConflicts); - StatisticsRegistry::registerStat(&d_commitsOnConflicts); - StatisticsRegistry::registerStat(&d_nontrivialSatChecks); - - - StatisticsRegistry::registerStat(&d_satPivots); - StatisticsRegistry::registerStat(&d_unsatPivots); - StatisticsRegistry::registerStat(&d_unknownPivots); - - StatisticsRegistry::registerStat(&d_replayLogRecCount); - StatisticsRegistry::registerStat(&d_replayLogRecConflictEscalation); - StatisticsRegistry::registerStat(&d_replayLogRecEarlyExit); - StatisticsRegistry::registerStat(&d_replayBranchCloseFailures); - StatisticsRegistry::registerStat(&d_replayLeafCloseFailures); - StatisticsRegistry::registerStat(&d_replayBranchSkips); - StatisticsRegistry::registerStat(&d_mirCutsAttempted); - StatisticsRegistry::registerStat(&d_gmiCutsAttempted); - StatisticsRegistry::registerStat(&d_branchCutsAttempted); - StatisticsRegistry::registerStat(&d_cutsReconstructed); - StatisticsRegistry::registerStat(&d_cutsProven); - StatisticsRegistry::registerStat(&d_cutsProofFailed); - StatisticsRegistry::registerStat(&d_cutsReconstructionFailed); - StatisticsRegistry::registerStat(&d_mipReplayLemmaCalls); - StatisticsRegistry::registerStat(&d_mipExternalCuts); - StatisticsRegistry::registerStat(&d_mipExternalBranch); - - StatisticsRegistry::registerStat(&d_inSolveInteger); - StatisticsRegistry::registerStat(&d_branchesExhausted); - StatisticsRegistry::registerStat(&d_execExhausted); - StatisticsRegistry::registerStat(&d_pivotsExhausted); - StatisticsRegistry::registerStat(&d_panicBranches); - StatisticsRegistry::registerStat(&d_relaxCalls); - StatisticsRegistry::registerStat(&d_relaxLinFeas); - StatisticsRegistry::registerStat(&d_relaxLinFeasFailures); - StatisticsRegistry::registerStat(&d_relaxLinInfeas); - StatisticsRegistry::registerStat(&d_relaxLinInfeasFailures); - StatisticsRegistry::registerStat(&d_relaxLinExhausted); - StatisticsRegistry::registerStat(&d_relaxOthers); - - StatisticsRegistry::registerStat(&d_applyRowsDeleted); - - StatisticsRegistry::registerStat(&d_replaySimplexTimer); - StatisticsRegistry::registerStat(&d_replayLogTimer); - StatisticsRegistry::registerStat(&d_solveIntTimer); - StatisticsRegistry::registerStat(&d_solveRealRelaxTimer); - - StatisticsRegistry::registerStat(&d_solveIntCalls); - StatisticsRegistry::registerStat(&d_solveStandardEffort); - - StatisticsRegistry::registerStat(&d_approxDisabled); - - StatisticsRegistry::registerStat(&d_replayAttemptFailed); - - StatisticsRegistry::registerStat(&d_cutsRejectedDuringReplay); - StatisticsRegistry::registerStat(&d_cutsRejectedDuringLemmas); - - StatisticsRegistry::registerStat(&d_solveIntModelsAttempts); - StatisticsRegistry::registerStat(&d_solveIntModelsSuccessful); - StatisticsRegistry::registerStat(&d_mipTimer); - StatisticsRegistry::registerStat(&d_lpTimer); - StatisticsRegistry::registerStat(&d_mipProofsAttempted); - StatisticsRegistry::registerStat(&d_mipProofsSuccessful); - StatisticsRegistry::registerStat(&d_numBranchesFailed); + 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(){ - StatisticsRegistry::unregisterStat(&d_statAssertUpperConflicts); - StatisticsRegistry::unregisterStat(&d_statAssertLowerConflicts); - - StatisticsRegistry::unregisterStat(&d_statUserVariables); - StatisticsRegistry::unregisterStat(&d_statAuxiliaryVariables); - StatisticsRegistry::unregisterStat(&d_statDisequalitySplits); - StatisticsRegistry::unregisterStat(&d_statDisequalityConflicts); - StatisticsRegistry::unregisterStat(&d_simplifyTimer); - StatisticsRegistry::unregisterStat(&d_staticLearningTimer); - - StatisticsRegistry::unregisterStat(&d_presolveTime); - StatisticsRegistry::unregisterStat(&d_newPropTime); - - StatisticsRegistry::unregisterStat(&d_externalBranchAndBounds); - - StatisticsRegistry::unregisterStat(&d_initialTableauSize); - StatisticsRegistry::unregisterStat(&d_currSetToSmaller); - StatisticsRegistry::unregisterStat(&d_smallerSetToCurr); - StatisticsRegistry::unregisterStat(&d_restartTimer); - - StatisticsRegistry::unregisterStat(&d_boundComputationTime); - StatisticsRegistry::unregisterStat(&d_boundComputations); - StatisticsRegistry::unregisterStat(&d_boundPropagations); - - StatisticsRegistry::unregisterStat(&d_unknownChecks); - StatisticsRegistry::unregisterStat(&d_maxUnknownsInARow); - StatisticsRegistry::unregisterStat(&d_avgUnknownsInARow); - StatisticsRegistry::unregisterStat(&d_revertsOnConflicts); - StatisticsRegistry::unregisterStat(&d_commitsOnConflicts); - StatisticsRegistry::unregisterStat(&d_nontrivialSatChecks); - - StatisticsRegistry::unregisterStat(&d_satPivots); - StatisticsRegistry::unregisterStat(&d_unsatPivots); - StatisticsRegistry::unregisterStat(&d_unknownPivots); - - StatisticsRegistry::unregisterStat(&d_replayLogRecCount); - StatisticsRegistry::unregisterStat(&d_replayLogRecConflictEscalation); - StatisticsRegistry::unregisterStat(&d_replayLogRecEarlyExit); - StatisticsRegistry::unregisterStat(&d_replayBranchCloseFailures); - StatisticsRegistry::unregisterStat(&d_replayLeafCloseFailures); - StatisticsRegistry::unregisterStat(&d_replayBranchSkips); - StatisticsRegistry::unregisterStat(&d_mirCutsAttempted); - StatisticsRegistry::unregisterStat(&d_gmiCutsAttempted); - StatisticsRegistry::unregisterStat(&d_branchCutsAttempted); - StatisticsRegistry::unregisterStat(&d_cutsReconstructed); - StatisticsRegistry::unregisterStat(&d_cutsProven); - StatisticsRegistry::unregisterStat(&d_cutsProofFailed); - StatisticsRegistry::unregisterStat(&d_cutsReconstructionFailed); - StatisticsRegistry::unregisterStat(&d_mipReplayLemmaCalls); - StatisticsRegistry::unregisterStat(&d_mipExternalCuts); - StatisticsRegistry::unregisterStat(&d_mipExternalBranch); - - - StatisticsRegistry::unregisterStat(&d_inSolveInteger); - StatisticsRegistry::unregisterStat(&d_branchesExhausted); - StatisticsRegistry::unregisterStat(&d_execExhausted); - StatisticsRegistry::unregisterStat(&d_pivotsExhausted); - StatisticsRegistry::unregisterStat(&d_panicBranches); - StatisticsRegistry::unregisterStat(&d_relaxCalls); - StatisticsRegistry::unregisterStat(&d_relaxLinFeas); - StatisticsRegistry::unregisterStat(&d_relaxLinFeasFailures); - StatisticsRegistry::unregisterStat(&d_relaxLinInfeas); - StatisticsRegistry::unregisterStat(&d_relaxLinInfeasFailures); - StatisticsRegistry::unregisterStat(&d_relaxLinExhausted); - StatisticsRegistry::unregisterStat(&d_relaxOthers); - - StatisticsRegistry::unregisterStat(&d_applyRowsDeleted); - - StatisticsRegistry::unregisterStat(&d_replaySimplexTimer); - StatisticsRegistry::unregisterStat(&d_replayLogTimer); - StatisticsRegistry::unregisterStat(&d_solveIntTimer); - StatisticsRegistry::unregisterStat(&d_solveRealRelaxTimer); - - StatisticsRegistry::unregisterStat(&d_solveIntCalls); - StatisticsRegistry::unregisterStat(&d_solveStandardEffort); - - StatisticsRegistry::unregisterStat(&d_approxDisabled); - - StatisticsRegistry::unregisterStat(&d_replayAttemptFailed); - - StatisticsRegistry::unregisterStat(&d_cutsRejectedDuringReplay); - StatisticsRegistry::unregisterStat(&d_cutsRejectedDuringLemmas); - - - StatisticsRegistry::unregisterStat(&d_solveIntModelsAttempts); - StatisticsRegistry::unregisterStat(&d_solveIntModelsSuccessful); - StatisticsRegistry::unregisterStat(&d_mipTimer); - StatisticsRegistry::unregisterStat(&d_lpTimer); - StatisticsRegistry::unregisterStat(&d_mipProofsAttempted); - StatisticsRegistry::unregisterStat(&d_mipProofsSuccessful); - StatisticsRegistry::unregisterStat(&d_numBranchesFailed); + 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){ diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 32c12eba7..1009dceb8 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -31,7 +31,6 @@ #include "expr/metakind.h" #include "expr/node.h" #include "expr/node_builder.h" -#include "expr/statistics_registry.h" #include "options/arith_options.h" #include "smt/logic_exception.h" #include "smt_util/boolean_simplification.h" @@ -67,6 +66,7 @@ #include "util/integer.h" #include "util/rational.h" #include "util/result.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { |