Support the SMT-LIB Unicode string standard by default (#4378)

This PR merges --lang=smt2.6.1 and --lang=smt2.6 (default). It makes it so that 2.6 always expects the syntax of the string standard http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml.

I've updated the regressions so that the 2.6 benchmarks are now compliant with the standard. Some of the <=2.5 benchmarks I've updated to 2.6. Others I have left for now, in particular the ones that rely on special characters or ad-hoc escape sequences. The old formats will be supported in the release but removed shortly afterwards.

This PR is a prerequisite for the release, but not necessarily SMT-COMP (which will use --lang=smt2.6.1 if needed). Notice that we still do not have parsing support for str.replace_re or str.replace_re_all. This is required to be fully compliant.

4 files changed, 6 insertions, 28 deletions

diff --git a/src/options/language.cpp b/src/options/language.cpp
index 8c6f8421f..52263567b 100644
--- a/src/options/language.cpp
+++ b/src/options/language.cpp
@@ -21,10 +21,10 @@ namespace language {
 
 /** define the end points of smt2 languages */
 namespace input {
-Language LANG_SMTLIB_V2_END = LANG_SMTLIB_V2_6_1;
+Language LANG_SMTLIB_V2_END = LANG_SMTLIB_V2_6;
 }
 namespace output {
-Language LANG_SMTLIB_V2_END = LANG_SMTLIB_V2_6_1;
+Language LANG_SMTLIB_V2_END = LANG_SMTLIB_V2_6;
 }
 
 bool isInputLang_smt2(InputLanguage lang)
@@ -83,7 +83,6 @@ InputLanguage toInputLanguage(OutputLanguage language) {
   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:
@@ -106,7 +105,6 @@ 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:
@@ -152,11 +150,6 @@ OutputLanguage toOutputLanguage(std::string language) {
            || language == "LANG_SMTLIB_V2")
   {
     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" ||
@@ -197,11 +190,6 @@ 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 3a9ebf9d5..7866becd3 100644
--- a/src/options/language.h
+++ b/src/options/language.h
@@ -48,12 +48,10 @@ enum CVC4_PUBLIC Language
   LANG_SMTLIB_V2_0 = 0,
   /** The SMTLIB v2.5 input language */
   LANG_SMTLIB_V2_5,
-  /** The SMTLIB v2.6 input language */
+  /** The SMTLIB v2.6 input language, with support for the strings standard */
   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 */
@@ -87,7 +85,6 @@ 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;
@@ -129,12 +126,10 @@ enum CVC4_PUBLIC Language
   LANG_SMTLIB_V2_0 = input::LANG_SMTLIB_V2_0,
   /** The SMTLIB v2.5 output language */
   LANG_SMTLIB_V2_5 = input::LANG_SMTLIB_V2_5,
-  /** The SMTLIB v2.6 output language */
+  /** The SMTLIB v2.6 output language, with support for the strings standard */
   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 */
@@ -168,7 +163,6 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
     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;
diff --git a/src/options/language.i b/src/options/language.i
index f61359d4e..acda19aec 100644
--- a/src/options/language.i
+++ b/src/options/language.i
@@ -23,7 +23,6 @@ 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,7 +35,6 @@ 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 8a227a2e7..fe742adfc 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -416,8 +416,7 @@ Languages currently supported as arguments to the -L / --lang option:\n\
   smt | smtlib | smt2 |\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\
+  smt2.6 | smtlib2.6             SMT-LIB format 2.6 with support for the strings standard\n\
   tptp                           TPTP format (cnf, fof and tff)\n\
   sygus | sygus2                 SyGuS version 1.0 and 2.0 formats\n\
 \n\
@@ -428,8 +427,7 @@ Languages currently supported as arguments to the --output-lang option:\n\
   smt | smtlib | smt2 |\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\
+  smt2.6 | smtlib2.6             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\