From 111351bea551ea1b73d73f8f583e913e27269151 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 17 Jan 2020 11:33:21 -0800 Subject: contd --- src/theory/strings/skolem_cache.cpp | 14 ++++---------- 1 file changed, 4 insertions(+), 10 deletions(-) diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index 2991737c4..f5430a91c 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -193,8 +193,6 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b) } else if (id == SK_SUFFIX_REM) { - std::cout << a << d_skolemToArgs[a].a << std::endl; - std::cout << b << std::endl; // SK_SUFFIX_REM(SK_SUFFIX_REM(a, b1), b2) ---> SK_SUFFIX_REM(a, (+ b1 b2)) while (d_skolemToArgs.find(a) != d_skolemToArgs.end() && d_skolemToArgs[a].id == SK_SUFFIX_REM) @@ -202,21 +200,17 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b) SkolemInfo info = d_skolemToArgs[a]; b = Rewriter::rewrite(nm->mkNode(PLUS, b, info.b)); a = info.a; - std::cout << a << std::endl; } } else if (id == SK_PREFIX) { - std::cout << "pfx" << a << d_skolemToArgs[a].a << std::endl; - std::cout << "pfx" << b << std::endl; // SK_PREFIX(SK_PREFIX(a, b1), b2) ---> SK_PREFIX(a, (+ b1 b2)) - /* - while (a.getKind() == kind::APPLY_UF - && a.getOperator() == d_skolemUfs[SK_PREFIX]) + while (d_skolemToArgs.find(a) != d_skolemToArgs.end() + && d_skolemToArgs[a].id == SK_PREFIX) { - a = a[0]; + SkolemInfo info = d_skolemToArgs[a]; + a = info.a; } - */ } Trace("skolem-cache") << "normalizeStringSkolem end: (" << id << ", " << a -- cgit v1.2.3