From 135f99f365920097ce48be87cb77fb1144d446a3 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 26 Feb 2016 13:39:06 -0600 Subject: [PATCH] Refactoring of inferences in strings. Add several options. --- src/options/strings_options | 8 + src/theory/strings/theory_strings.cpp | 503 +++++++++++---------- src/theory/strings/theory_strings.h | 4 +- src/theory/uf/theory_uf_strong_solver.cpp | 3 +- test/regress/regress0/strings/Makefile.am | 3 +- test/regress/regress0/strings/norn-31.smt2 | 23 + 6 files changed, 303 insertions(+), 241 deletions(-) create mode 100644 test/regress/regress0/strings/norn-31.smt2 diff --git a/src/options/strings_options b/src/options/strings_options index 1b64af83f..dee379878 100644 --- a/src/options/strings_options +++ b/src/options/strings_options @@ -55,6 +55,14 @@ option stringEagerLen strings-eager-len --strings-eager-len bool :default true strings eager length lemmas option stringCheckEntailLen strings-check-entail-len --strings-check-entail-len bool :default true check entailment between length terms to reduce splitting +option stringProcessLoop strings-process-loop --strings-process-loop bool :default true + reduce looping word equations to regular expressions +option stringAbortLoop strings-abort-loop --strings-abort-loop bool :default false + abort when a looping word equation is encountered +option stringInferAsLemmas strings-infer-as-lemmas --strings-infer-as-lemmas bool :default false + always send lemmas out instead of making internal inferences +option stringRExplainLemmas strings-rexplain-lemmas --strings-rexplain-lemmas bool :default true + regression explanations for string lemmas endmodule diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 175bd2c2a..dd498a2d2 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -653,7 +653,9 @@ void TheoryStrings::checkReduction( Node atom, int pol, int effort ) { if( atom.getKind()==kind::STRING_IN_REGEXP ){ if( atom[1].getKind()==kind::REGEXP_RANGE ){ Node eq = d_one.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, atom[0])); - sendLemma( atom, eq, "RE-Range-Len" ); + std::vector< Node > exp_vec; + exp_vec.push_back( atom ); + sendInference( d_empty_vec, exp_vec, eq, "RE-Range-Len", true ); } }else if( atom.getKind()==kind::STRING_STRCTN ){ Node x = atom[0]; @@ -663,7 +665,9 @@ void TheoryStrings::checkReduction( Node atom, int pol, int effort ) { Node sk1 = mkSkolemCached( x, s, sk_id_ctn_pre, "sc1" ); Node sk2 = mkSkolemCached( x, s, sk_id_ctn_post, "sc2" ); Node eq = Rewriter::rewrite( x.eqNode( mkConcat( sk1, s, sk2 ) ) ); - sendLemma( atom, eq, "POS-CTN" ); + std::vector< Node > exp_vec; + exp_vec.push_back( atom ); + sendInference( d_empty_vec, exp_vec, eq, "POS-CTN", true ); }else{ // for STRING_SUBSTR, // STRING_STRIDOF, STRING_ITOS, STRING_U16TOS, STRING_U32TOS, STRING_STOI, STRING_STOU16, STRING_STOU32, STRING_STRREPL @@ -675,7 +679,7 @@ void TheoryStrings::checkReduction( Node atom, int pol, int effort ) { nnlem = Rewriter::rewrite( nnlem ); Trace("strings-red-lemma") << "Reduction_" << effort << " lemma : " << nnlem << std::endl; Trace("strings-red-lemma") << "...from " << atom << std::endl; - sendLemma( d_true, nnlem, "Reduction" ); + sendInference( d_empty_vec, nnlem, "Reduction", true ); } } } @@ -950,7 +954,7 @@ void TheoryStrings::checkInit() { } } //infer the equality - sendInfer( mkAnd( exp ), n.eqNode( nc ), "I_Norm" ); + sendInference( exp, n.eqNode( nc ), "I_Norm" ); }else{ //update the extf map : only process if neither has been reduced NodeBoolMap::const_iterator it = d_ext_func_terms.find( n ); @@ -989,7 +993,7 @@ void TheoryStrings::checkInit() { } AlwaysAssert( foundNEmpty ); //infer the equality - sendInfer( mkAnd( exp ), n.eqNode( c[0] ), "I_Norm_S" ); + sendInference( exp, n.eqNode( c[0] ), "I_Norm_S" ); } d_congruent.insert( n ); congruent[k]++; @@ -1141,11 +1145,7 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) { } if( !conc.isNull() ){ Trace("strings-extf") << " resolve extf : " << nr << " -> " << nrc << std::endl; - if( n.getType().isInteger() || d_extf_exp[n].empty() ){ - sendLemma( mkExplain( d_extf_exp[n] ), conc, effort==0 ? "EXTF" : "EXTF-N" ); - }else{ - sendInfer( mkAnd( d_extf_exp[n] ), conc, effort==0 ? "EXTF" : "EXTF-N" ); - } + sendInference( d_extf_exp[n], conc, effort==0 ? "EXTF" : "EXTF-N", n.getType().isInteger() || d_extf_exp[n].empty() ); if( d_conflict ){ Trace("strings-extf-debug") << " conflict, return." << std::endl; return; @@ -1158,7 +1158,7 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) { Trace("strings-extf-debug") << " decomposable..." << std::endl; Trace("strings-extf") << " resolve extf : " << nr << " -> " << nrc << ", pol = " << d_extf_pol[n] << std::endl; for( unsigned i=0; i children; children.push_back( nr[0] ); children.push_back( nr[1] ); - Node exp_n = mkAnd( d_extf_exp[n] ); + //Node exp_n = mkAnd( d_extf_exp[n] ); for( unsigned i=0; imkNode( kind::STRING_STRCTN, children ); //can mark as reduced, since model for n => model for conc d_ext_func_terms[conc] = false; - sendInfer( exp_n, n_pol==1 ? conc : conc.negate(), "CTN_Decompose" ); + sendInference( d_extf_exp[n], n_pol==1 ? conc : conc.negate(), "CTN_Decompose" ); } } }else{ @@ -1238,7 +1238,7 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, int effort ){ Node ofrom = d_extf_info[nr[0]].d_ctn_from[opol][i]; Assert( d_extf_exp.find( ofrom )!=d_extf_exp.end() ); exp.insert( exp.end(), d_extf_exp[ofrom].begin(), d_extf_exp[ofrom].end() ); - sendInfer( mkAnd( exp ), conc, "CTN_Trans" ); + sendInference( exp, conc, "CTN_Trans" ); } } }else{ @@ -1462,11 +1462,13 @@ void TheoryStrings::checkFlatForms() { break; }else{ //if lengths are the same, apply LengthEq - Node lcc = getLength( cc, lexp ); + std::vector< Node > lexp2; + Node lcc = getLength( cc, lexp2 ); if( areEqual( lcurr, lcc ) ){ Trace("strings-ff-debug") << "Infer " << ac << " == " << bc << " since " << lcurr << " == " << lcc << std::endl; //exp_n.push_back( getLength( curr, true ).eqNode( getLength( cc, true ) ) ); exp.insert( exp.end(), lexp.begin(), lexp.end() ); + exp.insert( exp.end(), lexp2.begin(), lexp2.end() ); addToExplanation( lcurr, lcc, exp ); conc = ac.eqNode( bc ); inf_type = 1; @@ -1505,7 +1507,7 @@ void TheoryStrings::checkFlatForms() { } } //if( exp_n.empty() ){ - sendInfer( mkAnd( exp ), conc, inf_type==0? "F_Const" : ( inf_type==1 ? "F_LengthEq" : ( inf_type==2 ? "F_Endpoint" : "F_EndpointEq" ) ) ); + sendInference( exp, conc, inf_type==0? "F_Const" : ( inf_type==1 ? "F_LengthEq" : ( inf_type==2 ? "F_Endpoint" : "F_EndpointEq" ) ) ); //}else{ //} if( d_conflict ){ @@ -1555,7 +1557,9 @@ Node TheoryStrings::checkCycles( Node eqc, std::vector< Node >& curr, std::vecto if( eqc==d_emptyString_r ){ //for empty eqc, ensure all components are empty if( nr!=d_emptyString_r ){ - sendInfer( n.eqNode( d_emptyString ), n[i].eqNode( d_emptyString ), "I_CYCLE_E" ); + std::vector< Node > exp; + exp.push_back( n.eqNode( d_emptyString ) ); + sendInference( exp, n[i].eqNode( d_emptyString ), "I_CYCLE_E" ); return Node::null(); } }else{ @@ -1574,7 +1578,7 @@ Node TheoryStrings::checkCycles( Node eqc, std::vector< Node >& curr, std::vecto for( unsigned j=0; j & nf, ant.insert( ant.end(), nf_exp_n.begin(), nf_exp_n.end() ); ant.push_back( n.eqNode( eqc ) ); Node conc = Rewriter::rewrite( nn.eqNode( eqc ) ); - sendInfer( mkAnd( ant ), conc, "CYCLE-T" ); + sendInference( ant, conc, "CYCLE-T" ); return true; } */ @@ -1958,7 +1962,7 @@ bool TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_form Node other_str = normal_forms[nconst_k][nconst_index_k]; Assert( other_str.getKind()!=kind::CONST_STRING, "Other string is not constant." ); Assert( other_str.getKind()!=kind::STRING_CONCAT, "Other string is not CONCAT." ); - if( !areDisequal(other_str, d_emptyString) ) { + if( !d_equalityEngine.areDisequal(other_str, d_emptyString, true) ) { sendSplit( other_str, d_emptyString, "Len-Split(CST)" ); } else { Assert(areDisequal(other_str, d_emptyString), "CST Split on empty Var"); @@ -1987,8 +1991,7 @@ bool TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_form } conc = Rewriter::rewrite( conc ); - sendLemma( mkExplain( antec ), conc, "S-Split(CST-P)" ); - //sendInfer(mkAnd( antec ), conc, "S-Split(CST-P)"); + sendInference( antec, conc, "S-Split(CST-P)", true ); } return true; } else { @@ -2036,9 +2039,7 @@ bool TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_form } - Node ant = mkExplain( antec, antec_new_lits ); - sendLemma( ant, conc, "S-Split(VAR)" ); - //sendInfer( ant, conc, "S-Split(VAR)" ); + sendInference( antec, antec_new_lits, conc, "S-Split(VAR)", true ); //++(d_statistics.d_eq_splits); return true; } @@ -2094,13 +2095,13 @@ bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal //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 = mkAnd( curr_exp ); + //Node eq_exp = mkAnd( curr_exp ); while(!d_conflict && index_k > &normal Node length_eq = length_term_i.eqNode( length_term_j ); temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() ); temp_exp.push_back(length_eq); - sendInfer( mkAnd( temp_exp ), eq, "LengthEq" ); + sendInference( temp_exp, eq, "LengthEq" ); 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 ) ){ @@ -2154,8 +2155,7 @@ bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal } if( !areEqual( eqn[0], eqn[1] ) ) { conc = eqn[0].eqNode( eqn[1] ); - sendLemma( mkExplain( antec ), conc, "ENDPOINT" ); - //sendInfer( mkAnd( antec ), conc, "ENDPOINT" ); + sendInference( antec, conc, "ENDPOINT", true ); return true; }else{ index_i = normal_forms[i].size(); @@ -2192,8 +2192,7 @@ bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal std::vector< Node > antec; //curr_exp is conflict antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); - Node ant = mkExplain( antec ); - sendLemma( ant, d_false, "Const Conflict" ); + sendInference( antec, d_false, "Const Conflict", true ); return true; } } @@ -2234,162 +2233,172 @@ bool TheoryStrings::detectLoop( std::vector< std::vector< Node > > &normal_forms //xs(zy)=t(yz)xr bool TheoryStrings::processLoop( std::vector< Node > &antec, 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; - 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( options::stringAbortLoop() ){ + Message() << "Looping word equation encountered." << std::endl; + exit( 1 ); + }else{ + Node conc; + 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().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 if(t_yz.isConst()) { - Trace("strings-loop") << "Strings::Loop: Const Normal Breaking." << std::endl; - CVC4::String s = t_yz.getConst< CVC4::String >(); - unsigned size = s.size(); - std::vector< Node > vconc; - for(unsigned len=1; len<=size; len++) { - Node y = NodeManager::currentNM()->mkConst(s.substr(0, len)); - Node z = NodeManager::currentNM()->mkConst(s.substr(len, size - len)); - Node restr = s_zy; - Node cc; - if(r != d_emptyString) { - std::vector< Node > v2(vec_r); - v2.insert(v2.begin(), y); - v2.insert(v2.begin(), z); - restr = mkConcat( z, y ); - cc = Rewriter::rewrite(s_zy.eqNode( mkConcat( v2 ) )); - } else { - cc = Rewriter::rewrite(s_zy.eqNode( mkConcat( z, y) )); - } - if(cc == d_false) { - continue; - } - Node conc2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, normal_forms[other_n_index][other_index], - NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, - NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, y), - NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, - NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, restr)))); - cc = cc==d_true ? conc2 : NodeManager::currentNM()->mkNode( kind::AND, cc, conc2 ); - d_regexp_ant[conc2] = ant; - vconc.push_back(cc); + Node r = mkConcat( vec_r ); + Trace("strings-loop") << " (" << r << ")" << std::endl; + + //Trace("strings-loop") << "Lemma Cache: " << normal_form_src[i] << " vs " << normal_form_src[j] << std::endl; + //TODO: can be more general + 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) ); + r = d_emptyString; + vec_r.clear(); + Trace("strings-loop") << "Strings::Loop: Refactor S(Z.Y)= " << s_zy << ", c=" << c << std::endl; + flag = false; } - conc = vconc.size()==0 ? Node::null() : vconc.size()==1 ? vconc[0] : NodeManager::currentNM()->mkNode(kind::OR, vconc); - } else { - Trace("strings-loop") << "Strings::Loop: Normal Loop Breaking." << std::endl; - //right - Node sk_w= mkSkolemS( "w_loop" ); - Node sk_y= mkSkolemS( "y_loop", 1 ); - Node sk_z= mkSkolemS( "z_loop" ); - //t1 * ... * tn = y * z - Node conc1 = t_yz.eqNode( mkConcat( 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 ) ); - Node restr = r == d_emptyString ? s_zy : mkConcat( sk_z, sk_y ); - 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, restr ) ) ); - - 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());//by mkskolems - conc = NodeManager::currentNM()->mkNode( kind::AND, vec_conc ); - } // normal case - - //set its antecedant to ant, to say when it is relevant - if(!str_in_re.isNull()) { - d_regexp_ant[str_in_re] = ant; } + if(flag) { + Trace("strings-loop") << "Strings::Loop: tails are different." << std::endl; + sendInference( antec, conc, "Loop Conflict", true ); + return true; + } + } - sendLemma( ant, conc, "F-LOOP" ); - ++(d_statistics.d_loop_lemmas); - - //we will be done - addNormalFormPair( normal_form_src[i], normal_form_src[j] ); + //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, "Len-Split(Loop-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, "Len-Split(Loop-YZ)" ); } 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; + //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 ); + if(d_loop_antec.find(ant) == d_loop_antec.end()) { + d_loop_antec.insert(ant); + + 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 if(t_yz.isConst()) { + Trace("strings-loop") << "Strings::Loop: Const Normal Breaking." << std::endl; + CVC4::String s = t_yz.getConst< CVC4::String >(); + unsigned size = s.size(); + std::vector< Node > vconc; + for(unsigned len=1; len<=size; len++) { + Node y = NodeManager::currentNM()->mkConst(s.substr(0, len)); + Node z = NodeManager::currentNM()->mkConst(s.substr(len, size - len)); + Node restr = s_zy; + Node cc; + if(r != d_emptyString) { + std::vector< Node > v2(vec_r); + v2.insert(v2.begin(), y); + v2.insert(v2.begin(), z); + restr = mkConcat( z, y ); + cc = Rewriter::rewrite(s_zy.eqNode( mkConcat( v2 ) )); + } else { + cc = Rewriter::rewrite(s_zy.eqNode( mkConcat( z, y) )); + } + if(cc == d_false) { + continue; + } + Node conc2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, normal_forms[other_n_index][other_index], + NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, + NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, y), + NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, + NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, restr)))); + cc = cc==d_true ? conc2 : NodeManager::currentNM()->mkNode( kind::AND, cc, conc2 ); + d_regexp_ant[conc2] = ant; + vconc.push_back(cc); + } + conc = vconc.size()==0 ? Node::null() : vconc.size()==1 ? vconc[0] : NodeManager::currentNM()->mkNode(kind::OR, vconc); + } else { + Trace("strings-loop") << "Strings::Loop: Normal Loop Breaking." << std::endl; + //right + Node sk_w= mkSkolemS( "w_loop" ); + Node sk_y= mkSkolemS( "y_loop", 1 ); + Node sk_z= mkSkolemS( "z_loop" ); + //t1 * ... * tn = y * z + Node conc1 = t_yz.eqNode( mkConcat( 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 ) ); + Node restr = r == d_emptyString ? s_zy : mkConcat( sk_z, sk_y ); + 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, restr ) ) ); + + 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());//by mkskolems + conc = NodeManager::currentNM()->mkNode( kind::AND, vec_conc ); + } // normal case + + //set its antecedant to ant, to say when it is relevant + if(!str_in_re.isNull()) { + d_regexp_ant[str_in_re] = ant; + } + //we will be done + addNormalFormPair( normal_form_src[i], normal_form_src[j] ); + if( options::stringProcessLoop() ){ + sendLemma( ant, conc, "F-LOOP" ); + ++(d_statistics.d_loop_lemmas); + }else{ + d_out->setIncomplete(); + return false; + } + + } 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; } return true; } @@ -2455,7 +2464,7 @@ bool TheoryStrings::processDeq( Node ni, Node nj ) { Node lsk2 = mkLength( sk2 ); conc.push_back( lsk2.eqNode( lj ) ); conc.push_back( NodeManager::currentNM()->mkNode( kind::OR, j.eqNode( mkConcat( sk1, sk3 ) ), i.eqNode( mkConcat( sk2, sk3 ) ) ) ); - sendLemma( mkExplain( antec, antec_new_lits ), NodeManager::currentNM()->mkNode( kind::AND, conc ), "D-DISL-Split" ); + sendInference( antec, antec_new_lits, NodeManager::currentNM()->mkNode( kind::AND, conc ), "D-DISL-Split" ); ++(d_statistics.d_deq_splits); return true; }else if( areEqual( li, lj ) ){ @@ -2516,8 +2525,7 @@ int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node } Node conc = cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( kind::AND, cc ); conc = Rewriter::rewrite( conc ); - sendLemma(mkExplain( ant ), conc, "Disequality Normalize Empty"); - //sendInfer(mkAnd( ant ), conc, "Disequality Normalize Empty"); + sendInference( ant, conc, "Disequality Normalize Empty", true); return -1; } else { Node i = nfi[index]; @@ -2681,6 +2689,39 @@ void TheoryStrings::registerTerm( Node n, int effort ) { } } +void TheoryStrings::sendInference( std::vector< Node >& exp, std::vector< Node >& exp_n, Node eq, const char * c, bool asLemma ) { + eq = eq.isNull() ? d_false : Rewriter::rewrite( eq ); + if( eq!=d_true ){ + bool doSendLemma = ( asLemma || eq==d_false || eq.getKind()==kind::OR || options::stringInferAsLemmas() ); + if( doSendLemma ){ + Node eq_exp; + if( options::stringRExplainLemmas() ){ + eq_exp = mkExplain( exp, exp_n ); + }else{ + if( exp.empty() ){ + eq_exp = mkAnd( exp_n ); + }else if( exp_n.empty() ){ + eq_exp = mkAnd( exp ); + }else{ + std::vector< Node > ev; + ev.insert( ev.end(), exp.begin(), exp.end() ); + ev.insert( ev.end(), exp_n.begin(), exp_n.end() ); + eq_exp = NodeManager::currentNM()->mkNode( kind::AND, ev ); + } + } + sendLemma( eq_exp, eq, c ); + }else{ + Assert( exp_n.empty() ); + sendInfer( mkAnd( exp ), eq, c ); + } + } +} + +void TheoryStrings::sendInference( std::vector< Node >& exp, Node eq, const char * c, bool asLemma ) { + std::vector< Node > exp_n; + sendInference( exp, exp_n, eq, c, asLemma ); +} + void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) { if( conc.isNull() || conc == d_false ) { d_out->conflict(ant); @@ -2703,37 +2744,33 @@ void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) { void TheoryStrings::sendInfer( Node eq_exp, Node eq, const char * c ) { Trace("strings-infer-debug") << "infer : " << eq << " from " << eq_exp << std::endl; - eq = Rewriter::rewrite( eq ); - if( eq==d_false || eq.getKind()==kind::OR ) { - sendLemma( eq_exp, eq, c ); - }else if( eq!=d_true ){ - if( options::stringInferSym() ){ - std::vector< Node > vars; - std::vector< Node > subs; - std::vector< Node > unproc; - inferSubstitutionProxyVars( eq_exp, vars, subs, unproc ); - if( unproc.empty() ){ - Trace("strings-lemma-debug") << "Strings::Infer " << eq << " from " << eq_exp << " by " << c << std::endl; - Node eqs = eq.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); - Trace("strings-lemma-debug") << "Strings::Infer Alternate : " << eqs << std::endl; - for( unsigned i=0; i " << subs[i] << std::endl; - } - sendLemma( d_true, eqs, c ); - return; - }else{ - for( unsigned i=0; i vars; + std::vector< Node > subs; + std::vector< Node > unproc; + inferSubstitutionProxyVars( eq_exp, vars, subs, unproc ); + if( unproc.empty() ){ + Trace("strings-lemma-debug") << "Strings::Infer " << eq << " from " << eq_exp << " by " << c << std::endl; + Node eqs = eq.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + Trace("strings-lemma-debug") << "Strings::Infer Alternate : " << eqs << std::endl; + for( unsigned i=0; i " << subs[i] << std::endl; + } + sendLemma( d_true, eqs, c ); + return; + }else{ + for( unsigned i=0; i " << eq_exp << " " << eq << ")) ; infer " << c << 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 ); } + Trace("strings-lemma") << "Strings::Infer " << eq << " from " << eq_exp << " by " << c << std::endl; + Trace("strings-assert") << "(assert (=> " << eq_exp << " " << eq << ")) ; infer " << c << 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 ); + } void TheoryStrings::sendSplit( Node a, Node b, const char * c, bool preq ) { @@ -3011,7 +3048,7 @@ void TheoryStrings::checkLengthsEqc() { Node eq = llt.eqNode( lc ); if( llt!=lc ){ ei->d_normalized_length.set( eq ); - sendLemma( mkExplain( ant ), eq, "LEN-NORM" ); + sendInference( ant, eq, "LEN-NORM", true ); } } }else{ @@ -3027,7 +3064,7 @@ void TheoryStrings::checkLengthsEqc() { Assert( d_proxy_var_to_length.find( pv )!=d_proxy_var_to_length.end() ); Node pvl = d_proxy_var_to_length[pv]; Node ceq = Rewriter::rewrite( mkLength( pv ).eqNode( pvl ) ); - sendLemma( d_true, ceq, "LEN-NORM-I" ); + sendInference( d_empty_vec, ceq, "LEN-NORM-I", true ); } } */ @@ -3093,13 +3130,12 @@ void TheoryStrings::checkCardinality() { vec_node.push_back( len_eq_lr ); } } - Node antc = NodeManager::currentNM()->mkNode( kind::AND, vec_node ); Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, cols[i][0] ); Node cons = NodeManager::currentNM()->mkNode( kind::GEQ, len, k_node ); cons = Rewriter::rewrite( cons ); ei->d_cardinality_lem_k.set( int_k+1 ); if( cons!=d_true ){ - sendLemma( antc, cons, "CARDINALITY" ); + sendInference( d_empty_vec, vec_node, cons, "CARDINALITY", true ); return; } } @@ -3362,9 +3398,8 @@ bool TheoryStrings::normalizePosMemberships(std::map< Node, std::vector< Node > inter_r = d_regexp_opr.intersect(inter_r, inter_r2, spflag); if(inter_r == d_emptyRegexp) { //conflict - Node antec = exp.size() == 1? exp[0] : NodeManager::currentNM()->mkNode(kind::AND, exp); Node conc; - sendLemma(antec, conc, "INTERSECT CONFLICT"); + sendInference( d_empty_vec, exp, conc, "INTERSECT CONFLICT", true ); addLemma = true; break; } @@ -3435,17 +3470,15 @@ bool TheoryStrings::applyRLen(std::map< Node, std::vector< Node > > &XinR_with_e bool TheoryStrings::checkMembershipsWithoutLength( std::map< Node, std::vector< Node > > &memb_with_exps, std::map< Node, std::vector< Node > > &XinR_with_exps) { - for(std::map< Node, std::vector< Node > >::const_iterator itr = memb_with_exps.begin(); - itr != memb_with_exps.end(); ++itr) { + for(std::map< Node, std::vector< Node > >::iterator itr = memb_with_exps.begin(); itr != memb_with_exps.end(); ++itr) { Node memb = itr->first; Node s = memb[0]; Node r = memb[1]; if(s.isConst()) { memb = Rewriter::rewrite( memb ); if(memb == d_false) { - Node antec = itr->second.size() == 1? itr->second[0] : NodeManager::currentNM()->mkNode(kind::AND, itr->second); Node conc; - sendLemma(antec, conc, "MEMBERSHIP CONFLICT"); + sendInference(d_empty_vec, itr->second, conc, "MEMBERSHIP CONFLICT", true); //addLemma = true; return true; } else { @@ -3456,14 +3489,13 @@ bool TheoryStrings::checkMembershipsWithoutLength( XinR_with_exps[itr->first] = itr->second; } else { Assert(s.getKind() == kind::STRING_CONCAT); - Node antec = itr->second.size() == 1? itr->second[0] : NodeManager::currentNM()->mkNode(kind::AND, itr->second); Node conc; for( unsigned i=0; i() ); //R-Consume, see Tianyi's thesis if(!applyRConsume(str, r)) { - sendLemma(antec, conc, "R-Consume CONFLICT"); + sendInference(d_empty_vec, itr->second, conc, "R-Consume CONFLICT", true); //addLemma = true; return true; } @@ -3485,11 +3517,11 @@ bool TheoryStrings::checkMembershipsWithoutLength( break; } else if(conc.isNull() || conc == d_false) { conc = Node::null(); - sendLemma(antec, conc, "R-Split Conflict"); + sendInference(d_empty_vec, itr->second, conc, "R-Split Conflict", true); //addLemma = true; return true; } else { - sendLemma(antec, conc, "R-Split"); + sendInference(d_empty_vec, itr->second, conc, "R-Split", true); //addLemma = true; return true; } @@ -3587,9 +3619,8 @@ void TheoryStrings::checkMemberships() { Node n = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, *itr2); vec_nodes.push_back( n ); } - Node antec = vec_nodes.size() == 1? vec_nodes[0] : NodeManager::currentNM()->mkNode(kind::AND, vec_nodes); Node conc; - sendLemma(antec, conc, "INTERSECT CONFLICT"); + sendInference(vec_nodes, conc, "INTERSECT CONFLICT", true); addedLemma = true; break; } @@ -3679,9 +3710,6 @@ void TheoryStrings::checkMemberships() { } else { processed.push_back( assertion ); } - } else if(conc == d_false) { - conc = Node::null(); - sendLemma(antec, conc, "RegExp CST-SP Conflict"); } else { sendLemma(antec, conc, "RegExp-CST-SP"); } @@ -3730,8 +3758,7 @@ void TheoryStrings::checkMemberships() { } } antec = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, antec, mkExplain(rnfexp)) ); - Node conc = nvec.size()==1 ? nvec[0] : - NodeManager::currentNM()->mkNode(kind::AND, nvec); + Node conc = nvec.size()==1 ? nvec[0] : NodeManager::currentNM()->mkNode(kind::AND, nvec); conc = Rewriter::rewrite(conc); sendLemma( antec, conc, "REGEXP" ); addedLemma = true; @@ -3964,7 +3991,7 @@ void TheoryStrings::checkConstantEquivalenceClasses( TermIndex* ti, std::vector< //exp contains an explanation of n==c Assert( countc==vecc.size() ); if( hasTerm( c ) ){ - sendInfer( mkAnd( exp ), n.eqNode( c ), "I_CONST_MERGE" ); + sendInference( exp, n.eqNode( c ), "I_CONST_MERGE" ); return; }else if( !hasProcessed() ){ Node nr = getRepresentative( n ); @@ -3985,7 +4012,7 @@ void TheoryStrings::checkConstantEquivalenceClasses( TermIndex* ti, std::vector< exp.push_back( d_eqc_to_const_exp[nr] ); addToExplanation( n, d_eqc_to_const_base[nr], exp ); } - sendLemma( mkExplain( exp ), d_false, "I_CONST_CONFLICT" ); + sendInference( exp, d_false, "I_CONST_CONFLICT" ); return; }else{ Trace("strings-debug") << "Duplicate constant." << std::endl; @@ -4071,7 +4098,7 @@ void TheoryStrings::checkNegContains( std::vector< Node >& negContains ) { lexp.push_back( atom.negate() ); Node xneqs = x.eqNode(s).negate(); d_neg_ctn_eqlen.insert( atom ); - sendLemma( mkExplain( lexp ), xneqs, "NEG-CTN-EQL" ); + sendInference( lexp, xneqs, "NEG-CTN-EQL", true ); } }else if( !areDisequal( lenx, lens ) ){ if(d_neg_ctn_ulen.find(atom) == d_neg_ctn_ulen.end()) { @@ -4111,7 +4138,9 @@ void TheoryStrings::checkNegContains( std::vector< Node >& negContains ) { conc = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::OR, xlss, conc ) ); d_neg_ctn_cached.insert( atom ); - sendLemma( atom.negate(), conc, "NEG-CTN-BRK" ); + std::vector< Node > exp; + exp.push_back( atom.negate() ); + sendInference( d_empty_vec, exp, conc, "NEG-CTN-BRK", true ); //d_pending_req_phase[xlss] = true; } } diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index fef2983fd..63098552d 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -174,7 +174,7 @@ private: NodeBoolMap d_preproc_cache; // extended functions inferences cache NodeSet d_extf_infer_cache; - + std::vector< Node > d_empty_vec; private: NodeSet d_congruent; std::map< Node, Node > d_eqc_to_const; @@ -337,6 +337,8 @@ protected: //register term void registerTerm( Node n, int effort ); //send lemma + void sendInference( std::vector< Node >& exp, std::vector< Node >& exp_n, Node eq, const char * c, bool asLemma = false ); + void sendInference( std::vector< Node >& exp, Node eq, const char * c, bool asLemma = false ); void sendLemma( Node ant, Node conc, const char * c ); void sendInfer( Node eq_exp, Node eq, const char * c ); void sendSplit( Node a, Node b, const char * c, bool preq = true ); diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 661c67354..977b9f4c1 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1039,9 +1039,8 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){ //check for abort case if( options::ufssAbortCardinality()==d_aloc_cardinality ){ - //abort here DO_THIS Message() << "Maximum cardinality reached." << std::endl; - exit( 0 ); + exit( 1 ); }else{ if( applyTotality( d_aloc_cardinality ) ){ //must generate new cardinality lemma term diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index f5c6048e6..2058f429b 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -74,7 +74,8 @@ TESTS = \ idof-handg.smt2 \ fmf001.smt2 \ type002.smt2 \ - crash-1019.smt2 + crash-1019.smt2 \ + norn-31.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/strings/norn-31.smt2 b/test/regress/regress0/strings/norn-31.smt2 new file mode 100644 index 000000000..4698f966f --- /dev/null +++ b/test/regress/regress0/strings/norn-31.smt2 @@ -0,0 +1,23 @@ +(set-logic QF_SLIA) +(set-option :strings-exp true) +(set-info :status unsat) + +(declare-fun var_0 () String) +(declare-fun var_1 () String) +(declare-fun var_2 () String) +(declare-fun var_3 () String) +(declare-fun var_4 () String) +(declare-fun var_5 () String) +(declare-fun var_6 () String) +(declare-fun var_7 () String) +(declare-fun var_8 () String) +(declare-fun var_9 () String) +(declare-fun var_10 () String) +(declare-fun var_11 () String) +(declare-fun var_12 () String) + +(assert (str.in.re var_1 (re.* (re.range "a" "u")))) +(assert (str.in.re var_1 (re.++ (re.* (str.to.re "a")) (str.to.re "b")))) +(assert (str.in.re var_1 (re.++ (re.++ (re.++ (re.* (re.union (str.to.re "a") (str.to.re "b"))) (str.to.re "b")) (str.to.re "a")) (re.* (re.union (str.to.re "a") (str.to.re "b")))))) +(assert (not (str.in.re "" re.nostr))) +(check-sat) -- 2.30.2