From 2506e17ca86c42b7590f65326b70a69b0efdb0bd Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 2 Apr 2021 19:47:43 +0200 Subject: [PATCH] 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. --- src/api/cvc4cpp.cpp | 6 ++-- src/main/command_executor.cpp | 68 +++++++---------------------------- src/main/command_executor.h | 17 ++++----- src/main/main.cpp | 2 +- src/main/signal_handlers.cpp | 4 +-- src/smt/env.cpp | 4 +-- src/smt/env.h | 2 +- src/smt/smt_engine.cpp | 22 ++++++------ src/smt/smt_engine.h | 6 ++-- src/smt/smt_engine_scope.cpp | 2 +- 10 files changed, 45 insertions(+), 88 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index f304ae5a0..463fe74df 100644 --- 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 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: ", " - - 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); } } diff --git a/src/smt/env.cpp b/src/smt/env.cpp index fc19299d4..e88710628 100644 --- 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 79377206a..4ad8c81e2 100644 --- 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 724c5d48f..d7c44fef3 100644 --- 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 stats; - for (StatisticsRegistry::const_iterator i = d_env->getStatisticsRegistry()->begin(); - i != d_env->getStatisticsRegistry()->end(); - ++i) + for (const auto& s: d_env->getStatisticsRegistry()) { vector 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 909c1cc50..493042bbe 100644 --- 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 cbb6a9679..aa349d980 100644 --- 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 -- 2.30.2