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.h | |
| 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.h')
| -rw-r--r-- | src/main/command_executor_portfolio.h | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/main/command_executor_portfolio.h b/src/main/command_executor_portfolio.h index cc0a77698..72a677789 100644 --- a/src/main/command_executor_portfolio.h +++ b/src/main/command_executor_portfolio.h @@ -23,6 +23,11 @@ #include "main/command_executor.h" #include "main/portfolio_util.h" +#include <vector> +#include <string> +#include <iostream> +#include <sstream> + namespace CVC4 { class CommandSequence; @@ -55,6 +60,9 @@ public: ~CommandExecutorPortfolio(); std::string getSmtEngineStatus(); + + void flushStatistics(std::ostream& out) const; + protected: bool doCommandSingleton(Command* cmd); private: |