Minor refactoring (#6273)

This PR does some minor refactorings in preparation for the new statistics: some renamings, removal of now obsolete code and usage of references instead of pointers.

4 files changed, 25 insertions, 66 deletions

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 6152064be..b7e3ad8b0 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -61,16 +61,20 @@ CommandExecutor::~CommandExecutor()
   d_solver.reset(nullptr);
 }
 
-void CommandExecutor::flushStatistics(std::ostream& out) const
+void CommandExecutor::printStatistics(std::ostream& out) const
 {
-  // SmtEngine + node manager flush statistics is part of the call below
-  getSmtEngine()->flushStatistics(out);
+  if (d_options.getStatistics())
+  {
+    getSmtEngine()->printStatistics(out);
+  }
 }
 
-void CommandExecutor::safeFlushStatistics(int fd) const
+void CommandExecutor::printStatisticsSafe(int fd) const
 {
-  // SmtEngine + node manager flush statistics is part of the call below
-  getSmtEngine()->safeFlushStatistics(fd);
+  if (d_options.getStatistics())
+  {
+    getSmtEngine()->printStatisticsSafe(fd);
+  }
 }
 
 bool CommandExecutor::doCommand(Command* cmd)
@@ -103,10 +107,7 @@ bool CommandExecutor::doCommand(Command* cmd)
 
 void CommandExecutor::reset()
 {
-  if (d_options.getStatistics())
-  {
-    flushStatistics(*d_options.getErr());
-  }
+  printStatistics(*d_options.getErr());
   /* We have to keep options passed via CL on reset. These options are stored
    * in CommandExecutor::d_options (populated and created in the driver), and
    * CommandExecutor::d_options only contains *these* options since the
@@ -144,7 +145,7 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
 
   if((cs != nullptr || q != nullptr) && d_options.getStatsEveryQuery()) {
     std::ostringstream ossCurStats;
-    flushStatistics(ossCurStats);
+    printStatistics(ossCurStats);
     std::ostream& err = *d_options.getErr();
     printStatsIncremental(err, d_lastStatistics, ossCurStats.str());
     d_lastStatistics = ossCurStats.str();
@@ -280,51 +281,8 @@ void printStatsIncremental(std::ostream& out,
   }
 }
 
-void CommandExecutor::printStatsFilterZeros(std::ostream& out,
-                                            const std::string& statsString) {
-  // read each line, if a number, check zero and skip if so
-  // Stat are assumed to one-per line: "<statName>, <statValue>"
-
-  std::istringstream iss(statsString);
-  std::string statName, statValue;
-
-  std::getline(iss, statName, ',');
-
-  while (!iss.eof())
-  {
-    std::getline(iss, statValue, '\n');
-
-    bool skip = false;
-    try
-    {
-      double dval = std::stod(statValue);
-      skip = (dval == 0.0);
-    }
-    // Value can not be converted, don't skip
-    catch (const std::invalid_argument&) {}
-    catch (const std::out_of_range&) {}
-
-    skip = skip || (statValue == " \"0\"" || statValue == " \"[]\"");
-
-    if (!skip)
-    {
-      out << statName << "," << statValue << std::endl;
-    }
-
-    std::getline(iss, statName, ',');
-  }
-}
-
 void CommandExecutor::flushOutputStreams() {
-  if(d_options.getStatistics()) {
-    if(d_options.getStatsHideZeros() == false) {
-      flushStatistics(*(d_options.getErr()));
-    } else {
-      std::ostringstream ossStats;
-      flushStatistics(ossStats);
-      printStatsFilterZeros(*(d_options.getErr()), ossStats.str());
-    }
-  }
+  printStatistics(*(d_options.getErr()));
 
   // make sure out and err streams are flushed too
   d_options.flushOut();
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index f066a27b6..60305ff1f 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -84,18 +84,19 @@ class CommandExecutor
   SmtEngine* getSmtEngine() const { return d_solver->getSmtEngine(); }
 
   /**
-   * Flushes statistics to a file descriptor.
+   * Prints statistics to an output stream.
+   * Checks whether statistics should be printed according to the options.
+   * Thus, this method can always be called without checking the options.
    */
-  virtual void flushStatistics(std::ostream& out) const;
+  virtual void printStatistics(std::ostream& out) const;
 
   /**
-   * Flushes statistics to a file descriptor.
-   * Safe to use in a signal handler.
+   * Safely prints statistics to a file descriptor.
+   * This method is safe to be used within a signal handler.
+   * Checks whether statistics should be printed according to the options.
+   * Thus, this method can always be called without checking the options.
    */
-  void safeFlushStatistics(int fd) const;
-
-  static void printStatsFilterZeros(std::ostream& out,
-                                    const std::string& statsString);
+  void printStatisticsSafe(int fd) const;
 
   void flushOutputStreams();
 
diff --git a/src/main/main.cpp b/src/main/main.cpp
index a17b2e7c5..2a8bc7ab2 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -69,7 +69,7 @@ int main(int argc, char* argv[]) {
     if (opts.getStatistics() && pExecutor != nullptr)
     {
       totalTime.reset();
-      pExecutor->flushStatistics(*opts.getErr());
+      pExecutor->printStatistics(*opts.getErr());
     }
   }
   exit(1);
diff --git a/src/main/signal_handlers.cpp b/src/main/signal_handlers.cpp
index ae549e9a6..bd9ec7ee0 100644
--- a/src/main/signal_handlers.cpp
+++ b/src/main/signal_handlers.cpp
@@ -58,10 +58,10 @@ namespace signal_handlers {
 
 void print_statistics()
 {
-  if (pOptions != NULL && pOptions->getStatistics() && pExecutor != NULL)
+  if (pExecutor != nullptr)
   {
     totalTime.reset();
-    pExecutor->safeFlushStatistics(STDERR_FILENO);
+    pExecutor->printStatisticsSafe(STDERR_FILENO);
   }
 }