diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-08 11:32:43 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-08 17:32:43 +0000 |
commit | 4395b6d728d2a25bff3a56801f7218d79834f423 (patch) | |
tree | 09effe93f7cc5d115b4975692bc2bd450d7ca073 /src | |
parent | b536a5fefb654439d6a0dee65b91ece12419fc0b (diff) |
(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.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/strings/skolem_cache.cpp | 20 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 3 |
2 files changed, 15 insertions, 8 deletions
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index b68eb4a04..3c47b8f28 100644 --- 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 f0afe5f26..eb897b2e5 100644 --- 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 |