From: Tianyi Liang Date: Mon, 20 Jan 2014 22:45:11 +0000 (-0600) Subject: improve string contains X-Git-Tag: cvc5-1.0.0~7140 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8c0f9af1769883a10ccb2c9e864800e4c57181c2;p=cvc5.git improve string contains --- diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index ac50ed21d..231173058 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -44,6 +44,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_length_nodes(c), //d_var_lmin( c ), //d_var_lmax( c ), + d_charAtUF(), d_str_pos_ctn( c ), d_str_neg_ctn( c ), d_reg_exp_mem( c ), @@ -380,13 +381,13 @@ void TheoryStrings::preRegisterTerm(TNode n) { //d_equalityEngine.addTriggerPredicate(n); break; default: - if(n.getType().isString() && (n.getKind() == kind::VARIABLE || n.getKind()==kind::SKOLEM)) { + if(n.getType().isString() && n.getKind() != kind::CONST_STRING && n.getKind()!=kind::STRING_CONCAT ) { if( std::find( d_length_intro_vars.begin(), d_length_intro_vars.end(), n )==d_length_intro_vars.end() ) { Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n); Node n_len_eq_z = n_len.eqNode( d_zero ); 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 geq 0 : " << n_len_geq_zero << std::endl; + 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 ); } @@ -712,7 +713,7 @@ bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std } std::vector< Node > empty_vec; Node conc = cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( kind::AND, cc ); - sendLemma( mkExplain( ant ), conc, "Component" ); + sendLemma( mkExplain( ant ), conc, "COMPONENT" ); return true; } } @@ -983,7 +984,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms if(index_i==normal_forms[i].size() || index_j==normal_forms[j].size() ) { if( index_i==normal_forms[i].size() && index_j==normal_forms[j].size() ) { //we're done - addNormalFormPair( normal_form_src[i], normal_form_src[j] ); + //addNormalFormPair( normal_form_src[i], normal_form_src[j] ); } else { //the remainder must be empty unsigned k = index_i==normal_forms[i].size() ? j : i; @@ -1069,7 +1070,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms eqn.push_back( mkConcat( eqnc ) ); } if( areEqual( eqn[0], eqn[1] ) ) { - addNormalFormPair( normal_form_src[i], normal_form_src[j] ); + //addNormalFormPair( normal_form_src[i], normal_form_src[j] ); } else { conc = eqn[0].eqNode( eqn[1] ); Node ant = mkExplain( antec ); @@ -1341,6 +1342,8 @@ bool TheoryStrings::normalizeDisequality( Node ni, Node nj ) { Node li = getLength( i ); Node lj = getLength( j ); if( areDisequal(li, lj) ){ + //if( i.getKind()==kind::CONST_STRING || j.getKind()==kind::CONST_STRING ){ + Trace("strings-solve") << "Case 2 : add lemma " << std::endl; //must add lemma std::vector< Node > antec; @@ -1459,14 +1462,14 @@ void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) { } } -void TheoryStrings::sendSplit( Node a, Node b, const char * c ) { +void TheoryStrings::sendSplit( Node a, Node b, const char * c, bool preq ) { Node eq = a.eqNode( b ); eq = Rewriter::rewrite( eq ); Node neq = NodeManager::currentNM()->mkNode( kind::NOT, eq ); Node lemma_or = NodeManager::currentNM()->mkNode( kind::OR, eq, neq ); Trace("strings-lemma") << "Strings::Lemma " << c << " SPLIT : " << lemma_or << std::endl; d_lemma_cache.push_back(lemma_or); - d_pending_req_phase[eq] = true; + d_pending_req_phase[eq] = preq; } Node TheoryStrings::mkConcat( Node n1, Node n2 ) { @@ -1566,14 +1569,14 @@ bool TheoryStrings::checkLengths() { 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 ); - if( d_length_nodes.find(nr)==d_length_nodes.end() ) { + //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" ); d_length_intro_vars.push_back( sk ); Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, n ); eq = Rewriter::rewrite(eq); - Trace("strings-lemma") << "Strings::Lemma LENGTH term : " << eq << std::endl; + Trace("strings-lemma") << "Strings::Lemma LENGTH Term : " << eq << std::endl; d_out->lemma(eq); Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ); Node lsum; @@ -1594,7 +1597,7 @@ bool TheoryStrings::checkLengths() { Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq << std::endl; d_out->lemma(ceq); addedLemma = true; - } + //} } d_length_nodes[n] = true; } @@ -1707,7 +1710,7 @@ bool TheoryStrings::checkNormalForms() { if( nf_to_eqc.find(nf_term)!=nf_to_eqc.end() ){ //Trace("strings-debug") << "Merge because of normal form : " << eqc << " and " << nf_to_eqc[nf_term] << " both have normal form " << nf_term << std::endl; //two equivalence classes have same normal form, merge - Node eq_exp = NodeManager::currentNM()->mkNode( kind::AND, nf_term_exp, eqc_to_exp[nf_to_eqc[nf_term]] ); + Node eq_exp = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, nf_term_exp, eqc_to_exp[nf_to_eqc[nf_term]] ) ); Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, eqc, nf_to_eqc[nf_term] ); Trace("strings-lemma") << "Strings (by normal forms) : Infer " << eq << " from " << eq_exp << std::endl; //d_equalityEngine.assertEquality( eq, true, eq_exp ); @@ -1744,17 +1747,22 @@ bool TheoryStrings::checkNormalForms() { Trace("strings-solve") << "- Verify disequalities are processed for "; printConcat( d_normal_forms[cols[i][0]], "strings-solve" ); Trace("strings-solve") << "..." << std::endl; + //must ensure that normal forms are disequal - for( unsigned j=1; jd_normalized_length.set( eq ); - sendLemma( mkExplain( ant ), eq, "Length Normalization" ); + sendLemma( mkExplain( ant ), eq, "LEN-NORM" ); addedLemma = true; } } @@ -1835,7 +1843,7 @@ bool TheoryStrings::checkCardinality() { if(!d_equalityEngine.areDisequal( *itr1, *itr2, false )) { allDisequal = false; // add split lemma - sendSplit( *itr1, *itr2, "Cardinality" ); + sendSplit( *itr1, *itr2, "CARD-SP" ); doPendingLemmas(); return true; } @@ -1872,7 +1880,7 @@ bool TheoryStrings::checkCardinality() { lemma = Rewriter::rewrite( lemma ); ei->d_cardinality_lem_k.set( int_k+1 ); if( lemma!=d_true ){ - Trace("strings-lemma") << "Strings cardinality lemma : " << lemma << std::endl; + Trace("strings-lemma") << "Strings::Lemma CARDINALITY : " << lemma << std::endl; d_out->lemma(lemma); return true; } @@ -2213,100 +2221,55 @@ bool TheoryStrings::checkNegContains() { addedLemma = true; } else { if(d_str_neg_ctn_rewritten.find(atom) == d_str_neg_ctn_rewritten.end()) { - /*std::vector< TypeNode > argTypes; - argTypes.push_back(NodeManager::currentNM()->stringType()); - argTypes.push_back(NodeManager::currentNM()->integerType()); - Node d_charAtUF = NodeManager::currentNM()->mkSkolem("charAt", - NodeManager::currentNM()->mkFunctionType( - argTypes, - NodeManager::currentNM()->stringType()), - "total charat", - NodeManager::SKOLEM_EXACT_NAME);*/ - /* - Node e1 = NodeManager::currentNM()->mkSkolem( "nc1_$$", s.getType(), "created for contain" ); - Node e2 = NodeManager::currentNM()->mkSkolem( "nc2_$$", s.getType(), "created for contain" ); - Node z = NodeManager::currentNM()->mkSkolem( "ncz_$$", s.getType(), "created for contain" ); - Node w = NodeManager::currentNM()->mkSkolem( "ncw_$$", s.getType(), "created for contain" ); - std::vector< Node > vec_conc; - Node cc = Rewriter::rewrite( x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, e1, z ) ) ); - vec_conc.push_back(cc); - cc = Rewriter::rewrite( x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, w, e2 ) ) ); - vec_conc.push_back(cc); - cc = Rewriter::rewrite( z.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, s, e2 ) ).negate() ); - vec_conc.push_back(cc); - cc = Rewriter::rewrite( w.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, e1, s ) ).negate() ); - vec_conc.push_back(cc); - cc = Rewriter::rewrite( lenx.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, e1, s, e2 ) ) ) ); - vec_conc.push_back(cc); - //Incomplete - //cc = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, e1, s ).negate(); - //vec_conc.push_back(cc); - //cc = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, e2, s ).negate(); - //vec_conc.push_back(cc); - Node conc = NodeManager::currentNM()->mkNode( kind::AND, vec_conc ); - */ - //x[i+j] != y[j] - /*Node conc = NodeManager::currentNM()->mkNode( kind::STRING_CHARAT, x , NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 ) ).eqNode( - NodeManager::currentNM()->mkNode( kind::STRING_CHARAT, s , b2) ).negate(); - Node conc = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_charAtUF, x, NodeManager::currentNM()->mkNode(kind::PLUS, b1, b2)).eqNode( - NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_charAtUF, s , b2)).negate(); - conc = NodeManager::currentNM()->mkNode( kind::AND, g2, conc ); - conc = NodeManager::currentNM()->mkNode( kind::EXISTS, b2v, conc ); - conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, g1, conc ); - conc = NodeManager::currentNM()->mkNode( kind::FORALL, b1v, conc ); - Node xlss = NodeManager::currentNM()->mkNode( kind::GT, lens, lenx ); - conc = NodeManager::currentNM()->mkNode( kind::OR, xlss, conc ); - */ Node b1 = NodeManager::currentNM()->mkBoundVar("bi", NodeManager::currentNM()->integerType()); Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1); 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 d_charAtUF; - std::vector< TypeNode > 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); - Node s2 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_charAtUF, x, NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 )); - Node s5 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_charAtUF, s, b2); - - Node s1 = NodeManager::currentNM()->mkBoundVar("s1", NodeManager::currentNM()->stringType()); - Node s3 = NodeManager::currentNM()->mkBoundVar("s3", NodeManager::currentNM()->stringType()); - Node s4 = NodeManager::currentNM()->mkBoundVar("s4", NodeManager::currentNM()->stringType()); - Node s6 = NodeManager::currentNM()->mkBoundVar("s6", NodeManager::currentNM()->stringType()); - Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b2, s1, s3, s4, s6); - - std::vector< Node > vec_nodes; - Node cc = NodeManager::currentNM()->mkNode( kind::GEQ, b2, d_zero ); - vec_nodes.push_back(cc); - cc = NodeManager::currentNM()->mkNode( kind::GEQ, lens, b2 ); - vec_nodes.push_back(cc); - - cc = x.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s1, s2, s3)); - vec_nodes.push_back(cc); - cc = s.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s4, s5, s6)); - vec_nodes.push_back(cc); - cc = s2.eqNode(s5).negate(); - vec_nodes.push_back(cc); - cc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s2).eqNode(NodeManager::currentNM()->mkConst( Rational(1))); - vec_nodes.push_back(cc); - cc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s5).eqNode(NodeManager::currentNM()->mkConst( Rational(1))); - vec_nodes.push_back(cc); - cc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s1).eqNode(NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 )); - vec_nodes.push_back(cc); - cc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s4).eqNode(b2); - vec_nodes.push_back(cc); - - Node conc = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, vec_nodes) ); + if(d_charAtUF.isNull()) { + std::vector< TypeNode > 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); + } + Node s2 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_charAtUF, x, NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 )); + Node s5 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_charAtUF, s, b2); + + Node s1 = NodeManager::currentNM()->mkBoundVar("s1", NodeManager::currentNM()->stringType()); + Node s3 = NodeManager::currentNM()->mkBoundVar("s3", NodeManager::currentNM()->stringType()); + Node s4 = NodeManager::currentNM()->mkBoundVar("s4", NodeManager::currentNM()->stringType()); + Node s6 = NodeManager::currentNM()->mkBoundVar("s6", NodeManager::currentNM()->stringType()); + Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b2, s1, s3, s4, s6); + + std::vector< Node > vec_nodes; + Node cc = NodeManager::currentNM()->mkNode( kind::GEQ, b2, d_zero ); + vec_nodes.push_back(cc); + cc = NodeManager::currentNM()->mkNode( kind::GEQ, lens, b2 ); + vec_nodes.push_back(cc); + + cc = x.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s1, s2, s3)); + vec_nodes.push_back(cc); + cc = s.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s4, s5, s6)); + vec_nodes.push_back(cc); + cc = s2.eqNode(s5).negate(); + vec_nodes.push_back(cc); + cc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s2).eqNode(NodeManager::currentNM()->mkConst( Rational(1))); + vec_nodes.push_back(cc); + cc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s5).eqNode(NodeManager::currentNM()->mkConst( Rational(1))); + vec_nodes.push_back(cc); + cc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s1).eqNode(NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 )); + vec_nodes.push_back(cc); + cc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s4).eqNode(b2); + 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 ); - //conc = NodeManager::currentNM()->mkNode( kind::AND, g2, conc ); conc = NodeManager::currentNM()->mkNode( kind::EXISTS, b2v, conc ); conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, g1, conc ); conc = NodeManager::currentNM()->mkNode( kind::FORALL, b1v, conc ); @@ -2420,13 +2383,13 @@ bool TheoryStrings::splitRegExp( Node x, Node r, Node ant ) { spp.simplify( sdc ); for( unsigned i=1; imkNode( kind::OR, lit, lit.negate() ); - Trace("strings-fmf") << "Strings FMF: Add split lemma " << lem << ", decideCard = " << decideCard << std::endl; + Trace("strings-fmf") << "Strings::FMF: Add decision lemma " << lem << ", decideCard = " << decideCard << std::endl; d_out->lemma( lem ); d_out->requirePhase( lit, true ); } - Trace("strings-fmf") << "Strings FMF: Decide positive on " << d_cardinality_lits[ decideCard ] << std::endl; + Trace("strings-fmf") << "Strings::FMF: Decide positive on " << d_cardinality_lits[ decideCard ] << std::endl; return d_cardinality_lits[ decideCard ]; } } @@ -2499,7 +2462,7 @@ Node TheoryStrings::mkSplitEq( const char * c, const char * info, Node lhs, Node if( lgtZero ) { d_var_lgtz[sk] = true; Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, d_emptyString).negate(); - Trace("strings-lemma") << "Strings::Lemma sk GT zero: " << sk_gt_zero << std::endl; + Trace("strings-lemma") << "Strings::Lemma SK-NON-EMPTY: " << sk_gt_zero << std::endl; d_lemma_cache.push_back( sk_gt_zero ); } //store it in proper map diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 6b4899c80..c0a979cb0 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -245,7 +245,7 @@ protected: void doPendingLemmas(); void sendLemma( Node ant, Node conc, const char * c ); - void sendSplit( Node a, Node b, const char * c ); + void sendSplit( Node a, Node b, const char * c, bool preq = true ); /** mkConcat **/ Node mkConcat( Node n1, Node n2 ); Node mkConcat( std::vector< Node >& c ); @@ -275,6 +275,7 @@ private: int getMaxPossibleLength( Node x ); // Special String Functions + Node d_charAtUF; NodeList d_str_pos_ctn; NodeList d_str_neg_ctn; std::map< Node, bool > d_str_ctn_eqlen; diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 7edddbe76..d53382c82 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -24,6 +24,15 @@ namespace theory { namespace strings { StringsPreprocess::StringsPreprocess() { + std::vector< TypeNode > 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); } void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret, std::vector< Node > &nn ) { @@ -91,7 +100,21 @@ bool StringsPreprocess::checkStarPlus( Node t ) { return true; } } - +int StringsPreprocess::checkFixLenVar( Node t ) { + int ret = 2; + if(t.getKind() == kind::EQUAL) { + if(t[0].getType().isInteger() && t[0].isConst() && t[1].getKind() == kind::STRING_LENGTH) { + if(t[1][0].getKind() == kind::VARIABLE) { + ret = 0; + } + } else if(t[1].getType().isInteger() && t[1].isConst() && t[0].getKind() == kind::STRING_LENGTH) { + if(t[0][0].getKind() == kind::VARIABLE) { + ret = 1; + } + } + } + return ret; +} Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { std::hash_map::const_iterator i = d_cache.find(t); if(i != d_cache.end()) { @@ -100,7 +123,27 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Trace("strings-preprocess") << "StringsPreprocess::simplify: " << t << std::endl; Node retNode = t; - if( t.getKind() == kind::STRING_IN_REGEXP ) { + int c_id = checkFixLenVar(t); + if( c_id != 2 ) { + int v_id = 1 - c_id; + int len = t[c_id].getConst().getNumerator().toUnsignedInt(); + Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) ); + std::vector< Node > vec; + for(int i=0; imkSkolem( "fl_$$", NodeManager::currentNM()->stringType(), "created for fixed length" ); + Node num = NodeManager::currentNM()->mkConst( ::CVC4::Rational(i) ); + Node sk = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_charAtUF, t[v_id][0], num); + vec.push_back(sk); + Node lem = one.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ) ); + new_nodes.push_back( lem ); + } + Node lem = t[v_id][0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, vec ) ); + lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, t, lem ); + new_nodes.push_back( lem ); + + d_cache[t] = t; + retNode = t; + } else if( t.getKind() == kind::STRING_IN_REGEXP ) { // t0 in t1 Node t0 = simplify( t[0], new_nodes ); @@ -227,31 +270,20 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { throw LogicException("string replace not supported in this release"); } } else if(t.getKind() == kind::STRING_CHARAT) { - Node d_charAtUF; - std::vector< TypeNode > 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); Node sk2 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_charAtUF, 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 = 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 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 ); Node len_sk2_eq_1 = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkConst( Rational( 1 ) ), NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ) ); + tp = NodeManager::currentNM()->mkNode( kind::AND, len_sk2_eq_1, tp ); - Node tp = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, len_sk2_eq_1 ); - tp = NodeManager::currentNM()->mkNode( kind::IMPLIES, lenxgti, tp ); new_nodes.push_back( tp ); d_cache[t] = sk2; diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index 6d278cc7a..4610a300d 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -30,8 +30,10 @@ namespace strings { class StringsPreprocess { // NOTE: this class is NOT context-dependent std::hash_map d_cache; + Node d_charAtUF; private: bool checkStarPlus( Node t ); + int checkFixLenVar( Node t ); void simplifyRegExp( Node s, Node r, std::vector< Node > &ret, std::vector< Node > &nn ); Node simplify( Node t, std::vector< Node > &new_nodes ); public: