From ab526dfb6ef1bdeedea2f2ed002a61fc5de4d743 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 4 Dec 2018 16:20:02 -0800 Subject: nit --- src/theory/strings/skolem_cache.cpp | 6 ++---- 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); -- cgit v1.2.3