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.

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index f304ae5a063511311affe0c2c13aeffba02a6a91..463fe74df4de9df546c6d4d090e911688685daa0 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -4074,9 +4074,9 @@ Solver::Solver(Options* opts)
   d_rng.reset(new Random(d_smtEngine->getOptions()[options::seed]));
 #if CVC4_STATISTICS_ON
   d_stats.reset(new Statistics());
-  d_smtEngine->getStatisticsRegistry()->registerStat(&d_stats->d_consts);
-  d_smtEngine->getStatisticsRegistry()->registerStat(&d_stats->d_vars);
-  d_smtEngine->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/main/command_executor.cpp b/src/main/command_executor.cpp
index 6152064be02a0ca2ff805b8d466df6d403056941..b7e3ad8b04ae79d8e467e6fbb77def5774740f5e 100644 (file)
--- 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 f066a27b61fed1a5e2e5b5c227f48b1b71457523..60305ff1f2ce15c0818e3f480d07aca320f57bca 100644 (file)
--- 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 a17b2e7c536ed1068c65e61065733c7667dab57e..2a8bc7ab2b0432425c81780b9cd97a5199f33c26 100644 (file)
--- 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 ae549e9a6fd0f0c59771e8510e8070b5f412d1f5..bd9ec7ee019282b02417b1e0735af8d6b5a7cd8a 100644 (file)
--- 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);
   }
 }
 

diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index fc19299d43c28d6307b2c96355c10f91fa134dd1..e88710628d15aa76ec7992f7ba8c478340196afd 100644 (file)
--- a/src/smt/env.cpp
+++ b/src/smt/env.cpp
@@ -82,9 +82,9 @@ DumpManager* Env::getDumpManager() { return d_dumpManager.get(); }
 
 const LogicInfo& Env::getLogicInfo() const { return d_logic; }
 
-StatisticsRegistry* Env::getStatisticsRegistry()
+StatisticsRegistry& Env::getStatisticsRegistry()
 {
-  return d_statisticsRegistry.get();
+  return *d_statisticsRegistry;
 }
 
 const Options& Env::getOptions() const { return d_options; }

diff --git a/src/smt/env.h b/src/smt/env.h
index 79377206a118b61aa923161409978158a5d29be7..4ad8c81e2b295eb01f61bb411967d4b904d30c77 100644 (file)
--- a/src/smt/env.h
+++ b/src/smt/env.h
@@ -97,7 +97,7 @@ class Env
   const LogicInfo& getLogicInfo() const;
 
   /** Get a pointer to the StatisticsRegistry. */
-  StatisticsRegistry* getStatisticsRegistry();
+  StatisticsRegistry& getStatisticsRegistry();
 
   /* Option helpers---------------------------------------------------------- */
 

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 724c5d48f9aea10fa02a5979a48d5ce818e79aed..d7c44fef3c169bef2ac81c9284247e55fe56944d 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -511,13 +511,11 @@ cvc5::SExpr SmtEngine::getInfo(const std::string& key) const
   if (key == "all-statistics")
   {
     vector<SExpr> stats;
-    for (StatisticsRegistry::const_iterator i = d_env->getStatisticsRegistry()->begin();
-         i != d_env->getStatisticsRegistry()->end();
-         ++i)
+    for (const auto& s: d_env->getStatisticsRegistry())
     {
       vector<SExpr> v;
-      v.push_back((*i).first);
-      v.push_back((*i).second);
+      v.push_back(s.first);
+      v.push_back(s.second);
       stats.push_back(v);
     }
     return SExpr(stats);
@@ -1393,7 +1391,7 @@ void SmtEngine::checkProof()
   }
 }
 
-StatisticsRegistry* SmtEngine::getStatisticsRegistry()
+StatisticsRegistry& SmtEngine::getStatisticsRegistry()
 {
   return d_env->getStatisticsRegistry();
 }
@@ -1852,22 +1850,22 @@ NodeManager* SmtEngine::getNodeManager() const
 
 Statistics SmtEngine::getStatistics() const
 {
-  return Statistics(*d_env->getStatisticsRegistry());
+  return Statistics(d_env->getStatisticsRegistry());
 }
 
 SExpr SmtEngine::getStatistic(std::string name) const
 {
-  return d_env->getStatisticsRegistry()->getStatistic(name);
+  return d_env->getStatisticsRegistry().getStatistic(name);
 }
 
-void SmtEngine::flushStatistics(std::ostream& out) const
+void SmtEngine::printStatistics(std::ostream& out) const
 {
-  d_env->getStatisticsRegistry()->flushInformation(out);
+  d_env->getStatisticsRegistry().flushInformation(out);
 }
 
-void SmtEngine::safeFlushStatistics(int fd) const
+void SmtEngine::printStatisticsSafe(int fd) const
 {
-  d_env->getStatisticsRegistry()->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 909c1cc500712c500118bf3b567a97aceab9915d..493042bbe62f525c345d5e2ebdc4d72c5b745e06 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -824,13 +824,13 @@ class CVC4_EXPORT SmtEngine
   SExpr getStatistic(std::string name) const;
 
   /** Flush statistics from this SmtEngine and the NodeManager it uses. */
-  void flushStatistics(std::ostream& out) const;
+  void printStatistics(std::ostream& out) const;
 
   /**
    * Flush statistics from this SmtEngine and the NodeManager it uses. Safe to
    * use in a signal handler.
    */
-  void safeFlushStatistics(int fd) const;
+  void printStatisticsSafe(int fd) const;
 
   /**
    * Set user attribute.
@@ -906,7 +906,7 @@ class CVC4_EXPORT SmtEngine
   smt::PfManager* getPfManager() { return d_pfManager.get(); };
 
   /** Get a pointer to the StatisticsRegistry owned by this SmtEngine. */
-  StatisticsRegistry* getStatisticsRegistry();
+  StatisticsRegistry& getStatisticsRegistry();
 
   /**
    * Internal method to get an unsatisfiable core (only if immediately preceded

diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp
index cbb6a9679a82e1ec3d0078fa703848da889e1ecc..aa349d9805b6e730e0902da0e5521e02f1eb2969 100644 (file)
--- a/src/smt/smt_engine_scope.cpp
+++ b/src/smt/smt_engine_scope.cpp
@@ -62,7 +62,7 @@ SmtScope::~SmtScope() {
 
 StatisticsRegistry* SmtScope::currentStatisticsRegistry() {
   Assert(smtEngineInScope());
-  return s_smtEngine_current->getStatisticsRegistry();
+  return &(s_smtEngine_current->getStatisticsRegistry());
 }
 
 }  // namespace smt