From: Tianyi Liang Date: Tue, 22 Oct 2013 03:08:53 +0000 (-0500) Subject: remove nested re or; opt loop X-Git-Tag: cvc5-1.0.0~7275^2~5 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d676b7e044b7a92377cb3d9bb7063faefb80d7f9;p=cvc5.git remove nested re or; opt loop --- diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 910447589..4cb5e0293 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -913,24 +913,34 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v Trace("strings-loop") << "Detected possible loop for " << normal_forms[loop_n_index][loop_index] << std::endl; Trace("strings-loop") << " ... (X)= " << normal_forms[other_n_index][other_index] << std::endl; + Trace("strings-loop") << " ... T(Y.Z)= "; + std::vector< Node > vec_t; for(int lp=index; lp & v //s1 * ... * sk = n[other_n_index][other_index+1].....n[other_n_index][k+1] = z * y // for some y,z,k - Trace("strings-loop") << "Must add lemma." << std::endl; - Trace("strings-loop") << "Cache: " << normal_form_src[i] << " vs " << normal_form_src[j] << std::endl; + Trace("strings-loop") << "Lemma Cache: " << normal_form_src[i] << " vs " << normal_form_src[j] << std::endl; + + if( s_zy.isConst() && r.isConst() && r != d_emptyString) { + int c; + bool flag = true; + if(s_zy.getConst().tailcmp( r.getConst(), c ) ) { + if(c >= 0) { + s_zy = NodeManager::currentNM()->mkConst( s_zy.getConst().substr(0, c + 1) ); + r = d_emptyString; + vec_r.clear(); + Trace("strings-loop") << "Refactor : S(Z.Y)= " << s_zy << ", c=" << c << std::endl; + flag = false; + } + } + if(flag) { + Trace("strings-loop") << "Loop different tail." << std::endl; + antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); + Node ant = mkExplain( antec, antec_new_lits ); + sendLemma( ant, conc, "Conflict" ); + return true; + } + } antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); //require that x is non-empty @@ -949,7 +979,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v //if( d_equalityEngine.hasTerm( d_emptyString ) && d_equalityEngine.areDisequal( normal_forms[loop_n_index][loop_index], d_emptyString, true ) ){ // antec.push_back( x_empty.negate() ); //}else{ - antec_new_lits.push_back( x_empty.negate() ); + //antec_new_lits.push_back( x_empty.negate() ); //} d_pending_req_phase[ x_empty ] = true; @@ -957,48 +987,33 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v //need to break Node ant = mkExplain( antec, antec_new_lits ); Node str_in_re; - if(index == loop_index - 1 && - other_index + 2 == (int) normal_forms[other_n_index].size() && - loop_index + 1 == (int) normal_forms[loop_n_index].size() && - normal_forms[loop_n_index][index] == normal_forms[other_n_index][other_index + 1] && - normal_forms[loop_n_index][index].isConst() && - normal_forms[loop_n_index][index].getConst().size() == 1 ) { + if( s_zy == t_yz && + r == d_emptyString && + s_zy.isConst() && + s_zy.getConst().isRepeated() + ) { + Node rep_c = NodeManager::currentNM()->mkConst( s_zy.getConst().substr(0, 1) ); Trace("strings-loop") << "Special case (X)=" << normal_forms[other_n_index][other_index] << " " << std::endl; - Trace("strings-loop") << "... (C)=" << normal_forms[loop_n_index][index] << " " << std::endl; + Trace("strings-loop") << "... (C)=" << rep_c << " " << std::endl; //special case //Node conc3 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], mkConcat( normal_forms[loop_n_index][index], sk_w ) ); str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, normal_forms[other_n_index][other_index], NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, - NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, normal_forms[loop_n_index][index] ) ) ); + NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, rep_c ) ) ); conc = str_in_re; } else { + Trace("strings-loop") << "...Normal Splitting." << std::endl; Node sk_w= NodeManager::currentNM()->mkSkolem( "w_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); Node sk_y= NodeManager::currentNM()->mkSkolem( "y_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); Node sk_z= NodeManager::currentNM()->mkSkolem( "z_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); //t1 * ... * tn = y * z - std::vector< Node > c1c; - //n[loop_n_index][index]....n[loop_n_index][loop_lindex-1] - for( int r=index; r<=loop_index-1; r++ ) { - c1c.push_back( normal_forms[loop_n_index][r] ); - } - Node conc1 = mkConcat( c1c ); - conc1 = NodeManager::currentNM()->mkNode( kind::EQUAL, conc1, + Node conc1 = NodeManager::currentNM()->mkNode( kind::EQUAL, t_yz, NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk_y, sk_z ) ); - std::vector< Node > c2c; - //s1 * ... * sk = n[other_n_index][other_index+1].....n[other_n_index][k+1] - for( int r=other_index+1; r < (int)normal_forms[other_n_index].size(); r++ ) { - c2c.push_back( normal_forms[other_n_index][r] ); - } - Node left2 = mkConcat( c2c ); - std::vector< Node > c3c; - c3c.push_back( sk_z ); - c3c.push_back( sk_y ); - //r1 * ... * rk = n[loop_n_index][loop_index+1]....n[loop_n_index][loop_index-1] - for( int r=loop_index+1; r < (int)normal_forms[loop_n_index].size(); r++ ) { - c3c.push_back( normal_forms[loop_n_index][r] ); - } - Node conc2 = NodeManager::currentNM()->mkNode( kind::EQUAL, left2, - mkConcat( c3c ) ); + // s1 * ... * sk = z * y * r + vec_r.insert(vec_r.begin(), sk_y); + vec_r.insert(vec_r.begin(), sk_z); + Node conc2 = NodeManager::currentNM()->mkNode( kind::EQUAL, s_zy, + mkConcat( vec_r ) ); Node conc3 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], mkConcat( sk_y, sk_w ) ); str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_w, NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, @@ -1030,9 +1045,10 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v //we will be done addNormalFormPair( normal_form_src[i], normal_form_src[j] ); //Assert( isNormalFormPair( normal_form_src[i], normal_form_src[j] ) ); + conc = NodeManager::currentNM()->mkNode( kind::OR, x_empty, conc ); sendLemma( ant, conc, "Loop" ); return true; - }else{ + } else { Trace("strings-solve-debug") << "No loops detected." << std::endl; if( normal_forms[i][index_i].getKind() == kind::CONST_STRING || normal_forms[j][index_j].getKind() == kind::CONST_STRING) { @@ -1818,8 +1834,8 @@ bool TheoryStrings::unrollStar( Node atom ) { Node x = atom[0]; Node r = atom[1]; int depth = d_reg_exp_unroll_depth.find( atom )==d_reg_exp_unroll_depth.end() ? 0 : d_reg_exp_unroll_depth[atom]; - if( depth <= options::stringRegExpUnrollDepth() ){ - Trace("strings-regex") << "...unroll " << atom << " now." << std::endl; + if( depth <= options::stringRegExpUnrollDepth() ) { + Trace("strings-regex") << "Strings::regex: Unroll " << atom << " for " << depth << " times." << std::endl; d_reg_exp_unroll[atom] = true; //add lemma? Node xeqe = x.eqNode( d_emptyString ); @@ -1853,16 +1869,27 @@ bool TheoryStrings::unrollStar( Node atom ) { Node len_x_gt_len_xp = NodeManager::currentNM()->mkNode( kind::GT, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x ), NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_xp ) ); - - Node unr = NodeManager::currentNM()->mkNode( kind::AND, unr0, urc[0], unr2, unr3, len_x_gt_len_xp ); + + //Node len_x_eq_s_xp = NodeManager::currentNM()->mkNode( kind::EQUAL, + // NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x ), + // NodeManager::currentNM()->mkNode( kind::PLUS, + // NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_s ), + // NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_xp ) )); + + std::vector< Node >cc; + cc.push_back(unr0); cc.push_back(urc[0]); cc.push_back(unr2); cc.push_back(unr3); cc.push_back(len_x_gt_len_xp); + //cc.push_back(len_x_eq_s_xp); + + Node unr = NodeManager::currentNM()->mkNode( kind::AND, cc ); Node lem = NodeManager::currentNM()->mkNode( kind::OR, xeqe, unr ); Node ant = atom; - if( d_reg_exp_ant.find( atom )!=d_reg_exp_ant.end() ){ + if( d_reg_exp_ant.find( atom )!=d_reg_exp_ant.end() ) { ant = d_reg_exp_ant[atom]; } sendLemma( ant, lem, "Unroll" ); return true; }else{ + Trace("strings-regex") << "Strings::regex: Stop unrolling " << atom << " the max (" << depth << ") is reached." << std::endl; return false; } } @@ -1916,6 +1943,7 @@ bool TheoryStrings::checkMemberships() { Node TheoryStrings::getNextDecisionRequest() { if(options::stringFMF() && !d_conflict) { + //Trace("strings-fmf-debug") << "Strings::FMF: Assertion Level = " << d_valuation.getAssertionLevel() << std::endl; //initialize the term we will minimize if( d_in_var_lsum.isNull() && !d_in_vars.empty() ){ Trace("strings-fmf-debug") << "Input variables: "; diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 95e19c5aa..73f17a146 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -145,6 +145,30 @@ Node TheoryStringsRewriter::prerewriteConcatRegExp( TNode node ) { return retNode; } +Node TheoryStringsRewriter::prerewriteOrRegExp(TNode node) { + Assert( node.getKind() == kind::REGEXP_OR ); + Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp start " << node << std::endl; + Node retNode = node; + std::vector node_vec; + bool flag = true; + for(unsigned int i=0; imkNode(kind::REGEXP_OR, node_vec); + } + Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp end " << retNode << std::endl; + return retNode; +} + bool TheoryStringsRewriter::checkConstRegExp( TNode t ) { if( t.getKind() != kind::STRING_TO_REGEXP ) { for( unsigned i = 0; imkNode( kind::REGEXP_CONCAT, node[0], NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, node[0])); diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h index e7d7eccb5..78f0da59e 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -35,6 +35,7 @@ public: static Node rewriteConcatString(TNode node); static Node prerewriteConcatRegExp(TNode node); + static Node prerewriteOrRegExp(TNode node); static Node rewriteMembership(TNode node); static RewriteResponse postRewrite(TNode node); diff --git a/src/util/regexp.h b/src/util/regexp.h index 024bfd32e..fef039371 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -159,6 +159,30 @@ public: return convertUnsignedIntToChar( d_str[0] ); } + bool isRepeated() const { + if(d_str.size() > 1) { + unsigned int f = d_str[0]; + for(unsigned i=1; i=0 && id_y>=0) { + if(d_str[id_x] != y.d_str[id_y]) { + c = id_x; + return false; + } + --id_x; --id_y; + } + c = id_x == -1 ? ( - id_y) : id_x; + return true; + } + String substr(unsigned i) const { std::vector ret_vec; std::vector::const_iterator itr = d_str.begin() + i;