Add new interface for parsing inputsinput-parser

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, 32 insertions, 26 deletions

diff --git a/test/unit/parser/parser_black.cpp b/test/unit/parser/parser_black.cpp
index 78a67f6d0..a0cd0499e 100644
--- a/test/unit/parser/parser_black.cpp
+++ b/test/unit/parser/parser_black.cpp
@@ -21,6 +21,7 @@
 #include "options/base_options.h"
 #include "options/language.h"
 #include "options/options.h"
+#include "parser/input_parser.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
 #include "parser/smt2/smt2.h"
@@ -90,10 +91,11 @@ class TestParserBlackParser : public TestInternal
                                        .withOptions(d_options)
                                        .withInputLanguage(d_lang)
                                        .build());
-    parser->setInput(Input::newStringInput(d_lang, goodInput, "test"));
+    std::unique_ptr<InputParser> inputParser =
+        parser->parseString("test", goodInput);
     ASSERT_FALSE(parser->done());
     Command* cmd;
-    while ((cmd = parser->nextCommand()) != NULL)
+    while ((cmd = inputParser->nextCommand()) != NULL)
     {
       Debug("parser") << "Parsed command: " << (*cmd) << std::endl;
       delete cmd;
@@ -110,11 +112,12 @@ class TestParserBlackParser : public TestInternal
                                        .withInputLanguage(d_lang)
                                        .withStrictMode(strictMode)
                                        .build());
-    parser->setInput(Input::newStringInput(d_lang, badInput, "test"));
+    std::unique_ptr<InputParser> inputParser =
+        parser->parseString("test", badInput);
     ASSERT_THROW(
         {
           Command* cmd;
-          while ((cmd = parser->nextCommand()) != NULL)
+          while ((cmd = inputParser->nextCommand()) != NULL)
           {
             Debug("parser") << "Parsed command: " << (*cmd) << std::endl;
             delete cmd;
@@ -131,7 +134,8 @@ class TestParserBlackParser : public TestInternal
                                        .withOptions(d_options)
                                        .withInputLanguage(d_lang)
                                        .build());
-    parser->setInput(Input::newStringInput(d_lang, goodExpr, "test"));
+    std::unique_ptr<InputParser> inputParser =
+        parser->parseString("test", goodExpr);
     if (d_lang == LANG_SMTLIB_V2)
     {
       /* Use QF_LIA to make multiplication ("*") available */
@@ -142,9 +146,9 @@ class TestParserBlackParser : public TestInternal
     ASSERT_FALSE(parser->done());
     setupContext(*parser);
     ASSERT_FALSE(parser->done());
-    api::Term e = parser->nextExpression();
+    api::Term e = inputParser->nextExpression();
     ASSERT_FALSE(e.isNull());
-    e = parser->nextExpression();
+    e = inputParser->nextExpression();
     ASSERT_TRUE(parser->done());
     ASSERT_TRUE(e.isNull());
   }
@@ -166,10 +170,11 @@ class TestParserBlackParser : public TestInternal
                                        .withInputLanguage(d_lang)
                                        .withStrictMode(strictMode)
                                        .build());
-    parser->setInput(Input::newStringInput(d_lang, badExpr, "test"));
+    std::unique_ptr<InputParser> inputParser =
+        parser->parseString("test", badExpr);
     setupContext(*parser);
     ASSERT_FALSE(parser->done());
-    ASSERT_THROW(api::Term e = parser->nextExpression();
+    ASSERT_THROW(api::Term e = inputParser->nextExpression();
                  std::cout << std::endl
                            << "Bad expr succeeded." << std::endl
                            << "Input: <<" << badExpr << ">>" << std::endl
diff --git a/test/unit/parser/parser_builder_black.cpp b/test/unit/parser/parser_builder_black.cpp
index fa532f6b6..f8d29efbe 100644
--- a/test/unit/parser/parser_builder_black.cpp
+++ b/test/unit/parser/parser_builder_black.cpp
@@ -24,6 +24,7 @@
 #include "api/cpp/cvc5.h"
 #include "expr/symbol_manager.h"
 #include "options/language.h"
+#include "parser/input_parser.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
 #include "test_api.h"
@@ -40,18 +41,18 @@ class TestParseBlackParserBuilder : public TestApi
  protected:
   void SetUp() override { d_symman.reset(new SymbolManager(&d_solver)); }
 
-  void checkEmptyInput(Parser* parser)
+  void checkEmptyInput(InputParser* inputParser)
   {
-    api::Term e = parser->nextExpression();
+    api::Term e = inputParser->nextExpression();
     ASSERT_TRUE(e.isNull());
   }
 
-  void checkTrueInput(Parser* parser)
+  void checkTrueInput(InputParser* inputParser)
   {
-    api::Term e = parser->nextExpression();
+    api::Term e = inputParser->nextExpression();
     ASSERT_EQ(e, d_solver.mkTrue());
 
-    e = parser->nextExpression();
+    e = inputParser->nextExpression();
     ASSERT_TRUE(e.isNull());
   }
 
@@ -74,8 +75,8 @@ TEST_F(TestParseBlackParserBuilder, empty_file_input)
   std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get())
                                      .withInputLanguage(LANG_CVC)
                                      .build());
-  parser->setInput(Input::newFileInput(LANG_CVC, filename, false));
-  checkEmptyInput(parser.get());
+  std::unique_ptr<InputParser> inputParser = parser->parseFile(filename, false);
+  checkEmptyInput(inputParser.get());
 
   remove(filename);
   free(filename);
@@ -92,8 +93,8 @@ TEST_F(TestParseBlackParserBuilder, simple_file_input)
   std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get())
                                      .withInputLanguage(LANG_CVC)
                                      .build());
-  parser->setInput(Input::newFileInput(LANG_CVC, filename, false));
-  checkTrueInput(parser.get());
+  std::unique_ptr<InputParser> inputParser = parser->parseFile(filename, false);
+  checkTrueInput(inputParser.get());
 
   remove(filename);
   free(filename);
@@ -104,8 +105,8 @@ TEST_F(TestParseBlackParserBuilder, empty_string_input)
   std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get())
                                      .withInputLanguage(LANG_CVC)
                                      .build());
-  parser->setInput(Input::newStringInput(LANG_CVC, "", "foo"));
-  checkEmptyInput(parser.get());
+  std::unique_ptr<InputParser> inputParser = parser->parseString("foo", "");
+  checkEmptyInput(inputParser.get());
 }
 
 TEST_F(TestParseBlackParserBuilder, true_string_input)
@@ -113,8 +114,8 @@ TEST_F(TestParseBlackParserBuilder, true_string_input)
   std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get())
                                      .withInputLanguage(LANG_CVC)
                                      .build());
-  parser->setInput(Input::newStringInput(LANG_CVC, "TRUE", "foo"));
-  checkTrueInput(parser.get());
+  std::unique_ptr<InputParser> inputParser = parser->parseString("foo", "TRUE");
+  checkTrueInput(inputParser.get());
 }
 
 TEST_F(TestParseBlackParserBuilder, empty_stream_input)
@@ -123,8 +124,8 @@ TEST_F(TestParseBlackParserBuilder, empty_stream_input)
   std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get())
                                      .withInputLanguage(LANG_CVC)
                                      .build());
-  parser->setInput(Input::newStreamInput(LANG_CVC, ss, "foo"));
-  checkEmptyInput(parser.get());
+  std::unique_ptr<InputParser> inputParser = parser->parseStream("foo", ss);
+  checkEmptyInput(inputParser.get());
 }
 
 TEST_F(TestParseBlackParserBuilder, true_stream_input)
@@ -133,8 +134,8 @@ TEST_F(TestParseBlackParserBuilder, true_stream_input)
   std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get())
                                      .withInputLanguage(LANG_CVC)
                                      .build());
-  parser->setInput(Input::newStreamInput(LANG_CVC, ss, "foo"));
-  checkTrueInput(parser.get());
+  std::unique_ptr<InputParser> inputParser = parser->parseStream("foo", ss);
+  checkTrueInput(inputParser.get());
 }
 
 }  // namespace test