diff options
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.++"; |