diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-12-15 00:39:02 -0800 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-12-15 00:39:02 -0800 |
| commit | 17870b43a8f84340003e3473823930364abfe456 (patch) | |
| tree | 85b48f981c6f1b2d0c9273dcc9da42e32e10f1f9 /src/theory/strings/skolem_cache.cpp | |
| parent | 34fc320ad434aacc97e75f6b64f78a1810bbcc3e (diff) | |
minoraggSkolemSharingAlt
Diffstat (limited to 'src/theory/strings/skolem_cache.cpp')
| -rw-r--r-- | src/theory/strings/skolem_cache.cpp | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index 24109c980..7fb452182 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -126,13 +126,7 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b) PLUS, nm->mkNode(STRING_LENGTH, pre), nm->mkNode(STRING_LENGTH, b))); } - if (id == SK_ID_V_SPT_X) { - id = SK_SUFFIX_REM; - b = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, b)); - } else if (id == SK_ID_V_SPT_Y) { - id = SK_SUFFIX_REM; - b = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, b)); - } else if (id == SK_ID_V_SPT_REV) { + if (id == SK_ID_V_SPT_REV) { id = SK_PREFIX; b = Rewriter::rewrite(nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, a), nm->mkNode(STRING_LENGTH, b))); } |