From 17870b43a8f84340003e3473823930364abfe456 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Sat, 15 Dec 2018 00:39:02 -0800 Subject: minor --- src/theory/strings/skolem_cache.cpp | 8 +-- src/theory/strings/skolem_cache.h | 3 +- src/theory/strings/theory_strings.cpp | 111 +++++++++------------------------- 3 files changed, 30 insertions(+), 92 deletions(-) diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index 24109c980..7fb452182 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -126,13 +126,7 @@ 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) { + 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))); } diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h index b1dc48f75..2cd03bfe6 100644 --- a/src/theory/strings/skolem_cache.h +++ b/src/theory/strings/skolem_cache.h @@ -68,8 +68,7 @@ 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_X, - SK_ID_V_SPT_Y, + SK_ID_V_SPT, 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 b8e960f7b..416391fa2 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -3148,20 +3148,10 @@ void TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal isRev ? SkolemCache::SK_ID_C_SPT_REV : SkolemCache::SK_ID_C_SPT, "c_spt"); - Node lem = other_str.eqNode( isRev ? mkConcat( sk, prea ) : mkConcat(prea, sk) );; - if (false && !isRev && d_sk_cache.d_preSkolems.find(Node(other_str)) != d_sk_cache.d_preSkolems.end()) { - Node aa, bb; - std::tie(aa, bb) = d_sk_cache.d_preSkolems.find(other_str)->second; - if (bb == NodeManager::currentNM()->mkConst(strb)) { - lem = other_str.eqNode(prea); // other_str.eqNode(mkConcat(prea, NodeManager::currentNM()->mkConst(String("")))); - sk = Node::null(); - } - } - Trace("strings-csp") << "Const Split: " << other_str << " " << prea << " is removed from " << stra << " due to " << strb << ", p=" << p << std::endl; + Trace("strings-csp") << "Const Split: " << prea << " is removed from " << stra << " due to " << strb << ", p=" << p << std::endl; //set info - info.d_conc = lem; - if (!sk.isNull()) - info.d_new_skolem[LENGTH_SPLIT].push_back(sk); + info.d_conc = other_str.eqNode( isRev ? mkConcat( sk, prea ) : mkConcat(prea, sk) ); + info.d_new_skolem[LENGTH_SPLIT].push_back(sk); info.d_id = INFER_SSPLIT_CST_PROP; info_valid = true; } @@ -3254,78 +3244,33 @@ void TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal info.d_antn.push_back( xgtz ); } } - 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{ - 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; + 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 ); }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; + 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; } } } -- cgit v1.2.3