From 2384a8d85517e00bc94e7fcf759a75dc6ea9b009 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Sat, 11 Sep 2021 21:13:34 +0200 Subject: [PATCH] Use StatisticsRegistry from Env (#7166) This commit better integrates the StatisticsRegistry with the environment. It makes the registry an `EnvObj` itself and adds a getter to `EnvObj` to get the registry. It also refactors parts of cvc5 to use this new mechanism to obtain the registry instead of using the (global, static) `smtStatisticsRegistry()` function. --- src/preprocessing/passes/bool_to_bv.cpp | 15 +- src/preprocessing/passes/bool_to_bv.h | 2 +- src/preprocessing/passes/bv_to_bool.cpp | 14 +- src/preprocessing/passes/bv_to_bool.h | 2 +- src/preprocessing/passes/ite_simp.cpp | 8 +- src/preprocessing/passes/ite_simp.h | 2 +- src/preprocessing/passes/learned_rewrite.cpp | 2 +- src/preprocessing/passes/miplib_trick.cpp | 7 +- src/preprocessing/passes/miplib_trick.h | 2 +- src/preprocessing/passes/non_clausal_simp.cpp | 5 +- src/preprocessing/passes/non_clausal_simp.h | 2 +- .../passes/unconstrained_simplifier.cpp | 2 +- src/preprocessing/preprocessing_pass.cpp | 2 +- src/preprocessing/util/ite_utilities.cpp | 37 ++- src/preprocessing/util/ite_utilities.h | 4 +- src/smt/env.cpp | 2 +- src/smt/env_obj.cpp | 5 + src/smt/env_obj.h | 4 + src/theory/arith/theory_arith.cpp | 4 +- src/theory/arith/theory_arith_private.cpp | 250 ++++++++---------- src/theory/arith/theory_arith_private.h | 2 +- src/theory/arrays/theory_arrays.cpp | 22 +- src/theory/bv/theory_bv.cpp | 8 +- src/theory/bv/theory_bv.h | 2 +- src/theory/theory.cpp | 6 +- src/theory/theory_engine.cpp | 2 +- src/theory/theory_inference_manager.cpp | 6 +- src/util/statistics_registry.cpp | 19 +- src/util/statistics_registry.h | 5 +- test/unit/test_env.h | 48 ++++ test/unit/util/stats_black.cpp | 6 +- 31 files changed, 259 insertions(+), 238 deletions(-) create mode 100644 test/unit/test_env.h diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp index 206f12a3f..90b55a48a 100644 --- a/src/preprocessing/passes/bool_to_bv.cpp +++ b/src/preprocessing/passes/bool_to_bv.cpp @@ -34,7 +34,8 @@ namespace passes { using namespace cvc5::theory; BoolToBV::BoolToBV(PreprocessingPassContext* preprocContext) - : PreprocessingPass(preprocContext, "bool-to-bv"), d_statistics() + : PreprocessingPass(preprocContext, "bool-to-bv"), + d_statistics(statisticsRegistry()) { d_boolToBVMode = options().bv.boolToBitvector; }; @@ -403,15 +404,15 @@ void BoolToBV::rebuildNode(const TNode& n, Kind new_kind) updateCache(n, builder.constructNode()); } -BoolToBV::Statistics::Statistics() - : d_numIteToBvite(smtStatisticsRegistry().registerInt( - "preprocessing::passes::BoolToBV::NumIteToBvite")), +BoolToBV::Statistics::Statistics(StatisticsRegistry& reg) + : d_numIteToBvite( + reg.registerInt("preprocessing::passes::BoolToBV::NumIteToBvite")), // the following two statistics are not correct in the ITE mode, because // we might discard rebuilt nodes if we fails to convert a bool to // width-one bit-vector (never forces) - d_numTermsLowered(smtStatisticsRegistry().registerInt( - "preprocessing::passes:BoolToBV::NumTermsLowered")), - d_numIntroducedItes(smtStatisticsRegistry().registerInt( + d_numTermsLowered( + reg.registerInt("preprocessing::passes:BoolToBV::NumTermsLowered")), + d_numIntroducedItes(reg.registerInt( "preprocessing::passes::BoolToBV::NumTermsForcedLowered")) { } diff --git a/src/preprocessing/passes/bool_to_bv.h b/src/preprocessing/passes/bool_to_bv.h index 0bef7c6b5..06c4dd1c1 100644 --- a/src/preprocessing/passes/bool_to_bv.h +++ b/src/preprocessing/passes/bool_to_bv.h @@ -43,7 +43,7 @@ class BoolToBV : public PreprocessingPass IntStat d_numIteToBvite; IntStat d_numTermsLowered; IntStat d_numIntroducedItes; - Statistics(); + Statistics(StatisticsRegistry& reg); }; /** Takes an assertion and attempts to create more bit-vector structure diff --git a/src/preprocessing/passes/bv_to_bool.cpp b/src/preprocessing/passes/bv_to_bool.cpp index 0d0131e3e..ca48c1a37 100644 --- a/src/preprocessing/passes/bv_to_bool.cpp +++ b/src/preprocessing/passes/bv_to_bool.cpp @@ -43,7 +43,7 @@ BVToBool::BVToBool(PreprocessingPassContext* preprocContext) d_boolCache(), d_one(bv::utils::mkOne(1)), d_zero(bv::utils::mkZero(1)), - d_statistics(){}; + d_statistics(statisticsRegistry()){}; PreprocessingPassResult BVToBool::applyInternal( AssertionPipeline* assertionsToPreprocess) @@ -287,12 +287,12 @@ void BVToBool::liftBvToBool(const std::vector& assertions, } } -BVToBool::Statistics::Statistics() - : d_numTermsLifted(smtStatisticsRegistry().registerInt( - "preprocessing::passes::BVToBool::NumTermsLifted")), - d_numAtomsLifted(smtStatisticsRegistry().registerInt( - "preprocessing::passes::BVToBool::NumAtomsLifted")), - d_numTermsForcedLifted(smtStatisticsRegistry().registerInt( +BVToBool::Statistics::Statistics(StatisticsRegistry& reg) + : d_numTermsLifted( + reg.registerInt("preprocessing::passes::BVToBool::NumTermsLifted")), + d_numAtomsLifted( + reg.registerInt("preprocessing::passes::BVToBool::NumAtomsLifted")), + d_numTermsForcedLifted(reg.registerInt( "preprocessing::passes::BVToBool::NumTermsForcedLifted")) { } diff --git a/src/preprocessing/passes/bv_to_bool.h b/src/preprocessing/passes/bv_to_bool.h index d34f2f77f..cca79c900 100644 --- a/src/preprocessing/passes/bv_to_bool.h +++ b/src/preprocessing/passes/bv_to_bool.h @@ -44,7 +44,7 @@ class BVToBool : public PreprocessingPass IntStat d_numTermsLifted; IntStat d_numAtomsLifted; IntStat d_numTermsForcedLifted; - Statistics(); + Statistics(StatisticsRegistry& reg); }; void addToBoolCache(TNode term, Node new_term); Node getBoolCache(TNode term) const; diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp index 5f9b4fb1d..e951b9cb0 100644 --- a/src/preprocessing/passes/ite_simp.cpp +++ b/src/preprocessing/passes/ite_simp.cpp @@ -80,8 +80,8 @@ void compressBeforeRealAssertions(AssertionPipeline* assertionsToPreprocess, /* -------------------------------------------------------------------------- */ -ITESimp::Statistics::Statistics() - : d_arithSubstitutionsAdded(smtStatisticsRegistry().registerInt( +ITESimp::Statistics::Statistics(StatisticsRegistry& reg) + : d_arithSubstitutionsAdded(reg.registerInt( "preprocessing::passes::ITESimp::ArithSubstitutionsAdded")) { } @@ -222,7 +222,9 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess) /* -------------------------------------------------------------------------- */ ITESimp::ITESimp(PreprocessingPassContext* preprocContext) - : PreprocessingPass(preprocContext, "ite-simp"), d_iteUtilities(d_env) + : PreprocessingPass(preprocContext, "ite-simp"), + d_iteUtilities(d_env), + d_statistics(statisticsRegistry()) { } diff --git a/src/preprocessing/passes/ite_simp.h b/src/preprocessing/passes/ite_simp.h index ca8547d46..183cec946 100644 --- a/src/preprocessing/passes/ite_simp.h +++ b/src/preprocessing/passes/ite_simp.h @@ -39,7 +39,7 @@ class ITESimp : public PreprocessingPass struct Statistics { IntStat d_arithSubstitutionsAdded; - Statistics(); + Statistics(StatisticsRegistry& reg); }; Node simpITE(util::ITEUtilities* ite_utils, TNode assertion); diff --git a/src/preprocessing/passes/learned_rewrite.cpp b/src/preprocessing/passes/learned_rewrite.cpp index c2693e927..81f5718cf 100644 --- a/src/preprocessing/passes/learned_rewrite.cpp +++ b/src/preprocessing/passes/learned_rewrite.cpp @@ -52,7 +52,7 @@ std::ostream& operator<<(std::ostream& out, LearnedRewriteId i) LearnedRewrite::LearnedRewrite(PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "learned-rewrite"), - d_lrewCount(smtStatisticsRegistry().registerHistogram( + d_lrewCount(statisticsRegistry().registerHistogram( "LearnedRewrite::lrewCount")) { } diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index c40a65bc1..8202acb15 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -73,7 +73,8 @@ void traceBackToAssertions(booleans::CircuitPropagator* propagator, } // namespace MipLibTrick::MipLibTrick(PreprocessingPassContext* preprocContext) - : PreprocessingPass(preprocContext, "miplib-trick") + : PreprocessingPass(preprocContext, "miplib-trick"), + d_statistics(statisticsRegistry()) { if (!options().base.incrementalSolving) { @@ -655,8 +656,8 @@ PreprocessingPassResult MipLibTrick::applyInternal( return PreprocessingPassResult::NO_CONFLICT; } -MipLibTrick::Statistics::Statistics() - : d_numMiplibAssertionsRemoved(smtStatisticsRegistry().registerInt( +MipLibTrick::Statistics::Statistics(StatisticsRegistry& reg) + : d_numMiplibAssertionsRemoved(reg.registerInt( "preprocessing::passes::MipLibTrick::numMiplibAssertionsRemoved")) { } diff --git a/src/preprocessing/passes/miplib_trick.h b/src/preprocessing/passes/miplib_trick.h index 537d27a0a..796063b46 100644 --- a/src/preprocessing/passes/miplib_trick.h +++ b/src/preprocessing/passes/miplib_trick.h @@ -46,7 +46,7 @@ class MipLibTrick : public PreprocessingPass, public NodeManagerListener { /** number of assertions removed by miplib pass */ IntStat d_numMiplibAssertionsRemoved; - Statistics(); + Statistics(StatisticsRegistry& reg); }; size_t removeFromConjunction( diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index 8f390a402..e380a1073 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -40,8 +40,8 @@ namespace passes { /* -------------------------------------------------------------------------- */ -NonClausalSimp::Statistics::Statistics() - : d_numConstantProps(smtStatisticsRegistry().registerInt( +NonClausalSimp::Statistics::Statistics(StatisticsRegistry& reg) + : d_numConstantProps(reg.registerInt( "preprocessing::passes::NonClausalSimp::NumConstantProps")) { } @@ -51,6 +51,7 @@ NonClausalSimp::Statistics::Statistics() NonClausalSimp::NonClausalSimp(PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "non-clausal-simp"), + d_statistics(statisticsRegistry()), d_pnm(preprocContext->getProofNodeManager()), d_llpg(d_pnm ? new smt::PreprocessProofGenerator( d_pnm, userContext(), "NonClausalSimp::llpg") diff --git a/src/preprocessing/passes/non_clausal_simp.h b/src/preprocessing/passes/non_clausal_simp.h index 329542f38..4f1c3ae7b 100644 --- a/src/preprocessing/passes/non_clausal_simp.h +++ b/src/preprocessing/passes/non_clausal_simp.h @@ -51,7 +51,7 @@ class NonClausalSimp : public PreprocessingPass struct Statistics { IntStat d_numConstantProps; - Statistics(); + Statistics(StatisticsRegistry& reg); }; Statistics d_statistics; diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index c59aa86ef..270904905 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -40,7 +40,7 @@ using namespace cvc5::theory; UnconstrainedSimplifier::UnconstrainedSimplifier( PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "unconstrained-simplifier"), - d_numUnconstrainedElim(smtStatisticsRegistry().registerInt( + d_numUnconstrainedElim(statisticsRegistry().registerInt( "preprocessor::number of unconstrained elims")), d_context(context()), d_substitutions(context()) diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp index 35c1a7fc2..758f119f5 100644 --- a/src/preprocessing/preprocessing_pass.cpp +++ b/src/preprocessing/preprocessing_pass.cpp @@ -61,7 +61,7 @@ PreprocessingPass::PreprocessingPass(PreprocessingPassContext* preprocContext, : EnvObj(preprocContext->getEnv()), d_preprocContext(preprocContext), d_name(name), - d_timer(smtStatisticsRegistry().registerTimer("preprocessing::" + name)) + d_timer(statisticsRegistry().registerTimer("preprocessing::" + name)) { } diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp index 63f09d553..897846698 100644 --- a/src/preprocessing/util/ite_utilities.cpp +++ b/src/preprocessing/util/ite_utilities.cpp @@ -292,7 +292,8 @@ ITECompressor::ITECompressor(Env& env, ContainsTermITEVisitor* contains) : EnvObj(env), d_contains(contains), d_assertions(NULL), - d_incoming(true, true) + d_incoming(true, true), + d_statistics(env.getStatisticsRegistry()) { Assert(d_contains != NULL); @@ -310,10 +311,9 @@ void ITECompressor::reset() void ITECompressor::garbageCollect() { reset(); } -ITECompressor::Statistics::Statistics() - : d_compressCalls( - smtStatisticsRegistry().registerInt("ite-simp::compressCalls")), - d_skolemsAdded(smtStatisticsRegistry().registerInt("ite-simp::skolems")) +ITECompressor::Statistics::Statistics(StatisticsRegistry& reg) + : d_compressCalls(reg.registerInt("ite-simp::compressCalls")), + d_skolemsAdded(reg.registerInt("ite-simp::skolems")) { } @@ -653,7 +653,8 @@ ITESimplifier::ITESimplifier(Env& env, ContainsTermITEVisitor* contains) d_leavesConstCache(), d_simpConstCache(), d_simpContextCache(), - d_simpITECache() + d_simpITECache(), + d_statistics(env.getStatisticsRegistry()) { Assert(d_containsVisitor != NULL); d_true = NodeManager::currentNM()->mkConst(true); @@ -702,22 +703,16 @@ bool ITESimplifier::doneALotOfWorkHeuristic() const return (d_citeEqConstApplications > SIZE_BOUND); } -ITESimplifier::Statistics::Statistics() +ITESimplifier::Statistics::Statistics(StatisticsRegistry& reg) : d_maxNonConstantsFolded( - smtStatisticsRegistry().registerInt("ite-simp::maxNonConstantsFolded")), - d_unexpected(smtStatisticsRegistry().registerInt("ite-simp::unexpected")), - d_unsimplified( - smtStatisticsRegistry().registerInt("ite-simp::unsimplified")), - d_exactMatchFold( - smtStatisticsRegistry().registerInt("ite-simp::exactMatchFold")), - d_binaryPredFold( - smtStatisticsRegistry().registerInt("ite-simp::binaryPredFold")), - d_specialEqualityFolds(smtStatisticsRegistry().registerInt( - "ite-simp::specialEqualityFolds")), - d_simpITEVisits( - smtStatisticsRegistry().registerInt("ite-simp::simpITE.visits")), - d_inSmaller(smtStatisticsRegistry().registerHistogram( - "ite-simp::inSmaller")) + reg.registerInt("ite-simp::maxNonConstantsFolded")), + d_unexpected(reg.registerInt("ite-simp::unexpected")), + d_unsimplified(reg.registerInt("ite-simp::unsimplified")), + d_exactMatchFold(reg.registerInt("ite-simp::exactMatchFold")), + d_binaryPredFold(reg.registerInt("ite-simp::binaryPredFold")), + d_specialEqualityFolds(reg.registerInt("ite-simp::specialEqualityFolds")), + d_simpITEVisits(reg.registerInt("ite-simp::simpITE.visits")), + d_inSmaller(reg.registerHistogram("ite-simp::inSmaller")) { } diff --git a/src/preprocessing/util/ite_utilities.h b/src/preprocessing/util/ite_utilities.h index 1d2aa7084..d1a93a2c2 100644 --- a/src/preprocessing/util/ite_utilities.h +++ b/src/preprocessing/util/ite_utilities.h @@ -182,7 +182,7 @@ class ITECompressor : protected EnvObj public: IntStat d_compressCalls; IntStat d_skolemsAdded; - Statistics(); + Statistics(StatisticsRegistry& reg); }; void reset(); @@ -238,7 +238,7 @@ class ITESimplifier : protected EnvObj HistogramStat d_inSmaller; - Statistics(); + Statistics(StatisticsRegistry& reg); }; inline bool containsTermITE(TNode n) diff --git a/src/smt/env.cpp b/src/smt/env.cpp index 30158799d..12e3c7520 100644 --- a/src/smt/env.cpp +++ b/src/smt/env.cpp @@ -42,7 +42,7 @@ Env::Env(NodeManager* nm, const Options* opts) d_topLevelSubs(new theory::TrustSubstitutionMap(d_userContext.get())), d_dumpManager(new DumpManager(d_userContext.get())), d_logic(), - d_statisticsRegistry(std::make_unique()), + d_statisticsRegistry(std::make_unique(*this)), d_options(), d_originalOptions(opts), d_resourceManager() diff --git a/src/smt/env_obj.cpp b/src/smt/env_obj.cpp index 32c6e4b02..fcbcc92d2 100644 --- a/src/smt/env_obj.cpp +++ b/src/smt/env_obj.cpp @@ -45,4 +45,9 @@ context::UserContext* EnvObj::userContext() const return d_env.getUserContext(); } +StatisticsRegistry& EnvObj::statisticsRegistry() const +{ + return d_env.getStatisticsRegistry(); +} + } // namespace cvc5 diff --git a/src/smt/env_obj.h b/src/smt/env_obj.h index 4b907c27b..ef9a82b17 100644 --- a/src/smt/env_obj.h +++ b/src/smt/env_obj.h @@ -29,6 +29,7 @@ class Env; class LogicInfo; class NodeManager; class Options; +class StatisticsRegistry; namespace context { class Context; @@ -67,6 +68,9 @@ class EnvObj /** Get a pointer to the UserContext via Env. */ context::UserContext* userContext() const; + /** Get the statistics registry via Env. */ + StatisticsRegistry& statisticsRegistry() const; + /** The associated environment. */ Env& d_env; }; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 9642bf394..03fb06a96 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -37,8 +37,8 @@ namespace arith { TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation) : Theory(THEORY_ARITH, env, out, valuation), - d_ppRewriteTimer(smtStatisticsRegistry().registerTimer( - "theory::arith::ppRewriteTimer")), + d_ppRewriteTimer( + statisticsRegistry().registerTimer("theory::arith::ppRewriteTimer")), d_astate(env, valuation), d_im(env, *this, d_astate, d_pnm), d_ppre(context(), d_pnm), diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 4efc4136a..e43f86743 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -171,7 +171,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, d_solveIntAttempts(0u), d_newFacts(false), d_previousStatus(Result::SAT_UNKNOWN), - d_statistics("theory::arith::") + d_statistics(statisticsRegistry(), "theory::arith::") { } @@ -260,153 +260,117 @@ TheoryArithPrivate::ModelException::ModelException(TNode n, const char* msg) } TheoryArithPrivate::ModelException::~ModelException() {} -TheoryArithPrivate::Statistics::Statistics(const std::string& name) +TheoryArithPrivate::Statistics::Statistics(StatisticsRegistry& reg, + const std::string& name) : d_statAssertUpperConflicts( - smtStatisticsRegistry().registerInt(name + "AssertUpperConflicts")), + reg.registerInt(name + "AssertUpperConflicts")), d_statAssertLowerConflicts( - smtStatisticsRegistry().registerInt(name + "AssertLowerConflicts")), - d_statUserVariables( - smtStatisticsRegistry().registerInt(name + "UserVariables")), - d_statAuxiliaryVariables( - smtStatisticsRegistry().registerInt(name + "AuxiliaryVariables")), - d_statDisequalitySplits( - smtStatisticsRegistry().registerInt(name + "DisequalitySplits")), + reg.registerInt(name + "AssertLowerConflicts")), + d_statUserVariables(reg.registerInt(name + "UserVariables")), + d_statAuxiliaryVariables(reg.registerInt(name + "AuxiliaryVariables")), + d_statDisequalitySplits(reg.registerInt(name + "DisequalitySplits")), d_statDisequalityConflicts( - smtStatisticsRegistry().registerInt(name + "DisequalityConflicts")), - d_simplifyTimer( - smtStatisticsRegistry().registerTimer(name + "simplifyTimer")), - d_staticLearningTimer( - smtStatisticsRegistry().registerTimer(name + "staticLearningTimer")), - d_presolveTime( - smtStatisticsRegistry().registerTimer(name + "presolveTime")), - d_newPropTime( - smtStatisticsRegistry().registerTimer(name + "newPropTimer")), - d_externalBranchAndBounds(smtStatisticsRegistry().registerInt( - name + "externalBranchAndBounds")), - d_initialTableauSize( - smtStatisticsRegistry().registerInt(name + "initialTableauSize")), - d_currSetToSmaller( - smtStatisticsRegistry().registerInt(name + "currSetToSmaller")), - d_smallerSetToCurr( - smtStatisticsRegistry().registerInt(name + "smallerSetToCurr")), - d_restartTimer( - smtStatisticsRegistry().registerTimer(name + "restartTimer")), - d_boundComputationTime( - smtStatisticsRegistry().registerTimer(name + "bound::time")), - d_boundComputations(smtStatisticsRegistry().registerInt( - name + "bound::boundComputations")), - d_boundPropagations(smtStatisticsRegistry().registerInt( - name + "bound::boundPropagations")), - d_unknownChecks( - smtStatisticsRegistry().registerInt(name + "status::unknowns")), - d_maxUnknownsInARow(smtStatisticsRegistry().registerInt( - name + "status::maxUnknownsInARow")), - d_avgUnknownsInARow(smtStatisticsRegistry().registerAverage( - name + "status::avgUnknownsInARow")), - d_revertsOnConflicts(smtStatisticsRegistry().registerInt( - name + "status::revertsOnConflicts")), - d_commitsOnConflicts(smtStatisticsRegistry().registerInt( - name + "status::commitsOnConflicts")), - d_nontrivialSatChecks(smtStatisticsRegistry().registerInt( - name + "status::nontrivialSatChecks")), - d_replayLogRecCount( - smtStatisticsRegistry().registerInt(name + "z::approx::replay::rec")), - d_replayLogRecConflictEscalation(smtStatisticsRegistry().registerInt( - name + "z::approx::replay::rec::escalation")), - d_replayLogRecEarlyExit(smtStatisticsRegistry().registerInt( - name + "z::approx::replay::rec::earlyexit")), - d_replayBranchCloseFailures(smtStatisticsRegistry().registerInt( + reg.registerInt(name + "DisequalityConflicts")), + d_simplifyTimer(reg.registerTimer(name + "simplifyTimer")), + d_staticLearningTimer(reg.registerTimer(name + "staticLearningTimer")), + d_presolveTime(reg.registerTimer(name + "presolveTime")), + d_newPropTime(reg.registerTimer(name + "newPropTimer")), + d_externalBranchAndBounds( + reg.registerInt(name + "externalBranchAndBounds")), + d_initialTableauSize(reg.registerInt(name + "initialTableauSize")), + d_currSetToSmaller(reg.registerInt(name + "currSetToSmaller")), + d_smallerSetToCurr(reg.registerInt(name + "smallerSetToCurr")), + d_restartTimer(reg.registerTimer(name + "restartTimer")), + d_boundComputationTime(reg.registerTimer(name + "bound::time")), + d_boundComputations(reg.registerInt(name + "bound::boundComputations")), + d_boundPropagations(reg.registerInt(name + "bound::boundPropagations")), + d_unknownChecks(reg.registerInt(name + "status::unknowns")), + d_maxUnknownsInARow(reg.registerInt(name + "status::maxUnknownsInARow")), + d_avgUnknownsInARow( + reg.registerAverage(name + "status::avgUnknownsInARow")), + d_revertsOnConflicts( + reg.registerInt(name + "status::revertsOnConflicts")), + d_commitsOnConflicts( + reg.registerInt(name + "status::commitsOnConflicts")), + d_nontrivialSatChecks( + reg.registerInt(name + "status::nontrivialSatChecks")), + d_replayLogRecCount(reg.registerInt(name + "z::approx::replay::rec")), + d_replayLogRecConflictEscalation( + reg.registerInt(name + "z::approx::replay::rec::escalation")), + d_replayLogRecEarlyExit( + reg.registerInt(name + "z::approx::replay::rec::earlyexit")), + d_replayBranchCloseFailures(reg.registerInt( name + "z::approx::replay::rec::branch::closefailures")), - d_replayLeafCloseFailures(smtStatisticsRegistry().registerInt( + d_replayLeafCloseFailures(reg.registerInt( name + "z::approx::replay::rec::leaf::closefailures")), - d_replayBranchSkips(smtStatisticsRegistry().registerInt( - name + "z::approx::replay::rec::branch::skips")), - d_mirCutsAttempted(smtStatisticsRegistry().registerInt( - name + "z::approx::cuts::mir::attempted")), - d_gmiCutsAttempted(smtStatisticsRegistry().registerInt( - name + "z::approx::cuts::gmi::attempted")), - d_branchCutsAttempted(smtStatisticsRegistry().registerInt( - name + "z::approx::cuts::branch::attempted")), - d_cutsReconstructed(smtStatisticsRegistry().registerInt( - name + "z::approx::cuts::reconstructed")), - d_cutsReconstructionFailed(smtStatisticsRegistry().registerInt( - name + "z::approx::cuts::reconstructed::failed")), - d_cutsProven(smtStatisticsRegistry().registerInt( - name + "z::approx::cuts::proofs")), - d_cutsProofFailed(smtStatisticsRegistry().registerInt( - name + "z::approx::cuts::proofs::failed")), - d_mipReplayLemmaCalls(smtStatisticsRegistry().registerInt( - name + "z::approx::external::calls")), - d_mipExternalCuts(smtStatisticsRegistry().registerInt( - name + "z::approx::external::cuts")), - d_mipExternalBranch(smtStatisticsRegistry().registerInt( - name + "z::approx::external::branches")), - d_inSolveInteger(smtStatisticsRegistry().registerInt( - name + "z::approx::inSolverInteger")), - d_branchesExhausted(smtStatisticsRegistry().registerInt( - name + "z::approx::exhausted::branches")), - d_execExhausted(smtStatisticsRegistry().registerInt( - name + "z::approx::exhausted::exec")), - d_pivotsExhausted(smtStatisticsRegistry().registerInt( - name + "z::approx::exhausted::pivots")), - d_panicBranches( - smtStatisticsRegistry().registerInt(name + "z::arith::paniclemmas")), - d_relaxCalls( - smtStatisticsRegistry().registerInt(name + "z::arith::relax::calls")), - d_relaxLinFeas(smtStatisticsRegistry().registerInt( - name + "z::arith::relax::feasible::res")), - d_relaxLinFeasFailures(smtStatisticsRegistry().registerInt( - name + "z::arith::relax::feasible::failures")), - d_relaxLinInfeas(smtStatisticsRegistry().registerInt( - name + "z::arith::relax::infeasible")), - d_relaxLinInfeasFailures(smtStatisticsRegistry().registerInt( - name + "z::arith::relax::infeasible::failures")), - d_relaxLinExhausted(smtStatisticsRegistry().registerInt( - name + "z::arith::relax::exhausted")), - d_relaxOthers( - smtStatisticsRegistry().registerInt(name + "z::arith::relax::other")), - d_applyRowsDeleted(smtStatisticsRegistry().registerInt( - name + "z::arith::cuts::applyRowsDeleted")), - d_replaySimplexTimer(smtStatisticsRegistry().registerTimer( - name + "z::approx::replay::simplex::timer")), - d_replayLogTimer(smtStatisticsRegistry().registerTimer( - name + "z::approx::replay::log::timer")), - d_solveIntTimer( - smtStatisticsRegistry().registerTimer(name + "z::solveInt::timer")), - d_solveRealRelaxTimer(smtStatisticsRegistry().registerTimer( - name + "z::solveRealRelax::timer")), - d_solveIntCalls( - smtStatisticsRegistry().registerInt(name + "z::solveInt::calls")), - d_solveStandardEffort(smtStatisticsRegistry().registerInt( - name + "z::solveInt::calls::standardEffort")), - d_approxDisabled( - smtStatisticsRegistry().registerInt(name + "z::approxDisabled")), - d_replayAttemptFailed( - smtStatisticsRegistry().registerInt(name + "z::replayAttemptFailed")), - d_cutsRejectedDuringReplay(smtStatisticsRegistry().registerInt( - name + "z::approx::replay::cuts::rejected")), - d_cutsRejectedDuringLemmas(smtStatisticsRegistry().registerInt( - name + "z::approx::external::cuts::rejected")), - d_satPivots(smtStatisticsRegistry().registerHistogram( - name + "pivots::sat")), - d_unsatPivots(smtStatisticsRegistry().registerHistogram( - name + "pivots::unsat")), - d_unknownPivots(smtStatisticsRegistry().registerHistogram( - name + "pivots::unknown")), - d_solveIntModelsAttempts(smtStatisticsRegistry().registerInt( - name + "z::solveInt::models::attempts")), - d_solveIntModelsSuccessful(smtStatisticsRegistry().registerInt( - name + "zzz::solveInt::models::successful")), - d_mipTimer(smtStatisticsRegistry().registerTimer( - name + "z::approx::mip::timer")), - d_lpTimer( - smtStatisticsRegistry().registerTimer(name + "z::approx::lp::timer")), - d_mipProofsAttempted(smtStatisticsRegistry().registerInt( - name + "z::mip::proofs::attempted")), - d_mipProofsSuccessful(smtStatisticsRegistry().registerInt( - name + "z::mip::proofs::successful")), - d_numBranchesFailed(smtStatisticsRegistry().registerInt( - name + "z::mip::branch::proof::failed")) + d_replayBranchSkips( + reg.registerInt(name + "z::approx::replay::rec::branch::skips")), + d_mirCutsAttempted( + reg.registerInt(name + "z::approx::cuts::mir::attempted")), + d_gmiCutsAttempted( + reg.registerInt(name + "z::approx::cuts::gmi::attempted")), + d_branchCutsAttempted( + reg.registerInt(name + "z::approx::cuts::branch::attempted")), + d_cutsReconstructed( + reg.registerInt(name + "z::approx::cuts::reconstructed")), + d_cutsReconstructionFailed( + reg.registerInt(name + "z::approx::cuts::reconstructed::failed")), + d_cutsProven(reg.registerInt(name + "z::approx::cuts::proofs")), + d_cutsProofFailed( + reg.registerInt(name + "z::approx::cuts::proofs::failed")), + d_mipReplayLemmaCalls( + reg.registerInt(name + "z::approx::external::calls")), + d_mipExternalCuts(reg.registerInt(name + "z::approx::external::cuts")), + d_mipExternalBranch( + reg.registerInt(name + "z::approx::external::branches")), + d_inSolveInteger(reg.registerInt(name + "z::approx::inSolverInteger")), + d_branchesExhausted( + reg.registerInt(name + "z::approx::exhausted::branches")), + d_execExhausted(reg.registerInt(name + "z::approx::exhausted::exec")), + d_pivotsExhausted(reg.registerInt(name + "z::approx::exhausted::pivots")), + d_panicBranches(reg.registerInt(name + "z::arith::paniclemmas")), + d_relaxCalls(reg.registerInt(name + "z::arith::relax::calls")), + d_relaxLinFeas(reg.registerInt(name + "z::arith::relax::feasible::res")), + d_relaxLinFeasFailures( + reg.registerInt(name + "z::arith::relax::feasible::failures")), + d_relaxLinInfeas(reg.registerInt(name + "z::arith::relax::infeasible")), + d_relaxLinInfeasFailures( + reg.registerInt(name + "z::arith::relax::infeasible::failures")), + d_relaxLinExhausted(reg.registerInt(name + "z::arith::relax::exhausted")), + d_relaxOthers(reg.registerInt(name + "z::arith::relax::other")), + d_applyRowsDeleted( + reg.registerInt(name + "z::arith::cuts::applyRowsDeleted")), + d_replaySimplexTimer( + reg.registerTimer(name + "z::approx::replay::simplex::timer")), + d_replayLogTimer( + reg.registerTimer(name + "z::approx::replay::log::timer")), + d_solveIntTimer(reg.registerTimer(name + "z::solveInt::timer")), + d_solveRealRelaxTimer( + reg.registerTimer(name + "z::solveRealRelax::timer")), + d_solveIntCalls(reg.registerInt(name + "z::solveInt::calls")), + d_solveStandardEffort( + reg.registerInt(name + "z::solveInt::calls::standardEffort")), + d_approxDisabled(reg.registerInt(name + "z::approxDisabled")), + d_replayAttemptFailed(reg.registerInt(name + "z::replayAttemptFailed")), + d_cutsRejectedDuringReplay( + reg.registerInt(name + "z::approx::replay::cuts::rejected")), + d_cutsRejectedDuringLemmas( + reg.registerInt(name + "z::approx::external::cuts::rejected")), + d_satPivots(reg.registerHistogram(name + "pivots::sat")), + d_unsatPivots(reg.registerHistogram(name + "pivots::unsat")), + d_unknownPivots( + reg.registerHistogram(name + "pivots::unknown")), + d_solveIntModelsAttempts( + reg.registerInt(name + "z::solveInt::models::attempts")), + d_solveIntModelsSuccessful( + reg.registerInt(name + "zzz::solveInt::models::successful")), + d_mipTimer(reg.registerTimer(name + "z::approx::mip::timer")), + d_lpTimer(reg.registerTimer(name + "z::approx::lp::timer")), + d_mipProofsAttempted(reg.registerInt(name + "z::mip::proofs::attempted")), + d_mipProofsSuccessful( + reg.registerInt(name + "z::mip::proofs::successful")), + d_numBranchesFailed( + reg.registerInt(name + "z::mip::branch::proof::failed")) { } diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 173579cef..221c0a781 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -867,7 +867,7 @@ private: IntStat d_numBranchesFailed; - Statistics(const std::string& name); + Statistics(StatisticsRegistry& reg, const std::string& name); }; diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index c24290b6e..c975fbbfa 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -60,25 +60,23 @@ TheoryArrays::TheoryArrays(Env& env, Valuation valuation, std::string name) : Theory(THEORY_ARRAYS, env, out, valuation, name), - d_numRow( - smtStatisticsRegistry().registerInt(name + "number of Row lemmas")), - d_numExt( - smtStatisticsRegistry().registerInt(name + "number of Ext lemmas")), + d_numRow(statisticsRegistry().registerInt(name + "number of Row lemmas")), + d_numExt(statisticsRegistry().registerInt(name + "number of Ext lemmas")), d_numProp( - smtStatisticsRegistry().registerInt(name + "number of propagations")), + statisticsRegistry().registerInt(name + "number of propagations")), d_numExplain( - smtStatisticsRegistry().registerInt(name + "number of explanations")), - d_numNonLinear(smtStatisticsRegistry().registerInt( + statisticsRegistry().registerInt(name + "number of explanations")), + d_numNonLinear(statisticsRegistry().registerInt( name + "number of calls to setNonLinear")), - d_numSharedArrayVarSplits(smtStatisticsRegistry().registerInt( + d_numSharedArrayVarSplits(statisticsRegistry().registerInt( name + "number of shared array var splits")), - d_numGetModelValSplits(smtStatisticsRegistry().registerInt( + d_numGetModelValSplits(statisticsRegistry().registerInt( name + "number of getModelVal splits")), - d_numGetModelValConflicts(smtStatisticsRegistry().registerInt( + d_numGetModelValConflicts(statisticsRegistry().registerInt( name + "number of getModelVal conflicts")), - d_numSetModelValSplits(smtStatisticsRegistry().registerInt( + d_numSetModelValSplits(statisticsRegistry().registerInt( name + "number of setModelVal splits")), - d_numSetModelValConflicts(smtStatisticsRegistry().registerInt( + d_numSetModelValConflicts(statisticsRegistry().registerInt( name + "number of setModelVal conflicts")), d_ppEqualityEngine(userContext(), name + "pp", true), d_ppFacts(userContext()), diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 96eccea57..397120ff1 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -41,7 +41,7 @@ TheoryBV::TheoryBV(Env& env, d_im(env, *this, d_state, nullptr, "theory::bv::"), d_notify(d_im), d_invalidateModelCache(context(), true), - d_stats("theory::bv::") + d_stats(statisticsRegistry(), "theory::bv::") { switch (options().bv.bvSolver) { @@ -402,9 +402,9 @@ Node TheoryBV::getValue(TNode node) return it->second; } -TheoryBV::Statistics::Statistics(const std::string& name) - : d_solveSubstitutions( - smtStatisticsRegistry().registerInt(name + "NumSolveSubstitutions")) +TheoryBV::Statistics::Statistics(StatisticsRegistry& reg, + const std::string& name) + : d_solveSubstitutions(reg.registerInt(name + "NumSolveSubstitutions")) { } diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index b4afb5f5d..0249fe890 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -137,7 +137,7 @@ class TheoryBV : public Theory /** TheoryBV statistics. */ struct Statistics { - Statistics(const std::string& name); + Statistics(StatisticsRegistry& reg, const std::string& name); IntStat d_solveSubstitutions; } d_stats; diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 44b3da53e..415672e97 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -71,9 +71,9 @@ Theory::Theory(TheoryId id, d_sharedTermsIndex(d_env.getContext(), 0), d_careGraph(nullptr), d_instanceName(name), - d_checkTime(smtStatisticsRegistry().registerTimer(getStatsPrefix(id) - + name + "checkTime")), - d_computeCareGraphTime(smtStatisticsRegistry().registerTimer( + d_checkTime(statisticsRegistry().registerTimer(getStatsPrefix(id) + name + + "checkTime")), + d_computeCareGraphTime(statisticsRegistry().registerTimer( getStatsPrefix(id) + name + "computeCareGraphTime")), d_sharedTerms(d_env.getContext()), d_out(&out), diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index e2789a5b5..be4b7dd76 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -242,7 +242,7 @@ TheoryEngine::TheoryEngine(Env& env) d_propagatedLiterals(context()), d_propagatedLiteralsIndex(context(), 0), d_atomRequests(context()), - d_combineTheoriesTime(smtStatisticsRegistry().registerTimer( + d_combineTheoriesTime(statisticsRegistry().registerTimer( "TheoryEngine::combineTheoriesTime")), d_true(), d_false(), diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index f83d92158..08d713b0f 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -49,11 +49,11 @@ TheoryInferenceManager::TheoryInferenceManager(Env& env, d_numConflicts(0), d_numCurrentLemmas(0), d_numCurrentFacts(0), - d_conflictIdStats(smtStatisticsRegistry().registerHistogram( + d_conflictIdStats(statisticsRegistry().registerHistogram( statsName + "inferencesConflict")), - d_factIdStats(smtStatisticsRegistry().registerHistogram( + d_factIdStats(statisticsRegistry().registerHistogram( statsName + "inferencesFact")), - d_lemmaIdStats(smtStatisticsRegistry().registerHistogram( + d_lemmaIdStats(statisticsRegistry().registerHistogram( statsName + "inferencesLemma")) { // don't add true lemma diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp index 51da36aba..815c61059 100644 --- a/src/util/statistics_registry.cpp +++ b/src/util/statistics_registry.cpp @@ -22,7 +22,8 @@ namespace cvc5 { -StatisticsRegistry::StatisticsRegistry(bool registerPublic) +StatisticsRegistry::StatisticsRegistry(Env& env, bool registerPublic) + : EnvObj(env) { if (registerPublic) { @@ -52,8 +53,8 @@ void StatisticsRegistry::storeSnapshot() d_lastSnapshot = std::make_unique(); for (const auto& s : d_stats) { - if (!options::statisticsExpert() && s.second->d_expert) continue; - if (!options::statisticsAll() && s.second->isDefault()) continue; + if (!options().base.statisticsExpert && s.second->d_expert) continue; + if (!options().base.statisticsAll && s.second->isDefault()) continue; d_lastSnapshot->emplace( s.first, s.second->getViewer()); @@ -78,8 +79,8 @@ void StatisticsRegistry::print(std::ostream& os) const { for (const auto& s : d_stats) { - if (!options::statisticsExpert() && s.second->d_expert) continue; - if (!options::statisticsAll() && s.second->isDefault()) continue; + if (!options().base.statisticsExpert && s.second->d_expert) continue; + if (!options().base.statisticsAll && s.second->isDefault()) continue; os << s.first << " = " << *s.second << std::endl; } } @@ -91,8 +92,8 @@ void StatisticsRegistry::printSafe(int fd) const { for (const auto& s : d_stats) { - if (!options::statisticsExpert() && s.second->d_expert) continue; - if (!options::statisticsAll() && s.second->isDefault()) continue; + if (!options().base.statisticsExpert && s.second->d_expert) continue; + if (!options().base.statisticsAll && s.second->isDefault()) continue; safe_print(fd, s.first); safe_print(fd, " = "); @@ -113,8 +114,8 @@ void StatisticsRegistry::printDiff(std::ostream& os) const } for (const auto& s : d_stats) { - if (!options::statisticsExpert() && s.second->d_expert) continue; - if (!options::statisticsAll() && s.second->isDefault()) + if (!options().base.statisticsExpert && s.second->d_expert) continue; + if (!options().base.statisticsAll && s.second->isDefault()) { auto oldit = d_lastSnapshot->find(s.first); if (oldit != d_lastSnapshot->end() && oldit->second != s.second->getViewer()) diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index 7a714012e..923880dbf 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -74,6 +74,7 @@ #include #include "base/check.h" +#include "smt/env_obj.h" #include "util/statistics_stats.h" #include "util/statistics_value.h" @@ -111,7 +112,7 @@ struct StatisticBaseValue; * However, no data is stored in the registry and the modification functions * of the proxy objects do nothing. */ -class StatisticsRegistry +class StatisticsRegistry : protected EnvObj { public: friend std::ostream& operator<<(std::ostream& os, @@ -124,7 +125,7 @@ class StatisticsRegistry * pre-registered as such. This argument mostly exists so that unit tests * can disable this pre-registration. */ - StatisticsRegistry(bool registerPublic = true); + StatisticsRegistry(Env& env, bool registerPublic = true); /** Register a new running average statistic for `name` */ diff --git a/test/unit/test_env.h b/test/unit/test_env.h new file mode 100644 index 000000000..a0c7c68c3 --- /dev/null +++ b/test/unit/test_env.h @@ -0,0 +1,48 @@ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Common header for unit tests involving env. + */ + +#ifndef CVC5__TEST__UNIT__TEST_NODE_H +#define CVC5__TEST__UNIT__TEST_NODE_H + +#include "expr/node_manager.h" +#include "expr/skolem_manager.h" +#include "options/options.h" +#include "smt/env.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" +#include "test.h" + +namespace cvc5 { +namespace test { + +class TestEnv : public TestInternal +{ + protected: + void SetUp() override + { + d_options.reset(new Options()); + d_nodeManager.reset(new NodeManager()); + d_env.reset(new Env(d_nodeManager.get(), d_options.get())); + } + + + std::unique_ptr d_options; + std::unique_ptr d_nodeManager; + std::unique_ptr d_env; +}; + +} // namespace test +} // namespace cvc5 +#endif diff --git a/test/unit/util/stats_black.cpp b/test/unit/util/stats_black.cpp index 669857e96..03610d9ce 100644 --- a/test/unit/util/stats_black.cpp +++ b/test/unit/util/stats_black.cpp @@ -22,7 +22,7 @@ #include "lib/clock_gettime.h" #include "proof/proof_rule.h" -#include "test.h" +#include "test_env.h" #include "util/statistics_registry.h" #include "util/statistics_stats.h" @@ -41,14 +41,14 @@ bool operator==(const StatisticBaseValue* sbv, const std::string& s) namespace test { -class TestUtilBlackStats : public TestInternal +class TestUtilBlackStats : public TestEnv { }; TEST_F(TestUtilBlackStats, stats) { #ifdef CVC5_STATISTICS_ON - StatisticsRegistry reg(false); + StatisticsRegistry reg(*d_env.get(), false); std::string empty, bar = "bar", baz = "baz"; AverageStat avg = reg.registerAverage("avg"); -- 2.30.2