diff options
Diffstat (limited to 'src/theory/strings/skolem_cache.cpp')
| -rw-r--r-- | src/theory/strings/skolem_cache.cpp | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index cce4074ee..24109c980 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -126,6 +126,17 @@ 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) { + id = SK_PREFIX; + b = Rewriter::rewrite(nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, a), nm->mkNode(STRING_LENGTH, b))); + } + if (id == SK_ID_C_SPT) { id = SK_SUFFIX_REM; b = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, b)); @@ -136,6 +147,15 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b) b = nm->mkConst(Rational(1)); } + if (id == SK_ID_DC_SPT) { + id = SK_PREFIX; + b = nm->mkConst(Rational(1)); + } + if (id == SK_ID_DC_SPT_REM) { + id = SK_SUFFIX_REM; + b = nm->mkConst(Rational(1)); + } + if (id == SK_ID_DEQ_Y) { id = SK_PREFIX; b = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, b)); |