Trace("sygus-unif") << "Strategy for candidate " << c << " is : " << std::endl;
std::map<Node, std::map<NodeRole, bool> > visited;
std::map<Node, std::map<unsigned, bool> > 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<const Node, std::map<unsigned, bool> >& nce : needs_cons)
{
NodeRole nrole,
std::map<Node, std::map<NodeRole, bool> >& visited,
std::map<Node, std::map<unsigned, bool> >& 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() ){
Assert(itsn != tinfo.d_snodes.end());
StrategyNode& snode = itsn->second;
- if (!snode.d_strats.empty())
+ if (snode.d_strats.empty())
{
- std::map<unsigned, bool> needs_cons_curr;
- // various strategies
- for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++)
+ return;
+ }
+ std::map<unsigned, bool> 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<unsigned>(cindex)] = false;
+ for (std::pair<Node, NodeRole>& 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<unsigned>(cindex)] = false;
- for (std::pair<Node, NodeRole>& 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<TypeNode, Node>::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<TypeNode, Node>::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<DatatypeType>(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<DatatypeType>(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];
}
}
}
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<bool>())
+ if (gstatus.isNull() || !gstatus.getConst<bool>())
{
- 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<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());
+ std::vector<Node> 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<Node> 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
Node templ = itv->second.d_template;
TNode templ_var = itv->second.d_template_arg;
std::map< Node, bool > cond_vals;
- for( unsigned j=0; j<itx->second.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;
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() ){
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<Node, bool>::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<Node, EnumInfo>::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; i<results.size(); i++ ){
- Assert( results[i].isConst() );
- Assert( itxo->second[i].isConst() );
- /*
- unsigned vlen = results[i].getConst<String>().size();
- unsigned xlen = itxo->second[i].getConst<String>().size();
- Trace("sygus-pbe-cterm-debug") << " " << results[i] << " <> " << itxo->second[i];
- int index = vlen>xlen ? 1 : ( vlen<xlen ? -1 : 0 );
- Trace("sygus-pbe-cterm-debug") << "..." << index << std::endl;
- cmp_indices[index].push_back( i );
- */
- Trace("sygus-pbe-cterm-debug") << " " << results[i] << " <> " << 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<Node>& results,
+ EnumInfo& ei,
+ std::vector<Node>& 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<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 str.contains." << std::endl;
+ std::vector<unsigned> 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;
}
* (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<Node>& results);
// for template
Node d_template;
Node d_template_arg;
-
+
Node d_active_guard;
- std::vector< Node > d_enum_slave;
+ std::vector<Node> d_enum_slave;
/** values we have enumerated */
- std::vector< Node > d_enum_vals;
+ std::vector<Node> 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<std::vector<Node> > d_enum_vals_res;
+ std::vector<Node> d_enum_subsume;
+ std::map<Node, unsigned> 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;
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<Node, bool> d_use_str_contains_eexc;
//------------------------------ strategy registration
/** collect enumerator types
* 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,
NodeRole nrole,
std::map<Node, std::map<NodeRole, bool> >& visited,
std::map<Node, std::map<unsigned, bool> >& needs_cons,
- int ind);
+ int ind,
+ bool isCond);
//------------------------------ end strategy registration
//------------------------------ constructing solutions
projects / cvc5.git / commitdiff