From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Mon, 22 Mar 2021 21:09:55 +0000 (+0100)
Subject: Move statistics from the driver into the SmtEngine (#6170)
X-Git-Tag: cvc5-1.0.0~2042
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=442bc26b6ce093efed14bfd6764dac30bfdf918f;p=cvc5.git

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.
---

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index e87e6176b..dce190460 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -4040,9 +4040,9 @@ Solver::Solver(Options* opts)
   d_rng.reset(new Random(o[options::seed]));
 #if CVC4_STATISTICS_ON
   d_stats.reset(new Statistics());
-  d_nodeMgr->getStatisticsRegistry()->registerStat(&d_stats->d_consts);
-  d_nodeMgr->getStatisticsRegistry()->registerStat(&d_stats->d_vars);
-  d_nodeMgr->getStatisticsRegistry()->registerStat(&d_stats->d_terms);
+  d_smtEngine->getStatisticsRegistry()->registerStat(&d_stats->d_consts);
+  d_smtEngine->getStatisticsRegistry()->registerStat(&d_stats->d_vars);
+  d_smtEngine->getStatisticsRegistry()->registerStat(&d_stats->d_terms);
 #endif
 }
 
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 2d2b8a2e5..a176744ef 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -3687,12 +3687,12 @@ class CVC4_EXPORT Solver
 
   /** The node manager of this solver. */
   std::unique_ptr<NodeManager> d_nodeMgr;
+  /** The statistics collected on the Api level. */
+  std::unique_ptr<Statistics> d_stats;
   /** The SMT engine of this solver. */
   std::unique_ptr<SmtEngine> d_smtEngine;
   /** The random number generator of this solver. */
   std::unique_ptr<Random> d_rng;
-  /** The statistics collected on the Api level. */
-  std::unique_ptr<Statistics> d_stats;
 };
 
 }  // namespace api
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index fdd7e5f5a..599d3e8f7 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -18,6 +18,7 @@
 #include "expr/node_manager.h"
 
 #include <algorithm>
+#include <sstream>
 #include <stack>
 #include <utility>
 
@@ -32,7 +33,6 @@
 #include "expr/skolem_manager.h"
 #include "expr/type_checker.h"
 #include "util/resource_manager.h"
-#include "util/statistics_registry.h"
 
 using namespace std;
 using namespace CVC4::expr;
@@ -93,8 +93,7 @@ namespace attr {
 typedef expr::Attribute<attr::LambdaBoundVarListTag, Node> LambdaBoundVarListAttr;
 
 NodeManager::NodeManager()
-    : d_statisticsRegistry(new StatisticsRegistry()),
-      d_skManager(new SkolemManager),
+    : d_skManager(new SkolemManager),
       d_bvManager(new BoundVarManager),
       next_id(0),
       d_attrManager(new expr::attr::AttributeManager()),
@@ -264,8 +263,6 @@ NodeManager::~NodeManager() {
   }
 
   // defensive coding, in case destruction-order issues pop up (they often do)
-  delete d_statisticsRegistry;
-  d_statisticsRegistry = NULL;
   delete d_attrManager;
   d_attrManager = NULL;
 }
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 348200b6e..ce89f5dc6 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -41,7 +41,6 @@ namespace api {
 class Solver;
 }
 
-class StatisticsRegistry;
 class ResourceManager;
 class SkolemManager;
 class BoundVarManager;
@@ -116,8 +115,6 @@ class NodeManager
 
   static thread_local NodeManager* s_current;
 
-  StatisticsRegistry* d_statisticsRegistry;
-
   /** The skolem manager */
   std::unique_ptr<SkolemManager> d_skManager;
   /** The bound variable manager */
@@ -390,12 +387,6 @@ class NodeManager
   /** Get this node manager's bound variable manager */
   BoundVarManager* getBoundVarManager() { return d_bvManager.get(); }
 
-  /** Get this node manager's statistics registry */
-  StatisticsRegistry* getStatisticsRegistry() const
-  {
-    return d_statisticsRegistry;
-  }
-
   /** Subscribe to NodeManager events */
   void subscribeEvents(NodeManagerListener* listener) {
     Assert(std::find(d_listeners.begin(), d_listeners.end(), listener)
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index a343b4a37..551880b98 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -50,9 +50,7 @@ void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString
 CommandExecutor::CommandExecutor(Options& options)
     : d_solver(new api::Solver(&options)),
       d_symman(new SymbolManager(d_solver.get())),
-      d_smtEngine(d_solver->getSmtEngine()),
       d_options(options),
-      d_stats(),
       d_result()
 {
 }
@@ -66,15 +64,13 @@ CommandExecutor::~CommandExecutor()
 void CommandExecutor::flushStatistics(std::ostream& out) const
 {
   // SmtEngine + node manager flush statistics is part of the call below
-  d_smtEngine->flushStatistics(out);
-  d_stats.flushInformation(out);
+  getSmtEngine()->flushStatistics(out);
 }
 
 void CommandExecutor::safeFlushStatistics(int fd) const
 {
   // SmtEngine + node manager flush statistics is part of the call below
-  d_smtEngine->safeFlushStatistics(fd);
-  d_stats.safeFlushInformation(fd);
+  getSmtEngine()->safeFlushStatistics(fd);
 }
 
 bool CommandExecutor::doCommand(Command* cmd)
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index 48761b7ad..0dea41383 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -52,9 +52,7 @@ class CommandExecutor
    * symbol manager.
    */
   std::unique_ptr<SymbolManager> d_symman;
-  SmtEngine* d_smtEngine;
   Options& d_options;
-  StatisticsRegistry d_stats;
   api::Result d_result;
 
  public:
@@ -82,11 +80,7 @@ class CommandExecutor
   api::Result getResult() const { return d_result; }
   void reset();
 
-  StatisticsRegistry& getStatisticsRegistry() {
-    return d_stats;
-  }
-
-  SmtEngine* getSmtEngine() { return d_smtEngine; }
+  SmtEngine* getSmtEngine() const { return d_solver->getSmtEngine(); }
 
   /**
    * Flushes statistics to a file descriptor.
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 846bef5be..d2b676e82 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -15,6 +15,7 @@
 #include <stdio.h>
 #include <unistd.h>
 
+#include <chrono>
 #include <cstdlib>
 #include <cstring>
 #include <fstream>
@@ -38,7 +39,6 @@
 #include "parser/parser_builder.h"
 #include "smt/command.h"
 #include "util/result.h"
-#include "util/statistics_registry.h"
 
 using namespace std;
 using namespace CVC4;
@@ -59,9 +59,6 @@ namespace CVC4 {
     /** A pointer to the CommandExecutor (the signal handlers need it) */
     CVC4::main::CommandExecutor* pExecutor = nullptr;
 
-    /** A pointer to the totalTime driver stat (the signal handlers need it) */
-    CVC4::TimerStat* pTotalTime = nullptr;
-
   }/* CVC4::main namespace */
 }/* CVC4 namespace */
 
@@ -82,10 +79,7 @@ void printUsage(Options& opts, bool full) {
 
 int runCvc4(int argc, char* argv[], Options& opts) {
 
-  // Timer statistic
-  pTotalTime = new TimerStat("driver::totalTime");
-  pTotalTime->start();
-
+  std::chrono::time_point totalTimeStart = std::chrono::steady_clock::now();
   // For the signal handlers' benefit
   pOptions = &opts;
 
@@ -186,14 +180,6 @@ int runCvc4(int argc, char* argv[], Options& opts) {
 
   int returnValue = 0;
   {
-    // Timer statistic
-    RegisterStatistic statTotalTime(&pExecutor->getStatisticsRegistry(),
-                                    pTotalTime);
-
-    // Filename statistics
-    ReferenceStat<std::string> s_statFilename("driver::filename", filenameStr);
-    RegisterStatistic statFilenameReg(&pExecutor->getStatisticsRegistry(),
-                                      &s_statFilename);
     // notify SmtEngine that we are starting to parse
     pExecutor->getSmtEngine()->notifyStartParsing(filenameStr);
 
@@ -471,16 +457,10 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     // or other on_exit/atexit stuff.
     _exit(returnValue);
 #endif /* CVC4_COMPETITION_MODE */
+    pExecutor->getSmtEngine()->setResultStatistic(result.toString());
+    std::chrono::duration totalTime = std::chrono::steady_clock::now() - totalTimeStart;
+    pExecutor->getSmtEngine()->setTotalTimeStatistic(std::chrono::duration<double>(totalTime).count());
 
-    ReferenceStat<api::Result> s_statSatResult("driver::sat/unsat", result);
-    RegisterStatistic statSatResultReg(&pExecutor->getStatisticsRegistry(),
-                                       &s_statSatResult);
-
-    pTotalTime->stop();
-
-    // Tim: I think that following comment is out of date?
-    // Set the global executor pointer to nullptr first.  If we get a
-    // signal while dumping statistics, we don't want to try again.
     pExecutor->flushOutputStreams();
 
 #ifdef CVC4_DEBUG
@@ -494,12 +474,8 @@ int runCvc4(int argc, char* argv[], Options& opts) {
 #endif /* CVC4_DEBUG */
   }
 
-  // On exceptional exit, these are leaked, but that's okay... they
-  // need to be around in that case for main() to print statistics.
-  delete pTotalTime;
   delete pExecutor;
 
-  pTotalTime = nullptr;
   pExecutor = nullptr;
 
   signal_handlers::cleanup();
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 7e0ed1e83..eb313c3bd 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -32,7 +32,6 @@
 #include "parser/parser_builder.h"
 #include "parser/parser_exception.h"
 #include "util/result.h"
-#include "util/statistics.h"
 
 using namespace std;
 using namespace CVC4;
@@ -68,7 +67,6 @@ int main(int argc, char* argv[]) {
       *opts.getErr() << "(error \"" << e << "\")" << endl;
     }
     if(opts.getStatistics() && pExecutor != NULL) {
-      pTotalTime->stop();
       pExecutor->flushStatistics(*opts.getErr());
     }
   }
diff --git a/src/main/main.h b/src/main/main.h
index 37430b507..b769bee7d 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -20,9 +20,6 @@
 #include "base/exception.h"
 #include "cvc4autoconfig.h"
 #include "options/options.h"
-#include "util/statistics.h"
-#include "util/statistics_registry.h"
-#include "util/stats_timer.h"
 
 #ifndef CVC4__MAIN__MAIN_H
 #define CVC4__MAIN__MAIN_H
@@ -41,9 +38,6 @@ extern const std::string* progName;
 /** A reference for use by the signal handlers to print statistics */
 extern CVC4::main::CommandExecutor* pExecutor;
 
-/** A reference for use by the signal handlers to print statistics */
-extern CVC4::TimerStat* pTotalTime;
-
 /**
  * If true, will not spin on segfault even when CVC4_DEBUG is on.
  * Useful for nightly regressions, noninteractive performance runs
diff --git a/src/main/signal_handlers.cpp b/src/main/signal_handlers.cpp
index f3f32c4cd..ccd6c0b19 100644
--- a/src/main/signal_handlers.cpp
+++ b/src/main/signal_handlers.cpp
@@ -40,7 +40,6 @@
 #include "options/options.h"
 #include "smt/smt_engine.h"
 #include "util/safe_print.h"
-#include "util/statistics.h"
 
 using CVC4::Exception;
 using namespace std;
@@ -61,10 +60,6 @@ void print_statistics()
 {
   if (pOptions != NULL && pOptions->getStatistics() && pExecutor != NULL)
   {
-    if (pTotalTime != NULL && pTotalTime->running())
-    {
-      pTotalTime->stop();
-    }
     pExecutor->safeFlushStatistics(STDERR_FILENO);
   }
 }
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,10 +247,19 @@ 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