diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-22 21:10:51 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-22 21:10:51 +0000 |
commit | e2611a54c5479086df0c4a80f56597aae80b5c4e (patch) | |
tree | b0d98600bd70147f28197883d3481614b87d76f6 /src/main/command_executor_portfolio.cpp | |
parent | 8b106b77c11d12d16abac845ed704845ef888bd2 (diff) |
Separate public-facing and internal-facing interfaces to Statistics.
The external interface (e.g., what's answered by ExprManager::getStatistics() and SmtEngine::getStatistics()) is a snapshot of the current statistics (rather than a reference to the actual StatisticsRegistry).
The StatisticsRegistry is now internal-only. However, it's built as a convenience library so that the parser and driver can use it too (by re-linking against it).
This is part of the ongoing effort to clean up the public interface.
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/main/command_executor_portfolio.cpp')
-rw-r--r-- | src/main/command_executor_portfolio.cpp | 54 |
1 files changed, 29 insertions, 25 deletions
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index 045cac8f1..32a507d78 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -21,6 +21,7 @@ #include <boost/thread/condition.hpp> #include <boost/exception_ptr.hpp> #include <boost/lexical_cast.hpp> +#include <string> #include "expr/command.h" #include "expr/pickler.h" @@ -63,26 +64,10 @@ CommandExecutorPortfolio::CommandExecutorPortfolio d_smts.push_back(new SmtEngine(d_exprMgrs[i])); } - for(unsigned i = 1; i < d_numThreads; ++i) { - // Register the statistics registry of the thread - string emTag = "ExprManager thread #" - + boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]); - string smtTag = "SmtEngine thread #" - + boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]); - d_exprMgrs[i]->getStatisticsRegistry()->setName(emTag); - d_smts[i]->getStatisticsRegistry()->setName(smtTag); - pStatistics->registerStat_ - (d_exprMgrs[i]->getStatisticsRegistry() ); - pStatistics->registerStat_ - (d_smts[i]->getStatisticsRegistry() ); - } - Assert(d_vmaps.size() == 0); for(unsigned i = 0; i < d_numThreads; ++i) { d_vmaps.push_back(new ExprManagerMapCollection()); } - - } CommandExecutorPortfolio::~CommandExecutorPortfolio() @@ -116,7 +101,7 @@ void CommandExecutorPortfolio::lemmaSharingInit() for(unsigned i = 0; i < d_numThreads; ++i){ if(Debug.isOn("channel-empty")) { - d_channelsOut.push_back + d_channelsOut.push_back (new EmptySharedChannel<ChannelFormat>(sharingChannelSize)); d_channelsIn.push_back (new EmptySharedChannel<ChannelFormat>(sharingChannelSize)); @@ -143,7 +128,7 @@ void CommandExecutorPortfolio::lemmaSharingInit() } /* Output to string stream */ - if(d_options[options::verbosity] == 0 + if(d_options[options::verbosity] == 0 || d_options[options::separateOutput]) { Assert(d_ostringstreams.size() == 0); for(unsigned i = 0; i < d_numThreads; ++i) { @@ -152,7 +137,7 @@ void CommandExecutorPortfolio::lemmaSharingInit() } } } -} +}/* CommandExecutorPortfolio::lemmaSharingInit() */ void CommandExecutorPortfolio::lemmaSharingCleanup() { @@ -180,7 +165,8 @@ void CommandExecutorPortfolio::lemmaSharingCleanup() d_ostringstreams.clear(); } -} +}/* CommandExecutorPortfolio::lemmaSharingCleanup() */ + bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) { @@ -200,7 +186,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) // } else if(dynamic_cast<GetValueCommand*>(cmd) != NULL) { // mode = 2; // } - + if(mode == 0) { d_seq->addCommand(cmd->clone()); return CommandExecutor::doCommandSingleton(cmd); @@ -290,7 +276,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) *d_options[options::out] << d_ostringstreams[portfolioReturn.first]->str(); } - + /* cleanup this check sat specific stuff */ lemmaSharingCleanup(); @@ -303,12 +289,30 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) Unreachable(); } -} +}/* CommandExecutorPortfolio::doCommandSingleton() */ std::string CommandExecutorPortfolio::getSmtEngineStatus() { return d_smts[d_lastWinner]->getInfo("status").getValue(); } -}/*main namespace*/ -}/*CVC4 namespace*/ +void CommandExecutorPortfolio::flushStatistics(std::ostream& out) const { + Assert(d_numThreads == d_exprMgrs.size() && d_exprMgrs.size() == d_smts.size()); + for(size_t i = 0; i < d_numThreads; ++i) { + string emTag = "ExprManager thread #" + + boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]); + Statistics stats = d_exprMgrs[i]->getStatistics(); + stats.setPrefix(emTag); + stats.flushInformation(out); + + string smtTag = "SmtEngine thread #" + + boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]); + stats = d_smts[i]->getStatistics(); + stats.setPrefix(smtTag); + stats.flushInformation(out); + } + d_stats.flushInformation(out); +} + +}/* CVC4::main namespace */ +}/* CVC4 namespace */ |