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.

2 files changed, 9 insertions, 8 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;
 }