minoraggSkolemSharingAlt

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;
                 }
               }
             }