Adding ParserBuilder, reducing visibility of Parser and Input constructors

Adding Smt2 subclass of Parser
Checking for multiple calls to set-logic in SMT v2

12 files changed, 382 insertions, 119 deletions

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 19e1d0cff..a16db2411 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -22,8 +22,8 @@
 #include "cvc4autoconfig.h"
 #include "main.h"
 #include "usage.h"
-#include "parser/input.h"
 #include "parser/parser.h"
+#include "parser/parser_builder.h"
 #include "expr/expr_manager.h"
 #include "smt/smt_engine.h"
 #include "expr/command.h"
@@ -149,29 +149,19 @@ int runCvc4(int argc, char* argv[]) {
     }
   }
 
-  // Create the parser
-  Input* input;
-
   /* TODO: Hack ANTLR3 to support input from streams */
-//  if(inputFromStdin) {
-    //    parser = Parser::getNewParser(&exprMgr, options.lang, cin, "<stdin>");
-//  } else {
-    input = Input::newFileInput(options.lang, argv[firstArgIndex],
-                                     options.memoryMap);
-//  }
-  Parser parser(&exprMgr, input);
-
-  if(!options.semanticChecks || Configuration::isMuzzledBuild()) {
-    parser.disableChecks();
-  }
+  ParserBuilder parserBuilder(options.lang,  argv[firstArgIndex]);
 
-  if( options.strictParsing ) {
-    parser.enableStrictMode();
-  }
+  Parser *parser =
+      parserBuilder.withExprManager(exprMgr)
+        .withMmap(options.memoryMap)
+        .withChecks(options.semanticChecks && !Configuration::isMuzzledBuild() )
+        .withStrictMode( options.strictParsing )
+        .build();
 
   // Parse and execute commands until we are done
   Command* cmd;
-  while((cmd = parser.nextCommand())) {
+  while((cmd = parser->nextCommand())) {
     if( !options.parseOnly ) {
       doCommand(smt, cmd);
     }
@@ -179,7 +169,7 @@ int runCvc4(int argc, char* argv[]) {
   }
 
   // Remove the parser
-  delete input;
+  delete parser;
 
   switch(lastResult.asSatisfiabilityResult().isSAT()) {
 
diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index 7029c01e5..f95b01b8c 100644
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -48,6 +48,8 @@ libcvc4parser_noinst_la_SOURCES = \
 	memory_mapped_input_buffer.cpp \
     parser.h \
     parser.cpp \
+    parser_builder.h \
+    parser_builder.cpp \
     parser_options.h \
     parser_exception.h
 
diff --git a/src/parser/input.h b/src/parser/input.h
index 114880bb0..ccae2d84b 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -75,6 +75,7 @@ class Parser;
  */
 class CVC4_PUBLIC Input {
   friend class Parser; // for parseError, parseCommand, parseExpr
+  friend class ParserBuilder;
 
   /** The input stream. */
   InputStream *d_inputStream;
@@ -85,11 +86,6 @@ class CVC4_PUBLIC Input {
   Input(const Input& input) { Unimplemented("Copy constructor for Input."); }
   Input& operator=(const Input& input) { Unimplemented("operator= for Input."); }
 
-public:
-
-  /** Destructor. Frees the token stream and closes the input. */
-  virtual ~Input();
-
   /** Create an input for the given file.
     *
     * @param lang the input language
@@ -116,6 +112,11 @@ public:
   static Input* newStringInput(InputLanguage lang, const std::string& input, const std::string& name)
     throw (InputStreamException);
 
+public:
+
+  /** Destructor. Frees the token stream and closes the input. */
+  virtual ~Input();
+
 protected:
 
   /** Create an input.
diff --git a/src/parser/parser.h b/src/parser/parser.h
index c191d9f39..e6e5a2250 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -95,6 +95,7 @@ inline std::string toString(SymbolType type) {
  * declarations.
  */
 class CVC4_PUBLIC Parser {
+  friend class ParserBuilder;
 
   /** The expression manager */
   ExprManager *d_exprManager;
@@ -123,15 +124,20 @@ class CVC4_PUBLIC Parser {
   /** Lookup a symbol in the given namespace. */
   Expr getSymbol(const std::string& var_name, SymbolType type);
 
-public:
-  /** Create a parser state.
+protected:
+  /** Create a parser state. NOTE: The parser takes "ownership" of the given
+   * input and will delete it on destruction.
    *
    * @param exprManager the expression manager to use when creating expressions
    * @param input the parser input
    */
   Parser(ExprManager* exprManager, Input* input, bool strictMode = false);
 
-  virtual ~Parser() { }
+public:
+
+  virtual ~Parser() {
+    delete d_input;
+  }
 
   /** Get the associated <code>ExprManager</code>. */
   inline ExprManager* getExprManager() const {
@@ -145,9 +151,9 @@ public:
 
   /** Set the declaration scope manager for this input. NOTE: This should <em>only</me> be
    * called before parsing begins. Otherwise, previous declarations will be lost. */
-  inline void setDeclarationScope(DeclarationScope declScope) {
+/*  inline void setDeclarationScope(DeclarationScope declScope) {
     d_declScope = declScope;
-  }
+  }*/
 
   /**
    * Check if we are done -- either the end of input has been reached, or some
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
new file mode 100644
index 000000000..b2bb15a6a
--- /dev/null
+++ b/src/parser/parser_builder.cpp
@@ -0,0 +1,141 @@
+/*********************                                                        */
+/** parser_builder.cpp
+ ** Original author: cconway
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** A builder for parsers.
+ **/
+
+#include <string>
+
+#include "parser_builder.h"
+#include "expr/expr_manager.h"
+#include "parser/input.h"
+#include "parser/parser.h"
+#include "parser/smt2/smt2.h"
+
+namespace CVC4 {
+
+namespace parser {
+
+/*class FileInputBuilder : public InputBuilder {
+  bool d_useMmap;
+public:
+  FileInputBuilder(InputLanguage lang, const std::string& filename, bool useMmap) :
+    InputBuilder(lang,filename),
+    d_useMmap(useMmap) {
+  }
+  ParserBuilder& useMmap();
+
+  Input& build() {
+    return Input::newFileInput(d_lang,d_name,d_useMmap);
+  }
+};
+
+class StringInputBuilder : public InputBuilder {
+  std::string d_input;
+public:
+  StringInputBuilder(InputLanguage lang, const std::string& input, const std::string& name) :
+    InputBuilder(lang,name),
+    d_input(input) {
+  }
+
+  Input& build() {
+    return Input::newStringInput(lang,input,name);
+  }
+};*/
+
+ParserBuilder::ParserBuilder(InputLanguage lang, const std::string& filename) :
+    d_inputType(FILE_INPUT),
+    d_lang(lang),
+    d_filename(filename),
+    d_exprManager(NULL),
+    d_checksEnabled(true),
+    d_strictMode(false),
+    d_mmap(false) {
+}
+
+Parser *ParserBuilder::build() throw (InputStreamException) {
+  Input *input;
+  switch( d_inputType ) {
+  case FILE_INPUT:
+    input = Input::newFileInput(d_lang,d_filename,d_mmap);
+    break;
+  case STRING_INPUT:
+    input = Input::newStringInput(d_lang,d_stringInput,d_filename);
+    break;
+  }
+  switch(d_lang) {
+  case LANG_SMTLIB_V2:
+    return new Smt2(d_exprManager, input, d_strictMode);
+  default:
+    return new Parser(d_exprManager, input, d_strictMode);
+  }
+}
+
+/*ParserBuilder& ParserBuilder::disableChecks() {
+  d_checksEnabled = false;
+  return *this;
+}
+
+ParserBuilder& ParserBuilder::disableMmap() {
+  d_mmap = false;
+  return *this;
+}
+
+ParserBuilder& ParserBuilder::disableStrictMode() {
+  d_strictMode = false;
+  return *this;
+}
+
+ParserBuilder& ParserBuilder::enableChecks() {
+  d_checksEnabled = true;
+  return *this;
+}
+
+ParserBuilder& ParserBuilder::enableMmap() {
+  d_mmap = true;
+  return *this;
+}
+
+ParserBuilder& ParserBuilder::enableStrictMode() {
+  d_strictMode = true;
+  return *this;
+}*/
+
+ParserBuilder& ParserBuilder::withChecks(bool flag) {
+  d_checksEnabled = flag;
+  return *this;
+}
+
+ParserBuilder& ParserBuilder::withMmap(bool flag) {
+  d_mmap = flag;
+  return *this;
+}
+
+ParserBuilder& ParserBuilder::withStrictMode(bool flag) {
+  d_strictMode = flag;
+  return *this;
+}
+
+ParserBuilder& ParserBuilder::withExprManager(ExprManager& exprManager) {
+  d_exprManager = &exprManager;
+  return *this;
+}
+
+ParserBuilder& ParserBuilder::withStringInput(const std::string& input) {
+  d_inputType = STRING_INPUT;
+  d_stringInput = input;
+  return *this;
+}
+
+} /* namespace parser */
+
+} /* namespace CVC4 */
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
new file mode 100644
index 000000000..d0b8b7bb2
--- /dev/null
+++ b/src/parser/parser_builder.h
@@ -0,0 +1,91 @@
+/*********************                                                        */
+/** parser_builder.h
+ ** Original author: cconway
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** A builder for parsers.
+ **/
+
+#include "cvc4parser_public.h"
+
+#ifndef __CVC4__PARSER__PARSER_BUILDER_H_
+#define __CVC4__PARSER__PARSER_BUILDER_H_
+
+#include <string>
+
+#include "parser/input.h"
+#include "parser/parser_options.h"
+
+namespace CVC4 {
+
+class ExprManager;
+
+namespace parser {
+/*
+
+class InputBuilder {
+protected:
+  InputLanguage d_lang;
+  std::string d_name;
+public:
+  InputBuilder(InputLanguage lang, const std::string& name) :
+    d_lang(lang),
+    d_name(name) {
+  }
+  virtual Input& build() = 0;
+};
+*/
+
+class Parser;
+
+class CVC4_PUBLIC ParserBuilder {
+  enum InputType {
+    FILE_INPUT,
+    STRING_INPUT
+  };
+
+  /** The input type. */
+  InputType d_inputType;
+
+  /** The input language */
+  InputLanguage d_lang;
+
+  /** The file name (may not exist) */
+  std::string d_filename;
+
+  /** The string input, if any. */
+  std::string d_stringInput;
+
+  /** The expression manager */
+  ExprManager *d_exprManager;
+
+  /** Should semantic checks be enabled during parsing? */
+  bool d_checksEnabled;
+
+  /** Should we parse in strict mode? */
+  bool d_strictMode;
+
+  /** Should we memory-map a file input? */
+  bool d_mmap;
+
+public:
+  ParserBuilder(InputLanguage lang, const std::string& filename);
+  Parser *build() throw (InputStreamException);
+  ParserBuilder& withChecks(bool flag = true);
+  ParserBuilder& withMmap(bool flag = true);
+  ParserBuilder& withStrictMode(bool flag = true);
+  ParserBuilder& withExprManager(ExprManager& exprManager);
+  ParserBuilder& withStringInput(const std::string& input);
+};
+
+} /* namespace parser */
+
+} /* namespace CVC4 */
+#endif /* __CVC4__PARSER__PARSER_BUILDER_H_ */
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index dec052859..105976628 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -52,14 +52,14 @@ options {
 @lexer::postinclude {
 #include <stdint.h>
 
-#include "parser/parser.h"
+#include "parser/smt2/smt2.h"
 #include "parser/antlr_input.h"
 
 using namespace CVC4;
 using namespace CVC4::parser;
 
 #undef PARSER_STATE 
-#define PARSER_STATE ((Parser*)LEXER->super)
+#define PARSER_STATE ((Smt2*)LEXER->super)
 }
 
 @parser::includes {
@@ -89,7 +89,7 @@ using namespace CVC4::parser;
 /* These need to be macros so they can refer to the PARSER macro, which will be defined
  * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */
 #undef PARSER_STATE 
-#define PARSER_STATE ((Parser*)PARSER->super)
+#define PARSER_STATE ((Smt2*)PARSER->super)
 #undef EXPR_MANAGER
 #define EXPR_MANAGER PARSER_STATE->getExprManager()
 #undef MK_EXPR
@@ -132,11 +132,14 @@ command returns [CVC4::Command* cmd]
     SET_LOGIC_TOK SYMBOL
     { name = AntlrInput::tokenText($SYMBOL);
       Debug("parser") << "set logic: '" << name << "' " << std::endl;
-      Smt2::setLogic(*PARSER_STATE,name);
+      if( PARSER_STATE->strictModeEnabled() && PARSER_STATE->logicIsSet() ) {
+        PARSER_STATE->parseError("Only one set-logic is allowed.");
+      }
+      PARSER_STATE->setLogic(name);
       $cmd = new SetBenchmarkLogicCommand(name); }
   | SET_INFO_TOK KEYWORD symbolicExpr[sexpr]
     { name = AntlrInput::tokenText($KEYWORD);
-      Smt2::setInfo(*PARSER_STATE,name,sexpr);    
+      PARSER_STATE->setInfo(name,sexpr);    
       cmd = new SetInfoCommand(name,sexpr); }
   | /* sort declaration */
     DECLARE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] n=INTEGER_LITERAL
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 9fd6588bb..d7da84a43 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -39,15 +39,23 @@ Smt2::Logic Smt2::toLogic(const std::string& name) {
   return logicMap[name];
 }
 
-void Smt2::addArithmeticOperators(Parser& parser) {
-  parser.addOperator(kind::PLUS);
-  parser.addOperator(kind::MINUS);
-  parser.addOperator(kind::UMINUS);
-  parser.addOperator(kind::MULT);
-  parser.addOperator(kind::LT);
-  parser.addOperator(kind::LEQ);
-  parser.addOperator(kind::GT);
-  parser.addOperator(kind::GEQ);
+Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode) :
+  Parser(exprManager,input,strictMode),
+  d_logicSet(false) {
+  if( !strictModeEnabled() ) {
+    addTheory(Smt2::THEORY_CORE);
+  }
+}
+
+void Smt2::addArithmeticOperators() {
+  addOperator(kind::PLUS);
+  addOperator(kind::MINUS);
+  addOperator(kind::UMINUS);
+  addOperator(kind::MULT);
+  addOperator(kind::LT);
+  addOperator(kind::LEQ);
+  addOperator(kind::GT);
+  addOperator(kind::GEQ);
 }
 
 /**
@@ -56,34 +64,34 @@ void Smt2::addArithmeticOperators(Parser& parser) {
  * @param parser the CVC4 Parser object
  * @param theory the theory to open (e.g., Core, Ints)
  */
-void Smt2::addTheory(Parser& parser, Theory theory) {
+void Smt2::addTheory(Theory theory) {
   switch(theory) {
   case THEORY_CORE:
-    parser.defineType("Bool", parser.getExprManager()->booleanType());
-    parser.defineVar("true", parser.getExprManager()->mkConst(true));
-    parser.defineVar("false", parser.getExprManager()->mkConst(false));
-    parser.addOperator(kind::AND);
-    parser.addOperator(kind::EQUAL);
-    parser.addOperator(kind::IFF);
-    parser.addOperator(kind::IMPLIES);
-    parser.addOperator(kind::ITE);
-    parser.addOperator(kind::NOT);
-    parser.addOperator(kind::OR);
-    parser.addOperator(kind::XOR);
+    defineType("Bool", getExprManager()->booleanType());
+    defineVar("true", getExprManager()->mkConst(true));
+    defineVar("false", getExprManager()->mkConst(false));
+    addOperator(kind::AND);
+    addOperator(kind::EQUAL);
+    addOperator(kind::IFF);
+    addOperator(kind::IMPLIES);
+    addOperator(kind::ITE);
+    addOperator(kind::NOT);
+    addOperator(kind::OR);
+    addOperator(kind::XOR);
     break;
 
   case THEORY_REALS_INTS:
-    parser.defineType("Real", parser.getExprManager()->realType());
+    defineType("Real", getExprManager()->realType());
     // falling-through on purpose, to add Ints part of RealsInts
 
   case THEORY_INTS:
-    parser.defineType("Int", parser.getExprManager()->integerType());
-    addArithmeticOperators(parser);
+    defineType("Int", getExprManager()->integerType());
+    addArithmeticOperators();
     break;
 
   case THEORY_REALS:
-    parser.defineType("Real", parser.getExprManager()->realType());
-    addArithmeticOperators(parser);
+    defineType("Real", getExprManager()->realType());
+    addArithmeticOperators();
     break;
 
   default:
@@ -91,23 +99,30 @@ void Smt2::addTheory(Parser& parser, Theory theory) {
   }
 }
 
+bool Smt2::logicIsSet() {
+  return d_logicSet;
+}
+
 /**
  * Sets the logic for the current benchmark. Declares any logic and theory symbols.
  *
  * @param parser the CVC4 Parser object
  * @param name the name of the logic (e.g., QF_UF, AUFLIA)
  */
-void Smt2::setLogic(Parser& parser, const std::string& name) {
+void Smt2::setLogic(const std::string& name) {
+  d_logicSet = true;
+  d_logic = toLogic(name);
+
   // Core theory belongs to every logic
-  addTheory(parser, THEORY_CORE);
+  addTheory(THEORY_CORE);
 
-  switch(toLogic(name)) {
+  switch(d_logic) {
   case QF_UF:
-    parser.addOperator(kind::APPLY_UF);
+    addOperator(kind::APPLY_UF);
     break;
 
   case QF_LRA:
-    addTheory(parser, THEORY_REALS);
+    addTheory(THEORY_REALS);
     break;
 
   default:
@@ -115,7 +130,7 @@ void Smt2::setLogic(Parser& parser, const std::string& name) {
   }
 }
 
-void Smt2::setInfo(Parser& parser, const std::string& flag, const SExpr& sexpr) {
+void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
   // TODO: ???
 }
 
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 715d3199f..0bb3020a3 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -22,6 +22,7 @@
 namespace std { using namespace __gnu_cxx; }
 
 #include "util/hash.h"
+#include "parser/parser.h"
 
 namespace CVC4 {
 
@@ -29,9 +30,8 @@ class SExpr;
 
 namespace parser {
 
-class Parser;
-
-class Smt2 {
+class Smt2 : public Parser {
+  friend class ParserBuilder;
 
 public:
   enum Logic {
@@ -51,14 +51,25 @@ public:
     THEORY_REALS_INTS,
   };
 
+private:
+  bool d_logicSet;
+  Logic d_logic;
+
+protected:
+  Smt2(ExprManager* exprManager, Input* input, bool strictMode = false);
+
+public:
   /**
    * Add theory symbols to the parser state.
    *
    * @param parser the CVC4 Parser object
    * @param theory the theory to open (e.g., Core, Ints)
    */
-  static void
-  addTheory(Parser& parser, Theory theory);
+  void
+  addTheory(Theory theory);
+
+  bool
+  logicIsSet();
 
   /**
    * Sets the logic for the current benchmark. Declares any logic and theory symbols.
@@ -66,17 +77,17 @@ public:
    * @param parser the CVC4 Parser object
    * @param name the name of the logic (e.g., QF_UF, AUFLIA)
    */
-  static void
-  setLogic(Parser& parser, const std::string& name);
+  void
+  setLogic(const std::string& name);
 
-  static void
-  setInfo(Parser& parser, const std::string& flag, const SExpr& sexpr);
+  void
+  setInfo(const std::string& flag, const SExpr& sexpr);
 
   static Logic toLogic(const std::string& name);
 
 private:
 
-  static void addArithmeticOperators(Parser& parser);
+  void addArithmeticOperators();
   static std::hash_map<const std::string, Logic, CVC4::StringHashFunction> newLogicMap();
 };
 }/* CVC4::parser namespace */
diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp
index 6d7a04800..5150ba010 100644
--- a/src/parser/smt2/smt2_input.cpp
+++ b/src/parser/smt2/smt2_input.cpp
@@ -65,12 +65,5 @@ Expr Smt2Input::parseExpr() throw (ParserException) {
   return d_pSmt2Parser->parseExpr(d_pSmt2Parser);
 }
 
-void Smt2Input::setParser(Parser& parser) {
-  super::setParser(parser);
-  if( !parser.strictModeEnabled() ) {
-    Smt2::addTheory(parser,Smt2::THEORY_CORE);
-  }
-}
-
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h
index c003a76ec..962e2a987 100644
--- a/src/parser/smt2/smt2_input.h
+++ b/src/parser/smt2/smt2_input.h
@@ -32,6 +32,8 @@ class ExprManager;
 
 namespace parser {
 
+class Smt2;
+
 class Smt2Input : public AntlrInput {
   typedef AntlrInput super;
 
@@ -86,11 +88,6 @@ protected:
    */
   Expr parseExpr() throw(ParserException);
 
-  /** Set the Parser object for this input. This implementation overrides the super-class
-   * implementation to add the core theory symbols to the parser state when strict
-   * mode is disabled. */
-  virtual void setParser(Parser& parser);
-
 };/* class Smt2Input */
 
 }/* CVC4::parser namespace */
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 49ff24863..6f09820c5 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -19,8 +19,8 @@
 
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
-#include "parser/input.h"
 #include "parser/parser.h"
+#include "parser/parser_builder.h"
 #include "parser/smt2/smt2.h"
 #include "expr/command.h"
 #include "util/output.h"
@@ -62,17 +62,20 @@ protected:
 //         Debug.on("parser-extra");
 //        cerr << "Testing good input: <<" << goodInput << ">>" << endl;
 //        istringstream stream(goodInputs[i]);
-        Input* input = Input::newStringInput(d_lang, goodInput, "test");
-        Parser parser(d_exprManager, input);
-        TS_ASSERT( !parser.done() );
+        ParserBuilder parserBuilder(d_lang,"test");
+        Parser *parser =
+          parserBuilder.withStringInput(goodInput)
+            .withExprManager(*d_exprManager)
+            .build();
+        TS_ASSERT( !parser->done() );
         Command* cmd;
-        while((cmd = parser.nextCommand()) != NULL) {
+        while((cmd = parser->nextCommand()) != NULL) {
           Debug("parser") << "Parsed command: " << (*cmd) << endl;
         }
 
-        TS_ASSERT( parser.done() );
-        delete input;
-        Debug.off("parser");
+        TS_ASSERT( parser->done() );
+        delete parser;
+//        Debug.off("parser");
 //        Debug.off("parser-extra");
       } catch (Exception& e) {
         cout << "\nGood input failed:\n" << goodInput << endl
@@ -85,14 +88,18 @@ protected:
   void tryBadInput(const string badInput, bool strictMode = false) {
 //      cerr << "Testing bad input: '" << badInput << "'\n";
 //      Debug.on("parser");
-      Input* input = Input::newStringInput(d_lang, badInput, "test");
-      Parser parser(d_exprManager, input, strictMode);
+    ParserBuilder parserBuilder(d_lang,"test");
+    Parser *parser =
+      parserBuilder.withStringInput(badInput)
+        .withExprManager(*d_exprManager)
+        .withStrictMode(strictMode)
+        .build();
       TS_ASSERT_THROWS
-        ( while(parser.nextCommand());
+        ( while(parser->nextCommand());
           cout << "\nBad input succeeded:\n" << badInput << endl;,
           const ParserException& );
 //      Debug.off("parser");
-      delete input;
+      delete parser;
   }
 
   void tryGoodExpr(const string goodExpr) {
@@ -102,18 +109,20 @@ protected:
 //        cerr << "Testing good expr: '" << goodExpr << "'\n";
         // Debug.on("parser");
 //        istringstream stream(context + goodBooleanExprs[i]);
-        Input* input = Input::newStringInput(d_lang,
-                                              goodExpr, "test");
-        Parser parser(d_exprManager, input);
-        TS_ASSERT( !parser.done() );
-        setupContext(parser);
-        TS_ASSERT( !parser.done() );
-        Expr e = parser.nextExpression();
+        ParserBuilder parserBuilder(d_lang,"test");
+        Parser *parser =
+          parserBuilder.withStringInput(goodExpr)
+            .withExprManager(*d_exprManager)
+            .build();
+        TS_ASSERT( !parser->done() );
+        setupContext(*parser);
+        TS_ASSERT( !parser->done() );
+        Expr e = parser->nextExpression();
         TS_ASSERT( !e.isNull() );
-        e = parser.nextExpression();
-        TS_ASSERT( parser.done() );
+        e = parser->nextExpression();
+        TS_ASSERT( parser->done() );
         TS_ASSERT( e.isNull() );
-        delete input;
+        delete parser;
       } catch (Exception& e) {
         cout << endl
              << "Good expr failed." << endl
@@ -133,18 +142,22 @@ protected:
 //    Debug.on("parser");
 //    Debug.on("parser-extra");
 //      cout << "Testing bad expr: '" << badExpr << "'\n";
-      Input* input = Input::newStringInput(d_lang, badExpr, "test");
-      Parser parser(d_exprManager, input, strictMode);
-      setupContext(parser);
-      TS_ASSERT( !parser.done() );
+      ParserBuilder parserBuilder(d_lang,"test");
+      Parser *parser =
+        parserBuilder.withStringInput(badExpr)
+          .withExprManager(*d_exprManager)
+          .withStrictMode(strictMode)
+          .build();
+      setupContext(*parser);
+      TS_ASSERT( !parser->done() );
       TS_ASSERT_THROWS
-        ( Expr e = parser.nextExpression();
+        ( Expr e = parser->nextExpression();
           cout << endl
                << "Bad expr succeeded." << endl
                << "Input: <<" << badExpr << ">>" << endl
                << "Output: <<" << e << ">>" << endl;,
           const ParserException& );
-      delete input;
+      delete parser;
 //    Debug.off("parser");
   }
 
@@ -266,8 +279,8 @@ class Smt2ParserTest : public CxxTest::TestSuite, public ParserBlack {
 public:
   Smt2ParserTest() : ParserBlack(LANG_SMTLIB_V2) { }
 
-  void setupContext(Parser& parser) {
-    Smt2::addTheory(parser,Smt2::THEORY_CORE);
+  void setupContext(Smt2& parser) {
+    parser.addTheory(Smt2::THEORY_CORE);
     super::setupContext(parser);
   }