From 68d3518e446b1e0f1ac16c2146c162580fa377f9 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 9 Sep 2015 10:34:20 +0200 Subject: [PATCH] Fix bug in strings rewriter regarding lengths of substr terms. --- src/theory/strings/theory_strings.cpp | 3 ++- .../strings/theory_strings_rewriter.cpp | 22 +++++++++---------- test/regress/regress0/strings/Makefile.am | 9 ++++---- .../regress0/strings/unsound-0908.smt2 | 12 ++++++++++ 4 files changed, 30 insertions(+), 16 deletions(-) create mode 100755 test/regress/regress0/strings/unsound-0908.smt2 diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 059db91f2..4ac178cbd 100644 --- 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 872933cbd..575da9344 100644 --- 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 vtmp; for(unsigned i=0; imkNode(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().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().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_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 d521680d5..eb88df905 100644 --- 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 index 000000000..cbaf5f5e4 --- /dev/null +++ b/test/regress/regress0/strings/unsound-0908.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_S) +(set-info :status sat) +(declare-const x String) +(assert (= (str.len x) 1)) +;(assert (= x "X")) +(assert + (or + (not (> (str.len x) 1)) + (= (str.at x 1) "Z") + ) +) +(check-sat) -- 2.30.2