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.

diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp
index 206f12a3fe0e3740ebc38c074f9e0cef48518e68..90b55a48a94ad39a6a8dbcc542eb0899e671fe67 100644 (file)
--- 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 0bef7c6b5222f286c3f69155334be2d217ba4596..06c4dd1c197e9fd950e948c908fc9be422aff3f6 100644 (file)
--- 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 0d0131e3e6813e1f65a9ae9d29036f683e56790d..ca48c1a37fc2f38752dd373ba30adbd2f44e60f9 100644 (file)
--- 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<Node>& 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 d34f2f77f6984a65d72c2dae2308c719bcb69a3a..cca79c9008b75634e0498481358bcc1112367e95 100644 (file)
--- 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 5f9b4fb1d8f2962c76c9a6d06c3363077e3fd3c7..e951b9cb00492d06bb0a635a873b91625353e4bf 100644 (file)
--- 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 ca8547d469c525da5bbf5720a3360616365038a1..183cec946af276c4fae8f00b171c3dd7ebb5261d 100644 (file)
--- 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 c2693e927a1a4f7eac897325cef6660b28c74395..81f5718cf4e8d5b4bea120424f1c626fc78fb437 100644 (file)
--- 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<LearnedRewriteId>(
+      d_lrewCount(statisticsRegistry().registerHistogram<LearnedRewriteId>(
           "LearnedRewrite::lrewCount"))
 {
 }

diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index c40a65bc1e8db0b607f68bbd8c7590999ec4d84c..8202acb15f15b4afe5c566f33ed82322806091fe 100644 (file)
--- 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 537d27a0af2bf5364c40fc8688dca6a005faf4c7..796063b4620299c1cac7da7b46397eb1a0c89ae7 100644 (file)
--- 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 8f390a40261fa89e2eb47bfeced243d189e84f92..e380a107396c3b993e2fa00aae3567ffee50d6f5 100644 (file)
--- 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 329542f383326af14ef312a9bb9ccc29aaf27cc7..4f1c3ae7b56485896ca482a5968a42e003549d59 100644 (file)
--- 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 c59aa86ef01f5ba244d7fd60c15b586309252212..270904905b07f593f3aabe482a70f33eec233bb1 100644 (file)
--- 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 35c1a7fc20b2d85c4db0b0e13cd992b82ea7931d..758f119f538270c560a01d711be94ece9f40a93e 100644 (file)
--- 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 63f09d5537fb701da2cd66e6a94a8446d40602a9..8978466984b09e55882d82cfa0f73ff0e3c041ba 100644 (file)
--- 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<bool>(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<uint32_t>(
-          "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<uint32_t>("ite-simp::inSmaller"))
 {
 }
 

diff --git a/src/preprocessing/util/ite_utilities.h b/src/preprocessing/util/ite_utilities.h
index 1d2aa70848d78deca11ad3989b28bcec20e41088..d1a93a2c237d3b87ea0fe4d6e03dafb31c7f916c 100644 (file)
--- 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<uint32_t> d_inSmaller;
 
-    Statistics();
+    Statistics(StatisticsRegistry& reg);
   };
 
   inline bool containsTermITE(TNode n)

diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index 30158799d58f2b5b9db10c75788fb56a02b9559c..12e3c7520dc166085e296dc243e2d33e247611b4 100644 (file)
--- 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<StatisticsRegistry>()),
+      d_statisticsRegistry(std::make_unique<StatisticsRegistry>(*this)),
       d_options(),
       d_originalOptions(opts),
       d_resourceManager()

diff --git a/src/smt/env_obj.cpp b/src/smt/env_obj.cpp
index 32c6e4b027bb08d0801477d0399d0b807633fca7..fcbcc92d2b1099c5721594112e5ef5755047f5a8 100644 (file)
--- 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 4b907c27b10f32431e7159cdd0e698d5699f852b..ef9a82b17f2483259654529bc3ab3997287663d3 100644 (file)
--- 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 9642bf394edd280fd03e9a1df87a10e5224b9f36..03fb06a965e2b28fcc158e7fc7780840c5010e86 100644 (file)
--- 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 4efc4136a13ae0dc396c8c605edb0f5c02b89af0..e43f86743dfa4525698cff7f0ee5644fbb0a8154 100644 (file)
--- 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<uint32_t>(
-          name + "pivots::sat")),
-      d_unsatPivots(smtStatisticsRegistry().registerHistogram<uint32_t>(
-          name + "pivots::unsat")),
-      d_unknownPivots(smtStatisticsRegistry().registerHistogram<uint32_t>(
-          name + "pivots::unknown")),
-      d_solveIntModelsAttempts(smtStatisticsRegistry().registerInt(
-          name + "z::solveInt::models::attempts")),
-      d_solveIntModelsSuccessful(smtStatisticsRegistry().registerInt(
-          name + "zzz::solveInt::models::successful")),
-      d_mipTimer(smtStatisticsRegistry().registerTimer(
-          name + "z::approx::mip::timer")),
-      d_lpTimer(
-          smtStatisticsRegistry().registerTimer(name + "z::approx::lp::timer")),
-      d_mipProofsAttempted(smtStatisticsRegistry().registerInt(
-          name + "z::mip::proofs::attempted")),
-      d_mipProofsSuccessful(smtStatisticsRegistry().registerInt(
-          name + "z::mip::proofs::successful")),
-      d_numBranchesFailed(smtStatisticsRegistry().registerInt(
-          name + "z::mip::branch::proof::failed"))
+      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<uint32_t>(name + "pivots::sat")),
+      d_unsatPivots(reg.registerHistogram<uint32_t>(name + "pivots::unsat")),
+      d_unknownPivots(
+          reg.registerHistogram<uint32_t>(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 173579ceff0965f66b14fbf4ffd603a5e4ce570c..221c0a781532ddeea51291264352e09e720047c1 100644 (file)
--- 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 c24290b6edcbbe387c4e5813b7a228b2fe6e567c..c975fbbfac872f429715fbb3533f37282f4e32a5 100644 (file)
--- 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 96eccea57705ce2916648bd64e22fb83caedff4d..397120ff1f89f825774274e0e70248a2469dba24 100644 (file)
--- 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 b4afb5f5de41362b91dac61e215b463bc3cadbd1..0249fe8901f2bd7e4ec04543c2ed77a88e6a2202 100644 (file)
--- 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 44b3da53ef1b8d0d4c610898d24578d889363d23..415672e9742647aab7a9c8493cd29928b1052fa0 100644 (file)
--- 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 e2789a5b51bfb46e918814e6ff0c2fc9c3dc1b32..be4b7dd7659da224811973fbfc24ef2b75bb68c3 100644 (file)
--- 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 f83d92158ed8e6b4af427ae891000150c9ff4fc4..08d713b0f19f57d9b9c453537f0f2f901648db35 100644 (file)
--- 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<InferenceId>(
+      d_conflictIdStats(statisticsRegistry().registerHistogram<InferenceId>(
           statsName + "inferencesConflict")),
-      d_factIdStats(smtStatisticsRegistry().registerHistogram<InferenceId>(
+      d_factIdStats(statisticsRegistry().registerHistogram<InferenceId>(
           statsName + "inferencesFact")),
-      d_lemmaIdStats(smtStatisticsRegistry().registerHistogram<InferenceId>(
+      d_lemmaIdStats(statisticsRegistry().registerHistogram<InferenceId>(
           statsName + "inferencesLemma"))
 {
   // don't add true lemma

diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp
index 51da36aba6d49b3ea1daeece3fa473bf2ab0e9e7..815c61059beee8fcd37f34bd08ee1ee17ad21565 100644 (file)
--- 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<Snapshot>();
     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 7a714012e4bef397682bf5ef560f6c9e38320b78..923880dbf181a0f4e2cb50daf63ffb7b59e4e1ea 100644 (file)
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -74,6 +74,7 @@
 #include <typeinfo>
 
 #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 (file)
index 0000000..a0c7c68
--- /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<Options> d_options;
+  std::unique_ptr<NodeManager> d_nodeManager;
+  std::unique_ptr<Env> d_env;
+};
+
+}  // namespace test
+}  // namespace cvc5
+#endif

diff --git a/test/unit/util/stats_black.cpp b/test/unit/util/stats_black.cpp
index 669857e96168b7228da2505e325a5a80bbb64773..03610d9cef6fa8ee2d11edd07186a3bf8e87bc24 100644 (file)
--- 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");