diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-11-29 13:21:31 -0800 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-11-29 13:21:31 -0800 |
| commit | 78e698f44d426d51e5139d2e6724b07203ef5914 (patch) | |
| tree | 5c5ff51c9c2a2f3715a91118104a7baa32198093 /src/theory/strings/skolem_cache.cpp | |
| parent | 362201ae4b3d7ba0c035ff4ac698c555023b76b3 (diff) | |
Diffstat (limited to 'src/theory/strings/skolem_cache.cpp')
| -rw-r--r-- | src/theory/strings/skolem_cache.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index ebd6875eb..1e1b8cc72 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -94,6 +94,12 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b) NodeManager* nm = NodeManager::currentNM(); + if (id == SK_FIRST_CTN_POST) { + id = SK_SUFFIX_REM; + Node pre = mkSkolemCached(a, b, SK_FIRST_CTN_PRE, "pre"); + b = Rewriter::rewrite(nm->mkNode(PLUS, nm->mkNode(STRING_LENGTH, pre), nm->mkNode(STRING_LENGTH, b))); + } + if (id == SK_PURIFY && a.getKind() == kind::STRING_SUBSTR) { Node s = a[0]; |