From 9547af1fb7fa26d6a3299ede363fc2faaae85908 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 2 Aug 2021 17:05:54 -0700 Subject: [PATCH] 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. --- src/main/command_executor.cpp | 10 ++++++++-- src/smt/smt_engine.cpp | 5 ----- src/smt/smt_engine.h | 6 ------ 3 files changed, 8 insertions(+), 13 deletions(-) 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. -- 2.30.2