diff options
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 111 |
1 files changed, 28 insertions, 83 deletions
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; } } } |