Initial support for string standard in smt lib 2.6 (#1848)

18 files changed, 279 insertions, 154 deletions

diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 4761ba07e..e58c5319a 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -125,22 +125,25 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager,
       commandsBegin = smt1_commands;
       commandsEnd = smt1_commands + sizeof(smt1_commands) / sizeof(*smt1_commands);
       break;
-    case output::LANG_SMTLIB_V2_0:
-    case output::LANG_SMTLIB_V2_5:
-    case output::LANG_SMTLIB_V2_6:
-      d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib2";
-      commandsBegin = smt2_commands;
-      commandsEnd = smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands);
-      break;
     case output::LANG_TPTP:
       d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_tptp";
       commandsBegin = tptp_commands;
       commandsEnd = tptp_commands + sizeof(tptp_commands) / sizeof(*tptp_commands);
       break;
     default:
-      std::stringstream ss;
-      ss << "internal error: unhandled language " << lang;
-      throw Exception(ss.str());
+      if (language::isOutputLang_smt2(lang))
+      {
+        d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib2";
+        commandsBegin = smt2_commands;
+        commandsEnd =
+            smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands);
+      }
+      else
+      {
+        std::stringstream ss;
+        ss << "internal error: unhandled language " << lang;
+        throw Exception(ss.str());
+      }
     }
     d_usingReadline = true;
     int err = ::read_history(d_historyFilename.c_str());
@@ -333,9 +336,8 @@ restart:
     line += "\n";
     goto restart;
   } catch(ParserException& pe) {
-    if(d_options.getOutputLanguage() == output::LANG_SMTLIB_V2_0 ||
-       d_options.getOutputLanguage() == output::LANG_SMTLIB_V2_5 ||
-       d_options.getOutputLanguage() == output::LANG_SMTLIB_V2_6) {
+    if (language::isOutputLang_smt2(d_options.getOutputLanguage()))
+    {
       d_out << "(error \"" << pe << "\")" << endl;
     } else {
       d_out << pe << endl;
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 758d10af8..29d720b90 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -64,9 +64,8 @@ int main(int argc, char* argv[]) {
 #ifdef CVC4_COMPETITION_MODE
     *opts.getOut() << "unknown" << endl;
 #endif
-    if(opts.getOutputLanguage() == output::LANG_SMTLIB_V2_0 ||
-       opts.getOutputLanguage() == output::LANG_SMTLIB_V2_5 ||
-       opts.getOutputLanguage() == output::LANG_SMTLIB_V2_6) {
+    if (language::isOutputLang_smt2(opts.getOutputLanguage()))
+    {
       *opts.getOut() << "(error \"" << e << "\")" << endl;
     } else {
       *opts.getErr() << "CVC4 Error:" << endl << e << endl;
diff --git a/src/options/language.cpp b/src/options/language.cpp
index 86beffd6d..f76893866 100644
--- a/src/options/language.cpp
+++ b/src/options/language.cpp
@@ -19,12 +19,62 @@
 namespace CVC4 {
 namespace language {
 
+/** define the end points of smt2 languages */
+namespace input {
+Language LANG_SMTLIB_V2_END = LANG_SMTLIB_V2_6_1;
+}
+namespace output {
+Language LANG_SMTLIB_V2_END = LANG_SMTLIB_V2_6_1;
+}
+
+bool isInputLang_smt2(InputLanguage lang)
+{
+  return (lang >= input::LANG_SMTLIB_V2_0 && lang <= input::LANG_SMTLIB_V2_END)
+         || lang == input::LANG_Z3STR;
+}
+
+bool isOutputLang_smt2(OutputLanguage lang)
+{
+  return (lang >= output::LANG_SMTLIB_V2_0
+          && lang <= output::LANG_SMTLIB_V2_END)
+         || lang == output::LANG_Z3STR;
+}
+
+bool isInputLang_smt2_5(InputLanguage lang, bool exact)
+{
+  return exact ? lang == input::LANG_SMTLIB_V2_5
+               : (lang >= input::LANG_SMTLIB_V2_5
+                  && lang <= input::LANG_SMTLIB_V2_END);
+}
+
+bool isOutputLang_smt2_5(OutputLanguage lang, bool exact)
+{
+  return exact ? lang == output::LANG_SMTLIB_V2_5
+               : (lang >= output::LANG_SMTLIB_V2_5
+                  && lang <= output::LANG_SMTLIB_V2_END);
+}
+
+bool isInputLang_smt2_6(InputLanguage lang, bool exact)
+{
+  return exact ? lang == input::LANG_SMTLIB_V2_6
+               : (lang >= input::LANG_SMTLIB_V2_6
+                  && lang <= input::LANG_SMTLIB_V2_END);
+}
+
+bool isOutputLang_smt2_6(OutputLanguage lang, bool exact)
+{
+  return exact ? lang == output::LANG_SMTLIB_V2_6
+               : (lang >= output::LANG_SMTLIB_V2_6
+                  && lang <= output::LANG_SMTLIB_V2_END);
+}
+
 InputLanguage toInputLanguage(OutputLanguage language) {
   switch(language) {
   case output::LANG_SMTLIB_V1:
   case output::LANG_SMTLIB_V2_0:
   case output::LANG_SMTLIB_V2_5:
   case output::LANG_SMTLIB_V2_6:
+  case output::LANG_SMTLIB_V2_6_1:
   case output::LANG_TPTP:
   case output::LANG_CVC4:
   case output::LANG_Z3STR:
@@ -47,6 +97,7 @@ OutputLanguage toOutputLanguage(InputLanguage language) {
   case input::LANG_SMTLIB_V2_0:
   case input::LANG_SMTLIB_V2_5:
   case input::LANG_SMTLIB_V2_6:
+  case input::LANG_SMTLIB_V2_6_1:
   case input::LANG_TPTP:
   case input::LANG_CVC4:
   case input::LANG_Z3STR:
@@ -90,6 +141,11 @@ OutputLanguage toOutputLanguage(std::string language) {
   } else if(language == "smtlib2.6" || language == "smt2.6" ||
             language == "LANG_SMTLIB_V2_6") {
     return output::LANG_SMTLIB_V2_6;
+  }
+  else if (language == "smtlib2.6.1" || language == "smt2.6.1"
+           || language == "LANG_SMTLIB_V2_6_1")
+  {
+    return output::LANG_SMTLIB_V2_6_1;
   } else if(language == "tptp" || language == "LANG_TPTP") {
     return output::LANG_TPTP;
   } else if(language == "z3str" || language == "z3-str" ||
@@ -125,6 +181,11 @@ InputLanguage toInputLanguage(std::string language) {
             language == "smtlib2.6" || language == "smt2.6" ||
             language == "LANG_SMTLIB_V2_6" || language == "LANG_SMTLIB_V2") {
     return input::LANG_SMTLIB_V2_6;
+  }
+  else if (language == "smtlib2.6.1" || language == "smt2.6.1"
+           || language == "LANG_SMTLIB_V2_6_1")
+  {
+    return input::LANG_SMTLIB_V2_6_1;
   } else if(language == "tptp" || language == "LANG_TPTP") {
     return input::LANG_TPTP;
   } else if(language == "z3str" || language == "z3-str" ||
diff --git a/src/options/language.h b/src/options/language.h
index f238e765d..2b2e7d5da 100644
--- a/src/options/language.h
+++ b/src/options/language.h
@@ -30,7 +30,8 @@ namespace language {
 
 namespace input {
 
-enum CVC4_PUBLIC Language {
+enum CVC4_PUBLIC Language
+{
   // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0
 
   /** Auto-detect the language */
@@ -53,6 +54,8 @@ enum CVC4_PUBLIC Language {
   LANG_SMTLIB_V2_6,
   /** Backward-compatibility for enumeration naming */
   LANG_SMTLIB_V2 = LANG_SMTLIB_V2_6,
+  /** The SMTLIB v2.6 input language, with support for the strings standard */
+  LANG_SMTLIB_V2_6_1,
   /** The TPTP input language */
   LANG_TPTP,
   /** The CVC4 input language */
@@ -67,7 +70,7 @@ enum CVC4_PUBLIC Language {
 
   /** LANG_MAX is > any valid InputLanguage id */
   LANG_MAX
-};/* enum Language */
+}; /* enum Language */
 
 inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_PUBLIC;
 inline std::ostream& operator<<(std::ostream& out, Language lang) {
@@ -87,6 +90,7 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
   case LANG_SMTLIB_V2_6:
     out << "LANG_SMTLIB_V2_6";
     break;
+  case LANG_SMTLIB_V2_6_1: out << "LANG_SMTLIB_V2_6_1"; break;
   case LANG_TPTP:
     out << "LANG_TPTP";
     break;
@@ -109,7 +113,8 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
 
 namespace output {
 
-enum CVC4_PUBLIC Language {
+enum CVC4_PUBLIC Language
+{
   // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0
 
   /** Match the output language to the input language */
@@ -132,6 +137,8 @@ enum CVC4_PUBLIC Language {
   LANG_SMTLIB_V2_6 = input::LANG_SMTLIB_V2_6,
   /** Backward-compatibility for enumeration naming */
   LANG_SMTLIB_V2 = input::LANG_SMTLIB_V2,
+  /** The SMTLIB v2.6 output language */
+  LANG_SMTLIB_V2_6_1 = input::LANG_SMTLIB_V2_6_1,
   /** The TPTP output language */
   LANG_TPTP = input::LANG_TPTP,
   /** The CVC4 output language */
@@ -151,7 +158,7 @@ enum CVC4_PUBLIC Language {
 
   /** LANG_MAX is > any valid OutputLanguage id */
   LANG_MAX
-};/* enum Language */
+}; /* enum Language */
 
 inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_PUBLIC;
 inline std::ostream& operator<<(std::ostream& out, Language lang) {
@@ -165,6 +172,8 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
   case LANG_SMTLIB_V2_5:
     out << "LANG_SMTLIB_V2_5";
     break;
+  case LANG_SMTLIB_V2_6: out << "LANG_SMTLIB_V2_6"; break;
+  case LANG_SMTLIB_V2_6_1: out << "LANG_SMTLIB_V2_6_1"; break;
   case LANG_TPTP:
     out << "LANG_TPTP";
     break;
@@ -198,6 +207,23 @@ typedef language::output::Language OutputLanguage;
 
 namespace language {
 
+/** Is the language a variant of the smtlib version 2 language? */
+bool isInputLang_smt2(InputLanguage lang) CVC4_PUBLIC;
+bool isOutputLang_smt2(OutputLanguage lang) CVC4_PUBLIC;
+
+/**
+  * Is the language smtlib 2.5 or above? If exact=true, then this method returns
+  * false if the input language is not exactly SMT-LIB 2.6.
+  */
+bool isInputLang_smt2_5(InputLanguage lang, bool exact = false) CVC4_PUBLIC;
+bool isOutputLang_smt2_5(OutputLanguage lang, bool exact = false) CVC4_PUBLIC;
+/**
+  * Is the language smtlib 2.6 or above? If exact=true, then this method returns
+  * false if the input language is not exactly SMT-LIB 2.6.
+  */
+bool isInputLang_smt2_6(InputLanguage lang, bool exact = false) CVC4_PUBLIC;
+bool isOutputLang_smt2_6(OutputLanguage lang, bool exact = false) CVC4_PUBLIC;
+
 InputLanguage toInputLanguage(OutputLanguage language) CVC4_PUBLIC;
 OutputLanguage toOutputLanguage(InputLanguage language) CVC4_PUBLIC;
 InputLanguage toInputLanguage(std::string language) CVC4_PUBLIC;
diff --git a/src/options/language.i b/src/options/language.i
index 427e6c608..177e590f5 100644
--- a/src/options/language.i
+++ b/src/options/language.i
@@ -24,6 +24,7 @@ namespace CVC4 {
 %rename(INPUT_LANG_SMTLIB_V2_0) CVC4::language::input::LANG_SMTLIB_V2_0;
 %rename(INPUT_LANG_SMTLIB_V2_5) CVC4::language::input::LANG_SMTLIB_V2_5;
 %rename(INPUT_LANG_SMTLIB_V2_6) CVC4::language::input::LANG_SMTLIB_V2_6;
+%rename(INPUT_LANG_SMTLIB_V2_6_1) CVC4::language::input::LANG_SMTLIB_V2_6_1;
 %rename(INPUT_LANG_TPTP) CVC4::language::input::LANG_TPTP;
 %rename(INPUT_LANG_CVC4) CVC4::language::input::LANG_CVC4;
 %rename(INPUT_LANG_MAX) CVC4::language::input::LANG_MAX;
@@ -36,6 +37,7 @@ namespace CVC4 {
 %rename(OUTPUT_LANG_SMTLIB_V2_0) CVC4::language::output::LANG_SMTLIB_V2_0;
 %rename(OUTPUT_LANG_SMTLIB_V2_5) CVC4::language::output::LANG_SMTLIB_V2_5;
 %rename(OUTPUT_LANG_SMTLIB_V2_6) CVC4::language::output::LANG_SMTLIB_V2_6;
+%rename(OUTPUT_LANG_SMTLIB_V2_6_1) CVC4::language::output::LANG_SMTLIB_V2_6_1;
 %rename(OUTPUT_LANG_TPTP) CVC4::language::output::LANG_TPTP;
 %rename(OUTPUT_LANG_CVC4) CVC4::language::output::LANG_CVC4;
 %rename(OUTPUT_LANG_AST) CVC4::language::output::LANG_AST;
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index 917dae687..4fdd477b9 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -423,7 +423,8 @@ static const std::string optionsFootnote = "\n\
     sense of the option.\n\
 ";
 
-static const std::string languageDescription = "\
+static const std::string languageDescription =
+    "\
 Languages currently supported as arguments to the -L / --lang option:\n\
   auto                           attempt to automatically determine language\n\
   cvc4 | presentation | pl       CVC4 presentation language\n\
@@ -432,6 +433,7 @@ Languages currently supported as arguments to the -L / --lang option:\n\
   smt2.0 | smtlib2 | smtlib2.0   SMT-LIB format 2.0\n\
   smt2.5 | smtlib2.5             SMT-LIB format 2.5\n\
   smt2.6 | smtlib2.6             SMT-LIB format 2.6\n\
+  smt2.6.1 | smtlib2.6.1         SMT-LIB format 2.6 with support for the strings standard\n\
   tptp                           TPTP format (cnf and fof)\n\
   sygus                          SyGuS format\n\
 \n\
@@ -444,6 +446,7 @@ Languages currently supported as arguments to the --output-lang option:\n\
   smt2.0 | smtlib2.0 | smtlib2   SMT-LIB format 2.0\n\
   smt2.5 | smtlib2.5             SMT-LIB format 2.5\n\
   smt2.6 | smtlib2.6             SMT-LIB format 2.6\n\
+  smt2.6.1 | smtlib2.6.1         SMT-LIB format 2.6 with support for the strings standard\n\
   tptp                           TPTP format\n\
   z3str                          SMT-LIB 2.0 with Z3-str string constraints\n\
   ast                            internal format (simple syntax trees)\n\
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index a4bab5a8d..1e5d62ef8 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -254,12 +254,6 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStre
     input = new Smt1Input(inputStream);
     break;
 
-  case LANG_SMTLIB_V2_0:
-  case LANG_SMTLIB_V2_5:
-  case LANG_SMTLIB_V2_6:
-    input = new Smt2Input(inputStream, lang);
-    break;
-
   case LANG_SYGUS:
     input = new SygusInput(inputStream);
     break;
@@ -269,9 +263,17 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStre
     break;
 
   default:
-    std::stringstream ss;
-    ss << "internal error: unhandled language " << lang << " in AntlrInput::newInput";
-    throw InputStreamException(ss.str());
+    if (language::isInputLang_smt2(lang))
+    {
+      input = new Smt2Input(inputStream, lang);
+    }
+    else
+    {
+      std::stringstream ss;
+      ss << "internal error: unhandled language " << lang
+         << " in AntlrInput::newInput";
+      throw InputStreamException(ss.str());
+    }
   }
 
   return input;
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index ceda2ba47..9f161b830 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -91,11 +91,6 @@ 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_0:
-  case language::input::LANG_SMTLIB_V2_5:
-  case language::input::LANG_SMTLIB_V2_6:
-    parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly);
-    break;
   case language::input::LANG_SYGUS:
     parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly);
     break;
@@ -103,7 +98,14 @@ Parser* ParserBuilder::build()
     parser = new Tptp(d_exprManager, input, d_strictMode, d_parseOnly);
     break;
   default:
-    parser = new Parser(d_exprManager, input, d_strictMode, d_parseOnly);
+    if (language::isInputLang_smt2(d_lang))
+    {
+      parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly);
+    }
+    else
+    {
+      parser = new Parser(d_exprManager, input, d_strictMode, d_parseOnly);
+    }
     break;
   }
 
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index ae9d304f1..74f8e71d3 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -3103,7 +3103,7 @@ GET_PROOF_TOK : 'get-proof';
 GET_UNSAT_ASSUMPTIONS_TOK : 'get-unsat-assumptions';
 GET_UNSAT_CORE_TOK : 'get-unsat-core';
 EXIT_TOK : 'exit';
-RESET_TOK : { PARSER_STATE->v2_5(false) }? 'reset';
+RESET_TOK : { PARSER_STATE->v2_5() }? 'reset';
 RESET_ASSERTIONS_TOK : 'reset-assertions';
 ITE_TOK : 'ite';
 LET_TOK : { !PARSER_STATE->sygus() }? 'let';
@@ -3362,7 +3362,7 @@ STRING_LITERAL_2_0
  * will be part of the token text.  Use the str[] parser rule instead.
  */
 STRING_LITERAL_2_5
-  : { PARSER_STATE->v2_5(false) || PARSER_STATE->sygus() }?=>
+  : { PARSER_STATE->v2_5() || PARSER_STATE->sygus() }?=>
     '"' (~('"') | '""')* '"'
   ;
 
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 332c66be1..1d66ab0c1 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -129,10 +129,22 @@ void Smt2::addStringOperators() {
   addOperator(kind::STRING_STRREPL, "str.replace" );
   addOperator(kind::STRING_PREFIX, "str.prefixof" );
   addOperator(kind::STRING_SUFFIX, "str.suffixof" );
-  addOperator(kind::STRING_ITOS, "int.to.str" );
-  addOperator(kind::STRING_STOI, "str.to.int" );
-  addOperator(kind::STRING_IN_REGEXP, "str.in.re");
-  addOperator(kind::STRING_TO_REGEXP, "str.to.re");
+  // at the moment, we only use this syntax for smt2.6.1
+  if (getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_6_1)
+  {
+    addOperator(kind::STRING_ITOS, "str.from-int");
+    addOperator(kind::STRING_STOI, "str.to-int");
+    addOperator(kind::STRING_IN_REGEXP, "str.in-re");
+    addOperator(kind::STRING_TO_REGEXP, "str.to-re");
+  }
+  else
+  {
+    addOperator(kind::STRING_ITOS, "int.to.str");
+    addOperator(kind::STRING_STOI, "str.to.int");
+    addOperator(kind::STRING_IN_REGEXP, "str.in.re");
+    addOperator(kind::STRING_TO_REGEXP, "str.to.re");
+  }
+
   addOperator(kind::REGEXP_CONCAT, "re.++");
   addOperator(kind::REGEXP_UNION, "re.union");
   addOperator(kind::REGEXP_INTER, "re.inter");
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 71aa32492..e9e36e78c 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -155,14 +155,21 @@ public:
   bool v2_0() const {
     return getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_0;
   }
-  // 2.6 is a superset of 2.5, use exact=false to query whether smt lib 2.5 or above
-  bool v2_5( bool exact = true ) const {
-    return exact ? getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_5 : 
-                   ( getInput()->getLanguage() >= language::input::LANG_SMTLIB_V2_5 && 
-                     getInput()->getLanguage() <= language::input::LANG_SMTLIB_V2 );
+  /**
+   * Are we using smtlib 2.5 or above? If exact=true, then this method returns
+   * false if the input language is not exactly SMT-LIB 2.5.
+   */
+  bool v2_5(bool exact = false) const
+  {
+    return language::isInputLang_smt2_5(getInput()->getLanguage(), exact);
   }
-  bool v2_6() const {
-    return getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_6;
+  /**
+   * Are we using smtlib 2.6 or above? If exact=true, then this method returns
+   * false if the input language is not exactly SMT-LIB 2.6.
+   */
+  bool v2_6(bool exact = false) const
+  {
+    return language::isInputLang_smt2_6(getInput()->getLanguage(), exact);
   }
   bool sygus() const {
     return getInput()->getLanguage() == language::input::LANG_SYGUS;
diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp
index 0958e9d6c..b7ffe6991 100644
--- a/src/parser/smt2/smt2_input.cpp
+++ b/src/parser/smt2/smt2_input.cpp
@@ -66,9 +66,7 @@ Smt2Input::~Smt2Input() {
 }
 
 void Smt2Input::setLanguage(InputLanguage lang) {
-  CheckArgument(lang == language::input::LANG_SMTLIB_V2_0 ||
-                lang == language::input::LANG_SMTLIB_V2_5 ||
-                lang == language::input::LANG_SMTLIB_V2_6, lang);
+  CheckArgument(language::isInputLang_smt2(lang), lang);
   d_lang = lang;
 }
 
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index e8ebadeb8..f9486f017 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -50,6 +50,10 @@ unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang)
     return unique_ptr<Printer>(
         new printer::smt2::Smt2Printer(printer::smt2::smt2_6_variant));
 
+  case LANG_SMTLIB_V2_6_1:
+    return unique_ptr<Printer>(
+        new printer::smt2::Smt2Printer(printer::smt2::smt2_6_1_variant));
+
   case LANG_TPTP:
     return unique_ptr<Printer>(new printer::tptp::TptpPrinter());
 
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 8c9680a74..5d2b8972d 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -42,7 +42,13 @@ namespace smt2 {
 
 static OutputLanguage variantToLanguage(Variant v);
 
-static string smtKindString(Kind k);
+static string smtKindString(Kind k, Variant v);
+
+/** returns whether the variant is smt-lib 2.6 or greater */
+bool isVariant_2_6(Variant v)
+{
+  return v == smt2_6_variant || v == smt2_6_1_variant;
+}
 
 static void printBvParameterizedOp(std::ostream& out, TNode n);
 static void printFpParameterizedOp(std::ostream& out, TNode n);
@@ -191,10 +197,10 @@ void Smt2Printer::toStream(std::ostream& out,
       out << (n.getConst<bool>() ? "true" : "false");
       break;
     case kind::BUILTIN:
-      out << smtKindString(n.getConst<Kind>());
+      out << smtKindString(n.getConst<Kind>(), d_variant);
       break;
     case kind::CHAIN_OP:
-      out << smtKindString(n.getConst<Chain>().getOperator());
+      out << smtKindString(n.getConst<Chain>().getOperator(), d_variant);
       break;
     case kind::CONST_RATIONAL: {
       const Rational& r = n.getConst<Rational>();
@@ -323,7 +329,8 @@ void Smt2Printer::toStream(std::ostream& out,
       if (force_nt.isReal())
       {
         out << "(" << smtKindString(force_nt.isInteger() ? kind::TO_INTEGER
-                                                         : kind::TO_REAL)
+                                                         : kind::TO_REAL,
+                                    d_variant)
             << " ";
         toStream(out, n, toDepth, types, TypeNode::null());
         out << ")";
@@ -385,8 +392,8 @@ void Smt2Printer::toStream(std::ostream& out,
     // builtin theory
   case kind::APPLY: break;
   case kind::EQUAL:
-  case kind::DISTINCT: 
-    out << smtKindString(k) << " "; 
+  case kind::DISTINCT:
+    out << smtKindString(k, d_variant) << " ";
     parametricTypeChildren = true;
     break;
   case kind::CHAIN: break;
@@ -407,14 +414,16 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::IMPLIES:
   case kind::OR:
   case kind::XOR:
-  case kind::ITE: out << smtKindString(k) << " "; break;
+  case kind::ITE:
+    out << smtKindString(k, d_variant) << " ";
+    break;
 
-    // uf theory
+  // uf theory
   case kind::APPLY_UF: typeChildren = true; break;
   // higher-order
   case kind::HO_APPLY: break;
   case kind::LAMBDA:
-    out << smtKindString(k) << " ";
+    out << smtKindString(k, d_variant) << " ";
     break;
 
   // arith theory
@@ -453,7 +462,7 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::TO_REAL:
   case kind::POW: 
     parametricTypeChildren = true;
-    out << smtKindString(k) << " "; 
+    out << smtKindString(k, d_variant) << " ";
     break;
 
   case kind::DIVISIBLE:
@@ -466,9 +475,11 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::STORE: typeChildren = true;
   case kind::PARTIAL_SELECT_0:
   case kind::PARTIAL_SELECT_1:
-  case kind::ARRAY_TYPE: out << smtKindString(k) << " "; break;
+  case kind::ARRAY_TYPE:
+    out << smtKindString(k, d_variant) << " ";
+    break;
 
-    // string theory
+  // string theory
   case kind::STRING_CONCAT:
     if(d_variant == z3str_variant) {
       out << "Concat ";
@@ -499,30 +510,30 @@ void Smt2Printer::toStream(std::ostream& out,
       out << ")";
       return;
     }
-    out << "str.in.re ";
+    out << smtKindString(k, d_variant) << " ";
     break;
   }
-  case kind::STRING_LENGTH: out << (d_variant == z3str_variant ? "Length " : "str.len "); break;
-  case kind::STRING_SUBSTR: out << "str.substr "; break;
-  case kind::STRING_CHARAT: out << "str.at "; break;
-  case kind::STRING_STRCTN: out << "str.contains "; break;
-  case kind::STRING_STRIDOF: out << "str.indexof "; break;
-  case kind::STRING_STRREPL: out << "str.replace "; break;
-  case kind::STRING_PREFIX: out << "str.prefixof "; break;
-  case kind::STRING_SUFFIX: out << "str.suffixof "; break;
-  case kind::STRING_ITOS: out << "int.to.str "; break;
-  case kind::STRING_STOI: out << "str.to.int "; break;
-  case kind::STRING_TO_REGEXP: out << "str.to.re "; break;
-  case kind::REGEXP_CONCAT: out << "re.++ "; break;
-  case kind::REGEXP_UNION: out << "re.union "; break;
-  case kind::REGEXP_INTER: out << "re.inter "; break;
-  case kind::REGEXP_STAR: out << "re.* "; break;
-  case kind::REGEXP_PLUS: out << "re.+ "; break;
-  case kind::REGEXP_OPT: out << "re.opt "; break;
-  case kind::REGEXP_RANGE: out << "re.range "; break;
-  case kind::REGEXP_LOOP: out << "re.loop "; break;
-  case kind::REGEXP_EMPTY: out << "re.nostr "; break;
-  case kind::REGEXP_SIGMA: out << "re.allchar "; break;
+  case kind::STRING_LENGTH:
+  case kind::STRING_SUBSTR:
+  case kind::STRING_CHARAT:
+  case kind::STRING_STRCTN:
+  case kind::STRING_STRIDOF:
+  case kind::STRING_STRREPL:
+  case kind::STRING_PREFIX:
+  case kind::STRING_SUFFIX:
+  case kind::STRING_ITOS:
+  case kind::STRING_STOI:
+  case kind::STRING_TO_REGEXP:
+  case kind::REGEXP_CONCAT:
+  case kind::REGEXP_UNION:
+  case kind::REGEXP_INTER:
+  case kind::REGEXP_STAR:
+  case kind::REGEXP_PLUS:
+  case kind::REGEXP_OPT:
+  case kind::REGEXP_RANGE:
+  case kind::REGEXP_LOOP:
+  case kind::REGEXP_EMPTY:
+  case kind::REGEXP_SIGMA: out << smtKindString(k, d_variant) << " "; break;
 
   case kind::CARDINALITY_CONSTRAINT: out << "fmf.card "; break;
   case kind::CARDINALITY_VALUE: out << "fmf.card.val "; break;
@@ -586,12 +597,12 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::TRANSPOSE:
   case kind::TCLOSURE:
     parametricTypeChildren = true;
-    out << smtKindString(k) << " "; 
+    out << smtKindString(k, d_variant) << " ";
     break;
   case kind::MEMBER: typeChildren = true;
   case kind::SET_TYPE:
   case kind::SINGLETON:
-  case kind::COMPLEMENT:out << smtKindString(k) << " "; break;
+  case kind::COMPLEMENT: out << smtKindString(k, d_variant) << " "; break;
   case kind::UNIVERSE_SET:out << "(as univset " << n.getType() << ")";break;
 
     // fp theory
@@ -621,7 +632,8 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::FLOATINGPOINT_ISNEG:
   case kind::FLOATINGPOINT_ISPOS:
   case kind::FLOATINGPOINT_TO_REAL:
-    out << smtKindString(k) << ' '; break;
+    out << smtKindString(k, d_variant) << ' ';
+    break;
 
   case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
   case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT:
@@ -681,7 +693,7 @@ void Smt2Printer::toStream(std::ostream& out,
     case kind::SEP_EMP:
     case kind::SEP_PTO:
     case kind::SEP_STAR:
-    case kind::SEP_WAND: out << smtKindString(k) << " "; break;
+    case kind::SEP_WAND: out << smtKindString(k, d_variant) << " "; break;
 
     case kind::SEP_NIL:
       out << "(as sep.nil " << n.getType() << ")";
@@ -773,7 +785,8 @@ void Smt2Printer::toStream(std::ostream& out,
       }else if( n.getKind()==kind::APPLY_TESTER ){
         unsigned cindex = Datatype::indexOf(n.getOperator().toExpr());
         const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
-        if( d_variant==smt2_6_variant ){
+        if (isVariant_2_6(d_variant))
+        {
           out << "(_ is ";
           toStream(out, Node::fromExpr(dt[cindex].getConstructor()), toDepth < 0 ? toDepth : toDepth - 1, types, TypeNode::null());
           out << ")";
@@ -856,7 +869,7 @@ void Smt2Printer::toStream(std::ostream& out,
       if(forceBinary && i < n.getNumChildren() - 1) {
         // not going to work properly for parameterized kinds!
         Assert(n.getMetaKind() != kind::metakind::PARAMETERIZED);
-        out << " (" << smtKindString(n.getKind()) << ' ';
+        out << " (" << smtKindString(n.getKind(), d_variant) << ' ';
         parens << ')';
         ++c;
       } else {
@@ -869,7 +882,7 @@ void Smt2Printer::toStream(std::ostream& out,
   }
 }/* Smt2Printer::toStream(TNode) */
 
-static string smtKindString(Kind k)
+static string smtKindString(Kind k, Variant v)
 {
   switch(k) {
     // builtin theory
@@ -1039,7 +1052,7 @@ static string smtKindString(Kind k)
 
   //string theory
   case kind::STRING_CONCAT: return "str.++";
-  case kind::STRING_LENGTH: return "str.len";
+  case kind::STRING_LENGTH: return v == z3str_variant ? "Length" : "str.len";
   case kind::STRING_SUBSTR: return "str.substr" ;
   case kind::STRING_STRCTN: return "str.contains" ;
   case kind::STRING_CHARAT: return "str.at" ;
@@ -1047,10 +1060,14 @@ static string smtKindString(Kind k)
   case kind::STRING_STRREPL: return "str.replace" ;
   case kind::STRING_PREFIX: return "str.prefixof" ;
   case kind::STRING_SUFFIX: return "str.suffixof" ;
-  case kind::STRING_ITOS: return "int.to.str" ;
-  case kind::STRING_STOI: return "str.to.int" ;
-  case kind::STRING_IN_REGEXP: return "str.in.re";
-  case kind::STRING_TO_REGEXP: return "str.to.re";
+  case kind::STRING_ITOS:
+    return v == smt2_6_1_variant ? "str.from-int" : "int.to.str";
+  case kind::STRING_STOI:
+    return v == smt2_6_1_variant ? "str.to-int" : "str.to.int";
+  case kind::STRING_IN_REGEXP:
+    return v == smt2_6_1_variant ? "str.in-re" : "str.in.re";
+  case kind::STRING_TO_REGEXP:
+    return v == smt2_6_1_variant ? "str.to-re" : "str.to.re";
   case kind::REGEXP_CONCAT: return "re.++";
   case kind::REGEXP_UNION: return "re.union";
   case kind::REGEXP_INTER: return "re.inter";
@@ -1310,7 +1327,7 @@ void DeclareTypeCommandToStream(std::ostream& out,
   const std::vector<Node>* type_refs = model.getRepSet()->getTypeRepsOrNull(tn);
   if (options::modelUninterpDtEnum() && tn.isSort() && type_refs != nullptr)
   {
-    if (variant == smt2_6_variant)
+    if (isVariant_2_6(variant))
     {
       out << "(declare-datatypes ((" << command.getSymbol() << " 0)) (";
     }
@@ -1893,7 +1910,7 @@ static void toStream(std::ostream& out,
     out << "co";
   }
   out << "datatypes";
-  if (v == smt2_6_variant)
+  if (isVariant_2_6(v))
   {
     out << " (";
     for (vector<DatatypeType>::const_iterator i = datatypes.begin(),
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index 922b69a9e..1d281aed4 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -27,14 +27,16 @@ namespace CVC4 {
 namespace printer {
 namespace smt2 {
 
-enum Variant {
+enum Variant
+{
   no_variant,
-  smt2_0_variant, // old-style 2.0 syntax, when it makes a difference
-  smt2_6_variant, // new-style 2.6 syntax, when it makes a difference
-  z3str_variant, // old-style 2.0 and also z3str syntax
-  sygus_variant  // variant for sygus
-};/* enum Variant */
-
+  smt2_0_variant,    // old-style 2.0 syntax, when it makes a difference
+  smt2_6_variant,    // new-style 2.6 syntax, when it makes a difference
+  smt2_6_1_variant,  // new-style 2.6 syntax, when it makes a difference, with
+                     // support for the string standard
+  z3str_variant,     // old-style 2.0 and also z3str syntax
+  sygus_variant      // variant for sygus
+};                   /* enum Variant */
 class Smt2Printer : public CVC4::Printer {
  public:
   Smt2Printer(Variant variant = no_variant) : d_variant(variant) { }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 97e3f0215..ca01ccd8e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1304,8 +1304,8 @@ void SmtEngine::setDefaults() {
   // Language-based defaults
   if (!options::bitvectorDivByZeroConst.wasSetByUser())
   {
-    options::bitvectorDivByZeroConst.set(options::inputLanguage()
-                                         == language::input::LANG_SMTLIB_V2_6);
+    options::bitvectorDivByZeroConst.set(
+        language::isInputLang_smt2_6(options::inputLanguage()));
   }
   if (options::inputLanguage() == language::input::LANG_SYGUS)
   {
@@ -2262,44 +2262,40 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
     d_filename = value.getValue();
     return;
   } else if(key == "smt-lib-version") {
+    language::input::Language ilang = language::input::LANG_AUTO;
     if( (value.isInteger() && value.getIntegerValue() == Integer(2)) ||
         (value.isRational() && value.getRationalValue() == Rational(2)) ||
         value.getValue() == "2" ||
         value.getValue() == "2.0" ) {
-      options::inputLanguage.set(language::input::LANG_SMTLIB_V2_0);
-
-      // supported SMT-LIB version
-      if(!options::outputLanguage.wasSetByUser() &&
-         ( options::outputLanguage() == language::output::LANG_SMTLIB_V2_5 || options::outputLanguage() == language::output::LANG_SMTLIB_V2_6 )) {
-        options::outputLanguage.set(language::output::LANG_SMTLIB_V2_0);
-        *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_0);
-      }
-      return;
+      ilang = language::input::LANG_SMTLIB_V2_0;
     } else if( (value.isRational() && value.getRationalValue() == Rational(5, 2)) ||
                value.getValue() == "2.5" ) {
-      options::inputLanguage.set(language::input::LANG_SMTLIB_V2_5);
-
-      // supported SMT-LIB version
-      if(!options::outputLanguage.wasSetByUser() &&
-         options::outputLanguage() == language::output::LANG_SMTLIB_V2_0) {
-        options::outputLanguage.set(language::output::LANG_SMTLIB_V2_5);
-        *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_5);
-      }
-      return;
+      ilang = language::input::LANG_SMTLIB_V2_5;
     } else if( (value.isRational() && value.getRationalValue() == Rational(13, 5)) ||
                value.getValue() == "2.6" ) {
-      options::inputLanguage.set(language::input::LANG_SMTLIB_V2_6);
-
-      // supported SMT-LIB version
-      if(!options::outputLanguage.wasSetByUser() &&
-         options::outputLanguage() == language::output::LANG_SMTLIB_V2_0) {
-        options::outputLanguage.set(language::output::LANG_SMTLIB_V2_6);
-        *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_6);
+      ilang = language::input::LANG_SMTLIB_V2_6;
+    }
+    else if (value.getValue() == "2.6.1")
+    {
+      ilang = language::input::LANG_SMTLIB_V2_6_1;
+    }
+    else
+    {
+      Warning() << "Warning: unsupported smt-lib-version: " << value << endl;
+      throw UnrecognizedOptionException();
+    }
+    options::inputLanguage.set(ilang);
+    // also update the output language
+    if (!options::outputLanguage.wasSetByUser())
+    {
+      language::output::Language olang = language::toOutputLanguage(ilang);
+      if (options::outputLanguage() != olang)
+      {
+        options::outputLanguage.set(olang);
+        *options::out() << language::SetLanguage(olang);
       }
-      return;
     }
-    Warning() << "Warning: unsupported smt-lib-version: " << value << endl;
-    throw UnrecognizedOptionException();
+    return;
   } else if(key == "status") {
     string s;
     if(value.isAtom()) {
diff --git a/src/util/result.cpp b/src/util/result.cpp
index 27d82bb6f..dfcd74ff7 100644
--- a/src/util/result.cpp
+++ b/src/util/result.cpp
@@ -349,24 +349,21 @@ void Result::toStreamTptp(std::ostream& out) const {
 
 void Result::toStream(std::ostream& out, OutputLanguage language) const {
   switch (language) {
-    case language::output::LANG_SMTLIB_V2_0:
-    case language::output::LANG_SMTLIB_V2_5:
-    case language::output::LANG_SMTLIB_V2_6:
     case language::output::LANG_SYGUS:
-    case language::output::LANG_Z3STR:
       toStreamSmt2(out);
       break;
     case language::output::LANG_TPTP:
       toStreamTptp(out);
       break;
-    case language::output::LANG_AST:
-    case language::output::LANG_AUTO:
-    case language::output::LANG_CVC3:
-    case language::output::LANG_CVC4:
-    case language::output::LANG_MAX:
-    case language::output::LANG_SMTLIB_V1:
     default:
-      toStreamDefault(out);
+      if (language::isOutputLang_smt2(language))
+      {
+        toStreamSmt2(out);
+      }
+      else
+      {
+        toStreamDefault(out);
+      }
       break;
   };
 }
diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp
index 504d58b0e..fbc8802d6 100644
--- a/src/util/sexpr.cpp
+++ b/src/util/sexpr.cpp
@@ -273,18 +273,13 @@ void SExpr::toStreamRec(std::ostream& out, const SExpr& sexpr,
 bool SExpr::languageQuotesKeywords(OutputLanguage language) {
   switch (language) {
     case language::output::LANG_SMTLIB_V1:
-    case language::output::LANG_SMTLIB_V2_0:
-    case language::output::LANG_SMTLIB_V2_5:
-    case language::output::LANG_SMTLIB_V2_6:
     case language::output::LANG_SYGUS:
     case language::output::LANG_TPTP:
-    case language::output::LANG_Z3STR:
       return true;
     case language::output::LANG_AST:
     case language::output::LANG_CVC3:
     case language::output::LANG_CVC4:
-    default:
-      return false;
+    default: return language::isOutputLang_smt2(language);
   };
 }