Split parser state from parser classparser-state

This commit splits the parser state from the parser class.

4 files changed, 7 insertions, 23 deletions

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index b94b49db3..12a86be82 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -37,7 +37,6 @@
 #include "options/set_language.h"
 #include "parser/input_parser.h"
 #include "parser/parser.h"
-#include "parser/parser_builder.h"
 #include "smt/command.h"
 #include "smt/smt_engine.h"
 #include "util/result.h"
@@ -258,10 +257,8 @@ int runCvc5(int argc, char* argv[], Options& opts)
         // pExecutor->doCommand(cmd);
       }
 
-      ParserBuilder parserBuilder(pExecutor->getSolver(),
-                                  pExecutor->getSymbolManager(),
-                                  opts);
-      std::unique_ptr<Parser> parser(parserBuilder.build());
+      std::unique_ptr<Parser> parser(new Parser(
+          pExecutor->getSolver(), pExecutor->getSymbolManager(), opts));
       std::unique_ptr<InputParser> inputParser;
       if( inputFromStdin ) {
         inputParser = parser->parseStream(filename, cin);
@@ -413,10 +410,8 @@ int runCvc5(int argc, char* argv[], Options& opts)
         pExecutor->doCommand(cmd);
       }
 
-      ParserBuilder parserBuilder(pExecutor->getSolver(),
-                                  pExecutor->getSymbolManager(),
-                                  opts);
-      std::unique_ptr<Parser> parser(parserBuilder.build());
+      std::unique_ptr<Parser> parser(new Parser(
+          pExecutor->getSolver(), pExecutor->getSymbolManager(), opts));
       std::unique_ptr<InputParser> inputParser;
       if( inputFromStdin ) {
         inputParser = parser->parseStream(filename, cin);
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 1b3ad643b..0abcb72f0 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -47,7 +47,6 @@
 #include "parser/input.h"
 #include "parser/input_parser.h"
 #include "parser/parser.h"
-#include "parser/parser_builder.h"
 #include "smt/command.h"
 #include "theory/logic_info.h"
 
@@ -94,13 +93,7 @@ InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm)
       d_out(*d_options.getOutConst()),
       d_quit(false)
 {
-  ParserBuilder parserBuilder(solver, sm, d_options);
-  /* Create parser with bogus input. */
-  d_parser = parserBuilder.build();
-  if(d_options.wasSetByUserForceLogicString()) {
-    LogicInfo tmp(d_options.getForceLogicString());
-    d_parser->forceLogic(tmp.getLogicString());
-  }
+  d_parser.reset(new Parser(solver, sm, d_options));
 
 #if HAVE_LIBEDITLINE
   if(&d_in == &cin) {
@@ -172,7 +165,6 @@ InteractiveShell::~InteractiveShell() {
              << ": " << strerror(err) << std::endl;
   }
 #endif /* HAVE_LIBEDITLINE */
-  delete d_parser;
 }
 
 Command* InteractiveShell::readCommand()
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index cf5f22b51..856106187 100644
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -43,7 +43,7 @@ class InteractiveShell
   const Options& d_options;
   std::istream& d_in;
   std::ostream& d_out;
-  parser::Parser* d_parser;
+  std::unique_ptr<parser::Parser> d_parser;
   bool d_quit;
   bool d_usingEditline;
 
@@ -69,7 +69,7 @@ public:
  /**
   * Return the internal parser being used.
   */
- parser::Parser* getParser() { return d_parser; }
+ parser::Parser* getParser() { return d_parser.get(); }
 
 };/* class InteractiveShell */
 
diff --git a/src/main/main.cpp b/src/main/main.cpp
index b96598b0b..20d542de2 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -24,13 +24,10 @@
 #include "base/configuration.h"
 #include "base/output.h"
 #include "main/command_executor.h"
-#include "main/interactive_shell.h"
 #include "options/language.h"
 #include "options/option_exception.h"
 #include "options/options.h"
 #include "parser/parser.h"
-#include "parser/parser_builder.h"
-#include "parser/parser_exception.h"
 #include "util/result.h"
 
 using namespace std;