diff options
| -rw-r--r-- | src/theory/strings/skolem_cache.cpp | 6 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 7 |
2 files changed, 7 insertions, 6 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]; diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index e2a057e49..d095d6801 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -84,13 +84,8 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { nm->mkNode(GEQ, lt0, t12), nm->mkNode(MINUS, lt0, t12), d_zero)); - Node b14 = nm->mkNode(STRING_LENGTH, skt) - .eqNode(nm->mkNode(ITE, - nm->mkNode(GEQ, lt0, t12), - m, - nm->mkNode(MINUS, lt0, n))); - Node b1 = nm->mkNode(AND, b11, b12, b13, b14); + Node b1 = nm->mkNode(AND, b11, b12, b13); Node b2 = skt.eqNode(d_empty_str); Node lemma = nm->mkNode(ITE, cond, b1, b2); |