From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Wed, 7 May 2014 20:49:09 +0000 (-0500)
Subject: fix a bug in contain
X-Git-Tag: cvc5-1.0.0~6924
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e8bafcf829335a011c551b29f1700c485087bf56;p=cvc5.git

fix a bug in contain
---

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index e60e67ac1..e73cf5e9d 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -2846,12 +2846,16 @@ bool TheoryStrings::checkNegContains() {
             }
           } else if(!areDisequal(lenx, lens)) {
             if(d_neg_ctn_ulen.find(atom) == d_neg_ctn_ulen.end()) {
+              lenx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x);
+              lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s);
               d_neg_ctn_ulen.insert( atom );
               sendSplit(lenx, lens, "NEG-CTN-SP");
               addedLemma = true;
             }
           } else {
             if(d_neg_ctn_cached.find(atom) == d_neg_ctn_cached.end()) {
+              lenx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x);
+              lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s);
               Node b1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
               Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1);
               Node g1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::GEQ, b1, d_zero ),
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 0cccdf0ef..be419a36a 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -482,9 +482,14 @@ 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,
+                  NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, sk1,
+                     NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, y, d_zero,
+                        NodeManager::currentNM()->mkNode(kind::MINUS, 
+                          NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, y), 
+                          NodeManager::currentNM()->mkConst(::CVC4::Rational(1))))), 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) );