summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/api/cvc4cpp.cpp6
-rw-r--r--src/main/command_executor.cpp68
-rw-r--r--src/main/command_executor.h17
-rw-r--r--src/main/main.cpp2
-rw-r--r--src/main/signal_handlers.cpp4
-rw-r--r--src/smt/env.cpp4
-rw-r--r--src/smt/env.h2
-rw-r--r--src/smt/smt_engine.cpp22
-rw-r--r--src/smt/smt_engine.h6
-rw-r--r--src/smt/smt_engine_scope.cpp2
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: "<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 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<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 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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback