summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/strings/skolem_cache.cpp49
-rw-r--r--src/theory/strings/skolem_cache.h22
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback