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;
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 ){
}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();
}
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;
//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;
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;
}
}
}
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);
+ }
}
}
}
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{
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;
//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 */
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
projects / cvc5.git / commitdiff