(proof-new) Separating optimizations for strings skolem caching (#6064)

This PR ensures that several optimizations are not performed in the reference implementation of skolem sharing (d_useOpts=false). This is to ensure that the many of the rules in the strings proof checker do not depend on the rewriter.

These errors were caught by the LFSC proof checker.

diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index b68eb4a04d673aec00d37e58881588113109b54e..3c47b8f28aa354fc44ae655d3312fa810227f885 100644 (file)
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -62,9 +62,13 @@ Node SkolemCache::mkTypedSkolemCached(
   Trace("skolem-cache") << "mkTypedSkolemCached start: (" << id << ", " << a
                         << ", " << b << ")" << std::endl;
   SkolemId idOrig = id;
-  a = a.isNull() ? a : Rewriter::rewrite(a);
-  b = b.isNull() ? b : Rewriter::rewrite(b);
-
+  // do not rewrite beforehand if we are not using optimizations, this is so
+  // that the proof checker does not depend on the rewriter.
+  if (d_useOpts)
+  {
+    a = a.isNull() ? a : Rewriter::rewrite(a);
+    b = b.isNull() ? b : Rewriter::rewrite(b);
+  }
   std::tie(id, a, b) = normalizeStringSkolem(id, a, b);
 
   // optimization: if we aren't asking for the purification skolem for constant
@@ -79,6 +83,7 @@ Node SkolemCache::mkTypedSkolemCached(
   std::map<SkolemId, Node>::iterator it = d_skolemCache[a][b].find(id);
   if (it != d_skolemCache[a][b].end())
   {
+    Trace("skolem-cache") << "...return existing " << it->second << std::endl;
     // already cached
     return it->second;
   }
@@ -120,6 +125,7 @@ Node SkolemCache::mkTypedSkolemCached(
     }
     break;
   }
+  Trace("skolem-cache") << "...returned " << sk << std::endl;
   d_allSkolems.insert(sk);
   d_skolemCache[a][b][id] = sk;
   return sk;
@@ -265,9 +271,11 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b)
     b = Node::null();
   }
 
-  a = a.isNull() ? a : Rewriter::rewrite(a);
-  b = b.isNull() ? b : Rewriter::rewrite(b);
-
+  if (d_useOpts)
+  {
+    a = a.isNull() ? a : Rewriter::rewrite(a);
+    b = b.isNull() ? b : Rewriter::rewrite(b);
+  }
   Trace("skolem-cache") << "normalizeStringSkolem end: (" << id << ", " << a
                         << ", " << b << ")" << std::endl;
   return std::make_tuple(id, a, b);

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index f0afe5f260ff9a845d5e2356e6b8bfc9a4fe8d74..eb897b2e593eaa0f6508efe4b379c3c7754c9907 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -69,7 +69,6 @@ Node StringsPreprocess::reduce(Node t,
     Node m = t[2];
     Node skt = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "sst");
     Node t12 = nm->mkNode(PLUS, n, m);
-    t12 = Rewriter::rewrite(t12);
     Node lt0 = nm->mkNode(STRING_LENGTH, s);
     //start point is greater than or equal zero
     Node c1 = nm->mkNode(GEQ, n, zero);
@@ -101,7 +100,7 @@ Node StringsPreprocess::reduce(Node t,
     Node lemma = nm->mkNode(ITE, cond, b1, b2);
 
     // assert:
-    // IF    n >=0 AND n < len( s ) AND m > 0
+    // IF    n >=0 AND len( s ) > n AND m > 0
     // THEN: s = sk1 ++ skt ++ sk2 AND
     //       len( sk1 ) = n AND
     //       ( len( sk2 ) = len( s )-(n+m) OR len( sk2 ) = 0 ) AND