From 1774420cec44f09f81ffa225b05057f3ab7703a9 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Tue, 3 Dec 2013 17:03:34 -0600 Subject: [PATCH] Last version for undelayed LB --- src/theory/strings/theory_strings.cpp | 848 +++++++++++++------------- src/theory/strings/theory_strings.h | 15 +- 2 files changed, 436 insertions(+), 427 deletions(-) diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 226411b8a..916478024 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -732,6 +732,424 @@ bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std } return true; } + +bool TheoryStrings::detectLoop( std::vector< std::vector< Node > > &normal_forms, + int i, int j, int index_i, int index_j, + int &loop_in_i, int &loop_in_j) { + int has_loop[2] = { -1, -1 }; + //if( !options::stringFMF() ) { + for( unsigned r=0; r<2; r++ ) { + int index = (r==0 ? index_i : index_j); + int other_index = (r==0 ? index_j : index_i ); + int n_index = (r==0 ? i : j); + int other_n_index = (r==0 ? j : i); + if( normal_forms[other_n_index][other_index].getKind() != kind::CONST_STRING ) { + for( unsigned lp = index+1; lp &curr_exp, + std::vector< std::vector< Node > > &normal_forms, + std::vector< Node > &normal_form_src, + int i, int j, int loop_n_index, int other_n_index, + int loop_index, int index, int other_index) { + Node conc; + std::vector< Node > antec; + std::vector< Node > antec_new_lits; + 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().tailcmp( r.getConst(), c ) ) { + if(c >= 0) { + s_zy = NodeManager::currentNM()->mkConst( s_zy.getConst().substr(0, c) ); + r = d_emptyString; + vec_r.clear(); + Trace("strings-loop") << "Strings::Loop: Refactor S(Z.Y)= " << s_zy << ", c=" << c << std::endl; + flag = false; + } + } + if(flag) { + Trace("strings-loop") << "Strings::Loop: tails are different." << 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 + if( !areDisequal( normal_forms[loop_n_index][loop_index], d_emptyString ) ){ + //try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop + sendSplit( normal_forms[loop_n_index][loop_index], d_emptyString, "Loop Empty x" ); + } else if( !areDisequal( t_yz, d_emptyString ) && t_yz.getKind()!=kind::CONST_STRING ) { + //try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop + sendSplit( t_yz, d_emptyString, "Loop Empty yz" ); + } else { + //need to break + antec.push_back( normal_forms[loop_n_index][loop_index].eqNode( d_emptyString ).negate() ); + if( t_yz.getKind()!=kind::CONST_STRING ) { + antec.push_back( t_yz.eqNode( d_emptyString ).negate() ); + } + Node ant = mkExplain( antec, antec_new_lits ); + if(d_loop_antec.find(ant) == d_loop_antec.end()) { + d_loop_antec[ant] = true; + + Node str_in_re; + 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)=" << rep_c << " " << std::endl; + //special case + 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, rep_c ) ) ); + conc = str_in_re; + } else { + Trace("strings-loop") << "Strings::Loop: Normal Splitting." << std::endl; + //right + Node sk_w= NodeManager::currentNM()->mkSkolem( "w_loop_$$", normal_forms[other_n_index][other_index].getType(), "created for loop detection split" ); + Node sk_y= NodeManager::currentNM()->mkSkolem( "y_loop_$$", normal_forms[other_n_index][other_index].getType(), "created for loop detection split" ); + Node sk_z= NodeManager::currentNM()->mkSkolem( "z_loop_$$", normal_forms[other_n_index][other_index].getType(), "created for loop detection split" ); + //t1 * ... * tn = y * z + Node conc1 = t_yz.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk_y, sk_z ) ); + // s1 * ... * sk = z * y * r + vec_r.insert(vec_r.begin(), sk_y); + vec_r.insert(vec_r.begin(), sk_z); + Node conc2 = s_zy.eqNode( mkConcat( vec_r ) ); + Node conc3 = normal_forms[other_n_index][other_index].eqNode( mkConcat( sk_y, sk_w ) ); + str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_w, + NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, + NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, mkConcat( sk_z, sk_y ) ) ) ); + + //Node sk_y_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_y ); + //Node zz_imp_yz = NodeManager::currentNM()->mkNode( kind::IMPLIES, sk_z.eqNode(d_emptyString), sk_y.eqNode(d_emptyString)); + + std::vector< Node > vec_conc; + vec_conc.push_back(conc1); vec_conc.push_back(conc2); vec_conc.push_back(conc3); + vec_conc.push_back(str_in_re); + vec_conc.push_back(sk_y.eqNode(d_emptyString).negate()); + conc = NodeManager::currentNM()->mkNode( kind::AND, vec_conc );//, len_x_gt_len_y + } // normal case + + //set its antecedant to ant, to say when it is relevant + d_reg_exp_ant[str_in_re] = ant; + //unroll the str in re constraint once + unrollStar( str_in_re ); + sendLemma( ant, conc, "LOOP-BREAK" ); + + //we will be done + addNormalFormPair( normal_form_src[i], normal_form_src[j] ); + } else { + Trace("strings-loop") << "Strings::Loop: loop lemma for " << ant << " has already added." << std::endl; + addNormalFormPair( normal_form_src[i], normal_form_src[j] ); + return false; + } + } + return true; +} +bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms, + std::vector< std::vector< Node > > &normal_forms_exp, + std::vector< Node > &normal_form_src) { + bool flag_lb = false; + for(unsigned i=0; i curr_exp; + curr_exp.insert(curr_exp.end(), normal_forms_exp[i].begin(), normal_forms_exp[i].end() ); + curr_exp.insert(curr_exp.end(), normal_forms_exp[j].begin(), normal_forms_exp[j].end() ); + curr_exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, normal_form_src[i], normal_form_src[j] ) ); + //ensure that normal_forms[i] and normal_forms[j] are the same modulo equality + unsigned index_i = 0; + unsigned index_j = 0; + bool success; + do + { + success = false; + //if we are at the end + 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] ); + } else { + //the remainder must be empty + unsigned k = index_i==normal_forms[i].size() ? j : i; + unsigned index_k = index_i==normal_forms[i].size() ? index_j : index_i; + Node eq_exp; + if( curr_exp.empty() ) { + eq_exp = d_true; + } else if( curr_exp.size() == 1 ) { + eq_exp = curr_exp[0]; + } else { + eq_exp = NodeManager::currentNM()->mkNode( kind::AND, curr_exp ); + } + while(!d_conflict && index_kmkNode( kind::EQUAL, length_term_i, length_term_j ); + Trace("strings-solve-debug") << "Case 2.1 : string lengths neither equal nor disequal" << std::endl; + //try to make the lengths equal via splitting on demand + sendSplit( length_term_i, length_term_j, "Length" ); + length_eq = Rewriter::rewrite( length_eq ); + d_pending_req_phase[ length_eq ] = true; + return true; + } else if( areEqual(length_term_i, length_term_j) ) { + Trace("strings-solve-debug") << "Case 2.2 : string lengths are equal" << std::endl; + Node eq = normal_forms[i][index_i].eqNode( normal_forms[j][index_j] ); + Node length_eq = length_term_i.eqNode( length_term_j ); + std::vector< Node > temp_exp; + temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() ); + temp_exp.push_back(length_eq); + Node eq_exp = temp_exp.empty() ? d_true : + temp_exp.size() == 1 ? temp_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, temp_exp ); + Trace("strings-lemma") << "Strings: Infer " << eq << " from " << eq_exp << std::endl; + d_pending.push_back( eq ); + d_pending_exp[eq] = eq_exp; + d_infer.push_back(eq); + d_infer_exp.push_back(eq_exp); + return true; + } else if(( normal_forms[i][index_i].getKind()!=kind::CONST_STRING && index_i==normal_forms[i].size()-1 ) || + ( normal_forms[j][index_j].getKind()!=kind::CONST_STRING && index_j==normal_forms[j].size()-1 ) ) { + Trace("strings-solve-debug") << "Case 3 : at endpoint" << std::endl; + Node conc; + std::vector< Node > antec; + antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); + std::vector< Node > antec_new_lits; + std::vector< Node > eqn; + for( unsigned r=0; r<2; r++ ) { + int index_k = r==0 ? index_i : index_j; + int k = r==0 ? i : j; + std::vector< Node > eqnc; + for( unsigned index_l=index_k; index_l antec; + std::vector< Node > antec_new_lits; + 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) { + unsigned const_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? i : j; + unsigned const_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_i : index_j; + unsigned nconst_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? j : i; + unsigned nconst_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_j : index_i; + Node const_str = normal_forms[const_k][const_index_k]; + Node other_str = normal_forms[nconst_k][nconst_index_k]; + if( other_str.getKind() == kind::CONST_STRING ) { + unsigned len_short = const_str.getConst().size() <= other_str.getConst().size() ? const_str.getConst().size() : other_str.getConst().size(); + if( const_str.getConst().strncmp(other_str.getConst(), len_short) ) { + //same prefix + //k is the index of the string that is shorter + int k = const_str.getConst().size()().size() ? i : j; + int index_k = const_str.getConst().size()().size() ? index_i : index_j; + int l = const_str.getConst().size()().size() ? j : i; + int index_l = const_str.getConst().size()().size() ? index_j : index_i; + Node remainderStr = NodeManager::currentNM()->mkConst( normal_forms[l][index_l].getConst().substr(len_short) ); + Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms[l][index_l] << " into " << normal_forms[k][index_k] << ", " << remainderStr << std::endl; + normal_forms[l].insert( normal_forms[l].begin()+index_l + 1, remainderStr ); + normal_forms[l][index_l] = normal_forms[k][index_k]; + success = true; + } else { + //curr_exp is conflict + antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); + Node ant = mkExplain( antec, antec_new_lits ); + sendLemma( ant, conc, "Conflict" ); + return true; + } + } else { + Assert( other_str.getKind()!=kind::STRING_CONCAT ); + antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); + Node firstChar = const_str.getConst().size() == 1 ? const_str : + NodeManager::currentNM()->mkConst( const_str.getConst().substr(0, 1) ); + //split the string + //Node sk = NodeManager::currentNM()->mkSkolem( "c_spt_$$", normal_forms[i][index_i].getType(), "created for v/c split" ); + + Node eq1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, d_emptyString ) ); + Node eq2 = mkSplitEq( "c_spt_$$", "created for v/c split", other_str, firstChar, false ); + //Node eq2 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, + // NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, sk ) ) ); + d_pending_req_phase[ eq1 ] = true; + conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); + Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl; + + Node ant = mkExplain( antec, antec_new_lits ); + sendLemma( ant, conc, "CST-SPLIT" ); + return true; + } + } else { + antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); + + Node ldeq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ).negate(); + if( d_equalityEngine.areDisequal( length_term_i, length_term_j, true ) ){ + antec.push_back( ldeq ); + }else{ + antec_new_lits.push_back(ldeq); + } + + //x!=e /\ y!=e + for(unsigned xory=0; xory<2; xory++) { + Node x = xory==0 ? normal_forms[i][index_i] : normal_forms[j][index_j]; + Node xgtz = x.eqNode( d_emptyString ).negate(); + if( areDisequal( x, d_emptyString ) ) { + antec.push_back( xgtz ); + } else { + antec_new_lits.push_back( xgtz ); + } + } + + //Node sk = NodeManager::currentNM()->mkSkolem( "v_spt_$$", normal_forms[i][index_i].getType(), "created for v/v split" ); + //Node eq1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i], + // NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[j][index_j], sk ) ) ); + //Node eq2 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[j][index_j], + // NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[i][index_i], sk ) ) ); + Node eq1 = mkSplitEq( "v_spt_l_$$", "created for v/v split", normal_forms[i][index_i], normal_forms[j][index_j], true ); + Node eq2 = mkSplitEq( "v_spt_r_$$", "created for v/v split", normal_forms[j][index_j], normal_forms[i][index_i], true ); + conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); + // |sk| > 0 + ////Node sk_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ); + ////Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::GT, sk_len, d_zero); + //Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, d_emptyString).negate(); + //Trace("strings-lemma") << "Strings lemma : " << sk_gt_zero << std::endl; + ////d_out->lemma(sk_gt_zero); + //d_lemma_cache.push_back( sk_gt_zero ); + + Node ant = mkExplain( antec, antec_new_lits ); + sendLemma( ant, conc, "VAR-SPLIT" ); + return true; + } + } + } + } + } + } while(success); + } + } + if(!flag_lb) { + return false; + } + } + if(flag_lb) { + //TODO + return true; + } else { + return false; + } +} + //nf_exp is conjunction bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ) { Trace("strings-process") << "Process equivalence class " << eqc << std::endl; @@ -761,7 +1179,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v } else { visited.push_back( eqc ); bool result; - if(d_normal_forms.find(eqc)==d_normal_forms.end() ){ + if(d_normal_forms.find(eqc)==d_normal_forms.end() ) { //phi => t = s1 * ... * sn // normal form for each non-variable term in this eqc (s1...sn) std::vector< std::vector< Node > > normal_forms; @@ -773,431 +1191,9 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v result = getNormalForms(eqc, visited, nf, normal_forms, normal_forms_exp, normal_form_src); if( d_conflict || !d_pending.empty() || !d_lemma_cache.empty() ) { return true; - }else if( result ){ - unsigned i = 0; - //unify each normal form > 0 with normal_forms[0] - for( unsigned j=1; j curr_exp; - curr_exp.insert(curr_exp.end(), normal_forms_exp[i].begin(), normal_forms_exp[i].end() ); - curr_exp.insert(curr_exp.end(), normal_forms_exp[j].begin(), normal_forms_exp[j].end() ); - curr_exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, normal_form_src[i], normal_form_src[j] ) ); - //ensure that normal_forms[i] and normal_forms[j] are the same modulo equality - unsigned index_i = 0; - unsigned index_j = 0; - bool success; - do - { - success = false; - //if we are at the end - 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] ); - }else{ - //the remainder must be empty - unsigned k = index_i==normal_forms[i].size() ? j : i; - unsigned index_k = index_i==normal_forms[i].size() ? index_j : index_i; - while(!d_conflict && index_kmkNode( kind::AND, curr_exp ); - } - Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, d_emptyString, normal_forms[k][index_k] ); - Trace("strings-lemma") << "Strings : Infer " << eq << " from " << eq_exp << std::endl; - Assert( !areEqual( d_emptyString, normal_forms[k][index_k] ) ); - d_pending.push_back( eq ); - d_pending_exp[eq] = eq_exp; - d_infer.push_back(eq); - d_infer_exp.push_back(eq_exp); - index_k++; - } - } - }else { - Trace("strings-solve-debug") << "Process " << normal_forms[i][index_i] << " ... " << normal_forms[j][index_j] << std::endl; - if(areEqual(normal_forms[i][index_i],normal_forms[j][index_j])){ - Trace("strings-solve-debug") << "Case 1 : strings are equal" << std::endl; - //terms are equal, continue - if( normal_forms[i][index_i]!=normal_forms[j][index_j] ){ - Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL,normal_forms[i][index_i], - normal_forms[j][index_j]); - Trace("strings-solve-debug") << "Add to explanation : " << eq << std::endl; - curr_exp.push_back(eq); - } - index_j++; - index_i++; - success = true; - }else{ - Node length_term_i = getLength( normal_forms[i][index_i] ); - Node length_term_j = getLength( normal_forms[j][index_j] ); - //check length(normal_forms[i][index]) == length(normal_forms[j][index]) - if( !areDisequal(length_term_i, length_term_j) && - !areEqual(length_term_i, length_term_j) && - normal_forms[i][index_i].getKind()!=kind::CONST_STRING && - normal_forms[j][index_j].getKind()!=kind::CONST_STRING ) { - //length terms are equal, merge equivalence classes if not already done so - Node length_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ); - Trace("strings-solve-debug") << "Case 2.1 : string lengths neither equal nor disequal" << std::endl; - //try to make the lengths equal via splitting on demand - sendSplit( length_term_i, length_term_j, "Length" ); - length_eq = Rewriter::rewrite( length_eq ); - d_pending_req_phase[ length_eq ] = true; - return true; - } else if( areEqual(length_term_i, length_term_j) ) { - Trace("strings-solve-debug") << "Case 2.2 : string lengths are equal" << std::endl; - Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i], normal_forms[j][index_j] ); - Node length_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ); - std::vector< Node > temp_exp; - temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() ); - temp_exp.push_back(length_eq); - Node eq_exp = temp_exp.empty() ? d_true : - temp_exp.size() == 1 ? temp_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, temp_exp ); - Trace("strings-lemma") << "Strings : Infer " << eq << " from " << eq_exp << std::endl; - d_pending.push_back( eq ); - d_pending_exp[eq] = eq_exp; - d_infer.push_back(eq); - d_infer_exp.push_back(eq_exp); - return true; - } else if( ( normal_forms[i][index_i].getKind()!=kind::CONST_STRING && index_i==normal_forms[i].size()-1 ) || - ( normal_forms[j][index_j].getKind()!=kind::CONST_STRING && index_j==normal_forms[j].size()-1 ) ){ - Trace("strings-solve-debug") << "Case 3 : at endpoint" << std::endl; - Node conc; - std::vector< Node > antec; - antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); - std::vector< Node > antec_new_lits; - std::vector< Node > eqn; - for( unsigned r=0; r<2; r++ ){ - int index_k = r==0 ? index_i : index_j; - int k = r==0 ? i : j; - std::vector< Node > eqnc; - for( unsigned index_l=index_k; index_l antec; - std::vector< Node > antec_new_lits; - //check for loops - //Trace("strings-loop") << "Check for loops i,j = " << (index_i+1) << "/" << normal_forms[i].size() << " " << (index_j+1) << "/" << normal_forms[j].size() << std::endl; - int has_loop[2] = { -1, -1 }; - //if( !options::stringFMF() ) { - for( unsigned r=0; r<2; r++ ) { - int index = (r==0 ? index_i : index_j); - int other_index = (r==0 ? index_j : index_i ); - int n_index = (r==0 ? i : j); - int other_n_index = (r==0 ? j : i); - if( normal_forms[other_n_index][other_index].getKind() != kind::CONST_STRING ) { - for( unsigned lp = index+1; lp().tailcmp( r.getConst(), c ) ) { - if(c >= 0) { - s_zy = NodeManager::currentNM()->mkConst( s_zy.getConst().substr(0, c) ); - 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; - } - } - - //Node loop_eq = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::EQUAL, - // NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[other_n_index][other_index], s_zy ), - // NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, t_yz, normal_forms[other_n_index][other_index], r ) ) ); - - antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); - //require that x is non-empty - //Node x_empty = normal_forms[loop_n_index][loop_index].eqNode( d_emptyString ); - //x_empty = Rewriter::rewrite( x_empty ); - //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() ); - //} - //d_pending_req_phase[ x_empty ] = true; - if( !areDisequal( normal_forms[loop_n_index][loop_index], d_emptyString ) ){ - //try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop - sendSplit( normal_forms[loop_n_index][loop_index], d_emptyString, "Loop Empty x" ); - return true; - } else if( !areDisequal( t_yz, d_emptyString ) && t_yz.getKind()!=kind::CONST_STRING ) { - //TODO........... - //try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop - sendSplit( t_yz, d_emptyString, "Loop Empty yz" ); - return true; - } else { - //need to break - antec.push_back( normal_forms[loop_n_index][loop_index].eqNode( d_emptyString ).negate() ); - if( t_yz.getKind()!=kind::CONST_STRING ){ - antec.push_back( t_yz.eqNode( d_emptyString ).negate() ); - } - Node ant = mkExplain( antec, antec_new_lits ); - if(d_loop_antec.find(ant) == d_loop_antec.end()) { - d_loop_antec[ant] = true; - - Node str_in_re; - 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)=" << rep_c << " " << std::endl; - //special case - //conc = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], mkConcat( rep_c, 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, rep_c ) ) ); - //conc = NodeManager::currentNM()->mkNode( kind::AND, conc, str_in_re ); - conc = str_in_re; - } else { - Trace("strings-loop") << "Strings::Loop: ...Normal Splitting." << std::endl; - //left - /* - Node t_eq_sr = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::EQUAL, t_yz, - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, s_zy, r ) ) ); - Node x_in_s = 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, s_zy ) ) ); - Node cleft = NodeManager::currentNM()->mkNode( kind::AND, t_eq_sr, x_in_s ); - - //unroll for once - unrollStar(x_in_s); - */ - - //right - 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 - Node conc1 = NodeManager::currentNM()->mkNode( kind::EQUAL, t_yz, - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk_y, sk_z ) ); - // 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, - NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, mkConcat( sk_z, sk_y ) ) ) ); - - //Node sk_y_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_y ); - //Node zz_imp_yz = NodeManager::currentNM()->mkNode( kind::IMPLIES, sk_z.eqNode(d_emptyString), sk_y.eqNode(d_emptyString)); - - //Node len_x_gt_len_y = NodeManager::currentNM()->mkNode( kind::GT, - // NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, normal_forms[other_n_index][other_index]), - // sk_y_len ); - std::vector< Node > vec_conc; - vec_conc.push_back(conc1); vec_conc.push_back(conc2); vec_conc.push_back(conc3); - vec_conc.push_back(str_in_re); - vec_conc.push_back(sk_y.eqNode(d_emptyString).negate()); - conc = NodeManager::currentNM()->mkNode( kind::AND, vec_conc );//, len_x_gt_len_y - - //conc = NodeManager::currentNM()->mkNode( kind::OR, cleft, conc ); - - //Node x_eq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], d_emptyString); - //conc = NodeManager::currentNM()->mkNode( kind::OR, x_eq_empty, conc ); - } // normal case - - //set its antecedant to ant, to say when it is relevant - d_reg_exp_ant[str_in_re] = ant; - //unroll the str in re constraint once - unrollStar( str_in_re ); - //conc = NodeManager::currentNM()->mkNode( kind::OR, x_empty, conc ); - sendLemma( ant, conc, "LOOP-BREAK" ); - - //we will be done - addNormalFormPair( normal_form_src[i], normal_form_src[j] ); - //Assert( isNormalFormPair( normal_form_src[i], normal_form_src[j] ) ); - return true; - } else { - Trace("strings-loop") << "Strings::Loop: loop lemma for " << ant << " has already added." << std::endl; - addNormalFormPair( normal_form_src[i], normal_form_src[j] ); - } - } - } 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) { - unsigned const_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? i : j; - unsigned const_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_i : index_j; - unsigned nconst_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? j : i; - unsigned nconst_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_j : index_i; - Node const_str = normal_forms[const_k][const_index_k]; - Node other_str = normal_forms[nconst_k][nconst_index_k]; - if( other_str.getKind() == kind::CONST_STRING ) { - unsigned len_short = const_str.getConst().size() <= other_str.getConst().size() ? const_str.getConst().size() : other_str.getConst().size(); - if( const_str.getConst().strncmp(other_str.getConst(), len_short) ) { - //same prefix - //k is the index of the string that is shorter - int k = const_str.getConst().size()().size() ? i : j; - int index_k = const_str.getConst().size()().size() ? index_i : index_j; - int l = const_str.getConst().size()().size() ? j : i; - int index_l = const_str.getConst().size()().size() ? index_j : index_i; - Node remainderStr = NodeManager::currentNM()->mkConst( normal_forms[l][index_l].getConst().substr(len_short) ); - Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms[l][index_l] << " into " << normal_forms[k][index_k] << ", " << remainderStr << std::endl; - normal_forms[l].insert( normal_forms[l].begin()+index_l + 1, remainderStr ); - normal_forms[l][index_l] = normal_forms[k][index_k]; - success = true; - } else { - //curr_exp is conflict - antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); - Node ant = mkExplain( antec, antec_new_lits ); - sendLemma( ant, conc, "Conflict" ); - return true; - } - } else { - Assert( other_str.getKind()!=kind::STRING_CONCAT ); - antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); - Node firstChar = const_str.getConst().size() == 1 ? const_str : - NodeManager::currentNM()->mkConst( const_str.getConst().substr(0, 1) ); - //split the string - //Node sk = NodeManager::currentNM()->mkSkolem( "c_spt_$$", normal_forms[i][index_i].getType(), "created for v/c split" ); - - Node eq1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, d_emptyString ) ); - Node eq2 = mkSplitEq( "c_spt_$$", "created for v/c split", other_str, firstChar, false ); - //Node eq2 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, - // NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, sk ) ) ); - d_pending_req_phase[ eq1 ] = true; - conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); - Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl; - - Node ant = mkExplain( antec, antec_new_lits ); - sendLemma( ant, conc, "CST-SPLIT" ); - return true; - } - }else{ - antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); - - Node ldeq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ).negate(); - if( d_equalityEngine.areDisequal( length_term_i, length_term_j, true ) ){ - antec.push_back( ldeq ); - }else{ - antec_new_lits.push_back(ldeq); - } - - //x!=e /\ y!=e - for(unsigned xory=0; xory<2; xory++) { - Node x = xory==0 ? normal_forms[i][index_i] : normal_forms[j][index_j]; - Node xgtz = x.eqNode( d_emptyString ).negate(); - if( areDisequal( x, d_emptyString ) ) { - antec.push_back( xgtz ); - } else { - antec_new_lits.push_back( xgtz ); - } - } - - //Node sk = NodeManager::currentNM()->mkSkolem( "v_spt_$$", normal_forms[i][index_i].getType(), "created for v/v split" ); - //Node eq1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i], - // NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[j][index_j], sk ) ) ); - //Node eq2 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[j][index_j], - // NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[i][index_i], sk ) ) ); - Node eq1 = mkSplitEq( "v_spt_l_$$", "created for v/v split", normal_forms[i][index_i], normal_forms[j][index_j], true ); - Node eq2 = mkSplitEq( "v_spt_r_$$", "created for v/v split", normal_forms[j][index_j], normal_forms[i][index_i], true ); - conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); - // |sk| > 0 - ////Node sk_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ); - ////Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::GT, sk_len, d_zero); - //Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, d_emptyString).negate(); - //Trace("strings-lemma") << "Strings lemma : " << sk_gt_zero << std::endl; - ////d_out->lemma(sk_gt_zero); - //d_lemma_cache.push_back( sk_gt_zero ); - - Node ant = mkExplain( antec, antec_new_lits ); - sendLemma( ant, conc, "VAR-SPLIT" ); - return true; - } - } - } - } - } - }while(success); - } + } else if( result ) { + if(processNEqc(normal_forms, normal_forms_exp, normal_form_src)) { + return true; } } diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index fb6599919..c7ea830b6 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -192,7 +192,20 @@ private: std::map< Node, bool > d_length_inst; private: bool getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf, - std::vector< std::vector< Node > > &normal_forms, std::vector< std::vector< Node > > &normal_forms_exp, std::vector< Node > &normal_form_src); + std::vector< std::vector< Node > > &normal_forms, + std::vector< std::vector< Node > > &normal_forms_exp, + std::vector< Node > &normal_form_src); + bool detectLoop(std::vector< std::vector< Node > > &normal_forms, + int i, int j, int index_i, int index_j, + int &loop_in_i, int &loop_in_j); + bool processLoop(std::vector< Node > &curr_exp, + std::vector< std::vector< Node > > &normal_forms, + std::vector< Node > &normal_form_src, + int i, int j, int loop_n_index, int other_n_index, + int loop_index, int index, int other_index); + bool processNEqc(std::vector< std::vector< Node > > &normal_forms, + std::vector< std::vector< Node > > &normal_forms_exp, + std::vector< Node > &normal_form_src); bool normalizeEquivalenceClass( Node n, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ); bool normalizeDisequality( Node n1, Node n2 ); bool unrollStar( Node atom ); -- 2.30.2