Parsing and infrastructure support for SMT-LIBv2.5 input and output languages.

* support for new commands meta-info, declare-const, echo, get-model,
  reset, and reset-assertions
* support for set-option :global-declarations
* support for set-option :produce-assertions
* support for set-option :reproducible-resource-limit
* support for get-info :assertion-stack-levels
* support for set-info :smt-lib-version 2.5
* ascribe types for abstract values (the new 2.5 standard clarifies that
  this is required)
* SMT-LIB v2.5 string literals (we still support 2.0 string literals when
  in 2.0 mode)

What's still to do:
* check-sat-assumptions/get-unsat-assumptions (still being hotly debated).
  Also set-option :produce-unsat-assumptions.
* define-fun-rec doesn't allow mutual recursion
* All options should be restored to defaults with (reset) command.
  (Currently :incremental and maybe others get "stuck" due to late driver
  integration.)

11 files changed, 277 insertions, 50 deletions

diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index aa431ef42..f8730e372 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -201,8 +201,9 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStre
     input = new Smt1Input(inputStream);
     break;
 
-  case LANG_SMTLIB_V2:
-    input = new Smt2Input(inputStream);
+  case LANG_SMTLIB_V2_0:
+  case LANG_SMTLIB_V2_5:
+    input = new Smt2Input(inputStream, lang);
     break;
 
   case LANG_TPTP:
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index ead8caa20..2b442015a 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -702,6 +702,11 @@ mainCommand[CVC4::Command*& cmd]
       PARSER_STATE->reset();
     }
 
+  | RESET_TOK ASSERTIONS_TOK
+    { cmd = new ResetAssertionsCommand();
+      PARSER_STATE->reset();
+    }
+
     // Datatypes can be mututally-recursive if they're in the same
     // definition block, separated by a comma.  So we parse everything
     // and then ask the ExprManager to resolve everything in one go.
diff --git a/src/parser/options b/src/parser/options
index c80914596..66e95889f 100644
--- a/src/parser/options
+++ b/src/parser/options
@@ -14,6 +14,9 @@ option memoryMap --mmap bool
 option semanticChecks /--no-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--no-type-checking
  disable ALL semantic checks, including type checks
 
+option globalDeclarations global-declarations bool :default false
+ force all declarations and definitions to be global
+
 # this is to support security in the online version, and in other similar contexts
 # (--no-include-file disables filesystem access in TPTP and SMT2 parsers)
 # the name --no-include-file is legacy: it also now limits any filesystem access
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 064379cf3..045cd4ae1 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -29,7 +29,6 @@
 #include "expr/kind.h"
 #include "expr/type.h"
 #include "util/output.h"
-#include "options/options.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -43,6 +42,7 @@ Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool par
   d_symtabAllocated(),
   d_symtab(&d_symtabAllocated),
   d_assertionLevel(0),
+  d_globalDeclarations(false),
   d_anonymousFunctionCount(0),
   d_done(false),
   d_checksEnabled(true),
@@ -142,6 +142,9 @@ bool Parser::isPredicate(const std::string& name) {
 
 Expr
 Parser::mkVar(const std::string& name, const Type& type, uint32_t flags) {
+  if(d_globalDeclarations) {
+    flags |= ExprManager::VAR_FLAG_GLOBAL;
+  }
   Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
   Expr expr = d_exprManager->mkVar(name, type, flags);
   defineVar(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL);
@@ -158,6 +161,9 @@ Parser::mkBoundVar(const std::string& name, const Type& type) {
 
 Expr
 Parser::mkFunction(const std::string& name, const Type& type, uint32_t flags) {
+  if(d_globalDeclarations) {
+    flags |= ExprManager::VAR_FLAG_GLOBAL;
+  }
   Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
   Expr expr = d_exprManager->mkVar(name, type, flags);
   defineFunction(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL);
@@ -166,6 +172,9 @@ Parser::mkFunction(const std::string& name, const Type& type, uint32_t flags) {
 
 Expr
 Parser::mkAnonymousFunction(const std::string& prefix, const Type& type, uint32_t flags) {
+  if(d_globalDeclarations) {
+    flags |= ExprManager::VAR_FLAG_GLOBAL;
+  }
   stringstream name;
   name << prefix << "_anon_" << ++d_anonymousFunctionCount;
   return d_exprManager->mkVar(name.str(), type, flags);
@@ -173,6 +182,9 @@ Parser::mkAnonymousFunction(const std::string& prefix, const Type& type, uint32_
 
 std::vector<Expr>
 Parser::mkVars(const std::vector<std::string> names, const Type& type, uint32_t flags) {
+  if(d_globalDeclarations) {
+    flags |= ExprManager::VAR_FLAG_GLOBAL;
+  }
   std::vector<Expr> vars;
   for(unsigned i = 0; i < names.size(); ++i) {
     vars.push_back(mkVar(names[i], type, flags));
@@ -234,6 +246,9 @@ Parser::defineParameterizedType(const std::string& name,
 
 SortType
 Parser::mkSort(const std::string& name, uint32_t flags) {
+  if(d_globalDeclarations) {
+    flags |= ExprManager::VAR_FLAG_GLOBAL;
+  }
   Debug("parser") << "newSort(" << name << ")" << std::endl;
   Type type = d_exprManager->mkSort(name, flags);
   defineType(name, type);
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 52236294a..ffe33a980 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -134,6 +134,12 @@ class CVC4_PUBLIC Parser {
   size_t d_assertionLevel;
 
   /**
+   * Whether we're in global declarations mode (all definitions and
+   * declarations are global).
+   */
+  bool d_globalDeclarations;
+
+  /**
    * Maintains a list of reserved symbols at the assertion level that might
    * not occur in our symbol table.  This is necessary to e.g. support the
    * proper behavior of the :named annotation in SMT-LIBv2 when used under
@@ -561,10 +567,14 @@ public:
     }
   }
 
-  inline void reset() {
+  virtual void reset() {
     d_symtab->reset();
   }
 
+  void setGlobalDeclarations(bool flag) {
+    d_globalDeclarations = flag;
+  }
+
   /**
    * Set the current symbol table used by this parser.
    * From now on, this parser will perform its definitions and
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index b467acfeb..241c9c815 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -89,7 +89,8 @@ Parser* ParserBuilder::build()
   case language::input::LANG_SMTLIB_V1:
     parser = new Smt1(d_exprManager, input, d_strictMode, d_parseOnly);
     break;
-  case language::input::LANG_SMTLIB_V2:
+  case language::input::LANG_SMTLIB_V2_0:
+  case language::input::LANG_SMTLIB_V2_5:
     parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly);
     break;
   case language::input::LANG_TPTP:
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 3d57eebff..9281b19f2 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -234,20 +234,22 @@ command returns [CVC4::Command* cmd = NULL]
       }
       PARSER_STATE->setLogic(name);
       $cmd = new SetBenchmarkLogicCommand(name); }
-  | SET_INFO_TOK KEYWORD symbolicExpr[sexpr]
-    { name = AntlrInput::tokenText($KEYWORD);
-      if(name == ":cvc4-logic" || name == ":cvc4_logic") {
-        PARSER_STATE->setLogic(sexpr.getValue());
-      }
-      PARSER_STATE->setInfo(name.c_str() + 1, sexpr);
-      cmd = new SetInfoCommand(name.c_str() + 1, sexpr); }
+  | /* set-info */
+    SET_INFO_TOK metaInfoInternal[cmd]
   | /* get-info */
     GET_INFO_TOK KEYWORD
     { cmd = new GetInfoCommand(AntlrInput::tokenText($KEYWORD).c_str() + 1); }
   | /* set-option */
     SET_OPTION_TOK keyword[name] symbolicExpr[sexpr]
     { PARSER_STATE->setOption(name.c_str() + 1, sexpr);
-      cmd = new SetOptionCommand(name.c_str() + 1, sexpr); }
+      cmd = new SetOptionCommand(name.c_str() + 1, sexpr);
+      // Ugly that this changes the state of the parser; but
+      // global-declarations affects parsing, so we can't hold off
+      // on this until some SmtEngine eventually (if ever) executes it.
+      if(name == ":global-declarations") {
+        PARSER_STATE->setGlobalDeclarations(sexpr.getValue() == "true");
+      }
+    }
   | /* get-option */
     GET_OPTION_TOK KEYWORD
     { cmd = new GetOptionCommand(AntlrInput::tokenText($KEYWORD).c_str() + 1); }
@@ -443,9 +445,18 @@ command returns [CVC4::Command* cmd = NULL]
           cmd = new PopCommand();
         }
       } )
+
+    /* exit */
   | EXIT_TOK
     { cmd = new QuitCommand(); }
 
+    /* New SMT-LIB 2.5 command set */
+  | smt25Command[cmd]
+    { if(PARSER_STATE->v2_0() && PARSER_STATE->strictModeEnabled()) {
+        PARSER_STATE->parseError("SMT-LIB 2.5 commands are not permitted while operating in strict compliance mode and in SMT-LIB 2.0 mode.");
+      }
+    }
+
     /* CVC4-extended SMT-LIB commands */
   | extendedCommand[cmd]
     { if(PARSER_STATE->strictModeEnabled()) {
@@ -464,25 +475,56 @@ command returns [CVC4::Command* cmd = NULL]
     }
   ;
 
-extendedCommand[CVC4::Command*& cmd]
+// Separate this into its own rule (can be invoked by set-info or meta-info)
+metaInfoInternal[CVC4::Command*& cmd]
 @declarations {
-  std::vector<CVC4::Datatype> dts;
-  Type t;
-  Expr e, e2;
+  std::string name;
   SExpr sexpr;
+}
+  : KEYWORD symbolicExpr[sexpr]
+    { name = AntlrInput::tokenText($KEYWORD);
+      if(name == ":cvc4-logic" || name == ":cvc4_logic") {
+        PARSER_STATE->setLogic(sexpr.getValue());
+      } else if(name == ":smt-lib-version") {
+        // if we don't recognize the revision name, just keep the current mode
+        if( (sexpr.isRational() && sexpr.getRationalValue() == Rational(2)) ||
+            sexpr.getValue() == "2" ||
+            sexpr.getValue() == "2.0" ) {
+          PARSER_STATE->setLanguage(language::input::LANG_SMTLIB_V2_0);
+        } else if( (sexpr.isRational() && sexpr.getRationalValue() == Rational(5, 2)) ||
+                   sexpr.getValue() == "2.5" ) {
+          PARSER_STATE->setLanguage(language::input::LANG_SMTLIB_V2_5);
+        }
+      }
+      PARSER_STATE->setInfo(name.c_str() + 1, sexpr);
+      cmd = new SetInfoCommand(name.c_str() + 1, sexpr);
+    }
+  ;
+
+smt25Command[CVC4::Command*& cmd]
+@declarations {
   std::string name;
-  std::vector<std::string> names;
-  std::vector<Expr> terms;
-  std::vector<Type> sorts;
+  Expr expr, expr2;
   std::vector<std::pair<std::string, Type> > sortedVarNames;
+  SExpr sexpr;
+  Type t;
 }
-    /* Extended SMT-LIB set of commands syntax, not permitted in
-     * --smtlib2 compliance mode. */
-  : DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd]
-  | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd]
-  | /* get model */
-    GET_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    /* meta-info */
+  : META_INFO_TOK metaInfoInternal[cmd]
+
+    /* declare-const */
+  | DECLARE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
+    { PARSER_STATE->checkUserSymbol(name); }
+    sortSymbol[t,CHECK_DECLARED]
+    { Expr c = PARSER_STATE->mkVar(name, t);
+      $cmd = new DeclareFunctionCommand(name, c, t); }
+
+    /* get model */
+  | GET_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     { cmd = new GetModelCommand(); }
+
+    /* echo */
   | ECHO_TOK
     ( simpleSymbolicExpr[sexpr]
       { std::stringstream ss;
@@ -491,17 +533,77 @@ extendedCommand[CVC4::Command*& cmd]
       }
     | { cmd = new EchoCommand(); }
     )
+
+    /* reset: reset everything, returning solver to initial state.
+     * Logic and options must be set again. */
+  | RESET_TOK
+    { cmd = new ResetCommand();
+      PARSER_STATE->reset();
+    }
+    /* reset-assertions: reset assertions, assertion stack, declarations,
+     * etc., but the logic and options remain as they were. */
+  | RESET_ASSERTIONS_TOK
+    { cmd = new ResetAssertionsCommand();
+      PARSER_STATE->resetAssertions();
+    }
+
+  | /* recursive function definition */
+    DEFINE_FUN_REC_TOK { PARSER_STATE->checkThatLogicIsSet(); } LPAREN_TOK
+    { PARSER_STATE->pushScope(true); }
+    ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
+      { PARSER_STATE->checkUserSymbol(name); }
+      LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
+      sortSymbol[t,CHECK_DECLARED]
+      { /* add variables to parser state before parsing term */
+        Debug("parser") << "define fun rec: '" << name << "'" << std::endl;
+          if( sortedVarNames.size() > 0 ) {
+          std::vector<CVC4::Type> sorts;
+          sorts.reserve(sortedVarNames.size());
+          for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
+                sortedVarNames.begin(), iend = sortedVarNames.end();
+              i != iend;
+              ++i) {
+            sorts.push_back((*i).second);
+          }
+          t = EXPR_MANAGER->mkFunctionType(sorts, t);
+        }
+        PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED);
+        PARSER_STATE->pushScope(true);
+        for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
+              sortedVarNames.begin(), iend = sortedVarNames.end();
+            i != iend;
+            ++i) {
+          PARSER_STATE->mkBoundVar((*i).first, (*i).second);
+        }
+      }
+      term[expr, expr2]
+      { PARSER_STATE->popScope(); }
+      RPAREN_TOK )+ RPAREN_TOK
+      { PARSER_STATE->popScope(); }
+
+  // CHECK_SAT_ASSUMING still being discussed
+  // GET_UNSAT_ASSUMPTIONS
+  ;
+
+extendedCommand[CVC4::Command*& cmd]
+@declarations {
+  std::vector<CVC4::Datatype> dts;
+  Expr e, e2;
+  Type t;
+  std::string name;
+  std::vector<std::string> names;
+  std::vector<Expr> terms;
+  std::vector<Type> sorts;
+  std::vector<std::pair<std::string, Type> > sortedVarNames;
+}
+    /* Extended SMT-LIB set of commands syntax, not permitted in
+     * --smtlib2 compliance mode. */
+  : DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd]
+  | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd]
   | rewriterulesCommand[cmd]
 
     /* Support some of Z3's extended SMT-LIB commands */
 
-  | DECLARE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
-    { PARSER_STATE->checkUserSymbol(name); }
-    sortSymbol[t,CHECK_DECLARED]
-    { Expr c = PARSER_STATE->mkVar(name, t);
-      $cmd = new DeclareFunctionCommand(name, c, t); }
-      
   | DECLARE_SORTS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF) &&
          !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) &&
@@ -799,11 +901,11 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr]
 //	}
   | symbol[s,CHECK_NONE,SYM_SORT]
     { sexpr = SExpr(SExpr::Keyword(s)); }
-  | tok=(ASSERT_TOK | CHECKSAT_TOK | DECLARE_FUN_TOK | DECLARE_SORT_TOK | DEFINE_FUN_TOK | DEFINE_SORT_TOK | GET_VALUE_TOK | GET_ASSIGNMENT_TOK | GET_ASSERTIONS_TOK | GET_PROOF_TOK | GET_UNSAT_CORE_TOK | EXIT_TOK | SET_LOGIC_TOK | SET_INFO_TOK | GET_INFO_TOK | SET_OPTION_TOK | GET_OPTION_TOK | PUSH_TOK | POP_TOK | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | REWRITE_RULE_TOK | REDUCTION_RULE_TOK | PROPAGATION_RULE_TOK | SIMPLIFY_TOK)
+  | tok=(ASSERT_TOK | CHECKSAT_TOK | DECLARE_FUN_TOK | DECLARE_SORT_TOK | DEFINE_FUN_TOK | DEFINE_FUN_REC_TOK | DEFINE_SORT_TOK | GET_VALUE_TOK | GET_ASSIGNMENT_TOK | GET_ASSERTIONS_TOK | GET_PROOF_TOK | GET_UNSAT_CORE_TOK | EXIT_TOK | RESET_TOK | RESET_ASSERTIONS_TOK | SET_LOGIC_TOK | SET_INFO_TOK | GET_INFO_TOK | SET_OPTION_TOK | GET_OPTION_TOK | PUSH_TOK | POP_TOK | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | REWRITE_RULE_TOK | REDUCTION_RULE_TOK | PROPAGATION_RULE_TOK | SIMPLIFY_TOK)
     { sexpr = SExpr(SExpr::Keyword(AntlrInput::tokenText($tok))); }
   | builtinOp[k]
     { std::stringstream ss;
-      ss << Expr::setlanguage(CVC4::language::output::LANG_SMTLIB_V2) << EXPR_MANAGER->mkConst(k);
+      ss << Expr::setlanguage(CVC4::language::output::LANG_SMTLIB_V2_5) << EXPR_MANAGER->mkConst(k);
       sexpr = SExpr(ss.str());
     }
   ;
@@ -1328,15 +1430,15 @@ termList[std::vector<CVC4::Expr>& formulas, CVC4::Expr& expr]
  * Matches a string, and strips off the quotes.
  */
 str[std::string& s, bool fsmtlib]
-  : STRING_LITERAL
-    { s = AntlrInput::tokenText($STRING_LITERAL);
+  : STRING_LITERAL_2_0
+    { s = AntlrInput::tokenText($STRING_LITERAL_2_0);
       /* strip off the quotes */
       s = s.substr(1, s.size() - 2);
-	  for(size_t i=0; i<s.size(); i++) {
-		if((unsigned)s[i] > 127) {
-			PARSER_STATE->parseError("Extended characters are not part of SMT-LIB, and they must be encoded as esacped sequences");
-		}
-	  }
+      for(size_t i=0; i<s.size(); i++) {
+        if((unsigned)s[i] > 127) {
+          PARSER_STATE->parseError("Extended characters are not part of SMT-LIB, and they must be encoded as esacped sequences");
+        }
+      }
       if(fsmtlib) {
         /* handle SMT-LIB standard escapes '\\' and '\"' */
         char* p_orig = strdup(s.c_str());
@@ -1360,6 +1462,29 @@ str[std::string& s, bool fsmtlib]
         free(p_orig);
       }
     }
+  | STRING_LITERAL_2_5
+    { s = AntlrInput::tokenText($STRING_LITERAL_2_5);
+      /* strip off the quotes */
+      s = s.substr(1, s.size() - 2);
+      for(size_t i=0; i<s.size(); i++) {
+        if((unsigned)s[i] > 127) {
+          PARSER_STATE->parseError("Extended characters are not part of SMT-LIB, and they must be encoded as esacped sequences");
+        }
+      }
+      // In the 2.5 version, always handle escapes (regardless of fsmtlib flag).
+      char* p_orig = strdup(s.c_str());
+      char *p = p_orig, *q = p_orig;
+      while(*q != '\0') {
+        if(*q == '"') {
+          ++q;
+          assert(*q == '"');
+        }
+        *p++ = *q++;
+      }
+      *p = '\0';
+      s = p_orig;
+      free(p_orig);
+    }
   ;
 
 /**
@@ -1718,6 +1843,7 @@ CHECKSAT_TOK : 'check-sat';
 DECLARE_FUN_TOK : 'declare-fun';
 DECLARE_SORT_TOK : 'declare-sort';
 DEFINE_FUN_TOK : 'define-fun';
+DEFINE_FUN_REC_TOK : 'define-fun-rec';
 DEFINE_SORT_TOK : 'define-sort';
 GET_VALUE_TOK : 'get-value';
 GET_ASSIGNMENT_TOK : 'get-assignment';
@@ -1725,6 +1851,8 @@ GET_ASSERTIONS_TOK : 'get-assertions';
 GET_PROOF_TOK : 'get-proof';
 GET_UNSAT_CORE_TOK : 'get-unsat-core';
 EXIT_TOK : 'exit';
+RESET_TOK : 'reset';
+RESET_ASSERTIONS_TOK : 'reset-assertions';
 ITE_TOK : 'ite';
 LET_TOK : 'let';
 ATTRIBUTE_TOK : '!';
@@ -1733,6 +1861,7 @@ RPAREN_TOK : ')';
 INDEX_TOK : '_';
 SET_LOGIC_TOK : 'set-logic';
 SET_INFO_TOK : 'set-info';
+META_INFO_TOK : 'meta-info';
 GET_INFO_TOK : 'get-info';
 SET_OPTION_TOK : 'set-option';
 GET_OPTION_TOK : 'get-option';
@@ -1960,14 +2089,28 @@ BINARY_LITERAL
   ;
 
 /**
- * Matches a double quoted string literal.  Escaping is supported, and
- * escape character '\' has to be escaped.
+ * Matches a double-quoted string literal from SMT-LIB 2.0.
+ * Escaping is supported, and * escape character '\' has to be escaped.
+ *
+ * You shouldn't generally use this in parser rules, as the quotes
+ * will be part of the token text.  Use the str[] parser rule instead.
+ */
+STRING_LITERAL_2_0
+  : { PARSER_STATE->v2_0() }?=>
+    '"' ('\\' . | ~('\\' | '"'))* '"'
+  ;
+
+/**
+ * Matches a double-quoted string literal from SMT-LIB 2.5.
+ * You escape a double-quote inside the string with "", e.g.,
+ * "This is a string literal with "" a single, embedded double quote."
  *
  * You shouldn't generally use this in parser rules, as the quotes
  * will be part of the token text.  Use the str[] parser rule instead.
  */
-STRING_LITERAL
-  : '"' ('\\' . | ~('\\' | '"'))* '"'
+STRING_LITERAL_2_5
+  : { PARSER_STATE->v2_5() }?=>
+    '"' (~('"') | '""')* '"'
   ;
 
 /**
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 21b6a1e5b..62814ca25 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -233,6 +233,24 @@ bool Smt2::logicIsSet() {
   return d_logicSet;
 }
 
+void Smt2::reset() {
+  d_logicSet = false;
+  d_logic = LogicInfo();
+  operatorKindMap.clear();
+  d_lastNamedTerm = std::pair<Expr, std::string>();
+  d_unsatCoreNames = std::stack< std::map<Expr, std::string> >();
+  this->Parser::reset();
+
+  d_unsatCoreNames.push(std::map<Expr, std::string>());
+  if( !strictModeEnabled() ) {
+    addTheory(Smt2::THEORY_CORE);
+  }
+}
+
+void Smt2::resetAssertions() {
+  this->Parser::reset();
+}
+
 void Smt2::setLogic(const std::string& name) {
   d_logicSet = true;
   if(logicIsForced()) {
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 290bbc975..8c23c8657 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -23,6 +23,7 @@
 #include "parser/smt1/smt1.h"
 #include "theory/logic_info.h"
 #include "util/abstract_value.h"
+#include "parser/smt2/smt2_input.h"
 
 #include <string>
 #include <sstream>
@@ -82,6 +83,10 @@ public:
 
   bool logicIsSet();
 
+  void reset();
+
+  void resetAssertions();
+
   /**
    * Sets the logic for the current benchmark. Declares any logic and
    * theory symbols.
@@ -95,6 +100,17 @@ public:
    */
   const LogicInfo& getLogic() const { return d_logic; }
 
+  bool v2_0() const {
+    return getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_0;
+  }
+  bool v2_5() const {
+    return getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_5;
+  }
+
+  void setLanguage(InputLanguage lang) {
+    ((Smt2Input*) getInput())->setLanguage(lang);
+  }
+
   void setInfo(const std::string& flag, const SExpr& sexpr);
 
   void setOption(const std::string& flag, const SExpr& sexpr);
diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp
index c1e177dc4..22c2fd9a7 100644
--- a/src/parser/smt2/smt2_input.cpp
+++ b/src/parser/smt2/smt2_input.cpp
@@ -29,8 +29,9 @@ namespace CVC4 {
 namespace parser {
 
 /* Use lookahead=2 */
-Smt2Input::Smt2Input(AntlrInputStream& inputStream) :
+Smt2Input::Smt2Input(AntlrInputStream& inputStream, InputLanguage lang) :
   AntlrInput(inputStream, 2) {
+
   pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
   assert( input != NULL );
 
@@ -50,14 +51,21 @@ Smt2Input::Smt2Input(AntlrInputStream& inputStream) :
   }
 
   setAntlr3Parser(d_pSmt2Parser->pParser);
-}
 
+  setLanguage(lang);
+}
 
 Smt2Input::~Smt2Input() {
   d_pSmt2Lexer->free(d_pSmt2Lexer);
   d_pSmt2Parser->free(d_pSmt2Parser);
 }
 
+void Smt2Input::setLanguage(InputLanguage lang) {
+  CheckArgument(lang == language::input::LANG_SMTLIB_V2_0 ||
+                lang == language::input::LANG_SMTLIB_V2_5, lang);
+  d_lang = lang;
+}
+
 Command* Smt2Input::parseCommand() {
   return d_pSmt2Parser->parseCommand(d_pSmt2Parser);
 }
diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h
index b2244db4d..c6a94f07a 100644
--- a/src/parser/smt2/smt2_input.h
+++ b/src/parser/smt2/smt2_input.h
@@ -44,6 +44,9 @@ class Smt2Input : public AntlrInput {
   /** The ANTLR3 SMT2 parser for the input. */
   pSmt2Parser d_pSmt2Parser;
 
+  /** Which (variant of the) input language we're using */
+  InputLanguage d_lang;
+
   /**
    * Initialize the class. Called from the constructors once the input
    * stream is initialized.
@@ -57,16 +60,20 @@ public:
    *
    * @param inputStream the input stream to use
    */
-  Smt2Input(AntlrInputStream& inputStream);
+  Smt2Input(AntlrInputStream& inputStream,
+            InputLanguage lang = language::input::LANG_SMTLIB_V2_5);
 
   /** Destructor. Frees the lexer and the parser. */
   virtual ~Smt2Input();
 
   /** Get the language that this Input is reading. */
   InputLanguage getLanguage() const throw() {
-    return language::input::LANG_SMTLIB_V2;
+    return d_lang;
   }
 
+  /** Set the language that this Input is reading. */
+  void setLanguage(InputLanguage);
+
 protected:
 
   /**