From: Andrew Reynolds Date: Thu, 27 Feb 2020 03:54:29 +0000 (-0600) Subject: Add support for is_digit and regular expression difference (#3828) X-Git-Tag: cvc5-1.0.0~3586 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=87f3741db6ed41d3a776774bc1b60fd696585391;p=cvc5.git Add support for is_digit and regular expression difference (#3828) Towards support for the strings standard. This adds support for str.is_digit and re.diff, which both can be eliminated eager during preprocessing. --- diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 02fbbc42c..0a365a4d5 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -263,6 +263,7 @@ const static std::unordered_map s_kinds{ {STRING_LEQ, CVC4::Kind::STRING_LEQ}, {STRING_PREFIX, CVC4::Kind::STRING_PREFIX}, {STRING_SUFFIX, CVC4::Kind::STRING_SUFFIX}, + {STRING_IS_DIGIT, CVC4::Kind::STRING_IS_DIGIT}, {STRING_ITOS, CVC4::Kind::STRING_ITOS}, {STRING_STOI, CVC4::Kind::STRING_STOI}, {CONST_STRING, CVC4::Kind::CONST_STRING}, @@ -270,6 +271,7 @@ const static std::unordered_map s_kinds{ {REGEXP_CONCAT, CVC4::Kind::REGEXP_CONCAT}, {REGEXP_UNION, CVC4::Kind::REGEXP_UNION}, {REGEXP_INTER, CVC4::Kind::REGEXP_INTER}, + {REGEXP_DIFF, CVC4::Kind::REGEXP_DIFF}, {REGEXP_STAR, CVC4::Kind::REGEXP_STAR}, {REGEXP_PLUS, CVC4::Kind::REGEXP_PLUS}, {REGEXP_OPT, CVC4::Kind::REGEXP_OPT}, @@ -527,6 +529,7 @@ const static std::unordered_map {CVC4::Kind::STRING_LEQ, STRING_LEQ}, {CVC4::Kind::STRING_PREFIX, STRING_PREFIX}, {CVC4::Kind::STRING_SUFFIX, STRING_SUFFIX}, + {CVC4::Kind::STRING_IS_DIGIT, STRING_IS_DIGIT}, {CVC4::Kind::STRING_ITOS, STRING_ITOS}, {CVC4::Kind::STRING_STOI, STRING_STOI}, {CVC4::Kind::CONST_STRING, CONST_STRING}, @@ -534,6 +537,7 @@ const static std::unordered_map {CVC4::Kind::REGEXP_CONCAT, REGEXP_CONCAT}, {CVC4::Kind::REGEXP_UNION, REGEXP_UNION}, {CVC4::Kind::REGEXP_INTER, REGEXP_INTER}, + {CVC4::Kind::REGEXP_DIFF, REGEXP_DIFF}, {CVC4::Kind::REGEXP_STAR, REGEXP_STAR}, {CVC4::Kind::REGEXP_PLUS, REGEXP_PLUS}, {CVC4::Kind::REGEXP_OPT, REGEXP_OPT}, diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index ca5696537..eb8575907 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -2045,6 +2045,16 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, const std::vector& children) */ STRING_SUFFIX, + /** + * String is-digit. + * Returns true if string s is digit (it is one of "0", ..., "9"). + * Parameters: 1 + * -[1]: Term of sort String + * Create with: + * mkTerm(Kind kind, Term child1) + * mkTerm(Kind kind, const std::vector& children) + */ + STRING_IS_DIGIT, /** * Integer to string. * If the integer is negative this operator returns the empty string. @@ -2110,6 +2120,15 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, const std::vector& children) */ REGEXP_INTER, + /** + * Regexp difference. + * Parameters: 2 + * -[1]..[2]: Terms of Regexp sort + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector& children) + */ + REGEXP_DIFF, /** * Regexp *. * Parameters: 1 diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index d915d2ab4..ff155d0f9 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -171,6 +171,7 @@ void Smt2::addStringOperators() { } addOperator(kind::STRING_PREFIX, "str.prefixof" ); addOperator(kind::STRING_SUFFIX, "str.suffixof" ); + addOperator(kind::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 || getLanguage() == language::input::LANG_SYGUS_V2) @@ -201,6 +202,7 @@ void Smt2::addStringOperators() { addOperator(kind::REGEXP_RANGE, "re.range"); addOperator(kind::REGEXP_LOOP, "re.loop"); addOperator(kind::REGEXP_COMPLEMENT, "re.comp"); + addOperator(kind::REGEXP_DIFF, "re.diff"); addOperator(kind::STRING_LT, "str.<"); addOperator(kind::STRING_LEQ, "str.<="); } diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 052b75302..965c56ee4 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -25,6 +25,7 @@ operator STRING_STRREPL 3 "string replace" operator STRING_STRREPLALL 3 "string replace all" operator STRING_PREFIX 2 "string prefixof" operator STRING_SUFFIX 2 "string suffixof" +operator STRING_IS_DIGIT 1 "string isdigit, returns true if argument is a string of length one that represents a digit" operator STRING_ITOS 1 "integer to string" operator STRING_STOI 1 "string to integer (total function)" operator STRING_CODE 1 "string to code, returns the code of the first character of the string if it has length one, -1 otherwise" @@ -63,6 +64,7 @@ operator STRING_TO_REGEXP 1 "convert string to regexp" operator REGEXP_CONCAT 2: "regexp concat" operator REGEXP_UNION 2: "regexp union" operator REGEXP_INTER 2: "regexp intersection" +operator REGEXP_DIFF 2: "regexp difference" operator REGEXP_STAR 1 "regexp *" operator REGEXP_PLUS 1 "regexp +" operator REGEXP_OPT 1 "regexp ?" @@ -81,6 +83,7 @@ typerule REGEXP_RV "SimpleTypeRule" typerule REGEXP_CONCAT "SimpleTypeRuleVar" typerule REGEXP_UNION "SimpleTypeRuleVar" typerule REGEXP_INTER "SimpleTypeRuleVar" +typerule REGEXP_DIFF "SimpleTypeRuleVar" typerule REGEXP_STAR "SimpleTypeRule" typerule REGEXP_PLUS "SimpleTypeRule" typerule REGEXP_OPT "SimpleTypeRule" @@ -102,6 +105,7 @@ typerule STRING_STRREPL "SimpleTypeRule" typerule STRING_STRREPLALL "SimpleTypeRule" typerule STRING_PREFIX "SimpleTypeRule" typerule STRING_SUFFIX "SimpleTypeRule" +typerule STRING_IS_DIGIT "SimpleTypeRule" typerule STRING_ITOS "SimpleTypeRule" typerule STRING_STOI "SimpleTypeRule" typerule STRING_CODE "SimpleTypeRule" diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index e58a51e63..d8bc7f34f 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1664,6 +1664,14 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { { retNode = rewritePrefixSuffix(node); } + else if (nk == STRING_IS_DIGIT) + { + // eliminate str.is_digit(s) ----> 48 <= str.to_code(s) <= 57 + Node t = nm->mkNode(STRING_CODE, node[0]); + retNode = nm->mkNode(AND, + nm->mkNode(LEQ, nm->mkConst(Rational(48)), t), + nm->mkNode(LEQ, t, nm->mkConst(Rational(57)))); + } else if (nk == kind::STRING_ITOS) { if(node[0].isConst()) { @@ -1713,6 +1721,10 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { { retNode = rewriteAndOrRegExp(node); } + else if (nk == REGEXP_DIFF) + { + retNode = nm->mkNode(REGEXP_INTER, node[0],nm->mkNode(REGEXP_COMPLEMENT, node[1])); + } else if (nk == REGEXP_STAR) { retNode = rewriteStarRegExp(node); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 295575728..7be085d48 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -906,6 +906,7 @@ set(regress_0_tests regress0/strings/idof-sem.smt2 regress0/strings/ilc-like.smt2 regress0/strings/indexof-sym-simp.smt2 + regress0/strings/is_digit_simple.smt2 regress0/strings/issue1189.smt2 regress0/strings/issue2958.smt2 regress0/strings/issue3440.smt2 @@ -921,6 +922,7 @@ set(regress_0_tests regress0/strings/parser-syms.cvc regress0/strings/re.all.smt2 regress0/strings/re-syntax.smt2 + regress0/strings/re_diff.smt2 regress0/strings/regexp-native-simple.cvc regress0/strings/regexp_inclusion.smt2 regress0/strings/regexp_inclusion_reduction.smt2 diff --git a/test/regress/regress0/strings/is_digit_simple.smt2 b/test/regress/regress0/strings/is_digit_simple.smt2 new file mode 100644 index 000000000..d95a22078 --- /dev/null +++ b/test/regress/regress0/strings/is_digit_simple.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --lang=smt2.6.1 +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) + +(assert (str.is_digit "0")) +(assert (str.is_digit "7")) +(assert (not (str.is_digit "A"))) +(assert (not (str.is_digit ""))) + +(check-sat) diff --git a/test/regress/regress0/strings/re_diff.smt2 b/test/regress/regress0/strings/re_diff.smt2 new file mode 100644 index 000000000..d63731acb --- /dev/null +++ b/test/regress/regress0/strings/re_diff.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --lang=smt2.6.1 +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(declare-fun x () String) +(declare-fun y () String) + +(assert (str.in_re x (re.diff (re.* (str.to_re "A")) re.none))) +(assert (or (not (str.in_re x (re.* (str.to_re "A")))) (str.in_re y (re.diff (re.* (str.to_re "B")) re.all)))) + +(check-sat)