Plug solver API object into parser. (#2240)

5 files changed, 80 insertions, 55 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)
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);
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index f97b037eb..c29212c4f 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -26,6 +26,7 @@
 // This must come before PORTFOLIO_BUILD.
 #include "cvc4autoconfig.h"
 
+#include "api/cvc4cpp.h"
 #include "base/configuration.h"
 #include "base/output.h"
 #include "expr/expr_iomanip.h"
@@ -200,10 +201,10 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   (*(opts.getOut())) << language::SetLanguage(opts.getOutputLanguage());
 
   // Create the expression manager using appropriate options
-  ExprManager* exprMgr;
+  std::unique_ptr<api::Solver> solver;
 # ifndef PORTFOLIO_BUILD
-  exprMgr = new ExprManager(opts);
-  pExecutor = new CommandExecutor(*exprMgr, opts);
+  solver.reset(new api::Solver(&opts));
+  pExecutor = new CommandExecutor(solver.get(), opts);
 # else
   OptionsList threadOpts;
   parseThreadSpecificOptions(threadOpts, opts);
@@ -230,19 +231,23 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     }
   }
   // pick appropriate one
-  if(useParallelExecutor) {
-    exprMgr = new ExprManager(threadOpts[0]);
-    pExecutor = new CommandExecutorPortfolio(*exprMgr, opts, threadOpts);
-  } else {
-    exprMgr = new ExprManager(opts);
-    pExecutor = new CommandExecutor(*exprMgr, opts);
+  if (useParallelExecutor)
+  {
+    solver.reset(&threadOpts[0]);
+    pExecutor = new CommandExecutorPortfolio(solver.get(), opts, threadOpts);
+  }
+  else
+  {
+    solver.reset(&opts);
+    pExecutor = new CommandExecutor(solver.get(), opts);
   }
 # endif
 
   std::unique_ptr<Parser> replayParser;
-  if( opts.getReplayInputFilename() != "" ) {
+  if (opts.getReplayInputFilename() != "")
+  {
     std::string replayFilename = opts.getReplayInputFilename();
-    ParserBuilder replayParserBuilder(exprMgr, replayFilename, opts);
+    ParserBuilder replayParserBuilder(solver.get(), replayFilename, opts);
 
     if( replayFilename == "-") {
       if( inputFromStdin ) {
@@ -281,7 +286,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         delete cmd;
       }
 #endif /* PORTFOLIO_BUILD */
-      InteractiveShell shell(*exprMgr);
+      InteractiveShell shell(solver.get());
       if(opts.getInteractivePrompt()) {
         Message() << Configuration::getPackageName()
                   << " " << Configuration::getVersionString();
@@ -334,7 +339,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         // delete cmd;
       }
 
-      ParserBuilder parserBuilder(exprMgr, filename, opts);
+      ParserBuilder parserBuilder(solver.get(), filename, opts);
 
       if( inputFromStdin ) {
 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
@@ -491,7 +496,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         delete cmd;
       }
 
-      ParserBuilder parserBuilder(exprMgr, filename, opts);
+      ParserBuilder parserBuilder(solver.get(), filename, opts);
 
       if( inputFromStdin ) {
 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
@@ -578,7 +583,6 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   // need to be around in that case for main() to print statistics.
   delete pTotalTime;
   delete pExecutor;
-  delete exprMgr;
 
   pTotalTime = NULL;
   pExecutor = NULL;
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 2cec42fbf..aeccd3a64 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -37,6 +37,7 @@
 #  endif /* HAVE_EXT_STDIO_FILEBUF_H */
 #endif /* HAVE_LIBREADLINE */
 
+#include "api/cvc4cpp.h"
 #include "base/output.h"
 #include "options/language.h"
 #include "options/options.h"
@@ -87,13 +88,13 @@ static set<string> s_declarations;
 
 #endif /* HAVE_LIBREADLINE */
 
-InteractiveShell::InteractiveShell(ExprManager& exprManager)
-    : d_options(exprManager.getOptions()),
+InteractiveShell::InteractiveShell(api::Solver* solver)
+    : d_options(solver->getExprManager()->getOptions()),
       d_in(*d_options.getIn()),
       d_out(*d_options.getOutConst()),
       d_quit(false)
 {
-  ParserBuilder parserBuilder(&exprManager, INPUT_FILENAME, d_options);
+  ParserBuilder parserBuilder(solver, INPUT_FILENAME, d_options);
   /* Create parser with bogus input. */
   d_parser = parserBuilder.withStringInput("").build();
   if(d_options.wasSetByUserForceLogicString()) {
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index 203dfb766..ac52a78c4 100644
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -25,9 +25,12 @@
 namespace CVC4 {
 
 class Command;
-class ExprManager;
 class Options;
 
+namespace api {
+class Solver;
+}
+
 namespace parser {
   class Parser;
 }/* CVC4::parser namespace */
@@ -47,7 +50,7 @@ class CVC4_PUBLIC InteractiveShell
   static const unsigned s_historyLimit = 500;
 
 public:
- InteractiveShell(ExprManager& exprManager);
+ InteractiveShell(api::Solver* solver);
 
  /**
   * Close out the interactive session.