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.

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current
index 8a1d674ed1182ecc8ee8ff92a76eaa72be2046e4..c7f9d0a710f7965213023390218d71ba4b194272 100755 (executable)
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current
@@ -141,8 +141,8 @@ QF_ALIA)
   finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas
   ;;
 QF_S|QF_SLIA)
-  trywith 300 --strings-exp --rewrite-divk --lang=smt2.6.1 --strings-fmf
-  finishwith --strings-exp --rewrite-divk --lang=smt2.6.1
+  trywith 300 --strings-exp --rewrite-divk --strings-fmf
+  finishwith --strings-exp --rewrite-divk
   ;;
 QF_ABVFP)
   finishwith --fp-exp

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
index 5e827128e9669180e404c5a7eb4e308a07048904..6cebad7fd0dbe6c09b8a6425fe5bdd06be6d0df0 100755 (executable)
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
@@ -66,7 +66,7 @@ QF_ALIA)
   finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas
   ;;
 QF_S|QF_SLIA)
-  finishwith --strings-exp --rewrite-divk --lang=smt2.6.1
+  finishwith --strings-exp --rewrite-divk
   ;;
 QF_ABVFP)
   finishwith --fp-exp

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 24cd762a1323ad1483e64093962073006bb18ab6..b27cc48b460f712eb742a396c6d5224f4d7a68ef 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -4384,9 +4384,9 @@ void Solver::setInfo(const std::string& keyword, const std::string& value) const
          "'notes', 'smt-lib-version' or 'status'";
   CVC4_API_ARG_CHECK_EXPECTED(keyword != "smt-lib-version" || value == "2"
                                   || value == "2.0" || value == "2.5"
-                                  || value == "2.6" || value == "2.6.1",
+                                  || value == "2.6",
                               value)
-      << "'2.0', '2.5', '2.6' or '2.6.1'";
+      << "'2.0', '2.5', '2.6'";
   CVC4_API_ARG_CHECK_EXPECTED(keyword != "status" || value == "sat"
                                   || value == "unsat" || value == "unknown",
                               value)

diff --git a/src/options/language.cpp b/src/options/language.cpp
index 8c6f8421ff6da3f36ac5f40391c0f1d8158abd6c..52263567b3d1febb2caaa1ba6c12fc44d645278f 100644 (file)
--- 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 3a9ebf9d5e208b2ff4c5f90489dcdd9502ab7a69..7866becd3707440c2fa493b864e141906684e42f 100644 (file)
--- 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 f61359d4e0d37bb7787678b4fb8de1f4385e72fa..acda19aeca5cd01c5adafcf8c4654e7119a2d688 100644 (file)
--- 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 8a227a2e76b17aaad54a0c7e91754d6e3510fcda..fe742adfc4c590f0aabb8e4ebf0e8806c766efc2 100644 (file)
--- 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\

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 5dca923708c3f3e48c4460204269b7a56c753ee5..c860d14c7ff2c72ee411d78524f94f575ea2c8d3 100644 (file)
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -895,8 +895,7 @@ std::vector<unsigned> Parser::processAdHocStringEsc(const std::string& s)
 Expr Parser::mkStringConstant(const std::string& s)
 {
   ExprManager* em = d_solver->getExprManager();
-  if (em->getOptions().getInputLanguage()
-      == language::input::LANG_SMTLIB_V2_6_1)
+  if (language::isInputLang_smt2_6(em->getOptions().getInputLanguage()))
   {
     return d_solver->mkString(s, true).getExpr();
   }

diff --git a/src/parser/parser.h b/src/parser/parser.h
index cd4105cd0cffb6f749a9b7a9147e029d3a023563..7941cfdd577a479ca2d090b585ded69b3c0fb33e 100644 (file)
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -842,7 +842,7 @@ public:
    *
    * This makes the string constant based on the string s. This may involve
    * processing ad-hoc escape sequences (if the language is not
-   * SMT-LIB 2.6.1 or higher), or otherwise calling the solver to construct
+   * SMT-LIB 2.6 or higher), or otherwise calling the solver to construct
    * the string.
    */
   Expr mkStringConstant(const std::string& s);

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 6cba1ce1903f6e021c7ffa020098d95ce8b15221..3c30f5c49970d4270788325869af8fec06c533c4 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -166,8 +166,8 @@ void Smt2::addStringOperators() {
   addOperator(api::STRING_SUFFIX, "str.suffixof");
   addOperator(api::STRING_FROM_CODE, "str.from_code");
   addOperator(api::STRING_IS_DIGIT, "str.is_digit");
-  // at the moment, we only use this syntax for smt2.6.1
-  if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1
+  // at the moment, we only use this syntax for smt2.6
+  if (getLanguage() == language::input::LANG_SMTLIB_V2_6
       || getLanguage() == language::input::LANG_SYGUS_V2)
   {
     addOperator(api::STRING_ITOS, "str.from_int");
@@ -682,7 +682,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
     defineType("RegLan", d_solver->getRegExpSort());
     defineType("Int", d_solver->getIntegerSort());
 
-    if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1
+    if (getLanguage() == language::input::LANG_SMTLIB_V2_6
         || getLanguage() == language::input::LANG_SYGUS_V2)
     {
       defineVar("re.none", d_solver->mkRegexpEmpty());

diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 886be0cfabc61fc98aa392dedda3c77ab7ce011e..085a32c434eddbc117e1509676d06dd6eb094174 100644 (file)
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -46,10 +46,6 @@ 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());
 
@@ -68,7 +64,7 @@ unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang)
     // sygus version 2.0 does not have discrepancies with smt2, hence we use
     // a normal smt2 variant here.
     return unique_ptr<Printer>(
-        new printer::smt2::Smt2Printer(printer::smt2::smt2_6_1_variant));
+        new printer::smt2::Smt2Printer(printer::smt2::smt2_6_variant));
 
   case LANG_AST:
     return unique_ptr<Printer>(new printer::ast::AstPrinter());

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 4013cbd083bd5cee29aebbc403e74790d1710e4c..fbccd26ed35064f43f3b2b69df6dbf9390a24c09 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -48,10 +48,7 @@ static OutputLanguage variantToLanguage(Variant v);
 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;
-}
+bool isVariant_2_6(Variant v) { return v == smt2_6_variant; }
 
 static void toStreamRational(std::ostream& out,
                              const Rational& r,
@@ -1203,8 +1200,7 @@ static string smtKindString(Kind k, Variant v)
   case kind::STRING_CHARAT: return "str.at" ;
   case kind::STRING_STRIDOF: return "str.indexof" ;
   case kind::STRING_STRREPL: return "str.replace" ;
-  case kind::STRING_STRREPLALL:
-    return v == smt2_6_1_variant ? "str.replace_all" : "str.replaceall";
+  case kind::STRING_STRREPLALL: return "str.replace_all";
   case kind::STRING_TOLOWER: return "str.tolower";
   case kind::STRING_TOUPPER: return "str.toupper";
   case kind::STRING_REV: return "str.rev";
@@ -1213,16 +1209,11 @@ static string smtKindString(Kind k, Variant v)
   case kind::STRING_LEQ: return "str.<=";
   case kind::STRING_LT: return "str.<";
   case kind::STRING_FROM_CODE: return "str.from_code";
-  case kind::STRING_TO_CODE:
-    return v == smt2_6_1_variant ? "str.to_code" : "str.code";
-  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::STRING_TO_CODE: return "str.to_code";
+  case kind::STRING_ITOS: return "str.from_int";
+  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::REGEXP_EMPTY: return "re.nostr";
   case kind::REGEXP_SIGMA: return "re.allchar";
   case kind::REGEXP_CONCAT: return "re.++";

diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index 57923136411e4726794a9ce0acdd95a10926c917..b34acacbbf15664c373c8d8dbe686c34e581fe0e 100644 (file)
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -30,13 +30,12 @@ namespace smt2 {
 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
-  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 */
+  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, 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 990ffd04d77109f02c34258532a3067d81004699..d4e83c672b4feb83097c2112c9044e2bd6a264f6 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -990,10 +990,6 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
                value.getValue() == "2.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;

diff --git a/test/regress/regress0/lang_opts_2_6_1.smt2 b/test/regress/regress0/lang_opts_2_6_1.smt2
index bb005d527b8d4bb6b3212bb2f17e02ea564bbb8b..9701df4556b6c548ddb71c396b12a7549e9b4c62 100644 (file)
--- a/test/regress/regress0/lang_opts_2_6_1.smt2
+++ b/test/regress/regress0/lang_opts_2_6_1.smt2
@@ -1,7 +1,7 @@
 ; Check that the language set in the command line options has higher priority
 ; than the language specified in the input file.
 ;
-; COMMAND-LINE: --lang=smt2.6.1
-; EXPECT: "LANG_SMTLIB_V2_6_1"
+; COMMAND-LINE: --lang=smt2.6
+; EXPECT: "LANG_SMTLIB_V2_6"
 (set-info :smt-lib-version 2.6)
 (get-option :input-language)

diff --git a/test/regress/regress0/strings/bidir_star.smt2 b/test/regress/regress0/strings/bidir_star.smt2
index 7303d138f6bf69089956b08742e6095747e13780..8a13ed085e2e19f68efca6e9d128a8fc3a4dad7f 100644 (file)
--- a/test/regress/regress0/strings/bidir_star.smt2
+++ b/test/regress/regress0/strings/bidir_star.smt2
@@ -2,7 +2,7 @@
 (set-logic SLIA)
 (declare-fun a () String)
 (assert (>= (str.len a) 2))
-(assert (str.in.re a (re.+ (re.range "0" "1"))))
-(assert (<= 3 (str.to.int (str.substr a (+ (- 2) (str.len a)) 1))))
+(assert (str.in_re a (re.+ (re.range "0" "1"))))
+(assert (<= 3 (str.to_int (str.substr a (+ (- 2) (str.len a)) 1))))
 (set-info :status unsat)
 (check-sat)

diff --git a/test/regress/regress0/strings/bug001.smt2 b/test/regress/regress0/strings/bug001.smt2
index cdeebd20bdf09883113c17b8fdfc72f430439261..a8d2d8992f489695258473080fe23a3623ea10d9 100644 (file)
--- a/test/regress/regress0/strings/bug001.smt2
+++ b/test/regress/regress0/strings/bug001.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 

diff --git a/test/regress/regress0/strings/char-representations.smt2 b/test/regress/regress0/strings/char-representations.smt2
index aaf119ab42067cc91cbc4f6bc91a4dbf48b1e6ad..1b3cef25aab06d9ab48b8c7d09104e367cdc19b8 100644 (file)
--- a/test/regress/regress0/strings/char-representations.smt2
+++ b/test/regress/regress0/strings/char-representations.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=smt2.6.1
+; COMMAND-LINE: --lang=smt2.6
 ; EXPECT: sat
 (set-logic SLIA)
 (set-info :status sat)

diff --git a/test/regress/regress0/strings/code-eval.smt2 b/test/regress/regress0/strings/code-eval.smt2
index faa5c174c56c521b533e2f22a178fd3cd6ef7350..bc5f964945a0b2fc65ac422c61ed42327eed6f64 100644 (file)
--- a/test/regress/regress0/strings/code-eval.smt2
+++ b/test/regress/regress0/strings/code-eval.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=smt2.6.1
+; COMMAND-LINE: --lang=smt2.6
 ; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)

diff --git a/test/regress/regress0/strings/code-perf.smt2 b/test/regress/regress0/strings/code-perf.smt2
index 4d7e22bd314700cb60eb6efb73cbda5896ae8ca2..e2b41c67f12f2bd636b24ea5cca3be40fada1a24 100644 (file)
--- a/test/regress/regress0/strings/code-perf.smt2
+++ b/test/regress/regress0/strings/code-perf.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --strings-exp
 ; EXPECT: sat
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_SLIA)
 (declare-const x0 String)
 (declare-const x1 String)
@@ -24,17 +24,17 @@
 (declare-const y8 Int)
 (declare-const y9 Int)
 (declare-const y10 Int)
-(assert (and (= y0 (str.code x0)) (>= y0 (str.code "0")) (<= y0 (str.code "9"))))
-(assert (and (= y1 (str.code x1)) (>= y1 (str.code "0")) (<= y1 (str.code "9"))))
-(assert (and (= y2 (str.code x2)) (>= y2 (str.code "0")) (<= y2 (str.code "9"))))
-(assert (and (= y3 (str.code x3)) (>= y3 (str.code "0")) (<= y3 (str.code "9"))))
-(assert (and (= y4 (str.code x4)) (>= y4 (str.code "0")) (<= y4 (str.code "9"))))
-(assert (and (= y5 (str.code x5)) (>= y5 (str.code "0")) (<= y5 (str.code "9"))))
-(assert (and (= y6 (str.code x6)) (>= y6 (str.code "0")) (<= y6 (str.code "9"))))
-(assert (and (= y7 (str.code x7)) (>= y7 (str.code "0")) (<= y7 (str.code "9"))))
-(assert (and (= y8 (str.code x8)) (>= y8 (str.code "0")) (<= y8 (str.code "9"))))
-(assert (and (= y9 (str.code x9)) (>= y9 (str.code "0")) (<= y9 (str.code "9"))))
-(assert (and (= y10 (str.code x10)) (>= y10 (str.code "0")) (<= y10 (str.code "9"))))
+(assert (and (= y0 (str.to_code x0)) (>= y0 (str.to_code "0")) (<= y0 (str.to_code "9"))))
+(assert (and (= y1 (str.to_code x1)) (>= y1 (str.to_code "0")) (<= y1 (str.to_code "9"))))
+(assert (and (= y2 (str.to_code x2)) (>= y2 (str.to_code "0")) (<= y2 (str.to_code "9"))))
+(assert (and (= y3 (str.to_code x3)) (>= y3 (str.to_code "0")) (<= y3 (str.to_code "9"))))
+(assert (and (= y4 (str.to_code x4)) (>= y4 (str.to_code "0")) (<= y4 (str.to_code "9"))))
+(assert (and (= y5 (str.to_code x5)) (>= y5 (str.to_code "0")) (<= y5 (str.to_code "9"))))
+(assert (and (= y6 (str.to_code x6)) (>= y6 (str.to_code "0")) (<= y6 (str.to_code "9"))))
+(assert (and (= y7 (str.to_code x7)) (>= y7 (str.to_code "0")) (<= y7 (str.to_code "9"))))
+(assert (and (= y8 (str.to_code x8)) (>= y8 (str.to_code "0")) (<= y8 (str.to_code "9"))))
+(assert (and (= y9 (str.to_code x9)) (>= y9 (str.to_code "0")) (<= y9 (str.to_code "9"))))
+(assert (and (= y10 (str.to_code x10)) (>= y10 (str.to_code "0")) (<= y10 (str.to_code "9"))))
 (assert (= (str.len x0) 1))
 (assert (= (str.len x1) 1))
 (assert (= (str.len x2) 1))

diff --git a/test/regress/regress0/strings/code-sat-neg-one.smt2 b/test/regress/regress0/strings/code-sat-neg-one.smt2
index 403319d02e9af059f255a1682963d3df0d2ed776..3e7161328aed22f3537d948fbae9b6a3bdee3b13 100644 (file)
--- a/test/regress/regress0/strings/code-sat-neg-one.smt2
+++ b/test/regress/regress0/strings/code-sat-neg-one.smt2
@@ -1,8 +1,8 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_SLIA)
 (set-info :status sat)
 (declare-fun x () String)
 (declare-fun y () String)
 (assert (not (= x y)))
-(assert (= (str.code x) (str.code y)))
+(assert (= (str.to_code x) (str.to_code y)))
 (check-sat)

diff --git a/test/regress/regress0/strings/complement-simple.smt2 b/test/regress/regress0/strings/complement-simple.smt2
index c19699448c793fbabb000d26e72ad61cc113ed41..d86fcd225804583d0160df469e6185cd1914a6eb 100644 (file)
--- a/test/regress/regress0/strings/complement-simple.smt2
+++ b/test/regress/regress0/strings/complement-simple.smt2
@@ -1,5 +1,5 @@
 (set-logic SLIA)
 (set-info :status sat)
 (declare-fun x () String)
-(assert (str.in.re x (re.comp (str.to.re "ABC"))))
+(assert (str.in_re x (re.comp (str.to_re "ABC"))))
 (check-sat)

diff --git a/test/regress/regress0/strings/escchar_25.smt2 b/test/regress/regress0/strings/escchar_25.smt2
index af93a7ae5786fe24586bafa183cb66fd7d37d55e..a8a7c242f252d3557e5a31cf01594c17268faf23 100644 (file)
--- a/test/regress/regress0/strings/escchar_25.smt2
+++ b/test/regress/regress0/strings/escchar_25.smt2
@@ -1,6 +1,6 @@
 (set-logic QF_S)
 (set-info :status sat)
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 
 (declare-fun x () String)
 (declare-const I Int)

diff --git a/test/regress/regress0/strings/from_code.smt2 b/test/regress/regress0/strings/from_code.smt2
index ecde829ecaf63d030963ad39b8f79c462b95805f..c9b49a931b28e87d7ae84da289c015f1b9856923 100644 (file)
--- a/test/regress/regress0/strings/from_code.smt2
+++ b/test/regress/regress0/strings/from_code.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=smt2.6.1
+; COMMAND-LINE: --lang=smt2.6
 ; EXPECT: unsat
 ; EXPECT: unsat
 ; EXPECT: sat

diff --git a/test/regress/regress0/strings/gen-esc-seq.smt2 b/test/regress/regress0/strings/gen-esc-seq.smt2
index 59f66046f2d3080c1c069cc147872800cdfda54f..19edd7fc0cb2612324b7892cfda7dc7e7b0480cf 100644 (file)
--- a/test/regress/regress0/strings/gen-esc-seq.smt2
+++ b/test/regress/regress0/strings/gen-esc-seq.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --produce-models --lang=smt2.6.1
+; COMMAND-LINE: --produce-models --lang=smt2.6
 ; EXPECT: sat
 ; EXPECT: ((x "\u{5c}u1000"))
 (set-logic ALL)

diff --git a/test/regress/regress0/strings/is_digit_simple.smt2 b/test/regress/regress0/strings/is_digit_simple.smt2
index d95a22078933dc830aa212b4bb6ca06384d14195..d69ec6b21e69bd9a3563ff6c16ae423e3053d26d 100644 (file)
--- a/test/regress/regress0/strings/is_digit_simple.smt2
+++ b/test/regress/regress0/strings/is_digit_simple.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=smt2.6.1
+; COMMAND-LINE: --lang=smt2.6
 ; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)

diff --git a/test/regress/regress0/strings/issue1189.smt2 b/test/regress/regress0/strings/issue1189.smt2
index 0b581994c4b383b4c46e32e1b6d9eb5e6b4dade0..3200c815d347b8bae4b32b1605467fa56a59dc10 100644 (file)
--- a/test/regress/regress0/strings/issue1189.smt2
+++ b/test/regress/regress0/strings/issue1189.smt2
@@ -1,7 +1,7 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic ALL_SUPPORTED)
 (set-info :status unsat)
 (set-option :strings-exp true)
 (declare-const x Int)
-(assert (str.contains (str.++ "some text" (int.to.str x) "tor") "vector"))
+(assert (str.contains (str.++ "some text" (str.from_int x) "tor") "vector"))
 (check-sat)

diff --git a/test/regress/regress0/strings/issue2958.smt2 b/test/regress/regress0/strings/issue2958.smt2
index 7ed5ef7f3b0aea4447b2f4a0444a5d7c2af9bb7e..99d8462c34756ccf21cfb5cc715780d5af5186a2 100644 (file)
--- a/test/regress/regress0/strings/issue2958.smt2
+++ b/test/regress/regress0/strings/issue2958.smt2
@@ -1,7 +1,7 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_SLIA)
 (set-info :status unsat)
 (declare-const x String)
 (assert (not (str.prefixof "ab" x)))
-(assert (str.in.re (str.substr x 0 2) (re.++ (str.to.re "ab") (re.* (str.to.re "dcab")))))
+(assert (str.in_re (str.substr x 0 2) (re.++ (str.to_re "ab") (re.* (str.to_re "dcab")))))
 (check-sat)

diff --git a/test/regress/regress0/strings/issue3440.smt2 b/test/regress/regress0/strings/issue3440.smt2
index 7eb3419f237ba96a168d7cfc7e3e976e8e83235a..32f6bf90f88ca8451f4c1c651c4b5edf5c9e48c1 100644 (file)
--- a/test/regress/regress0/strings/issue3440.smt2
+++ b/test/regress/regress0/strings/issue3440.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-strings-lazy-pp
 ; EXPECT: sat
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_S)
 (set-info :status sat)
 (declare-fun a () String)                                                       

diff --git a/test/regress/regress0/strings/issue3497.smt2 b/test/regress/regress0/strings/issue3497.smt2
index c804de820aa0e1d1be3a658e688702787dab51d4..99597dffaafeffba98841b9a9a53d488dbb2ff80 100644 (file)
--- a/test/regress/regress0/strings/issue3497.smt2
+++ b/test/regress/regress0/strings/issue3497.smt2
@@ -1,4 +1,4 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_SLIA)
 (set-info :status sat)
 (set-option :strings-exp true)

diff --git a/test/regress/regress0/strings/issue3657-evalLeq.smt2 b/test/regress/regress0/strings/issue3657-evalLeq.smt2
index a557f4e6266dee0b4e2788fb4302959a2ffd57b5..91295f73a2cc24e28d6b58917ff75913a74c2171 100644 (file)
--- a/test/regress/regress0/strings/issue3657-evalLeq.smt2
+++ b/test/regress/regress0/strings/issue3657-evalLeq.smt2
@@ -1,4 +1,4 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic ALL)
 (set-info :status sat)
 (assert (not (str.< "\xe8" "\x19")))

diff --git a/test/regress/regress0/strings/issue4070.smt2 b/test/regress/regress0/strings/issue4070.smt2
index 2de58c4d25fcc1a49f2be6d4741d3e718d093112..a629c30ecd8d913aac51ee8cb14b70c19d9a01e8 100644 (file)
--- a/test/regress/regress0/strings/issue4070.smt2
+++ b/test/regress/regress0/strings/issue4070.smt2
@@ -2,5 +2,5 @@
 (set-logic QF_S)
 (declare-fun a () String)
 (declare-fun b () String)
-(assert (str.in.re a (re.++ (str.to.re b) (re.* re.allchar))))
+(assert (str.in_re a (re.++ (str.to_re b) (re.* re.allchar))))
 (check-sat)

diff --git a/test/regress/regress0/strings/issue4376.smt2 b/test/regress/regress0/strings/issue4376.smt2
index f6dd8805907e99f4d72e12b65b3c8f384cd0bea9..3a7088c5b9213c8dd7791a16df507547714164bb 100644 (file)
--- a/test/regress/regress0/strings/issue4376.smt2
+++ b/test/regress/regress0/strings/issue4376.smt2
@@ -7,5 +7,5 @@
 (declare-const Str11 String)
 (declare-const Str15 String)
 (assert (= (str.++ Str1 "ijruldtzyp") Str15))
-(assert (= (str.++ (str.++ Str1 "ijruldtzyp") Str11 (int.to.str i0)) Str15 Str9))
+(assert (= (str.++ (str.++ Str1 "ijruldtzyp") Str11 (str.from_int i0)) Str15 Str9))
 (check-sat)

diff --git a/test/regress/regress0/strings/itos-entail.smt2 b/test/regress/regress0/strings/itos-entail.smt2
index f9dcf4c7703eb7b800b24b7ef06cb0c0aa59594c..aca5e4f6ac3d1b43f6822c1f09794000a5ad7978 100644 (file)
--- a/test/regress/regress0/strings/itos-entail.smt2
+++ b/test/regress/regress0/strings/itos-entail.smt2
@@ -1,4 +1,4 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic ALL)
 (set-info :status sat)
 (set-option :strings-exp true)
@@ -6,6 +6,6 @@
 (declare-fun y () String)
 (declare-fun z () String)
 
-(assert (str.contains "ABCD" (str.++ y (int.to.str x) z)))
+(assert (str.contains "ABCD" (str.++ y (str.from_int x) z)))
 
 (check-sat)

diff --git a/test/regress/regress0/strings/large-model.smt2 b/test/regress/regress0/strings/large-model.smt2
index ca52e816bfd8552824f2843b037030e39c413e9e..74b781c82932992ba2dc05c55864377c315a8f4a 100644 (file)
--- a/test/regress/regress0/strings/large-model.smt2
+++ b/test/regress/regress0/strings/large-model.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=smt2.6.1 --check-models
+; COMMAND-LINE: --lang=smt2.6 --check-models
 ; EXPECT: (error "Cannot generate model with string whose length exceeds UINT32_MAX")
 ; EXIT: 1
 (set-logic SLIA)

diff --git a/test/regress/regress0/strings/leadingzero001.smt2 b/test/regress/regress0/strings/leadingzero001.smt2
index 09fd80a7b7e6b757f372094b367b271ea47be057..d646a8930845fdd8b7ed998839965b6913170158 100644 (file)
--- a/test/regress/regress0/strings/leadingzero001.smt2
+++ b/test/regress/regress0/strings/leadingzero001.smt2
@@ -1,4 +1,4 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_S)
 (set-option :strings-exp true)
 (set-info :status sat)
@@ -6,7 +6,7 @@
 (declare-fun Y () String)
 
 (assert (= Y "0001"))
-;(assert (= (str.to.int Y) (- 1)))
-(assert (= (str.to.int Y) 1))
+;(assert (= (str.to_int Y) (- 1)))
+(assert (= (str.to_int Y) 1))
 
 (check-sat)

diff --git a/test/regress/regress0/strings/loop-wrong-sem.smt2 b/test/regress/regress0/strings/loop-wrong-sem.smt2
index d0dd3fcb244655b306ee93339f69a7f26dc4b279..32ec26c0a4da6caf748f304dc4063c9894e1fb89 100644 (file)
--- a/test/regress/regress0/strings/loop-wrong-sem.smt2
+++ b/test/regress/regress0/strings/loop-wrong-sem.smt2
@@ -1,4 +1,4 @@
 (set-logic ALL)
 (set-info :status unsat)
-(assert (str.in.re "" ((_ re.loop 1 0) (str.to.re ""))))
+(assert (str.in_re "" ((_ re.loop 1 0) (str.to_re ""))))
 (check-sat)

diff --git a/test/regress/regress0/strings/model-code-point.smt2 b/test/regress/regress0/strings/model-code-point.smt2
index 1200ae704aa0fd4fa3e39288d2bb9e117a0a0085..86cb24fc736eb096bfc1f5a4b33838a25a508ea7 100644 (file)
--- a/test/regress/regress0/strings/model-code-point.smt2
+++ b/test/regress/regress0/strings/model-code-point.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=smt2.6.1 --produce-models
+; COMMAND-LINE: --lang=smt2.6 --produce-models
 ; EXPECT: sat
 ; EXPECT: ((x "\u{a}"))
 ; EXPECT: ((y "\u{7f}"))

diff --git a/test/regress/regress0/strings/model-friendly.smt2 b/test/regress/regress0/strings/model-friendly.smt2
index 985ffaa626cb5e471f327e96423306dd11869f38..21a89c00cacf7dd13999f88e351c7a02786dcab0 100644 (file)
--- a/test/regress/regress0/strings/model-friendly.smt2
+++ b/test/regress/regress0/strings/model-friendly.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=smt2.6.1 --produce-models
+; COMMAND-LINE: --lang=smt2.6 --produce-models
 ; EXPECT: sat
 ; EXPECT: ((x "AAAAA"))
 (set-logic ALL)

diff --git a/test/regress/regress0/strings/norn-31.smt2 b/test/regress/regress0/strings/norn-31.smt2
index 1830dd882fa79c016d415b7cf26ae4d1b522c67e..be759a8856a50a98cb4b89eeab69e82b6c9eaea7 100644 (file)
--- a/test/regress/regress0/strings/norn-31.smt2
+++ b/test/regress/regress0/strings/norn-31.smt2
@@ -1,4 +1,4 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-info :status unsat)
@@ -17,8 +17,8 @@
 (declare-fun var_11 () String)
 (declare-fun var_12 () String)
 
-(assert (str.in.re var_1 (re.* (re.range "a" "u"))))
-(assert (str.in.re var_1 (re.++ (re.* (str.to.re "a")) (str.to.re "b"))))
-(assert (str.in.re var_1 (re.++ (re.++ (re.++ (re.* (re.union (str.to.re "a") (str.to.re "b"))) (str.to.re "b")) (str.to.re "a")) (re.* (re.union (str.to.re "a") (str.to.re "b"))))))
-(assert (not (str.in.re "" re.nostr)))
+(assert (str.in_re var_1 (re.* (re.range "a" "u"))))
+(assert (str.in_re var_1 (re.++ (re.* (str.to_re "a")) (str.to_re "b"))))
+(assert (str.in_re var_1 (re.++ (re.++ (re.++ (re.* (re.union (str.to_re "a") (str.to_re "b"))) (str.to_re "b")) (str.to_re "a")) (re.* (re.union (str.to_re "a") (str.to_re "b"))))))
+(assert (not (str.in_re "" re.none)))
 (check-sat)

diff --git a/test/regress/regress0/strings/norn-simp-rew.smt2 b/test/regress/regress0/strings/norn-simp-rew.smt2
index d729fe5d0106fb15a8511d98a884297ebb87bae6..4ef281ce9148ee68bde2e0bb4368ae576439f358 100644 (file)
--- a/test/regress/regress0/strings/norn-simp-rew.smt2
+++ b/test/regress/regress0/strings/norn-simp-rew.smt2
@@ -1,4 +1,4 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-info :status unsat)
@@ -17,14 +17,14 @@
 (declare-fun var_11 () String)
 (declare-fun var_12 () String)
 
-(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.union (re.union (str.to.re "z") (str.to.re "a")) (re.++ (str.to.re "b") (re.++ (re.* (str.to.re "b")) (re.union (str.to.re "z") (str.to.re "a")))))) (re.++ (str.to.re "b") (re.* (str.to.re "b"))))))
-(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.union (str.to.re "a") (re.++ (str.to.re "b") (re.++ (re.* (re.union (str.to.re "b") (str.to.re "a"))) (str.to.re "z"))))) (re.++ (str.to.re "b") (re.* (re.union (str.to.re "b") (str.to.re "a")))))))
-(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.++ (str.to.re "b") (re.++ (re.* (re.union (str.to.re "z") (str.to.re "b"))) (str.to.re "a")))) (re.++ (str.to.re "b") (re.* (re.union (str.to.re "z") (str.to.re "b")))))))
-(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.union (str.to.re "z") (re.++ (re.union (str.to.re "b") (str.to.re "a")) (re.union (str.to.re "z") (str.to.re "b"))))) (re.union (str.to.re "b") (str.to.re "a")))))
-(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.* (re.++ (str.to.re "b") (re.++ (re.* (str.to.re "z")) (str.to.re "b"))))))
-(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.++ (str.to.re "b") (str.to.re "z"))) (str.to.re "b"))))
-(assert (str.in.re (str.++ "a" var_8 ) (re.* (re.range "a" "u"))))
-(assert (str.in.re var_8 (re.* (re.range "a" "u"))))
-(assert (str.in.re var_7 (re.* (re.range "a" "u"))))
-(assert (not (str.in.re (str.++ "b" var_7 ) (re.* (re.range "a" "u")))))
+(assert (str.in_re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.union (re.union (str.to_re "z") (str.to_re "a")) (re.++ (str.to_re "b") (re.++ (re.* (str.to_re "b")) (re.union (str.to_re "z") (str.to_re "a")))))) (re.++ (str.to_re "b") (re.* (str.to_re "b"))))))
+(assert (str.in_re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.union (str.to_re "a") (re.++ (str.to_re "b") (re.++ (re.* (re.union (str.to_re "b") (str.to_re "a"))) (str.to_re "z"))))) (re.++ (str.to_re "b") (re.* (re.union (str.to_re "b") (str.to_re "a")))))))
+(assert (str.in_re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.++ (str.to_re "b") (re.++ (re.* (re.union (str.to_re "z") (str.to_re "b"))) (str.to_re "a")))) (re.++ (str.to_re "b") (re.* (re.union (str.to_re "z") (str.to_re "b")))))))
+(assert (str.in_re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.union (str.to_re "z") (re.++ (re.union (str.to_re "b") (str.to_re "a")) (re.union (str.to_re "z") (str.to_re "b"))))) (re.union (str.to_re "b") (str.to_re "a")))))
+(assert (str.in_re (str.++ var_7 "z" var_8 ) (re.* (re.++ (str.to_re "b") (re.++ (re.* (str.to_re "z")) (str.to_re "b"))))))
+(assert (str.in_re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.++ (str.to_re "b") (str.to_re "z"))) (str.to_re "b"))))
+(assert (str.in_re (str.++ "a" var_8 ) (re.* (re.range "a" "u"))))
+(assert (str.in_re var_8 (re.* (re.range "a" "u"))))
+(assert (str.in_re var_7 (re.* (re.range "a" "u"))))
+(assert (not (str.in_re (str.++ "b" var_7 ) (re.* (re.range "a" "u")))))
 (check-sat)

diff --git a/test/regress/regress0/strings/re-syntax.smt2 b/test/regress/regress0/strings/re-syntax.smt2
index 4c25a65a4b0097dc7db5c340d7e6ffb9b13712db..f073884b807f56757d98fd2a4e4b1b7e7685261d 100644 (file)
--- a/test/regress/regress0/strings/re-syntax.smt2
+++ b/test/regress/regress0/strings/re-syntax.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=smt2.6.1
+; COMMAND-LINE: --lang=smt2.6
 ; EXPECT: unsat
 (set-logic ALL)
 (set-info :status unsat)

diff --git a/test/regress/regress0/strings/re.all.smt2 b/test/regress/regress0/strings/re.all.smt2
index 5200b924f5a374afa9d2017480e6c08a6cf1a426..d17a0d0499bbb6130a3706de46f9394e982a2895 100644 (file)
--- a/test/regress/regress0/strings/re.all.smt2
+++ b/test/regress/regress0/strings/re.all.smt2
@@ -1,6 +1,6 @@
 (set-logic QF_SLIA)
 (set-info :status unsat)
 (declare-const x String)
-(assert (str.in.re x (re.++ (str.to.re "abc") re.all)))
+(assert (str.in_re x (re.++ (str.to_re "abc") re.all)))
 (assert (not (str.prefixof "abc" x)))
 (check-sat)

diff --git a/test/regress/regress0/strings/re_diff.smt2 b/test/regress/regress0/strings/re_diff.smt2
index d63731acbc2674f27b152f213434d0ee081789b1..a20c5be7efe148aaf8372a7bb6879fde545d53cc 100644 (file)
--- a/test/regress/regress0/strings/re_diff.smt2
+++ b/test/regress/regress0/strings/re_diff.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=smt2.6.1
+; COMMAND-LINE: --lang=smt2.6
 ; EXPECT: unsat
 (set-logic ALL)
 (set-info :status unsat)

diff --git a/test/regress/regress0/strings/regexp_inclusion.smt2 b/test/regress/regress0/strings/regexp_inclusion.smt2
index c5c68a408ce71e846444a15ae2df37889935862a..648a1b11103f374b48e14c757c7b218acc0b4b5c 100644 (file)
--- a/test/regress/regress0/strings/regexp_inclusion.smt2
+++ b/test/regress/regress0/strings/regexp_inclusion.smt2
@@ -4,10 +4,10 @@
 (declare-const actionName String)
 
 (assert
-(str.in.re actionName (re.++ (str.to.re "wiz") (re.* re.allchar) (str.to.re "foobar") (re.* re.allchar) (str.to.re "baz/") (re.* re.allchar))))
+(str.in_re actionName (re.++ (str.to_re "wiz") (re.* re.allchar) (str.to_re "foobar") (re.* re.allchar) (str.to_re "baz/") (re.* re.allchar))))
 
 (assert (not
-(str.in.re actionName (re.++ (str.to.re "wiz") (re.* re.allchar) (re.++ (str.to.re "foo") re.allchar (str.to.re "ar")) (re.* re.allchar) (str.to.re "baz/") (re.* re.allchar)))
+(str.in_re actionName (re.++ (str.to_re "wiz") (re.* re.allchar) (re.++ (str.to_re "foo") re.allchar (str.to_re "ar")) (re.* re.allchar) (str.to_re "baz/") (re.* re.allchar)))
 ))
 
 (check-sat)

diff --git a/test/regress/regress0/strings/regexp_inclusion_reduction.smt2 b/test/regress/regress0/strings/regexp_inclusion_reduction.smt2
index c10c287bbfe829177ecb18af10c3644c2a3f06d8..20ac8f4e497db1683407db3bc53ea6a32b3cec0b 100644 (file)
--- a/test/regress/regress0/strings/regexp_inclusion_reduction.smt2
+++ b/test/regress/regress0/strings/regexp_inclusion_reduction.smt2
@@ -4,11 +4,11 @@
 (declare-const x String)
 (declare-const y String)
 
-(assert (str.in.re x (re.++ (str.to.re "bar") (re.* re.allchar) (str.to.re "bar"))))
-(assert (str.in.re x (re.++ (str.to.re "ba") re.allchar (re.* re.allchar) (str.to.re "bar"))))
+(assert (str.in_re x (re.++ (str.to_re "bar") (re.* re.allchar) (str.to_re "bar"))))
+(assert (str.in_re x (re.++ (str.to_re "ba") re.allchar (re.* re.allchar) (str.to_re "bar"))))
 
-(assert (not (str.in.re y (re.++ (str.to.re "bar") (re.* re.allchar) (str.to.re "bar")))))
-(assert (not (str.in.re y (re.++ (str.to.re "ba") re.allchar (re.* re.allchar) (str.to.re "bar")))))
+(assert (not (str.in_re y (re.++ (str.to_re "bar") (re.* re.allchar) (str.to_re "bar")))))
+(assert (not (str.in_re y (re.++ (str.to_re "ba") re.allchar (re.* re.allchar) (str.to_re "bar")))))
 (assert (not (= y "")))
 
 (check-sat)

diff --git a/test/regress/regress0/strings/replace-const.smt2 b/test/regress/regress0/strings/replace-const.smt2
index a7f225e33b1c3c5b28e0360093ed917449495733..8b1b182e37c20930a39a02d0c23d704975cf2c18 100644 (file)
--- a/test/regress/regress0/strings/replace-const.smt2
+++ b/test/regress/regress0/strings/replace-const.smt2
@@ -1,4 +1,4 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic ALL)
 (set-info :status sat)
 (declare-fun x () String)

diff --git a/test/regress/regress0/strings/replaceall-eval.smt2 b/test/regress/regress0/strings/replaceall-eval.smt2
index c118a7dc4ab8a3470b01a2589fefdbbc7eb37c96..f2edfe3fbeb0da44c100719d0466e0c3ad14a1c3 100644 (file)
--- a/test/regress/regress0/strings/replaceall-eval.smt2
+++ b/test/regress/regress0/strings/replaceall-eval.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=smt2.6.1
+; COMMAND-LINE: --lang=smt2.6
 ; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)

diff --git a/test/regress/regress0/strings/rewrites-re-concat.smt2 b/test/regress/regress0/strings/rewrites-re-concat.smt2
index fe6691e7309a5c201c56af26d497afc43b61f4dc..f2004204a43998d88dccac35fa6bb61a825f135a 100644 (file)
--- a/test/regress/regress0/strings/rewrites-re-concat.smt2
+++ b/test/regress/regress0/strings/rewrites-re-concat.smt2
@@ -1,20 +1,20 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic SLIA)
 (set-info :status unsat)
 
 (declare-fun x () String)
-(assert (str.in.re x (re.++ (str.to.re "baa") (re.* (str.to.re "a")) (re.* (str.to.re "c")))))
+(assert (str.in_re x (re.++ (str.to_re "baa") (re.* (str.to_re "a")) (re.* (str.to_re "c")))))
 
 (declare-fun y () String)
 (assert (< (str.len y) 2))
 
 (assert (or
-(not (str.in.re x (re.++ (str.to.re "baa") (re.* (str.to.re "a")) (re.* (str.to.re "a")) (re.* (str.to.re "c")))))
-(not (str.in.re x (re.++ (str.to.re "ba") (str.to.re "") (re.* (str.to.re "a")) (str.to.re "a") (re.* (str.to.re "c")))))
-(not (str.in.re x (re.++ (str.to.re "b") (re.* (str.to.re "a")) (str.to.re "a") (re.* (str.to.re "a")) (str.to.re "a") (re.* (str.to.re "c")))))
+(not (str.in_re x (re.++ (str.to_re "baa") (re.* (str.to_re "a")) (re.* (str.to_re "a")) (re.* (str.to_re "c")))))
+(not (str.in_re x (re.++ (str.to_re "ba") (str.to_re "") (re.* (str.to_re "a")) (str.to_re "a") (re.* (str.to_re "c")))))
+(not (str.in_re x (re.++ (str.to_re "b") (re.* (str.to_re "a")) (str.to_re "a") (re.* (str.to_re "a")) (str.to_re "a") (re.* (str.to_re "c")))))
 
-(str.in.re y (re.++ re.allchar re.allchar (re.* re.allchar) re.allchar))
-(str.in.re y (re.++ re.allchar re.allchar re.allchar))
+(str.in_re y (re.++ re.allchar re.allchar (re.* re.allchar) re.allchar))
+(str.in_re y (re.++ re.allchar re.allchar re.allchar))
 )
 )
 

diff --git a/test/regress/regress0/strings/rewrites-v2.smt2 b/test/regress/regress0/strings/rewrites-v2.smt2
index 15954525f6a32ab84527bfdcedba670f717d1811..be9f18681d96e2ceadb304bb8fea3eaa45ee74d4 100644 (file)
--- a/test/regress/regress0/strings/rewrites-v2.smt2
+++ b/test/regress/regress0/strings/rewrites-v2.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --strings-exp
 ; EXPECT: unsat
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic SLIA)
 (set-info :status unsat)
 (declare-fun x () String)
@@ -9,8 +9,8 @@
 
 ; these should all rewrite to false
 (assert (or
-(str.contains "abcdef0ghij1abced" (str.++ "g" (int.to.str (str.len z)) x "a" y (int.to.str (+ (str.len z) 1))))
-(str.contains "abc23cd" (str.++ (int.to.str (str.len z)) (int.to.str (str.len z)) (int.to.str (str.len z))))
+(str.contains "abcdef0ghij1abced" (str.++ "g" (str.from_int (str.len z)) x "a" y (str.from_int (+ (str.len z) 1))))
+(str.contains "abc23cd" (str.++ (str.from_int (str.len z)) (str.from_int (str.len z)) (str.from_int (str.len z))))
 (not (str.contains (str.++ x "ab" y) (str.++ "b" (str.substr y 0 4))))
 (not (str.contains (str.++ x "ab" y) (str.++ (str.substr x 5 (str.len x)) "a")))
 (str.contains (str.++ x y) (str.++ x "a" y))

diff --git a/test/regress/regress0/strings/std2.6.1.smt2 b/test/regress/regress0/strings/std2.6.1.smt2
index d30cfc83c9720d917d2ee014f6e49ccb93764029..8881f874db963e00b1b339e69a1880bbae2ee24c 100644 (file)
--- a/test/regress/regress0/strings/std2.6.1.smt2
+++ b/test/regress/regress0/strings/std2.6.1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --strings-exp --lang=smt2.6.1
+; COMMAND-LINE: --strings-exp --lang=smt2.6
 ; EXPECT: sat
 (set-logic QF_UFSLIA)
 (set-info :status sat)

diff --git a/test/regress/regress0/strings/strip-endpoint-itos.smt2 b/test/regress/regress0/strings/strip-endpoint-itos.smt2
index c8d8c5af3b0f592b2e3b7319bfc7ab4316539942..4f098e3192b5ee43eddfe1770073da43dfbfee37 100644 (file)
--- a/test/regress/regress0/strings/strip-endpoint-itos.smt2
+++ b/test/regress/regress0/strings/strip-endpoint-itos.smt2
@@ -1,7 +1,7 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-info :status sat)
 (declare-fun x () Int)
-(assert (str.contains "Ducati100" (int.to.str x)))
+(assert (str.contains "Ducati100" (str.from_int x)))
 (check-sat)

diff --git a/test/regress/regress0/strings/tolower-rrs.smt2 b/test/regress/regress0/strings/tolower-rrs.smt2
index 7b8b393cd878e7644936eb18f38a74fab4da272c..217255807a2b24f2508c0366a4ac1b8d46e686c7 100644 (file)
--- a/test/regress/regress0/strings/tolower-rrs.smt2
+++ b/test/regress/regress0/strings/tolower-rrs.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --strings-exp
 ; EXPECT: unsat
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic ALL)
 (set-info :status unsat)
 (declare-fun x () String)
@@ -9,7 +9,7 @@
 (assert (or 
 (not (= (str.tolower (str.toupper (str.tolower x))) (str.tolower x)))
 (not (= (str.tolower (str.++ x "A")) (str.++ (str.tolower x) "a")))
-(not (= (str.tolower (int.to.str y)) (int.to.str y)))
+(not (= (str.tolower (str.from_int y)) (str.from_int y)))
 ))
 
 (check-sat)

diff --git a/test/regress/regress0/strings/type001.smt2 b/test/regress/regress0/strings/type001.smt2
index 36a6aaec1a1bc21915ac00abcefca5f184e191b1..168d066ea8b1498406a8e91ecbb9c6f11c3a031a 100644 (file)
--- a/test/regress/regress0/strings/type001.smt2
+++ b/test/regress/regress0/strings/type001.smt2
@@ -1,4 +1,4 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_SLIA)
 (set-info :status sat)
 (set-option :strings-exp true)
@@ -10,13 +10,13 @@
 (declare-fun z () String)
 
 ;big num test
-(assert (= x (int.to.str 4785582390527685649)))
+(assert (= x (str.from_int 4785582390527685649)))
 ;should be ""
-(assert (= y (int.to.str (- 9))))
+(assert (= y (str.from_int (- 9))))
 
 ;big num
-(assert (= i (str.to.int "783914785582390527685649")))
+(assert (= i (str.to_int "783914785582390527685649")))
 ;should be -1
-(assert (= j (str.to.int "-783914785582390527685649")))
+(assert (= j (str.to_int "-783914785582390527685649")))
 
 (check-sat)

diff --git a/test/regress/regress0/strings/unicode-esc.smt2 b/test/regress/regress0/strings/unicode-esc.smt2
index 02b313d4ac51265c6ddfa4892452438bd481051f..4039ecd0a0aa249a701e461252d16a66cd54dc05 100644 (file)
--- a/test/regress/regress0/strings/unicode-esc.smt2
+++ b/test/regress/regress0/strings/unicode-esc.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --strings-exp --lang=smt2.6.1
+; COMMAND-LINE: --strings-exp --lang=smt2.6
 ; EXPECT: sat
 (set-logic ALL)
 

diff --git a/test/regress/regress1/fmf/bug723-irrelevant-funs.smt2 b/test/regress/regress1/fmf/bug723-irrelevant-funs.smt2
index b9141f2e27ecc6a35099307119fb13a51d185f93..d700d3b189747107838ba4242ac18a485a4ae996 100644 (file)
--- a/test/regress/regress1/fmf/bug723-irrelevant-funs.smt2
+++ b/test/regress/regress1/fmf/bug723-irrelevant-funs.smt2
@@ -5,7 +5,7 @@
 (define-fun $$isFalse$$ ((b Bool)) Bool (not b))
 (define-fun $$toString$$ ((b Bool)) String (ite b "true" "false"))
 (define-fun $$fromString$$ ((s String)) Bool (= s "true"))
-(define-fun $$inttostr$$ ((i Int)) String (ite (< i 0) (str.++ "-" (int.to.str (- i))) (int.to.str i)))
+(define-fun $$inttostr$$ ((i Int)) String (ite (< i 0) (str.++ "-" (str.from_int (- i))) (str.from_int i)))
 (declare-fun $$takeWhile$$ (String String) String)
 (declare-fun $$takeWhileNot$$ (String String) String)
 (declare-fun $$dropWhile$$ (String String) String)

diff --git a/test/regress/regress1/strings/artemis-0512-nonterm.smt2 b/test/regress/regress1/strings/artemis-0512-nonterm.smt2
index 328317ea491167d90a189e5cd57e24ba1023f5da..1d76f3ca044d6d5799c01d8702d9feb5f6b4dad3 100644 (file)
--- a/test/regress/regress1/strings/artemis-0512-nonterm.smt2
+++ b/test/regress/regress1/strings/artemis-0512-nonterm.smt2
@@ -1,4 +1,4 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-info :status unsat)
@@ -21,7 +21,7 @@
   )
 )
  
-(assert (= (<= (str.to.int Y) 31) false))
+(assert (= (<= (str.to_int Y) 31) false))
  
 (check-sat)
  

diff --git a/test/regress/regress1/strings/bug615.smt2 b/test/regress/regress1/strings/bug615.smt2
index 673b0dbd03eaab2964659f909cef675ed16c9bcc..3098a59baab6c2c70b28351c672468ae3ac913be 100644 (file)
--- a/test/regress/regress1/strings/bug615.smt2
+++ b/test/regress/regress1/strings/bug615.smt2
@@ -1,4 +1,4 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_S)
 (set-option :strings-exp true)
 (set-info :status sat)
@@ -11,16 +11,16 @@
 (assert (str.contains joined "<script>alert(1);</script>"))
 
 ; (<script>[^<]*</script>)+
-(assert (str.in.re joined
+(assert (str.in_re joined
             (re.+ (re.++
-                    (str.to.re "<script>")
+                    (str.to_re "<script>")
                     (re.*
                         (re.union
                             (re.range " " ";")
                             (re.range "=" "~")
                         )
                     )
-                    (str.to.re "</script>")
+                    (str.to_re "</script>")
             ))
   ))
 

diff --git a/test/regress/regress1/strings/bug799-min.smt2 b/test/regress/regress1/strings/bug799-min.smt2
index 0cd15af4ed6ee40a349660a60d26a523f7f4134b..d6054925d569e457ced47b743d6941c675c2973c 100644 (file)
--- a/test/regress/regress1/strings/bug799-min.smt2
+++ b/test/regress/regress1/strings/bug799-min.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --incremental --strings-exp
 ; EXPECT: sat
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic ALL)
 (set-info :status sat)
 
@@ -14,6 +14,6 @@
 (assert (= (str.at u 8) "6"))
 
 (push 1)
-(assert (str.in.re s (re.range "0" "3")))
+(assert (str.in_re s (re.range "0" "3")))
 
 (check-sat)

diff --git a/test/regress/regress1/strings/code-sequence.smt2 b/test/regress/regress1/strings/code-sequence.smt2
index 2654017d48e93d146101cda2396795c5b9e13938..e378f9850adce6280adeed938a361adcf3df08ad 100644 (file)
--- a/test/regress/regress1/strings/code-sequence.smt2
+++ b/test/regress/regress1/strings/code-sequence.smt2
@@ -6,9 +6,9 @@
 (declare-fun x () String)
 (assert (forall ((n Int)) (=> (and (<= 0 n) (< n (str.len x))) 
 (and
-(<= 60 (str.code (str.at x n)))
-(<= (str.code (str.at x n)) 90)
-(< (+ 1 (str.code (str.at x (- n 1)))) (str.code (str.at x n)))
+(<= 60 (str.to_code (str.at x n)))
+(<= (str.to_code (str.at x n)) 90)
+(< (+ 1 (str.to_code (str.at x (- n 1)))) (str.to_code (str.at x n)))
 ))))
 (assert (> (str.len x) 3))
 (check-sat)

diff --git a/test/regress/regress1/strings/complement-test.smt2 b/test/regress/regress1/strings/complement-test.smt2
index 1fcbdc2c3e10072e9d00237a575bbc9b69820fa0..5d3c8310f9d29b68815114a46086f7a2c88c932e 100644 (file)
--- a/test/regress/regress1/strings/complement-test.smt2
+++ b/test/regress/regress1/strings/complement-test.smt2
@@ -5,8 +5,8 @@
 (declare-fun z () String)
 (assert (= x (str.++ "AB" y)))
 (assert (or (= y "C") (= y (str.++ "D" z)) (= (str.len y) 10)))
-(assert (str.in.re x 
+(assert (str.in_re x 
             (re.inter 
-              (re.comp (str.to.re "AB")) 
-              (re.comp (re.++ (str.to.re "AB") (re.range "A" "E") (re.* re.allchar))))))
+              (re.comp (str.to_re "AB")) 
+              (re.comp (re.++ (str.to_re "AB") (re.range "A" "E") (re.* re.allchar))))))
 (check-sat)

diff --git a/test/regress/regress1/strings/fmf001.smt2 b/test/regress/regress1/strings/fmf001.smt2
index 71ae63e87b4eb429aa55b7af8b9f9076f51e5b34..4c6b2091b1abf5bd060668c2f4519668f912e7e7 100644 (file)
--- a/test/regress/regress1/strings/fmf001.smt2
+++ b/test/regress/regress1/strings/fmf001.smt2
@@ -1,4 +1,4 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_S)
 (set-option :strings-exp true)
 (set-option :strings-fmf true)
@@ -7,12 +7,12 @@
 (declare-fun x () String)
 (declare-fun y () String)
 
-(assert (str.in.re x
-               (re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") ))
+(assert (str.in_re x
+               (re.* (re.++ (re.* (str.to_re "a") ) (str.to_re "b") ))
        ))
 
-(assert (str.in.re y
-               (re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") ))
+(assert (str.in_re y
+               (re.* (re.++ (re.* (str.to_re "a") ) (str.to_re "b") ))
        ))
 
 (assert (not (= x y)))

diff --git a/test/regress/regress1/strings/fmf002.smt2 b/test/regress/regress1/strings/fmf002.smt2
index 2f2209ae7ecfb6f0aadb045082920996afa4bbdb..8daaa6ee46e556e4a20918f5e321defaedeff8f1 100644 (file)
--- a/test/regress/regress1/strings/fmf002.smt2
+++ b/test/regress/regress1/strings/fmf002.smt2
@@ -1,4 +1,4 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-option :strings-fmf true)
@@ -8,7 +8,7 @@
 (declare-fun y () String)
 (declare-fun z () String)
 
-(assert (str.in.re x
+(assert (str.in_re x
                 (re.+ (re.range "a" "c"))
                                                ))
 

diff --git a/test/regress/regress1/strings/issue1684-regex.smt2 b/test/regress/regress1/strings/issue1684-regex.smt2
index 35eb8456d2873469da3fd94106b0cd9c4758ddeb..de0739bd80ef025afa284d48b8fc0f1398d6b2d6 100644 (file)
--- a/test/regress/regress1/strings/issue1684-regex.smt2
+++ b/test/regress/regress1/strings/issue1684-regex.smt2
@@ -5,4 +5,4 @@
 (declare-const s String)
 (assert (str.in.re s (re.* (re.range "\x00" "\xFF"))))
 (assert (str.in.re s (re.range "\x00" "\xFF")))
-(check-sat)
\ No newline at end of file
+(check-sat)

diff --git a/test/regress/regress1/strings/issue2060.smt2 b/test/regress/regress1/strings/issue2060.smt2
index 784fe18621ff3a8acf04544d123e6480306ecd0e..ade68a6a12a6cc9fb2ae954e838f25dbcd766ce7 100644 (file)
--- a/test/regress/regress1/strings/issue2060.smt2
+++ b/test/regress/regress1/strings/issue2060.smt2
@@ -4,8 +4,8 @@
 (declare-const action String)
 (declare-const example_key String)
 
-(assert (str.in.re action (re.++
-                           (str.to.re "foobar:ab")
+(assert (str.in_re action (re.++
+                           (str.to_re "foobar:ab")
                            (re.* re.allchar)
                    )))
 

diff --git a/test/regress/regress1/strings/issue2429-code.smt2 b/test/regress/regress1/strings/issue2429-code.smt2
index 9dc29794e8cca174a24965b0cb0d3340d8a40b24..ea564dc4844cc1f2736e90c2f8570703c6c96831 100644 (file)
--- a/test/regress/regress1/strings/issue2429-code.smt2
+++ b/test/regress/regress1/strings/issue2429-code.smt2
@@ -3,7 +3,7 @@
 (set-option :produce-models true)
 (set-info :status sat)
 
-(define-fun byte_2_int ((s String)) Int (ite (= (str.len s) 1) (str.code s) 256))
+(define-fun byte_2_int ((s String)) Int (ite (= (str.len s) 1) (str.to_code s) 256))
 
 (define-fun read_buffer16 ((s1 String) (s2 String)) Int
   (+ (* 256 (byte_2_int s1)) 

diff --git a/test/regress/regress1/strings/issue2981.smt2 b/test/regress/regress1/strings/issue2981.smt2
index 78cdb2a8cf7a088207f372c717cd39bf8ea6805b..615140fc9ce870342ee23fbca59126f55cfd4b76 100644 (file)
--- a/test/regress/regress1/strings/issue2981.smt2
+++ b/test/regress/regress1/strings/issue2981.smt2
@@ -6,8 +6,8 @@
 (declare-const y String)
 (declare-const m String)
 (declare-const n String)
-(assert (str.in.re x (re.+ (re.range "0" "9"))))
-(assert (= 0 (str.to.int x)))                   
+(assert (str.in_re x (re.+ (re.range "0" "9"))))
+(assert (= 0 (str.to_int x)))                   
 (assert (not (= x ""))) 
 (assert (not (= x "0")))
 (assert (not (= x "3")))

diff --git a/test/regress/regress1/strings/issue2982.smt2 b/test/regress/regress1/strings/issue2982.smt2
index 41be8d1fd825626ca315c5e3e2e982d563878d5f..a57915b446cc84079c81fbf5d9eef19b311f0a0d 100644 (file)
--- a/test/regress/regress1/strings/issue2982.smt2
+++ b/test/regress/regress1/strings/issue2982.smt2
@@ -16,8 +16,8 @@
 (declare-fun var_11 () String)
 (declare-fun var_12 () String)
 
-(assert (str.in.re (str.++ var_7 "z" var_7 ) (re.* (str.to.re "z"))))
-(assert (str.in.re var_7 (re.* (re.range "a" "u"))))
-(assert (not (str.in.re (str.++ "a" var_7 "z" "a" var_7 ) (re.++ (re.* (re.union (str.to.re "z") (re.++ (str.to.re "a") (re.++ (re.* (str.to.re "a")) (str.to.re "z"))))) (re.++ (str.to.re "a") (re.* (str.to.re "a")))))))
+(assert (str.in_re (str.++ var_7 "z" var_7 ) (re.* (str.to_re "z"))))
+(assert (str.in_re var_7 (re.* (re.range "a" "u"))))
+(assert (not (str.in_re (str.++ "a" var_7 "z" "a" var_7 ) (re.++ (re.* (re.union (str.to_re "z") (re.++ (str.to_re "a") (re.++ (re.* (str.to_re "a")) (str.to_re "z"))))) (re.++ (str.to_re "a") (re.* (str.to_re "a")))))))
 (assert (and (<= (str.len var_7) 0 ) (<= 0  (str.len var_7))))
 (check-sat)

diff --git a/test/regress/regress1/strings/issue3090.smt2 b/test/regress/regress1/strings/issue3090.smt2
index 734257a25445b4e54de9a7313c5da26304d5cd92..dc04289d608c579461c5f28d07a5423e365e10af 100644 (file)
--- a/test/regress/regress1/strings/issue3090.smt2
+++ b/test/regress/regress1/strings/issue3090.smt2
@@ -2,5 +2,5 @@
 (set-option :strings-exp true)
 (set-info :status unsat)
 (declare-const id String)
-(assert (and (str.in.re id (re.+ (re.range "0" "9"))) (str.contains id "value")))
+(assert (and (str.in_re id (re.+ (re.range "0" "9"))) (str.contains id "value")))
 (check-sat)

diff --git a/test/regress/regress1/strings/issue3272.smt2 b/test/regress/regress1/strings/issue3272.smt2
index 47759ef1eb18c86dd3f2aec54ba6bd775e88557c..cf33afb9256770133be152386785ba582060c318 100644 (file)
--- a/test/regress/regress1/strings/issue3272.smt2
+++ b/test/regress/regress1/strings/issue3272.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic ALL_SUPPORTED)
 (set-option :strings-exp true)
 (set-info :status sat)
@@ -10,7 +11,7 @@
             (and                          
                 (not (= (ite (= (str.at (str.substr c 1 (- (str.len (str.substr c 0 (- (str.len c) 1))) 1)) (- (str.len (str.substr (str.substr c 1 (- (str.len (str.replace a b "")) 1)) 0 (- (str.len (str.substr (str.replace a b "") 1 (- (str.len (str.replace a b "")) 1))) 1))) 1)) "\t") 1 0) 0))   
                    
-                (= (ite (= (str.at (str.substr (str.substr c 1 (- (str.len (str.replace a b "")) 1)) 0 (- (str.len (str.substr (str.replace a b "") 1 (- (str.len (str.replace a b "")) 1))) 1)) 0) "\n") 1 0) 0)
+                (= (ite (= (str.at (str.substr (str.substr c 1 (- (str.len (str.replace a b "")) 1)) 0 (- (str.len (str.substr (str.replace a b "") 1 (- (str.len (str.replace a b "")) 1))) 1)) 0) "B") 1 0) 0)
             )     
                             
             (= (ite (= (str.at (str.substr (str.substr c 1 (- (str.len c) 1)) 0 (- (str.len (str.substr (str.replace a b "") 1 (- (str.len (str.replace a b "")) 1))) 1)) 0) " ") 1 0) 0)                   

diff --git a/test/regress/regress1/strings/issue3357.smt2 b/test/regress/regress1/strings/issue3357.smt2
index d0e436038eca344f6b3a2b8119be03aa6825a669..6951d47e1046268a8a730b5e55accfad5c814707 100644 (file)
--- a/test/regress/regress1/strings/issue3357.smt2
+++ b/test/regress/regress1/strings/issue3357.smt2
@@ -9,10 +9,10 @@
 (declare-const e String)
 (declare-const f String)
 (assert (or  
-            (and (= d (str.++ e g)) (str.in.re e (re.* (str.to.re "HG4"))) (> 0 (str.to.int g)) (= 1 (str.len e)) (= 2 (str.len (str.substr b 0 (str.len d)))))  
+            (and (= d (str.++ e g)) (str.in_re e (re.* (str.to_re "HG4"))) (> 0 (str.to_int g)) (= 1 (str.len e)) (= 2 (str.len (str.substr b 0 (str.len d)))))  
             (and 
-                (str.in.re (str.replace (str.replace a c "") "T" "") (re.* (re.union (str.to.re "a") (str.to.re "")))) 
-                (= 0 (str.to.int (str.replace (str.replace a c "") "T" "")))))
+                (str.in_re (str.replace (str.replace a c "") "T" "") (re.* (re.union (str.to_re "a") (str.to_re "")))) 
+                (= 0 (str.to_int (str.replace (str.replace a c "") "T" "")))))
 )
 (assert (= b (str.++ d f)))
 (check-sat)

diff --git a/test/regress/regress1/strings/kaluza-fl.smt2 b/test/regress/regress1/strings/kaluza-fl.smt2
index d277d85e634df1f9128829c3bd4effb31a1f23cf..27065916ffcb1096993e8f114fb3e035c30634dc 100644 (file)
--- a/test/regress/regress1/strings/kaluza-fl.smt2
+++ b/test/regress/regress1/strings/kaluza-fl.smt2
@@ -1,4 +1,4 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_SLIA)
 (set-info :status sat)
 
@@ -60,16 +60,16 @@
 
 (assert (= T_SELECT_1 (not (= PCTEMP_LHS_1 (- 1)))))
 (assert (ite T_SELECT_1 
-  (and (= PCTEMP_LHS_1 (+ I0_2 0))(= var_0xINPUT_12454 (str.++ T0_2 T1_2))(= I0_2 (str.len T4_2))(= 0 (str.len T0_2))(= T1_2 (str.++ T2_2 T3_2))(= T2_2 (str.++ T4_2 T5_2))(= T5_2 "__utma=169413169.")(not (str.in.re T4_2 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "a") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "."))))) 
-  (and (= PCTEMP_LHS_1 (- 1))(= var_0xINPUT_12454 (str.++ T0_2 T1_2))(= 0 (str.len T0_2))(not (str.in.re T1_2 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "a") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re ".")))))))
+  (and (= PCTEMP_LHS_1 (+ I0_2 0))(= var_0xINPUT_12454 (str.++ T0_2 T1_2))(= I0_2 (str.len T4_2))(= 0 (str.len T0_2))(= T1_2 (str.++ T2_2 T3_2))(= T2_2 (str.++ T4_2 T5_2))(= T5_2 "__utma=169413169.")(not (str.in_re T4_2 (re.++ (str.to_re "_") (str.to_re "_") (str.to_re "u") (str.to_re "t") (str.to_re "m") (str.to_re "a") (str.to_re "=") (str.to_re "1") (str.to_re "6") (str.to_re "9") (str.to_re "4") (str.to_re "1") (str.to_re "3") (str.to_re "1") (str.to_re "6") (str.to_re "9") (str.to_re "."))))) 
+  (and (= PCTEMP_LHS_1 (- 1))(= var_0xINPUT_12454 (str.++ T0_2 T1_2))(= 0 (str.len T0_2))(not (str.in_re T1_2 (re.++ (str.to_re "_") (str.to_re "_") (str.to_re "u") (str.to_re "t") (str.to_re "m") (str.to_re "a") (str.to_re "=") (str.to_re "1") (str.to_re "6") (str.to_re "9") (str.to_re "4") (str.to_re "1") (str.to_re "3") (str.to_re "1") (str.to_re "6") (str.to_re "9") (str.to_re ".")))))))
 (assert (= T_SELECT_2 (not (= PCTEMP_LHS_2 (- 1)))))
 (assert (ite T_SELECT_2 
-  (and (= PCTEMP_LHS_2 (+ I0_4 0))(= var_0xINPUT_12454 (str.++ T0_4 T1_4))(= I0_4 (str.len T4_4))(= 0 (str.len T0_4))(= T1_4 (str.++ T2_4 T3_4))(= T2_4 (str.++ T4_4 T5_4))(= T5_4 "__utmb=169413169")(not (str.in.re T4_4 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9"))))) 
-  (and (= PCTEMP_LHS_2 (- 1))(= var_0xINPUT_12454 (str.++ T0_4 T1_4))(= 0 (str.len T0_4))(not (str.in.re T1_4 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9")))))))
+  (and (= PCTEMP_LHS_2 (+ I0_4 0))(= var_0xINPUT_12454 (str.++ T0_4 T1_4))(= I0_4 (str.len T4_4))(= 0 (str.len T0_4))(= T1_4 (str.++ T2_4 T3_4))(= T2_4 (str.++ T4_4 T5_4))(= T5_4 "__utmb=169413169")(not (str.in_re T4_4 (re.++ (str.to_re "_") (str.to_re "_") (str.to_re "u") (str.to_re "t") (str.to_re "m") (str.to_re "b") (str.to_re "=") (str.to_re "1") (str.to_re "6") (str.to_re "9") (str.to_re "4") (str.to_re "1") (str.to_re "3") (str.to_re "1") (str.to_re "6") (str.to_re "9"))))) 
+  (and (= PCTEMP_LHS_2 (- 1))(= var_0xINPUT_12454 (str.++ T0_4 T1_4))(= 0 (str.len T0_4))(not (str.in_re T1_4 (re.++ (str.to_re "_") (str.to_re "_") (str.to_re "u") (str.to_re "t") (str.to_re "m") (str.to_re "b") (str.to_re "=") (str.to_re "1") (str.to_re "6") (str.to_re "9") (str.to_re "4") (str.to_re "1") (str.to_re "3") (str.to_re "1") (str.to_re "6") (str.to_re "9")))))))
 (assert (= T_SELECT_3 (not (= PCTEMP_LHS_3 (- 1)))))
 (assert (ite T_SELECT_3 
-  (and (= PCTEMP_LHS_3 (+ I0_6 0))(= var_0xINPUT_12454 (str.++ T0_6 T1_6))(= I0_6 (str.len T4_6))(= 0 (str.len T0_6))(= T1_6 (str.++ T2_6 T3_6))(= T2_6 (str.++ T4_6 T5_6))(= T5_6 "__utmc=169413169")(not (str.in.re T4_6 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "c") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9"))))) 
-  (and (= PCTEMP_LHS_3 (- 1))(= var_0xINPUT_12454 (str.++ T0_6 T1_6))(= 0 (str.len T0_6))(not (str.in.re T1_6 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "c") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9")))))))
+  (and (= PCTEMP_LHS_3 (+ I0_6 0))(= var_0xINPUT_12454 (str.++ T0_6 T1_6))(= I0_6 (str.len T4_6))(= 0 (str.len T0_6))(= T1_6 (str.++ T2_6 T3_6))(= T2_6 (str.++ T4_6 T5_6))(= T5_6 "__utmc=169413169")(not (str.in_re T4_6 (re.++ (str.to_re "_") (str.to_re "_") (str.to_re "u") (str.to_re "t") (str.to_re "m") (str.to_re "c") (str.to_re "=") (str.to_re "1") (str.to_re "6") (str.to_re "9") (str.to_re "4") (str.to_re "1") (str.to_re "3") (str.to_re "1") (str.to_re "6") (str.to_re "9"))))) 
+  (and (= PCTEMP_LHS_3 (- 1))(= var_0xINPUT_12454 (str.++ T0_6 T1_6))(= 0 (str.len T0_6))(not (str.in_re T1_6 (re.++ (str.to_re "_") (str.to_re "_") (str.to_re "u") (str.to_re "t") (str.to_re "m") (str.to_re "c") (str.to_re "=") (str.to_re "1") (str.to_re "6") (str.to_re "9") (str.to_re "4") (str.to_re "1") (str.to_re "3") (str.to_re "1") (str.to_re "6") (str.to_re "9")))))))
 (assert (= T_4 (<= 0 PCTEMP_LHS_1)))
 (assert T_4)
 (assert (= T_5 (<= 0 PCTEMP_LHS_2)))
@@ -84,14 +84,14 @@
 (assert T_a)
 (assert (= T_SELECT_4 (not (= PCTEMP_LHS_4 (- 1)))))
 (assert (ite T_SELECT_4 
-  (and (= PCTEMP_LHS_4 (+ I0_15 0))(= var_0xINPUT_12454 (str.++ T0_15 T1_15))(= I0_15 (str.len T4_15))(= 0 (str.len T0_15))(= T1_15 (str.++ T2_15 T3_15))(= T2_15 (str.++ T4_15 T5_15))(= T5_15 "__utmb=169413169")(not (str.in.re T4_15 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9"))))) 
-  (and (= PCTEMP_LHS_4 (- 1))(= var_0xINPUT_12454 (str.++ T0_15 T1_15))(= 0 (str.len T0_15))(not (str.in.re T1_15 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9")))))))
+  (and (= PCTEMP_LHS_4 (+ I0_15 0))(= var_0xINPUT_12454 (str.++ T0_15 T1_15))(= I0_15 (str.len T4_15))(= 0 (str.len T0_15))(= T1_15 (str.++ T2_15 T3_15))(= T2_15 (str.++ T4_15 T5_15))(= T5_15 "__utmb=169413169")(not (str.in_re T4_15 (re.++ (str.to_re "_") (str.to_re "_") (str.to_re "u") (str.to_re "t") (str.to_re "m") (str.to_re "b") (str.to_re "=") (str.to_re "1") (str.to_re "6") (str.to_re "9") (str.to_re "4") (str.to_re "1") (str.to_re "3") (str.to_re "1") (str.to_re "6") (str.to_re "9"))))) 
+  (and (= PCTEMP_LHS_4 (- 1))(= var_0xINPUT_12454 (str.++ T0_15 T1_15))(= 0 (str.len T0_15))(not (str.in_re T1_15 (re.++ (str.to_re "_") (str.to_re "_") (str.to_re "u") (str.to_re "t") (str.to_re "m") (str.to_re "b") (str.to_re "=") (str.to_re "1") (str.to_re "6") (str.to_re "9") (str.to_re "4") (str.to_re "1") (str.to_re "3") (str.to_re "1") (str.to_re "6") (str.to_re "9")))))))
 (assert (= T_c (< (- 1) PCTEMP_LHS_4)))
 (assert T_c)
 (assert (= T_SELECT_5 (not (= PCTEMP_LHS_5 (- 1)))))
 (assert (ite T_SELECT_5 
-  (and (= PCTEMP_LHS_5 (+ I0_18 PCTEMP_LHS_4))(= var_0xINPUT_12454 (str.++ T0_18 T1_18))(= I0_18 (str.len T4_18))(= PCTEMP_LHS_4 (str.len T0_18))(= T1_18 (str.++ T2_18 T3_18))(= T2_18 (str.++ T4_18 T5_18))(= T5_18 ";")(not (str.in.re T4_18 (str.to.re ";")))) 
-  (and (= PCTEMP_LHS_5 (- 1))(= var_0xINPUT_12454 (str.++ T0_18 T1_18))(= PCTEMP_LHS_4 (str.len T0_18))(not (str.in.re T1_18 (str.to.re ";"))))))
+  (and (= PCTEMP_LHS_5 (+ I0_18 PCTEMP_LHS_4))(= var_0xINPUT_12454 (str.++ T0_18 T1_18))(= I0_18 (str.len T4_18))(= PCTEMP_LHS_4 (str.len T0_18))(= T1_18 (str.++ T2_18 T3_18))(= T2_18 (str.++ T4_18 T5_18))(= T5_18 ";")(not (str.in_re T4_18 (str.to_re ";")))) 
+  (and (= PCTEMP_LHS_5 (- 1))(= var_0xINPUT_12454 (str.++ T0_18 T1_18))(= PCTEMP_LHS_4 (str.len T0_18))(not (str.in_re T1_18 (str.to_re ";"))))))
 (assert (= T_e (< PCTEMP_LHS_5 0)))
 (assert T_e)
 

diff --git a/test/regress/regress1/strings/no-lazy-pp-quant.smt2 b/test/regress/regress1/strings/no-lazy-pp-quant.smt2
index 672c4e5fc7a8c5b843ffa2e7973d8636f4282574..60f7e575e53df2472e1ee7685e9757eebc9d5d9b 100644 (file)
--- a/test/regress/regress1/strings/no-lazy-pp-quant.smt2
+++ b/test/regress/regress1/strings/no-lazy-pp-quant.smt2
@@ -1,9 +1,9 @@
 ; COMMAND-LINE: --strings-exp --no-strings-lazy-pp
 ; EXPECT: sat
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic ALL)
 (set-info :status sat)
 (declare-fun result () Int)
 (declare-fun s () String)
-(assert (! (not (= (str.to.int s) result)) :named a0))
+(assert (! (not (= (str.to_int s) result)) :named a0))
 (check-sat)

diff --git a/test/regress/regress1/strings/non_termination_regular_expression4.smt2 b/test/regress/regress1/strings/non_termination_regular_expression4.smt2
index 0b527345d299f9d7e4648948acfaeecb1555e39b..1e3f3cb96da107323811d2fc2bad40ac5127eca0 100644 (file)
--- a/test/regress/regress1/strings/non_termination_regular_expression4.smt2
+++ b/test/regress/regress1/strings/non_termination_regular_expression4.smt2
@@ -1,4 +1,4 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic ALL)
 (set-info :status unsat)
 (set-option :strings-exp true)
@@ -8,7 +8,7 @@
 
 ; Action: p0.0
 (declare-const p0.0.action Bool)
-(assert (= p0.0.action (and (= actionNamespace "foobar") (str.in.re actionName (re.++ (str.to.re "foo") (re.* re.allchar) (re.++ (str.to.re "") re.allchar (str.to.re "bar")))))))
+(assert (= p0.0.action (and (= actionNamespace "foobar") (str.in_re actionName (re.++ (str.to_re "foo") (re.* re.allchar) (re.++ (str.to_re "") re.allchar (str.to_re "bar")))))))
 
 ; Policy: 0
 (declare-const p0.denies Bool)
@@ -20,7 +20,7 @@
 
 ; Action: p1.0
 (declare-const p1.0.action Bool)
-(assert (= p1.0.action (and (= actionNamespace "foobar") (str.in.re actionName (re.++ (re.++ (str.to.re "foo") re.allchar (str.to.re "")) (re.* re.allchar) (str.to.re "bar"))))))
+(assert (= p1.0.action (and (= actionNamespace "foobar") (str.in_re actionName (re.++ (re.++ (str.to_re "foo") re.allchar (str.to_re "")) (re.* re.allchar) (str.to_re "bar"))))))
 
 ; Policy: 1
 (declare-const p1.denies Bool)

diff --git a/test/regress/regress1/strings/norn-13.smt2 b/test/regress/regress1/strings/norn-13.smt2
index 912f4477a21b3cb8089fa1f39e02157b8ea67813..2a8d9f323d9773d9353e7a6ca2ead27578a8cdb3 100644 (file)
--- a/test/regress/regress1/strings/norn-13.smt2
+++ b/test/regress/regress1/strings/norn-13.smt2
@@ -16,8 +16,8 @@
 (declare-fun var_11 () String)
 (declare-fun var_12 () String)
 
-(assert (str.in.re "" (re.* (re.range "a" "u"))))
-(assert (str.in.re var_4 (re.* (re.range "a" "u"))))
-(assert (str.in.re var_4 (re.* (re.union (str.to.re "a") (str.to.re "b")))))
-(assert (not (str.in.re (str.++ var_4 "z" ) (re.* (str.to.re "z")))))
+(assert (str.in_re "" (re.* (re.range "a" "u"))))
+(assert (str.in_re var_4 (re.* (re.range "a" "u"))))
+(assert (str.in_re var_4 (re.* (re.union (str.to_re "a") (str.to_re "b")))))
+(assert (not (str.in_re (str.++ var_4 "z" ) (re.* (str.to_re "z")))))
 (check-sat)

diff --git a/test/regress/regress1/strings/norn-360.smt2 b/test/regress/regress1/strings/norn-360.smt2
index 20ab0b33808544372407a694392950475fd67335..bdbca494d008fd606f20f1068252c8afe5578692 100644 (file)
--- a/test/regress/regress1/strings/norn-360.smt2
+++ b/test/regress/regress1/strings/norn-360.smt2
@@ -1,4 +1,4 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-info :status sat)
@@ -17,10 +17,10 @@
 (declare-fun var_11 () String)
 (declare-fun var_12 () String)
 
-(assert (str.in.re (str.++ var_3 "z" var_4 ) (re.++ (re.* (re.union (re.union (str.to.re "z") (str.to.re "b")) (re.++ (str.to.re "a") (re.union (re.union (str.to.re "z") (str.to.re "b")) (str.to.re "a"))))) (str.to.re "a"))))
-(assert (str.in.re (str.++ var_3 "z" var_4 ) (re.++ (re.* (re.union (re.union (str.to.re "z") (str.to.re "b")) (re.++ (str.to.re "a") (re.union (str.to.re "z") (str.to.re "a"))))) (str.to.re "a"))))
-(assert (str.in.re (str.++ var_3 "z" var_4 ) (re.++ (re.* (re.union (str.to.re "z") (re.++ (re.union (str.to.re "b") (str.to.re "a")) (re.union (str.to.re "z") (str.to.re "b"))))) (re.union (str.to.re "b") (str.to.re "a")))))
-(assert (str.in.re var_4 (re.* (re.range "a" "u"))))
-(assert (str.in.re var_3 (re.* (re.range "a" "u"))))
+(assert (str.in_re (str.++ var_3 "z" var_4 ) (re.++ (re.* (re.union (re.union (str.to_re "z") (str.to_re "b")) (re.++ (str.to_re "a") (re.union (re.union (str.to_re "z") (str.to_re "b")) (str.to_re "a"))))) (str.to_re "a"))))
+(assert (str.in_re (str.++ var_3 "z" var_4 ) (re.++ (re.* (re.union (re.union (str.to_re "z") (str.to_re "b")) (re.++ (str.to_re "a") (re.union (str.to_re "z") (str.to_re "a"))))) (str.to_re "a"))))
+(assert (str.in_re (str.++ var_3 "z" var_4 ) (re.++ (re.* (re.union (str.to_re "z") (re.++ (re.union (str.to_re "b") (str.to_re "a")) (re.union (str.to_re "z") (str.to_re "b"))))) (re.union (str.to_re "b") (str.to_re "a")))))
+(assert (str.in_re var_4 (re.* (re.range "a" "u"))))
+(assert (str.in_re var_3 (re.* (re.range "a" "u"))))
 (assert (<= 0  (str.len var_4)))
 (check-sat)

diff --git a/test/regress/regress1/strings/norn-ab.smt2 b/test/regress/regress1/strings/norn-ab.smt2
index 47c218179ae9972bfe5c12262bade3b6c40a7c56..63a95bb78ea8f4de4207cb6f9589f617c648bf46 100644 (file)
--- a/test/regress/regress1/strings/norn-ab.smt2
+++ b/test/regress/regress1/strings/norn-ab.smt2
@@ -1,4 +1,4 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_SLIA)
 (set-info :status unsat)
 (set-option :strings-exp true)
@@ -17,10 +17,10 @@
 (declare-fun var_11 () String)
 (declare-fun var_12 () String)
 
-(assert (str.in.re var_4 (re.++ (str.to.re "a") (re.* (str.to.re "b")))))
-(assert (str.in.re var_4 (re.++ (re.* (str.to.re "a")) (str.to.re "b"))))
-(assert (str.in.re var_4 (re.* (re.range "a" "u"))))
-(assert (str.in.re var_4 (re.++ (re.* (str.to.re "a")) (re.++ (str.to.re "b") (re.* (str.to.re "b"))))))
-(assert (not (str.in.re (str.++ "a" var_4 "b" ) (re.++ (re.* (str.to.re "a")) (re.++ (str.to.re "b") (re.* (str.to.re "b")))))))
+(assert (str.in_re var_4 (re.++ (str.to_re "a") (re.* (str.to_re "b")))))
+(assert (str.in_re var_4 (re.++ (re.* (str.to_re "a")) (str.to_re "b"))))
+(assert (str.in_re var_4 (re.* (re.range "a" "u"))))
+(assert (str.in_re var_4 (re.++ (re.* (str.to_re "a")) (re.++ (str.to_re "b") (re.* (str.to_re "b"))))))
+(assert (not (str.in_re (str.++ "a" var_4 "b" ) (re.++ (re.* (str.to_re "a")) (re.++ (str.to_re "b") (re.* (str.to_re "b")))))))
 (assert (and (<= 0  (str.len var_4)) (not (not (exists ((v Int)) (= (* v 2 ) (+ (str.len var_4) 2 )))))))
 (check-sat)

diff --git a/test/regress/regress1/strings/norn-nel-bug-052116.smt2 b/test/regress/regress1/strings/norn-nel-bug-052116.smt2
index 9f06152f708c387e3a1298ab872fd8c661888826..883f7c4dddcfe8351fd6fd88a8e84c6b1938aa24 100644 (file)
--- a/test/regress/regress1/strings/norn-nel-bug-052116.smt2
+++ b/test/regress/regress1/strings/norn-nel-bug-052116.smt2
@@ -1,4 +1,4 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)
@@ -17,8 +17,8 @@
 (declare-fun var_11 () String)
 (declare-fun var_12 () String)
 
-(assert (str.in.re var_4 (re.* (re.range "a" "u"))))
-(assert (str.in.re var_4 (re.++ (re.* (re.union (str.to.re "a") (re.++ (str.to.re "b") (str.to.re "a")))) (str.to.re "b"))))
-(assert (str.in.re (str.++ "a" var_4 "b" ) (re.* (re.range "a" "u"))))
-(assert (not (str.in.re (str.++ "a" var_4 "b" ) (re.++ (re.* (str.to.re "a")) (re.++ (str.to.re "b") (re.* (str.to.re "b")))))))
+(assert (str.in_re var_4 (re.* (re.range "a" "u"))))
+(assert (str.in_re var_4 (re.++ (re.* (re.union (str.to_re "a") (re.++ (str.to_re "b") (str.to_re "a")))) (str.to_re "b"))))
+(assert (str.in_re (str.++ "a" var_4 "b" ) (re.* (re.range "a" "u"))))
+(assert (not (str.in_re (str.++ "a" var_4 "b" ) (re.++ (re.* (str.to_re "a")) (re.++ (str.to_re "b") (re.* (str.to_re "b")))))))
 (check-sat)

diff --git a/test/regress/regress1/strings/norn-simp-rew-sat.smt2 b/test/regress/regress1/strings/norn-simp-rew-sat.smt2
index 1336d3bfc2979040c32930beb07faa6b0f3040c3..f7cad1c09e82821b4465c83c1987046261f57ba0 100644 (file)
--- a/test/regress/regress1/strings/norn-simp-rew-sat.smt2
+++ b/test/regress/regress1/strings/norn-simp-rew-sat.smt2
@@ -1,4 +1,4 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-info :status sat)
@@ -17,10 +17,10 @@
 (declare-fun var_11 () String)
 (declare-fun var_12 () String)
 
-(assert (str.in.re (str.++ var_3 "z" var_4 ) (re.++ (re.* (re.union (re.union (str.to.re "z") (str.to.re "a")) (re.++ (str.to.re "b") (re.++ (re.* (str.to.re "b")) (re.union (str.to.re "z") (str.to.re "a")))))) (re.++ (str.to.re "b") (re.* (str.to.re "b"))))))
-(assert (str.in.re var_4 (re.* (re.range "a" "u"))))
-(assert (str.in.re var_4 (re.* (str.to.re "b"))))
-(assert (str.in.re var_3 (re.* (re.range "a" "u"))))
-(assert (str.in.re var_3 (re.* (str.to.re "a"))))
+(assert (str.in_re (str.++ var_3 "z" var_4 ) (re.++ (re.* (re.union (re.union (str.to_re "z") (str.to_re "a")) (re.++ (str.to_re "b") (re.++ (re.* (str.to_re "b")) (re.union (str.to_re "z") (str.to_re "a")))))) (re.++ (str.to_re "b") (re.* (str.to_re "b"))))))
+(assert (str.in_re var_4 (re.* (re.range "a" "u"))))
+(assert (str.in_re var_4 (re.* (str.to_re "b"))))
+(assert (str.in_re var_3 (re.* (re.range "a" "u"))))
+(assert (str.in_re var_3 (re.* (str.to_re "a"))))
 (assert (<= 0  (str.len var_4)))
 (check-sat)

diff --git a/test/regress/regress1/strings/nt6-dd.smt2 b/test/regress/regress1/strings/nt6-dd.smt2
index 30a0884a3f967bc81552fdc291271a1a63b5624c..ad1e4edf5b863f8d55c0e0e1056123ae9e87291b 100644 (file)
--- a/test/regress/regress1/strings/nt6-dd.smt2
+++ b/test/regress/regress1/strings/nt6-dd.smt2
@@ -1,13 +1,13 @@
 ; COMMAND-LINE: --strings-exp --re-elim
 ; EXPECT: sat
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic ALL)
 (set-info :status sat)
 (declare-const resource_resource String)
 (declare-const p1.0.resource Bool)
 
-(assert (str.in.re resource_resource (re.++ (str.to.re "ab") (re.* re.allchar) (str.to.re "b") )))
+(assert (str.in_re resource_resource (re.++ (str.to_re "ab") (re.* re.allchar) (str.to_re "b") )))
 
-(assert (= p1.0.resource (str.in.re resource_resource (re.++ (str.to.re "a") (re.* re.allchar) (str.to.re "b") ))))
+(assert (= p1.0.resource (str.in_re resource_resource (re.++ (str.to_re "a") (re.* re.allchar) (str.to_re "b") ))))
 
 (check-sat)

diff --git a/test/regress/regress1/strings/nterm-re-inter-sigma.smt2 b/test/regress/regress1/strings/nterm-re-inter-sigma.smt2
index 4ac3efff710b7d80b27f947e16cce0350103b8f4..63d6a1391e9269ff7143ce2dffe4e130099b40a5 100644 (file)
--- a/test/regress/regress1/strings/nterm-re-inter-sigma.smt2
+++ b/test/regress/regress1/strings/nterm-re-inter-sigma.smt2
@@ -1,11 +1,11 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic ALL)
 (set-info :status sat)
 (set-option :strings-exp true)
 (declare-fun x () String)
 
 (assert
-(not (= (str.in.re x (re.++ (re.++ re.allchar  re.allchar ) (re.* re.allchar ))) (not (str.in.re x (re.* (str.to.re "A")))))
+(not (= (str.in_re x (re.++ (re.++ re.allchar  re.allchar ) (re.* re.allchar ))) (not (str.in_re x (re.* (str.to_re "A")))))
 ))
 
 (check-sat)

diff --git a/test/regress/regress1/strings/pierre150331.smt2 b/test/regress/regress1/strings/pierre150331.smt2
index e04db8e9a05c921caa8d8325442dbb1ea1dd923e..ae4277874d3ab4e7a368b22b7fd0e5473eaafec9 100644 (file)
--- a/test/regress/regress1/strings/pierre150331.smt2
+++ b/test/regress/regress1/strings/pierre150331.smt2
@@ -1,7 +1,6 @@
 (set-info :smt-lib-version 2.5)\r
 (set-logic SLIA)\r
 (set-info :status sat)\r
-(set-info :smt-lib-version 2.5)\r
 (set-option :strings-exp true)\r
 (define-fun stringEval ((?s String)) Bool (str.in.re ?s \r
 (re.union \r

diff --git a/test/regress/regress1/strings/policy_variable.smt2 b/test/regress/regress1/strings/policy_variable.smt2
index 4d14e95d5f17780fcf7cbf293e797e47c7b53b12..c74765108d7e696c140347a4e381916cea8d6291 100644 (file)
--- a/test/regress/regress1/strings/policy_variable.smt2
+++ b/test/regress/regress1/strings/policy_variable.smt2
@@ -1,4 +1,4 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic ALL)
 (set-info :status unsat)
 (set-option :strings-exp true)

diff --git a/test/regress/regress1/strings/query4674.smt2 b/test/regress/regress1/strings/query4674.smt2
index 7132fa6a84993436feb96302e4d014a51ce6887e..86a08162a9231d920fa6c0c061f51ad2c24e618c 100644 (file)
--- a/test/regress/regress1/strings/query4674.smt2
+++ b/test/regress/regress1/strings/query4674.smt2
@@ -4,5 +4,5 @@
 (set-option :strings-exp true)
 (set-option :re-elim false)
 (declare-fun x () String)
-(assert (let ((_let_0 (re.* re.allchar ))) (and (not (= (str.in.re x (re.++ _let_0 re.allchar  _let_0 (str.to.re (str.++ "A" (str.++ "B" (str.++ "C" "A")))) _let_0 re.allchar  _let_0)) (str.in.re x (re.++ _let_0 re.allchar  _let_0 re.allchar  _let_0 (str.to.re (str.++ "B" (str.++ "C" (str.++ "B" "B")))) _let_0)))) (not (= (str.in.re x (re.++ _let_0 re.allchar  _let_0 (str.to.re (str.++ "C" (str.++ "B" "C"))) _let_0 (str.to.re "B") _let_0)) (str.in.re x (re.++ _let_0 re.allchar  _let_0 (str.to.re "C") _let_0 (str.to.re (str.++ "B" (str.++ "C" "B"))) _let_0)))))))
+(assert (let ((_let_0 (re.* re.allchar ))) (and (not (= (str.in_re x (re.++ _let_0 re.allchar  _let_0 (str.to_re (str.++ "A" (str.++ "B" (str.++ "C" "A")))) _let_0 re.allchar  _let_0)) (str.in_re x (re.++ _let_0 re.allchar  _let_0 re.allchar  _let_0 (str.to_re (str.++ "B" (str.++ "C" (str.++ "B" "B")))) _let_0)))) (not (= (str.in_re x (re.++ _let_0 re.allchar  _let_0 (str.to_re (str.++ "C" (str.++ "B" "C"))) _let_0 (str.to_re "B") _let_0)) (str.in_re x (re.++ _let_0 re.allchar  _let_0 (str.to_re "C") _let_0 (str.to_re (str.++ "B" (str.++ "C" "B"))) _let_0)))))))
 (check-sat)

diff --git a/test/regress/regress1/strings/query8485.smt2 b/test/regress/regress1/strings/query8485.smt2
index ccd3b7f9afd494e4d45adc8f3683b44a73552c8a..ca222119fb33afe18ea15a5631f129d77468333f 100644 (file)
--- a/test/regress/regress1/strings/query8485.smt2
+++ b/test/regress/regress1/strings/query8485.smt2
@@ -4,5 +4,5 @@
 (set-option :strings-exp true)
 (set-option :re-elim false)
 (declare-fun x () String)
-(assert (let ((_let_0 (re.* re.allchar ))) (and (not (= (str.in.re x (re.++ _let_0 re.allchar  _let_0 (str.to.re (str.++ "B" (str.++ "A" (str.++ "C" "B")))) _let_0 re.allchar  _let_0)) (str.in.re x (re.++ _let_0 re.allchar  _let_0 (str.to.re (str.++ "A" (str.++ "B" (str.++ "C" "C")))) _let_0 re.allchar  _let_0)))) (not (= (str.in.re x (re.++ _let_0 re.allchar  _let_0 (str.to.re (str.++ "C" (str.++ "B" (str.++ "A" "B")))) _let_0 re.allchar  _let_0)) (str.in.re x (re.++ _let_0 re.allchar  _let_0 (str.to.re (str.++ "C" (str.++ "B" "A"))) _let_0 (str.to.re "B") _let_0)))))))
+(assert (let ((_let_0 (re.* re.allchar ))) (and (not (= (str.in_re x (re.++ _let_0 re.allchar  _let_0 (str.to_re (str.++ "B" (str.++ "A" (str.++ "C" "B")))) _let_0 re.allchar  _let_0)) (str.in_re x (re.++ _let_0 re.allchar  _let_0 (str.to_re (str.++ "A" (str.++ "B" (str.++ "C" "C")))) _let_0 re.allchar  _let_0)))) (not (= (str.in_re x (re.++ _let_0 re.allchar  _let_0 (str.to_re (str.++ "C" (str.++ "B" (str.++ "A" "B")))) _let_0 re.allchar  _let_0)) (str.in_re x (re.++ _let_0 re.allchar  _let_0 (str.to_re (str.++ "C" (str.++ "B" "A"))) _let_0 (str.to_re "B") _let_0)))))))
 (check-sat)

diff --git a/test/regress/regress1/strings/re-agg-total1.smt2 b/test/regress/regress1/strings/re-agg-total1.smt2
index 2950066a08643364a2b97c23e9b341fbc8271837..fba863a6c8069e0f49d229217d4f57dac1c4b32e 100644 (file)
--- a/test/regress/regress1/strings/re-agg-total1.smt2
+++ b/test/regress/regress1/strings/re-agg-total1.smt2
@@ -7,9 +7,9 @@
 (declare-const y String)
 
 
-(assert (str.in.re x (re.* (str.to.re "ab") ) ) )
-(assert (str.in.re x (re.* (str.to.re "abab") ) ) )
-(assert (str.in.re x (re.* (str.to.re "ababac") ) ) )
+(assert (str.in_re x (re.* (str.to_re "ab") ) ) )
+(assert (str.in_re x (re.* (str.to_re "abab") ) ) )
+(assert (str.in_re x (re.* (str.to_re "ababac") ) ) )
 
 (assert (> (str.len x)  1) )
 

diff --git a/test/regress/regress1/strings/re-agg-total2.smt2 b/test/regress/regress1/strings/re-agg-total2.smt2
index 54bf493a3f53a27c765c710a1ef4e06d9a2a5219..80e4222249a7bd49c34e7521d03d7b40b408070e 100644 (file)
--- a/test/regress/regress1/strings/re-agg-total2.smt2
+++ b/test/regress/regress1/strings/re-agg-total2.smt2
@@ -5,8 +5,8 @@
 (set-option :re-elim-agg true)
 (declare-const x String)
 (declare-const y String)
-(assert (str.in.re x (re.* (str.to.re "'\r''k'\n'"))))
-(assert (str.in.re x (re.* (str.to.re "'\r''k'\n''\r''k'\n'"))))
+(assert (str.in_re x (re.* (str.to_re "'\r''k'\n'"))))
+(assert (str.in_re x (re.* (str.to_re "'\r''k'\n''\r''k'\n'"))))
 (assert (> (str.len x) 20))
 (assert (< (str.len x) 25))
 (check-sat)

diff --git a/test/regress/regress1/strings/re-all-char-hard.smt2 b/test/regress/regress1/strings/re-all-char-hard.smt2
index 2a643ac889696b13623d1050b95df1da84cc5419..fc156c11641e55991ac57d8be6c7a6ad64be2cc7 100644 (file)
--- a/test/regress/regress1/strings/re-all-char-hard.smt2
+++ b/test/regress/regress1/strings/re-all-char-hard.smt2
@@ -6,6 +6,6 @@
 (declare-fun x () String)
 
 ; we should not intersect these two regular expressions
-(assert (str.in.re x (re.++ (str.to.re "abc:def:ghi:") (re.* re.allchar ) (str.to.re ":") (re.* re.allchar ) (str.to.re ":cluster/sflower-bottle-guide-") (re.* re.allchar ))))
-(assert (str.in.re x (re.++ (re.* re.allchar ) (str.to.re ":") (re.* re.allchar ) (str.to.re ":") (re.* re.allchar ) (str.to.re ":") (re.* re.allchar ) (str.to.re ":") (re.* re.allchar ) (str.to.re ":") (re.* re.allchar ))))
+(assert (str.in_re x (re.++ (str.to_re "abc:def:ghi:") (re.* re.allchar ) (str.to_re ":") (re.* re.allchar ) (str.to_re ":cluster/sflower-bottle-guide-") (re.* re.allchar ))))
+(assert (str.in_re x (re.++ (re.* re.allchar ) (str.to_re ":") (re.* re.allchar ) (str.to_re ":") (re.* re.allchar ) (str.to_re ":") (re.* re.allchar ) (str.to_re ":") (re.* re.allchar ) (str.to_re ":") (re.* re.allchar ))))
 (check-sat)

diff --git a/test/regress/regress1/strings/re-elim-exact.smt2 b/test/regress/regress1/strings/re-elim-exact.smt2
index 62b934610e287ee624100b918ae9cccf685b6f04..9504aad93e2d60962cbf2584c7a61eb09d941040 100644 (file)
--- a/test/regress/regress1/strings/re-elim-exact.smt2
+++ b/test/regress/regress1/strings/re-elim-exact.smt2
@@ -1,10 +1,10 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic ALL)
 (set-info :status sat)
 (set-option :strings-exp true)
 (set-option :re-elim true)
 (declare-fun x () String)
 
-(assert (str.in.re x (re.++ re.allchar (str.to.re "A") re.allchar (str.to.re "B") re.allchar)))
+(assert (str.in_re x (re.++ re.allchar (str.to_re "A") re.allchar (str.to_re "B") re.allchar)))
 
 (check-sat)

diff --git a/test/regress/regress1/strings/re-mod-eq.smt2 b/test/regress/regress1/strings/re-mod-eq.smt2
index 531556e6df8846918e9244c01db10f7d66eaa7f6..ff20ec9d47bb59f5e863c83c88c98c57bf76709e 100644 (file)
--- a/test/regress/regress1/strings/re-mod-eq.smt2
+++ b/test/regress/regress1/strings/re-mod-eq.smt2
@@ -1,4 +1,4 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-info :status unsat)
@@ -6,8 +6,8 @@
 (declare-fun y () String)
 (declare-fun z () String)
 (assert (or (= x y)(= x z)))
-(assert (str.in.re x (re.++ (str.to.re "A") (re.* (str.to.re "BAA")))))
-(assert (str.in.re y (re.++ (str.to.re "AB") (re.* (str.to.re "AAB")) (str.to.re "A"))))
-(assert (str.in.re z (re.++ (str.to.re "AB") (re.* (str.to.re "AAB")) (str.to.re "A"))))
+(assert (str.in_re x (re.++ (str.to_re "A") (re.* (str.to_re "BAA")))))
+(assert (str.in_re y (re.++ (str.to_re "AB") (re.* (str.to_re "AAB")) (str.to_re "A"))))
+(assert (str.in_re z (re.++ (str.to_re "AB") (re.* (str.to_re "AAB")) (str.to_re "A"))))
 ; requires RE solver to reason modulo string equalties
 (check-sat)

diff --git a/test/regress/regress1/strings/re-neg-concat-reduct.smt2 b/test/regress/regress1/strings/re-neg-concat-reduct.smt2
index cbe8c4a8bf7a310bb133ca79f9935716aa096994..0f20f80a37dd6c5b012b39120bc839eb78a7c090 100644 (file)
--- a/test/regress/regress1/strings/re-neg-concat-reduct.smt2
+++ b/test/regress/regress1/strings/re-neg-concat-reduct.smt2
@@ -1,4 +1,4 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)
@@ -6,7 +6,7 @@
 (declare-fun x () String)
 
 (assert (not (= x "")))
-(assert (not (str.in.re x (re.++ (str.to.re "AB") (re.* (str.to.re "A"))))))
-(assert (not (str.in.re x (re.++ (re.* (str.to.re "A")) (str.to.re "B")))))
+(assert (not (str.in_re x (re.++ (str.to_re "AB") (re.* (str.to_re "A"))))))
+(assert (not (str.in_re x (re.++ (re.* (str.to_re "A")) (str.to_re "B")))))
 
 (check-sat)

diff --git a/test/regress/regress1/strings/re-neg-unfold-rev-a.smt2 b/test/regress/regress1/strings/re-neg-unfold-rev-a.smt2
index 3f99f85076cd067d6ce9adf58b49b252053a5840..0f869f155609c6fd4dee30efa1100f6ca5f0ab39 100644 (file)
--- a/test/regress/regress1/strings/re-neg-unfold-rev-a.smt2
+++ b/test/regress/regress1/strings/re-neg-unfold-rev-a.smt2
@@ -1,10 +1,10 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_S)
 (set-info :status unsat)
 (set-option :strings-exp true)
 
 (declare-const x String)
 (declare-const y String)
-(assert (and (= y "foobar") (str.in.re x (re.++ (str.to.re "ab") (re.* re.allchar) (str.to.re "b") (re.* re.allchar) (str.to.re "b") (re.* re.allchar) (str.to.re "b")))))
-(assert (not (and (= y "foobar") (str.in.re x (re.++ (str.to.re "a") (re.* re.allchar) (str.to.re "b") (re.* re.allchar) (str.to.re "b") (re.* re.allchar) (str.to.re "b"))))))
+(assert (and (= y "foobar") (str.in_re x (re.++ (str.to_re "ab") (re.* re.allchar) (str.to_re "b") (re.* re.allchar) (str.to_re "b") (re.* re.allchar) (str.to_re "b")))))
+(assert (not (and (= y "foobar") (str.in_re x (re.++ (str.to_re "a") (re.* re.allchar) (str.to_re "b") (re.* re.allchar) (str.to_re "b") (re.* re.allchar) (str.to_re "b"))))))
 (check-sat)

diff --git a/test/regress/regress1/strings/re-unsound-080718.smt2 b/test/regress/regress1/strings/re-unsound-080718.smt2
index 96353e746a8dcb7874d4634088c52842da5bb869..552a0a7067e1da4ae75b8ccae067e5e30e88a685 100644 (file)
--- a/test/regress/regress1/strings/re-unsound-080718.smt2
+++ b/test/regress/regress1/strings/re-unsound-080718.smt2
@@ -1,18 +1,18 @@
 ; COMMAND-LINE: --strings-print-ascii --strings-exp
 ; EXPECT: sat
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic ALL)
 (set-info :status sat)
 (declare-fun x () String)
 (assert
 (and 
 (not (= 
-  (str.in.re x (re.++ (str.to.re "B") (re.* (str.to.re "B")))) 
-  (str.in.re x (re.++ (str.to.re "B") (str.to.re (str.++ "B" "B"))))
+  (str.in_re x (re.++ (str.to_re "B") (re.* (str.to_re "B")))) 
+  (str.in_re x (re.++ (str.to_re "B") (str.to_re (str.++ "B" "B"))))
 )) 
 (not (= 
-  (str.in.re x (re.++ (re.union (re.++ (str.to.re "A") re.allchar ) re.allchar ) (str.to.re "B"))) 
-  (str.in.re x (re.++ (str.to.re "A") (str.to.re "B")))
+  (str.in_re x (re.++ (re.union (re.++ (str.to_re "A") re.allchar ) re.allchar ) (str.to_re "B"))) 
+  (str.in_re x (re.++ (str.to_re "A") (str.to_re "B")))
 ))
 )
 )

diff --git a/test/regress/regress1/strings/regexp-strat-fix.smt2 b/test/regress/regress1/strings/regexp-strat-fix.smt2
index 9ff78c935fe8e8bcabcb228bdc1ea75e130d6b70..34977466321b85fd7b535024b4befebb2876cb9c 100644 (file)
--- a/test/regress/regress1/strings/regexp-strat-fix.smt2
+++ b/test/regress/regress1/strings/regexp-strat-fix.smt2
@@ -1,8 +1,8 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_S)
 (set-info :status unsat)
 (set-option :strings-exp true)
 (declare-fun var0 () String)
-(assert (str.in.re var0 (re.* (re.* (str.to.re "0")))))
-(assert (not (str.in.re var0 (re.union (re.+ (str.to.re "0")) (re.* (str.to.re "1"))))))
+(assert (str.in_re var0 (re.* (re.* (str.to_re "0")))))
+(assert (not (str.in_re var0 (re.union (re.+ (str.to_re "0")) (re.* (str.to_re "1"))))))
 (check-sat)

diff --git a/test/regress/regress1/strings/regexp001.smt2 b/test/regress/regress1/strings/regexp001.smt2
index 142ff679d92a0d233d7234ed9819af16e6d51668..0562e66557769a37990bd8cc4e48df17b16e9c25 100644 (file)
--- a/test/regress/regress1/strings/regexp001.smt2
+++ b/test/regress/regress1/strings/regexp001.smt2
@@ -1,12 +1,12 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)
 
 (declare-fun x () String)
 
-(assert (str.in.re x
-               (re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") ))
+(assert (str.in_re x
+               (re.* (re.++ (re.* (str.to_re "a") ) (str.to_re "b") ))
        ))
 
 (assert (= (str.len x) 3))

diff --git a/test/regress/regress1/strings/regexp002.smt2 b/test/regress/regress1/strings/regexp002.smt2
index f109a484e925a68ffac3108913133e9fe844a5ca..35501ac1036b1d88b6f3c3cea5c298259f33f126 100644 (file)
--- a/test/regress/regress1/strings/regexp002.smt2
+++ b/test/regress/regress1/strings/regexp002.smt2
@@ -1,4 +1,4 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)
@@ -10,12 +10,12 @@
 (declare-fun x () String)
 (declare-fun y () String)
 
-(assert (str.in.re x
-               (re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") ))
+(assert (str.in_re x
+               (re.* (re.++ (re.* (str.to_re "a") ) (str.to_re "b") ))
        ))
 
-(assert (str.in.re y
-               (re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") ))
+(assert (str.in_re y
+               (re.* (re.++ (re.* (str.to_re "a") ) (str.to_re "b") ))
        ))
 
 (assert (not (= x y)))

diff --git a/test/regress/regress1/strings/regexp003.smt2 b/test/regress/regress1/strings/regexp003.smt2
index 7c05b422f82086cee41da4c2748ce857658f28e7..fa3828745225f532b25b236d63254a5f7c2a463c 100644 (file)
--- a/test/regress/regress1/strings/regexp003.smt2
+++ b/test/regress/regress1/strings/regexp003.smt2
@@ -1,14 +1,14 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)
 
 (declare-const s String)
 
-(assert (str.in.re s (re.inter
-       (re.++ (str.to.re "a") (re.* (str.to.re "b")) 
-               (re.inter (str.to.re "c") (re.* (str.to.re "c"))))
-       (re.++ (str.to.re "a") (re.* (str.to.re "b")) (re.* (str.to.re "c")))
+(assert (str.in_re s (re.inter
+       (re.++ (str.to_re "a") (re.* (str.to_re "b")) 
+               (re.inter (str.to_re "c") (re.* (str.to_re "c"))))
+       (re.++ (str.to_re "a") (re.* (str.to_re "b")) (re.* (str.to_re "c")))
        )))
 
 (check-sat)

diff --git a/test/regress/regress1/strings/reloop.smt2 b/test/regress/regress1/strings/reloop.smt2
index 6230d1656c615f638dce4dcf56370abfe7d8b894..1e90501782d9d6004a42afbade2979ce1b154a13 100644 (file)
--- a/test/regress/regress1/strings/reloop.smt2
+++ b/test/regress/regress1/strings/reloop.smt2
@@ -1,4 +1,4 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-info :status sat)
@@ -8,11 +8,11 @@
 (declare-fun z () String)
 (declare-fun w () String)
 
-(assert (str.in.re x ((_ re.^ 5) (str.to.re "a"))))
-(assert (str.in.re y ((_ re.loop 2 5) (str.to.re "b"))))
-(assert (str.in.re z ((_ re.loop 5 15) (str.to.re "c"))))
+(assert (str.in_re x ((_ re.^ 5) (str.to_re "a"))))
+(assert (str.in_re y ((_ re.loop 2 5) (str.to_re "b"))))
+(assert (str.in_re z ((_ re.loop 5 15) (str.to_re "c"))))
 (assert (> (str.len z) 7))
-(assert (str.in.re w ((_ re.loop  2 7) (str.to.re "b"))))
+(assert (str.in_re w ((_ re.loop  2 7) (str.to_re "b"))))
 (assert (> (str.len w) 2))
 (assert (< (str.len w) 5))
 

diff --git a/test/regress/regress1/strings/replaceall-len.smt2 b/test/regress/regress1/strings/replaceall-len.smt2
index 448d8e98ff309db6b79c43de3546dde02294b117..3c0d7e8e5fd8beca0f2ad6e8d51f2eb12c20df78 100644 (file)
--- a/test/regress/regress1/strings/replaceall-len.smt2
+++ b/test/regress/regress1/strings/replaceall-len.smt2
@@ -1,10 +1,10 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic ALL)
 (set-info :status sat)
 (set-option :strings-exp true)
 (set-option :strings-fmf true)
 (set-option :produce-models true)
 (declare-fun x () String)
-(assert (= (str.len (str.replaceall x "B" "CC")) (+ (str.len x) 2)))
+(assert (= (str.len (str.replace_all x "B" "CC")) (+ (str.len x) 2)))
 (assert (> (str.len x) 2))
 (check-sat)

diff --git a/test/regress/regress1/strings/replaceall-replace.smt2 b/test/regress/regress1/strings/replaceall-replace.smt2
index 5bf5b5b167c3ed2f8f68096fb95925bfa79c4b9e..5f62ff4d5546ebd2448fbfa06aed71b15c4aeb3f 100644 (file)
--- a/test/regress/regress1/strings/replaceall-replace.smt2
+++ b/test/regress/regress1/strings/replaceall-replace.smt2
@@ -1,4 +1,4 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic ALL)
 (set-info :status sat)
 (set-option :strings-exp true)
@@ -9,5 +9,5 @@
 (declare-fun z () String)
 (assert (not (= x "")))
 (assert (not (= y "")))
-(assert (not (= (str.replace x y z) (str.replaceall x y z))))
+(assert (not (= (str.replace x y z) (str.replace_all x y z))))
 (check-sat)

diff --git a/test/regress/regress1/strings/rew-check1.smt2 b/test/regress/regress1/strings/rew-check1.smt2
index 5cb85e4ca197542767af3814cc0a996078717525..2de2c574709f782f2c0d0f85f2241f0ec94f2cc4 100644 (file)
--- a/test/regress/regress1/strings/rew-check1.smt2
+++ b/test/regress/regress1/strings/rew-check1.smt2
@@ -1,10 +1,10 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic ALL)
 (set-info :status unsat)
 (declare-fun x () String)
 (assert (not (=
-(str.in.re x (re.++ (re.* re.allchar ) (str.to.re "A")  (re.* re.allchar ) re.allchar  (re.* re.allchar ) (re.* (str.to.re "A")) (re.* re.allchar ))) 
-(str.in.re x (re.++ (re.* (str.to.re "A")) (re.* (str.to.re "B")) (re.* re.allchar ) (str.to.re "A")  (re.* re.allchar ) re.allchar  (re.* re.allchar )))
+(str.in_re x (re.++ (re.* re.allchar ) (str.to_re "A")  (re.* re.allchar ) re.allchar  (re.* re.allchar ) (re.* (str.to_re "A")) (re.* re.allchar ))) 
+(str.in_re x (re.++ (re.* (str.to_re "A")) (re.* (str.to_re "B")) (re.* re.allchar ) (str.to_re "A")  (re.* re.allchar ) re.allchar  (re.* re.allchar )))
 )))
 
 (check-sat)

diff --git a/test/regress/regress1/strings/simple-re-consume.smt2 b/test/regress/regress1/strings/simple-re-consume.smt2
index af34ef1c9e9f13a517f860e03f983d62fc6de827..d8facc6c80c7f669ede70d77bd473593f2141493 100644 (file)
--- a/test/regress/regress1/strings/simple-re-consume.smt2
+++ b/test/regress/regress1/strings/simple-re-consume.smt2
@@ -1,6 +1,6 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_SLIA)
 (set-info :status sat)
 (declare-fun x () String)
-(assert (str.in.re (str.++ "bbbbbbbb" x) (re.* (re.++ (str.to.re "bbbb") (re.* (str.to.re "aaaa"))))))
+(assert (str.in_re (str.++ "bbbbbbbb" x) (re.* (re.++ (str.to_re "bbbb") (re.* (str.to_re "aaaa"))))))
 (check-sat)

diff --git a/test/regress/regress1/strings/stoi-400million.smt2 b/test/regress/regress1/strings/stoi-400million.smt2
index 9b9acf673a3047ac4c9b7854500e21345bd17447..6bb992a5e85c9a8364c1f7fb3dbb53df38c2aeb9 100644 (file)
--- a/test/regress/regress1/strings/stoi-400million.smt2
+++ b/test/regress/regress1/strings/stoi-400million.smt2
@@ -1,7 +1,7 @@
 ; COMMAND-LINE: --strings-exp
 ; EXPECT: sat
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic ALL)
 (declare-fun s () String)
-(assert (> (str.to.int s) 400000000))
+(assert (> (str.to_int s) 400000000))
 (check-sat)

diff --git a/test/regress/regress1/strings/stoi-solve.smt2 b/test/regress/regress1/strings/stoi-solve.smt2
index 4fbbdcfc10bc72544ce92cf511707d090db6d05b..e84f5b42c48fe0ee47c1c7aa5940f5f3f8e550e7 100644 (file)
--- a/test/regress/regress1/strings/stoi-solve.smt2
+++ b/test/regress/regress1/strings/stoi-solve.smt2
@@ -2,5 +2,5 @@
 (set-info :status sat)
 (set-option :strings-exp true)
 (declare-fun x () String)
-(assert (= (str.to.int x) 12345)) 
+(assert (= (str.to_int x) 12345)) 
 (check-sat)

diff --git a/test/regress/regress1/strings/str-code-sat.smt2 b/test/regress/regress1/strings/str-code-sat.smt2
index 1acc091c1d510ceef9346af0f3fc9fc16e27939c..7345e25bbe10418f1b052bf2f08f5b46d70841b8 100644 (file)
--- a/test/regress/regress1/strings/str-code-sat.smt2
+++ b/test/regress/regress1/strings/str-code-sat.smt2
@@ -5,19 +5,19 @@
 (declare-fun z () String)
 (declare-fun w () String)
 
-(assert (>= (str.code x) 65))
-(assert (<= (str.code x) 75))
+(assert (>= (str.to_code x) 65))
+(assert (<= (str.to_code x) 75))
 
-(assert (>= (str.code y) 65))
-(assert (<= (str.code y) 75))
+(assert (>= (str.to_code y) 65))
+(assert (<= (str.to_code y) 75))
 
-(assert (>= (str.code z) 65))
-(assert (<= (str.code z) 75))
+(assert (>= (str.to_code z) 65))
+(assert (<= (str.to_code z) 75))
 
 (assert (= (str.len w) 1))
 
-(assert (= (+ (str.code x) (str.code y)) 140))
-(assert (= (+ (str.code x) (str.code z)) 141))
+(assert (= (+ (str.to_code x) (str.to_code y)) 140))
+(assert (= (+ (str.to_code x) (str.to_code z)) 141))
 
 (assert (distinct x y z w "A" "B" "C" "D" "AA"))
 

diff --git a/test/regress/regress1/strings/str-code-unsat-2.smt2 b/test/regress/regress1/strings/str-code-unsat-2.smt2
index 38116061ef8f1e20a128805f7811f2c81ab56966..721cbc533054d96e629a558d89ea6e395341f053 100644 (file)
--- a/test/regress/regress1/strings/str-code-unsat-2.smt2
+++ b/test/regress/regress1/strings/str-code-unsat-2.smt2
@@ -2,5 +2,5 @@
 (set-info :status unsat)
 (declare-fun x () String)
 (assert (= (str.len x) 1))
-(assert (or (< (str.code x) 0) (> (str.code x) 10000000000000000000000000000)))
+(assert (or (< (str.to_code x) 0) (> (str.to_code x) 10000000000000000000000000000)))
 (check-sat)

diff --git a/test/regress/regress1/strings/str-code-unsat-3.smt2 b/test/regress/regress1/strings/str-code-unsat-3.smt2
index fa34785c2f14572b66525b540e430e04ae512487..06d297fe8bc4897b25bfe9746c1275a2aee39ef8 100644 (file)
--- a/test/regress/regress1/strings/str-code-unsat-3.smt2
+++ b/test/regress/regress1/strings/str-code-unsat-3.smt2
@@ -4,17 +4,17 @@
 (declare-fun y () String)
 (declare-fun z () String)
 
-(assert (>= (str.code x) 65))
-(assert (<= (str.code x) 75))
+(assert (>= (str.to_code x) 65))
+(assert (<= (str.to_code x) 75))
 
-(assert (>= (str.code y) 65))
-(assert (<= (str.code y) 75))
+(assert (>= (str.to_code y) 65))
+(assert (<= (str.to_code y) 75))
 
-(assert (>= (str.code z) 65))
-(assert (<= (str.code z) 75))
+(assert (>= (str.to_code z) 65))
+(assert (<= (str.to_code z) 75))
 
-(assert (= (+ (str.code x) (str.code y)) 140))
-(assert (= (+ (str.code x) (str.code z)) 141))
+(assert (= (+ (str.to_code x) (str.to_code y)) 140))
+(assert (= (+ (str.to_code x) (str.to_code z)) 141))
 
 (assert (distinct x y z "B" "C" "D" "E"))
 

diff --git a/test/regress/regress1/strings/str-code-unsat.smt2 b/test/regress/regress1/strings/str-code-unsat.smt2
index 6a3e9062bf362beedeb67ac1bb6e430d51931588..118ab775002479670484a2cc6b6aa791449421ae 100644 (file)
--- a/test/regress/regress1/strings/str-code-unsat.smt2
+++ b/test/regress/regress1/strings/str-code-unsat.smt2
@@ -4,17 +4,17 @@
 (declare-fun y () String)
 (declare-fun z () String)
 
-(assert (>= (str.code x) 65))
-(assert (<= (str.code x) 75))
+(assert (>= (str.to_code x) 65))
+(assert (<= (str.to_code x) 75))
 
-(assert (>= (str.code y) 65))
-(assert (<= (str.code y) 75))
+(assert (>= (str.to_code y) 65))
+(assert (<= (str.to_code y) 75))
 
-(assert (>= (str.code z) 65))
-(assert (<= (str.code z) 75))
+(assert (>= (str.to_code z) 65))
+(assert (<= (str.to_code z) 75))
 
-(assert (= (+ (str.code x) (str.code y)) 140))
-(assert (= (+ (str.code x) (str.code z)) 140))
+(assert (= (+ (str.to_code x) (str.to_code y)) 140))
+(assert (= (+ (str.to_code x) (str.to_code z)) 140))
 
 (assert (distinct x y z))
 

diff --git a/test/regress/regress1/strings/string-unsound-sem.smt2 b/test/regress/regress1/strings/string-unsound-sem.smt2
index 44591b47ba6a760bfd4ebae1b064aba0bdb16924..59c2d4a176c236fee29a539e4bedbfced2742553 100644 (file)
--- a/test/regress/regress1/strings/string-unsound-sem.smt2
+++ b/test/regress/regress1/strings/string-unsound-sem.smt2
@@ -1,4 +1,4 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic ALL)
 (set-option :strings-exp true)
 (set-info :status sat)
@@ -6,7 +6,7 @@
 (declare-fun y () String)
 (declare-fun z () Int)
 (assert (and
-(not (= (str.replace "A" (int.to.str z) x) (str.++ "A" (str.replace "" (int.to.str z) x))))
+(not (= (str.replace "A" (str.from_int z) x) (str.++ "A" (str.replace "" (str.from_int z) x))))
 (not (= (str.replace x (str.at x z) "") (str.++ (str.replace (str.++ (str.substr x 0 z) (str.substr x z 1)) (str.substr x z 1) "") (str.substr x (+ 1 z) (str.len x)))))
 )
 )

diff --git a/test/regress/regress1/strings/type002.smt2 b/test/regress/regress1/strings/type002.smt2
index 3b46b25a8d2717638847961fd1108c6a60ee9a7a..af2e293c216c8a98b85dac5b8b269a253728ec0e 100644 (file)
--- a/test/regress/regress1/strings/type002.smt2
+++ b/test/regress/regress1/strings/type002.smt2
@@ -1,4 +1,4 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_SLIA)
 (set-info :status sat)
 (set-option :strings-exp true)
@@ -9,7 +9,7 @@
 (declare-fun i () Int)
 
 (assert (>= i 420))
-(assert (= x (int.to.str i)))
+(assert (= x (str.from_int i)))
 (assert (= x (str.++ y "0" z)))
 (assert (not (= y "")))
 (assert (not (= z "")))

diff --git a/test/regress/regress1/strings/type003.smt2 b/test/regress/regress1/strings/type003.smt2
index 332ec3ec364c1ba8b00b22a2b9535111eb16b680..87c8b39034885d8a29452e9bd1b321fa662c20b3 100644 (file)
--- a/test/regress/regress1/strings/type003.smt2
+++ b/test/regress/regress1/strings/type003.smt2
@@ -1,4 +1,4 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_SLIA)
 (set-info :status sat)
 (set-option :strings-exp true)
@@ -6,7 +6,7 @@
 (declare-fun i () Int)
 (declare-fun s () String)
 
-(assert (< 67 (str.to.int s)))
+(assert (< 67 (str.to_int s)))
 (assert (= (str.len s) 2))
 (assert (not (= s "68")))
 

diff --git a/test/regress/regress1/strings/username_checker_min.smt2 b/test/regress/regress1/strings/username_checker_min.smt2
index f6c152a2a580ff5d41dc548454ee3e5935045d0f..c4c21dface0a430d747a78f454e9983dbaa3af43 100644 (file)
--- a/test/regress/regress1/strings/username_checker_min.smt2
+++ b/test/regress/regress1/strings/username_checker_min.smt2
@@ -1,4 +1,4 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_S)
 (set-option :strings-exp true)
 (set-info :status unsat)
@@ -8,7 +8,7 @@
 (assert (= (str.len buff) 4))
 (assert (= (str.len pass_mem) 1))
 
-(assert (str.in.re (str.++ buff pass_mem) (re.+ (str.to.re "A"))))
+(assert (str.in_re (str.++ buff pass_mem) (re.+ (str.to_re "A"))))
 
 (assert (str.contains buff "<"))
 

diff --git a/test/regress/regress2/strings/issue918.smt2 b/test/regress/regress2/strings/issue918.smt2
index 8f390df26d8562c685770fe46cae60094b2e8517..0843a17002dd0f88d316837b82c053223dccc093 100644 (file)
--- a/test/regress/regress2/strings/issue918.smt2
+++ b/test/regress/regress2/strings/issue918.smt2
@@ -1,8 +1,8 @@
 ; COMMAND-LINE: --strings-exp --re-elim
 ; EXPECT: sat
+(set-info :smt-lib-version 2.5)
 (set-option :produce-models true)
 (set-logic UFDTSLIA)
-(set-info :smt-lib-version 2.5)
 (declare-datatypes () (
     (StringRotation (StringRotation$C_StringRotation (StringRotation$C_StringRotation$sr String)))
     (StringRotation2 (StringRotation2$C_StringRotation2 (StringRotation2$C_StringRotation2$sr1 StringRotation) (StringRotation2$C_StringRotation2$sr2 StringRotation)))

diff --git a/test/regress/regress2/strings/non_termination_regular_expression6.smt2 b/test/regress/regress2/strings/non_termination_regular_expression6.smt2
index 340cade1cd7a32ebadf5e915365ad41608f18ecd..175ee5cc0dc63f6c8f1df8848e58b82fa571782f 100644 (file)
--- a/test/regress/regress2/strings/non_termination_regular_expression6.smt2
+++ b/test/regress/regress2/strings/non_termination_regular_expression6.smt2
@@ -17,7 +17,7 @@
 
 ; Resource: p0.0
 (declare-const p0.0.resource Bool)
-(assert (= p0.0.resource (and (= resource_prefix "arn") (= resource_partition "aws") (= resource_service "sqs") (= resource_region "us-east-1") (= resource_account "111144448888") (str.in.re resource_resource (re.++ (str.to.re "ab") (re.* re.allchar) (str.to.re "b") (re.* re.allchar) (str.to.re "b") (re.* re.allchar) (str.to.re "b"))))))
+(assert (= p0.0.resource (and (= resource_prefix "arn") (= resource_partition "aws") (= resource_service "sqs") (= resource_region "us-east-1") (= resource_account "111144448888") (str.in_re resource_resource (re.++ (str.to_re "ab") (re.* re.allchar) (str.to_re "b") (re.* re.allchar) (str.to_re "b") (re.* re.allchar) (str.to_re "b"))))))
 
 ; Statement: p0.0
 (declare-const p0.0.statement.allows Bool)
@@ -37,7 +37,7 @@
 
 ; Resource: p1.0
 (declare-const p1.0.resource Bool)
-(assert (= p1.0.resource (and (= resource_prefix "arn") (= resource_partition "aws") (= resource_service "sqs") (= resource_region "us-east-1") (= resource_account "111144448888") (str.in.re resource_resource (re.++ (str.to.re "a") (re.* re.allchar) (str.to.re "b") (re.* re.allchar) (str.to.re "b") (re.* re.allchar) (str.to.re "b"))))))
+(assert (= p1.0.resource (and (= resource_prefix "arn") (= resource_partition "aws") (= resource_service "sqs") (= resource_region "us-east-1") (= resource_account "111144448888") (str.in_re resource_resource (re.++ (str.to_re "a") (re.* re.allchar) (str.to_re "b") (re.* re.allchar) (str.to_re "b") (re.* re.allchar) (str.to_re "b"))))))
 
 ; Statement: p1.0
 (declare-const p1.0.statement.allows Bool)

diff --git a/test/regress/regress2/strings/norn-dis-0707-3.smt2 b/test/regress/regress2/strings/norn-dis-0707-3.smt2
index 47b2e6b196e3a3f2c457e823b75b6bf6742a0ace..242d7e958d48030b08aac510516a1d06d3d70bc3 100644 (file)
--- a/test/regress/regress2/strings/norn-dis-0707-3.smt2
+++ b/test/regress/regress2/strings/norn-dis-0707-3.smt2
@@ -17,11 +17,11 @@
 (declare-fun var_11 () String)
 (declare-fun var_12 () String)
 
-(assert (str.in.re (str.++ var_8 "z" var_9 ) (re.++ (re.* (re.union (str.to.re "a") (re.++ (str.to.re "b") (re.++ (re.* (re.union (str.to.re "b") (str.to.re "a"))) (str.to.re "z"))))) (re.++ (str.to.re "b") (re.* (re.union (str.to.re "b") (str.to.re "a")))))))
-(assert (str.in.re (str.++ var_8 "z" var_9 ) (re.++ (re.* (re.union (re.union (str.to.re "z") (str.to.re "a")) (re.++ (str.to.re "b") (re.++ (re.* (str.to.re "b")) (re.union (str.to.re "z") (str.to.re "a")))))) (re.++ (str.to.re "b") (re.* (str.to.re "b"))))))
-(assert (str.in.re (str.++ var_8 "z" var_9 ) (re.++ (re.* (re.union (str.to.re "a") (re.++ (str.to.re "b") (re.++ (re.* (re.union (str.to.re "z") (str.to.re "a"))) (str.to.re "b"))))) (re.++ (str.to.re "b") (re.* (re.union (str.to.re "z") (str.to.re "a")))))))
-(assert (str.in.re (str.++ var_8 "z" var_9 ) (re.* (re.++ (re.union (str.to.re "b") (str.to.re "a")) (re.++ (re.* (str.to.re "a")) (re.union (str.to.re "z") (str.to.re "b")))))))
-(assert (str.in.re var_9 (re.* (re.range "a" "u"))))
-(assert (str.in.re var_8 (re.* (re.range "a" "u"))))
-(assert (not (str.in.re (str.++ "b" var_8 "z" "b" var_9 ) (re.++ (re.* (re.++ (str.to.re "b") (str.to.re "z"))) (str.to.re "b")))))
+(assert (str.in_re (str.++ var_8 "z" var_9 ) (re.++ (re.* (re.union (str.to_re "a") (re.++ (str.to_re "b") (re.++ (re.* (re.union (str.to_re "b") (str.to_re "a"))) (str.to_re "z"))))) (re.++ (str.to_re "b") (re.* (re.union (str.to_re "b") (str.to_re "a")))))))
+(assert (str.in_re (str.++ var_8 "z" var_9 ) (re.++ (re.* (re.union (re.union (str.to_re "z") (str.to_re "a")) (re.++ (str.to_re "b") (re.++ (re.* (str.to_re "b")) (re.union (str.to_re "z") (str.to_re "a")))))) (re.++ (str.to_re "b") (re.* (str.to_re "b"))))))
+(assert (str.in_re (str.++ var_8 "z" var_9 ) (re.++ (re.* (re.union (str.to_re "a") (re.++ (str.to_re "b") (re.++ (re.* (re.union (str.to_re "z") (str.to_re "a"))) (str.to_re "b"))))) (re.++ (str.to_re "b") (re.* (re.union (str.to_re "z") (str.to_re "a")))))))
+(assert (str.in_re (str.++ var_8 "z" var_9 ) (re.* (re.++ (re.union (str.to_re "b") (str.to_re "a")) (re.++ (re.* (str.to_re "a")) (re.union (str.to_re "z") (str.to_re "b")))))))
+(assert (str.in_re var_9 (re.* (re.range "a" "u"))))
+(assert (str.in_re var_8 (re.* (re.range "a" "u"))))
+(assert (not (str.in_re (str.++ "b" var_8 "z" "b" var_9 ) (re.++ (re.* (re.++ (str.to_re "b") (str.to_re "z"))) (str.to_re "b")))))
 (check-sat)

diff --git a/test/regress/regress2/strings/range-perf.smt2 b/test/regress/regress2/strings/range-perf.smt2
index 33960e1246e8f3d40b39312f2bbd7897a07095bc..c8a8f42fac4618082133ad716815b646ef0bc1b1 100644 (file)
--- a/test/regress/regress2/strings/range-perf.smt2
+++ b/test/regress/regress2/strings/range-perf.smt2
@@ -2,6 +2,6 @@
 ; EXPECT: sat
 (set-logic QF_SLIA)
 (declare-const x String)
-(assert (str.in.re x ((_ re.loop 12 12) (re.range "0" "9"))))
-(assert (str.in.re x (re.++ (re.* re.allchar) (str.to.re "01") (re.* re.allchar))))
+(assert (str.in_re x ((_ re.loop 12 12) (re.range "0" "9"))))
+(assert (str.in_re x (re.++ (re.* re.allchar) (str.to_re "01") (re.* re.allchar))))
 (check-sat)

diff --git a/test/regress/regress2/strings/replaceall-diffrange.smt2 b/test/regress/regress2/strings/replaceall-diffrange.smt2
index 5d1ef57bfd07d419fe8b890441b3ce5213b15ee6..507c972182758216f07571849520dbab3c5098e3 100644 (file)
--- a/test/regress/regress2/strings/replaceall-diffrange.smt2
+++ b/test/regress/regress2/strings/replaceall-diffrange.smt2
@@ -1,4 +1,4 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic ALL)
 (set-info :status sat)
 (set-option :strings-exp true)
@@ -7,5 +7,5 @@
 (declare-fun y () String)
 (declare-fun z () String)
 (declare-fun w () String)
-(assert (= (str.len (str.replaceall x y z)) (+ (str.len (str.replaceall x y w)) 3)))
+(assert (= (str.len (str.replace_all x y z)) (+ (str.len (str.replace_all x y w)) 3)))
 (check-sat)

diff --git a/test/regress/regress2/strings/replaceall-len-c.smt2 b/test/regress/regress2/strings/replaceall-len-c.smt2
index 336ec10e49683cb5495bd89688b0656e188b8b49..75840a52f9a8e0bb07fa08581b45541118aca7a6 100644 (file)
--- a/test/regress/regress2/strings/replaceall-len-c.smt2
+++ b/test/regress/regress2/strings/replaceall-len-c.smt2
@@ -1,8 +1,8 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic ALL)
 (set-info :status sat)
 (set-option :strings-exp true)
 (set-option :strings-fmf true)
 (declare-fun x () String)
-(assert (= (str.len (str.replaceall "ABBABAAB" x "C")) 5))
+(assert (= (str.len (str.replace_all "ABBABAAB" x "C")) 5))
 (check-sat)

diff --git a/test/regress/regress2/strings/small-1.smt2 b/test/regress/regress2/strings/small-1.smt2
index 9fc2c9f9e0169c1e6b3f3f3776c2c57369cdf004..e0dea5d8913ec2236a7f66046f7e839897e20128 100644 (file)
--- a/test/regress/regress2/strings/small-1.smt2
+++ b/test/regress/regress2/strings/small-1.smt2
@@ -1,8 +1,8 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic ALL)
 (set-info :status sat)
 (set-option :strings-exp true)
 (set-option :re-elim true)
 (declare-const x String)
-(assert (str.in.re x (re.++ (str.to.re "example-bucket/") (re.* re.allchar) (str.to.re "/") re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar (str.to.re "-") re.allchar re.allchar re.allchar re.allchar (str.to.re "-") re.allchar re.allchar re.allchar re.allchar (str.to.re "-") re.allchar re.allchar re.allchar re.allchar (str.to.re "-") re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar (str.to.re "/foo"))))
+(assert (str.in_re x (re.++ (str.to_re "example-bucket/") (re.* re.allchar) (str.to_re "/") re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar (str.to_re "-") re.allchar re.allchar re.allchar re.allchar (str.to_re "-") re.allchar re.allchar re.allchar re.allchar (str.to_re "-") re.allchar re.allchar re.allchar re.allchar (str.to_re "-") re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar (str.to_re "/foo"))))
 (check-sat)

diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index bfbe201d28d6ee490926327a93028362e6e0c423..07b5c5aec6ce616d81ac14bdc61fd2dd1e970eaf 100644 (file)
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -1041,7 +1041,6 @@ void SolverBlack::testSetInfo()
   TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("smt-lib-version", "2.0"));
   TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("smt-lib-version", "2.5"));
   TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("smt-lib-version", "2.6"));
-  TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("smt-lib-version", "2.6.1"));
   TS_ASSERT_THROWS(d_solver->setInfo("smt-lib-version", ".0"),
                    CVC4ApiException&);