From 2fda1f59b3f5c5d0d6d9b36ae206b8984fb6064c Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Fri, 31 Jan 2014 12:22:07 -0600 Subject: [PATCH] Substr fix: (= (str.substr "" 0 3) "xxx") should be SAT in the defintion of SMT-Lib --- src/theory/strings/theory_strings.cpp | 57 +++++++++--------- src/theory/strings/theory_strings.h | 2 +- .../strings/theory_strings_preprocess.cpp | 60 +++++++++++++++++-- .../strings/theory_strings_preprocess.h | 2 + 4 files changed, 89 insertions(+), 32 deletions(-) diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index d0876d983..58344964c 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); - d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR); + //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 ) ); @@ -1725,20 +1725,6 @@ void TheoryStrings::getConcatVec( Node n, std::vector< Node >& c ) { bool TheoryStrings::checkSimple() { bool addedLemma = false; - //Initialize UF - if(d_undefSubstr.isNull()) { - std::vector< TypeNode > argTypes; - argTypes.push_back(NodeManager::currentNM()->stringType()); - argTypes.push_back(NodeManager::currentNM()->integerType()); - argTypes.push_back(NodeManager::currentNM()->integerType()); - d_undefSubstr = NodeManager::currentNM()->mkSkolem("__undefSS", - NodeManager::currentNM()->mkFunctionType( - argTypes, NodeManager::currentNM()->stringType()), - "undefined substr", - NodeManager::SKOLEM_EXACT_NAME); - } - - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); while( !eqcs_i.isFinished() ) { Node eqc = (*eqcs_i); @@ -1780,7 +1766,7 @@ 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 ) { + } /*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" ); @@ -1788,12 +1774,11 @@ bool TheoryStrings::checkSimple() { 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 cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1greq0 )); Node lemma = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i ); - Node uf = sk.eqNode( NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_undefSubstr, n[0], n[1], d_one)); - lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond, lemma, uf) ); + 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 ) { @@ -1807,16 +1792,14 @@ bool TheoryStrings::checkSimple() { 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 cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 )); 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 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 )); - Node uf = sk.eqNode( NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_undefSubstr, n[0], n[1], n[2])); - lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond, lemma, uf ) ); + 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); Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq << std::endl; @@ -2409,6 +2392,18 @@ 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::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 s1 = NodeManager::currentNM()->mkBoundVar("s1", NodeManager::currentNM()->stringType()); Node s3 = NodeManager::currentNM()->mkBoundVar("s3", NodeManager::currentNM()->stringType()); @@ -2476,6 +2473,12 @@ bool TheoryStrings::checkNegContains() { cc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s4).eqNode(b2); vec_nodes.push_back(cc); + // charAt length + cc = d_one.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s2)); + vec_nodes.push_back(cc); + cc = d_one.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s5)); + vec_nodes.push_back(cc); + Node conc = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, vec_nodes) ); Node xlss = NodeManager::currentNM()->mkNode( kind::GT, lens, lenx ); conc = NodeManager::currentNM()->mkNode( kind::OR, xlss, conc ); diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 05e6ebf71..5d8ff016f 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -115,7 +115,7 @@ private: Node d_false; Node d_zero; Node d_one; - Node d_undefSubstr; + 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 ae5303d9d..707fae459 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -127,18 +127,35 @@ 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); + /*int c_id = checkFixLenVar(t); if( c_id != 2 ) { int v_id = 1 - c_id; int len = t[c_id].getConst().getNumerator().toUnsignedInt(); if(len > 1) { + Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) ); std::vector< Node > vec; for(int i=0; imkConst( ::CVC4::Rational(i) ); - Node sk = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT, t[v_id][0], num); + //Node sk = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT, t[v_id][0], num); + Node sk = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, t[v_id][0], num, one); vec.push_back(sk); + Node cc = one.eqNode(NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk )); + new_nodes.push_back( cc ); } Node lem = t[v_id][0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, vec ) ); lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, t, lem ); @@ -146,7 +163,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { d_cache[t] = t; retNode = t; } - } else if( t.getKind() == kind::STRING_IN_REGEXP ) { + } else */if( t.getKind() == kind::STRING_IN_REGEXP ) { // t0 in t1 Node t0 = simplify( t[0], new_nodes ); @@ -164,7 +181,42 @@ 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_STRIDOF ){ + } 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 ) { + 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 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 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_STRIDOF ) { if(options::stringExp()) { Node sk1 = NodeManager::currentNM()->mkSkolem( "io1_$$", t[0].getType(), "created for indexof" ); Node sk2 = NodeManager::currentNM()->mkSkolem( "io2_$$", 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 630c7595c..a8074861e 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -31,7 +31,9 @@ namespace strings { class StringsPreprocess { // NOTE: this class is NOT context-dependent std::hash_map d_cache; + //Constants Node d_zero; + Node d_ufSubstr; private: bool checkStarPlus( Node t ); int checkFixLenVar( Node t ); -- 2.30.2