From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Tue, 6 May 2014 01:17:31 +0000 (-0500)
Subject: fix a bug in replace and contains
X-Git-Tag: cvc5-1.0.0~6929
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5254bf67589daeb387778cf9f392ddd8285b75cb;p=cvc5.git

fix a bug in replace and contains
---

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 0c20b12cd..4bb0711fe 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -2820,18 +2820,18 @@ bool TheoryStrings::checkNegContains() {
               std::vector< Node > vec_nodes;
               Node cc = NodeManager::currentNM()->mkNode( kind::GEQ, b2, d_zero );
               vec_nodes.push_back(cc);
-              cc = NodeManager::currentNM()->mkNode( kind::GEQ, lens, b2 );
+              cc = NodeManager::currentNM()->mkNode( kind::GT, lens, b2 );
               vec_nodes.push_back(cc);
 
               cc = s2.eqNode(s5).negate();
               vec_nodes.push_back(cc);
 
-              Node conc = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, vec_nodes) );
-              Node xlss = NodeManager::currentNM()->mkNode( kind::GT, lens, lenx );
-              conc = NodeManager::currentNM()->mkNode( kind::OR, xlss, conc );
+              Node conc = NodeManager::currentNM()->mkNode(kind::AND, vec_nodes);
               conc = NodeManager::currentNM()->mkNode( kind::EXISTS, b2v, conc );
               conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, g1, conc );
               conc = NodeManager::currentNM()->mkNode( kind::FORALL, b1v, conc );
+              Node xlss = NodeManager::currentNM()->mkNode( kind::GT, lens, lenx );
+              conc = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::OR, xlss, conc ) );
 
               d_neg_ctn_cached.insert( atom );
               sendLemma( atom.negate(), conc, "NEG-CTN-BRK" );
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 54156c85d..0cccdf0ef 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -482,11 +482,13 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
       Node cond = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, x, y );
       Node c1 = x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, y, sk2 ) );
       Node c2 = skw.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, z, sk2 ) );
-      Node c3 = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, sk1, y ).negate();
+      //Node c3 = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, sk1, y ).negate();
       Node rr = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond,
-              NodeManager::currentNM()->mkNode( kind::AND, c1, c2, c3 ),
+              NodeManager::currentNM()->mkNode( kind::AND, c1, c2), // c3 
               skw.eqNode(x) ) );
       new_nodes.push_back( rr );
+      rr = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::GT, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, y), d_zero) );
+      new_nodes.push_back( rr );
 
       d_cache[t] = skw;
       retNode = skw;
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index c226afa7d..88b43f2bf 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -403,6 +403,42 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
       } else {
         retNode = NodeManager::currentNM()->mkConst( false );
       }
+    } else if( node[0].getKind() == kind::STRING_CONCAT ) {
+      if( node[1].getKind() != kind::STRING_CONCAT ){
+        bool flag = false;
+        for(unsigned i=0; i<node[0].getNumChildren(); i++) {
+          if(node[0][i] == node[1]) {
+            flag = true;
+            break;
+          }
+        }
+        if(flag) {
+          retNode = NodeManager::currentNM()->mkConst( true );
+        }
+      } else {
+        bool flag = false;
+        unsigned n1 = node[0].getNumChildren();
+        unsigned n2 = node[1].getNumChildren();
+        if(n1 - n2) {
+          for(unsigned i=0; i<=n1 - n2; i++) {
+            if(node[0][i] == node[1][0]) {
+              flag = true;
+              for(unsigned j=1; j<n2; j++) {
+                if(node[0][i+j] != node[1][j]) {
+                  flag = false;
+                  break;
+                }
+              }
+              if(flag) {
+                break;
+              }
+            }
+          }
+          if(flag) {
+            retNode = NodeManager::currentNM()->mkConst( true );
+          }
+        }
+      }
     }
   } else if(node.getKind() == kind::STRING_STRIDOF) {
     if( node[0].isConst() && node[1].isConst() && node[2].isConst() ) {