Fix bug in strings rewriter regarding lengths of substr terms.

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 059db91f2981ba538e93cdc9e3cfc86062f06555..4ac178cbd9498211c596643090b5e6c4422f53cc 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -1893,6 +1893,7 @@ bool TheoryStrings::registerTerm( Node n ) {
         }
         Node ceq = Rewriter::rewrite( skl.eqNode( lsum ) );
         Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq << std::endl;
+        Trace("strings-lemma-debug") << "  prerewrite : " << skl.eqNode( lsum ) << std::endl;
         d_out->lemma(ceq);
         //also add this to the equality engine
         if( n.getKind() == kind::CONST_STRING ) {
@@ -3307,7 +3308,7 @@ bool TheoryStrings::checkNegContains() {
         Node conc = Node::null();
         sendLemma( ant, conc, "NEG-CTN Conflict 2" );
         addedLemma = true;
-      } 
+      }
     }
   }
   if( !d_conflict ){

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 872933cbd7112f4f3fa52bb279316d4da2bce702..575da934464414c7fef8887cb989f6c6974d5c15 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Tianyi Liang
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
@@ -283,15 +283,15 @@ Node TheoryStringsRewriter::applyAX( TNode node ) {
         retNode = emptysingleton;
       } else if(vec_nodes.size() == 1) {
         shrinkConVec(vec_nodes[0]);
-        retNode = vec_nodes[0].empty()? emptysingleton 
-          : vec_nodes[0].size()==1? vec_nodes[0][0] 
+        retNode = vec_nodes[0].empty()? emptysingleton
+          : vec_nodes[0].size()==1? vec_nodes[0][0]
           : NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, vec_nodes[0]);
       } else {
         std::vector<Node> vtmp;
         for(unsigned i=0; i<vec_nodes.size(); i++) {
           shrinkConVec(vec_nodes[i]);
           if(!vec_nodes[i].empty()) {
-            Node ntmp = vec_nodes[i].size()==1? vec_nodes[i][0] 
+            Node ntmp = vec_nodes[i].size()==1? vec_nodes[i][0]
               : NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, vec_nodes[i]);
             vtmp.push_back(ntmp);
           }
@@ -614,7 +614,7 @@ Node TheoryStringsRewriter::prerewriteAndRegExp(TNode node) {
   }
   if(!emptyflag) {
     std::vector< Node > nvec;
-    retNode = node_vec.size() == 0 ? 
+    retNode = node_vec.size() == 0 ?
           NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, NodeManager::currentNM()->mkNode(kind::REGEXP_SIGMA, nvec)) :
           node_vec.size() == 1 ? node_vec[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_INTER, node_vec);
   }
@@ -867,13 +867,13 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
     if(node[0].isConst()) {
       retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( node[0].getConst<String>().size() ) );
     } else if(node[0].getKind() == kind::STRING_SUBSTR_TOTAL) {
-        retNode = node[0][2];
+      //retNode = node[0][2];
     } else if(node[0].getKind() == kind::STRING_CONCAT) {
       Node tmpNode = rewriteConcatString(node[0]);
       if(tmpNode.isConst()) {
         retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( tmpNode.getConst<String>().size() ) );
       } else if(tmpNode.getKind() == kind::STRING_SUBSTR_TOTAL) {
-        retNode = tmpNode[2];
+        //retNode = tmpNode[2];
       } else {
         // it has to be string concat
         std::vector<Node> node_vec;
@@ -1138,14 +1138,14 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) {
 
   if(node.getKind() == kind::STRING_CONCAT) {
     retNode = rewriteConcatString(node);
-  } 
+  }
   else if(node.getKind() == kind::REGEXP_CONCAT) {
     retNode = prerewriteConcatRegExp(node);
   } else if(node.getKind() == kind::REGEXP_UNION) {
     retNode = prerewriteOrRegExp(node);
   } else if(node.getKind() == kind::REGEXP_INTER) {
     retNode = prerewriteAndRegExp(node);
-  } 
+  }
   else if(node.getKind() == kind::REGEXP_STAR) {
     if(node[0].getKind() == kind::REGEXP_STAR) {
       retNode = node[0];
@@ -1240,8 +1240,8 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) {
         }
       } else {
         retNode = l==0? NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, node[0]) :
-          NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, 
-            NodeManager::currentNM()->mkNode(kind::REGEXP_LOOP, node[0], n1, n1), 
+          NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT,
+            NodeManager::currentNM()->mkNode(kind::REGEXP_LOOP, node[0], n1, n1),
             NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, node[0]));
       }
     }*/ //lazy

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index d521680d5b605b62385e4452bf70c06dcfee23b7..eb88df9057b48e8c8f2770c7108576e509bfb4ae 100644 (file)
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -9,8 +9,8 @@ AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXE
 if AUTOMAKE_1_11
 # old-style (pre-automake 1.12) test harness
 TESTS_ENVIRONMENT = \
-       $(LOG_COMPILER) \
-       $(AM_LOG_FLAGS) $(LOG_FLAGS)
+  $(LOG_COMPILER) \
+  $(AM_LOG_FLAGS) $(LOG_FLAGS)
 endif
 
 MAKEFLAGS = -k
@@ -18,7 +18,7 @@ MAKEFLAGS = -k
 # These are run for all build profiles.
 # If a test shouldn't be run in e.g. competition mode,
 # put it below in "TESTS +="
-TESTS =        \
+TESTS = \
   at001.smt2 \
   bug001.smt2 \
   bug002.smt2 \
@@ -49,7 +49,8 @@ TESTS =       \
   loop007.smt2 \
   loop008.smt2 \
   loop009.smt2 \
-  reloop.smt2 
+  reloop.smt2 \
+  unsound-0908.smt2 
 
 
 FAILING_TESTS =

diff --git a/test/regress/regress0/strings/unsound-0908.smt2 b/test/regress/regress0/strings/unsound-0908.smt2
new file mode 100755 (executable)
index 0000000..cbaf5f5
--- /dev/null
+++ b/test/regress/regress0/strings/unsound-0908.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_S)\r
+(set-info :status sat)\r
+(declare-const x String)\r
+(assert (= (str.len x) 1))\r
+;(assert (= x "X"))\r
+(assert\r
+    (or \r
+      (not (> (str.len x) 1))\r
+      (= (str.at x 1) "Z")\r
+    )\r
+)\r
+(check-sat)\r