From 17c748fdbfd281d0031ac7de9e4b855fdb4827a3 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 29 Nov 2018 14:01:35 -0800 Subject: Rewrite SK_FIRST_CTN_POST to SK_SUFFIX_REM skolem --- src/theory/strings/skolem_cache.cpp | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index b6604d6e0..7cc3e3fe5 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -18,6 +18,8 @@ #include "theory/strings/theory_strings_rewriter.h" #include "util/rational.h" +using namespace CVC4::kind; + namespace CVC4 { namespace theory { namespace strings { @@ -90,6 +92,18 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b) Trace("skolem-cache") << "normalizeStringSkolem start: (" << id << ", " << a << ", " << b << ")" << std::endl; + NodeManager* nm = NodeManager::currentNM(); + + if (id == SK_FIRST_CTN_POST) + { + // SK_FIRST_CTN_POST(x, y) ---> + // SK_SUFFIX_REM(x, (+ (str.len SK_FIRST_CTN_PRE(x, y)) (str.len y))) + 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))); + } + // SK_PURIFY(str.substr x 0 (str.indexof x y 0)) ---> SK_FIRST_CTN_PRE(x, y) if (id == SK_PURIFY && a.getKind() == kind::STRING_SUBSTR) { -- cgit v1.2.3