From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Thu, 18 Mar 2021 21:27:35 +0000 (+0100)
Subject: Move stats registry to env. (#6173)
X-Git-Tag: cvc5-1.0.0~2056
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d2a155a8c780cd1ef52db884db1e4e4df2cf76b7;p=cvc5.git

Move stats registry to env. (#6173)

This PR moves the statistics registry from SmtEngine to Env.
---

diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index 0b6607c35..55afcadf7 100644
--- a/src/smt/env.cpp
+++ b/src/smt/env.cpp
@@ -37,8 +37,8 @@ Env::Env(NodeManager* nm)
       d_rewriter(new theory::Rewriter()),
       d_dumpManager(new DumpManager(d_userContext.get())),
       d_logic(),
-      d_statisticsRegistry(nullptr),
-      d_resourceManager(nullptr)
+      d_statisticsRegistry(std::make_unique<StatisticsRegistry>()),
+      d_resourceManager(std::make_unique<ResourceManager>(*d_statisticsRegistry, d_options))
 {
 }
 
@@ -54,13 +54,6 @@ void Env::setOptions(Options* optr)
   }
 }
 
-void Env::setStatisticsRegistry(StatisticsRegistry* statReg)
-{
-  d_statisticsRegistry = statReg;
-  // now initialize resource manager
-  d_resourceManager.reset(new ResourceManager(*statReg, d_options));
-}
-
 void Env::setProofNodeManager(ProofNodeManager* pnm)
 {
   d_proofNodeManager = pnm;
@@ -91,7 +84,7 @@ const LogicInfo& Env::getLogicInfo() const { return d_logic; }
 
 StatisticsRegistry* Env::getStatisticsRegistry()
 {
-  return d_statisticsRegistry;
+  return d_statisticsRegistry.get();
 }
 
 const Options& Env::getOptions() const { return d_options; }
diff --git a/src/smt/env.h b/src/smt/env.h
index c777a7755..18f0de0b5 100644
--- a/src/smt/env.h
+++ b/src/smt/env.h
@@ -23,6 +23,7 @@
 #include "options/options.h"
 #include "theory/logic_info.h"
 #include "util/statistics.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 
@@ -164,9 +165,9 @@ class Env
    */
   LogicInfo d_logic;
   /**
-   * The statistics registry, which is owned by the SmtEngine that owns this.
+   * The statistics registry owned by this Env.
    */
-  StatisticsRegistry* d_statisticsRegistry;
+  std::unique_ptr<StatisticsRegistry> d_statisticsRegistry;
   /**
    * The options object, which contains the modified version of the options
    * provided as input to the SmtEngine that owns this environment. Note
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3493aae11..4436666a7 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -123,11 +123,6 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr)
   // Set options in the environment, which makes a deep copy of optr if
   // non-null. This may throw an options exception.
   d_env->setOptions(optr);
-  // now construct the statistics registry
-  d_statisticsRegistry.reset(new StatisticsRegistry());
-  // initialize the environment, which keeps a pointer to statistics registry
-  // and sets up resource manager
-  d_env->setStatisticsRegistry(d_statisticsRegistry.get());
   // set the options manager
   d_optm.reset(new smt::OptionsManager(&getOptions(), getResourceManager()));
   // listen to node manager events
@@ -357,7 +352,6 @@ SmtEngine::~SmtEngine()
     d_routListener.reset(nullptr);
     d_optm.reset(nullptr);
     d_pp.reset(nullptr);
-    d_statisticsRegistry.reset(nullptr);
     // destroy the state
     d_state.reset(nullptr);
     // destroy the environment
@@ -522,8 +516,8 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
       v.push_back((*i).second);
       stats.push_back(v);
     }
-    for (StatisticsRegistry::const_iterator i = d_statisticsRegistry->begin();
-         i != d_statisticsRegistry->end();
+    for (StatisticsRegistry::const_iterator i = d_env->getStatisticsRegistry()->begin();
+         i != d_env->getStatisticsRegistry()->end();
          ++i)
     {
       vector<SExpr> v;
@@ -1406,7 +1400,7 @@ void SmtEngine::checkProof()
 
 StatisticsRegistry* SmtEngine::getStatisticsRegistry()
 {
-  return d_statisticsRegistry.get();
+  return d_env->getStatisticsRegistry();
 }
 
 UnsatCore SmtEngine::getUnsatCoreInternal()
@@ -1891,24 +1885,24 @@ NodeManager* SmtEngine::getNodeManager() const
 
 Statistics SmtEngine::getStatistics() const
 {
-  return Statistics(*d_statisticsRegistry);
+  return Statistics(*d_env->getStatisticsRegistry());
 }
 
 SExpr SmtEngine::getStatistic(std::string name) const
 {
-  return d_statisticsRegistry->getStatistic(name);
+  return d_env->getStatisticsRegistry()->getStatistic(name);
 }
 
 void SmtEngine::flushStatistics(std::ostream& out) const
 {
   getNodeManager()->getStatisticsRegistry()->flushInformation(out);
-  d_statisticsRegistry->flushInformation(out);
+  d_env->getStatisticsRegistry()->flushInformation(out);
 }
 
 void SmtEngine::safeFlushStatistics(int fd) const
 {
   getNodeManager()->getStatisticsRegistry()->safeFlushInformation(fd);
-  d_statisticsRegistry->safeFlushInformation(fd);
+  d_env->getStatisticsRegistry()->safeFlushInformation(fd);
 }
 
 void SmtEngine::setUserAttribute(const std::string& attr,
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index dd0fe3a6e..16434d6d7 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -1053,12 +1053,6 @@ class CVC4_EXPORT SmtEngine
   /** Solver instance that owns this SmtEngine instance. */
   api::Solver* d_solver = nullptr;
 
-  /**
-   * The statistics registry. Notice that this definition must be before the
-   * other members since it must be destroyed last if exceptions occur in the
-   * constructor of SmtEngine.
-   */
-  std::unique_ptr<StatisticsRegistry> d_statisticsRegistry;
   /**
    * The environment object, which contains all utilities that are globally
    * available to internal code.