diff options
Diffstat (limited to 'src/theory')
78 files changed, 899 insertions, 834 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 { diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp index cd0025fe2..e94abe9cb 100644 --- a/src/theory/arrays/array_info.cpp +++ b/src/theory/arrays/array_info.cpp @@ -17,10 +17,53 @@ #include "theory/arrays/array_info.h" +#include "smt/smt_statistics_registry.h" + namespace CVC4 { namespace theory { namespace arrays { +ArrayInfo::ArrayInfo(context::Context* c, Backtracker<TNode>* b) + : ct(c), bck(b), info_map(), + d_mergeInfoTimer("theory::arrays::mergeInfoTimer"), + d_avgIndexListLength("theory::arrays::avgIndexListLength"), + d_avgStoresListLength("theory::arrays::avgStoresListLength"), + d_avgInStoresListLength("theory::arrays::avgInStoresListLength"), + d_listsCount("theory::arrays::listsCount",0), + d_callsMergeInfo("theory::arrays::callsMergeInfo",0), + d_maxList("theory::arrays::maxList",0), + d_tableSize("theory::arrays::infoTableSize", info_map) { + emptyList = new(true) CTNodeList(ct); + emptyInfo = new Info(ct, bck); + smtStatisticsRegistry()->registerStat(&d_mergeInfoTimer); + smtStatisticsRegistry()->registerStat(&d_avgIndexListLength); + smtStatisticsRegistry()->registerStat(&d_avgStoresListLength); + smtStatisticsRegistry()->registerStat(&d_avgInStoresListLength); + smtStatisticsRegistry()->registerStat(&d_listsCount); + smtStatisticsRegistry()->registerStat(&d_callsMergeInfo); + smtStatisticsRegistry()->registerStat(&d_maxList); + smtStatisticsRegistry()->registerStat(&d_tableSize); +} + +ArrayInfo::~ArrayInfo() { + CNodeInfoMap::iterator it = info_map.begin(); + for( ; it != info_map.end(); it++ ) { + if((*it).second!= emptyInfo) { + delete (*it).second; + } + } + emptyList->deleteSelf(); + delete emptyInfo; + smtStatisticsRegistry()->unregisterStat(&d_mergeInfoTimer); + smtStatisticsRegistry()->unregisterStat(&d_avgIndexListLength); + smtStatisticsRegistry()->unregisterStat(&d_avgStoresListLength); + smtStatisticsRegistry()->unregisterStat(&d_avgInStoresListLength); + smtStatisticsRegistry()->unregisterStat(&d_listsCount); + smtStatisticsRegistry()->unregisterStat(&d_callsMergeInfo); + smtStatisticsRegistry()->unregisterStat(&d_maxList); + smtStatisticsRegistry()->unregisterStat(&d_tableSize); +} + bool inList(const CTNodeList* l, const TNode el) { CTNodeList::const_iterator it = l->begin(); for ( ; it!= l->end(); it ++) { diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index f14788ed5..3e479e0f9 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -27,8 +27,8 @@ #include "context/cdlist.h" #include "context/cdhashmap.h" #include "expr/node.h" -#include "expr/statistics_registry.h" #include "util/ntuple.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { @@ -163,54 +163,18 @@ public: d_callsMergeInfo("theory::arrays::callsMergeInfo",0), d_maxList("theory::arrays::maxList",0), d_tableSize("theory::arrays::infoTableSize", info_map) { - StatisticsRegistry::registerStat(&d_mergeInfoTimer); - StatisticsRegistry::registerStat(&d_avgIndexListLength); - StatisticsRegistry::registerStat(&d_avgStoresListLength); - StatisticsRegistry::registerStat(&d_avgInStoresListLength); - StatisticsRegistry::registerStat(&d_listsCount); - StatisticsRegistry::registerStat(&d_callsMergeInfo); - StatisticsRegistry::registerStat(&d_maxList); - StatisticsRegistry::registerStat(&d_tableSize); + currentStatisticsRegistry()->registerStat(&d_mergeInfoTimer); + currentStatisticsRegistry()->registerStat(&d_avgIndexListLength); + currentStatisticsRegistry()->registerStat(&d_avgStoresListLength); + currentStatisticsRegistry()->registerStat(&d_avgInStoresListLength); + currentStatisticsRegistry()->registerStat(&d_listsCount); + currentStatisticsRegistry()->registerStat(&d_callsMergeInfo); + currentStatisticsRegistry()->registerStat(&d_maxList); + currentStatisticsRegistry()->registerStat(&d_tableSize); }*/ - ArrayInfo(context::Context* c, Backtracker<TNode>* b): ct(c), bck(b), info_map(), - d_mergeInfoTimer("theory::arrays::mergeInfoTimer"), - d_avgIndexListLength("theory::arrays::avgIndexListLength"), - d_avgStoresListLength("theory::arrays::avgStoresListLength"), - d_avgInStoresListLength("theory::arrays::avgInStoresListLength"), - d_listsCount("theory::arrays::listsCount",0), - d_callsMergeInfo("theory::arrays::callsMergeInfo",0), - d_maxList("theory::arrays::maxList",0), - d_tableSize("theory::arrays::infoTableSize", info_map) { - emptyList = new(true) CTNodeList(ct); - emptyInfo = new Info(ct, bck); - StatisticsRegistry::registerStat(&d_mergeInfoTimer); - StatisticsRegistry::registerStat(&d_avgIndexListLength); - StatisticsRegistry::registerStat(&d_avgStoresListLength); - StatisticsRegistry::registerStat(&d_avgInStoresListLength); - StatisticsRegistry::registerStat(&d_listsCount); - StatisticsRegistry::registerStat(&d_callsMergeInfo); - StatisticsRegistry::registerStat(&d_maxList); - StatisticsRegistry::registerStat(&d_tableSize); - } + ArrayInfo(context::Context* c, Backtracker<TNode>* b); - ~ArrayInfo() { - CNodeInfoMap::iterator it = info_map.begin(); - for( ; it != info_map.end(); it++ ) { - if((*it).second!= emptyInfo) { - delete (*it).second; - } - } - emptyList->deleteSelf(); - delete emptyInfo; - StatisticsRegistry::unregisterStat(&d_mergeInfoTimer); - StatisticsRegistry::unregisterStat(&d_avgIndexListLength); - StatisticsRegistry::unregisterStat(&d_avgStoresListLength); - StatisticsRegistry::unregisterStat(&d_avgInStoresListLength); - StatisticsRegistry::unregisterStat(&d_listsCount); - StatisticsRegistry::unregisterStat(&d_callsMergeInfo); - StatisticsRegistry::unregisterStat(&d_maxList); - StatisticsRegistry::unregisterStat(&d_tableSize); - }; + ~ArrayInfo(); /** * adds the node a to the map if it does not exist diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index ab57eb260..508a4b323 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -22,6 +22,7 @@ #include "options/arrays_options.h" #include "options/smt_options.h" #include "smt/logic_exception.h" +#include "smt/smt_statistics_registry.h" #include "smt_util/command.h" #include "theory/rewriter.h" #include "theory/theory_model.h" @@ -98,16 +99,16 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, d_arrayMerges(c), d_inCheckModel(false) { - StatisticsRegistry::registerStat(&d_numRow); - StatisticsRegistry::registerStat(&d_numExt); - StatisticsRegistry::registerStat(&d_numProp); - StatisticsRegistry::registerStat(&d_numExplain); - StatisticsRegistry::registerStat(&d_numNonLinear); - StatisticsRegistry::registerStat(&d_numSharedArrayVarSplits); - StatisticsRegistry::registerStat(&d_numGetModelValSplits); - StatisticsRegistry::registerStat(&d_numGetModelValConflicts); - StatisticsRegistry::registerStat(&d_numSetModelValSplits); - StatisticsRegistry::registerStat(&d_numSetModelValConflicts); + smtStatisticsRegistry()->registerStat(&d_numRow); + smtStatisticsRegistry()->registerStat(&d_numExt); + smtStatisticsRegistry()->registerStat(&d_numProp); + smtStatisticsRegistry()->registerStat(&d_numExplain); + smtStatisticsRegistry()->registerStat(&d_numNonLinear); + smtStatisticsRegistry()->registerStat(&d_numSharedArrayVarSplits); + smtStatisticsRegistry()->registerStat(&d_numGetModelValSplits); + smtStatisticsRegistry()->registerStat(&d_numGetModelValConflicts); + smtStatisticsRegistry()->registerStat(&d_numSetModelValSplits); + smtStatisticsRegistry()->registerStat(&d_numSetModelValConflicts); d_true = NodeManager::currentNM()->mkConst<bool>(true); d_false = NodeManager::currentNM()->mkConst<bool>(false); @@ -137,16 +138,16 @@ TheoryArrays::~TheoryArrays() { it2->second->deleteSelf(); } delete d_constReadsContext; - StatisticsRegistry::unregisterStat(&d_numRow); - StatisticsRegistry::unregisterStat(&d_numExt); - StatisticsRegistry::unregisterStat(&d_numProp); - StatisticsRegistry::unregisterStat(&d_numExplain); - StatisticsRegistry::unregisterStat(&d_numNonLinear); - StatisticsRegistry::unregisterStat(&d_numSharedArrayVarSplits); - StatisticsRegistry::unregisterStat(&d_numGetModelValSplits); - StatisticsRegistry::unregisterStat(&d_numGetModelValConflicts); - StatisticsRegistry::unregisterStat(&d_numSetModelValSplits); - StatisticsRegistry::unregisterStat(&d_numSetModelValConflicts); + smtStatisticsRegistry()->unregisterStat(&d_numRow); + smtStatisticsRegistry()->unregisterStat(&d_numExt); + smtStatisticsRegistry()->unregisterStat(&d_numProp); + smtStatisticsRegistry()->unregisterStat(&d_numExplain); + smtStatisticsRegistry()->unregisterStat(&d_numNonLinear); + smtStatisticsRegistry()->unregisterStat(&d_numSharedArrayVarSplits); + smtStatisticsRegistry()->unregisterStat(&d_numGetModelValSplits); + smtStatisticsRegistry()->unregisterStat(&d_numGetModelValConflicts); + smtStatisticsRegistry()->unregisterStat(&d_numSetModelValSplits); + smtStatisticsRegistry()->unregisterStat(&d_numSetModelValConflicts); } void TheoryArrays::setMasterEqualityEngine(eq::EqualityEngine* eq) { diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 98cba0420..f1b02d99e 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -22,10 +22,10 @@ #include "context/cdhashmap.h" #include "context/cdhashset.h" #include "context/cdqueue.h" -#include "expr/statistics_registry.h" #include "theory/arrays/array_info.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp index f05520306..842ff60b1 100644 --- a/src/theory/bv/abstraction.cpp +++ b/src/theory/bv/abstraction.cpp @@ -16,6 +16,7 @@ #include "options/bv_options.h" #include "smt_util/dump.h" +#include "smt/smt_statistics_registry.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" @@ -1047,13 +1048,13 @@ AbstractionModule::Statistics::Statistics() , d_numArgsSkolemized("theory::bv::AbstractioModule::NumArgsSkolemized", 0) , d_abstractionTime("theory::bv::AbstractioModule::AbstractionTime") { - StatisticsRegistry::registerStat(&d_numFunctionsAbstracted); - StatisticsRegistry::registerStat(&d_numArgsSkolemized); - StatisticsRegistry::registerStat(&d_abstractionTime); + smtStatisticsRegistry()->registerStat(&d_numFunctionsAbstracted); + smtStatisticsRegistry()->registerStat(&d_numArgsSkolemized); + smtStatisticsRegistry()->registerStat(&d_abstractionTime); } AbstractionModule::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_numFunctionsAbstracted); - StatisticsRegistry::unregisterStat(&d_numArgsSkolemized); - StatisticsRegistry::unregisterStat(&d_abstractionTime); + smtStatisticsRegistry()->unregisterStat(&d_numFunctionsAbstracted); + smtStatisticsRegistry()->unregisterStat(&d_numArgsSkolemized); + smtStatisticsRegistry()->unregisterStat(&d_abstractionTime); } diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h index 6b4d5a7dc..cba170d76 100644 --- a/src/theory/bv/abstraction.h +++ b/src/theory/bv/abstraction.h @@ -23,8 +23,8 @@ #include <ext/hash_set> #include "expr/node.h" -#include "expr/statistics_registry.h" #include "theory/substitutions.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp index f07bd49f7..d84493daf 100644 --- a/src/theory/bv/aig_bitblaster.cpp +++ b/src/theory/bv/aig_bitblaster.cpp @@ -455,19 +455,19 @@ AigBitblaster::Statistics::Statistics() , d_cnfConversionTime("theory::bv::AigBitblaster::cnfConversionTime") , d_solveTime("theory::bv::AigBitblaster::solveTime") { - StatisticsRegistry::registerStat(&d_numClauses); - StatisticsRegistry::registerStat(&d_numVariables); - StatisticsRegistry::registerStat(&d_simplificationTime); - StatisticsRegistry::registerStat(&d_cnfConversionTime); - StatisticsRegistry::registerStat(&d_solveTime); + smtStatisticsRegistry()->registerStat(&d_numClauses); + smtStatisticsRegistry()->registerStat(&d_numVariables); + smtStatisticsRegistry()->registerStat(&d_simplificationTime); + smtStatisticsRegistry()->registerStat(&d_cnfConversionTime); + smtStatisticsRegistry()->registerStat(&d_solveTime); } AigBitblaster::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_numClauses); - StatisticsRegistry::unregisterStat(&d_numVariables); - StatisticsRegistry::unregisterStat(&d_simplificationTime); - StatisticsRegistry::unregisterStat(&d_cnfConversionTime); - StatisticsRegistry::unregisterStat(&d_solveTime); + smtStatisticsRegistry()->unregisterStat(&d_numClauses); + smtStatisticsRegistry()->unregisterStat(&d_numVariables); + smtStatisticsRegistry()->unregisterStat(&d_simplificationTime); + smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime); + smtStatisticsRegistry()->unregisterStat(&d_solveTime); } #else // CVC4_USE_ABC diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp index 6231b8e46..40ac3d560 100644 --- a/src/theory/bv/bv_quick_check.cpp +++ b/src/theory/bv/bv_quick_check.cpp @@ -15,9 +15,10 @@ **/ #include "theory/bv/bv_quick_check.h" -#include "theory/bv/theory_bv_utils.h" +#include "smt/smt_statistics_registry.h" #include "theory/bv/bitblaster_template.h" +#include "theory/bv/theory_bv_utils.h" using namespace CVC4; using namespace CVC4::theory; @@ -357,22 +358,21 @@ QuickXPlain::Statistics::Statistics(const std::string& name) , d_finalPeriod("theory::bv::"+name+"::QuickXplain::FinalPeriod", 0) , d_avgMinimizationRatio("theory::bv::"+name+"::QuickXplain::AvgMinRatio") { - StatisticsRegistry::registerStat(&d_xplainTime); - StatisticsRegistry::registerStat(&d_numSolved); - StatisticsRegistry::registerStat(&d_numUnknown); - StatisticsRegistry::registerStat(&d_numUnknownWasUnsat); - StatisticsRegistry::registerStat(&d_numConflictsMinimized); - StatisticsRegistry::registerStat(&d_finalPeriod); - StatisticsRegistry::registerStat(&d_avgMinimizationRatio); + smtStatisticsRegistry()->registerStat(&d_xplainTime); + smtStatisticsRegistry()->registerStat(&d_numSolved); + smtStatisticsRegistry()->registerStat(&d_numUnknown); + smtStatisticsRegistry()->registerStat(&d_numUnknownWasUnsat); + smtStatisticsRegistry()->registerStat(&d_numConflictsMinimized); + smtStatisticsRegistry()->registerStat(&d_finalPeriod); + smtStatisticsRegistry()->registerStat(&d_avgMinimizationRatio); } QuickXPlain::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_xplainTime); - StatisticsRegistry::unregisterStat(&d_numSolved); - StatisticsRegistry::unregisterStat(&d_numUnknown); - StatisticsRegistry::unregisterStat(&d_numUnknownWasUnsat); - StatisticsRegistry::unregisterStat(&d_numConflictsMinimized); - StatisticsRegistry::unregisterStat(&d_finalPeriod); - StatisticsRegistry::unregisterStat(&d_avgMinimizationRatio); + smtStatisticsRegistry()->unregisterStat(&d_xplainTime); + smtStatisticsRegistry()->unregisterStat(&d_numSolved); + smtStatisticsRegistry()->unregisterStat(&d_numUnknown); + smtStatisticsRegistry()->unregisterStat(&d_numUnknownWasUnsat); + smtStatisticsRegistry()->unregisterStat(&d_numConflictsMinimized); + smtStatisticsRegistry()->unregisterStat(&d_finalPeriod); + smtStatisticsRegistry()->unregisterStat(&d_avgMinimizationRatio); } - diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h index 8ef49f786..8d2a62287 100644 --- a/src/theory/bv/bv_quick_check.h +++ b/src/theory/bv/bv_quick_check.h @@ -24,9 +24,9 @@ #include "context/cdo.h" #include "expr/node.h" -#include "expr/statistics_registry.h" #include "prop/sat_solver_types.h" #include "theory/bv/theory_bv_utils.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index 4531be040..fc9d67cb4 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -13,11 +13,12 @@ ** ** Algebraic solver. **/ +#include "theory/bv/bv_subtheory_algebraic.h" #include "options/bv_options.h" #include "smt_util/boolean_simplification.h" +#include "smt/smt_statistics_registry.h" #include "theory/bv/bv_quick_check.h" -#include "theory/bv/bv_subtheory_algebraic.h" #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory_model.h" @@ -734,25 +735,25 @@ AlgebraicSolver::Statistics::Statistics() , d_solveTime("theory::bv::AlgebraicSolver::SolveTime") , d_useHeuristic("theory::bv::AlgebraicSolver::UseHeuristic", 0.2) { - StatisticsRegistry::registerStat(&d_numCallstoCheck); - StatisticsRegistry::registerStat(&d_numSimplifiesToTrue); - StatisticsRegistry::registerStat(&d_numSimplifiesToFalse); - StatisticsRegistry::registerStat(&d_numUnsat); - StatisticsRegistry::registerStat(&d_numSat); - StatisticsRegistry::registerStat(&d_numUnknown); - StatisticsRegistry::registerStat(&d_solveTime); - StatisticsRegistry::registerStat(&d_useHeuristic); + smtStatisticsRegistry()->registerStat(&d_numCallstoCheck); + smtStatisticsRegistry()->registerStat(&d_numSimplifiesToTrue); + smtStatisticsRegistry()->registerStat(&d_numSimplifiesToFalse); + smtStatisticsRegistry()->registerStat(&d_numUnsat); + smtStatisticsRegistry()->registerStat(&d_numSat); + smtStatisticsRegistry()->registerStat(&d_numUnknown); + smtStatisticsRegistry()->registerStat(&d_solveTime); + smtStatisticsRegistry()->registerStat(&d_useHeuristic); } AlgebraicSolver::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_numCallstoCheck); - StatisticsRegistry::unregisterStat(&d_numSimplifiesToTrue); - StatisticsRegistry::unregisterStat(&d_numSimplifiesToFalse); - StatisticsRegistry::unregisterStat(&d_numUnsat); - StatisticsRegistry::unregisterStat(&d_numSat); - StatisticsRegistry::unregisterStat(&d_numUnknown); - StatisticsRegistry::unregisterStat(&d_solveTime); - StatisticsRegistry::unregisterStat(&d_useHeuristic); + smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck); + smtStatisticsRegistry()->unregisterStat(&d_numSimplifiesToTrue); + smtStatisticsRegistry()->unregisterStat(&d_numSimplifiesToFalse); + smtStatisticsRegistry()->unregisterStat(&d_numUnsat); + smtStatisticsRegistry()->unregisterStat(&d_numSat); + smtStatisticsRegistry()->unregisterStat(&d_numUnknown); + smtStatisticsRegistry()->unregisterStat(&d_solveTime); + smtStatisticsRegistry()->unregisterStat(&d_useHeuristic); } bool hasExpensiveBVOperatorsRec(TNode fact, TNodeSet& seen) { diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index 1d0342c08..9f8cb580c 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -17,6 +17,7 @@ #include "decision/decision_attributes.h" #include "options/decision_options.h" #include "options/bv_options.h" +#include "smt/smt_statistics_registry.h" #include "theory/bv/abstraction.h" #include "theory/bv/bitblaster_template.h" #include "theory/bv/bv_quick_check.h" @@ -55,12 +56,12 @@ BitblastSolver::Statistics::Statistics() : d_numCallstoCheck("theory::bv::BitblastSolver::NumCallsToCheck", 0) , d_numBBLemmas("theory::bv::BitblastSolver::NumTimesLemmasBB", 0) { - StatisticsRegistry::registerStat(&d_numCallstoCheck); - StatisticsRegistry::registerStat(&d_numBBLemmas); + smtStatisticsRegistry()->registerStat(&d_numCallstoCheck); + smtStatisticsRegistry()->registerStat(&d_numBBLemmas); } BitblastSolver::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_numCallstoCheck); - StatisticsRegistry::unregisterStat(&d_numBBLemmas); + smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck); + smtStatisticsRegistry()->unregisterStat(&d_numBBLemmas); } void BitblastSolver::setAbstraction(AbstractionModule* abs) { diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index ef4d24e82..ec257468e 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -18,6 +18,7 @@ #include "options/bv_options.h" #include "options/smt_options.h" +#include "smt/smt_statistics_registry.h" #include "theory/bv/slicer.h" #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" @@ -438,10 +439,10 @@ CoreSolver::Statistics::Statistics() : d_numCallstoCheck("theory::bv::CoreSolver::NumCallsToCheck", 0) , d_slicerEnabled("theory::bv::CoreSolver::SlicerEnabled", false) { - StatisticsRegistry::registerStat(&d_numCallstoCheck); - StatisticsRegistry::registerStat(&d_slicerEnabled); + smtStatisticsRegistry()->registerStat(&d_numCallstoCheck); + smtStatisticsRegistry()->registerStat(&d_slicerEnabled); } CoreSolver::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_numCallstoCheck); - StatisticsRegistry::unregisterStat(&d_slicerEnabled); + smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck); + smtStatisticsRegistry()->unregisterStat(&d_slicerEnabled); } diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index 054e43b7c..7916d941e 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -17,6 +17,7 @@ #include "theory/bv/bv_subtheory_inequality.h" #include "options/smt_options.h" +#include "smt/smt_statistics_registry.h" #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory_model.h" @@ -228,8 +229,8 @@ bool InequalitySolver::addInequality(TNode a, TNode b, bool strict, TNode fact) InequalitySolver::Statistics::Statistics() : d_numCallstoCheck("theory::bv::InequalitySolver::NumCallsToCheck", 0) { - StatisticsRegistry::registerStat(&d_numCallstoCheck); + smtStatisticsRegistry()->registerStat(&d_numCallstoCheck); } InequalitySolver::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_numCallstoCheck); + smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck); } diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp index 00e6f9ff8..66ad4fec0 100644 --- a/src/theory/bv/bv_to_bool.cpp +++ b/src/theory/bv/bv_to_bool.cpp @@ -11,11 +11,12 @@ ** ** \brief Preprocessing pass that lifts bit-vectors of size 1 to booleans. ** - ** Preprocessing pass that lifts bit-vectors of size 1 to booleans. + ** Preprocessing pass that lifts bit-vectors of size 1 to booleans. **/ #include "theory/bv/bv_to_bool.h" #include "smt_util/node_visitor.h" +#include "smt/smt_statistics_registry.h" using namespace std; using namespace CVC4; @@ -31,7 +32,7 @@ BvToBoolPreprocessor::BvToBoolPreprocessor() {} void BvToBoolPreprocessor::addToLiftCache(TNode term, Node new_term) { - Assert (new_term != Node()); + Assert (new_term != Node()); Assert (!hasLiftCache(term)); Assert (term.getType() == new_term.getType()); d_liftCache[term] = new_term; @@ -239,13 +240,13 @@ BvToBoolPreprocessor::Statistics::Statistics() , d_numAtomsLifted("theory::bv::BvToBoolPreprocess::NumberOfAtomsLifted", 0) , d_numTermsForcedLifted("theory::bv::BvToBoolPreprocess::NumberOfTermsForcedLifted", 0) { - StatisticsRegistry::registerStat(&d_numTermsLifted); - StatisticsRegistry::registerStat(&d_numAtomsLifted); - StatisticsRegistry::registerStat(&d_numTermsForcedLifted); + smtStatisticsRegistry()->registerStat(&d_numTermsLifted); + smtStatisticsRegistry()->registerStat(&d_numAtomsLifted); + smtStatisticsRegistry()->registerStat(&d_numTermsForcedLifted); } BvToBoolPreprocessor::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_numTermsLifted); - StatisticsRegistry::unregisterStat(&d_numAtomsLifted); - StatisticsRegistry::unregisterStat(&d_numTermsForcedLifted); + smtStatisticsRegistry()->unregisterStat(&d_numTermsLifted); + smtStatisticsRegistry()->unregisterStat(&d_numAtomsLifted); + smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLifted); } diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h index 46b2d5c6e..e6c126440 100644 --- a/src/theory/bv/bv_to_bool.h +++ b/src/theory/bv/bv_to_bool.h @@ -11,7 +11,7 @@ ** ** \brief Preprocessing pass that lifts bit-vectors of size 1 to booleans. ** - ** Preprocessing pass that lifts bit-vectors of size 1 to booleans. + ** Preprocessing pass that lifts bit-vectors of size 1 to booleans. **/ #include "cvc4_private.h" @@ -19,14 +19,14 @@ #ifndef __CVC4__THEORY__BV__BV_TO_BOOL_H #define __CVC4__THEORY__BV__BV_TO_BOOL_H -#include "expr/statistics_registry.h" #include "theory/bv/theory_bv_utils.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { namespace bv { -typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap; +typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap; class BvToBoolPreprocessor { diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp index 39606ca7c..000abe62b 100644 --- a/src/theory/bv/eager_bitblaster.cpp +++ b/src/theory/bv/eager_bitblaster.cpp @@ -19,6 +19,7 @@ #include "options/bv_options.h" #include "prop/cnf_stream.h" #include "prop/sat_solver_factory.h" +#include "smt/smt_statistics_registry.h" #include "theory/bv/bitblaster_template.h" #include "theory/bv/theory_bv.h" #include "theory/theory_model.h" @@ -45,7 +46,8 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv) d_bitblastingRegistrar = new BitblastingRegistrar(this); d_nullContext = new context::Context(); - d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, "EagerBitblaster"); + d_satSolver = prop::SatSolverFactory::createMinisat( + d_nullContext, smtStatisticsRegistry(), "EagerBitblaster"); d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar, d_nullContext, d_bv->globals()); diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp index b8173cb8b..34a9418dd 100644 --- a/src/theory/bv/lazy_bitblaster.cpp +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -20,6 +20,7 @@ #include "prop/cnf_stream.h" #include "prop/sat_solver.h" #include "prop/sat_solver_factory.h" +#include "smt/smt_statistics_registry.h" #include "theory/bv/abstraction.h" #include "theory/bv/theory_bv.h" #include "theory/rewriter.h" @@ -46,7 +47,8 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, , d_name(name) , d_statistics(name) { - d_satSolver = prop::SatSolverFactory::createMinisat(c, name); + d_satSolver = prop::SatSolverFactory::createMinisat( + c, smtStatisticsRegistry(), name); d_nullRegistrar = new prop::NullRegistrar(); d_nullContext = new context::Context(); d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar, @@ -307,24 +309,24 @@ TLazyBitblaster::Statistics::Statistics(const std::string& prefix) : d_numBitblastingPropagations("theory::bv::"+prefix+"::NumberOfBitblastingPropagations", 0), d_bitblastTimer("theory::bv::"+prefix+"::BitblastTimer") { - StatisticsRegistry::registerStat(&d_numTermClauses); - StatisticsRegistry::registerStat(&d_numAtomClauses); - StatisticsRegistry::registerStat(&d_numTerms); - StatisticsRegistry::registerStat(&d_numAtoms); - StatisticsRegistry::registerStat(&d_numExplainedPropagations); - StatisticsRegistry::registerStat(&d_numBitblastingPropagations); - StatisticsRegistry::registerStat(&d_bitblastTimer); + smtStatisticsRegistry()->registerStat(&d_numTermClauses); + smtStatisticsRegistry()->registerStat(&d_numAtomClauses); + smtStatisticsRegistry()->registerStat(&d_numTerms); + smtStatisticsRegistry()->registerStat(&d_numAtoms); + smtStatisticsRegistry()->registerStat(&d_numExplainedPropagations); + smtStatisticsRegistry()->registerStat(&d_numBitblastingPropagations); + smtStatisticsRegistry()->registerStat(&d_bitblastTimer); } TLazyBitblaster::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_numTermClauses); - StatisticsRegistry::unregisterStat(&d_numAtomClauses); - StatisticsRegistry::unregisterStat(&d_numTerms); - StatisticsRegistry::unregisterStat(&d_numAtoms); - StatisticsRegistry::unregisterStat(&d_numExplainedPropagations); - StatisticsRegistry::unregisterStat(&d_numBitblastingPropagations); - StatisticsRegistry::unregisterStat(&d_bitblastTimer); + smtStatisticsRegistry()->unregisterStat(&d_numTermClauses); + smtStatisticsRegistry()->unregisterStat(&d_numAtomClauses); + smtStatisticsRegistry()->unregisterStat(&d_numTerms); + smtStatisticsRegistry()->unregisterStat(&d_numAtoms); + smtStatisticsRegistry()->unregisterStat(&d_numExplainedPropagations); + smtStatisticsRegistry()->unregisterStat(&d_numBitblastingPropagations); + smtStatisticsRegistry()->unregisterStat(&d_bitblastTimer); } bool TLazyBitblaster::MinisatNotify::notify(prop::SatLiteral lit) { @@ -496,7 +498,8 @@ void TLazyBitblaster::clearSolver() { invalidateModelCache(); // recreate sat solver - d_satSolver = prop::SatSolverFactory::createMinisat(d_ctx); + d_satSolver = prop::SatSolverFactory::createMinisat( + d_ctx, smtStatisticsRegistry()); d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar, d_nullContext, d_bv->globals()); diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp index d31ff50d1..0e6815f47 100644 --- a/src/theory/bv/slicer.cpp +++ b/src/theory/bv/slicer.cpp @@ -13,9 +13,10 @@ ** ** Bitvector theory. **/ +#include "theory/bv/slicer.h" #include "options/bv_options.h" -#include "theory/bv/slicer.h" +#include "smt/smt_statistics_registry.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" @@ -598,17 +599,17 @@ UnionFind::Statistics::Statistics(): d_avgFindDepth("theory::bv::slicer::AverageFindDepth"), d_numAddedEqualities("theory::bv::slicer::NumberOfEqualitiesAdded", Slicer::d_numAddedEqualities) { - StatisticsRegistry::registerStat(&d_numRepresentatives); - StatisticsRegistry::registerStat(&d_numSplits); - StatisticsRegistry::registerStat(&d_numMerges); - StatisticsRegistry::registerStat(&d_avgFindDepth); - StatisticsRegistry::registerStat(&d_numAddedEqualities); + smtStatisticsRegistry()->registerStat(&d_numRepresentatives); + smtStatisticsRegistry()->registerStat(&d_numSplits); + smtStatisticsRegistry()->registerStat(&d_numMerges); + smtStatisticsRegistry()->registerStat(&d_avgFindDepth); + smtStatisticsRegistry()->registerStat(&d_numAddedEqualities); } UnionFind::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_numRepresentatives); - StatisticsRegistry::unregisterStat(&d_numSplits); - StatisticsRegistry::unregisterStat(&d_numMerges); - StatisticsRegistry::unregisterStat(&d_avgFindDepth); - StatisticsRegistry::unregisterStat(&d_numAddedEqualities); + smtStatisticsRegistry()->unregisterStat(&d_numRepresentatives); + smtStatisticsRegistry()->unregisterStat(&d_numSplits); + smtStatisticsRegistry()->unregisterStat(&d_numMerges); + smtStatisticsRegistry()->unregisterStat(&d_avgFindDepth); + smtStatisticsRegistry()->unregisterStat(&d_numAddedEqualities); } diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h index 5ecc2a788..68642784f 100644 --- a/src/theory/bv/slicer.h +++ b/src/theory/bv/slicer.h @@ -23,11 +23,10 @@ #include <ext/hash_map> #include "expr/node.h" -#include "expr/statistics_registry.h" #include "theory/bv/theory_bv_utils.h" #include "util/bitvector.h" #include "util/index.h" - +#include "util/statistics_registry.h" #ifndef __CVC4__THEORY__BV__SLICER_BV_H #define __CVC4__THEORY__BV__SLICER_BV_H diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 0505035c7..4acd1b847 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -17,6 +17,7 @@ #include "options/bv_options.h" #include "options/smt_options.h" +#include "smt/smt_statistics_registry.h" #include "theory/bv/abstraction.h" #include "theory/bv/bv_eager_solver.h" #include "theory/bv/bv_subtheory_algebraic.h" @@ -123,23 +124,23 @@ TheoryBV::Statistics::Statistics(): d_weightComputationTimer("theory::bv::weightComputationTimer"), d_numMultSlice("theory::bv::NumMultSliceApplied", 0) { - StatisticsRegistry::registerStat(&d_avgConflictSize); - StatisticsRegistry::registerStat(&d_solveSubstitutions); - StatisticsRegistry::registerStat(&d_solveTimer); - StatisticsRegistry::registerStat(&d_numCallsToCheckFullEffort); - StatisticsRegistry::registerStat(&d_numCallsToCheckStandardEffort); - StatisticsRegistry::registerStat(&d_weightComputationTimer); - StatisticsRegistry::registerStat(&d_numMultSlice); + smtStatisticsRegistry()->registerStat(&d_avgConflictSize); + smtStatisticsRegistry()->registerStat(&d_solveSubstitutions); + smtStatisticsRegistry()->registerStat(&d_solveTimer); + smtStatisticsRegistry()->registerStat(&d_numCallsToCheckFullEffort); + smtStatisticsRegistry()->registerStat(&d_numCallsToCheckStandardEffort); + smtStatisticsRegistry()->registerStat(&d_weightComputationTimer); + smtStatisticsRegistry()->registerStat(&d_numMultSlice); } TheoryBV::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_avgConflictSize); - StatisticsRegistry::unregisterStat(&d_solveSubstitutions); - StatisticsRegistry::unregisterStat(&d_solveTimer); - StatisticsRegistry::unregisterStat(&d_numCallsToCheckFullEffort); - StatisticsRegistry::unregisterStat(&d_numCallsToCheckStandardEffort); - StatisticsRegistry::unregisterStat(&d_weightComputationTimer); - StatisticsRegistry::unregisterStat(&d_numMultSlice); + smtStatisticsRegistry()->unregisterStat(&d_avgConflictSize); + smtStatisticsRegistry()->unregisterStat(&d_solveSubstitutions); + smtStatisticsRegistry()->unregisterStat(&d_solveTimer); + smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckFullEffort); + smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckStandardEffort); + smtStatisticsRegistry()->unregisterStat(&d_weightComputationTimer); + smtStatisticsRegistry()->unregisterStat(&d_numMultSlice); } Node TheoryBV::getBVDivByZero(Kind k, unsigned width) { diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 8ded63c28..e7e4d464f 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -22,12 +22,12 @@ #include "context/cdhashset.h" #include "context/cdlist.h" #include "context/context.h" -#include "expr/statistics_registry.h" #include "smt/smt_globals.h" #include "theory/bv/bv_subtheory.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory.h" #include "util/hash.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index f5e2a2077..af080a970 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -22,10 +22,10 @@ #include <sstream> #include "context/context.h" -#include "expr/statistics_registry.h" #include "smt_util/command.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { @@ -328,7 +328,7 @@ class RewriteRule { // /** Constructor */ // RuleStatistics() // : d_ruleApplications(getStatName("theory::bv::RewriteRules::count"), 0) { - // StatisticsRegistry::registerStat(&d_ruleApplications); + // currentStatisticsRegistry()->registerStat(&d_ruleApplications); // } // /** Destructor */ diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 2c82943ce..6e2fdf58e 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -36,14 +36,14 @@ RewriteFunction TheoryBVRewriter::d_rewriteTable[kind::LAST_KIND]; void TheoryBVRewriter::init() { // s_allRules = new AllRewriteRules; // d_rewriteTimer = new TimerStat("theory::bv::rewriteTimer"); - // StatisticsRegistry::registerStat(d_rewriteTimer); + // smtStatisticsRegistry()->registerStat(d_rewriteTimer); initializeRewrites(); } void TheoryBVRewriter::shutdown() { // delete s_allRules; - // StatisticsRegistry::unregisterStat(d_rewriteTimer); + // smtStatisticsRegistry()->unregisterStat(d_rewriteTimer); //delete d_rewriteTimer; } diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index 7e5d429fd..3f0fa8194 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -20,8 +20,8 @@ #ifndef __CVC4__THEORY__BV__THEORY_BV_REWRITER_H #define __CVC4__THEORY__BV__THEORY_BV_REWRITER_H -#include "expr/statistics_registry.h" #include "theory/rewriter.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/ite_utilities.cpp b/src/theory/ite_utilities.cpp index 20464b14e..2791a9555 100644 --- a/src/theory/ite_utilities.cpp +++ b/src/theory/ite_utilities.cpp @@ -16,10 +16,11 @@ ** Kim, Somenzi, Jin. Efficient Term-ITE Conversion for SMT. FMCAD 2009. ** Burch, Jerry. Techniques for Verifying Superscalar Microprocessors. DAC '96 **/ - - #include "theory/ite_utilities.h" + #include <utility> + +#include "smt/smt_statistics_registry.h" #include "theory/rewriter.h" #include "theory/theory.h" @@ -276,13 +277,13 @@ ITECompressor::Statistics::Statistics(): d_compressCalls("ite-simp::compressCalls", 0), d_skolemsAdded("ite-simp::skolems", 0) { - StatisticsRegistry::registerStat(&d_compressCalls); - StatisticsRegistry::registerStat(&d_skolemsAdded); + smtStatisticsRegistry()->registerStat(&d_compressCalls); + smtStatisticsRegistry()->registerStat(&d_skolemsAdded); } ITECompressor::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_compressCalls); - StatisticsRegistry::unregisterStat(&d_skolemsAdded); + smtStatisticsRegistry()->unregisterStat(&d_compressCalls); + smtStatisticsRegistry()->unregisterStat(&d_skolemsAdded); } Node ITECompressor::push_back_boolean(Node original, Node compressed){ @@ -611,25 +612,25 @@ ITESimplifier::Statistics::Statistics(): d_simpITEVisits("ite-simp::simpITE.visits", 0), d_inSmaller("ite-simp::inSmaller") { - StatisticsRegistry::registerStat(&d_maxNonConstantsFolded); - StatisticsRegistry::registerStat(&d_unexpected); - StatisticsRegistry::registerStat(&d_unsimplified); - StatisticsRegistry::registerStat(&d_exactMatchFold); - StatisticsRegistry::registerStat(&d_binaryPredFold); - StatisticsRegistry::registerStat(&d_specialEqualityFolds); - StatisticsRegistry::registerStat(&d_simpITEVisits); - StatisticsRegistry::registerStat(&d_inSmaller); + smtStatisticsRegistry()->registerStat(&d_maxNonConstantsFolded); + smtStatisticsRegistry()->registerStat(&d_unexpected); + smtStatisticsRegistry()->registerStat(&d_unsimplified); + smtStatisticsRegistry()->registerStat(&d_exactMatchFold); + smtStatisticsRegistry()->registerStat(&d_binaryPredFold); + smtStatisticsRegistry()->registerStat(&d_specialEqualityFolds); + smtStatisticsRegistry()->registerStat(&d_simpITEVisits); + smtStatisticsRegistry()->registerStat(&d_inSmaller); } ITESimplifier::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_maxNonConstantsFolded); - StatisticsRegistry::unregisterStat(&d_unexpected); - StatisticsRegistry::unregisterStat(&d_unsimplified); - StatisticsRegistry::unregisterStat(&d_exactMatchFold); - StatisticsRegistry::unregisterStat(&d_binaryPredFold); - StatisticsRegistry::unregisterStat(&d_specialEqualityFolds); - StatisticsRegistry::unregisterStat(&d_simpITEVisits); - StatisticsRegistry::unregisterStat(&d_inSmaller); + smtStatisticsRegistry()->unregisterStat(&d_maxNonConstantsFolded); + smtStatisticsRegistry()->unregisterStat(&d_unexpected); + smtStatisticsRegistry()->unregisterStat(&d_unsimplified); + smtStatisticsRegistry()->unregisterStat(&d_exactMatchFold); + smtStatisticsRegistry()->unregisterStat(&d_binaryPredFold); + smtStatisticsRegistry()->unregisterStat(&d_specialEqualityFolds); + smtStatisticsRegistry()->unregisterStat(&d_simpITEVisits); + smtStatisticsRegistry()->unregisterStat(&d_inSmaller); } bool ITESimplifier::isConstantIte(TNode e){ diff --git a/src/theory/ite_utilities.h b/src/theory/ite_utilities.h index 27fce3071..10fe2853b 100644 --- a/src/theory/ite_utilities.h +++ b/src/theory/ite_utilities.h @@ -27,7 +27,7 @@ #include <vector> #include "expr/node.h" -#include "expr/statistics_registry.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 81fe00674..cc0b18ffe 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -16,6 +16,7 @@ #include "expr/datatype.h" #include "options/quantifiers_options.h" +#include "smt/smt_statistics_registry.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" @@ -696,15 +697,15 @@ CegInstantiation::Statistics::Statistics(): d_cegqi_lemmas_refine("CegInstantiation::cegqi_lemmas_refine", 0), d_cegqi_si_lemmas("CegInstantiation::cegqi_lemmas_si", 0) { - StatisticsRegistry::registerStat(&d_cegqi_lemmas_ce); - StatisticsRegistry::registerStat(&d_cegqi_lemmas_refine); - StatisticsRegistry::registerStat(&d_cegqi_si_lemmas); + smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_ce); + smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_refine); + smtStatisticsRegistry()->registerStat(&d_cegqi_si_lemmas); } CegInstantiation::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_cegqi_lemmas_ce); - StatisticsRegistry::unregisterStat(&d_cegqi_lemmas_refine); - StatisticsRegistry::unregisterStat(&d_cegqi_si_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_ce); + smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_refine); + smtStatisticsRegistry()->unregisterStat(&d_cegqi_si_lemmas); } diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h index 5b3c5263f..9504bd407 100644 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -18,8 +18,8 @@ #ifndef __CVC4__CEG_INSTANTIATOR_H #define __CVC4__CEG_INSTANTIATOR_H -#include "expr/statistics_registry.h" #include "theory/quantifiers_engine.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 2105007e2..5511af209 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -18,10 +18,10 @@ #ifndef __CVC4__INST_STRATEGY_CBQI_H #define __CVC4__INST_STRATEGY_CBQI_H -#include "expr/statistics_registry.h" #include "theory/arith/arithvar.h" #include "theory/quantifiers/ceg_instantiator.h" #include "theory/quantifiers/instantiation_engine.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h index a19bcca76..4e7afad5d 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/inst_strategy_e_matching.h @@ -19,10 +19,10 @@ #include "context/context.h" #include "context/context_mm.h" -#include "expr/statistics_registry.h" #include "theory/quantifiers/instantiation_engine.h" #include "theory/quantifiers/trigger.h" #include "theory/quantifiers_engine.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index dc18548a5..95b674cca 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -352,25 +352,25 @@ QModelBuilderIG::Statistics::Statistics(): d_eval_lits("QModelBuilderIG::Eval_Lits", 0 ), d_eval_lits_unknown("QModelBuilderIG::Eval_Lits_Unknown", 0 ) { - StatisticsRegistry::registerStat(&d_num_quants_init); - StatisticsRegistry::registerStat(&d_num_partial_quants_init); - StatisticsRegistry::registerStat(&d_init_inst_gen_lemmas); - StatisticsRegistry::registerStat(&d_inst_gen_lemmas); - StatisticsRegistry::registerStat(&d_eval_formulas); - StatisticsRegistry::registerStat(&d_eval_uf_terms); - StatisticsRegistry::registerStat(&d_eval_lits); - StatisticsRegistry::registerStat(&d_eval_lits_unknown); + smtStatisticsRegistry()->registerStat(&d_num_quants_init); + smtStatisticsRegistry()->registerStat(&d_num_partial_quants_init); + smtStatisticsRegistry()->registerStat(&d_init_inst_gen_lemmas); + smtStatisticsRegistry()->registerStat(&d_inst_gen_lemmas); + smtStatisticsRegistry()->registerStat(&d_eval_formulas); + smtStatisticsRegistry()->registerStat(&d_eval_uf_terms); + smtStatisticsRegistry()->registerStat(&d_eval_lits); + smtStatisticsRegistry()->registerStat(&d_eval_lits_unknown); } QModelBuilderIG::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_num_quants_init); - StatisticsRegistry::unregisterStat(&d_num_partial_quants_init); - StatisticsRegistry::unregisterStat(&d_init_inst_gen_lemmas); - StatisticsRegistry::unregisterStat(&d_inst_gen_lemmas); - StatisticsRegistry::unregisterStat(&d_eval_formulas); - StatisticsRegistry::unregisterStat(&d_eval_uf_terms); - StatisticsRegistry::unregisterStat(&d_eval_lits); - StatisticsRegistry::unregisterStat(&d_eval_lits_unknown); + smtStatisticsRegistry()->unregisterStat(&d_num_quants_init); + smtStatisticsRegistry()->unregisterStat(&d_num_partial_quants_init); + smtStatisticsRegistry()->unregisterStat(&d_init_inst_gen_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_inst_gen_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_eval_formulas); + smtStatisticsRegistry()->unregisterStat(&d_eval_uf_terms); + smtStatisticsRegistry()->unregisterStat(&d_eval_lits); + smtStatisticsRegistry()->unregisterStat(&d_eval_lits_unknown); } bool QModelBuilderIG::isQuantifierActive( Node f ){ diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 6a21a50e5..eb827edc3 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -326,13 +326,13 @@ ModelEngine::Statistics::Statistics(): d_exh_inst_lemmas("ModelEngine::Instantiations_Exhaustive", 0 ), d_mbqi_inst_lemmas("ModelEngine::Instantiations_Mbqi", 0 ) { - StatisticsRegistry::registerStat(&d_inst_rounds); - StatisticsRegistry::registerStat(&d_exh_inst_lemmas); - StatisticsRegistry::registerStat(&d_mbqi_inst_lemmas); + smtStatisticsRegistry()->registerStat(&d_inst_rounds); + smtStatisticsRegistry()->registerStat(&d_exh_inst_lemmas); + smtStatisticsRegistry()->registerStat(&d_mbqi_inst_lemmas); } ModelEngine::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_inst_rounds); - StatisticsRegistry::unregisterStat(&d_exh_inst_lemmas); - StatisticsRegistry::unregisterStat(&d_mbqi_inst_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_inst_rounds); + smtStatisticsRegistry()->unregisterStat(&d_exh_inst_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_mbqi_inst_lemmas); } diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index b6256980a..a890276f7 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -18,6 +18,7 @@ #include <vector> #include "options/quantifiers_options.h" +#include "smt/smt_statistics_registry.h" #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/trigger.h" @@ -2227,17 +2228,17 @@ QuantConflictFind::Statistics::Statistics(): d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 ), d_entailment_checks("QuantConflictFind::Entailment_Checks",0) { - StatisticsRegistry::registerStat(&d_inst_rounds); - StatisticsRegistry::registerStat(&d_conflict_inst); - StatisticsRegistry::registerStat(&d_prop_inst); - StatisticsRegistry::registerStat(&d_entailment_checks); + smtStatisticsRegistry()->registerStat(&d_inst_rounds); + smtStatisticsRegistry()->registerStat(&d_conflict_inst); + smtStatisticsRegistry()->registerStat(&d_prop_inst); + smtStatisticsRegistry()->registerStat(&d_entailment_checks); } QuantConflictFind::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_inst_rounds); - StatisticsRegistry::unregisterStat(&d_conflict_inst); - StatisticsRegistry::unregisterStat(&d_prop_inst); - StatisticsRegistry::unregisterStat(&d_entailment_checks); + smtStatisticsRegistry()->unregisterStat(&d_inst_rounds); + smtStatisticsRegistry()->unregisterStat(&d_conflict_inst); + smtStatisticsRegistry()->unregisterStat(&d_prop_inst); + smtStatisticsRegistry()->unregisterStat(&d_entailment_checks); } TNode QuantConflictFind::getZero( Kind k ) { diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index f24c10fc0..63f3379b8 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -24,9 +24,9 @@ #include <map> #include "context/cdhashmap.h" -#include "expr/statistics_registry.h" #include "theory/theory.h" #include "util/hash.h" +#include "util/statistics_registry.h" namespace CVC4 { class TheoryEngine; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index e46c59dc0..3813d7cd2 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -16,6 +16,7 @@ #include "options/quantifiers_options.h" #include "options/uf_options.h" +#include "smt/smt_statistics_registry.h" #include "theory/arrays/theory_arrays.h" #include "theory/datatypes/theory_datatypes.h" #include "theory/quantifiers/alpha_equivalence.h" @@ -82,14 +83,14 @@ quantifiers::TermDb * QuantifiersModule::getTermDatabase() { } QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te): -d_te( te ), -d_lemmas_produced_c(u), -d_skolemized(u), -d_presolve(u, true), -d_presolve_in(u), -d_presolve_cache(u), -d_presolve_cache_wq(u), -d_presolve_cache_wic(u){ + d_te( te ), + d_lemmas_produced_c(u), + d_skolemized(u), + d_presolve(u, true), + d_presolve_in(u), + d_presolve_cache(u), + d_presolve_cache_wq(u), + d_presolve_cache_wic(u){ d_eq_query = new EqualityQueryQuantifiersEngine( this ); d_term_db = new quantifiers::TermDb( c, u, this ); d_tr_trie = new inst::TriggerTrie; @@ -315,7 +316,7 @@ void QuantifiersEngine::presolve() { } void QuantifiersEngine::check( Theory::Effort e ){ - CodeTimer codeTimer(d_time); + CodeTimer codeTimer(d_statistics.d_time); if( !getMasterEqualityEngine()->consistent() ){ Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl; return; @@ -621,7 +622,7 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){ } void QuantifiersEngine::propagate( Theory::Effort level ){ - CodeTimer codeTimer(d_time); + CodeTimer codeTimer(d_statistics.d_time); for( int i=0; i<(int)d_modules.size(); i++ ){ d_modules[i]->propagate( level ); @@ -1098,59 +1099,62 @@ void QuantifiersEngine::printSynthSolution( std::ostream& out ) { } } -QuantifiersEngine::Statistics::Statistics(): - d_num_quant("QuantifiersEngine::Num_Quantifiers", 0), - d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0), - d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0), - d_instantiations("QuantifiersEngine::Instantiations_Total", 0), - d_inst_duplicate("QuantifiersEngine::Duplicate_Inst", 0), - d_inst_duplicate_eq("QuantifiersEngine::Duplicate_Inst_Eq", 0), - d_triggers("QuantifiersEngine::Triggers", 0), - d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0), - d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0), - d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0), - d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0), - d_red_lte_partial_inst("QuantifiersEngine::Reductions_Lte_Partial_Inst", 0), - d_instantiations_user_patterns("QuantifiersEngine::Instantiations_User_Patterns", 0), - d_instantiations_auto_gen("QuantifiersEngine::Instantiations_Auto_Gen", 0), - d_instantiations_guess("QuantifiersEngine::Instantiations_Guess", 0), - d_instantiations_cbqi_arith("QuantifiersEngine::Instantiations_Cbqi_Arith", 0) +QuantifiersEngine::Statistics::Statistics() + : d_time("theory::QuantifiersEngine::time"), + d_num_quant("QuantifiersEngine::Num_Quantifiers", 0), + d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0), + d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0), + d_instantiations("QuantifiersEngine::Instantiations_Total", 0), + d_inst_duplicate("QuantifiersEngine::Duplicate_Inst", 0), + d_inst_duplicate_eq("QuantifiersEngine::Duplicate_Inst_Eq", 0), + d_triggers("QuantifiersEngine::Triggers", 0), + d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0), + d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0), + d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0), + d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0), + d_red_lte_partial_inst("QuantifiersEngine::Reductions_Lte_Partial_Inst", 0), + d_instantiations_user_patterns("QuantifiersEngine::Instantiations_User_Patterns", 0), + d_instantiations_auto_gen("QuantifiersEngine::Instantiations_Auto_Gen", 0), + d_instantiations_guess("QuantifiersEngine::Instantiations_Guess", 0), + d_instantiations_cbqi_arith("QuantifiersEngine::Instantiations_Cbqi_Arith", 0) { - StatisticsRegistry::registerStat(&d_num_quant); - StatisticsRegistry::registerStat(&d_instantiation_rounds); - StatisticsRegistry::registerStat(&d_instantiation_rounds_lc); - StatisticsRegistry::registerStat(&d_instantiations); - StatisticsRegistry::registerStat(&d_inst_duplicate); - StatisticsRegistry::registerStat(&d_inst_duplicate_eq); - StatisticsRegistry::registerStat(&d_triggers); - StatisticsRegistry::registerStat(&d_simple_triggers); - StatisticsRegistry::registerStat(&d_multi_triggers); - StatisticsRegistry::registerStat(&d_multi_trigger_instantiations); - StatisticsRegistry::registerStat(&d_red_alpha_equiv); - StatisticsRegistry::registerStat(&d_red_lte_partial_inst); - StatisticsRegistry::registerStat(&d_instantiations_user_patterns); - StatisticsRegistry::registerStat(&d_instantiations_auto_gen); - StatisticsRegistry::registerStat(&d_instantiations_guess); - StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith); + smtStatisticsRegistry()->registerStat(&d_time); + smtStatisticsRegistry()->registerStat(&d_num_quant); + smtStatisticsRegistry()->registerStat(&d_instantiation_rounds); + smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc); + smtStatisticsRegistry()->registerStat(&d_instantiations); + smtStatisticsRegistry()->registerStat(&d_inst_duplicate); + smtStatisticsRegistry()->registerStat(&d_inst_duplicate_eq); + smtStatisticsRegistry()->registerStat(&d_triggers); + smtStatisticsRegistry()->registerStat(&d_simple_triggers); + smtStatisticsRegistry()->registerStat(&d_multi_triggers); + smtStatisticsRegistry()->registerStat(&d_multi_trigger_instantiations); + smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv); + smtStatisticsRegistry()->registerStat(&d_red_lte_partial_inst); + smtStatisticsRegistry()->registerStat(&d_instantiations_user_patterns); + smtStatisticsRegistry()->registerStat(&d_instantiations_auto_gen); + smtStatisticsRegistry()->registerStat(&d_instantiations_guess); + smtStatisticsRegistry()->registerStat(&d_instantiations_cbqi_arith); } QuantifiersEngine::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_num_quant); - StatisticsRegistry::unregisterStat(&d_instantiation_rounds); - StatisticsRegistry::unregisterStat(&d_instantiation_rounds_lc); - StatisticsRegistry::unregisterStat(&d_instantiations); - StatisticsRegistry::unregisterStat(&d_inst_duplicate); - StatisticsRegistry::unregisterStat(&d_inst_duplicate_eq); - StatisticsRegistry::unregisterStat(&d_triggers); - StatisticsRegistry::unregisterStat(&d_simple_triggers); - StatisticsRegistry::unregisterStat(&d_multi_triggers); - StatisticsRegistry::unregisterStat(&d_multi_trigger_instantiations); - StatisticsRegistry::unregisterStat(&d_red_alpha_equiv); - StatisticsRegistry::unregisterStat(&d_red_lte_partial_inst); - StatisticsRegistry::unregisterStat(&d_instantiations_user_patterns); - StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen); - StatisticsRegistry::unregisterStat(&d_instantiations_guess); - StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith); + smtStatisticsRegistry()->unregisterStat(&d_time); + smtStatisticsRegistry()->unregisterStat(&d_num_quant); + smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds); + smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc); + smtStatisticsRegistry()->unregisterStat(&d_instantiations); + smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate); + smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_eq); + smtStatisticsRegistry()->unregisterStat(&d_triggers); + smtStatisticsRegistry()->unregisterStat(&d_simple_triggers); + smtStatisticsRegistry()->unregisterStat(&d_multi_triggers); + smtStatisticsRegistry()->unregisterStat(&d_multi_trigger_instantiations); + smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv); + smtStatisticsRegistry()->unregisterStat(&d_red_lte_partial_inst); + smtStatisticsRegistry()->unregisterStat(&d_instantiations_user_patterns); + smtStatisticsRegistry()->unregisterStat(&d_instantiations_auto_gen); + smtStatisticsRegistry()->unregisterStat(&d_instantiations_guess); + smtStatisticsRegistry()->unregisterStat(&d_instantiations_cbqi_arith); } eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){ diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index ba41b2ca3..aa770ad67 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -24,12 +24,12 @@ #include "context/cdchunk_list.h" #include "context/cdhashset.h" #include "expr/attribute.h" -#include "expr/statistics_registry.h" #include "options/quantifiers_modes.h" #include "theory/quantifiers/inst_match.h" #include "theory/quantifiers/quant_util.h" #include "theory/theory.h" #include "util/hash.h" +#include "util/statistics_registry.h" namespace CVC4 { @@ -206,8 +206,7 @@ private: NodeList d_presolve_cache; BoolList d_presolve_cache_wq; BoolList d_presolve_cache_wic; -private: - KEEP_STATISTIC(TimerStat, d_time, "theory::QuantifiersEngine::time"); + public: QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te); ~QuantifiersEngine(); @@ -346,6 +345,7 @@ public: /** statistics class */ class Statistics { public: + TimerStat d_time; IntStat d_num_quant; IntStat d_instantiation_rounds; IntStat d_instantiation_rounds_lc; @@ -382,7 +382,7 @@ private: std::map< Node, int > d_rep_score; /** reset count */ int d_reset_count; -private: + /** node contains */ Node getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache ); /** get score */ diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 758f4a913..697736ebf 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -19,8 +19,10 @@ #include "expr/resource_manager.h" #include "theory/theory.h" -#include "theory/rewriter_tables.h" #include "smt/smt_engine_scope.h" +#include "smt/smt_statistics_registry.h" +#include "theory/rewriter_tables.h" + using namespace std; diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 0c3171065..d0866e537 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -20,6 +20,7 @@ #include "expr/emptyset.h" #include "options/sets_options.h" +#include "smt/smt_statistics_registry.h" #include "theory/sets/expr_patterns.h" // ONLY included here #include "theory/sets/scrutinize.h" #include "theory/sets/theory_sets.h" @@ -924,16 +925,16 @@ TheorySetsPrivate::Statistics::Statistics() : , d_memberLemmas("theory::sets::lemmas::member", 0) , d_disequalityLemmas("theory::sets::lemmas::disequality", 0) { - StatisticsRegistry::registerStat(&d_getModelValueTime); - StatisticsRegistry::registerStat(&d_memberLemmas); - StatisticsRegistry::registerStat(&d_disequalityLemmas); + smtStatisticsRegistry()->registerStat(&d_getModelValueTime); + smtStatisticsRegistry()->registerStat(&d_memberLemmas); + smtStatisticsRegistry()->registerStat(&d_disequalityLemmas); } TheorySetsPrivate::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_getModelValueTime); - StatisticsRegistry::unregisterStat(&d_memberLemmas); - StatisticsRegistry::unregisterStat(&d_disequalityLemmas); + smtStatisticsRegistry()->unregisterStat(&d_getModelValueTime); + smtStatisticsRegistry()->unregisterStat(&d_memberLemmas); + smtStatisticsRegistry()->unregisterStat(&d_disequalityLemmas); } diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index a41326350..89cba3ae4 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -13,8 +13,9 @@ ** \todo document this file **/ - #include "theory/shared_terms_database.h" + +#include "smt/smt_statistics_registry.h" #include "theory/theory_engine.h" using namespace std; @@ -33,12 +34,12 @@ SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine, context::Co , d_theoryEngine(theoryEngine) , d_inConflict(context, false) { - StatisticsRegistry::registerStat(&d_statSharedTerms); + smtStatisticsRegistry()->registerStat(&d_statSharedTerms); } SharedTermsDatabase::~SharedTermsDatabase() throw(AssertionException) { - StatisticsRegistry::unregisterStat(&d_statSharedTerms); + smtStatisticsRegistry()->unregisterStat(&d_statSharedTerms); } void SharedTermsDatabase::addEqualityToPropagate(TNode equality) { diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index fd45cca15..c15336e29 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -19,9 +19,9 @@ #include "context/cdhashset.h" #include "expr/node.h" -#include "expr/statistics_registry.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" +#include "util/statistics_registry.h" namespace CVC4 { diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index b68687d54..4405fe406 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -21,6 +21,7 @@ #include "expr/kind.h" #include "options/strings_options.h" #include "smt/logic_exception.h" +#include "smt/smt_statistics_registry.h" #include "smt_util/command.h" #include "theory/rewriter.h" #include "theory/strings/theory_strings_rewriter.h" @@ -4416,19 +4417,19 @@ TheoryStrings::Statistics::Statistics(): d_loop_lemmas("TheoryStrings::NumOfLoops", 0), d_new_skolems("TheoryStrings::NumOfNewSkolems", 0) { - StatisticsRegistry::registerStat(&d_splits); - StatisticsRegistry::registerStat(&d_eq_splits); - StatisticsRegistry::registerStat(&d_deq_splits); - StatisticsRegistry::registerStat(&d_loop_lemmas); - StatisticsRegistry::registerStat(&d_new_skolems); + smtStatisticsRegistry()->registerStat(&d_splits); + smtStatisticsRegistry()->registerStat(&d_eq_splits); + smtStatisticsRegistry()->registerStat(&d_deq_splits); + smtStatisticsRegistry()->registerStat(&d_loop_lemmas); + smtStatisticsRegistry()->registerStat(&d_new_skolems); } TheoryStrings::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_splits); - StatisticsRegistry::unregisterStat(&d_eq_splits); - StatisticsRegistry::unregisterStat(&d_deq_splits); - StatisticsRegistry::unregisterStat(&d_loop_lemmas); - StatisticsRegistry::unregisterStat(&d_new_skolems); + smtStatisticsRegistry()->unregisterStat(&d_splits); + smtStatisticsRegistry()->unregisterStat(&d_eq_splits); + smtStatisticsRegistry()->unregisterStat(&d_deq_splits); + smtStatisticsRegistry()->unregisterStat(&d_loop_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_new_skolems); } }/* CVC4::theory::strings namespace */ diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 05795ca8f..9e946f8d7 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -19,6 +19,7 @@ #include <vector> #include "base/cvc4_assert.h" +#include "smt/smt_statistics_registry.h" #include "theory/substitutions.h" #include "theory/quantifiers_engine.h" @@ -47,9 +48,33 @@ std::ostream& operator<<(std::ostream& os, Theory::Effort level){ return os; }/* ostream& operator<<(ostream&, Theory::Effort) */ +Theory::Theory(TheoryId id, context::Context* satContext, context::UserContext* userContext, + OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, + SmtGlobals* globals) throw() + : d_id(id) + , d_satContext(satContext) + , d_userContext(userContext) + , d_logicInfo(logicInfo) + , d_facts(satContext) + , d_factsHead(satContext, 0) + , d_sharedTermsIndex(satContext, 0) + , d_careGraph(NULL) + , d_quantEngine(NULL) + , d_checkTime(statName(id, "checkTime")) + , d_computeCareGraphTime(statName(id, "computeCareGraphTime")) + , d_sharedTerms(satContext) + , d_out(&out) + , d_valuation(valuation) + , d_proofEnabled(false) + , d_globals(globals) +{ + smtStatisticsRegistry()->registerStat(&d_checkTime); + smtStatisticsRegistry()->registerStat(&d_computeCareGraphTime); +} + Theory::~Theory() { - StatisticsRegistry::unregisterStat(&d_checkTime); - StatisticsRegistry::unregisterStat(&d_computeCareGraphTime); + smtStatisticsRegistry()->unregisterStat(&d_checkTime); + smtStatisticsRegistry()->unregisterStat(&d_computeCareGraphTime); } TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) { diff --git a/src/theory/theory.h b/src/theory/theory.h index d17d97f97..f7d9ee6a0 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -28,7 +28,6 @@ #include "context/cdo.h" #include "context/context.h" #include "expr/node.h" -#include "expr/statistics_registry.h" #include "lib/ffs.h" #include "options/options.h" #include "options/theory_options.h" @@ -40,6 +39,7 @@ #include "theory/logic_info.h" #include "theory/output_channel.h" #include "theory/valuation.h" +#include "util/statistics_registry.h" namespace CVC4 { @@ -247,27 +247,7 @@ protected: */ Theory(TheoryId id, context::Context* satContext, context::UserContext* userContext, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, - SmtGlobals* globals) throw() - : d_id(id) - , d_satContext(satContext) - , d_userContext(userContext) - , d_logicInfo(logicInfo) - , d_facts(satContext) - , d_factsHead(satContext, 0) - , d_sharedTermsIndex(satContext, 0) - , d_careGraph(NULL) - , d_quantEngine(NULL) - , d_checkTime(statName(id, "checkTime")) - , d_computeCareGraphTime(statName(id, "computeCareGraphTime")) - , d_sharedTerms(satContext) - , d_out(&out) - , d_valuation(valuation) - , d_proofEnabled(false) - , d_globals(globals) - { - StatisticsRegistry::registerStat(&d_checkTime); - StatisticsRegistry::registerStat(&d_computeCareGraphTime); - } + SmtGlobals* globals) throw(); /** * This is called at shutdown time by the TheoryEngine, just before diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index a55b3a1c9..bcc16c63a 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -49,9 +49,10 @@ using namespace std; -using namespace CVC4; using namespace CVC4::theory; +namespace CVC4 { + void TheoryEngine::finishInit() { PROOF (ProofManager::initTheoryProof(); ); @@ -152,13 +153,13 @@ TheoryEngine::TheoryEngine(context::Context* context, d_curr_model = new theory::TheoryModel(userContext, "DefaultModel", true); d_curr_model_builder = new theory::TheoryEngineModelBuilder(this); - StatisticsRegistry::registerStat(&d_combineTheoriesTime); + smtStatisticsRegistry()->registerStat(&d_combineTheoriesTime); d_true = NodeManager::currentNM()->mkConst<bool>(true); d_false = NodeManager::currentNM()->mkConst<bool>(false); d_iteUtilities = new ITEUtilities(d_iteRemover.getContainsVisitor()); - StatisticsRegistry::registerStat(&d_arithSubstitutionsAdded); + smtStatisticsRegistry()->registerStat(&d_arithSubstitutionsAdded); } TheoryEngine::~TheoryEngine() { @@ -178,13 +179,13 @@ TheoryEngine::~TheoryEngine() { delete d_masterEqualityEngine; - StatisticsRegistry::unregisterStat(&d_combineTheoriesTime); + smtStatisticsRegistry()->unregisterStat(&d_combineTheoriesTime); delete d_unconstrainedSimp; delete d_iteUtilities; - StatisticsRegistry::unregisterStat(&d_arithSubstitutionsAdded); + smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded); } void TheoryEngine::interrupt() throw(ModalException) { @@ -1762,3 +1763,30 @@ std::pair<bool, Node> TheoryEngine::entailmentCheck(theory::TheoryOfMode mode, T void TheoryEngine::spendResource(unsigned ammount) { d_resourceManager->spendResource(ammount); } + +TheoryEngine::Statistics::Statistics(theory::TheoryId theory): + conflicts(mkName("theory<", theory, ">::conflicts"), 0), + propagations(mkName("theory<", theory, ">::propagations"), 0), + lemmas(mkName("theory<", theory, ">::lemmas"), 0), + requirePhase(mkName("theory<", theory, ">::requirePhase"), 0), + flipDecision(mkName("theory<", theory, ">::flipDecision"), 0), + restartDemands(mkName("theory<", theory, ">::restartDemands"), 0) +{ + smtStatisticsRegistry()->registerStat(&conflicts); + smtStatisticsRegistry()->registerStat(&propagations); + smtStatisticsRegistry()->registerStat(&lemmas); + smtStatisticsRegistry()->registerStat(&requirePhase); + smtStatisticsRegistry()->registerStat(&flipDecision); + smtStatisticsRegistry()->registerStat(&restartDemands); +} + +TheoryEngine::Statistics::~Statistics() { + smtStatisticsRegistry()->unregisterStat(&conflicts); + smtStatisticsRegistry()->unregisterStat(&propagations); + smtStatisticsRegistry()->unregisterStat(&lemmas); + smtStatisticsRegistry()->unregisterStat(&requirePhase); + smtStatisticsRegistry()->unregisterStat(&flipDecision); + smtStatisticsRegistry()->unregisterStat(&restartDemands); +} + +}/* CVC4 namespace */ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index adc4daeee..7cb15ca97 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -26,7 +26,6 @@ #include "base/cvc4_assert.h" #include "context/cdhashset.h" #include "expr/node.h" -#include "expr/statistics_registry.h" #include "options/options.h" #include "options/smt_options.h" #include "prop/prop_engine.h" @@ -44,6 +43,7 @@ #include "theory/theory.h" #include "theory/uf/equality_engine.h" #include "theory/valuation.h" +#include "util/statistics_registry.h" #include "util/unsafe_interrupt_exception.h" namespace CVC4 { @@ -225,30 +225,8 @@ class TheoryEngine { IntStat conflicts, propagations, lemmas, requirePhase, flipDecision, restartDemands; - Statistics(theory::TheoryId theory): - conflicts(mkName("theory<", theory, ">::conflicts"), 0), - propagations(mkName("theory<", theory, ">::propagations"), 0), - lemmas(mkName("theory<", theory, ">::lemmas"), 0), - requirePhase(mkName("theory<", theory, ">::requirePhase"), 0), - flipDecision(mkName("theory<", theory, ">::flipDecision"), 0), - restartDemands(mkName("theory<", theory, ">::restartDemands"), 0) - { - StatisticsRegistry::registerStat(&conflicts); - StatisticsRegistry::registerStat(&propagations); - StatisticsRegistry::registerStat(&lemmas); - StatisticsRegistry::registerStat(&requirePhase); - StatisticsRegistry::registerStat(&flipDecision); - StatisticsRegistry::registerStat(&restartDemands); - } - - ~Statistics() { - StatisticsRegistry::unregisterStat(&conflicts); - StatisticsRegistry::unregisterStat(&propagations); - StatisticsRegistry::unregisterStat(&lemmas); - StatisticsRegistry::unregisterStat(&requirePhase); - StatisticsRegistry::unregisterStat(&flipDecision); - StatisticsRegistry::unregisterStat(&restartDemands); - } + Statistics(theory::TheoryId theory); + ~Statistics(); };/* class TheoryEngine::Statistics */ @@ -764,7 +742,7 @@ public: inline bool isTheoryEnabled(theory::TheoryId theoryId) const { return d_logicInfo.isTheoryEnabled(theoryId); } - + /** * Returns the equality status of the two terms, from the theory * that owns the domain type. The types of a and b must be the same. @@ -791,7 +769,7 @@ public: * Print solution for synthesis conjectures found by ce_guided_instantiation module */ void printSynthSolution( std::ostream& out ); - + /** * Forwards an entailment check according to the given theoryOfMode. * See theory.h for documentation on entailmentCheck(). @@ -835,11 +813,11 @@ public: SharedTermsDatabase* getSharedTermsDatabase() { return &d_sharedTerms; } theory::eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; } - + RemoveITE* getIteRemover() { return &d_iteRemover; } SortInference* getSortInference() { return &d_sortInfer; } - + /** Prints the assertions to the debug stream */ void printAssertions(const char* tag); diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index cd6459a3c..828d53144 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -17,10 +17,32 @@ #include "theory/uf/equality_engine.h" +#include "smt/smt_statistics_registry.h" + namespace CVC4 { namespace theory { namespace eq { +EqualityEngine::Statistics::Statistics(std::string name) + : mergesCount(name + "::mergesCount", 0), + termsCount(name + "::termsCount", 0), + functionTermsCount(name + "::functionTermsCount", 0), + constantTermsCount(name + "::constantTermsCount", 0) +{ + smtStatisticsRegistry()->registerStat(&mergesCount); + smtStatisticsRegistry()->registerStat(&termsCount); + smtStatisticsRegistry()->registerStat(&functionTermsCount); + smtStatisticsRegistry()->registerStat(&constantTermsCount); +} + +EqualityEngine::Statistics::~Statistics() { + smtStatisticsRegistry()->unregisterStat(&mergesCount); + smtStatisticsRegistry()->unregisterStat(&termsCount); + smtStatisticsRegistry()->unregisterStat(&functionTermsCount); + smtStatisticsRegistry()->unregisterStat(&constantTermsCount); +} + + /** * Data used in the BFS search through the equality graph. */ @@ -2058,4 +2080,3 @@ void EqProof::debug_print( const char * c, unsigned tb ){ } // Namespace uf } // Namespace theory } // Namespace CVC4 - diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index f7f7f9ddd..87074aebc 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -29,10 +29,10 @@ #include "context/cdo.h" #include "expr/kind_map.h" #include "expr/node.h" -#include "expr/statistics_registry.h" #include "theory/rewriter.h" #include "theory/theory.h" #include "theory/uf/equality_engine_types.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { @@ -193,24 +193,9 @@ public: /** Number of constant terms managed by the system */ IntStat constantTermsCount; - Statistics(std::string name) - : mergesCount(name + "::mergesCount", 0), - termsCount(name + "::termsCount", 0), - functionTermsCount(name + "::functionTermsCount", 0), - constantTermsCount(name + "::constantTermsCount", 0) - { - StatisticsRegistry::registerStat(&mergesCount); - StatisticsRegistry::registerStat(&termsCount); - StatisticsRegistry::registerStat(&functionTermsCount); - StatisticsRegistry::registerStat(&constantTermsCount); - } + Statistics(std::string name); - ~Statistics() { - StatisticsRegistry::unregisterStat(&mergesCount); - StatisticsRegistry::unregisterStat(&termsCount); - StatisticsRegistry::unregisterStat(&functionTermsCount); - StatisticsRegistry::unregisterStat(&constantTermsCount); - } + ~Statistics(); };/* struct EqualityEngine::statistics */ private: @@ -900,4 +885,3 @@ public: } // Namespace eq } // Namespace theory } // Namespace CVC4 - diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h index e49b4652a..763ced650 100644 --- a/src/theory/uf/symmetry_breaker.h +++ b/src/theory/uf/symmetry_breaker.h @@ -52,7 +52,8 @@ #include "context/context.h" #include "expr/node.h" #include "expr/node_builder.h" -#include "expr/statistics_registry.h" +#include "smt/smt_statistics_registry.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 0f8ccf49a..9fceedc96 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -2058,23 +2058,23 @@ StrongSolverTheoryUF::Statistics::Statistics(): d_totality_lemmas("StrongSolverTheoryUF::Totality_Lemmas", 0), d_max_model_size("StrongSolverTheoryUF::Max_Model_Size", 1) { - StatisticsRegistry::registerStat(&d_clique_conflicts); - StatisticsRegistry::registerStat(&d_clique_lemmas); - StatisticsRegistry::registerStat(&d_split_lemmas); - StatisticsRegistry::registerStat(&d_disamb_term_lemmas); - StatisticsRegistry::registerStat(&d_sym_break_lemmas); - StatisticsRegistry::registerStat(&d_totality_lemmas); - StatisticsRegistry::registerStat(&d_max_model_size); + smtStatisticsRegistry()->registerStat(&d_clique_conflicts); + smtStatisticsRegistry()->registerStat(&d_clique_lemmas); + smtStatisticsRegistry()->registerStat(&d_split_lemmas); + smtStatisticsRegistry()->registerStat(&d_disamb_term_lemmas); + smtStatisticsRegistry()->registerStat(&d_sym_break_lemmas); + smtStatisticsRegistry()->registerStat(&d_totality_lemmas); + smtStatisticsRegistry()->registerStat(&d_max_model_size); } StrongSolverTheoryUF::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_clique_conflicts); - StatisticsRegistry::unregisterStat(&d_clique_lemmas); - StatisticsRegistry::unregisterStat(&d_split_lemmas); - StatisticsRegistry::unregisterStat(&d_disamb_term_lemmas); - StatisticsRegistry::unregisterStat(&d_sym_break_lemmas); - StatisticsRegistry::unregisterStat(&d_totality_lemmas); - StatisticsRegistry::unregisterStat(&d_max_model_size); + smtStatisticsRegistry()->unregisterStat(&d_clique_conflicts); + smtStatisticsRegistry()->unregisterStat(&d_clique_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_split_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_disamb_term_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_sym_break_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_totality_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_max_model_size); } @@ -2141,9 +2141,9 @@ void DisequalityPropagator::assertPredicate( Node p, bool polarity ) { DisequalityPropagator::Statistics::Statistics(): d_propagations("StrongSolverTheoryUF::Disequality_Propagations", 0) { - StatisticsRegistry::registerStat(& d_propagations); + smtStatisticsRegistry()->registerStat(& d_propagations); } DisequalityPropagator::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(& d_propagations); + smtStatisticsRegistry()->unregisterStat(& d_propagations); } diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index 45d7fc3cc..24d7f840f 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -21,8 +21,8 @@ #include "context/cdhashmap.h" #include "context/context.h" #include "context/context_mm.h" -#include "expr/statistics_registry.h" #include "theory/theory.h" +#include "util/statistics_registry.h" namespace CVC4 { diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp index 997c998e6..dda73c1d9 100644 --- a/src/theory/unconstrained_simplifier.cpp +++ b/src/theory/unconstrained_simplifier.cpp @@ -17,8 +17,10 @@ #include "theory/unconstrained_simplifier.h" + #include "theory/rewriter.h" #include "theory/logic_info.h" +#include "smt/smt_statistics_registry.h" using namespace std; using namespace CVC4; @@ -30,13 +32,13 @@ UnconstrainedSimplifier::UnconstrainedSimplifier(context::Context* context, : d_numUnconstrainedElim("preprocessor::number of unconstrained elims", 0), d_context(context), d_substitutions(context), d_logicInfo(logicInfo) { - StatisticsRegistry::registerStat(&d_numUnconstrainedElim); + smtStatisticsRegistry()->registerStat(&d_numUnconstrainedElim); } UnconstrainedSimplifier::~UnconstrainedSimplifier() { - StatisticsRegistry::unregisterStat(&d_numUnconstrainedElim); + smtStatisticsRegistry()->unregisterStat(&d_numUnconstrainedElim); } diff --git a/src/theory/unconstrained_simplifier.h b/src/theory/unconstrained_simplifier.h index 6c04d66e7..e23c4853d 100644 --- a/src/theory/unconstrained_simplifier.h +++ b/src/theory/unconstrained_simplifier.h @@ -24,8 +24,8 @@ #include <utility> #include "expr/node.h" -#include "expr/statistics_registry.h" #include "theory/substitutions.h" +#include "util/statistics_registry.h" namespace CVC4 { |