From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 7 Oct 2021 09:41:01 +0000 (-0500)
Subject: Fast exit for string extended equality rewriter (#7312)
X-Git-Tag: cvc5-1.0.0~1112
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=556e63d784d0754a2fa31a588f98abef76365ab0;p=cvc5.git

Fast exit for string extended equality rewriter (#7312)

In benchmarks with many string equalities between variables and constants, a significant portion of the run time is spent on extended equality rewriting. This adds a fast exit when the equality is between variable/constants only.
---

diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 76175a32f..9887e7ef0 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -91,6 +91,22 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
   Assert(node.getKind() == EQUAL && node[0].getType().isStringLike());
   TypeNode stype = node[0].getType();
 
+  bool hasStrTerm = false;
+  for (size_t r = 0; r < 2; r++)
+  {
+    if (!node[r].isConst()
+        && kindToTheoryId(node[r].getKind()) == THEORY_STRINGS)
+    {
+      hasStrTerm = true;
+      break;
+    }
+  }
+  if (!hasStrTerm)
+  {
+    // equality between variables and constants, no rewrites apply
+    return node;
+  }
+
   NodeManager* nm = NodeManager::currentNM();
   // ( ~contains( s, t ) V ~contains( t, s ) ) => ( s == t ---> false )
   for (unsigned r = 0; r < 2; r++)