From: Gereon Kremer <nafur42@gmail.com>
Date: Tue, 3 Aug 2021 00:05:54 +0000 (-0700)
Subject: Properly honor --stats-all and --stats-expert when printing statistics (#6967)
X-Git-Tag: cvc5-1.0.0~1420
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9547af1fb7fa26d6a3299ede363fc2faaae85908;p=cvc5.git

Properly honor --stats-all and --stats-expert when printing statistics (#6967)

This PR fixes an issue that was introduced with fda4613 where printing the statistics would only show non-defaulted and non-expert options.
---

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index ce7a46b4e..bf658dfe0 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -65,9 +65,15 @@ CommandExecutor::~CommandExecutor()
 
 void CommandExecutor::printStatistics(std::ostream& out) const
 {
-  if (d_solver->getOptions().base.statistics)
+  const auto& baseopts = d_solver->getOptions().base;
+  if (baseopts.statistics)
   {
-    out << d_solver->getStatistics();
+    const auto& stats = d_solver->getStatistics();
+    auto it = stats.begin(baseopts.statisticsExpert, baseopts.statisticsAll);
+    for (; it != stats.end(); ++it)
+    {
+      out << it->first << " = " << it->second << std::endl;
+    }
   }
 }
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d3eb5c48a..b9ed95339 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1923,11 +1923,6 @@ NodeManager* SmtEngine::getNodeManager() const
   return d_env->getNodeManager();
 }
 
-void SmtEngine::printStatistics(std::ostream& out) const
-{
-  d_env->getStatisticsRegistry().print(out);
-}
-
 void SmtEngine::printStatisticsSafe(int fd) const
 {
   d_env->getStatisticsRegistry().printSafe(fd);
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 0e4e03f3a..357f60b85 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -810,12 +810,6 @@ class CVC5_EXPORT SmtEngine
   /** Permit access to the underlying NodeManager. */
   NodeManager* getNodeManager() const;
 
-  /**
-   * Print statistics from the statistics registry in the env object owned by
-   * this SmtEngine.
-   */
-  void printStatistics(std::ostream& out) const;
-
   /**
    * Print statistics from the statistics registry in the env object owned by
    * this SmtEngine. Safe to use in a signal handler.