diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-12-04 16:20:02 -0800 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-12-04 16:20:02 -0800 |
| commit | ab526dfb6ef1bdeedea2f2ed002a61fc5de4d743 (patch) | |
| tree | 0e62e1187f871b8bf149525b55416f2c3ea414db | |
| parent | 764b32922bdabbbe7197c8ac0f8a6dd2b5643f17 (diff) | |
| -rw-r--r-- | src/theory/strings/skolem_cache.cpp | 6 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 3 |
2 files changed, 3 insertions, 6 deletions
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index 40ac5eaba..ebd15e88c 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -130,17 +130,15 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b) Node m = a[2]; if (n == d_zero) { - if (m.getKind() == kind::STRING_STRIDOF && m[0] == s) + if (m.getKind() == kind::STRING_STRIDOF && m[0] == s && m[2] == d_zero) { - if (n == d_zero && m[2] == d_zero) - { id = SK_FIRST_CTN_PRE; a = m[0]; b = m[1]; - } } else { id = SK_PREFIX; a = s; + // b = Rewriter::rewrite(nm->mkNode(MINUS, m, nm->mkConst(Rational(1)))); b = m; } } diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 0780d8b0e..d095d6801 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -84,9 +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(NOT, skt.eqNode(nm->mkConst(String("")))); - 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); |