1 files changed, 27 insertions, 25 deletions

diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index 31a604174..7e7202a5a 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -2,7 +2,7 @@
 /*! \file command_executor.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Kshitij Bansal, Morgan Deters, Tim King
+ **   Kshitij Bansal, Morgan Deters, Aina Niemetz
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
@@ -25,6 +25,11 @@
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
+
+namespace api {
+class Solver;
+}
+
 namespace main {
 
 class CommandExecutor {
@@ -32,21 +37,22 @@ private:
   std::string d_lastStatistics;
 
 protected:
-  ExprManager& d_exprMgr;
-  SmtEngine* d_smtEngine;
-  Options& d_options;
-  StatisticsRegistry d_stats;
-  Result d_result;
-  ExprStream* d_replayStream;
+ api::Solver* d_solver;
+ SmtEngine* d_smtEngine;
+ Options& d_options;
+ StatisticsRegistry d_stats;
+ Result d_result;
+ ExprStream* d_replayStream;
 
 public:
-  CommandExecutor(ExprManager &exprMgr, Options &options);
-
-  virtual ~CommandExecutor() {
-    delete d_smtEngine;
-    if(d_replayStream != NULL){
-      delete d_replayStream;
-    }
+ CommandExecutor(api::Solver* solver, Options& options);
+
+ virtual ~CommandExecutor()
+ {
+   if (d_replayStream != NULL)
+   {
+     delete d_replayStream;
+   }
   }
 
   /**
@@ -63,20 +69,16 @@ public:
     return d_stats;
   }
 
-  virtual void flushStatistics(std::ostream& out) const {
-    d_exprMgr.getStatistics().flushInformation(out);
-    d_smtEngine->getStatistics().flushInformation(out);
-    d_stats.flushInformation(out);
-  }
+  /**
+   * Flushes statistics to a file descriptor.
+   */
+  virtual void flushStatistics(std::ostream& out) const;
 
   /**
-   * Flushes statistics to a file descriptor. Safe to use in a signal handler.
+   * Flushes statistics to a file descriptor.
+   * Safe to use in a signal handler.
    */
-  void safeFlushStatistics(int fd) const {
-    d_exprMgr.safeFlushStatistics(fd);
-    d_smtEngine->safeFlushStatistics(fd);
-    d_stats.safeFlushInformation(fd);
-  }
+  void safeFlushStatistics(int fd) const;
 
   static void printStatsFilterZeros(std::ostream& out,
                                     const std::string& statsString);