Try a bit harder on the EQ_NCTN rewrite rule (#7998)

This makes a small change to the sequence rewriter to work a bit harder
on one of the rewrite rule. This fixes some performance issues we've
observed.

Signed-off-by: Bruno Dutertre <dutebrun@amazon.com>

diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index e4db2f325371ad4e4746444d7d74d6c84cd9861b..bbe25b7a38128e9593ba8c62bf877ba58e4b3956 100644 (file)
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -114,8 +114,15 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
   {
     // must call rewrite contains directly to avoid infinite loop
     Node ctn = nm->mkNode(STRING_CONTAINS, node[r], node[1 - r]);
+    Node prev = ctn;
     ctn = rewriteContains(ctn);
     Assert(!ctn.isNull());
+    if (ctn != prev && ctn.getKind() == STRING_CONTAINS)
+    {
+      prev = ctn;
+      ctn = rewriteContains(ctn);
+      Assert(!ctn.isNull());
+    }
     if (ctn.isConst())
     {
       if (!ctn.getConst<bool>())