From: Andrew Reynolds Date: Wed, 19 Sep 2018 01:10:59 +0000 (-0500) Subject: Refactor strings extended functions inferences (#2480) X-Git-Tag: cvc5-1.0.0~4628 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2bb0196d4f9d0891bc7e95fff444c61ab09ee651;p=cvc5.git Refactor strings extended functions inferences (#2480) This refactors the extended function inference step of TheoryStrings. It also generalizes a data member (d_pol) so that we track extended functions that are equal to constants for any type. This is in preparation for working on solving equations and further inferences in this style. --- diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 4b73e496e..1acb5ec95 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -397,7 +397,12 @@ int TheoryStrings::getReduction( int effort, Node n, Node& nr ) { Assert( d_extf_info_tmp.find( n )!=d_extf_info_tmp.end() ); if( d_extf_info_tmp[n].d_model_active ){ int r_effort = -1; - int pol = d_extf_info_tmp[n].d_pol; + // polarity : 1 true, -1 false, 0 neither + int pol = 0; + if (n.getType().isBoolean() && !d_extf_info_tmp[n].d_const.isNull()) + { + pol = d_extf_info_tmp[n].d_const.getConst() ? 1 : -1; + } if( n.getKind()==kind::STRING_STRCTN ){ if( pol==1 ){ r_effort = 1; @@ -1505,22 +1510,23 @@ void TheoryStrings::checkExtfEval( int effort ) { Node n = terms[i]; Node sn = sterms[i]; //setup information about extf - d_extf_info_tmp[n].init(); - std::map< Node, ExtfInfoTmp >::iterator itit = d_extf_info_tmp.find( n ); - if( n.getType().isBoolean() ){ - if( areEqual( n, d_true ) ){ - itit->second.d_pol = 1; - }else if( areEqual( n, d_false ) ){ - itit->second.d_pol = -1; - } + ExtfInfoTmp& einfo = d_extf_info_tmp[n]; + Node r = getRepresentative(n); + std::map::iterator itcit = d_eqc_to_const.find(r); + if (itcit != d_eqc_to_const.end()) + { + einfo.d_const = itcit->second; } - Trace("strings-extf-debug") << "Check extf " << n << " == " << sn << ", pol = " << itit->second.d_pol << ", effort=" << effort << "..." << std::endl; + Trace("strings-extf-debug") << "Check extf " << n << " == " << sn + << ", constant = " << einfo.d_const + << ", effort=" << effort << "..." << std::endl; //do the inference Node to_reduce; if( n!=sn ){ - itit->second.d_exp.insert( itit->second.d_exp.end(), exp[i].begin(), exp[i].end() ); + einfo.d_exp.insert(einfo.d_exp.end(), exp[i].begin(), exp[i].end()); // inference is rewriting the substituted node Node nrc = Rewriter::rewrite( sn ); + Kind nrck = nrc.getKind(); //if rewrites to a constant, then do the inference and mark as reduced if( nrc.isConst() ){ if( effort<3 ){ @@ -1565,13 +1571,13 @@ void TheoryStrings::checkExtfEval( int effort ) { }else{ conc = nrs.eqNode( nrc ); } - itit->second.d_exp.clear(); + einfo.d_exp.clear(); } }else{ if( !areEqual( n, nrc ) ){ if( n.getType().isBoolean() ){ if( areEqual( n, nrc==d_true ? d_false : d_true ) ){ - itit->second.d_exp.push_back( nrc==d_true ? n.negate() : n ); + einfo.d_exp.push_back(nrc == d_true ? n.negate() : n); conc = d_false; }else{ conc = nrc==d_true ? n : n.negate(); @@ -1583,7 +1589,8 @@ void TheoryStrings::checkExtfEval( int effort ) { } if( !conc.isNull() ){ Trace("strings-extf") << " resolve extf : " << sn << " -> " << nrc << std::endl; - sendInference( itit->second.d_exp, conc, effort==0 ? "EXTF" : "EXTF-N", true ); + sendInference( + einfo.d_exp, conc, effort == 0 ? "EXTF" : "EXTF-N", true); if( d_conflict ){ Trace("strings-extf-debug") << " conflict, return." << std::endl; return; @@ -1593,18 +1600,25 @@ void TheoryStrings::checkExtfEval( int effort ) { //check if it is already equal, if so, mark as reduced. Otherwise, do nothing. if( areEqual( n, nrc ) ){ Trace("strings-extf") << " resolved extf, since satisfied by model: " << n << std::endl; - itit->second.d_model_active = false; + einfo.d_model_active = false; } } //if it reduces to a conjunction, infer each and reduce - }else if( ( nrc.getKind()==kind::OR && itit->second.d_pol==-1 ) || ( nrc.getKind()==kind::AND && itit->second.d_pol==1 ) ){ + } + else if ((nrck == OR && einfo.d_const == d_false) + || (nrck == AND && einfo.d_const == d_true)) + { Assert( effort<3 ); getExtTheory()->markReduced( n ); - itit->second.d_exp.push_back( itit->second.d_pol==-1 ? n.negate() : n ); + einfo.d_exp.push_back(einfo.d_const == d_false ? n.negate() : n); Trace("strings-extf-debug") << " decomposable..." << std::endl; - Trace("strings-extf") << " resolve extf : " << sn << " -> " << nrc << ", pol = " << itit->second.d_pol << std::endl; - for( unsigned i=0; isecond.d_exp, itit->second.d_pol==-1 ? nrc[i].negate() : nrc[i], effort==0 ? "EXTF_d" : "EXTF_d-N" ); + Trace("strings-extf") << " resolve extf : " << sn << " -> " << nrc + << ", const = " << einfo.d_const << std::endl; + for (const Node& nrcc : nrc) + { + sendInference(einfo.d_exp, + einfo.d_const == d_false ? nrcc.negate() : nrcc, + effort == 0 ? "EXTF_d" : "EXTF_d-N"); } }else{ to_reduce = nrc; @@ -1618,18 +1632,20 @@ void TheoryStrings::checkExtfEval( int effort ) { if( effort==1 ){ Trace("strings-extf") << " cannot rewrite extf : " << to_reduce << std::endl; } - checkExtfInference( n, to_reduce, itit->second, effort ); + checkExtfInference(n, to_reduce, einfo, effort); if( Trace.isOn("strings-extf-list") ){ Trace("strings-extf-list") << " * " << to_reduce; - if( itit->second.d_pol!=0 ){ - Trace("strings-extf-list") << ", pol = " << itit->second.d_pol; + if (!einfo.d_const.isNull()) + { + Trace("strings-extf-list") << ", const = " << einfo.d_const; } if( n!=to_reduce ){ Trace("strings-extf-list") << ", from " << n; } Trace("strings-extf-list") << std::endl; - } - if( getExtTheory()->isActive( n ) && itit->second.d_model_active ){ + } + if (getExtTheory()->isActive(n) && einfo.d_model_active) + { has_nreduce = true; } } @@ -1638,81 +1654,144 @@ void TheoryStrings::checkExtfEval( int effort ) { } void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int effort ){ - //make additional inferences that do not contribute to the reduction of n, but may help show a refutation - if( in.d_pol!=0 ){ - //add original to explanation - in.d_exp.push_back( in.d_pol==1 ? n : n.negate() ); - - //d_extf_infer_cache stores whether we have made the inferences associated with a node n, - // this may need to be generalized if multiple inferences apply - - if( nr.getKind()==kind::STRING_STRCTN ){ - if( ( in.d_pol==1 && nr[1].getKind()==kind::STRING_CONCAT ) || ( in.d_pol==-1 && nr[0].getKind()==kind::STRING_CONCAT ) ){ - if( d_extf_infer_cache.find( nr )==d_extf_infer_cache.end() ){ - d_extf_infer_cache.insert( nr ); - - //one argument does (not) contain each of the components of the other argument - int index = in.d_pol==1 ? 1 : 0; - std::vector< Node > children; - children.push_back( nr[0] ); - children.push_back( nr[1] ); - //Node exp_n = mkAnd( exp ); - for( unsigned i=0; imkNode( kind::STRING_STRCTN, children ); - conc = Rewriter::rewrite(in.d_pol == 1 ? conc : conc.negate()); - // check if it already (does not) hold - if (hasTerm(conc)) + if (in.d_const.isNull()) + { + return; + } + NodeManager* nm = NodeManager::currentNM(); + + Node exp = n.eqNode(in.d_const); + exp = Rewriter::rewrite(exp); + + // add original to explanation + in.d_exp.push_back(exp); + + // d_extf_infer_cache stores whether we have made the inferences associated + // with a node n, + // this may need to be generalized if multiple inferences apply + + if (nr.getKind() == STRING_STRCTN) + { + Assert(in.d_const.isConst()); + bool pol = in.d_const.getConst(); + if ((pol && nr[1].getKind() == STRING_CONCAT) + || (!pol && nr[0].getKind() == STRING_CONCAT)) + { + // If str.contains( x, str.++( y1, ..., yn ) ), + // we may infer str.contains( x, y1 ), ..., str.contains( x, yn ) + // The following recognizes two situations related to the above reasoning: + // (1) If ~str.contains( x, yi ) holds for some i, we are in conflict, + // (2) If str.contains( x, yj ) already holds for some j, then the term + // str.contains( x, yj ) is irrelevant since it is satisfied by all models + // for str.contains( x, str.++( y1, ..., yn ) ). + + // Notice that the dual of the above reasoning also holds, i.e. + // If ~str.contains( str.++( x1, ..., xn ), y ), + // we may infer ~str.contains( x1, y ), ..., ~str.contains( xn, y ) + // This is also handled here. + if (d_extf_infer_cache.find(nr) == d_extf_infer_cache.end()) + { + d_extf_infer_cache.insert(nr); + + int index = pol ? 1 : 0; + std::vector children; + children.push_back(nr[0]); + children.push_back(nr[1]); + for (const Node& nrc : nr[index]) + { + children[index] = nrc; + Node conc = nm->mkNode(STRING_STRCTN, children); + conc = Rewriter::rewrite(pol ? conc : conc.negate()); + // check if it already (does not) hold + if (hasTerm(conc)) + { + if (areEqual(conc, d_false)) { - if (areEqual(conc, d_false)) - { - // should be a conflict - sendInference(in.d_exp, conc, "CTN_Decompose"); - } - else if (getExtTheory()->hasFunctionKind(conc.getKind())) - { - // can mark as reduced, since model for n => model for conc - getExtTheory()->markReduced(conc); - } + // we are in conflict + sendInference(in.d_exp, conc, "CTN_Decompose"); + } + else if (getExtTheory()->hasFunctionKind(conc.getKind())) + { + // can mark as reduced, since model for n implies model for conc + getExtTheory()->markReduced(conc); } } - } - }else{ - //store this (reduced) assertion - //Assert( effort==0 || nr[0]==getRepresentative( nr[0] ) ); - bool pol = in.d_pol==1; - if( std::find( d_extf_info_tmp[nr[0]].d_ctn[pol].begin(), d_extf_info_tmp[nr[0]].d_ctn[pol].end(), nr[1] )==d_extf_info_tmp[nr[0]].d_ctn[pol].end() ){ - Trace("strings-extf-debug") << " store contains info : " << nr[0] << " " << pol << " " << nr[1] << std::endl; - d_extf_info_tmp[nr[0]].d_ctn[pol].push_back( nr[1] ); - d_extf_info_tmp[nr[0]].d_ctn_from[pol].push_back( n ); - //transitive closure for contains - bool opol = !pol; - for( unsigned i=0; imkNode( kind::STRING_STRCTN, pol ? nr[1] : onr, pol ? onr : nr[1] ); - conc = Rewriter::rewrite( conc ); - bool do_infer = false; - if( conc.getKind()==kind::EQUAL ){ - do_infer = !areDisequal( conc[0], conc[1] ); - }else{ - do_infer = !areEqual( conc, d_false ); - } - if( do_infer ){ - conc = conc.negate(); - std::vector< Node > exp_c; - exp_c.insert( exp_c.end(), in.d_exp.begin(), in.d_exp.end() ); - Node ofrom = d_extf_info_tmp[nr[0]].d_ctn_from[opol][i]; - Assert( d_extf_info_tmp.find( ofrom )!=d_extf_info_tmp.end() ); - exp_c.insert( exp_c.end(), d_extf_info_tmp[ofrom].d_exp.begin(), d_extf_info_tmp[ofrom].d_exp.end() ); - sendInference( exp_c, conc, "CTN_Trans" ); - } + } + } + else + { + if (std::find(d_extf_info_tmp[nr[0]].d_ctn[pol].begin(), + d_extf_info_tmp[nr[0]].d_ctn[pol].end(), + nr[1]) + == d_extf_info_tmp[nr[0]].d_ctn[pol].end()) + { + Trace("strings-extf-debug") << " store contains info : " << nr[0] + << " " << pol << " " << nr[1] << std::endl; + // Store s (does not) contains t, since nr = (~)contains( s, t ) holds. + d_extf_info_tmp[nr[0]].d_ctn[pol].push_back(nr[1]); + d_extf_info_tmp[nr[0]].d_ctn_from[pol].push_back(n); + // Do transistive closure on contains, e.g. + // if contains( s, t ) and ~contains( s, r ), then ~contains( t, r ). + + // The following infers new (negative) contains based on the above + // reasoning, provided that ~contains( t, r ) does not + // already hold in the current context. We test this by checking that + // contains( t, r ) is not already asserted false in the current + // context. We also handle the case where contains( t, r ) is equivalent + // to t = r, in which case we check that t != r does not already hold + // in the current context. + + // Notice that form of the above inference is enough to find + // conflicts purely due to contains predicates. For example, if we + // have only positive occurrences of contains, then no conflicts due to + // contains predicates are possible and this schema does nothing. For + // example, note that contains( s, t ) and contains( t, r ) implies + // contains( s, r ), which we could but choose not to infer. Instead, + // we prefer being lazy: only if ~contains( s, r ) appears later do we + // infer ~contains( t, r ), which suffices to show a conflict. + bool opol = !pol; + for (unsigned i = 0, size = d_extf_info_tmp[nr[0]].d_ctn[opol].size(); + i < size; + i++) + { + Node onr = d_extf_info_tmp[nr[0]].d_ctn[opol][i]; + Node conc = + nm->mkNode(STRING_STRCTN, pol ? nr[1] : onr, pol ? onr : nr[1]); + conc = Rewriter::rewrite(conc); + bool do_infer = false; + if (conc.getKind() == EQUAL) + { + do_infer = !areDisequal(conc[0], conc[1]); + } + else + { + do_infer = !areEqual(conc, d_false); + } + if (do_infer) + { + conc = conc.negate(); + std::vector exp_c; + exp_c.insert(exp_c.end(), in.d_exp.begin(), in.d_exp.end()); + Node ofrom = d_extf_info_tmp[nr[0]].d_ctn_from[opol][i]; + Assert(d_extf_info_tmp.find(ofrom) != d_extf_info_tmp.end()); + exp_c.insert(exp_c.end(), + d_extf_info_tmp[ofrom].d_exp.begin(), + d_extf_info_tmp[ofrom].d_exp.end()); + sendInference(exp_c, conc, "CTN_Trans"); } - }else{ - Trace("strings-extf-debug") << " redundant." << std::endl; - getExtTheory()->markReduced( n ); } } + else + { + // If we already know that s (does not) contain t, then n is redundant. + // For example, if str.contains( x, y ), str.contains( z, y ), and x=z + // are asserted in the current context, then str.contains( z, y ) is + // satisfied by all models of str.contains( x, y ) ^ x=z and thus can + // be ignored. + Trace("strings-extf-debug") << " redundant." << std::endl; + getExtTheory()->markReduced(n); + } } } } @@ -4503,8 +4582,9 @@ void TheoryStrings::checkMemberships() { for (unsigned i = 0; i < mems.size(); i++) { Node n = mems[i]; Assert( d_extf_info_tmp.find( n )!=d_extf_info_tmp.end() ); - if( d_extf_info_tmp[n].d_pol==1 || d_extf_info_tmp[n].d_pol==-1 ){ - bool pol = d_extf_info_tmp[n].d_pol==1; + if (!d_extf_info_tmp[n].d_const.isNull()) + { + bool pol = d_extf_info_tmp[n].d_const.getConst(); Trace("strings-process-debug") << " add membership : " << n << ", pol = " << pol << std::endl; addMembership( pol ? n : n.negate() ); }else{ diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 73906d029..2fd7b3525 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -289,6 +289,25 @@ private: NodeList d_ee_disequalities; private: NodeSet d_congruent; + /** + * The following three vectors are used for tracking constants that each + * equivalence class is entailed to be equal to. + * - The map d_eqc_to_const maps (representatives) r of equivalence classes to + * the constant that that equivalence class is entailed to be equal to, + * - The term d_eqc_to_const_base[r] is the term in the equivalence class r + * that is entailed to be equal to the constant d_eqc_to_const[r], + * - The term d_eqc_to_const_exp[r] is the explanation of why + * d_eqc_to_const_base[r] is equal to d_eqc_to_const[r]. + * + * For example, consider the equivalence class { r, x++"a"++y, x++z }, and + * assume x = "" and y = "bb" in the current context. We have that + * d_eqc_to_const[r] = "abb", + * d_eqc_to_const_base[r] = x++"a"++y + * d_eqc_to_const_exp[r] = ( x = "" AND y = "bb" ) + * + * This information is computed during checkInit and is used during various + * inference schemas for deriving inferences. + */ std::map< Node, Node > d_eqc_to_const; std::map< Node, Node > d_eqc_to_const_base; std::map< Node, Node > d_eqc_to_const_exp; @@ -375,24 +394,6 @@ private: //all variables in this term std::vector< Node > d_vars; }; - // non-static information about extf - class ExtfInfoTmp { - public: - void init(){ - d_pol = 0; - d_model_active = true; - } - // list of terms that something (does not) contain and their explanation - std::map< bool, std::vector< Node > > d_ctn; - std::map< bool, std::vector< Node > > d_ctn_from; - //polarity - int d_pol; - //explanation - std::vector< Node > d_exp; - //false if it is reduced in the model - bool d_model_active; - }; - std::map< Node, ExtfInfoTmp > d_extf_info_tmp; private: /** Length status, used for the registerLength function below */ @@ -441,9 +442,59 @@ private: SkolemCache d_sk_cache; void checkConstantEquivalenceClasses( TermIndex* ti, std::vector< Node >& vecc ); - void checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int effort ); Node getSymbolicDefinition( Node n, std::vector< Node >& exp ); + //--------------------------for checkExtfEval + /** + * Non-static information about an extended function t. This information is + * constructed and used during the check extended function evaluation + * inference schema. + * + * In the following, we refer to the "context-dependent simplified form" + * of a term t to be the result of rewriting t * sigma, where sigma is a + * derivable substitution in the current context. For example, the + * context-depdendent simplified form of contains( x++y, "a" ) given + * sigma = { x -> "" } is contains(y,"a"). + */ + class ExtfInfoTmp + { + public: + ExtfInfoTmp() : d_model_active(true) {} + /** + * If s is in d_ctn[true] (resp. d_ctn[false]), then contains( t, s ) + * (resp. ~contains( t, s )) holds in the current context. The vector + * d_ctn_from is the explanation for why this holds. For example, + * if d_ctn[false][i] is "A", then d_ctn_from[false][i] might be + * t = x ++ y AND x = "" AND y = "B". + */ + std::map > d_ctn; + std::map > d_ctn_from; + /** + * The constant that t is entailed to be equal to, or null if none exist. + */ + Node d_const; + /** + * The explanation for why t is equal to its context-dependent simplified + * form. + */ + std::vector d_exp; + /** This flag is false if t is reduced in the model. */ + bool d_model_active; + }; + /** map extended functions to the above information */ + std::map d_extf_info_tmp; + /** check extended function inferences + * + * This function makes additional inferences for n that do not contribute + * to its reduction, but may help show a refutation. + * + * This function is called when the context-depdendent simplified form of + * n is nr. The argument "in" is the information object for n. The argument + * "effort" has the same meaning as the effort argument of checkExtfEval. + */ + void checkExtfInference(Node n, Node nr, ExtfInfoTmp& in, int effort); + //--------------------------end for checkExtfEval + //--------------------------for checkFlatForm /** * This checks whether there are flat form inferences between eqc[start] and