diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-07 04:41:01 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-10-07 09:41:01 +0000 |
commit | 556e63d784d0754a2fa31a588f98abef76365ab0 (patch) | |
tree | 9be0c1d145b1286b638c036936c102b4e6bb1551 /src/theory | |
parent | 1967722d29bf1f4811f52210c4da84091365f333 (diff) |
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.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/strings/sequences_rewriter.cpp | 16 |
1 files changed, 16 insertions, 0 deletions
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++) |