From 614080814375998f494adc839484f455b31a5f43 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 15 Oct 2015 15:57:03 +0200 Subject: Change semantics of str.substr to allow endpoint out of bounds, and return empty string for error conditions. Improve rewriter for str.substr. --- src/theory/strings/kinds | 6 +- src/theory/strings/regexp_operation.cpp | 8 +- src/theory/strings/theory_strings.cpp | 73 +++------------- src/theory/strings/theory_strings.h | 6 -- src/theory/strings/theory_strings_preprocess.cpp | 40 +++++++-- src/theory/strings/theory_strings_rewriter.cpp | 106 ++++++++++++++--------- 6 files changed, 116 insertions(+), 123 deletions(-) (limited to 'src/theory') diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 0f68d1207..3cdff9cba 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -15,9 +15,8 @@ typechecker "theory/strings/theory_strings_type_rules.h" operator STRING_CONCAT 2: "string concat (N-ary)" operator STRING_IN_REGEXP 2 "membership" operator STRING_LENGTH 1 "string length" -operator STRING_SUBSTR 3 "string substr (user symbol)" -operator STRING_SUBSTR_TOTAL 3 "string substr (internal symbol)" -operator STRING_CHARAT 2 "string charat (user symbol)" +operator STRING_SUBSTR 3 "string substr" +operator STRING_CHARAT 2 "string charat" operator STRING_STRCTN 2 "string contains" operator STRING_STRIDOF 3 "string indexof" operator STRING_STRREPL 3 "string replace" @@ -107,7 +106,6 @@ typerule STRING_TO_REGEXP ::CVC4::theory::strings::StringToRegExpTypeRule typerule STRING_CONCAT ::CVC4::theory::strings::StringConcatTypeRule typerule STRING_LENGTH ::CVC4::theory::strings::StringLengthTypeRule typerule STRING_SUBSTR ::CVC4::theory::strings::StringSubstrTypeRule -typerule STRING_SUBSTR_TOTAL ::CVC4::theory::strings::StringSubstrTypeRule typerule STRING_CHARAT ::CVC4::theory::strings::StringCharAtTypeRule typerule STRING_STRCTN ::CVC4::theory::strings::StringContainTypeRule typerule STRING_STRIDOF ::CVC4::theory::strings::StringIndexOfTypeRule diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index cad1f3bf1..ac4bddd73 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -975,8 +975,8 @@ void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1); Node g1 = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode(kind::GEQ, b1, d_zero), NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s), b1 ) ); - Node s1 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, s, d_zero, b1)); - Node s2 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, s, b1, NodeManager::currentNM()->mkNode(kind::MINUS, lens, b1))); + Node s1 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, s, d_zero, b1)); + Node s2 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, s, b1, NodeManager::currentNM()->mkNode(kind::MINUS, lens, b1))); Node s1r1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s1, r[0]).negate(); if(r[0].getKind() == kind::STRING_TO_REGEXP) { s1r1 = s1.eqNode(r[0][0]).negate(); @@ -1054,8 +1054,8 @@ void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes Node g1 = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode(kind::GEQ, b1, d_one), NodeManager::currentNM()->mkNode( kind::GEQ, lens, b1 ) ); //internal - Node s1 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, s, d_zero, b1); - Node s2 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, s, b1, NodeManager::currentNM()->mkNode(kind::MINUS, lens, b1)); + Node s1 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, s, d_zero, b1); + Node s2 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, s, b1, NodeManager::currentNM()->mkNode(kind::MINUS, lens, b1)); Node s1r1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s1, r[0]).negate(); Node s2r2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s2, r).negate(); diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index fc8df8bbc..d985977d6 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -97,7 +97,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_equalityEngine.addFunctionKind(kind::STRING_LENGTH); d_equalityEngine.addFunctionKind(kind::STRING_CONCAT); d_equalityEngine.addFunctionKind(kind::STRING_STRCTN); - d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR_TOTAL); + d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR); d_equalityEngine.addFunctionKind(kind::STRING_ITOS); d_equalityEngine.addFunctionKind(kind::STRING_STOI); if( options::stringLazyPreproc() ){ @@ -466,7 +466,7 @@ void TheoryStrings::preRegisterTerm(TNode n) { d_equalityEngine.addTerm(n[1]); break; } - //case kind::STRING_SUBSTR_TOTAL: + //case kind::STRING_SUBSTR: default: { if( n.getType().isString() ) { registerTerm(n); @@ -488,60 +488,7 @@ void TheoryStrings::preRegisterTerm(TNode n) { } Node TheoryStrings::expandDefinition(LogicRequest &logicRequest, Node node) { - switch (node.getKind()) { - case kind::STRING_CHARAT: { - if(d_ufSubstr.isNull()) { - std::vector< TypeNode > argTypes; - argTypes.push_back(NodeManager::currentNM()->stringType()); - argTypes.push_back(NodeManager::currentNM()->integerType()); - argTypes.push_back(NodeManager::currentNM()->integerType()); - d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS", - NodeManager::currentNM()->mkFunctionType( - argTypes, NodeManager::currentNM()->stringType()), - "uf substr", - NodeManager::SKOLEM_EXACT_NAME); - } - Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT, - NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, node[0] ), node[1] ); - Node t1greq0 = NodeManager::currentNM()->mkNode( kind::GEQ, node[1], d_zero); - Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1greq0 )); - Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[0], node[1], d_one); - Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, node[0], node[1], d_one); - return NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf ); - //return NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[0], node[1], d_one); - break; - } - - case kind::STRING_SUBSTR: { - if(d_ufSubstr.isNull()) { - std::vector< TypeNode > argTypes; - argTypes.push_back(NodeManager::currentNM()->stringType()); - argTypes.push_back(NodeManager::currentNM()->integerType()); - argTypes.push_back(NodeManager::currentNM()->integerType()); - d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS", - NodeManager::currentNM()->mkFunctionType( - argTypes, NodeManager::currentNM()->stringType()), - "uf substr", - NodeManager::SKOLEM_EXACT_NAME); - } - Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, - NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, node[0] ), - NodeManager::currentNM()->mkNode( kind::PLUS, node[1], node[2] ) ); - Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, node[1], d_zero); - Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, node[2], d_zero); - Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 )); - Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[0], node[1], node[2]); - Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, node[0], node[1], node[2]); - return NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf ); - //return NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[0], node[1], node[2]); - break; - } - - default : - return node; - } - - Unreachable(); + return node; } @@ -3492,10 +3439,10 @@ void TheoryStrings::checkMemberships() { NodeManager::currentNM()->mkNode(kind::GEQ, len1, bi), NodeManager::currentNM()->mkNode(kind::GEQ, bj, d_zero), NodeManager::currentNM()->mkNode(kind::GEQ, len2, bj)); - Node s11 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, p1, d_zero, bi); - Node s12 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, p1, bi, NodeManager::currentNM()->mkNode(kind::MINUS, len1, bi)); - Node s21 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, p2, d_zero, bj); - Node s22 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, p2, bj, NodeManager::currentNM()->mkNode(kind::MINUS, len2, bj)); + Node s11 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, p1, d_zero, bi); + Node s12 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, p1, bi, NodeManager::currentNM()->mkNode(kind::MINUS, len1, bi)); + Node s21 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, p2, d_zero, bj); + Node s22 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, p2, bj, NodeManager::currentNM()->mkNode(kind::MINUS, len2, bj)); Node cc1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s11, r).negate(); Node cc2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, mkConcat(s12, s21), r[0]).negate(); Node cc3 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s22, r).negate(); @@ -4178,8 +4125,8 @@ void TheoryStrings::checkNegContains( std::vector< Node >& negContains ) { Node g1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::GEQ, b1, d_zero ), NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode( kind::MINUS, lenx, lens ), b1 ) ) ); Node b2 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType()); - Node s2 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, x, NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 ), d_one); - Node s5 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, s, b2, d_one); + Node s2 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, x, NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 ), d_one); + Node s5 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, s, b2, d_one); Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b2);//, s1, s3, s4, s6); @@ -4506,7 +4453,7 @@ void TheoryStrings::assertNode( Node lit ) { void TheoryStrings::collectExtendedFuncTerms( Node n, std::map< Node, bool >& visited ) { if( visited.find( n )==visited.end() ){ visited[n] = true; - if( n.getKind()==kind::STRING_SUBSTR_TOTAL || n.getKind()==kind::STRING_STRIDOF || + if( n.getKind()==kind::STRING_SUBSTR || n.getKind()==kind::STRING_STRIDOF || n.getKind() == kind::STRING_ITOS || n.getKind() == kind::STRING_U16TOS || n.getKind() == kind::STRING_U32TOS || n.getKind() == kind::STRING_STOI || n.getKind() == kind::STRING_STOU16 || n.getKind() == kind::STRING_STOU32 || n.getKind() == kind::STRING_STRREPL || n.getKind() == kind::STRING_STRCTN ){ diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index b2864656a..f57bf43f8 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -119,12 +119,6 @@ public: };/* class TheoryStrings::NotifyClass */ private: - /** - * Function symbol used to implement uninterpreted undefined string - * semantics. Needed to deal with partial charat/substr function. - */ - Node d_ufSubstr; - // Constants Node d_emptyString; Node d_emptyRegexp; diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index b2b7bac5e..8f899cd46 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -162,7 +162,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes, bool d Node retNode = t; if( options::stringLazyPreproc() ){ //only process extended operators after preprocess - if( during_pp && ( t.getKind() == kind::STRING_SUBSTR_TOTAL || t.getKind() == kind::STRING_STRIDOF || + if( during_pp && ( t.getKind() == kind::STRING_SUBSTR || t.getKind() == kind::STRING_STRIDOF || t.getKind() == kind::STRING_ITOS || t.getKind() == kind::STRING_U16TOS || t.getKind() == kind::STRING_U32TOS || t.getKind() == kind::STRING_STOI || t.getKind() == kind::STRING_STOU16 || t.getKind() == kind::STRING_STOU32 || t.getKind() == kind::STRING_STRREPL ) ){ @@ -203,7 +203,8 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes, bool d n = Rewriter::rewrite(n); d_cache[t] = (t == n) ? Node::null() : n; retNode = n; - } else if( t.getKind() == kind::STRING_SUBSTR_TOTAL ) { + } else if( t.getKind() == kind::STRING_SUBSTR ) { + /* Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ), NodeManager::currentNM()->mkNode( kind::PLUS, t[1], t[2] ) ); @@ -218,6 +219,31 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes, bool d Node lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond, NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, lenc ), t.eqNode(NodeManager::currentNM()->mkConst( ::CVC4::String("") )) )); + */ + Node t12 = NodeManager::currentNM()->mkNode( kind::PLUS, t[1], t[2] ); + Node lt0 = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ); + //start point is greater than or equal zero + Node c1 = NodeManager::currentNM()->mkNode( kind::GEQ, t[1], d_zero ); + //start point is less than end of string + Node c2 = NodeManager::currentNM()->mkNode( kind::GT, lt0, t[1] ); + //length is positive + Node c3 = NodeManager::currentNM()->mkNode( kind::GT, t[2], d_zero ); + Node cond = NodeManager::currentNM()->mkNode( kind::AND, c1, c2, c3 ); + + Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1", NodeManager::currentNM()->stringType(), "created for substr" ); + Node sk2 = NodeManager::currentNM()->mkSkolem( "ss2", NodeManager::currentNM()->stringType(), "created for substr" ); + Node b11 = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, t, sk2 ) ); + //length of first skolem is second argument + Node b12 = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ).eqNode( t[1] ); + //length of second skolem is abs difference between end point and end of string + Node b13 = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ).eqNode( + NodeManager::currentNM()->mkNode( kind::ITE, NodeManager::currentNM()->mkNode( kind::GEQ, lt0, t12 ), + NodeManager::currentNM()->mkNode( kind::MINUS, lt0, t12 ), d_zero ) ); + + Node b1 = NodeManager::currentNM()->mkNode( kind::AND, b11, b12, b13 ); + Node b2 = t.eqNode( NodeManager::currentNM()->mkConst( ::CVC4::String("") ) ); + + Node lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond, b1, b2 ) ); new_nodes.push_back( lemma ); d_cache[t] = t; } else if( t.getKind() == kind::STRING_STRIDOF ) { @@ -225,7 +251,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes, bool d Node sk3 = NodeManager::currentNM()->mkSkolem( "io3", NodeManager::currentNM()->stringType(), "created for indexof" ); Node sk4 = NodeManager::currentNM()->mkSkolem( "io4", NodeManager::currentNM()->stringType(), "created for indexof" ); Node skk = NodeManager::currentNM()->mkSkolem( "iok", NodeManager::currentNM()->integerType(), "created for indexof" ); - Node st = NodeManager::currentNM()->mkNode( kind::STRING_SUBSTR_TOTAL, t[0], t[2], NodeManager::currentNM()->mkNode( kind::MINUS, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ), t[2] ) ); + Node st = NodeManager::currentNM()->mkNode( kind::STRING_SUBSTR, t[0], t[2], NodeManager::currentNM()->mkNode( kind::MINUS, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ), t[2] ) ); Node eq = st.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk2, sk3, sk4 ) ); new_nodes.push_back( eq ); Node negone = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) ); @@ -250,7 +276,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes, bool d //~contain(t2, s2) Node c5 = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, sk2, - NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, t[1], d_zero, + NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, t[1], d_zero, NodeManager::currentNM()->mkNode(kind::MINUS, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, t[1]), NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) )))), @@ -437,7 +463,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes, bool d vec_n.push_back(g); g = NodeManager::currentNM()->mkNode(kind::GT, lenp, p); vec_n.push_back(g); - Node z2 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, str, p, one); + Node z2 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, str, p, one); char chtmp[2]; chtmp[1] = '\0'; for(unsigned i=0; i<=9; i++) { @@ -463,7 +489,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes, bool d vec_c3b.push_back(c3cc); c3cc = NodeManager::currentNM()->mkNode(kind::GEQ, nine, ufMx); vec_c3b.push_back(c3cc); - Node sx = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, str, b2, one); + Node sx = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, str, b2, one); for(unsigned i=0; i<=9; i++) { chtmp[0] = i + '0'; std::string stmp(chtmp); @@ -516,7 +542,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes, bool d Node c2 = skw.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, z, sk2 ) ); 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::STRING_SUBSTR, y, d_zero, NodeManager::currentNM()->mkNode(kind::MINUS, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, y), NodeManager::currentNM()->mkConst(::CVC4::Rational(1))))), y).negate(); diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 6356277ed..2d6c1e3af 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1014,13 +1014,13 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { } else if(node.getKind() == kind::STRING_LENGTH) { if(node[0].isConst()) { retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( node[0].getConst().size() ) ); - } else if(node[0].getKind() == kind::STRING_SUBSTR_TOTAL) { + } else if(node[0].getKind() == kind::STRING_SUBSTR) { //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) { + } else if(tmpNode.getKind() == kind::STRING_SUBSTR) { //retNode = tmpNode[2]; } else { // it has to be string concat @@ -1028,7 +1028,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { for(unsigned int i=0; imkConst( ::CVC4::Rational( tmpNode[i].getConst().size() ) ) ); - } else if(tmpNode[i].getKind() == kind::STRING_SUBSTR_TOTAL) { + } else if(tmpNode[i].getKind() == kind::STRING_SUBSTR) { node_vec.push_back( tmpNode[i][2] ); } else { node_vec.push_back( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, tmpNode[i]) ); @@ -1043,44 +1043,72 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { } } } - } else if( node.getKind() == kind::STRING_SUBSTR_TOTAL ){ + }else if( node.getKind() == kind::STRING_CHARAT ){ + Node one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); + retNode = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, node[0], node[1], one); + }else if( node.getKind() == kind::STRING_SUBSTR ){ Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ); - if(node[2] == zero) { + if( node[2].isConst() && node[2].getConst().sgn()<=0 ) { retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); - } else if( node[1].isConst() && node[2].isConst() ) { - if(node[1].getConst().sgn()>=0 && node[2].getConst().sgn()>=0) { - CVC4::Rational sum(node[1].getConst() + node[2].getConst()); - if( node[0].isConst() ) { - CVC4::Rational size(node[0].getConst().size()); - if( size >= sum ) { - //because size is smaller than MAX_INT - size_t i = node[1].getConst().getNumerator().toUnsignedInt(); - size_t j = node[2].getConst().getNumerator().toUnsignedInt(); - retNode = NodeManager::currentNM()->mkConst( node[0].getConst().substr(i, j) ); - } else { - retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); - } - } else if(node[0].getKind() == kind::STRING_CONCAT && node[0][0].isConst()) { - CVC4::Rational size2(node[0][0].getConst().size()); - if( size2 >= sum ) { - //because size2 is smaller than MAX_INT - size_t i = node[1].getConst().getNumerator().toUnsignedInt(); - size_t j = node[2].getConst().getNumerator().toUnsignedInt(); - retNode = NodeManager::currentNM()->mkConst( node[0][0].getConst().substr(i, j) ); - } - } - } else { + }else if( node[1].isConst() ){ + if( node[1].getConst().sgn()<0 ){ + //bring forward to start at zero? don't use this semantics, e.g. does not compose well with error conditions for str.indexof. + //retNode = NodeManager::currentNM()->mkNode( kind::STRING_SUBSTR, node[0], zero, NodeManager::currentNM()->mkNode( kind::PLUS, node[1], node[2] ) ); retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); - } - } else if(node[1] == zero ) { - if( node[2].getKind() == kind::STRING_LENGTH && node[2][0]==node[0] ){ - retNode = node[0]; }else{ - //check if lengths rewrite to the same thing - Node lt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, node[0] ); - lt = Rewriter::rewrite( lt ); - if( lt==node[2] ){ - retNode = node[0]; + if( node[2].isConst() ){ + Assert( node[2].getConst().sgn()>=0); + CVC4::Rational v1( node[1].getConst() ); + CVC4::Rational v2( node[2].getConst() ); + std::vector< Node > children; + getConcat( node[0], children ); + if( children[0].isConst() ){ + CVC4::Rational size(children[0].getConst().size()); + if( v1 >= size ){ + if( node[0].isConst() ){ + retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); + }else{ + children.erase( children.begin(), children.begin()+1 ); + retNode = NodeManager::currentNM()->mkNode( kind::STRING_SUBSTR, mkConcat( kind::STRING_CONCAT, children ), + NodeManager::currentNM()->mkNode( kind::MINUS, node[1], NodeManager::currentNM()->mkConst( size ) ), + node[2] ); + } + }else{ + //since size is smaller than MAX_INT, v1 is smaller than MAX_INT + size_t i = v1.getNumerator().toUnsignedInt(); + CVC4::Rational sum(v1 + v2); + bool full_spl = false; + size_t j; + if( sum>size ){ + j = size.getNumerator().toUnsignedInt(); + }else{ + //similarly, sum is smaller than MAX_INT + j = sum.getNumerator().toUnsignedInt(); + full_spl = true; + } + //split the first component of the string + Node spl = NodeManager::currentNM()->mkConst( children[0].getConst().substr(i, j-i) ); + if( node[0].isConst() || full_spl ){ + retNode = spl; + }else{ + children[0] = spl; + retNode = NodeManager::currentNM()->mkNode( kind::STRING_SUBSTR, mkConcat( kind::STRING_CONCAT, children ), zero, node[2] ); + } + } + } + }else{ + if( node[1]==zero ){ + if( node[2].getKind() == kind::STRING_LENGTH && node[2][0]==node[0] ){ + retNode = node[0]; + }else{ + //check if the length argument is always at least the length of the string + Node cmp = NodeManager::currentNM()->mkNode( kind::GEQ, node[2], NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, node[0] ) ); + cmp = Rewriter::rewrite( cmp ); + if( cmp==NodeManager::currentNM()->mkConst(true) ){ + retNode = node[0]; + } + } + } } } } @@ -1105,7 +1133,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { Node lent = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[1]); retNode = NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::GEQ, lent, lens), - node[0].eqNode(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[1], + node[0].eqNode(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, node[1], NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ), lens))); } }else if( node.getKind() == kind::STRING_SUFFIX ){ @@ -1123,7 +1151,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { Node lent = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[1]); retNode = NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::GEQ, lent, lens), - node[0].eqNode(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[1], + node[0].eqNode(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, node[1], NodeManager::currentNM()->mkNode(kind::MINUS, lent, lens), lens))); } }else if(node.getKind() == kind::STRING_ITOS || node.getKind() == kind::STRING_U16TOS || node.getKind() == kind::STRING_U32TOS) { -- cgit v1.2.3