summaryrefslogtreecommitdiff
path: root/src/theory/strings/skolem_cache.cpp
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2018-11-28 12:33:55 -0800
committerGitHub <noreply@github.com>2018-11-28 12:33:55 -0800
commiteef3d0d658aed64e8014c28eae5841eed298139a (patch)
tree7cf4a78c9f8d056c43fb9a8395edabe4787035c2 /src/theory/strings/skolem_cache.cpp
parente194e29c76f30ab9f0b42d20af699f132ef82fe4 (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/theory/strings/skolem_cache.cpp')
-rw-r--r--src/theory/strings/skolem_cache.cpp49
1 files changed, 48 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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback