diff options
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: |