diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-11-28 12:33:55 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-11-28 12:33:55 -0800 |
commit | eef3d0d658aed64e8014c28eae5841eed298139a (patch) | |
tree | 7cf4a78c9f8d056c43fb9a8395edabe4787035c2 /src | |
parent | e194e29c76f30ab9f0b42d20af699f132ef82fe4 (diff) |
Improve skolem caching by normalizing skolem args (#2723)
In certain cases, we can share skolems between similar reductions, e.g.
`(str.replace x y z)` and `(str.replace (str.substr x 0 n) y z)` because the
first occurrence of `y` in `x` has to be the first occurrence
of `y` in `(str.substr x 0 n)` (assuming that `y` appears in both, otherwise the value of
the skolems does not matter). This commit adds a helper function in the
skolem cache that does some of those simplifications.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/strings/skolem_cache.cpp | 49 | ||||
-rw-r--r-- | src/theory/strings/skolem_cache.h | 22 |
2 files changed, 70 insertions, 1 deletions
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index 7725b1b0d..b6604d6e0 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -15,6 +15,8 @@ #include "theory/strings/skolem_cache.h" #include "theory/rewriter.h" +#include "theory/strings/theory_strings_rewriter.h" +#include "util/rational.h" namespace CVC4 { namespace theory { @@ -22,7 +24,9 @@ namespace strings { SkolemCache::SkolemCache() { - d_strType = NodeManager::currentNM()->stringType(); + NodeManager* nm = NodeManager::currentNM(); + d_strType = nm->stringType(); + d_zero = nm->mkConst(Rational(0)); } Node SkolemCache::mkSkolemCached(Node a, Node b, SkolemId id, const char* c) @@ -40,6 +44,12 @@ Node SkolemCache::mkTypedSkolemCached( { a = a.isNull() ? a : Rewriter::rewrite(a); b = b.isNull() ? b : Rewriter::rewrite(b); + + if (tn == d_strType) + { + std::tie(id, a, b) = normalizeStringSkolem(id, a, b); + } + std::map<SkolemId, Node>::iterator it = d_skolemCache[a][b].find(id); if (it == d_skolemCache[a][b].end()) { @@ -74,6 +84,43 @@ bool SkolemCache::isSkolem(Node n) const return d_allSkolems.find(n) != d_allSkolems.end(); } +std::tuple<SkolemCache::SkolemId, Node, Node> +SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b) +{ + Trace("skolem-cache") << "normalizeStringSkolem start: (" << id << ", " << a + << ", " << b << ")" << std::endl; + + // 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) + { + Node s = a[0]; + Node n = a[1]; + Node m = a[2]; + if (m.getKind() == kind::STRING_STRIDOF && m[0] == s) + { + if (n == d_zero && m[2] == d_zero) + { + id = SK_FIRST_CTN_PRE; + a = m[0]; + b = m[1]; + } + } + } + + if (id == SK_FIRST_CTN_PRE) + { + // SK_FIRST_CTN_PRE((str.substr x 0 n), y) ---> SK_FIRST_CTN_PRE(x, y) + while (a.getKind() == kind::STRING_SUBSTR && a[1] == d_zero) + { + a = a[0]; + } + } + + Trace("skolem-cache") << "normalizeStringSkolem end: (" << id << ", " << a + << ", " << b << ")" << std::endl; + return std::make_tuple(id, a, b); +} + } // namespace strings } // namespace theory } // namespace CVC4 diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h index d0eabd4c2..a6e91a246 100644 --- a/src/theory/strings/skolem_cache.h +++ b/src/theory/strings/skolem_cache.h @@ -18,7 +18,9 @@ #define __CVC4__THEORY__STRINGS__SKOLEM_CACHE_H #include <map> +#include <tuple> #include <unordered_set> + #include "expr/node.h" namespace CVC4 { @@ -134,8 +136,28 @@ class SkolemCache bool isSkolem(Node n) const; private: + /** + * Simplifies the arguments for a string skolem used for indexing into the + * cache. In certain cases, we can share skolems with similar arguments e.g. + * SK_FIRST_CTN(a, c) can be used instead of SK_FIRST_CTN((str.substr a 0 n), + * c) because the first occurrence of "c" in "(str.substr a 0 n)" is also the + * first occurrence of "c" in "a" (assuming that "c" appears in both and + * otherwise the value of SK_FIRST_CTN does not matter). + * + * @param id The type of skolem + * @param a The first argument used for indexing + * @param b The second argument used for indexing + * @return A tuple with the new skolem id, the new first, and the new second + * argument + */ + std::tuple<SkolemId, Node, Node> normalizeStringSkolem(SkolemId id, + Node a, + Node b); + /** string type */ TypeNode d_strType; + /** Constant node zero */ + Node d_zero; /** map from node pairs and identifiers to skolems */ std::map<Node, std::map<Node, std::map<SkolemId, Node> > > d_skolemCache; /** the set of all skolems we have generated */ |