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);