Decouple parser creation from input selection

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.

3 files changed, 8 insertions, 40 deletions

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 8512f55eb..697e86fe2 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -69,33 +69,6 @@ Parser::~Parser() {
   d_commandQueue.clear();
 }
 
-std::unique_ptr<InputParser> Parser::parseFile(const std::string& fname,
-                                               bool useMmap)
-{
-  d_input = Input::newFileInput(d_lang, fname, useMmap);
-  d_input->setParser(*this);
-  d_done = false;
-  return std::unique_ptr<InputParser>(new InputParser(this, d_input));
-}
-
-std::unique_ptr<InputParser> Parser::parseStream(const std::string& name,
-                                                 std::istream& stream)
-{
-  d_input = Input::newStreamInput(d_lang, stream, name);
-  d_input->setParser(*this);
-  d_done = false;
-  return std::unique_ptr<InputParser>(new InputParser(this, d_input));
-}
-
-std::unique_ptr<InputParser> Parser::parseString(const std::string& name,
-                                                 const std::string& str)
-{
-  d_input = Input::newStringInput(d_lang, str, name);
-  d_input->setParser(*this);
-  d_done = false;
-  return std::unique_ptr<InputParser>(new InputParser(this, d_input));
-}
-
 api::Solver* Parser::getSolver() const { return d_solver; }
 
 api::Term Parser::getSymbol(const std::string& name, SymbolType type)
diff --git a/src/parser/parser.h b/src/parser/parser.h
index a22b24a0c..a7674ea63 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -252,11 +252,18 @@ class CVC5_EXPORT Parser
   api::Solver* getSolver() const;
 
   /** Get the associated input. */
-  Input* getInput() const { return d_input; }
+  Input* getInput() const { return d_input.get(); }
 
   /** Get unresolved sorts */
   inline std::set<api::Sort>& getUnresolvedSorts() { return d_unresolved; }
 
+  /** Deletes and replaces the current parser input. */
+  void setInput(Input* input)  {
+    d_input.reset(input);
+    d_input->setParser(*this);
+    d_done = false;
+  }
+
   /**
    * Check if we are done -- either the end of input has been reached, or some
    * error has been encountered.
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index ee918ae43..992ca408a 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -44,18 +44,6 @@ class Parser;
  */
 class CVC5_EXPORT ParserBuilder
 {
-<<<<<<< HEAD
-=======
-  enum InputType {
-    FILE_INPUT,
-    STREAM_INPUT,
-    STRING_INPUT
-  };
-
-  /** The input type. */
-  InputType d_inputType;
-
->>>>>>> 81404ddfc (Always parse streams with line buffer)
   /** The input language */
   InputLanguage d_lang;