diff options
Diffstat (limited to 'src/main/command_executor.h')
-rw-r--r-- | src/main/command_executor.h | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/src/main/command_executor.h b/src/main/command_executor.h index 273225e69..435299ce3 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -19,6 +19,12 @@ #include "expr/expr_manager.h" #include "smt/smt_engine.h" +#include "util/statistics_registry.h" +#include "options/options.h" +#include "expr/command.h" + +#include <string> +#include <iostream> namespace CVC4 { namespace main { @@ -29,6 +35,7 @@ protected: ExprManager& d_exprMgr; SmtEngine d_smtEngine; Options& d_options; + StatisticsRegistry d_stats; public: // Note: though the options are not cached (instead a reference is @@ -48,6 +55,16 @@ public: virtual std::string getSmtEngineStatus(); + StatisticsRegistry& getStatisticsRegistry() { + return d_stats; + } + + virtual void flushStatistics(std::ostream& out) const { + d_exprMgr.getStatistics().flushInformation(out); + d_smtEngine.getStatistics().flushInformation(out); + d_stats.flushInformation(out); + } + protected: /** Executes treating cmd as a singleton */ virtual bool doCommandSingleton(CVC4::Command* cmd); |