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`.

14 files changed, 364 insertions, 169 deletions

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index a26ee3b73..b94b49db3 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -35,6 +35,7 @@
 #include "main/time_limit.h"
 #include "options/options.h"
 #include "options/set_language.h"
+#include "parser/input_parser.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
 #include "smt/command.h"
@@ -261,14 +262,13 @@ int runCvc5(int argc, char* argv[], Options& opts)
                                   pExecutor->getSymbolManager(),
                                   opts);
       std::unique_ptr<Parser> parser(parserBuilder.build());
+      std::unique_ptr<InputParser> inputParser;
       if( inputFromStdin ) {
-        parser->setInput(
-            Input::newStreamInput(opts.getInputLanguage(), cin, filename));
+        inputParser = parser->parseStream(filename, cin);
       }
       else
       {
-        parser->setInput(Input::newFileInput(
-            opts.getInputLanguage(), filename, opts.getMemoryMap()));
+        inputParser = parser->parseFile(filename, opts.getMemoryMap());
       }
 
       vector< vector<Command*> > allCommands;
@@ -284,7 +284,7 @@ int runCvc5(int argc, char* argv[], Options& opts)
         }
 
         try {
-          cmd.reset(parser->nextCommand());
+          cmd.reset(inputParser->nextCommand());
           if (cmd == nullptr) break;
         } catch (UnsafeInterruptException& e) {
           interrupted = true;
@@ -417,14 +417,13 @@ int runCvc5(int argc, char* argv[], Options& opts)
                                   pExecutor->getSymbolManager(),
                                   opts);
       std::unique_ptr<Parser> parser(parserBuilder.build());
+      std::unique_ptr<InputParser> inputParser;
       if( inputFromStdin ) {
-        parser->setInput(
-            Input::newStreamInput(opts.getInputLanguage(), cin, filename));
+        inputParser = parser->parseStream(filename, cin);
       }
       else
       {
-        parser->setInput(Input::newFileInput(
-            opts.getInputLanguage(), filename, opts.getMemoryMap()));
+        inputParser = parser->parseFile(filename, opts.getMemoryMap());
       }
 
       bool interrupted = false;
@@ -436,7 +435,7 @@ int runCvc5(int argc, char* argv[], Options& opts)
           break;
         }
         try {
-          cmd.reset(parser->nextCommand());
+          cmd.reset(inputParser->nextCommand());
           if (cmd == nullptr) break;
         } catch (UnsafeInterruptException& e) {
           interrupted = true;
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 8ca10799f..1b3ad643b 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -17,11 +17,13 @@
  */
 #include "main/interactive_shell.h"
 
+#include <string.h>
+
 #include <algorithm>
 #include <cstdlib>
 #include <iostream>
+#include <memory>
 #include <set>
-#include <string.h>
 #include <string>
 #include <utility>
 #include <vector>
@@ -43,6 +45,7 @@
 #include "options/language.h"
 #include "options/options.h"
 #include "parser/input.h"
+#include "parser/input_parser.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
 #include "smt/command.h"
@@ -306,8 +309,8 @@ restart:
     }
   }
 
-  d_parser->setInput(Input::newStringInput(d_options.getInputLanguage(),
-                                           input, INPUT_FILENAME));
+  std::unique_ptr<InputParser> inputParser =
+      d_parser->parseString(INPUT_FILENAME, input);
 
   /* There may be more than one command in the input. Build up a
      sequence. */
@@ -316,7 +319,7 @@ restart:
 
   try
   {
-    while ((cmd = d_parser->nextCommand()))
+    while ((cmd = inputParser->nextCommand()))
     {
       cmd_seq->addCommand(cmd);
       if (dynamic_cast<QuitCommand*>(cmd) != NULL)
diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt
index f2596ceeb..81c7646f3 100644
--- a/src/parser/CMakeLists.txt
+++ b/src/parser/CMakeLists.txt
@@ -38,6 +38,8 @@ set(libcvc5parser_src_files
   cvc/cvc_input.h
   input.cpp
   input.h
+  input_parser.cpp
+  input_parser.h
   line_buffer.cpp
   line_buffer.h
   memory_mapped_input_buffer.cpp
diff --git a/src/parser/cvc/cvc.h b/src/parser/cvc/cvc.h
index e20e041cc..23fbd0f7e 100644
--- a/src/parser/cvc/cvc.h
+++ b/src/parser/cvc/cvc.h
@@ -38,9 +38,10 @@ class Cvc : public Parser
  protected:
   Cvc(api::Solver* solver,
       SymbolManager* sm,
+      InputLanguage lang,
       bool strictMode = false,
       bool parseOnly = false)
-      : Parser(solver, sm, strictMode, parseOnly)
+      : Parser(solver, sm, lang, strictMode, parseOnly)
   {
   }
 };
diff --git a/src/parser/input.h b/src/parser/input.h
index 1821bc034..250fa94aa 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -70,6 +70,7 @@ class InputStream
   const std::string getName() const;
 }; /* class InputStream */
 
+class InputParser;
 class Parser;
 
 /**
@@ -81,6 +82,7 @@ class Parser;
 class CVC5_EXPORT Input
 {
   friend class Parser; // for parseError, parseCommand, parseExpr
+  friend class InputParser;  // for parseError, parseCommand, parseExpr
   friend class ParserBuilder;
 
   /** The input stream. */
diff --git a/src/parser/input_parser.cpp b/src/parser/input_parser.cpp
new file mode 100644
index 000000000..01bd77b8d
--- /dev/null
+++ b/src/parser/input_parser.cpp
@@ -0,0 +1,91 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andres Noetzli
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The interface for parsing an input with a parser.
+ */
+
+#include "parser/input_parser.h"
+
+#include "base/output.h"
+#include "parser/input.h"
+#include "parser/parser.h"
+#include "smt/command.h"
+
+namespace cvc5 {
+namespace parser {
+
+Command* InputParser::nextCommand()
+{
+  Debug("parser") << "nextCommand()" << std::endl;
+  Command* cmd = nullptr;
+  if (d_state->hasCommand())
+  {
+    cmd = d_state->getNextCommand();
+    d_state->setDone(cmd == nullptr);
+  }
+  else
+  {
+    try
+    {
+      cmd = d_input->parseCommand();
+      d_state->preemptCommand(cmd);
+      cmd = d_state->getNextCommand();
+      d_state->setDone(cmd == nullptr);
+    }
+    catch (ParserException& e)
+    {
+      d_state->setDone();
+      throw;
+    }
+    catch (std::exception& e)
+    {
+      d_state->setDone();
+      d_input->parseError(e.what());
+    }
+  }
+  Debug("parser") << "nextCommand() => " << cmd << std::endl;
+  return cmd;
+}
+
+api::Term InputParser::nextExpression()
+{
+  Debug("parser") << "nextExpression()" << std::endl;
+  api::Term result;
+  if (!d_state->done())
+  {
+    try
+    {
+      result = d_input->parseExpr();
+      d_state->setDone(result.isNull());
+    }
+    catch (ParserException& e)
+    {
+      d_state->setDone();
+      throw;
+    }
+    catch (std::exception& e)
+    {
+      d_state->setDone();
+      d_input->parseError(e.what());
+    }
+  }
+  Debug("parser") << "nextExpression() => " << result << std::endl;
+  return result;
+}
+
+InputParser::InputParser(Parser* state, Input* input)
+    : d_state(state), d_input(input)
+{
+}
+
+}  // namespace parser
+}  // namespace cvc5
diff --git a/src/parser/input_parser.h b/src/parser/input_parser.h
new file mode 100644
index 000000000..a96aa0d7e
--- /dev/null
+++ b/src/parser/input_parser.h
@@ -0,0 +1,69 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andres Noetzli
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The interface for parsing an input with a parser.
+ */
+
+#include "cvc5parser_public.h"
+
+#ifndef CVC5__PARSER__INPUT_PARSER_H
+#define CVC5__PARSER__INPUT_PARSER_H
+
+#include <memory>
+
+#include "api/cpp/cvc5.h"
+#include "cvc5_export.h"
+
+namespace cvc5 {
+
+class Command;
+
+namespace parser {
+
+class Input;
+class Parser;
+
+/**
+ * This class is the main interface for retrieving commands and expressions
+ * from an input using a parser.
+ */
+class CVC5_EXPORT InputParser
+{
+  friend Parser;
+
+ public:
+  /** Parse and return the next command. */
+  Command* nextCommand();
+
+  /** Parse and return the next expression. */
+  api::Term nextExpression();
+
+ private:
+  /**
+   * Constructor.
+   *
+   * @param state The parser state to use.
+   * @param input The input to parse. This class takes ownership.
+   */
+  InputParser(Parser* state, Input* input);
+
+  /** The parser state */
+  Parser* d_state;
+
+  /** The underlying input */
+  std::unique_ptr<Input> d_input;
+};
+
+}  // namespace parser
+}  // namespace cvc5
+
+#endif
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index f3a0d5c83..8512f55eb 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -19,6 +19,7 @@
 #include <fstream>
 #include <iostream>
 #include <iterator>
+#include <memory>
 #include <sstream>
 #include <unordered_set>
 
@@ -28,6 +29,7 @@
 #include "expr/kind.h"
 #include "options/options.h"
 #include "parser/input.h"
+#include "parser/input_parser.h"
 #include "parser/parser_exception.h"
 #include "smt/command.h"
 
@@ -39,9 +41,11 @@ namespace parser {
 
 Parser::Parser(api::Solver* solver,
                SymbolManager* sm,
+               InputLanguage lang,
                bool strictMode,
                bool parseOnly)
     : d_symman(sm),
+      d_lang(lang),
       d_symtab(sm->getSymbolTable()),
       d_assertionLevel(0),
       d_anonymousFunctionCount(0),
@@ -65,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)
@@ -665,54 +696,18 @@ void Parser::checkFunctionLike(api::Term fun)
   }
 }
 
+bool Parser::hasCommand() { return !d_commandQueue.empty(); }
+
 void Parser::addOperator(api::Kind kind) { d_logicOperators.insert(kind); }
 
 void Parser::preemptCommand(Command* cmd) { d_commandQueue.push_back(cmd); }
-Command* Parser::nextCommand()
-{
-  Debug("parser") << "nextCommand()" << std::endl;
-  Command* cmd = NULL;
-  if (!d_commandQueue.empty()) {
-    cmd = d_commandQueue.front();
-    d_commandQueue.pop_front();
-    setDone(cmd == NULL);
-  } else {
-    try {
-      cmd = d_input->parseCommand();
-      d_commandQueue.push_back(cmd);
-      cmd = d_commandQueue.front();
-      d_commandQueue.pop_front();
-      setDone(cmd == NULL);
-    } catch (ParserException& e) {
-      setDone();
-      throw;
-    } catch (exception& e) {
-      setDone();
-      parseError(e.what());
-    }
-  }
-  Debug("parser") << "nextCommand() => " << cmd << std::endl;
-  return cmd;
-}
 
-api::Term Parser::nextExpression()
-{
-  Debug("parser") << "nextExpression()" << std::endl;
-  api::Term result;
-  if (!done()) {
-    try {
-      result = d_input->parseExpr();
-      setDone(result.isNull());
-    } catch (ParserException& e) {
-      setDone();
-      throw;
-    } catch (exception& e) {
-      setDone();
-      parseError(e.what());
-    }
-  }
-  Debug("parser") << "nextExpression() => " << result << std::endl;
-  return result;
+Command* Parser::getNextCommand()
+{
+  Assert(!d_commandQueue.empty());
+  Command* cmd = d_commandQueue.front();
+  d_commandQueue.pop_front();
+  return cmd;
 }
 
 void Parser::attributeNotSupported(const std::string& attr) {
diff --git a/src/parser/parser.h b/src/parser/parser.h
index b127221d7..a22b24a0c 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -105,132 +105,158 @@ inline std::ostream& operator<<(std::ostream& out, SymbolType type) {
 class CVC5_EXPORT Parser
 {
   friend class ParserBuilder;
-private:
 
- /** The input that we're parsing. */
- std::unique_ptr<Input> d_input;
+ private:
+  /** The input that we're parsing. */
+  Input* d_input;
 
- /**
-  * Reference to the symbol manager, which manages the symbol table used by
-  * this parser.
-  */
- SymbolManager* d_symman;
+  /**
+   * Reference to the symbol manager, which manages the symbol table used by
+   * this parser.
+   */
+  SymbolManager* d_symman;
 
- /**
-  * This current symbol table used by this parser, from symbol manager.
-  */
- SymbolTable* d_symtab;
+  /** The language that we are parsing. */
+  InputLanguage d_lang;
 
- /**
-  * The level of the assertions in the declaration scope.  Things declared
-  * after this level are bindings from e.g. a let, a quantifier, or a
-  * lambda.
-  */
- size_t d_assertionLevel;
+  /**
+   * This current symbol table used by this parser, from symbol manager.
+   */
+  SymbolTable* d_symtab;
 
- /** How many anonymous functions we've created. */
- size_t d_anonymousFunctionCount;
+  /**
+   * The level of the assertions in the declaration scope.  Things declared
+   * after this level are bindings from e.g. a let, a quantifier, or a
+   * lambda.
+   */
+  size_t d_assertionLevel;
 
- /** Are we done */
- bool d_done;
+  /** How many anonymous functions we've created. */
+  size_t d_anonymousFunctionCount;
 
- /** Are semantic checks enabled during parsing? */
- bool d_checksEnabled;
+  /** Are we done */
+  bool d_done;
 
- /** Are we parsing in strict mode? */
- bool d_strictMode;
+  /** Are semantic checks enabled during parsing? */
+  bool d_checksEnabled;
 
- /** Are we only parsing? */
- bool d_parseOnly;
+  /** Are we parsing in strict mode? */
+  bool d_strictMode;
 
- /**
-  * Can we include files?  (Set to false for security purposes in
-  * e.g. the online version.)
-  */
- bool d_canIncludeFile;
+  /** Are we only parsing? */
+  bool d_parseOnly;
 
- /**
-  * Whether the logic has been forced with --force-logic.
-  */
- bool d_logicIsForced;
+  /**
+   * Can we include files?  (Set to false for security purposes in
+   * e.g. the online version.)
+   */
+  bool d_canIncludeFile;
 
- /**
-  * The logic, if d_logicIsForced == true.
-  */
- std::string d_forcedLogic;
+  /**
+   * Whether the logic has been forced with --force-logic.
+   */
+  bool d_logicIsForced;
 
- /** The set of operators available in the current logic. */
- std::set<api::Kind> d_logicOperators;
+  /**
+   * The logic, if d_logicIsForced == true.
+   */
+  std::string d_forcedLogic;
 
- /** The set of attributes already warned about. */
- std::set<std::string> d_attributesWarnedAbout;
+  /** The set of operators available in the current logic. */
+  std::set<api::Kind> d_logicOperators;
 
- /**
-  * The current set of unresolved types.  We can get by with this NOT
-  * being on the scope, because we can only have one DATATYPE
-  * definition going on at one time.  This is a bit hackish; we
-  * depend on mkMutualDatatypeTypes() to check everything and clear
-  * this out.
-  */
- std::set<api::Sort> d_unresolved;
-
- /**
-  * "Preemption commands": extra commands implied by subterms that
-  * should be issued before the currently-being-parsed command is
-  * issued.  Used to support SMT-LIBv2 ":named" attribute on terms.
-  *
-  * Owns the memory of the Commands in the queue.
-  */
- std::list<Command*> d_commandQueue;
+  /** The set of attributes already warned about. */
+  std::set<std::string> d_attributesWarnedAbout;
 
- /** Lookup a symbol in the given namespace (as specified by the type).
-  * Only returns a symbol if it is not overloaded, returns null otherwise.
-  */
- api::Term getSymbol(const std::string& var_name, SymbolType type);
-
-protected:
- /** The API Solver object. */
- api::Solver* d_solver;
-
- /**
-  * Create a parser state.
-  *
-  * @attention The parser takes "ownership" of the given
-  * input and will delete it on destruction.
-  *
-  * @param solver solver API object
-  * @param symm reference to the symbol manager
-  * @param input the parser input
-  * @param strictMode whether to incorporate strict(er) compliance checks
-  * @param parseOnly whether we are parsing only (and therefore certain checks
-  * need not be performed, like those about unimplemented features, @see
-  * unimplementedFeature())
-  */
- Parser(api::Solver* solver,
-        SymbolManager* sm,
-        bool strictMode = false,
-        bool parseOnly = false);
+  /**
+   * The current set of unresolved types.  We can get by with this NOT
+   * being on the scope, because we can only have one DATATYPE
+   * definition going on at one time.  This is a bit hackish; we
+   * depend on mkMutualDatatypeTypes() to check everything and clear
+   * this out.
+   */
+  std::set<api::Sort> d_unresolved;
 
-public:
+  /**
+   * "Preemption commands": extra commands implied by subterms that
+   * should be issued before the currently-being-parsed command is
+   * issued.  Used to support SMT-LIBv2 ":named" attribute on terms.
+   *
+   * Owns the memory of the Commands in the queue.
+   */
+  std::list<Command*> d_commandQueue;
 
+  /** Lookup a symbol in the given namespace (as specified by the type).
+   * Only returns a symbol if it is not overloaded, returns null otherwise.
+   */
+  api::Term getSymbol(const std::string& var_name, SymbolType type);
+
+ protected:
+  /** The API Solver object. */
+  api::Solver* d_solver;
+
+  /**
+   * Create a parser state.
+   *
+   * @attention The parser takes "ownership" of the given
+   * input and will delete it on destruction.
+   *
+   * @param solver solver API object
+   * @param symm reference to the symbol manager
+   * @param input the parser input
+   * @param strictMode whether to incorporate strict(er) compliance checks
+   * @param parseOnly whether we are parsing only (and therefore certain checks
+   * need not be performed, like those about unimplemented features, @see
+   * unimplementedFeature())
+   */
+  Parser(api::Solver* solver,
+         SymbolManager* sm,
+         InputLanguage lang,
+         bool strictMode = false,
+         bool parseOnly = false);
+
+ public:
   virtual ~Parser();
 
+  /**
+   * Parse a file with this parser.
+   *
+   * @param fname The name of the file to parse.
+   * @param useMmap Whether to map the file.
+   * @return An `InputParser` that can be used to retrieve commands/expressions.
+   */
+  std::unique_ptr<InputParser> parseFile(const std::string& fname,
+                                         bool useMmap);
+
+  /**
+   * Parse a input stream with this parser.
+   *
+   * @param name The name of the stream (used for parser errors)
+   * @param stream The stream to parse.
+   * @return An `InputParser` that can be used to retrieve commands/expressions.
+   */
+  std::unique_ptr<InputParser> parseStream(const std::string& name,
+                                           std::istream& stream);
+
+  /**
+   * Parse a string with this parser.
+   *
+   * @param name The name of the stream (used for parser errors)
+   * @param str The string to parse.
+   * @return An `InputParser` that can be used to retrieve commands/expressions.
+   */
+  std::unique_ptr<InputParser> parseString(const std::string& name,
+                                           const std::string& str);
+
   /** Get the associated solver. */
   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.
@@ -637,6 +663,9 @@ public:
    */
   void addOperator(api::Kind kind);
 
+  /** Is there a command in the queue? */
+  bool hasCommand();
+
   /**
    * Preempt the next returned command with other ones; used to
    * support the :named attribute in SMT-LIBv2, which implicitly
@@ -645,6 +674,9 @@ public:
    */
   void preemptCommand(Command* cmd);
 
+  /** Get the next command from the queue. */
+  Command* getNextCommand();
+
   /** Is the symbol bound to a boolean variable? */
   bool isBoolean(const std::string& name);
 
@@ -656,12 +688,6 @@ public:
   /** Is the symbol bound to a predicate? */
   bool isPredicate(const std::string& name);
 
-  /** Parse and return the next command. */
-  Command* nextCommand();
-
-  /** Parse and return the next expression. */
-  api::Term nextExpression();
-
   /** Issue a warning to the user. */
   void warning(const std::string& msg) { d_input->warning(msg); }
   /** Issue a warning to the user, but only once per attribute. */
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index 26a867f95..179bc1ab2 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -65,19 +65,20 @@ Parser* ParserBuilder::build()
   switch (d_lang)
   {
     case language::input::LANG_SYGUS_V2:
-      parser = new Smt2(d_solver, d_symman, d_strictMode, d_parseOnly);
+      parser = new Smt2(d_solver, d_symman, d_lang, d_strictMode, d_parseOnly);
       break;
     case language::input::LANG_TPTP:
-      parser = new Tptp(d_solver, d_symman, d_strictMode, d_parseOnly);
+      parser = new Tptp(d_solver, d_symman, d_lang, d_strictMode, d_parseOnly);
       break;
     default:
       if (language::isInputLang_smt2(d_lang))
       {
-        parser = new Smt2(d_solver, d_symman, d_strictMode, d_parseOnly);
+        parser =
+            new Smt2(d_solver, d_symman, d_lang, d_strictMode, d_parseOnly);
       }
       else
       {
-        parser = new Cvc(d_solver, d_symman, d_strictMode, d_parseOnly);
+        parser = new Cvc(d_solver, d_symman, d_lang, d_strictMode, d_parseOnly);
       }
       break;
   }
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index a91c713d6..13bdad998 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -31,9 +31,10 @@ namespace parser {
 
 Smt2::Smt2(api::Solver* solver,
            SymbolManager* sm,
+           InputLanguage lang,
            bool strictMode,
            bool parseOnly)
-    : Parser(solver, sm, strictMode, parseOnly),
+    : Parser(solver, sm, lang, strictMode, parseOnly),
       d_logicSet(false),
       d_seenSetLogic(false)
 {
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 2dd4bf663..bc4ca1173 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -66,6 +66,7 @@ class Smt2 : public Parser
  protected:
   Smt2(api::Solver* solver,
        SymbolManager* sm,
+       InputLanguage lang,
        bool strictMode = false,
        bool parseOnly = false);
 
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 156f2e1e6..5f0e7f7e8 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -34,9 +34,12 @@ namespace parser {
 
 Tptp::Tptp(api::Solver* solver,
            SymbolManager* sm,
+           InputLanguage lang,
            bool strictMode,
            bool parseOnly)
-    : Parser(solver, sm, strictMode, parseOnly), d_cnf(false), d_fof(false)
+    : Parser(solver, sm, lang, strictMode, parseOnly),
+      d_cnf(false),
+      d_fof(false)
 {
   addTheory(Tptp::THEORY_CORE);
 
diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h
index 964c0bdfb..78cd11054 100644
--- a/src/parser/tptp/tptp.h
+++ b/src/parser/tptp/tptp.h
@@ -90,6 +90,7 @@ class Tptp : public Parser {
  protected:
   Tptp(api::Solver* solver,
        SymbolManager* sm,
+       InputLanguage lang,
        bool strictMode = false,
        bool parseOnly = false);