Add new interface for parsing inputs

This commit introduces the `InputParser` class, which is now the main
interface for retrieving commands and expressions from parsers for a
given input. The idea is that a `Parser` can be used to parse multiple
inputs (e.g., in the interactive shell) and that the
commands/expressions in each input can be retrieved using an
`InputParser`.

2 files changed, 28 insertions, 8 deletions

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 697e86fe2..8512f55eb 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -69,6 +69,33 @@ 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 a7674ea63..a22b24a0c 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -252,18 +252,11 @@ class CVC5_EXPORT Parser
   api::Solver* getSolver() const;
 
   /** Get the associated input. */
-  Input* getInput() const { return d_input.get(); }
+  Input* getInput() const { return d_input; }
 
   /** 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.