From 6b2b7c90c9dccb596181fcf399a8830b05db5408 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Tue, 28 Jan 2014 17:17:51 -0600 Subject: [PATCH] merge internal and user of charat & substr into one --- src/printer/smt2/smt2_printer.cpp | 8 +- src/smt/smt_engine.cpp | 71 +----------------- src/theory/strings/kinds | 4 - src/theory/strings/theory_strings.cpp | 75 +++++++++++++++---- src/theory/strings/theory_strings.h | 2 +- .../strings/theory_strings_preprocess.cpp | 44 +---------- .../strings/theory_strings_preprocess.h | 1 + .../strings/theory_strings_rewriter.cpp | 16 ++-- test/regress/regress0/strings/substr001.smt2 | 2 + 9 files changed, 84 insertions(+), 139 deletions(-) diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index cf3fac971..aae9938b7 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -278,12 +278,8 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::STRING_CONCAT: out << "str.++ "; break; case kind::STRING_IN_REGEXP: out << "str.in.re "; break; case kind::STRING_LENGTH: out << "str.len "; break; - case kind::STRING_SUBSTR: - case kind::STRING_SUBSTR_TOTAL: - out << "str.substr "; break; - case kind::STRING_CHARAT: - case kind::STRING_CHARAT_TOTAL: - out << "str.at "; break; + case kind::STRING_SUBSTR: out << "str.substr "; break; + case kind::STRING_CHARAT: out << "str.at "; break; case kind::STRING_STRCTN: out << "str.contain "; break; case kind::STRING_STRIDOF: out << "str.indexof "; break; case kind::STRING_STRREPL: out << "str.replace "; break; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c77c05423..8754dc084 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -310,9 +310,7 @@ class SmtEnginePrivate : public NodeManagerListener { * Function symbol used to implement uninterpreted undefined string * semantics. Needed to deal with partial charat/substr function. */ - Node d_charAtUF; - Node d_charAtUndef; - Node d_substrUndef; + //Node d_substrUndef; /** * Function symbol used to implement uninterpreted division-by-zero @@ -442,9 +440,6 @@ public: d_fakeContext(), d_abstractValueMap(&d_fakeContext), d_abstractValues(), - d_charAtUF(), - d_charAtUndef(), - d_substrUndef(), d_divByZero(), d_intDivByZero(), d_modZero(), @@ -1560,68 +1555,8 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map argTypes; - argTypes.push_back(NodeManager::currentNM()->stringType()); - argTypes.push_back(NodeManager::currentNM()->integerType()); - d_charAtUF = NodeManager::currentNM()->mkSkolem("charAt", - NodeManager::currentNM()->mkFunctionType( - argTypes, - NodeManager::currentNM()->stringType()), - "total charat", - NodeManager::SKOLEM_EXACT_NAME); - d_charAtUndef = NodeManager::currentNM()->mkSkolem("charAt_undef", - NodeManager::currentNM()->mkFunctionType( - argTypes, - NodeManager::currentNM()->stringType()), - "partial charat undef", - NodeManager::SKOLEM_EXACT_NAME); - if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) { - d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); - d_smt.d_logic.enableTheory(THEORY_UF); - d_smt.d_logic.lock(); - } - } - Node str = n[0]; - Node num = n[1]; - //Assert(str.getType() == NodeManager::currentNM()->stringType(), "String Type Check 1"); - Node lenx = nm->mkNode(kind::STRING_LENGTH, str); - Node cond = nm->mkNode(kind::GT, lenx, num); - Node total = nm->mkNode(kind::STRING_CHARAT_TOTAL, str, num); - Node undef = nm->mkNode(kind::APPLY_UF, d_charAtUndef, str, num); - node = nm->mkNode(kind::ITE, cond, total, undef); - node = nm->mkNode(kind::APPLY_UF, d_charAtUF, n[0], n[1]); - } - break;*/ - case kind::STRING_SUBSTR: { - if(d_substrUndef.isNull()) { - std::vector< TypeNode > argTypes; - argTypes.push_back(NodeManager::currentNM()->stringType()); - argTypes.push_back(NodeManager::currentNM()->integerType()); - argTypes.push_back(NodeManager::currentNM()->integerType()); - d_substrUndef = NodeManager::currentNM()->mkSkolem("substr_undef", - NodeManager::currentNM()->mkFunctionType( - argTypes, - NodeManager::currentNM()->stringType()), - "partial substring undef", - NodeManager::SKOLEM_EXACT_NAME); - if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) { - d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); - d_smt.d_logic.enableTheory(THEORY_UF); - d_smt.d_logic.lock(); - } - } - Node str = n[0]; - //Assert(str.getType() == NodeManager::currentNM()->stringType(), "String Type Check 2"); - Node lenx = nm->mkNode(kind::STRING_LENGTH, str); - Node num = nm->mkNode(kind::PLUS, n[1], n[2]); - Node cond = nm->mkNode(kind::GEQ, lenx, num); - Node total = nm->mkNode(kind::STRING_SUBSTR_TOTAL, str, n[1], n[2]); - Node undef = nm->mkNode(kind::APPLY_UF, d_substrUndef, str, n[1], n[2]); - node = nm->mkNode(kind::ITE, cond, total, undef); - } - break; + //case kind::STRING_CHARAT: + //case kind::STRING_SUBSTR: case kind::DIVISION: { // partial function: division diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index b30bf8f36..e55891ec2 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -14,9 +14,7 @@ operator STRING_CONCAT 2: "string concat" 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_CHARAT_TOTAL 2 "string charat (internal symbol)" operator STRING_STRCTN 2 "string contains" operator STRING_STRIDOF 3 "string indexof" operator STRING_STRREPL 3 "string replace" @@ -107,9 +105,7 @@ 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_CHARAT_TOTAL ::CVC4::theory::strings::StringCharAtTypeRule typerule STRING_STRCTN ::CVC4::theory::strings::StringContainTypeRule typerule STRING_STRIDOF ::CVC4::theory::strings::StringIndexOfTypeRule typerule STRING_STRREPL ::CVC4::theory::strings::StringReplaceTypeRule diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 4deb0a9d9..0a8781abb 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -54,8 +54,8 @@ 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_CHARAT_TOTAL); - //d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR_TOTAL); + d_equalityEngine.addFunctionKind(kind::STRING_CHARAT); + d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR); d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); @@ -381,22 +381,36 @@ void TheoryStrings::preRegisterTerm(TNode n) { case kind::STRING_IN_REGEXP: //d_equalityEngine.addTriggerPredicate(n); break; + case kind::CONST_STRING: + case kind::STRING_CONCAT: + case kind::STRING_CHARAT: + case kind::STRING_SUBSTR: + //do nothing + break; default: - if(n.getType().isString() && n.getKind() != kind::CONST_STRING && n.getKind()!=kind::STRING_CONCAT ) { + if(n.getType().isString() ) { if( std::find( d_length_intro_vars.begin(), d_length_intro_vars.end(), n )==d_length_intro_vars.end() ) { - if(n.getKind() == kind::STRING_CHARAT_TOTAL) { + /* + if(n.getKind() == kind::STRING_CHARAT) { Node lenc_eq_one = d_one.eqNode(NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n)); Trace("strings-lemma") << "Strings::Lemma LEN(CHAR) = 1 : " << lenc_eq_one << std::endl; d_out->lemma(lenc_eq_one); + } else if(n.getKind() == kind::STRING_SUBSTR) { + Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n); + Node lenc_eq_n2 = n_len.eqNode(n[2]); + Trace("strings-lemma") << "Strings::Lemma LEN(SUBSTR) : " << lenc_eq_n2 << std::endl; + d_out->lemma(lenc_eq_n2); } else { + */ Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n); Node n_len_eq_z = n_len.eqNode( d_zero ); + n_len_eq_z = Rewriter::rewrite( n_len_eq_z ); Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::OR, n_len_eq_z, NodeManager::currentNM()->mkNode( kind::GT, n_len, d_zero) ); Trace("strings-lemma") << "Strings::Lemma LENGTH >= 0 : " << n_len_geq_zero << std::endl; d_out->lemma(n_len_geq_zero); d_out->requirePhase( n_len_eq_z, true ); - } + //} } // FMF if( n.getKind() == kind::VARIABLE ) {//options::stringFMF() && @@ -466,8 +480,8 @@ void TheoryStrings::check(Effort e) { bool addedLemma = false; if( e == EFFORT_FULL && !d_conflict ) { - addedLemma = checkLengths(); - Trace("strings-process") << "Done check (constant) lengths, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; + addedLemma = checkSimple(); + Trace("strings-process") << "Done simple checking, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; if( !addedLemma ) { addedLemma = checkNormalForms(); Trace("strings-process") << "Done check normal forms, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; @@ -1693,7 +1707,7 @@ void TheoryStrings::getConcatVec( Node n, std::vector< Node >& c ) { } } -bool TheoryStrings::checkLengths() { +bool TheoryStrings::checkSimple() { bool addedLemma = false; eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); while( !eqcs_i.isFinished() ) { @@ -1709,14 +1723,14 @@ bool TheoryStrings::checkLengths() { //if n is concat, and //if n has not instantiatied the concat..length axiom //then, add lemma - if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) { // || n.getKind() == kind::STRING_CONCAT ){ + if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT || n.getKind()==kind::STRING_CHARAT || n.getKind()==kind::STRING_SUBSTR ) { if( d_length_nodes.find(n)==d_length_nodes.end() ) { if( d_length_inst.find(n)==d_length_inst.end() ) { - Node nr = d_equalityEngine.getRepresentative( n ); + //Node nr = d_equalityEngine.getRepresentative( n ); //if( d_length_nodes.find(nr)==d_length_nodes.end() ) { d_length_inst[n] = true; Trace("strings-debug") << "get n: " << n << endl; - Node sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for concat lemma" ); + Node sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for length" ); d_length_intro_vars.push_back( sk ); Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, n ); eq = Rewriter::rewrite(eq); @@ -1731,10 +1745,41 @@ bool TheoryStrings::checkLengths() { Node lni = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[i] ); node_vec.push_back(lni); } - lsum = NodeManager::currentNM()->mkNode( kind::PLUS, node_vec ); - } else { + lsum = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::PLUS, node_vec ) ); + } else if( n.getKind() == kind::CONST_STRING ) { //add lemma lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst().size() ) ); + } else if( n.getKind() == kind::STRING_CHARAT ) { + lsum = d_one; + Node sk1 = NodeManager::currentNM()->mkSkolem( "ca1_$$", NodeManager::currentNM()->stringType(), "created for charat" ); + Node sk3 = NodeManager::currentNM()->mkSkolem( "ca3_$$", NodeManager::currentNM()->stringType(), "created for charat" ); + Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT, + NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ), n[1] ); + Node t1greq0 = NodeManager::currentNM()->mkNode( kind::GEQ, n[1], d_zero); + Node x_eq_123 = n[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk, sk3 ) ); + Node len_sk1_eq_i = n[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) ); + Node lemma = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i ); + lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::IMPLIES, lenxgti, lemma ) ); + Trace("strings-lemma") << "Strings::Lemma CHARAT : " << lemma << std::endl; + d_out->lemma(lemma); + } else if( n.getKind() == kind::STRING_SUBSTR ) { + lsum = n[2]; + Node sk1 = NodeManager::currentNM()->mkSkolem( "st1_$$", NodeManager::currentNM()->stringType(), "created for substr" ); + Node sk3 = NodeManager::currentNM()->mkSkolem( "st3_$$", NodeManager::currentNM()->stringType(), "created for substr" ); + Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, + NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ), + NodeManager::currentNM()->mkNode( kind::PLUS, n[1], n[2] ) ); + Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[1], d_zero); + Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[2], d_zero); + Node x_eq_123 = n[0].eqNode(NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk, sk3 )); + Node len_sk1_eq_i = NodeManager::currentNM()->mkNode( kind::EQUAL, n[1], + NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) ); + + Node lemma = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i ); + Node cond = NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ); + lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::IMPLIES, cond, lemma ) ); + Trace("strings-lemma") << "Strings::Lemma SUBSTR : " << lemma << std::endl; + d_out->lemma(lemma); } Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum ); ceq = Rewriter::rewrite(ceq); @@ -2366,8 +2411,8 @@ bool TheoryStrings::checkNegContains() { 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("bj", NodeManager::currentNM()->integerType()); - Node s2 = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT_TOTAL, x, NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 )); - Node s5 = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT_TOTAL, s, b2); + Node s2 = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT, x, NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 )); + Node s5 = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT, s, b2); Node s1 = NodeManager::currentNM()->mkBoundVar("s1", NodeManager::currentNM()->stringType()); Node s3 = NodeManager::currentNM()->mkBoundVar("s3", NodeManager::currentNM()->stringType()); diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 1dae73360..d15a76aad 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -221,7 +221,7 @@ private: int processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj, unsigned& index, bool isRev ); bool unrollStar( Node atom ); - bool checkLengths(); + bool checkSimple(); bool checkNormalForms(); bool checkLengthsEqc(); bool checkCardinality(); diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 00d02e015..ae5303d9d 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -27,6 +27,9 @@ StringsPreprocess::StringsPreprocess() { std::vector< TypeNode > argTypes; argTypes.push_back(NodeManager::currentNM()->stringType()); argTypes.push_back(NodeManager::currentNM()->integerType()); + + //Constants + d_zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ); } void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret, std::vector< Node > &nn ) { @@ -134,7 +137,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { std::vector< Node > vec; for(int i=0; imkConst( ::CVC4::Rational(i) ); - Node sk = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT_TOTAL, t[v_id][0], num); + Node sk = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT, t[v_id][0], num); vec.push_back(sk); } Node lem = t[v_id][0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, vec ) ); @@ -161,27 +164,6 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { // TODO // return (t0 == t[0]) ? t : NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, t0, t[1] ); //} - } else if( t.getKind() == kind::STRING_SUBSTR_TOTAL ){ - Node sk1 = NodeManager::currentNM()->mkSkolem( "st1_$$", NodeManager::currentNM()->stringType(), "created for substr" ); - Node sk2 = NodeManager::currentNM()->mkSkolem( "st2_$$", NodeManager::currentNM()->stringType(), "created for substr" ); - Node sk3 = NodeManager::currentNM()->mkSkolem( "st3_$$", NodeManager::currentNM()->stringType(), "created for substr" ); - Node x = simplify( t[0], new_nodes ); - Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, - NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x ), - NodeManager::currentNM()->mkNode( kind::PLUS, t[1], t[2] ) ); - Node x_eq_123 = NodeManager::currentNM()->mkNode( kind::EQUAL, - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 ), x ); - Node len_sk1_eq_i = NodeManager::currentNM()->mkNode( kind::EQUAL, t[1], - NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) ); - Node len_sk2_eq_j = NodeManager::currentNM()->mkNode( kind::EQUAL, t[2], - NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ) ); - - Node tp = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, len_sk2_eq_j ); - tp = NodeManager::currentNM()->mkNode( kind::IMPLIES, lenxgti, tp ); - new_nodes.push_back( tp ); - - d_cache[t] = sk2; - retNode = sk2; } else if( t.getKind() == kind::STRING_STRIDOF ){ if(options::stringExp()) { Node sk1 = NodeManager::currentNM()->mkSkolem( "io1_$$", t[0].getType(), "created for indexof" ); @@ -228,7 +210,6 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { } } else if( t.getKind() == kind::STRING_STRREPL ){ if(options::stringExp()) { - Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ); Node x = t[0]; Node y = t[1]; Node z = t[2]; @@ -248,23 +229,6 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { } else { throw LogicException("string replace not supported in this release"); } - } else if(t.getKind() == kind::STRING_CHARAT) { - Node sk2 = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT_TOTAL, t[0], t[1]); - Node sk1 = NodeManager::currentNM()->mkSkolem( "ca1_$$", NodeManager::currentNM()->stringType(), "created for charat" ); - Node sk3 = NodeManager::currentNM()->mkSkolem( "ca3_$$", NodeManager::currentNM()->stringType(), "created for charat" ); - Node x = simplify( t[0], new_nodes ); - Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT, - NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x ), t[1] ); - Node x_eq_123 = x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 ) ); - Node len_sk1_eq_i = t[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) ); - Node tp = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i ); - tp = NodeManager::currentNM()->mkNode( kind::IMPLIES, lenxgti, tp ); - new_nodes.push_back( tp ); - - d_cache[t] = sk2; - retNode = sk2; - } else if(t.getKind() == kind::STRING_SUBSTR) { - InternalError("Substr should not be reached here."); } else if( t.getNumChildren()>0 ) { std::vector< Node > cc; if (t.getMetaKind() == kind::metakind::PARAMETERIZED) { diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index 99312ddc0..630c7595c 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -31,6 +31,7 @@ namespace strings { class StringsPreprocess { // NOTE: this class is NOT context-dependent std::hash_map d_cache; + Node d_zero; private: bool checkStarPlus( Node t ); int checkFixLenVar( Node t ); diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 86af2ffa8..ddfe1a39c 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -323,22 +323,28 @@ 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_CHARAT_TOTAL) { + } else if(node[0].getKind() == kind::STRING_CHARAT) { retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 1 ) ); + } 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_CHARAT_TOTAL) { + } else if(tmpNode.getKind() == kind::STRING_CHARAT) { retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 1 ) ); + } else if(tmpNode.getKind() == kind::STRING_SUBSTR) { + retNode = tmpNode[2]; } else { // it has to be string concat std::vector node_vec; for(unsigned int i=0; imkConst( ::CVC4::Rational( tmpNode[i].getConst().size() ) ) ); - } else if(tmpNode[i].getKind() == kind::STRING_CHARAT_TOTAL) { + } else if(tmpNode[i].getKind() == kind::STRING_CHARAT) { node_vec.push_back( NodeManager::currentNM()->mkConst( ::CVC4::Rational( 1 ) ) ); + } 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]) ); } @@ -346,7 +352,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { retNode = NodeManager::currentNM()->mkNode(kind::PLUS, node_vec); } } - } else if(node.getKind() == kind::STRING_SUBSTR_TOTAL) { + } else if(node.getKind() == kind::STRING_SUBSTR) { if( node[0].isConst() && node[1].isConst() && node[2].isConst() ) { int i = node[1].getConst().getNumerator().toUnsignedInt(); int j = node[2].getConst().getNumerator().toUnsignedInt(); @@ -366,7 +372,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { retNode = NodeManager::currentNM()->mkConst( false ); } } - } else if(node.getKind() == kind::STRING_CHARAT || node.getKind() == kind::STRING_CHARAT_TOTAL) { + } else if(node.getKind() == kind::STRING_CHARAT) { if( node[0].isConst() && node[1].isConst() ) { int i = node[1].getConst().getNumerator().toUnsignedInt(); if( node[0].getConst().size() > (unsigned) i ) { diff --git a/test/regress/regress0/strings/substr001.smt2 b/test/regress/regress0/strings/substr001.smt2 index 476b82699..bdfa33afb 100644 --- a/test/regress/regress0/strings/substr001.smt2 +++ b/test/regress/regress0/strings/substr001.smt2 @@ -7,6 +7,8 @@ (declare-fun i3 () Int) (declare-fun i4 () Int) +(assert (and (>= i1 0) (>= i2 0) (< (+ i1 i2) (str.len x)))) +(assert (and (>= i3 0) (>= i4 0) (< (+ i3 i4) (str.len x)))) (assert (= "efg" (str.substr x i1 i2) ) ) (assert (= "bef" (str.substr x i3 i4) ) ) (assert (> (str.len x) 5)) -- 2.30.2