Extended rewriter for string equalities (#2427)

5 files changed, 194 insertions, 1 deletions

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<bool>())
+          {
+            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<Node> 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<String>();
+          }
+          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<unsigned> vec = ret[i].getConst<String>().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<String>();
+      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)