Decouple parser creation from input selection (#6533)

This commit decouples the creation of a `Parser` instance from creating
an `Input` and setting the `Input` on the parser. This is a first step
in refactoring the parser infrastructure. A future PR will split the
parser class into three classes: `Parser`, `ParserState`, and
`InputParser`. The `Parser` and `InputParser` classes will be the
public-facing classes. The new `Parser` class will have methods to
create `InputParser`s from files, streams, and strings. `InputParser`s
will have methods to get commands/exprs from a given input. The
`ParserState` class will keep track of the state of the parser and will
be the internal interface for the parsers. The current `Parser` class is
used both publicly and internally, which is messy.

1 files changed, 16 insertions, 8 deletions

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index f27bf03f0..a26ee3b73 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -259,16 +259,20 @@ int runCvc5(int argc, char* argv[], Options& opts)
 
       ParserBuilder parserBuilder(pExecutor->getSolver(),
                                   pExecutor->getSymbolManager(),
-                                  filename,
                                   opts);
-
+      std::unique_ptr<Parser> parser(parserBuilder.build());
       if( inputFromStdin ) {
-        parserBuilder.withStreamInput(cin);
+        parser->setInput(
+            Input::newStreamInput(opts.getInputLanguage(), cin, filename));
+      }
+      else
+      {
+        parser->setInput(Input::newFileInput(
+            opts.getInputLanguage(), filename, opts.getMemoryMap()));
       }
 
       vector< vector<Command*> > allCommands;
       allCommands.push_back(vector<Command*>());
-      std::unique_ptr<Parser> parser(parserBuilder.build());
       int needReset = 0;
       // true if one of the commands was interrupted
       bool interrupted = false;
@@ -411,14 +415,18 @@ int runCvc5(int argc, char* argv[], Options& opts)
 
       ParserBuilder parserBuilder(pExecutor->getSolver(),
                                   pExecutor->getSymbolManager(),
-                                  filename,
                                   opts);
-
+      std::unique_ptr<Parser> parser(parserBuilder.build());
       if( inputFromStdin ) {
-        parserBuilder.withStreamInput(cin);
+        parser->setInput(
+            Input::newStreamInput(opts.getInputLanguage(), cin, filename));
+      }
+      else
+      {
+        parser->setInput(Input::newFileInput(
+            opts.getInputLanguage(), filename, opts.getMemoryMap()));
       }
 
-      std::unique_ptr<Parser> parser(parserBuilder.build());
       bool interrupted = false;
       while (status)
       {