diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-28 11:15:00 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-28 11:15:00 -0500 |
commit | 967332f464f3e26d43f05bb9c68a0be788337ef6 (patch) | |
tree | 561391457c65750a8e7fac9b6656a7e7e4176a69 /src/printer/smt2/smt2_printer.cpp | |
parent | 8ea1603f55d940e56ab3cbee8177f06200228aaa (diff) |
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.
Diffstat (limited to 'src/printer/smt2/smt2_printer.cpp')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 23 |
1 files changed, 7 insertions, 16 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 4013cbd08..fbccd26ed 100644 --- 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.++"; |