for( unsigned i=0; i<vars.size(); i++ ){
Node n = vars[i];
Trace("strings-subs") << " get subs for " << n << "..." << std::endl;
- if( effort>=3 ){
- //model values
- Node mv = d_valuation.getModel()->getRepresentative( n );
- Trace("strings-subs") << " model val : " << mv << std::endl;
- subs.push_back( mv );
- }else{
- Node nr = getRepresentative( n );
- std::map< Node, Node >::iterator itc = d_eqc_to_const.find( nr );
- if( itc!=d_eqc_to_const.end() ){
- //constant equivalence classes
- Trace("strings-subs") << " constant eqc : " << d_eqc_to_const_exp[nr] << " " << d_eqc_to_const_base[nr] << " " << nr << std::endl;
- subs.push_back( itc->second );
- if( !d_eqc_to_const_exp[nr].isNull() ){
- exp[n].push_back( d_eqc_to_const_exp[nr] );
- }
- if( !d_eqc_to_const_base[nr].isNull() ){
- addToExplanation( n, d_eqc_to_const_base[nr], exp[n] );
- }
- }else if( effort>=1 && effort<3 && n.getType().isString() ){
- //normal forms
- NormalForm& nfnr = getNormalForm(nr);
- Node ns = getNormalString(nfnr.d_base, exp[n]);
- subs.push_back( ns );
- Trace("strings-subs") << " normal eqc : " << ns << " " << nfnr.d_base
- << " " << nr << std::endl;
- if (!nfnr.d_base.isNull())
- {
- addToExplanation(n, nfnr.d_base, exp[n]);
- }
- }else{
- //representative?
- //Trace("strings-subs") << " representative : " << nr << std::endl;
- //addToExplanation( n, nr, exp[n] );
- //subs.push_back( nr );
- subs.push_back( n );
- }
- }
+ Node s = getCurrentSubstitutionFor(effort, n, exp[n]);
+ subs.push_back(s);
}
return true;
}
+Node TheoryStrings::getCurrentSubstitutionFor(int effort,
+ Node n,
+ std::vector<Node>& exp)
+{
+ if (effort >= 3)
+ {
+ // model values
+ Node mv = d_valuation.getModel()->getRepresentative(n);
+ Trace("strings-subs") << " model val : " << mv << std::endl;
+ return mv;
+ }
+ Node nr = getRepresentative(n);
+ std::map<Node, Node>::iterator itc = d_eqc_to_const.find(nr);
+ if (itc != d_eqc_to_const.end())
+ {
+ // constant equivalence classes
+ Trace("strings-subs") << " constant eqc : " << d_eqc_to_const_exp[nr]
+ << " " << d_eqc_to_const_base[nr] << " " << nr
+ << std::endl;
+ if (!d_eqc_to_const_exp[nr].isNull())
+ {
+ exp.push_back(d_eqc_to_const_exp[nr]);
+ }
+ if (!d_eqc_to_const_base[nr].isNull())
+ {
+ addToExplanation(n, d_eqc_to_const_base[nr], exp);
+ }
+ return itc->second;
+ }
+ else if (effort >= 1 && n.getType().isString())
+ {
+ Assert(effort < 3);
+ // normal forms
+ NormalForm& nfnr = getNormalForm(nr);
+ Node ns = getNormalString(nfnr.d_base, exp);
+ Trace("strings-subs") << " normal eqc : " << ns << " " << nfnr.d_base
+ << " " << nr << std::endl;
+ if (!nfnr.d_base.isNull())
+ {
+ addToExplanation(n, nfnr.d_base, exp);
+ }
+ return ns;
+ }
+ return n;
+}
+
bool TheoryStrings::doReduction(int effort, Node n, bool& isCd)
{
Assert(d_extf_info_tmp.find(n) != d_extf_info_tmp.end());
getExtTheory()->markCongruent( nc, n );
}
//this node is congruent to another one, we can ignore it
- Trace("strings-process-debug") << " congruent term : " << n << std::endl;
+ Trace("strings-process-debug")
+ << " congruent term : " << n << " (via " << nc << ")"
+ << std::endl;
d_congruent.insert( n );
congruent[k]++;
}else if( k==kind::STRING_CONCAT && c.size()==1 ){
void TheoryStrings::checkExtfEval( int effort ) {
Trace("strings-extf-list") << "Active extended functions, effort=" << effort << " : " << std::endl;
d_extf_info_tmp.clear();
+ NodeManager* nm = NodeManager::currentNM();
bool has_nreduce = false;
std::vector< Node > terms = getExtTheory()->getActive();
- std::vector< Node > sterms;
- std::vector< std::vector< Node > > exp;
- getExtTheory()->getSubstitutedTerms( effort, terms, sterms, exp );
- for( unsigned i=0; i<terms.size(); i++ ){
- Node n = terms[i];
- Node sn = sterms[i];
- //setup information about extf
+ for (const Node& n : terms)
+ {
+ // Setup information about n, including if it is equal to a constant.
ExtfInfoTmp& einfo = d_extf_info_tmp[n];
Node r = getRepresentative(n);
std::map<Node, Node>::iterator itcit = d_eqc_to_const.find(r);
{
einfo.d_const = itcit->second;
}
- Trace("strings-extf-debug") << "Check extf " << n << " == " << sn
- << ", constant = " << einfo.d_const
- << ", effort=" << effort << "..." << std::endl;
- //do the inference
+ // Get the current values of the children of n.
+ // Notice that we look up the value of the direct children of n, and not
+ // their free variables. In other words, given a term:
+ // t = (str.replace "B" (str.replace x "A" "B") "C")
+ // we may build the explanation that:
+ // ((str.replace x "A" "B") = "B") => t = (str.replace "B" "B" "C")
+ // instead of basing this on the free variable x:
+ // (x = "A") => t = (str.replace "B" (str.replace "A" "A" "B") "C")
+ // Although both allow us to infer t = "C", it is important to use the
+ // first kind of inference since it ensures that its subterms have the
+ // expected values. Otherwise, we may in rare cases fail to realize that
+ // the subterm (str.replace x "A" "B") does not currently have the correct
+ // value, say in this example that (str.replace x "A" "B") != "B".
+ std::vector<Node> exp;
+ std::vector<Node> schildren;
+ bool schanged = false;
+ for (const Node& nc : n)
+ {
+ Node sc = getCurrentSubstitutionFor(effort, nc, exp);
+ schildren.push_back(sc);
+ schanged = schanged || sc != nc;
+ }
+ // If there is information involving the children, attempt to do an
+ // inference and/or mark n as reduced.
Node to_reduce;
- if( n!=sn ){
- einfo.d_exp.insert(einfo.d_exp.end(), exp[i].begin(), exp[i].end());
+ if (schanged)
+ {
+ Node sn = nm->mkNode(n.getKind(), schildren);
+ Trace("strings-extf-debug")
+ << "Check extf " << n << " == " << sn
+ << ", constant = " << einfo.d_const << ", effort=" << effort << "..."
+ << std::endl;
+ einfo.d_exp.insert(einfo.d_exp.end(), exp.begin(), exp.end());
// inference is rewriting the substituted node
Node nrc = Rewriter::rewrite( sn );
//if rewrites to a constant, then do the inference and mark as reduced
}
to_reduce = nrc;
}
- }else{
- to_reduce = sterms[i];
+ }
+ else
+ {
+ to_reduce = n;
}
//if not reduced
if( !to_reduce.isNull() ){
projects / cvc5.git / commitdiff