Infer substitutions in str.contains rewriter

2 files changed, 183 insertions, 17 deletions

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index fa706b245..cf6bda328 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -1821,6 +1821,7 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
       }
     }
     Trace("strings-rewrite-multiset") << "For " << node << " : " << std::endl;
+    bool sameConst = true;
     for (const Node& ch : chars)
     {
       Trace("strings-rewrite-multiset") << "  # occurrences of substring ";
@@ -1832,7 +1833,51 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
         Node ret = NodeManager::currentNM()->mkConst(false);
         return returnRewrite(node, ret, "ctn-mset-nss");
       }
+      else if (count_const[0][ch] > count_const[1][ch])
+      {
+        sameConst = false;
+      }
     }
+
+    if (sameConst)
+    {
+      // Find all non-const components that appear in the second argument but
+      // not the first
+      std::unordered_set<Node, NodeHashFunction> nConstEmpty;
+      for (std::pair<const Node, unsigned>& nncp : num_nconst[1])
+      {
+        if (nncp.second > num_nconst[0][nncp.first])
+        {
+          nConstEmpty.insert(nncp.first);
+        }
+      }
+
+      if (nConstEmpty.size() > 0)
+      {
+        std::vector<Node> cs;
+        std::vector<Node> nnc2;
+        for (const Node& n : nc2)
+        {
+          if (nConstEmpty.find(n) == nConstEmpty.end())
+          {
+            nnc2.push_back(n);
+          }
+        }
+        cs.push_back(nm->mkNode(
+            kind::STRING_STRCTN, node[0], mkConcat(kind::STRING_CONCAT, nnc2)));
+
+        Node emptyStr = nm->mkConst(String(""));
+        for (const Node& n : nConstEmpty)
+        {
+          cs.push_back(nm->mkNode(kind::EQUAL, n, emptyStr));
+        }
+
+        Assert(cs.size() >= 2);
+        Node res = nm->mkNode(kind::AND, cs);
+        return returnRewrite(node, res, "ctn-mset-substs");
+      }
+    }
+
     // TODO (#1180): count the number of 2,3,4,.. character substrings
     // for example:
     // str.contains( str.++( x, "cbabc" ), str.++( "cabbc", x ) ) ---> false
@@ -1840,6 +1885,7 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
     // note this is orthogonal reasoning to inductive reasoning
     // via regular membership reduction in Liang et al CAV 2015.
   }
+
   // TODO (#1180): abstract interpretation with multi-set domain
   // to show first argument is a strict subset of second argument
 
@@ -2156,23 +2202,6 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
       return returnRewrite(node, ret, "rpl-const-find");
     }
   }
-  
-  if( node[0].isConst() )
-  {
-    // str.replace( "", x, t ) ---> str.replace( "", x, t{x->""} )
-    CVC4::String s = node[0].getConst<String>();
-    if( s.empty() )
-    {
-      TNode v = node[1];
-      TNode s = node[0];
-      Node sn2 = node[2].substitute(v,s);
-      if( sn2!=node[2] )
-      {
-        Node ret = nm->mkNode( STRING_STRREPL, node[0], node[1], sn2 );
-        return returnRewrite(node, ret, "repl-empty-subs");
-      }
-    }
-  }
 
   if (node[0] == node[2])
   {
@@ -2239,6 +2268,83 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
       return returnRewrite(node, node[0], "rpl-nctn");
     }
   }
+  else if (cmp_conr.getKind() == kind::EQUAL || cmp_conr.getKind() == kind::AND)
+  {
+    Node empty = nm->mkConst(::CVC4::String(""));
+
+    std::set<TNode> emptyNodes;
+    std::vector<TNode> nodesToKeep;
+    if (cmp_conr.getKind() == kind::EQUAL)
+    {
+      TNode n;
+      if (cmp_conr[0] == empty)
+      {
+        n = cmp_conr[1];
+      }
+      else if (cmp_conr[1] == empty)
+      {
+        n = cmp_conr[0];
+      }
+
+      if (!n.isNull())
+      {
+        emptyNodes.insert(n);
+        if (std::find(children0.begin(), children0.end(), n) == children0.end())
+        {
+          nodesToKeep.push_back(n);
+        }
+      }
+    }
+    else
+    {
+      for (const Node& c : cmp_conr)
+      {
+        TNode n;
+        if (c[0] == empty)
+        {
+          n = c[1];
+        }
+        else if (c[1] == empty)
+        {
+          n = c[0];
+        }
+
+        if (!n.isNull())
+        {
+          emptyNodes.insert(n);
+          if (std::find(children0.begin(), children0.end(), n)
+              == children0.end())
+          {
+            nodesToKeep.push_back(n);
+          }
+        }
+      }
+    }
+
+    if (emptyNodes.size() > 0)
+    {
+      std::vector<TNode> substs(emptyNodes.size(), TNode(empty));
+      Node nn2 = node[2].substitute(
+          emptyNodes.begin(), emptyNodes.end(), substs.begin(), substs.end());
+
+      std::vector<Node> nn1s;
+      for (const Node& child1 : children1)
+      {
+        if (emptyNodes.find(child1) == emptyNodes.end())
+        {
+          nn1s.push_back(child1);
+        }
+      }
+
+      nn1s.insert(nn1s.end(), nodesToKeep.begin(), nodesToKeep.end());
+
+      Node res = nm->mkNode(kind::STRING_STRREPL,
+                            node[0],
+                            mkConcat(kind::STRING_CONCAT, nn1s),
+                            nn2);
+      return returnRewrite(node, res, "rpl-cnts-substs");
+    }
+  }
 
   if (cmp_conr != cmp_con)
   {
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index a764634f0..5039f7b92 100644
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -332,6 +332,8 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     Node c = d_nm->mkConst(::CVC4::String("C"));
     Node d = d_nm->mkConst(::CVC4::String("D"));
     Node x = d_nm->mkVar("x", strType);
+    Node y = d_nm->mkVar("y", strType);
+    Node z = d_nm->mkVar("z", strType);
 
     // (str.replace "A" (str.replace "B", x, "C") "D") --> "A"
     Node repl_repl = d_nm->mkNode(kind::STRING_STRREPL,
@@ -348,12 +350,46 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
                              d);
     res_repl_repl = Rewriter::rewrite(repl_repl);
     TS_ASSERT_DIFFERS(res_repl_repl, a);
+
+    // Same normal form for:
+    //
+    // (str.replace (str.++ x y) (str.++ y x y x z) "D")
+    //
+    // (str.replace (str.++ x y) (str.++ y y x x z) "D")
+    Node xy = d_nm->mkNode(kind::STRING_CONCAT, x, y);
+    Node repl_xy_yxyxz =
+        d_nm->mkNode(kind::STRING_STRREPL,
+                     xy,
+                     d_nm->mkNode(kind::STRING_CONCAT, y, x, y, x, z),
+                     d);
+    Node repl_xy_yyxxz =
+        d_nm->mkNode(kind::STRING_STRREPL,
+                     xy,
+                     d_nm->mkNode(kind::STRING_CONCAT, y, y, x, x, z),
+                     d);
+    Node res_repl_xy_yxyxz = Rewriter::rewrite(repl_xy_yxyxz);
+    Node res_repl_xy_yyxxz = Rewriter::rewrite(repl_xy_yyxxz);
+    TS_ASSERT_EQUALS(res_repl_xy_yxyxz, res_repl_xy_yyxxz);
+
+    // Same normal form for:
+    //
+    // (str.replace x (str.++ x y z) y)
+    //
+    // (str.replace x (str.++ z y x) z)
+    Node repl_x_xyz = d_nm->mkNode(
+        kind::STRING_STRREPL, x, d_nm->mkNode(kind::STRING_CONCAT, x, y, z), y);
+    Node repl_x_zyx = d_nm->mkNode(
+        kind::STRING_STRREPL, x, d_nm->mkNode(kind::STRING_CONCAT, z, y, x), z);
+    Node res_repl_x_xyz = Rewriter::rewrite(repl_x_xyz);
+    Node res_repl_x_zyx = Rewriter::rewrite(repl_x_zyx);
+    TS_ASSERT_EQUALS(res_repl_x_xyz, res_repl_x_zyx);
   }
 
   void testRewriteContains()
   {
     TypeNode strType = d_nm->stringType();
 
+    Node empty = d_nm->mkConst(::CVC4::String(""));
     Node a = d_nm->mkConst(::CVC4::String("A"));
     Node b = d_nm->mkConst(::CVC4::String("B"));
     Node c = d_nm->mkConst(::CVC4::String("C"));
@@ -416,5 +452,29 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
                                   d_nm->mkNode(kind::STRING_STRREPL, b, x, c)));
     Node res_ctn_repl = Rewriter::rewrite(ctn_repl);
     TS_ASSERT_EQUALS(res_ctn_repl, f);
+
+    // (str.contains x (str.++ x x)) --> (= x "")
+    Node x_cnts_x_x = d_nm->mkNode(
+        kind::STRING_STRCTN, x, d_nm->mkNode(kind::STRING_CONCAT, x, x));
+    Node res_x_cnts_x_x = Rewriter::rewrite(x_cnts_x_x);
+    Node res_x_eq_empty =
+        Rewriter::rewrite(d_nm->mkNode(kind::EQUAL, x, empty));
+    TS_ASSERT_EQUALS(res_x_cnts_x_x, res_x_eq_empty);
+
+    // Same normal form for:
+    //
+    // (str.contains (str.++ y x) (str.++ x z y))
+    //
+    // (and (str.contains (str.++ y x) (str.++ x y)) (= z ""))
+    Node yx = d_nm->mkNode(kind::STRING_CONCAT, y, x);
+    Node yx_cnts_xzy = d_nm->mkNode(
+        kind::STRING_STRCTN, yx, d_nm->mkNode(kind::STRING_CONCAT, x, z, y));
+    Node res_yx_cnts_xzy = Rewriter::rewrite(yx_cnts_xzy);
+    Node xy = d_nm->mkNode(kind::STRING_CONCAT, x, y);
+    Node yx_cnts_xy = d_nm->mkNode(kind::AND,
+                                   d_nm->mkNode(kind::STRING_STRCTN, yx, xy),
+                                   d_nm->mkNode(kind::EQUAL, z, empty));
+    Node res_yx_cnts_xy = Rewriter::rewrite(yx_cnts_xy);
+    TS_ASSERT_EQUALS(res_yx_cnts_xzy, res_yx_cnts_xy);
   }
 };