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.

4 files changed, 64 insertions, 63 deletions

diff --git a/test/api/ouroborous.cpp b/test/api/ouroborous.cpp
index b51982d59..c226da13b 100644
--- a/test/api/ouroborous.cpp
+++ b/test/api/ouroborous.cpp
@@ -102,10 +102,10 @@ std::string parse(std::string instr,
   solver.setOption("input-language", input_language);
   solver.setOption("output-language", output_language);
   SymbolManager symman(&solver);
-  Parser* parser = ParserBuilder(&solver, &symman, "internal-buffer")
-                       .withStringInput(declarations)
-                       .withInputLanguage(ilang)
-                       .build();
+  std::unique_ptr<Parser> parser(
+      ParserBuilder(&solver, &symman).withInputLanguage(ilang).build());
+  parser->setInput(
+      Input::newStringInput(ilang, declarations, "internal-buffer"));
   // we don't need to execute the commands, but we DO need to parse them to
   // get the declarations
   while (Command* c = parser->nextCommand())
@@ -117,7 +117,6 @@ std::string parse(std::string instr,
   api::Term e = parser->nextExpression();
   std::string s = e.toString();
   assert(parser->nextExpression().isNull());  // next expr should be null
-  delete parser;
   return s;
 }
 
diff --git a/test/api/smt2_compliance.cpp b/test/api/smt2_compliance.cpp
index 431bde7d6..04b366cf0 100644
--- a/test/api/smt2_compliance.cpp
+++ b/test/api/smt2_compliance.cpp
@@ -60,8 +60,11 @@ void testGetInfo(api::Solver* solver, const char* s)
 {
   std::unique_ptr<SymbolManager> symman(new SymbolManager(solver));
 
-  ParserBuilder pb(solver, symman.get(), "<internal>", solver->getOptions());
-  Parser* p = pb.withStringInput(string("(get-info ") + s + ")").build();
+  std::unique_ptr<Parser> p(
+      ParserBuilder(solver, symman.get(), solver->getOptions()).build());
+  p->setInput(Input::newStringInput(language::input::LANG_SMTLIB_V2,
+                                    string("(get-info ") + s + ")",
+                                    "<internal>"));
   assert(p != NULL);
   Command* c = p->nextCommand();
   assert(c != NULL);
@@ -69,7 +72,6 @@ void testGetInfo(api::Solver* solver, const char* s)
   stringstream ss;
   c->invoke(solver, symman.get(), ss);
   assert(p->nextCommand() == NULL);
-  delete p;
   delete c;
   cout << ss.str() << endl << endl;
 }
diff --git a/test/unit/parser/parser_black.cpp b/test/unit/parser/parser_black.cpp
index b6c433663..78a67f6d0 100644
--- a/test/unit/parser/parser_black.cpp
+++ b/test/unit/parser/parser_black.cpp
@@ -86,11 +86,11 @@ class TestParserBlackParser : public TestInternal
   void tryGoodInput(const std::string goodInput)
   {
     d_symman.reset(new SymbolManager(d_solver.get()));
-    Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
-                         .withStringInput(goodInput)
-                         .withOptions(d_options)
-                         .withInputLanguage(d_lang)
-                         .build();
+    std::unique_ptr<Parser> parser(ParserBuilder(d_solver.get(), d_symman.get())
+                                       .withOptions(d_options)
+                                       .withInputLanguage(d_lang)
+                                       .build());
+    parser->setInput(Input::newStringInput(d_lang, goodInput, "test"));
     ASSERT_FALSE(parser->done());
     Command* cmd;
     while ((cmd = parser->nextCommand()) != NULL)
@@ -100,18 +100,17 @@ class TestParserBlackParser : public TestInternal
     }
 
     ASSERT_TRUE(parser->done());
-    delete parser;
   }
 
   void tryBadInput(const std::string badInput, bool strictMode = false)
   {
     d_symman.reset(new SymbolManager(d_solver.get()));
-    Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
-                         .withStringInput(badInput)
-                         .withOptions(d_options)
-                         .withInputLanguage(d_lang)
-                         .withStrictMode(strictMode)
-                         .build();
+    std::unique_ptr<Parser> parser(ParserBuilder(d_solver.get(), d_symman.get())
+                                       .withOptions(d_options)
+                                       .withInputLanguage(d_lang)
+                                       .withStrictMode(strictMode)
+                                       .build());
+    parser->setInput(Input::newStringInput(d_lang, badInput, "test"));
     ASSERT_THROW(
         {
           Command* cmd;
@@ -123,23 +122,21 @@ class TestParserBlackParser : public TestInternal
           std::cout << "\nBad input succeeded:\n" << badInput << std::endl;
         },
         ParserException);
-    delete parser;
   }
 
   void tryGoodExpr(const std::string goodExpr)
   {
     d_symman.reset(new SymbolManager(d_solver.get()));
-    Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
-                         .withStringInput(goodExpr)
-                         .withOptions(d_options)
-                         .withInputLanguage(d_lang)
-                         .build();
-
+    std::unique_ptr<Parser> parser(ParserBuilder(d_solver.get(), d_symman.get())
+                                       .withOptions(d_options)
+                                       .withInputLanguage(d_lang)
+                                       .build());
+    parser->setInput(Input::newStringInput(d_lang, goodExpr, "test"));
     if (d_lang == LANG_SMTLIB_V2)
     {
       /* Use QF_LIA to make multiplication ("*") available */
       std::unique_ptr<Command> cmd(
-          static_cast<Smt2*>(parser)->setLogic("QF_LIA"));
+          static_cast<Smt2*>(parser.get())->setLogic("QF_LIA"));
     }
 
     ASSERT_FALSE(parser->done());
@@ -150,7 +147,6 @@ class TestParserBlackParser : public TestInternal
     e = parser->nextExpression();
     ASSERT_TRUE(parser->done());
     ASSERT_TRUE(e.isNull());
-    delete parser;
   }
 
   /**
@@ -165,12 +161,12 @@ class TestParserBlackParser : public TestInternal
   void tryBadExpr(const std::string badExpr, bool strictMode = false)
   {
     d_symman.reset(new SymbolManager(d_solver.get()));
-    Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
-                         .withStringInput(badExpr)
-                         .withOptions(d_options)
-                         .withInputLanguage(d_lang)
-                         .withStrictMode(strictMode)
-                         .build();
+    std::unique_ptr<Parser> parser(ParserBuilder(d_solver.get(), d_symman.get())
+                                       .withOptions(d_options)
+                                       .withInputLanguage(d_lang)
+                                       .withStrictMode(strictMode)
+                                       .build());
+    parser->setInput(Input::newStringInput(d_lang, badExpr, "test"));
     setupContext(*parser);
     ASSERT_FALSE(parser->done());
     ASSERT_THROW(api::Term e = parser->nextExpression();
@@ -179,7 +175,6 @@ class TestParserBlackParser : public TestInternal
                            << "Input: <<" << badExpr << ">>" << std::endl
                            << "Output: <<" << e << ">>" << std::endl;
                  , ParserException);
-    delete parser;
   }
 
   Options d_options;
diff --git a/test/unit/parser/parser_builder_black.cpp b/test/unit/parser/parser_builder_black.cpp
index 4ed036202..fa532f6b6 100644
--- a/test/unit/parser/parser_builder_black.cpp
+++ b/test/unit/parser/parser_builder_black.cpp
@@ -40,28 +40,19 @@ class TestParseBlackParserBuilder : public TestApi
  protected:
   void SetUp() override { d_symman.reset(new SymbolManager(&d_solver)); }
 
-  void checkEmptyInput(ParserBuilder& builder)
+  void checkEmptyInput(Parser* parser)
   {
-    Parser* parser = builder.build();
-    ASSERT_NE(parser, nullptr);
-
     api::Term e = parser->nextExpression();
     ASSERT_TRUE(e.isNull());
-
-    delete parser;
   }
 
-  void checkTrueInput(ParserBuilder& builder)
+  void checkTrueInput(Parser* parser)
   {
-    Parser* parser = builder.build();
-    ASSERT_NE(parser, nullptr);
-
     api::Term e = parser->nextExpression();
     ASSERT_EQ(e, d_solver.mkTrue());
 
     e = parser->nextExpression();
     ASSERT_TRUE(e.isNull());
-    delete parser;
   }
 
   char* mkTemp()
@@ -80,8 +71,11 @@ TEST_F(TestParseBlackParserBuilder, empty_file_input)
   char* filename = mkTemp();
   ASSERT_NE(filename, nullptr);
 
-  checkEmptyInput(ParserBuilder(&d_solver, d_symman.get(), filename)
-                      .withInputLanguage(LANG_CVC));
+  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());
 
   remove(filename);
   free(filename);
@@ -95,8 +89,11 @@ TEST_F(TestParseBlackParserBuilder, simple_file_input)
   fs << "TRUE" << std::endl;
   fs.close();
 
-  checkTrueInput(ParserBuilder(&d_solver, d_symman.get(), filename)
-                     .withInputLanguage(LANG_CVC));
+  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());
 
   remove(filename);
   free(filename);
@@ -104,32 +101,40 @@ TEST_F(TestParseBlackParserBuilder, simple_file_input)
 
 TEST_F(TestParseBlackParserBuilder, empty_string_input)
 {
-  checkEmptyInput(ParserBuilder(&d_solver, d_symman.get(), "foo")
-                      .withInputLanguage(LANG_CVC)
-                      .withStringInput(""));
+  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());
 }
 
 TEST_F(TestParseBlackParserBuilder, true_string_input)
 {
-  checkTrueInput(ParserBuilder(&d_solver, d_symman.get(), "foo")
-                     .withInputLanguage(LANG_CVC)
-                     .withStringInput("TRUE"));
+  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());
 }
 
 TEST_F(TestParseBlackParserBuilder, empty_stream_input)
 {
   std::stringstream ss("", std::ios_base::in);
-  checkEmptyInput(ParserBuilder(&d_solver, d_symman.get(), "foo")
-                      .withInputLanguage(LANG_CVC)
-                      .withStreamInput(ss));
+  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());
 }
 
 TEST_F(TestParseBlackParserBuilder, true_stream_input)
 {
   std::stringstream ss("TRUE", std::ios_base::in);
-  checkTrueInput(ParserBuilder(&d_solver, d_symman.get(), "foo")
-                     .withInputLanguage(LANG_CVC)
-                     .withStreamInput(ss));
+  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());
 }
 
 }  // namespace test