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 ce7a46b4e85dad7e055836616b24848ca429826b..bf658dfe0e5669c0aae52dea523c7f707aa7bce4 100644 (file)
--- 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 d3eb5c48a628cf10b9d7ad9f631c6e146d87188c..b9ed95339fcc23554eec17a2d7c895e335e16647 100644 (file)
--- 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 0e4e03f3adefc6a32de9566f572737a0d39edf1f..357f60b854b7def6e49cfe58e59344984b4b0780 100644 (file)
--- 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.