From 3e3883200b02e706da643f031172a798b055ddec Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 21 Jan 2020 23:06:39 -0800 Subject: Add regexp concat skolem --- src/theory/strings/regexp_operation.cpp | 13 +++- src/theory/strings/skolem_cache.cpp | 91 +++++++++++++++++++----- src/theory/strings/skolem_cache.h | 35 +++++---- src/theory/strings/theory_strings_preprocess.cpp | 4 +- src/theory/strings/theory_strings_utils.cpp | 18 ++++- 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 prefix; + std::vector suffix(r.begin(), r.end()); bool emptyflag = false; for(unsigned i=0; imkSkolem( "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::iterator it = d_skolemCache[a][b].find(id); - if (it == d_skolemCache[a][b].end()) + std::map::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::normalizeStringSkolem(SkolemId id, Node a, Node b) +std::tuple +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 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 normalizeStringSkolem(SkolemId id, - Node a, - Node b); + std::tuple 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 > > d_skolemCache; + std::map>>> + d_skolemCache; /** the set of all skolems we have generated */ std::unordered_set 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 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& c) Node mkConcat(Kind k, const std::vector& 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) -- cgit v1.2.3