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 02fbbc42c47c76a45b563da372479427dfe61e9c..0a365a4d585050558b2005d02642cdc7152c1636 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -263,6 +263,7 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> 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<Kind, CVC4::Kind, KindHashFunction> 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, Kind, CVC4::kind::KindHashFunction>
         {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, Kind, CVC4::kind::KindHashFunction>
         {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 ca5696537ec93ffdba0b2d95fc799c6792666b3f..eb85759076fdddc0601a5dba1238fe0c3d40f60f 100644 (file)
--- 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<Term>& 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<Term>& 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<Term>& 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<Term>& children)
+   */
+  REGEXP_DIFF,
   /**
    * Regexp *.
    * Parameters: 1

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index d915d2ab43ed1aa3b5d13b1f73af49051c0c9ada..ff155d0f970cd344d3670aeff5256cb772e88eac 100644 (file)
--- 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 052b753022fee376e17b792ea2815016128ec575..965c56ee40b003111254da8813617a660a733c65 100644 (file)
--- 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<RRegExp, AInteger>"
 typerule REGEXP_CONCAT "SimpleTypeRuleVar<RRegExp, ARegExp>"
 typerule REGEXP_UNION "SimpleTypeRuleVar<RRegExp, ARegExp>"
 typerule REGEXP_INTER "SimpleTypeRuleVar<RRegExp, ARegExp>"
+typerule REGEXP_DIFF "SimpleTypeRuleVar<RRegExp, ARegExp>"
 typerule REGEXP_STAR "SimpleTypeRule<RRegExp, ARegExp>"
 typerule REGEXP_PLUS "SimpleTypeRule<RRegExp, ARegExp>"
 typerule REGEXP_OPT "SimpleTypeRule<RRegExp, ARegExp>"
@@ -102,6 +105,7 @@ typerule STRING_STRREPL "SimpleTypeRule<RString, AString, AString, AString>"
 typerule STRING_STRREPLALL "SimpleTypeRule<RString, AString, AString, AString>"
 typerule STRING_PREFIX "SimpleTypeRule<RBool, AString, AString>"
 typerule STRING_SUFFIX "SimpleTypeRule<RBool, AString, AString>"
+typerule STRING_IS_DIGIT "SimpleTypeRule<RBool, AString>"
 typerule STRING_ITOS "SimpleTypeRule<RString, AInteger>"
 typerule STRING_STOI "SimpleTypeRule<RInteger, AString>"
 typerule STRING_CODE "SimpleTypeRule<RInteger, AString>"

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index e58a51e6399eb564329d599a2f7463ee1a62c221..d8bc7f34f5548874f252daf9e45122852f73ac55 100644 (file)
--- 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 295575728bbdbc30e13a6b62ebac0b7b86bf2725..7be085d483513db992081d9ce089caa78adfacc0 100644 (file)
--- 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 (file)
index 0000000..d95a220
--- /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 (file)
index 0000000..d63731a
--- /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)