Move statistics from the driver into the SmtEngine (#6170)

This PR does some refactoring on how we handle statistics in the driver, and some minor cleanup along the way.

    The SmtEngine now has dedicated statistics for the data collected within the driver and provides utility functions to set them.
    The driver pushes the collected statistics to the SmtEngine instead of adding them itself to the statistics registry.
    The node manager no longer holds a statistics registry (that nobody used anymore anyway)
    The command executor no longer holds a pointer to the SmtEngine itself. The pointer is not necessary and seems to become stale after we call reset on the command executor (which, luckily, we don't seem to do usually)

The main motivation for this change is to make the whole statistics infrastructure private to the library and not exporting it to the outside world.

4 files changed, 38 insertions, 14 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8ec594faa..a5da782d0 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -410,9 +410,10 @@ LogicInfo SmtEngine::getUserLogicInfo() const
   return res;
 }
 
-void SmtEngine::notifyStartParsing(std::string filename)
+void SmtEngine::notifyStartParsing(const std::string& filename)
 {
   d_state->setFilename(filename);
+  d_stats->d_driverFilename.set(filename);
   // Copy the original options. This is called prior to beginning parsing.
   // Hence reset should revert to these options, which note is after reading
   // the command line.
@@ -423,6 +424,15 @@ const std::string& SmtEngine::getFilename() const
 {
   return d_state->getFilename();
 }
+
+void SmtEngine::setResultStatistic(const std::string& result) {
+    d_stats->d_driverResult.set(result);
+}
+
+void SmtEngine::setTotalTimeStatistic(double seconds) {
+  d_stats->d_driverTotalTime.set(seconds);
+}
+
 void SmtEngine::setLogicInternal()
 {
   Assert(!d_state->isFullyInited())
@@ -508,15 +518,6 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
   if (key == "all-statistics")
   {
     vector<SExpr> stats;
-    StatisticsRegistry* sr = getNodeManager()->getStatisticsRegistry();
-    for (StatisticsRegistry::const_iterator i = sr->begin(); i != sr->end();
-         ++i)
-    {
-      vector<SExpr> v;
-      v.push_back((*i).first);
-      v.push_back((*i).second);
-      stats.push_back(v);
-    }
     for (StatisticsRegistry::const_iterator i = d_env->getStatisticsRegistry()->begin();
          i != d_env->getStatisticsRegistry()->end();
          ++i)
@@ -1896,13 +1897,11 @@ SExpr SmtEngine::getStatistic(std::string name) const
 
 void SmtEngine::flushStatistics(std::ostream& out) const
 {
-  getNodeManager()->getStatisticsRegistry()->flushInformation(out);
   d_env->getStatisticsRegistry()->flushInformation(out);
 }
 
 void SmtEngine::safeFlushStatistics(int fd) const
 {
-  getNodeManager()->getStatisticsRegistry()->safeFlushInformation(fd);
   d_env->getStatisticsRegistry()->safeFlushInformation(fd);
 }
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 16434d6d7..de3a64ff6 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -247,11 +247,20 @@ class CVC4_EXPORT SmtEngine
    * to a state where its options were prior to parsing but after e.g.
    * reading command line options.
    */
-  void notifyStartParsing(std::string filename) CVC4_EXPORT;
+  void notifyStartParsing(const std::string& filename) CVC4_EXPORT;
   /** return the input name (if any) */
   const std::string& getFilename() const;
 
   /**
+   * Helper method for the API to put the last check result into the statistics.
+   */
+  void setResultStatistic(const std::string& result) CVC4_EXPORT;
+  /**
+   * Helper method for the API to put the total runtime into the statistics.
+   */
+  void setTotalTimeStatistic(double seconds) CVC4_EXPORT;
+
+  /**
    * Get the model (only if immediately preceded by a SAT or NOT_ENTAILED
    * query).  Only permitted if produce-models is on.
    */
diff --git a/src/smt/smt_engine_stats.cpp b/src/smt/smt_engine_stats.cpp
index d8c48fd1d..382dcba1f 100644
--- a/src/smt/smt_engine_stats.cpp
+++ b/src/smt/smt_engine_stats.cpp
@@ -30,7 +30,10 @@ SmtEngineStatistics::SmtEngineStatistics()
       d_solveTime("smt::SmtEngine::solveTime"),
       d_pushPopTime("smt::SmtEngine::pushPopTime"),
       d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"),
-      d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0)
+      d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0),
+      d_driverFilename("driver::filename", ""),
+      d_driverResult("driver::sat/unsat", ""),
+      d_driverTotalTime("driver::totalTime", 0.0)
 {
   smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime);
   smtStatisticsRegistry()->registerStat(&d_numConstantProps);
@@ -43,6 +46,9 @@ SmtEngineStatistics::SmtEngineStatistics()
   smtStatisticsRegistry()->registerStat(&d_pushPopTime);
   smtStatisticsRegistry()->registerStat(&d_processAssertionsTime);
   smtStatisticsRegistry()->registerStat(&d_simplifiedToFalse);
+  smtStatisticsRegistry()->registerStat(&d_driverFilename);
+  smtStatisticsRegistry()->registerStat(&d_driverResult);
+  smtStatisticsRegistry()->registerStat(&d_driverTotalTime);
 }
 
 SmtEngineStatistics::~SmtEngineStatistics()
@@ -58,6 +64,9 @@ SmtEngineStatistics::~SmtEngineStatistics()
   smtStatisticsRegistry()->unregisterStat(&d_pushPopTime);
   smtStatisticsRegistry()->unregisterStat(&d_processAssertionsTime);
   smtStatisticsRegistry()->unregisterStat(&d_simplifiedToFalse);
+  smtStatisticsRegistry()->unregisterStat(&d_driverFilename);
+  smtStatisticsRegistry()->unregisterStat(&d_driverResult);
+  smtStatisticsRegistry()->unregisterStat(&d_driverTotalTime);
 }
 
 }  // namespace smt
diff --git a/src/smt/smt_engine_stats.h b/src/smt/smt_engine_stats.h
index 0f2e4fd50..9e3e7989e 100644
--- a/src/smt/smt_engine_stats.h
+++ b/src/smt/smt_engine_stats.h
@@ -50,6 +50,13 @@ struct SmtEngineStatistics
 
   /** Has something simplified to false? */
   IntStat d_simplifiedToFalse;
+
+  /** Name of the input file */
+  BackedStat<std::string> d_driverFilename;
+  /** Result of the last check */
+  BackedStat<std::string> d_driverResult;
+  /** Total time of the current run */
+  BackedStat<double> d_driverTotalTime;
 }; /* struct SmtEngineStatistics */
 
 }  // namespace smt