contdreverseSkolemMap

1 files 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