Plug solver API object into parser. (#2240)

1 files changed, 25 insertions, 10 deletions

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 0fd421b24..40c31de99 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -24,6 +24,7 @@
 #include <string>
 #include <vector>
 
+#include "api/cvc4cpp.h"
 #include "main/main.h"
 #include "smt/command.h"
 
@@ -48,15 +49,29 @@ void setNoLimitCPU() {
 
 void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString, const std::string& curStatsString);
 
-CommandExecutor::CommandExecutor(ExprManager &exprMgr, Options &options) :
-  d_exprMgr(exprMgr),
-  d_smtEngine(new SmtEngine(&exprMgr)),
-  d_options(options),
-  d_stats("driver"),
-  d_result(),
-  d_replayStream(NULL)
+CommandExecutor::CommandExecutor(api::Solver* solver, Options& options)
+    : d_solver(solver),
+      d_smtEngine(d_solver->getSmtEngine()),
+      d_options(options),
+      d_stats("driver"),
+      d_result(),
+      d_replayStream(NULL)
 {}
 
+void CommandExecutor::flushStatistics(std::ostream& out) const
+{
+  d_solver->getExprManager()->getStatistics().flushInformation(out);
+  d_smtEngine->getStatistics().flushInformation(out);
+  d_stats.flushInformation(out);
+}
+
+void CommandExecutor::safeFlushStatistics(int fd) const
+{
+  d_solver->getExprManager()->safeFlushStatistics(fd);
+  d_smtEngine->safeFlushStatistics(fd);
+  d_stats.safeFlushInformation(fd);
+}
+
 void CommandExecutor::setReplayStream(ExprStream* replayStream) {
   assert(d_replayStream == NULL);
   d_replayStream = replayStream;
@@ -92,11 +107,11 @@ bool CommandExecutor::doCommand(Command* cmd)
 
 void CommandExecutor::reset()
 {
-  if(d_options.getStatistics()) {
+  if (d_options.getStatistics())
+  {
     flushStatistics(*d_options.getErr());
   }
-  delete d_smtEngine;
-  d_smtEngine = new SmtEngine(&d_exprMgr);
+  d_solver->reset();
 }
 
 bool CommandExecutor::doCommandSingleton(Command* cmd)