diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-04-02 19:47:43 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-02 17:47:43 +0000 |
commit | 2506e17ca86c42b7590f65326b70a69b0efdb0bd (patch) | |
tree | cf1686ebfa22300f03f60b0e80a9a8fdb6ddd33c /src/smt | |
parent | da3eff9ba6c632e290c9af990dc5750f65d78820 (diff) |
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.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/env.cpp | 4 | ||||
-rw-r--r-- | src/smt/env.h | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 22 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 6 | ||||
-rw-r--r-- | src/smt/smt_engine_scope.cpp | 2 |
5 files changed, 17 insertions, 19 deletions
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 |