From 44068c5fac9ffb0e9d9ce4bbb1035614a212b557 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 24 Jan 2020 12:35:31 -0800 Subject: Revert "Fix" This reverts commit c3b24d9aa9d7dc80f870fb578e0a27176341fadc. --- src/theory/strings/skolem_cache.cpp | 37 +++++++++++++------------- src/theory/strings/skolem_cache.h | 15 +++++------ src/theory/strings/theory_strings.cpp | 17 ++++++------ src/theory/strings/theory_strings_rewriter.cpp | 8 ------ 4 files changed, 34 insertions(+), 43 deletions(-) diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index bdfdeb7cd..1b2b93747 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -33,23 +33,23 @@ SkolemCache::SkolemCache() d_zero = nm->mkConst(Rational(0)); } -Node SkolemCache::mkSkolemCached(Node a, Node b, Node c, SkolemId id, const char* name, LengthStatus ls) +Node SkolemCache::mkSkolemCached(Node a, Node b, Node c, SkolemId id, const char* name) { - return mkTypedSkolemCached(d_strType, a, b, c, id, name, ls); + return mkTypedSkolemCached(d_strType, a, b, c, id, name); } -Node SkolemCache::mkSkolemCached(Node a, Node b, SkolemId id, const char* name, LengthStatus ls) +Node SkolemCache::mkSkolemCached(Node a, Node b, SkolemId id, const char* name) { - return mkTypedSkolemCached(d_strType, a, b, Node::null(), id, name, ls); + return mkTypedSkolemCached(d_strType, a, b, Node::null(), id, name); } -Node SkolemCache::mkSkolemCached(Node a, SkolemId id, const char* name, LengthStatus ls) +Node SkolemCache::mkSkolemCached(Node a, SkolemId id, const char* name) { - return mkSkolemCached(a, Node::null(), Node::null(), id, name, ls); + return mkSkolemCached(a, Node::null(), Node::null(), id, name); } Node SkolemCache::mkTypedSkolemCached( - TypeNode tn, Node a, Node b, Node c, SkolemId id, const char* name, LengthStatus ls) + 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); @@ -60,7 +60,7 @@ Node SkolemCache::mkTypedSkolemCached( std::tie(id, a, b, c) = normalizeStringSkolem(id, a, b, c); } - std::tuple args = std::make_tuple(a, b, c, id, ls); + std::tuple args = std::make_tuple(a, b, c, id); const auto& it = d_skolemCache.find(args); if (it == d_skolemCache.end()) { @@ -70,42 +70,41 @@ Node SkolemCache::mkTypedSkolemCached( { Node da = depurify(a); Node db = depurify(b); - Node na = Rewriter::rewrite(nm->mkNode(STRING_SUBSTR, da, d_zero, db)); sk = mkSkolemCached( - na, + Rewriter::rewrite(nm->mkNode(STRING_SUBSTR, da, d_zero, db)), SK_PURIFY, - name, ls); + "pur"); } else if (options::skolemDepurification() && id == SK_SUFFIX_REM) { Node da = depurify(a); Node db = depurify(b); - Node na = Rewriter::rewrite(nm->mkNode(STRING_SUBSTR, + sk = mkSkolemCached( + Rewriter::rewrite( + nm->mkNode(STRING_SUBSTR, da, db, - nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, da), db))); - sk = mkSkolemCached(na, + nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, da), db))), SK_PURIFY, - name, ls); + "pur"); } else { sk = mkTypedSkolem(tn, name); - d_skolemToArgs[sk] = args; } d_skolemCache[args] = sk; + d_skolemToArgs[sk] = args; return sk; } return it->second; } - Node SkolemCache::mkTypedSkolemCached(TypeNode tn, Node a, SkolemId id, - const char* name, LengthStatus ls) + const char* name) { - return mkTypedSkolemCached(tn, a, Node::null(), Node::null(), id, name, ls); + return mkTypedSkolemCached(tn, a, Node::null(), Node::null(), id, name); } Node SkolemCache::mkSkolem(const char* name) diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h index 4ccd56bee..1085ab43c 100644 --- a/src/theory/strings/skolem_cache.h +++ b/src/theory/strings/skolem_cache.h @@ -22,7 +22,6 @@ #include #include "expr/node.h" -#include "theory/strings/infer_info.h" namespace CVC4 { namespace theory { @@ -135,22 +134,22 @@ class SkolemCache * Returns a skolem of type string that is cached for (a,b,id) and has * name `name`. */ - Node mkSkolemCached(Node a, Node b, Node c, SkolemId id, const char* name, LengthStatus ls = LENGTH_SPLIT); + 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* name, LengthStatus ls = LENGTH_SPLIT); + 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 `name`. */ - Node mkSkolemCached(Node a, SkolemId id, const char* name, LengthStatus ls = LENGTH_SPLIT); + 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, Node c, SkolemId id, const char* name, LengthStatus ls = LENGTH_SPLIT); + 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* name, LengthStatus ls = LENGTH_SPLIT); + 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 */ @@ -185,9 +184,9 @@ class SkolemCache /** Constant node zero */ Node d_zero; /** map from node pairs and identifiers to skolems */ - std::map, Node> d_skolemCache; + std::map, Node> d_skolemCache; - std::map> d_skolemToArgs; + std::map> d_skolemToArgs; /** the set of all skolems we have generated */ std::unordered_set d_allSkolems; }; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 73aa752bc..5015207f1 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -3299,7 +3299,8 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi, prea, isRev ? SkolemCache::SK_ID_C_SPT_REV : SkolemCache::SK_ID_C_SPT, - "c_spt", LENGTH_GEQ_ONE); + "c_spt"); + Trace("strings-csp") << "Const Split: " << prea << " is removed from " << stra << " due to " << strb << ", p=" << p << std::endl; //set info info.d_conc = nm->mkNode(OR, other_str.eqNode(prea), other_str.eqNode( isRev ? utils::mkNConcat(sk, prea) @@ -3347,7 +3348,7 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi, other_str, isRev ? SkolemCache::SK_ID_VC_SPT_REV : SkolemCache::SK_ID_VC_SPT, - "vc_spt", LENGTH_GEQ_ONE); + "vc_spt"); Trace("strings-csp") << "Const Split: " << firstChar << " is removed from " << const_str << " (serial) " << std::endl; info.d_conc = nm->mkNode(OR, other_str.eqNode(firstChar), other_str.eqNode( isRev ? utils::mkNConcat(sk, firstChar) @@ -3401,13 +3402,13 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi, nfjv[index], isRev ? SkolemCache::SK_ID_V_SPT_REV_X : SkolemCache::SK_ID_V_SPT_X, - "v_spt_x", LENGTH_GEQ_ONE); + "v_spt_x"); Node sk2 = d_sk_cache.mkSkolemCached( nfiv[index], nfjv[index], isRev ? SkolemCache::SK_ID_V_SPT_REV_Y : SkolemCache::SK_ID_V_SPT_Y, - "v_spt_y", LENGTH_GEQ_ONE); + "v_spt_y"); // must add length requirement info.d_new_skolem[LENGTH_GEQ_ONE].push_back(sk1); info.d_new_skolem[LENGTH_GEQ_ONE].push_back(sk2); @@ -3763,12 +3764,12 @@ void TheoryStrings::processDeq( Node ni, Node nj ) { else { Node sk = d_sk_cache.mkSkolemCached( - nconst_k, SkolemCache::SK_ID_DC_SPT, "dc_spt", LENGTH_ONE); + nconst_k, SkolemCache::SK_ID_DC_SPT, "dc_spt"); d_im.registerLength(sk, LENGTH_ONE); Node skr = d_sk_cache.mkSkolemCached(nconst_k, SkolemCache::SK_ID_DC_SPT_REM, - "dc_spt_rem", LENGTH_GEQ_ONE); + "dc_spt_rem"); d_im.registerLength(skr, LENGTH_GEQ_ONE); Node eq1 = nconst_k.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk, skr ) ); eq1 = Rewriter::rewrite( eq1 ); @@ -3809,9 +3810,9 @@ void TheoryStrings::processDeq( Node ni, Node nj ) { Node sk2 = d_sk_cache.mkSkolemCached( i, j, SkolemCache::SK_ID_DEQ_Y, "y_dsplit"); Node sk3 = d_sk_cache.mkSkolemCached( - i, j, SkolemCache::SK_ID_DEQ_Z, "z_dsplit", LENGTH_GEQ_ONE); + i, j, SkolemCache::SK_ID_DEQ_Z, "z_dsplit"); Node sk4 = d_sk_cache.mkSkolemCached( - i, j, SkolemCache::SK_ID_DEQ_W, "w_dsplit", LENGTH_GEQ_ONE); + i, j, SkolemCache::SK_ID_DEQ_W, "w_dsplit"); d_im.registerLength(sk3, LENGTH_GEQ_ONE); d_im.registerLength(sk4, LENGTH_GEQ_ONE); //Node nemp = sk3.eqNode(d_emptyString).negate(); diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index e14180e8f..f17944027 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1836,14 +1836,6 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node) return returnRewrite(node, ret, "ss-len-non-pos"); } - if (node[1].getKind() == STRING_LENGTH - && node[1][0].getKind() == STRING_SUBSTR && node[1][0][0] == node[0] - && node[1][0][1] == zero && checkEntailArith(node[1][0][2])) - { - Node ret = nm->mkNode(STRING_SUBSTR, node[0], node[1][0][2], node[2]); - return returnRewrite(node, ret, "ss-len-substr"); - } - if (node[0].getKind() == STRING_SUBSTR) { // (str.substr (str.substr x a b) c d) ---> "" if c >= b -- cgit v1.2.3