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 | |
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')
-rw-r--r-- | src/printer/printer.cpp | 6 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 23 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.h | 13 |
3 files changed, 14 insertions, 28 deletions
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 886be0cfa..085a32c43 100644 --- 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 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.++"; diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 579231364..b34acacbb 100644 --- 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) { } |