From: Andrew Reynolds Date: Wed, 5 Sep 2018 14:14:14 +0000 (-0500) Subject: Extended rewriter for string equalities (#2427) X-Git-Tag: cvc5-1.0.0~4681 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cc653cb01f824313d22ffc569ba46bc14b447364;p=cvc5.git Extended rewriter for string equalities (#2427) --- diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index 21a7fe29c..01454c3c7 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -20,6 +20,7 @@ #include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" +#include "theory/strings/theory_strings_rewriter.h" using namespace CVC4::kind; using namespace std; @@ -207,6 +208,10 @@ Node ExtendedRewriter::extendedRewrite(Node n) { new_ret = extendedRewriteArith(ret); } + else if (tid == THEORY_STRINGS) + { + new_ret = extendedRewriteStrings(ret); + } } //----------------------end theory-specific post-rewriting @@ -1661,6 +1666,152 @@ Node ExtendedRewriter::extendedRewriteArith(Node ret) return new_ret; } +Node ExtendedRewriter::extendedRewriteStrings(Node ret) +{ + Node new_ret; + Trace("q-ext-rewrite-debug") + << "Extended rewrite strings : " << ret << std::endl; + NodeManager* nm = NodeManager::currentNM(); + if (ret.getKind() == EQUAL) + { + if (ret[0].getType().isString()) + { + Node tcontains[2]; + bool tcontainsOneTrue = false; + unsigned tcontainsTrueIndex = 0; + for (unsigned i = 0; i < 2; i++) + { + Node tc = nm->mkNode(STRING_STRCTN, ret[i], ret[1 - i]); + tcontains[i] = Rewriter::rewrite(tc); + if (tcontains[i].isConst()) + { + if (tcontains[i].getConst()) + { + tcontainsOneTrue = true; + tcontainsTrueIndex = i; + } + else + { + new_ret = tcontains[i]; + // if str.contains( x, y ) ---> false then x = y ---> false + // Notice we may not catch this in the rewriter for strings + // equality, since it only calls the specific rewriter for + // contains and not the full rewriter. + debugExtendedRewrite(ret, new_ret, "eq-contains-one-false"); + return new_ret; + } + } + } + if (tcontainsOneTrue) + { + // if str.contains( x, y ) ---> true + // then x = y ---> contains( y, x ) + new_ret = tcontains[1 - tcontainsTrueIndex]; + debugExtendedRewrite(ret, new_ret, "eq-contains-one-true"); + return new_ret; + } + else if (tcontains[0] == tcontains[1] && tcontains[0] != ret) + { + // if str.contains( x, y ) ---> t and str.contains( y, x ) ---> t, + // then x = y ---> t + new_ret = tcontains[0]; + debugExtendedRewrite(ret, new_ret, "eq-dual-contains-eq"); + return new_ret; + } + + std::vector c[2]; + for (unsigned i = 0; i < 2; i++) + { + strings::TheoryStringsRewriter::getConcat(ret[i], c[i]); + } + + bool changed = false; + for (unsigned i = 0; i < 2; i++) + { + while (!c[0].empty() && !c[1].empty() && c[0].back() == c[1].back()) + { + c[0].pop_back(); + c[1].pop_back(); + changed = true; + } + // splice constants + if (!c[0].empty() && !c[1].empty() && c[0].back().isConst() + && c[1].back().isConst()) + { + String cs[2]; + for (unsigned j = 0; j < 2; j++) + { + cs[j] = c[j].back().getConst(); + } + unsigned larger = cs[0].size() > cs[1].size() ? 0 : 1; + unsigned smallerSize = cs[1 - larger].size(); + if (cs[1 - larger] + == (i == 0 ? cs[larger].suffix(smallerSize) + : cs[larger].prefix(smallerSize))) + { + unsigned sizeDiff = cs[larger].size() - smallerSize; + c[larger][c[larger].size() - 1] = + nm->mkConst(i == 0 ? cs[larger].prefix(sizeDiff) + : cs[larger].suffix(sizeDiff)); + c[1 - larger].pop_back(); + changed = true; + } + } + for (unsigned j = 0; j < 2; j++) + { + std::reverse(c[j].begin(), c[j].end()); + } + } + if (changed) + { + // e.g. x++y = x++z ---> y = z, "AB" ++ x = "A" ++ y --> "B" ++ x = y + Node s1 = strings::TheoryStringsRewriter::mkConcat(STRING_CONCAT, c[0]); + Node s2 = strings::TheoryStringsRewriter::mkConcat(STRING_CONCAT, c[1]); + new_ret = s1.eqNode(s2); + debugExtendedRewrite(ret, new_ret, "string-eq-unify"); + return new_ret; + } + + // homogeneous constants + if (d_aggr) + { + for (unsigned i = 0; i < 2; i++) + { + if (ret[i].isConst()) + { + bool isHomogeneous = true; + std::vector vec = ret[i].getConst().getVec(); + if (vec.size() > 1) + { + unsigned hchar = vec[0]; + for (unsigned j = 1, size = vec.size(); j < size; j++) + { + if (vec[j] != hchar) + { + isHomogeneous = false; + break; + } + } + } + if (isHomogeneous && !std::is_sorted(c[1-i].begin(),c[1-i].end())) + { + Node ss = strings::TheoryStringsRewriter::mkConcat(STRING_CONCAT, + c[1 - i]); + Assert(ss != ret[1 - i]); + // e.g. "AA" = x ++ y ---> "AA" = y ++ x if y < x + new_ret = ret[i].eqNode(ss); + debugExtendedRewrite(ret, new_ret, "string-eq-homog-const"); + return new_ret; + } + } + } + } + } + } + + return new_ret; +} + void ExtendedRewriter::debugExtendedRewrite(Node n, Node ret, const char* c) const diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h index 29f3b7bb3..da77bda51 100644 --- a/src/theory/quantifiers/extended_rewrite.h +++ b/src/theory/quantifiers/extended_rewrite.h @@ -231,8 +231,18 @@ class ExtendedRewriter //--------------------------------------end generic utilities //--------------------------------------theory-specific top-level calls - /** extended rewrite arith */ + /** extended rewrite arith + * + * If this method returns a non-null node ret', then ret is equivalent to + * ret'. + */ Node extendedRewriteArith(Node ret); + /** extended rewrite strings + * + * If this method returns a non-null node ret', then ret is equivalent to + * ret'. + */ + Node extendedRewriteStrings(Node ret); //--------------------------------------end theory-specific top-level calls }; diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index e6f3da03a..e09eefddc 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -911,6 +911,25 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) { Node one = nm->mkConst(Rational(1)); retNode = one.eqNode(nm->mkNode(STRING_LENGTH, x)); } else if( r.getKind() == kind::REGEXP_STAR ) { + if (x.isConst()) + { + String s = x.getConst(); + if (s.size() == 0) + { + retNode = nm->mkConst(true); + // e.g. (str.in.re "" (re.* (str.to.re x))) ----> true + return returnRewrite(node, retNode, "re-empty-in-str-star"); + } + else if (s.size() == 1) + { + if (r[0].getKind() == STRING_TO_REGEXP) + { + retNode = r[0][0].eqNode(x); + // e.g. (str.in.re "A" (re.* (str.to.re x))) ----> "A" = x + return returnRewrite(node, retNode, "re-char-in-str-star"); + } + } + } if (r[0].getKind() == kind::REGEXP_SIGMA) { retNode = NodeManager::currentNM()->mkConst( true ); diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index ca9b88ecf..39a7a4f4d 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -824,6 +824,7 @@ REG0_TESTS = \ regress0/strings/strings-charat.cvc \ regress0/strings/strings-native-simple.cvc \ regress0/strings/strip-endpoint-itos.smt2 \ + regress0/strings/str_unsound_ext_rew_eq.smt2 \ regress0/strings/substr-rewrites.smt2 \ regress0/strings/type001.smt2 \ regress0/strings/unsound-0908.smt2 \ diff --git a/test/regress/regress0/strings/str_unsound_ext_rew_eq.smt2 b/test/regress/regress0/strings/str_unsound_ext_rew_eq.smt2 new file mode 100644 index 000000000..62ef4bd3a --- /dev/null +++ b/test/regress/regress0/strings/str_unsound_ext_rew_eq.smt2 @@ -0,0 +1,12 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-fun y () String) + +(declare-fun x () String) + +(assert +(= (str.++ (str.++ (str.++ y "B") "A") x) (str.++ (str.++ "A" x) "B")) +) + +; triggered an unsoundness during development of extended rewriter for strings, caught by sygus-rr-verify +(check-sat)