From 556e63d784d0754a2fa31a588f98abef76365ab0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 7 Oct 2021 04:41:01 -0500 Subject: [PATCH] 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. --- src/theory/strings/sequences_rewriter.cpp | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) 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++) -- 2.30.2