diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-11-29 14:01:35 -0800 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-11-29 14:01:35 -0800 |
| commit | 17c748fdbfd281d0031ac7de9e4b855fdb4827a3 (patch) | |
| tree | 1b01d77f624780ee05fdeccf26594d8fa4821d37 | |
| parent | 41b38de8b059d346764cd5ca112740aa09e1d163 (diff) | |
Rewrite SK_FIRST_CTN_POST to SK_SUFFIX_REM skolem
| -rw-r--r-- | src/theory/strings/skolem_cache.cpp | 14 |
1 files changed, 14 insertions, 0 deletions
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) { |