From 6f6708083a6b57243fd59ceb1a783ad65b086550 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Thu, 13 Feb 2014 18:08:49 -0600 Subject: [PATCH] fix expanding def --- src/smt/smt_engine.cpp | 52 +++++++++++++++++-- src/theory/strings/kinds | 2 + src/theory/strings/theory_strings.cpp | 51 ++++-------------- src/theory/strings/theory_strings.h | 1 - .../strings/theory_strings_preprocess.cpp | 43 +++------------ .../strings/theory_strings_preprocess.h | 1 - .../strings/theory_strings_rewriter.cpp | 25 +++------ 7 files changed, 71 insertions(+), 104 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8754dc084..ef4f01cd1 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -310,7 +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_substrUndef; + Node d_ufSubstr; /** * Function symbol used to implement uninterpreted division-by-zero @@ -1555,9 +1555,53 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map 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, n[0] ), n[1] ); + Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ); + Node t1greq0 = NodeManager::currentNM()->mkNode( kind::GEQ, n[1], zero); + Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1greq0 )); + Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) ); + Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, n[0], n[1], one); + Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, n[0], n[1], one); + node = NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf ); + 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, n[0] ), + NodeManager::currentNM()->mkNode( kind::PLUS, n[1], n[2] ) ); + Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ); + Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[1], zero); + Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[2], zero); + Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 )); + Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, n[0], n[1], n[2]); + Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, n[0], n[1], n[2]); + node = NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf ); + break; + } case kind::DIVISION: { // partial function: division if(d_divByZero.isNull()) { diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index b3a75a560..7d631e826 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -14,6 +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_STRCTN 2 "string contains" operator STRING_STRIDOF 3 "string indexof" @@ -107,6 +108,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_STRCTN ::CVC4::theory::strings::StringContainTypeRule typerule STRING_STRIDOF ::CVC4::theory::strings::StringIndexOfTypeRule diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index f1b6c133a..0b4fe80c5 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -54,8 +54,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_CHARAT); - //d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR); + d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR_TOTAL); d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); @@ -404,12 +403,9 @@ void TheoryStrings::preRegisterTerm(TNode n) { break; case kind::CONST_STRING: case kind::STRING_CONCAT: + case kind::STRING_SUBSTR_TOTAL: d_equalityEngine.addTerm(n); break; - case kind::STRING_CHARAT: - case kind::STRING_SUBSTR: - //d_equalityEngine.addTerm(n); - break; default: if(n.getType().isString() ) { if( std::find( d_length_intro_vars.begin(), d_length_intro_vars.end(), n )==d_length_intro_vars.end() ) { @@ -1761,7 +1757,7 @@ bool TheoryStrings::checkSimple() { //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_CHARAT || n.getKind()==kind::STRING_SUBSTR ) { + if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT || n.getKind()==kind::STRING_SUBSTR_TOTAL ) { 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 ); @@ -1788,23 +1784,8 @@ bool TheoryStrings::checkSimple() { } 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" ); - d_statistics.d_new_skolems += 2; - 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 cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1greq0 )); - 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, cond, lemma ) ); - Trace("strings-lemma") << "Strings::Lemma CHARAT : " << lemma << std::endl; - d_out->lemma(lemma); - } else if( n.getKind() == kind::STRING_SUBSTR ) { - lsum = n[2]; + } else if( n.getKind() == kind::STRING_SUBSTR_TOTAL ) { + 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" ); d_statistics.d_new_skolems += 2; @@ -1820,8 +1801,8 @@ bool TheoryStrings::checkSimple() { Node lemma = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i ); lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::IMPLIES, cond, lemma ) ); Trace("strings-lemma") << "Strings::Lemma SUBSTR : " << lemma << std::endl; - d_out->lemma(lemma); - }*/ + d_out->lemma(lemma);*/ + } Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum ); ceq = Rewriter::rewrite(ceq); Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq << std::endl; @@ -2421,18 +2402,6 @@ bool TheoryStrings::checkPosContains() { } bool TheoryStrings::checkNegContains() { - //Initialize UF - 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); - } bool is_unk = false; bool addedLemma = false; for( unsigned i=0; imkNode( 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, x, NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 )); - //Node s5 = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT, s, b2); - Node s2 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, x, NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 ), d_one); - Node s5 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, s, b2, d_one); + 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 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 3143d6e89..73d7619db 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -115,7 +115,6 @@ private: Node d_false; Node d_zero; Node d_one; - Node d_ufSubstr; // Options bool d_all_warning; bool d_opt_fmf; diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 707fae459..1e2eb2572 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -127,19 +127,6 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { return (*i).second.isNull() ? t : (*i).second; } - //Initialize UF - 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); - } - Trace("strings-preprocess") << "StringsPreprocess::simplify: " << t << std::endl; Node retNode = t; /*int c_id = checkFixLenVar(t); @@ -181,41 +168,23 @@ 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_CHARAT ) { - Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT, - NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ), t[1] ); - Node t1greq0 = NodeManager::currentNM()->mkNode( kind::GEQ, t[1], d_zero); - Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1greq0 )); - Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) ); - Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, t[0], t[1], one); - Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1_$$", NodeManager::currentNM()->stringType(), "created for charat/substr" ); - Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3_$$", NodeManager::currentNM()->stringType(), "created for charat/substr" ); - Node x_eq_123 = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, uf, sk3 ) ); - Node len_sk1_eq_i = t[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) ); - Node len_uf_eq_j = one.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, uf ) ); - Node lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::IMPLIES, cond, - NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, len_uf_eq_j )) ); - new_nodes.push_back( lemma ); - retNode = uf; - d_cache[t] = uf; - } else if( t.getKind() == kind::STRING_SUBSTR ) { + } else if( t.getKind() == kind::STRING_SUBSTR_TOTAL ) { Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ), NodeManager::currentNM()->mkNode( kind::PLUS, t[1], t[2] ) ); Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, t[1], d_zero); Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, t[2], d_zero); Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 )); - Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, t[0], t[1], t[2]); Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1_$$", NodeManager::currentNM()->stringType(), "created for charat/substr" ); Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3_$$", NodeManager::currentNM()->stringType(), "created for charat/substr" ); - Node x_eq_123 = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, uf, sk3 ) ); + Node x_eq_123 = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, t, sk3 ) ); Node len_sk1_eq_i = t[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) ); - Node len_uf_eq_j = t[2].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, uf ) ); + //Node len_uf_eq_j = t[2].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, uf ) ); Node lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::IMPLIES, cond, - NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, len_uf_eq_j )) ); + NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i )) ); new_nodes.push_back( lemma ); - retNode = uf; - d_cache[t] = uf; + retNode = t; + d_cache[t] = t; } else if( t.getKind() == kind::STRING_STRIDOF ) { if(options::stringExp()) { Node sk1 = NodeManager::currentNM()->mkSkolem( "io1_$$", t[0].getType(), "created for indexof" ); diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index a8074861e..7aa0a2af8 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -33,7 +33,6 @@ class StringsPreprocess { std::hash_map d_cache; //Constants Node d_zero; - Node d_ufSubstr; 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 1dc9cbe85..b08994927 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -323,17 +323,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_CHARAT) { - retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 1 ) ); - } else if(node[0].getKind() == kind::STRING_SUBSTR) { + } else if(node[0].getKind() == kind::STRING_SUBSTR_TOTAL) { 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) { - retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 1 ) ); - } else if(tmpNode.getKind() == kind::STRING_SUBSTR) { + } else if(tmpNode.getKind() == kind::STRING_SUBSTR_TOTAL) { retNode = tmpNode[2]; } else { // it has to be string concat @@ -341,9 +337,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_CHARAT) { - node_vec.push_back( NodeManager::currentNM()->mkConst( ::CVC4::Rational( 1 ) ) ); - } else if(tmpNode[i].getKind() == kind::STRING_SUBSTR) { + } else if(tmpNode[i].getKind() == kind::STRING_SUBSTR_TOTAL) { node_vec.push_back( tmpNode[i][2] ); } else { node_vec.push_back( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, tmpNode[i]) ); @@ -352,7 +346,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { retNode = NodeManager::currentNM()->mkNode(kind::PLUS, node_vec); } } - } else if(node.getKind() == kind::STRING_SUBSTR) { + } else if(node.getKind() == kind::STRING_SUBSTR_TOTAL) { Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ); if(node[2] == zero) { retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); @@ -375,13 +369,6 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { retNode = NodeManager::currentNM()->mkConst( false ); } } - } 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 ) { - retNode = NodeManager::currentNM()->mkConst( node[0].getConst().substr(i, 1) ); - } - } } else if(node.getKind() == kind::STRING_STRIDOF) { if( node[0].isConst() && node[1].isConst() && node[2].isConst() ) { CVC4::String s = node[0].getConst(); @@ -432,7 +419,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, node[1], + node[0].eqNode(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[1], NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ), lens))); } } else if(node.getKind() == kind::STRING_SUFFIX) { @@ -450,7 +437,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, node[1], + node[0].eqNode(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[1], NodeManager::currentNM()->mkNode(kind::MINUS, lent, lens), lens))); } } else if(node.getKind() == kind::STRING_IN_REGEXP) { -- 2.30.2