From: Andrew Reynolds Date: Mon, 29 Jan 2018 22:59:13 +0000 (-0600) Subject: Generalize explanations for PBE sygus strings based on negative contains when multipl... X-Git-Tag: cvc5-1.0.0~5342 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a695c35ebb077246cc7278fc3ad99a2ac536ef0d;p=cvc5.git Generalize explanations for PBE sygus strings based on negative contains when multiple strategies are present (#1546) --- diff --git a/src/theory/quantifiers/ce_guided_pbe.cpp b/src/theory/quantifiers/ce_guided_pbe.cpp index bee19daeb..7f339be5f 100644 --- a/src/theory/quantifiers/ce_guided_pbe.cpp +++ b/src/theory/quantifiers/ce_guided_pbe.cpp @@ -925,8 +925,13 @@ void CegConjecturePbe::staticLearnRedundantOps( Node c, std::vector< Node >& lem Trace("sygus-unif") << "Strategy for candidate " << c << " is : " << std::endl; std::map > visited; std::map > needs_cons; - staticLearnRedundantOps( - c, d_cinfo[c].getRootEnumerator(), role_equal, visited, needs_cons, 0); + staticLearnRedundantOps(c, + d_cinfo[c].getRootEnumerator(), + role_equal, + visited, + needs_cons, + 0, + false); // now, check the needs_cons map for (std::pair >& nce : needs_cons) { @@ -957,19 +962,30 @@ void CegConjecturePbe::staticLearnRedundantOps( NodeRole nrole, std::map >& visited, std::map >& needs_cons, - int ind) + int ind, + bool isCond) { std::map< Node, EnumInfo >::iterator itn = d_einfo.find( e ); Assert( itn!=d_einfo.end() ); - if (visited[e].find(nrole) == visited[e].end()) + + if (visited[e].find(nrole) == visited[e].end() + || (isCond && !itn->second.isConditional())) { visited[e][nrole] = true; - + // if conditional + if (isCond) + { + itn->second.setConditional(); + } indent("sygus-unif", ind); Trace("sygus-unif") << e << " :: node role : " << nrole; Trace("sygus-unif") << ", type : " << ((DatatypeType)e.getType().toType()).getDatatype().getName(); + if (isCond) + { + Trace("sygus-unif") << ", conditional"; + } Trace("sygus-unif") << ", enum role : " << itn->second.getRole(); if( itn->second.isTemplated() ){ @@ -991,57 +1007,65 @@ void CegConjecturePbe::staticLearnRedundantOps( Assert(itsn != tinfo.d_snodes.end()); StrategyNode& snode = itsn->second; - if (!snode.d_strats.empty()) + if (snode.d_strats.empty()) { - std::map needs_cons_curr; - // various strategies - for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++) + return; + } + std::map needs_cons_curr; + // various strategies + for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++) + { + EnumTypeInfoStrat* etis = snode.d_strats[j]; + StrategyType strat = etis->d_this; + bool newIsCond = isCond || strat == strat_ITE; + indent("sygus-unif", ind + 1); + Trace("sygus-unif") << "Strategy : " << strat + << ", from cons : " << etis->d_cons << std::endl; + int cindex = Datatype::indexOf(etis->d_cons.toExpr()); + Assert(cindex != -1); + needs_cons_curr[static_cast(cindex)] = false; + for (std::pair& cec : etis->d_cenum) { - EnumTypeInfoStrat* etis = snode.d_strats[j]; - StrategyType strat = etis->d_this; - indent("sygus-unif", ind+1); - Trace("sygus-unif") << "Strategy : " << strat - << ", from cons : " << etis->d_cons << std::endl; - int cindex = Datatype::indexOf(etis->d_cons.toExpr()); - Assert(cindex != -1); - needs_cons_curr[static_cast(cindex)] = false; - for (std::pair& cec : etis->d_cenum) - { - // recurse - staticLearnRedundantOps( - c, cec.first, cec.second, visited, needs_cons, ind + 2); - } + // recurse + staticLearnRedundantOps(c, + cec.first, + cec.second, + visited, + needs_cons, + ind + 2, + newIsCond); } - // get the master enumerator for the type of this enumerator - std::map::iterator itse = - d_cinfo[c].d_search_enum.find(etn); - if (itse != d_cinfo[c].d_search_enum.end()) + } + // get the master enumerator for the type of this enumerator + std::map::iterator itse = + d_cinfo[c].d_search_enum.find(etn); + if (itse == d_cinfo[c].d_search_enum.end()) + { + return; + } + Node em = itse->second; + Assert(!em.isNull()); + // get the current datatype + const Datatype& dt = + static_cast(etn.toType()).getDatatype(); + // all constructors that are not a part of a strategy are needed + for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++) + { + if (needs_cons_curr.find(j) == needs_cons_curr.end()) { - Node em = itse->second; - Assert(!em.isNull()); - // get the current datatype - const Datatype& dt = - static_cast(etn.toType()).getDatatype(); - // all constructors that are not a part of a strategy are needed - for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++) - { - if (needs_cons_curr.find(j) == needs_cons_curr.end()) - { - needs_cons_curr[j] = true; - } - } - // update the constructors that the master enumerator needs - if (needs_cons.find(em) == needs_cons.end()) - { - needs_cons[em] = needs_cons_curr; - } - else - { - for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++) - { - needs_cons[em][j] = needs_cons[em][j] || needs_cons_curr[j]; - } - } + needs_cons_curr[j] = true; + } + } + // update the constructors that the master enumerator needs + if (needs_cons.find(em) == needs_cons.end()) + { + needs_cons[em] = needs_cons_curr; + } + else + { + for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++) + { + needs_cons[em][j] = needs_cons[em][j] || needs_cons_curr[j]; } } } @@ -1116,21 +1140,53 @@ void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >& std::map< Node, EnumInfo >::iterator it = d_einfo.find( x ); Assert( it != d_einfo.end() ); Node gstatus = d_qe->getValuation().getSatValue(it->second.d_active_guard); - if (!gstatus.isNull() && gstatus.getConst()) + if (gstatus.isNull() || !gstatus.getConst()) { - Assert( std::find( it->second.d_enum_vals.begin(), it->second.d_enum_vals.end(), v )==it->second.d_enum_vals.end() ); - Node c = it->second.d_parent_candidate; - Node exp_exc; - if( d_examples_out_invalid.find( c )==d_examples_out_invalid.end() ){ - std::map< Node, CandidateInfo >::iterator itc = d_cinfo.find( c ); - Assert( itc != d_cinfo.end() ); - TypeNode xtn = x.getType(); - Node bv = d_tds->sygusToBuiltin( v, xtn ); - std::map< Node, std::vector< std::vector< Node > > >::iterator itx = d_examples.find( c ); - std::map< Node, std::vector< Node > >::iterator itxo = d_examples_out.find( c ); - Assert( itx!=d_examples.end() ); - Assert( itxo!=d_examples_out.end() ); - Assert( itx->second.size()==itxo->second.size() ); + Trace("sygus-pbe-enum-debug") << " ...guard is inactive." << std::endl; + return; + } + Assert( + std::find(it->second.d_enum_vals.begin(), it->second.d_enum_vals.end(), v) + == it->second.d_enum_vals.end()); + Node c = it->second.d_parent_candidate; + // The explanation for why the current value should be excluded in future + // iterations. + Node exp_exc; + if (d_examples_out_invalid.find(c) == d_examples_out_invalid.end()) + { + std::map::iterator itc = d_cinfo.find(c); + Assert(itc != d_cinfo.end()); + TypeNode xtn = x.getType(); + Node bv = d_tds->sygusToBuiltin(v, xtn); + std::map > >::iterator itx = + d_examples.find(c); + std::map >::iterator itxo = d_examples_out.find(c); + Assert(itx != d_examples.end()); + Assert(itxo != d_examples_out.end()); + Assert(itx->second.size() == itxo->second.size()); + std::vector base_results; + // compte the results + for (unsigned j = 0, size = itx->second.size(); j < size; j++) + { + Node res = d_tds->evaluateBuiltin(xtn, bv, itx->second[j]); + Trace("sygus-pbe-enum-debug") + << "...got res = " << res << " from " << bv << std::endl; + base_results.push_back(res); + } + // is it excluded for domain-specific reason? + std::vector exp_exc_vec; + if (getExplanationForEnumeratorExclude( + c, x, v, base_results, it->second, exp_exc_vec)) + { + Assert(!exp_exc_vec.empty()); + exp_exc = exp_exc_vec.size() == 1 + ? exp_exc_vec[0] + : NodeManager::currentNM()->mkNode(AND, exp_exc_vec); + Trace("sygus-pbe-enum") + << " ...fail : term is excluded (domain-specific)" << std::endl; + } + else + { // notify all slaves Assert( !it->second.d_enum_slave.empty() ); //explanation for why this value should be excluded @@ -1153,9 +1209,9 @@ void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >& Node templ = itv->second.d_template; TNode templ_var = itv->second.d_template_arg; std::map< Node, bool > cond_vals; - for( unsigned j=0; jsecond.size(); j++ ){ - Node res = d_tds->evaluateBuiltin( xtn, bv, itx->second[j] ); - Trace("sygus-pbe-enum-debug") << "...got res = " << res << " from " << bv << std::endl; + for (unsigned j = 0, size = base_results.size(); j < size; j++) + { + Node res = base_results[j]; Assert( res.isConst() ); if( !templ.isNull() ){ TNode tres = res; @@ -1185,7 +1241,9 @@ void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >& bool keep = false; if (itv->second.getRole() == enum_io) { - if( cond_vals.find( d_true )!=cond_vals.end() || cond_vals.empty() ){ // latter is the degenerate case of no examples + // latter is the degenerate case of no examples + if (cond_vals.find(d_true) != cond_vals.end() || cond_vals.empty()) + { //check subsumbed/subsuming std::vector< Node > subsume; if( cond_vals.find( d_false )==cond_vals.end() ){ @@ -1217,113 +1275,141 @@ void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >& Trace("sygus-pbe-enum") << " ...fail : it does not satisfy examples." << std::endl; } }else{ - // is it excluded for domain-specific reason? - std::vector< Node > exp_exc_vec; - if( getExplanationForEnumeratorExclude( c, x, v, results, it->second, exp_exc_vec ) ){ - Assert( !exp_exc_vec.empty() ); - exp_exc = exp_exc_vec.size() == 1 - ? exp_exc_vec[0] - : NodeManager::currentNM()->mkNode(AND, exp_exc_vec); - Trace("sygus-pbe-enum") << " ...fail : term is excluded (domain-specific)" << std::endl; + // must be unique up to examples + Node val = itv->second.d_term_trie.addCond(this, v, results, true); + if (val == v) + { + Trace("sygus-pbe-enum") << " ...success! add to PBE pool : " + << d_tds->sygusToBuiltin(v) << std::endl; + keep = true; }else{ - //if( cond_vals.size()!=2 ){ - // // must discriminate - // Trace("sygus-pbe-enum") << " ...fail : conditional is constant." << std::endl; - // keep = false; - //} - // must be unique up to examples - Node val = itv->second.d_term_trie.addCond( this, v, results, true ); - if( val==v ){ - Trace("sygus-pbe-enum") << " ...success! add to PBE pool : " << d_tds->sygusToBuiltin( v ) << std::endl; - keep = true; - }else{ - Trace("sygus-pbe-enum") << " ...fail : term is not unique" << std::endl; - } - itc->second.d_cond_count++; + Trace("sygus-pbe-enum") + << " ...fail : term is not unique" << std::endl; } + itc->second.d_cond_count++; } if( keep ){ // notify the parent to retry the build of PBE itc->second.d_check_sol = true; itv->second.addEnumValue( this, v, results ); - /* - if( Trace.isOn("sygus-pbe-enum") ){ - if( itv->second.getRole()==enum_io ){ - if( !prevIsCover && itv->second.isFeasible() ){ - Trace("sygus-pbe-enum") << "...PBE : success : Evaluation of " - << xs << " now covers all examples." << std::endl; - } - } - } - */ } } - }else{ - Trace("sygus-pbe-enum-debug") << " ...examples do not have output." << std::endl; - } - //exclude this value on subsequent iterations - Node g = it->second.d_active_guard; - if( exp_exc.isNull() ){ - // if we did not already explain why this should be excluded, use default - exp_exc = d_tds->getExplain()->getExplanationForConstantEquality(x, v); - } - Node exlem = - NodeManager::currentNM()->mkNode(OR, g.negate(), exp_exc.negate()); - Trace("sygus-pbe-enum-lemma") << "CegConjecturePbe : enumeration exclude lemma : " << exlem << std::endl; - lems.push_back( exlem ); + } }else{ - Trace("sygus-pbe-enum-debug") << " ...guard is inactive." << std::endl; + Trace("sygus-pbe-enum-debug") + << " ...examples do not have output." << std::endl; + } + // exclude this value on subsequent iterations + Node g = it->second.d_active_guard; + if (exp_exc.isNull()) + { + // if we did not already explain why this should be excluded, use default + exp_exc = d_tds->getExplain()->getExplanationForConstantEquality(x, v); } + Node exlem = + NodeManager::currentNM()->mkNode(OR, g.negate(), exp_exc.negate()); + Trace("sygus-pbe-enum-lemma") + << "CegConjecturePbe : enumeration exclude lemma : " << exlem + << std::endl; + lems.push_back(exlem); } -bool CegConjecturePbe::getExplanationForEnumeratorExclude( Node c, Node x, Node v, std::vector< Node >& results, EnumInfo& ei, std::vector< Node >& exp ) { - if( ei.d_enum_slave.size()==1 ){ - // this check whether the example evaluates to something that is larger than the output - // if so, then this term is never useful when using a concatenation strategy - if (ei.getRole() == enum_concat_term) +bool CegConjecturePbe::useStrContainsEnumeratorExclude(Node x, EnumInfo& ei) +{ + TypeNode xbt = d_tds->sygusToBuiltinType(x.getType()); + if (xbt.isString()) + { + std::map::iterator itx = d_use_str_contains_eexc.find(x); + if (itx != d_use_str_contains_eexc.end()) { - if( Trace.isOn("sygus-pbe-cterm-debug") ){ - Trace("sygus-pbe-enum") << std::endl; + return itx->second; + } + Trace("sygus-pbe-enum-debug") + << "Is " << x << " is str.contains exclusion?" << std::endl; + d_use_str_contains_eexc[x] = true; + for (const Node& sn : ei.d_enum_slave) + { + std::map::iterator itv = d_einfo.find(sn); + EnumRole er = itv->second.getRole(); + if (er != enum_io && er != enum_concat_term) + { + Trace("sygus-pbe-enum-debug") << " incompatible slave : " << sn + << ", role = " << er << std::endl; + d_use_str_contains_eexc[x] = false; + return false; } + if (itv->second.isConditional()) + { + Trace("sygus-pbe-enum-debug") + << " conditional slave : " << sn << std::endl; + d_use_str_contains_eexc[x] = false; + return false; + } + } + Trace("sygus-pbe-enum-debug") + << "...can use str.contains exclusion." << std::endl; + return d_use_str_contains_eexc[x]; + } + return false; +} - // check if all examples had longer length that the output - std::map< Node, std::vector< Node > >::iterator itxo = d_examples_out.find( c ); - Assert( itxo!=d_examples_out.end() ); - Assert( itxo->second.size()==results.size() ); - Trace("sygus-pbe-cterm-debug") << "Check enumerator exclusion for " << x << " -> " << d_tds->sygusToBuiltin( v ) << " based on containment." << std::endl; - std::vector< unsigned > cmp_indices; - for( unsigned i=0; isecond[i].isConst() ); - /* - unsigned vlen = results[i].getConst().size(); - unsigned xlen = itxo->second[i].getConst().size(); - Trace("sygus-pbe-cterm-debug") << " " << results[i] << " <> " << itxo->second[i]; - int index = vlen>xlen ? 1 : ( vlen " << itxo->second[i]; - Node cont = NodeManager::currentNM()->mkNode( - STRING_STRCTN, itxo->second[i], results[i]); - Node contr = Rewriter::rewrite( cont ); - if( contr==d_false ){ - cmp_indices.push_back( i ); - Trace("sygus-pbe-cterm-debug") << "...not contained." << std::endl; - }else{ - Trace("sygus-pbe-cterm-debug") << "...contained." << std::endl; - } +bool CegConjecturePbe::getExplanationForEnumeratorExclude( + Node c, + Node x, + Node v, + std::vector& results, + EnumInfo& ei, + std::vector& exp) +{ + if (useStrContainsEnumeratorExclude(x, ei)) + { + NodeManager* nm = NodeManager::currentNM(); + // This check whether the example evaluates to something that is larger than + // the output for some input/output pair. If so, then this term is never + // useful. We generalize its explanation below. + + if (Trace.isOn("sygus-pbe-cterm-debug")) + { + Trace("sygus-pbe-enum") << std::endl; + } + // check if all examples had longer length that the output + std::map >::iterator itxo = d_examples_out.find(c); + Assert(itxo != d_examples_out.end()); + Assert(itxo->second.size() == results.size()); + Trace("sygus-pbe-cterm-debug") + << "Check enumerator exclusion for " << x << " -> " + << d_tds->sygusToBuiltin(v) << " based on str.contains." << std::endl; + std::vector cmp_indices; + for (unsigned i = 0, size = results.size(); i < size; i++) + { + Assert(results[i].isConst()); + Assert(itxo->second[i].isConst()); + Trace("sygus-pbe-cterm-debug") + << " " << results[i] << " <> " << itxo->second[i]; + Node cont = nm->mkNode(STRING_STRCTN, itxo->second[i], results[i]); + Node contr = Rewriter::rewrite(cont); + if (contr == d_false) + { + cmp_indices.push_back(i); + Trace("sygus-pbe-cterm-debug") << "...not contained." << std::endl; } - // TODO : stronger requirement if we incorporate ITE + CONCAT mixed strategy : must be longer than *all* examples - if( !cmp_indices.empty() ){ - //set up the inclusion set - NegContainsSygusInvarianceTest ncset; - ncset.init(d_parent, x, itxo->second, cmp_indices); - d_tds->getExplain()->getExplanationFor(x, v, exp, ncset); - Trace("sygus-pbe-cterm") << "PBE-cterm : enumerator exclude " << d_tds->sygusToBuiltin( v ) << " due to negative containment." << std::endl; - return true; + else + { + Trace("sygus-pbe-cterm-debug") << "...contained." << std::endl; } } + if (!cmp_indices.empty()) + { + // we check invariance with respect to a negative contains test + NegContainsSygusInvarianceTest ncset; + ncset.init(d_parent, x, itxo->second, cmp_indices); + // construct the generalized explanation + d_tds->getExplain()->getExplanationFor(x, v, exp, ncset); + Trace("sygus-pbe-cterm") + << "PBE-cterm : enumerator exclude " << d_tds->sygusToBuiltin(v) + << " due to negative containment." << std::endl; + return true; + } } return false; } diff --git a/src/theory/quantifiers/ce_guided_pbe.h b/src/theory/quantifiers/ce_guided_pbe.h index e8bccaac5..ce1f2bf5e 100644 --- a/src/theory/quantifiers/ce_guided_pbe.h +++ b/src/theory/quantifiers/ce_guided_pbe.h @@ -386,15 +386,26 @@ class CegConjecturePbe { * (possibly multiple) slave enumerators, stored in d_enum_slave, */ class EnumInfo { - public: - EnumInfo() : d_role( enum_io ){} + public: + EnumInfo() : d_role(enum_io), d_is_conditional(false) {} /** initialize this class * c is the parent function-to-synthesize * role is the "role" the enumerator plays in the high-level strategy, * which is one of enum_* above. */ void initialize(Node c, EnumRole role); + /** is this enumerator associated with a template? */ bool isTemplated() { return !d_template.isNull(); } + /** set conditional + * + * This flag is set to true if this enumerator may not apply to all + * input/output examples. For example, if this enumerator is used + * as an output value beneath a conditional in an instance of strat_ITE, + * then this enumerator is conditional. + */ + void setConditional() { d_is_conditional = true; } + /** is conditional */ + bool isConditional() { return d_is_conditional; } void addEnumValue(CegConjecturePbe* pbe, Node v, std::vector& results); @@ -406,26 +417,30 @@ class CegConjecturePbe { // for template Node d_template; Node d_template_arg; - + Node d_active_guard; - std::vector< Node > d_enum_slave; + std::vector d_enum_slave; /** values we have enumerated */ - std::vector< Node > d_enum_vals; + std::vector d_enum_vals; /** - * This either stores the values of f( I ) for inputs - * or the value of f( I ) = O if d_role==enum_io - */ - std::vector< std::vector< Node > > d_enum_vals_res; - std::vector< Node > d_enum_subsume; - std::map< Node, unsigned > d_enum_val_to_index; + * This either stores the values of f( I ) for inputs + * or the value of f( I ) = O if d_role==enum_io + */ + std::vector > d_enum_vals_res; + std::vector d_enum_subsume; + std::map d_enum_val_to_index; SubsumeTrie d_term_trie; private: - /** whether an enumerated value for this conjecture has solved the entire - * conjecture */ + /** + * Whether an enumerated value for this conjecture has solved the entire + * conjecture. + */ Node d_enum_solved; /** the role of this enumerator (one of enum_* above). */ EnumRole d_role; + /** is this enumerator conditional */ + bool d_is_conditional; }; /** maps enumerators to the information above */ std::map< Node, EnumInfo > d_einfo; @@ -524,9 +539,42 @@ class CegConjecturePbe { std::map< Node, CandidateInfo > d_cinfo; //------------------------------ representation of an enumeration strategy - /** add enumerated value */ + /** add enumerated value + * + * We have enumerated the value v for x. This function adds x->v to the + * relevant data structures that are used for strategy-specific construction + * of solutions when necessary, and returns a set of lemmas, which are added + * to the input argument lems. These lemmas are used to rule out models where + * x = v, to force that a new value is enumerated for x. + */ void addEnumeratedValue( Node x, Node v, std::vector< Node >& lems ); + /** domain-specific enumerator exclusion techniques + * + * Returns true if the value v for x can be excluded based on a + * domain-specific exclusion technique like the ones below. + * + * c : the candidate variable that x is enumerating for, + * results : the values of v under the input examples of c, + * ei : the enumerator information for x, + * exp : if this function returns true, then exp contains a (possibly + * generalize) explanation for why v can be excluded. + */ bool getExplanationForEnumeratorExclude( Node c, Node x, Node v, std::vector< Node >& results, EnumInfo& ei, std::vector< Node >& exp ); + /** returns true if we can exlude values of x based on negative str.contains + * + * Values v for x may be excluded if we realize that the value of v under the + * substitution for some input example will never be contained in some output + * example. For details on this technique, see NegContainsSygusInvarianceTest + * in sygus_invariance.h. + * + * This function depends on whether x is being used to enumerate values + * for any node that is conditional in the strategy graph. For example, + * nodes that are children of ITE strategy nodes are conditional. If any node + * is conditional, then this function returns false. + */ + bool useStrContainsEnumeratorExclude(Node x, EnumInfo& ei); + /** cache for the above function */ + std::map d_use_str_contains_eexc; //------------------------------ strategy registration /** collect enumerator types @@ -567,6 +615,9 @@ class CegConjecturePbe { * to a map from the constructors that it needs. * * ind is the depth in the strategy graph we are at (for debugging). + * + * isCond is whether the current enumerator is conditional (beneath a + * conditional of an strat_ITE strategy). */ void staticLearnRedundantOps( Node c, @@ -574,7 +625,8 @@ class CegConjecturePbe { NodeRole nrole, std::map >& visited, std::map >& needs_cons, - int ind); + int ind, + bool isCond); //------------------------------ end strategy registration //------------------------------ constructing solutions diff --git a/src/theory/quantifiers/sygus_invariance.cpp b/src/theory/quantifiers/sygus_invariance.cpp index 6813f4320..1fd6bc7cb 100644 --- a/src/theory/quantifiers/sygus_invariance.cpp +++ b/src/theory/quantifiers/sygus_invariance.cpp @@ -191,6 +191,7 @@ bool NegContainsSygusInvarianceTest::invariant(TermDbSygus* tds, Node out = d_exo[ii]; Node cont = NodeManager::currentNM()->mkNode(kind::STRING_STRCTN, out, nbvre); + Trace("sygus-pbe-cterm-debug") << "Check: " << cont << std::endl; Node contr = Rewriter::rewrite(cont); if (contr == tds->d_false) { @@ -216,6 +217,8 @@ bool NegContainsSygusInvarianceTest::invariant(TermDbSygus* tds, } return true; } + Trace("sygus-pbe-cterm-debug2") + << "...check failed, rewrites to : " << contr << std::endl; } } return false;