summaryrefslogtreecommitdiff
path: root/src/theory/strings
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings')
-rw-r--r--src/theory/strings/regexp_operation.cpp13
-rw-r--r--src/theory/strings/skolem_cache.cpp91
-rw-r--r--src/theory/strings/skolem_cache.h35
-rw-r--r--src/theory/strings/theory_strings_preprocess.cpp4
-rw-r--r--src/theory/strings/theory_strings_utils.cpp18
5 files changed, 122 insertions, 39 deletions
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 5d4131465..96a0dd55f 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -1101,18 +1101,27 @@ void RegExpOpr::simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes
break;
}
case kind::REGEXP_CONCAT: {
+ NodeManager* nm = NodeManager::currentNM();
std::vector< Node > nvec;
std::vector< Node > cc;
+ std::vector<Node> prefix;
+ std::vector<Node> suffix(r.begin(), r.end());
bool emptyflag = false;
for(unsigned i=0; i<r.getNumChildren(); ++i) {
+ prefix.emplace_back(r[i]);
+ suffix.erase(suffix.begin());
if(r[i].getKind() == kind::STRING_TO_REGEXP) {
cc.push_back( r[i][0] );
} else if(r[i].getKind() == kind::REGEXP_EMPTY) {
emptyflag = true;
break;
} else {
- Node sk = NodeManager::currentNM()->mkSkolem( "rc", s.getType(), "created for regular expression concat" );
- Node lem = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, sk, r[i]);
+ Node sk = d_sc->mkSkolemCached(s,
+ utils::mkConcat(REGEXP_CONCAT, prefix),
+ utils::mkConcat(REGEXP_CONCAT, suffix),
+ SkolemCache::SK_REGEXP_CONCAT,
+ "rc");
+ Node lem = nm->mkNode(kind::STRING_IN_REGEXP, sk, r[i]);
nvec.push_back(lem);
cc.push_back(sk);
}
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index 2c4deb429..6cf1606a8 100644
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -17,6 +17,7 @@
#include "options/strings_options.h"
#include "theory/rewriter.h"
#include "theory/strings/theory_strings_rewriter.h"
+#include "theory/strings/theory_strings_utils.h"
#include "util/rational.h"
using namespace CVC4::kind;
@@ -32,32 +33,38 @@ SkolemCache::SkolemCache()
d_zero = nm->mkConst(Rational(0));
}
-Node SkolemCache::mkSkolemCached(Node a, Node b, SkolemId id, const char* c)
+Node SkolemCache::mkSkolemCached(Node a, Node b, Node c, SkolemId id, const char* name)
{
- return mkTypedSkolemCached(d_strType, a, b, id, c);
+ return mkTypedSkolemCached(d_strType, a, b, c, id, name);
}
-Node SkolemCache::mkSkolemCached(Node a, SkolemId id, const char* c)
+Node SkolemCache::mkSkolemCached(Node a, Node b, SkolemId id, const char* name)
{
- return mkSkolemCached(a, Node::null(), id, c);
+ return mkTypedSkolemCached(d_strType, a, b, Node::null(), id, name);
+}
+
+Node SkolemCache::mkSkolemCached(Node a, SkolemId id, const char* name)
+{
+ return mkSkolemCached(a, Node::null(), Node::null(), id, name);
}
Node SkolemCache::mkTypedSkolemCached(
- TypeNode tn, Node a, Node b, SkolemId id, const char* c)
+ TypeNode tn, Node a, Node b, Node c, SkolemId id, const char* name)
{
a = a.isNull() ? a : Rewriter::rewrite(a);
b = b.isNull() ? b : Rewriter::rewrite(b);
+ c = c.isNull() ? c : Rewriter::rewrite(c);
if (options::skolemSharing() && tn == d_strType)
{
- std::tie(id, a, b) = normalizeStringSkolem(id, a, b);
+ std::tie(id, a, b, c) = normalizeStringSkolem(id, a, b, c);
}
- std::map<SkolemId, Node>::iterator it = d_skolemCache[a][b].find(id);
- if (it == d_skolemCache[a][b].end())
+ std::map<SkolemId, Node>::iterator it = d_skolemCache[a][b][c].find(id);
+ if (it == d_skolemCache[a][b][c].end())
{
- Node sk = mkTypedSkolem(tn, c);
- d_skolemCache[a][b][id] = sk;
+ Node sk = mkTypedSkolem(tn, name);
+ d_skolemCache[a][b][c][id] = sk;
return sk;
}
return it->second;
@@ -65,19 +72,19 @@ Node SkolemCache::mkTypedSkolemCached(
Node SkolemCache::mkTypedSkolemCached(TypeNode tn,
Node a,
SkolemId id,
- const char* c)
+ const char* name)
{
- return mkTypedSkolemCached(tn, a, Node::null(), id, c);
+ return mkTypedSkolemCached(tn, a, Node::null(), Node::null(), id, name);
}
-Node SkolemCache::mkSkolem(const char* c)
+Node SkolemCache::mkSkolem(const char* name)
{
- return mkTypedSkolem(d_strType, c);
+ return mkTypedSkolem(d_strType, name);
}
-Node SkolemCache::mkTypedSkolem(TypeNode tn, const char* c)
+Node SkolemCache::mkTypedSkolem(TypeNode tn, const char* name)
{
- Node n = NodeManager::currentNM()->mkSkolem(c, tn, "string skolem");
+ Node n = NodeManager::currentNM()->mkSkolem(name, tn, "string skolem");
d_allSkolems.insert(n);
return n;
}
@@ -87,8 +94,8 @@ 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)
+std::tuple<SkolemCache::SkolemId, Node, Node, Node>
+SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b, Node c)
{
Trace("skolem-cache") << "normalizeStringSkolem start: (" << id << ", " << a
<< ", " << b << ")" << std::endl;
@@ -103,6 +110,52 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b)
{
id = SK_FIRST_CTN_POST;
}
+ else if (id == SK_REGEXP_CONCAT)
+ {
+ Node curr = b.getKind() == REGEXP_CONCAT ? b[b.getNumChildren() - 1] : b;
+ Node len = TheoryStringsRewriter::getFixedLengthForRegexp(curr);
+ if (!len.isNull())
+ {
+ if (b.getKind() != REGEXP_CONCAT)
+ {
+ id = SK_PREFIX;
+ b = len;
+ c = Node::null();
+ }
+ else if (c.getKind() != REGEXP_CONCAT)
+ {
+ id = SK_SUFFIX_REM;
+ b = nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, a), len);
+ c = Node::null();
+ }
+ else
+ {
+ std::vector<Node> vprefix(b.begin(), b.end() - 1);
+ Node prefix = utils::mkConcat(REGEXP_CONCAT, vprefix);
+ Node plen = TheoryStringsRewriter::getFixedLengthForRegexp(prefix);
+ Node slen = TheoryStringsRewriter::getFixedLengthForRegexp(c);
+ if (!plen.isNull())
+ {
+ id = SK_SUFFIX_REM;
+ a = mkSkolemCached(a, nm->mkNode(PLUS, len, plen), SK_PREFIX, "pre");
+ b = plen;
+ c = Node::null();
+ }
+ else if (!slen.isNull())
+ {
+ id = SK_PREFIX;
+ a = mkSkolemCached(a,
+ nm->mkNode(MINUS,
+ nm->mkNode(STRING_LENGTH, a),
+ nm->mkNode(PLUS, slen, len)),
+ SK_SUFFIX_REM,
+ "suf");
+ b = plen;
+ c = Node::null();
+ }
+ }
+ }
+ }
if (id == SK_FIRST_CTN_POST)
{
@@ -289,7 +342,7 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b)
Trace("skolem-cache") << "normalizeStringSkolem end: (" << id << ", " << a
<< ", " << b << ")" << std::endl;
- return std::make_tuple(id, a, b);
+ return std::make_tuple(id, a, b, c);
}
} // namespace strings
diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h
index 8cc5146b3..08df744de 100644
--- a/src/theory/strings/skolem_cache.h
+++ b/src/theory/strings/skolem_cache.h
@@ -117,6 +117,8 @@ class SkolemCache
SK_STAR_MID,
SK_STAR_SUFFIX,
+ SK_REGEXP_CONCAT,
+
// --------------- integer skolems
// exists k. ( b occurs k times in a )
SK_NUM_OCCUR,
@@ -130,23 +132,28 @@ class SkolemCache
};
/**
* Returns a skolem of type string that is cached for (a,b,id) and has
- * name c.
+ * name `name`.
+ */
+ Node mkSkolemCached(Node a, Node b, Node c, SkolemId id, const char* name);
+ /**
+ * Returns a skolem of type string that is cached for (a,b,id) and has
+ * name `name`.
*/
- Node mkSkolemCached(Node a, Node b, SkolemId id, const char* c);
+ Node mkSkolemCached(Node a, Node b, SkolemId id, const char* name);
/**
* Returns a skolem of type string that is cached for (a,[null],id) and has
- * name c.
+ * name `name`.
*/
- Node mkSkolemCached(Node a, SkolemId id, const char* c);
+ Node mkSkolemCached(Node a, SkolemId id, const char* name);
/** Same as above, but the skolem to construct has a custom type tn */
Node mkTypedSkolemCached(
- TypeNode tn, Node a, Node b, SkolemId id, const char* c);
+ TypeNode tn, Node a, Node b, Node c, SkolemId id, const char* name);
/** Same as mkTypedSkolemCached above for (a,[null],id) */
- Node mkTypedSkolemCached(TypeNode tn, Node a, SkolemId id, const char* c);
- /** Returns a (uncached) skolem of type string with name c */
- Node mkSkolem(const char* c);
+ Node mkTypedSkolemCached(TypeNode tn, Node a, SkolemId id, const char* name);
+ /** Returns a (uncached) skolem of type string with name `name` */
+ Node mkSkolem(const char* name);
/** Same as above, but for custom type tn */
- Node mkTypedSkolem(TypeNode tn, const char* c);
+ Node mkTypedSkolem(TypeNode tn, const char* name);
/** Returns true if n is a skolem allocated by this class */
bool isSkolem(Node n) const;
@@ -165,16 +172,18 @@ class SkolemCache
* @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);
+ std::tuple<SkolemId, Node, Node, Node> normalizeStringSkolem(SkolemId id,
+ Node a,
+ Node b,
+ Node c);
/** 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;
+ std::map<Node, std::map<Node, std::map<Node, std::map<SkolemId, Node>>>>
+ d_skolemCache;
/** the set of all skolems we have generated */
std::unordered_set<Node, NodeHashFunction> d_allSkolems;
};
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index e59bc95e8..56fe3e084 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -416,14 +416,14 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
Node rpaw = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "rpaw");
Node numOcc = d_sc->mkTypedSkolemCached(
- nm->integerType(), x, y, SkolemCache::SK_NUM_OCCUR, "numOcc");
+ nm->integerType(), x, y, Node::null(), SkolemCache::SK_NUM_OCCUR, "numOcc");
std::vector<TypeNode> argTypes;
argTypes.push_back(nm->integerType());
Node us =
nm->mkSkolem("Us", nm->mkFunctionType(argTypes, nm->stringType()));
TypeNode ufType = nm->mkFunctionType(argTypes, nm->integerType());
Node uf = d_sc->mkTypedSkolemCached(
- ufType, x, y, SkolemCache::SK_OCCUR_INDEX, "Uf");
+ ufType, x, y, Node::null(), SkolemCache::SK_OCCUR_INDEX, "Uf");
Node ufno = nm->mkNode(APPLY_UF, uf, numOcc);
Node usno = nm->mkNode(APPLY_UF, us, numOcc);
diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index 03c2419c4..8d8db31cf 100644
--- a/src/theory/strings/theory_strings_utils.cpp
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -105,10 +105,22 @@ void getConcat(Node n, std::vector<Node>& c)
Node mkConcat(Kind k, const std::vector<Node>& c)
{
- Assert(!c.empty() || k == STRING_CONCAT);
+ Assert(!c.empty() || k == STRING_CONCAT || k == REGEXP_CONCAT);
NodeManager* nm = NodeManager::currentNM();
- return c.size() > 1 ? nm->mkNode(k, c)
- : (c.size() == 1 ? c[0] : nm->mkConst(String("")));
+ if (c.size() > 1)
+ {
+ return nm->mkNode(k, c);
+ }
+ else if (c.size() == 1)
+ {
+ return c[0];
+ }
+ else
+ {
+ return k == STRING_CONCAT
+ ? nm->mkConst(String(""))
+ : nm->mkNode(STRING_TO_REGEXP, nm->mkConst(String("")));
+ }
}
Node mkNConcat(Node n1, Node n2)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback