diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-12-05 01:21:45 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-12-05 01:21:45 -0800 |
commit | 5bb74049b9ae776fe70e6f9a57dd85d1434147f1 (patch) | |
tree | 9e14dae777aa2fea7e656fe782b068bb9d1c7c45 | |
parent | 729ff5dcb63de155e24b1df1d05733b08fd99669 (diff) |
more aggressive
-rw-r--r-- | src/theory/strings/skolem_cache.cpp | 20 | ||||
-rw-r--r-- | src/theory/strings/skolem_cache.h | 3 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 95 |
3 files changed, 92 insertions, 26 deletions
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index cce4074ee..24109c980 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -126,6 +126,17 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b) PLUS, nm->mkNode(STRING_LENGTH, pre), nm->mkNode(STRING_LENGTH, b))); } + if (id == SK_ID_V_SPT_X) { + id = SK_SUFFIX_REM; + b = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, b)); + } else if (id == SK_ID_V_SPT_Y) { + id = SK_SUFFIX_REM; + b = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, b)); + } else if (id == SK_ID_V_SPT_REV) { + id = SK_PREFIX; + b = Rewriter::rewrite(nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, a), nm->mkNode(STRING_LENGTH, b))); + } + if (id == SK_ID_C_SPT) { id = SK_SUFFIX_REM; b = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, b)); @@ -136,6 +147,15 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b) b = nm->mkConst(Rational(1)); } + if (id == SK_ID_DC_SPT) { + id = SK_PREFIX; + b = nm->mkConst(Rational(1)); + } + if (id == SK_ID_DC_SPT_REM) { + id = SK_SUFFIX_REM; + b = nm->mkConst(Rational(1)); + } + if (id == SK_ID_DEQ_Y) { id = SK_PREFIX; b = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, b)); diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h index 2cd03bfe6..b1dc48f75 100644 --- a/src/theory/strings/skolem_cache.h +++ b/src/theory/strings/skolem_cache.h @@ -68,7 +68,8 @@ class SkolemCache SK_ID_VC_BIN_SPT_REV, // a != "" ^ b != "" ^ len(a)!=len(b) ^ a ++ a' = b ++ b' => // exists k. len( k )>0 ^ ( a ++ k = b OR a = b ++ k ) - SK_ID_V_SPT, + SK_ID_V_SPT_X, + SK_ID_V_SPT_Y, SK_ID_V_SPT_REV, // a != "" ^ b = "c" ^ a ++ a' != b ++ b' => // exists k, k_rem. diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index d01579b2e..6d0c6264b 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -3254,33 +3254,78 @@ void TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal info.d_antn.push_back( xgtz ); } } - Node sk = d_sk_cache.mkSkolemCached( - normal_forms[i][index], - normal_forms[j][index], - isRev ? SkolemCache::SK_ID_V_SPT_REV - : SkolemCache::SK_ID_V_SPT, - "v_spt"); - // must add length requirement - info.d_new_skolem[LENGTH_GEQ_ONE].push_back(sk); - Node eq1 = normal_forms[i][index].eqNode( isRev ? mkConcat(sk, normal_forms[j][index]) : mkConcat(normal_forms[j][index], sk) ); - Node eq2 = normal_forms[j][index].eqNode( isRev ? mkConcat(sk, normal_forms[i][index]) : mkConcat(normal_forms[i][index], sk) ); - - if( lentTestSuccess!=-1 ){ - info.d_antn.push_back( lentTestExp ); - info.d_conc = lentTestSuccess==0 ? eq1 : eq2; - info.d_id = INFER_SSPLIT_VAR_PROP; - info_valid = true; - }else{ - Node ldeq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ).negate(); - if( d_equalityEngine.areDisequal( length_term_i, length_term_j, true ) ){ - info.d_ant.push_back( ldeq ); + if (isRev) { + Node sk_x = d_sk_cache.mkSkolemCached( + normal_forms[i][index], + normal_forms[j][index], + SkolemCache::SK_ID_V_SPT_REV, + "v_sptx"); + Node sk_y = d_sk_cache.mkSkolemCached( + normal_forms[j][index], + normal_forms[i][index], + SkolemCache::SK_ID_V_SPT_REV, + "v_spty"); + // must add length requirement + if (lentTestSuccess == -1 || lentTestSuccess == 0) + info.d_new_skolem[LENGTH_GEQ_ONE].push_back(sk_x); + if (lentTestSuccess == -1 || lentTestSuccess != 0) + info.d_new_skolem[LENGTH_GEQ_ONE].push_back(sk_y); + Node eq1 = normal_forms[i][index].eqNode(mkConcat(sk_x, normal_forms[j][index])); + Node eq2 = normal_forms[j][index].eqNode(mkConcat(sk_y, normal_forms[i][index])); + + if( lentTestSuccess!=-1 ){ + info.d_antn.push_back( lentTestExp ); + info.d_conc = lentTestSuccess==0 ? eq1 : eq2; + info.d_id = INFER_SSPLIT_VAR_PROP; + info_valid = true; }else{ - info.d_antn.push_back(ldeq); + Node ldeq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ).negate(); + if( d_equalityEngine.areDisequal( length_term_i, length_term_j, true ) ){ + info.d_ant.push_back( ldeq ); + }else{ + info.d_antn.push_back(ldeq); + } + //set info + info.d_conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); + info.d_id = INFER_SSPLIT_VAR; + info_valid = true; + } + } else { + Node sk_x = d_sk_cache.mkSkolemCached( + normal_forms[i][index], + normal_forms[j][index], + SkolemCache::SK_ID_V_SPT_X, + "v_sptx"); + Node sk_y = d_sk_cache.mkSkolemCached( + normal_forms[j][index], + normal_forms[i][index], + SkolemCache::SK_ID_V_SPT_Y, + "v_spty"); + // must add length requirement + if (lentTestSuccess == -1 || lentTestSuccess == 0) + info.d_new_skolem[LENGTH_GEQ_ONE].push_back(sk_x); + if (lentTestSuccess == -1 || lentTestSuccess != 0) + info.d_new_skolem[LENGTH_GEQ_ONE].push_back(sk_y); + Node eq1 = normal_forms[i][index].eqNode(mkConcat(normal_forms[j][index], sk_x) ); + Node eq2 = normal_forms[j][index].eqNode(mkConcat(normal_forms[i][index], sk_y) ); + + if( lentTestSuccess!=-1 ){ + info.d_antn.push_back( lentTestExp ); + info.d_conc = lentTestSuccess==0 ? eq1 : eq2; + info.d_id = INFER_SSPLIT_VAR_PROP; + info_valid = true; + }else{ + Node ldeq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ).negate(); + if( d_equalityEngine.areDisequal( length_term_i, length_term_j, true ) ){ + info.d_ant.push_back( ldeq ); + }else{ + info.d_antn.push_back(ldeq); + } + //set info + info.d_conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); + info.d_id = INFER_SSPLIT_VAR; + info_valid = true; } - //set info - info.d_conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); - info.d_id = INFER_SSPLIT_VAR; - info_valid = true; } } } |