diff options
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/sep/kinds | 2 | ||||
| -rw-r--r-- | src/theory/sep/theory_sep.cpp | 45 | ||||
| -rw-r--r-- | src/theory/sep/theory_sep.h | 4 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 270 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.h | 89 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 39 |
6 files changed, 296 insertions, 153 deletions
diff --git a/src/theory/sep/kinds b/src/theory/sep/kinds index b83515d38..235b61172 100644 --- a/src/theory/sep/kinds +++ b/src/theory/sep/kinds @@ -8,7 +8,7 @@ theory THEORY_SEP ::CVC4::theory::sep::TheorySep "theory/sep/theory_sep.h" typechecker "theory/sep/theory_sep_type_rules.h" properties polite stable-infinite parametric -properties check propagate presolve getNextDecisionRequest +properties check propagate presolve rewriter ::CVC4::theory::sep::TheorySepRewriter "theory/sep/theory_sep_rewriter.h" diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 6085b1f23..d1ba65dd8 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -311,6 +311,7 @@ void TheorySep::check(Effort e) { TimerStat::CodeTimer checkTimer(d_checkTime); Trace("sep-check") << "Sep::check(): " << e << endl; + NodeManager* nm = NodeManager::currentNM(); while( !done() && !d_conflict ){ // Get all the assertions @@ -454,12 +455,16 @@ void TheorySep::check(Effort e) { if( !use_polarity ){ // introduce guard, assert positive version Trace("sep-lemma-debug") << "Negated spatial constraint asserted to sep theory: " << fact << std::endl; - Node lit = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) ); - lit = getValuation().ensureLiteral( lit ); + Node g = nm->mkSkolem("G", nm->booleanType()); + d_neg_guard_strategy[g].reset(new DecisionStrategySingleton( + "sep_neg_guard", g, getSatContext(), getValuation())); + DecisionStrategySingleton* ds = d_neg_guard_strategy[g].get(); + getDecisionManager()->registerStrategy( + DecisionManager::STRAT_SEP_NEG_GUARD, ds); + Node lit = ds->getLiteral(0); d_neg_guard[s_lbl][s_atom] = lit; Trace("sep-lemma-debug") << "Neg guard : " << s_lbl << " " << s_atom << " " << lit << std::endl; AlwaysAssert( !lit.isNull() ); - d_out->requirePhase( lit, true ); d_neg_guards.push_back( lit ); d_guard_to_assertion[lit] = s_atom; //Node lem = NodeManager::currentNM()->mkNode( kind::EQUAL, lit, conc ); @@ -822,40 +827,6 @@ bool TheorySep::needsCheckLastEffort() { return hasFacts(); } -Node TheorySep::getNextDecisionRequest( unsigned& priority ) { - for( unsigned i=0; i<d_neg_guards.size(); i++ ){ - Node g = d_neg_guards[i]; - bool success = true; - if( getLogicInfo().isQuantified() ){ - Assert( d_guard_to_assertion.find( g )!= d_guard_to_assertion.end() ); - Node a = d_guard_to_assertion[g]; - Node q = quantifiers::TermUtil::getInstConstAttr( a ); - if( !q.isNull() ){ - //must wait to decide on counterexample literal from quantified formula - Node cel = getQuantifiersEngine()->getTermUtil()->getCounterexampleLiteral( q ); - bool value; - if( d_valuation.hasSatValue( cel, value ) ){ - Trace("sep-dec-debug") << "TheorySep::getNextDecisionRequest : dependent guard " << g << " depends on value for guard for quantified formula : " << value << std::endl; - success = value; - }else{ - Trace("sep-dec-debug") << "TheorySep::getNextDecisionRequest : wait to decide on " << g << " until " << cel << " is set " << std::endl; - success = false; - } - } - } - if( success ){ - bool value; - if( !d_valuation.hasSatValue( g, value ) ) { - Trace("sep-dec") << "TheorySep::getNextDecisionRequest : " << g << " (" << i << "/" << d_neg_guards.size() << ")" << std::endl; - priority = 0; - return g; - } - } - } - Trace("sep-dec-debug") << "TheorySep::getNextDecisionRequest : null" << std::endl; - return Node::null(); -} - void TheorySep::conflict(TNode a, TNode b) { Trace("sep-conflict") << "Sep::conflict : " << a << " " << b << std::endl; Node conflictNode = explain(a.eqNode(b)); diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index df384739d..f8bb58784 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -112,7 +112,6 @@ class TheorySep : public Theory { ///////////////////////////////////////////////////////////////////////////// public: - Node getNextDecisionRequest(unsigned& priority) override; void presolve() override; void shutdown() override {} @@ -218,6 +217,9 @@ class TheorySep : public Theory { std::map< Node, std::map< Node, Node > > d_red_conc; std::map< Node, std::map< Node, Node > > d_neg_guard; std::vector< Node > d_neg_guards; + /** a (singleton) decision strategy for each negative guard. */ + std::map<Node, std::unique_ptr<DecisionStrategySingleton> > + d_neg_guard_strategy; std::map< Node, Node > d_guard_to_assertion; /** inferences: maintained to ensure ref count for internally introduced nodes */ NodeList d_infer; 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<bool>() ? 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<Node, Node>::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; i<nrc.getNumChildren(); i++ ){ - sendInference( itit->second.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; i<nr[index].getNumChildren(); i++ ){ - children[index] = nr[index][i]; - Node conc = NodeManager::currentNM()->mkNode( 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<bool>(); + 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<Node> 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; i<d_extf_info_tmp[nr[0]].d_ctn[opol].size(); i++ ){ - Node onr = d_extf_info_tmp[nr[0]].d_ctn[opol][i]; - Node conc = NodeManager::currentNM()->mkNode( 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<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{ - 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<bool>(); 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<bool, std::vector<Node> > d_ctn; + std::map<bool, std::vector<Node> > 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<Node> 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<Node, ExtfInfoTmp> 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 diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 6a9648311..7803224c6 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1495,6 +1495,45 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) { Node ret = NodeManager::currentNM()->mkConst(true); return returnRewrite(node, ret, "ctn-rhs-emptystr"); } + else if (t.size() == 1) + { + // The following rewrites are specific to a single character second + // argument of contains, where we can reason that this character is + // not split over multiple components in the first argument. + if (node[0].getKind() == STRING_CONCAT) + { + std::vector<Node> nc1; + getConcat(node[0], nc1); + NodeBuilder<> nb(OR); + for (const Node& ncc : nc1) + { + nb << nm->mkNode(STRING_STRCTN, ncc, node[1]); + } + Node ret = nb.constructNode(); + // str.contains( x ++ y, "A" ) ---> + // str.contains( x, "A" ) OR str.contains( y, "A" ) + return returnRewrite(node, ret, "ctn-concat-char"); + } + else if (node[0].getKind() == STRING_STRREPL) + { + Node rplDomain = nm->mkNode(STRING_STRCTN, node[0][1], node[1]); + rplDomain = Rewriter::rewrite(rplDomain); + if (rplDomain.isConst() && !rplDomain.getConst<bool>()) + { + Node d1 = nm->mkNode(STRING_STRCTN, node[0][0], node[1]); + Node d2 = + nm->mkNode(AND, + nm->mkNode(STRING_STRCTN, node[0][0], node[0][1]), + nm->mkNode(STRING_STRCTN, node[0][2], node[1])); + Node ret = nm->mkNode(OR, d1, d2); + // If str.contains( y, "A" ) ---> false, then: + // str.contains( str.replace( x, y, z ), "A" ) ---> + // str.contains( x, "A" ) OR + // ( str.contains( x, y ) AND str.contains( z, "A" ) ) + return returnRewrite(node, ret, "ctn-repl-char"); + } + } + } } std::vector<Node> nc1; getConcat(node[0], nc1); |