From: Bruno Dutertre <BrunoDutertre@users.noreply.github.com>
Date: Fri, 28 Jan 2022 20:33:10 +0000 (-0800)
Subject: Try a bit harder on the EQ_NCTN rewrite rule (#7998)
X-Git-Tag: cvc5-1.0.0~495
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b0d216c23bff2163be3f77dfc37f36af5f504686;p=cvc5.git

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 e4db2f325..bbe25b7a3 100644
--- 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>())