diff options
author | Tim King <taking@google.com> | 2016-01-08 16:44:57 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-01-08 16:44:57 -0800 |
commit | f4ef7af0a2295691f281ee1604dfeb4082fe229c (patch) | |
tree | 995e512e5669cec6bbc9447d00ec912d5e4c19e3 /src/theory/bv | |
parent | def0a07f9676a292a849d7fc8269ffd0901ce156 (diff) |
Removing StatisticsRegistry's static functions current() and registerStat().
- The functionality the get the StatisticsRegistry attached to the SmtEngine was previously through StatisticsRegistry::current(). This is the dominant StatisticsRegistry in the code. (There is another StatisticsRegistry attached to the NodeManager.) Having this be a static function on StatisticsRegistry requires the use of an SmtEngine in the wrong compilation unit.
- Usages of StatisticsRegistry::current() that were visible in prop/{bvminisat,minisat} has been removed. A pointer to the relevant StatisticsRegistry should be passed instead into the constructor.
- The function StatisticsRegistry::current() has been replaced by SmtScope::currentStatisticsRegistry(). SmtScope is in the libcvc4 package, where SmtEngine is available in the compilation unit.
- The function smtStatisticsRegistry() is a synonym for SmtScope::currentStatisticsRegistry() in smt/smt_statistics_registry.h. This header has fewer include dependencies than the one for SmtScope.
- Correspondingly, the static functions StatisticsRegistry::{registerStat, unregisterStat} have been removed. One should instead use smtStatisticsRegistry()->{registerStat,unregisterStat} instead.
- The KEEP_STATISTIC macro has been moved into smt/smt_statistics_registry.h.
- Documents the reason StatisticsRegistry is CVC4_PUBLIC. This lets me remove the warning I added.
- Removing most operators for timespec from statistics_registry.h file. These a bit error prone in clang.
- Most of the really confusing ifdef's in util/statistics_registry.h are gone.
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/abstraction.cpp | 13 | ||||
-rw-r--r-- | src/theory/bv/abstraction.h | 2 | ||||
-rw-r--r-- | src/theory/bv/aig_bitblaster.cpp | 20 | ||||
-rw-r--r-- | src/theory/bv/bv_quick_check.cpp | 32 | ||||
-rw-r--r-- | src/theory/bv/bv_quick_check.h | 2 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_algebraic.cpp | 35 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_bitblast.cpp | 9 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_core.cpp | 9 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_inequality.cpp | 5 | ||||
-rw-r--r-- | src/theory/bv/bv_to_bool.cpp | 17 | ||||
-rw-r--r-- | src/theory/bv/bv_to_bool.h | 6 | ||||
-rw-r--r-- | src/theory/bv/eager_bitblaster.cpp | 4 | ||||
-rw-r--r-- | src/theory/bv/lazy_bitblaster.cpp | 35 | ||||
-rw-r--r-- | src/theory/bv/slicer.cpp | 23 | ||||
-rw-r--r-- | src/theory/bv/slicer.h | 3 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 29 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules.h | 4 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 4 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.h | 2 |
20 files changed, 134 insertions, 122 deletions
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 { |