summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/strings/skolem_cache.cpp20
-rw-r--r--src/theory/strings/skolem_cache.h3
-rw-r--r--src/theory/strings/theory_strings.cpp95
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;
}
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback