From 40764e0b2dd2f00889b016f862da9458cc3123ad Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 26 Sep 2018 14:54:05 -0500 Subject: [PATCH] Symmetry breaking for variable agnostic enumerators (#2527) --- src/theory/datatypes/datatypes_sygus.cpp | 438 ++++++++++++++++++----- src/theory/datatypes/datatypes_sygus.h | 98 ++++- 2 files changed, 440 insertions(+), 96 deletions(-) diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 1d1d2c2be..227bd6170 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -299,15 +299,23 @@ void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std: if( min_depth<=max_depth ){ TNode x = getFreeVar( ntn ); std::vector sb_lemmas; + // symmetry breaking lemmas requiring predicate elimination + std::map sb_elim_pred; bool usingSymCons = d_tds->usingSymbolicConsForEnumerator(m); + bool isVarAgnostic = d_tds->isVariableAgnosticEnumerator(m); for (unsigned ds = 0; ds <= max_depth; ds++) { // static conjecture-independent symmetry breaking Trace("sygus-sb-debug") << " simple symmetry breaking...\n"; - Node ipred = getSimpleSymBreakPred(ntn, tindex, ds, usingSymCons); + Node ipred = getSimpleSymBreakPred( + m, ntn, tindex, ds, usingSymCons, isVarAgnostic); if (!ipred.isNull()) { sb_lemmas.push_back(ipred); + if (ds == 0 && isVarAgnostic) + { + sb_elim_pred[ipred] = true; + } } // static conjecture-dependent symmetry breaking Trace("sygus-sb-debug") @@ -332,6 +340,15 @@ void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std: for (const Node& slem : sb_lemmas) { Node sslem = slem.substitute(x, n, cache); + // if we require predicate elimination + if (sb_elim_pred.find(slem) != sb_elim_pred.end()) + { + Trace("sygus-sb-tp") << "Eliminate traversal predicates: start " + << sslem << std::endl; + sslem = eliminateTraversalPredicates(sslem); + Trace("sygus-sb-tp") << "Eliminate traversal predicates: finish " + << sslem << std::endl; + } if (!rlv.isNull()) { sslem = nm->mkNode(OR, rlv, sslem); @@ -407,14 +424,123 @@ Node SygusSymBreakNew::getRelevancyCondition( Node n ) { } } -Node SygusSymBreakNew::getSimpleSymBreakPred(TypeNode tn, +Node SygusSymBreakNew::getTraversalPredicate(TypeNode tn, Node n, bool isPre) +{ + unsigned index = isPre ? 0 : 1; + std::map::iterator itt = d_traversal_pred[index][tn].find(n); + if (itt != d_traversal_pred[index][tn].end()) + { + return itt->second; + } + NodeManager* nm = NodeManager::currentNM(); + std::vector types; + types.push_back(tn); + TypeNode ptn = nm->mkPredicateType(types); + Node pred = nm->mkSkolem(isPre ? "pre" : "post", ptn); + d_traversal_pred[index][tn][n] = pred; + return pred; +} + +Node SygusSymBreakNew::eliminateTraversalPredicates(Node n) +{ + NodeManager* nm = NodeManager::currentNM(); + std::unordered_map visited; + std::unordered_map::iterator it; + std::map::iterator ittb; + std::vector visit; + TNode cur; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + it = visited.find(cur); + + if (it == visited.end()) + { + if (cur.getKind() == APPLY_UF) + { + Assert(cur.getType().isBoolean()); + Assert(cur.getNumChildren() == 1 + && (cur[0].isVar() || cur[0].getKind() == APPLY_SELECTOR_TOTAL)); + ittb = d_traversal_bool.find(cur); + Node ret; + if (ittb == d_traversal_bool.end()) + { + std::stringstream ss; + ss << "v_" << cur; + ret = nm->mkSkolem(ss.str(), cur.getType()); + d_traversal_bool[cur] = ret; + } + else + { + ret = ittb->second; + } + visited[cur] = ret; + } + else + { + visited[cur] = Node::null(); + visit.push_back(cur); + for (const Node& cn : cur) + { + visit.push_back(cn); + } + } + } + else if (it->second.isNull()) + { + Node ret = cur; + bool childChanged = false; + std::vector children; + if (cur.getMetaKind() == metakind::PARAMETERIZED) + { + children.push_back(cur.getOperator()); + } + for (const Node& cn : cur) + { + it = visited.find(cn); + Assert(it != visited.end()); + Assert(!it->second.isNull()); + childChanged = childChanged || cn != it->second; + children.push_back(it->second); + } + if (childChanged) + { + ret = nm->mkNode(cur.getKind(), children); + } + visited[cur] = ret; + } + } while (!visit.empty()); + Assert(visited.find(n) != visited.end()); + Assert(!visited.find(n)->second.isNull()); + return visited[n]; +} + +Node SygusSymBreakNew::getSimpleSymBreakPred(Node e, + TypeNode tn, int tindex, unsigned depth, - bool usingSymCons) + bool usingSymCons, + bool isVarAgnostic) { + // Compute the tuple of expressions we hash the predicate for. + + // The hash value in d_simple_sb_pred for the given options + unsigned optHashVal = usingSymCons ? 1 : 0; + if (isVarAgnostic && depth == 0) + { + // variable agnostic symmetry breaking only applies at depth 0 + optHashVal = optHashVal + 2; + } + else + { + // enumerator is only specific to variable agnostic symmetry breaking + e = Node::null(); + } std::map::iterator it = - d_simple_sb_pred[tn][tindex][usingSymCons].find(depth); - if (it != d_simple_sb_pred[tn][tindex][usingSymCons].end()) + d_simple_sb_pred[e][tn][tindex][optHashVal].find(depth); + if (it != d_simple_sb_pred[e][tn][tindex][optHashVal].end()) { return it->second; } @@ -435,7 +561,7 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(TypeNode tn, Node sop = Node::fromExpr(dt[tindex].getSygusOp()); if (sop.getAttribute(SygusAnyConstAttribute()) || depth > 2) { - d_simple_sb_pred[tn][tindex][usingSymCons][depth] = Node::null(); + d_simple_sb_pred[e][tn][tindex][optHashVal][depth] = Node::null(); return Node::null(); } // conjunctive conclusion of lemma @@ -493,6 +619,82 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(TypeNode tn, sbp_conj.push_back(DatatypesRewriter::mkTester(children[j], i, cdt)); } } + + if (isVarAgnostic && depth == 0) + { + // Enforce symmetry breaking lemma template for each x_i: + // template z. + // is-x_i( z ) => pre_{x_{i-1}}( z ) + // for args a = 1...n + // // pre-definition + // pre_{x_i}( z.a ) = a=0 ? pre_{x_i}( z ) : post_{x_i}( z.{a-1} ) + // post_{x_i}( z ) = post_{x_i}( z.n ) OR is-x_i( z ) + + // Notice that we are constructing a symmetry breaking template + // under the condition that is-C( z ) holds in this method, where C + // is the tindex^{th} constructor of dt. Thus, is-x_i( z ) is either + // true or false below. + + Node svl = Node::fromExpr(dt.getSygusVarList()); + // for each variable + Assert(!e.isNull()); + TypeNode etn = e.getType(); + // for each variable in the sygus type + for (const Node& var : svl) + { + unsigned sc = d_tds->getSubclassForVar(etn, var); + if (d_tds->getNumSubclassVars(etn, sc) == 1) + { + // unique variable in singleton subclass, skip + continue; + } + // Compute the "predecessor" variable in the subclass of var. + Node predVar; + unsigned scindex = 0; + if (d_tds->getIndexInSubclassForVar(etn, var, scindex)) + { + if (scindex > 0) + { + predVar = d_tds->getVarSubclassIndex(etn, sc, scindex - 1); + } + } + Node preParentOp = getTraversalPredicate(tn, var, true); + Node preParent = nm->mkNode(APPLY_UF, preParentOp, n); + Node prev = preParent; + // for each child + for (const Node& child : children) + { + TypeNode ctn = child.getType(); + // my pre is equal to the previous + Node preCurrOp = getTraversalPredicate(ctn, var, true); + Node preCurr = nm->mkNode(APPLY_UF, preCurrOp, child); + // definition of pre, for each argument + sbp_conj.push_back(preCurr.eqNode(prev)); + Node postCurrOp = getTraversalPredicate(ctn, var, false); + prev = nm->mkNode(APPLY_UF, postCurrOp, child); + } + Node postParent = getTraversalPredicate(tn, var, false); + Node finish = nm->mkNode(APPLY_UF, postParent, n); + // check if we are constructing the symmetry breaking predicate for the + // variable in question. If so, is-{x_i}( z ) is true. + int varCn = d_tds->getOpConsNum(tn, var); + if (varCn == static_cast(tindex)) + { + // the post value is true + prev = d_true; + // requirement : If I am the variable, I must have seen + // the variable before this one in its type class. + if (!predVar.isNull()) + { + Node preParentPredVarOp = getTraversalPredicate(tn, predVar, true); + Node preParentPredVar = nm->mkNode(APPLY_UF, preParentPredVarOp, n); + sbp_conj.push_back(preParentPredVar); + } + } + // definition of post + sbp_conj.push_back(finish.eqNode(prev)); + } + } // depth 1 symmetry breaking : talks about direct children if (depth == 1) { @@ -721,7 +923,7 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(TypeNode tn, sb_pred = nm->mkNode( kind::OR, DatatypesRewriter::mkTester(n, tindex, dt).negate(), sb_pred); } - d_simple_sb_pred[tn][tindex][usingSymCons][depth] = sb_pred; + d_simple_sb_pred[e][tn][tindex][optHashVal][depth] = sb_pred; return sb_pred; } @@ -1062,70 +1264,115 @@ void SygusSymBreakNew::preRegisterTerm( TNode n, std::vector< Node >& lemmas ) } void SygusSymBreakNew::registerSizeTerm( Node e, std::vector< Node >& lemmas ) { - if( d_register_st.find( e )==d_register_st.end() ){ - if( e.getType().isDatatype() ){ - const Datatype& dt = ((DatatypeType)(e.getType()).toType()).getDatatype(); - if( dt.isSygus() ){ - if (d_tds->isEnumerator(e)) - { - d_register_st[e] = true; - Node ag = d_tds->getActiveGuardForEnumerator(e); - if( !ag.isNull() ){ - d_anchor_to_active_guard[e] = ag; - std::map>::iterator itaas = - d_anchor_to_ag_strategy.find(e); - if (itaas == d_anchor_to_ag_strategy.end()) - { - d_anchor_to_ag_strategy[e].reset( - new DecisionStrategySingleton("sygus_enum_active", - ag, - d_td->getSatContext(), - d_td->getValuation())); - } - d_td->getDecisionManager()->registerStrategy( - DecisionManager::STRAT_DT_SYGUS_ENUM_ACTIVE, - d_anchor_to_ag_strategy[e].get()); - } - Node m; - if( !ag.isNull() ){ - // if it has an active guard (it is an enumerator), use itself as measure term. This will enforce fairness on it independently. - m = e; - }else{ - // otherwise we enforce fairness in a unified way for all - if( d_generic_measure_term.isNull() ){ - // choose e as master for all future terms - d_generic_measure_term = e; - } - m = d_generic_measure_term; - } - Trace("sygus-sb") << "Sygus : register size term : " << e << " with measure " << m << std::endl; - registerMeasureTerm( m ); - d_szinfo[m]->d_anchors.push_back( e ); - d_anchor_to_measure_term[e] = m; - if( options::sygusFair()==SYGUS_FAIR_DT_SIZE ){ - // update constraints on the measure term - if( options::sygusFairMax() ){ - Node ds = NodeManager::currentNM()->mkNode(kind::DT_SIZE, e); - Node slem = NodeManager::currentNM()->mkNode( - kind::LEQ, ds, d_szinfo[m]->getOrMkMeasureValue(lemmas)); - lemmas.push_back(slem); - }else{ - Node mt = d_szinfo[m]->getOrMkActiveMeasureValue(lemmas); - Node new_mt = - d_szinfo[m]->getOrMkActiveMeasureValue(lemmas, true); - Node ds = NodeManager::currentNM()->mkNode(kind::DT_SIZE, e); - lemmas.push_back(mt.eqNode( - NodeManager::currentNM()->mkNode(kind::PLUS, new_mt, ds))); - } - } - }else{ - // not sure if it is a size term or not (may be registered later?) - } - }else{ - d_register_st[e] = false; - } + if (d_register_st.find(e) != d_register_st.end()) + { + // already registered + return; + } + TypeNode etn = e.getType(); + if (!etn.isDatatype()) + { + // not a datatype term + d_register_st[e] = false; + return; + } + const Datatype& dt = etn.getDatatype(); + if (!dt.isSygus()) + { + // not a sygus datatype term + d_register_st[e] = false; + return; + } + if (!d_tds->isEnumerator(e)) + { + // not sure if it is a size term or not (may be registered later?) + return; + } + d_register_st[e] = true; + Node ag = d_tds->getActiveGuardForEnumerator(e); + if (!ag.isNull()) + { + d_anchor_to_active_guard[e] = ag; + std::map>::iterator itaas = + d_anchor_to_ag_strategy.find(e); + if (itaas == d_anchor_to_ag_strategy.end()) + { + d_anchor_to_ag_strategy[e].reset( + new DecisionStrategySingleton("sygus_enum_active", + ag, + d_td->getSatContext(), + d_td->getValuation())); + } + d_td->getDecisionManager()->registerStrategy( + DecisionManager::STRAT_DT_SYGUS_ENUM_ACTIVE, + d_anchor_to_ag_strategy[e].get()); + } + Node m; + if (!ag.isNull()) + { + // if it has an active guard (it is an enumerator), use itself as measure + // term. This will enforce fairness on it independently. + m = e; + } + else + { + // otherwise we enforce fairness in a unified way for all + if (d_generic_measure_term.isNull()) + { + // choose e as master for all future terms + d_generic_measure_term = e; + } + m = d_generic_measure_term; + } + Trace("sygus-sb") << "Sygus : register size term : " << e << " with measure " + << m << std::endl; + registerMeasureTerm(m); + d_szinfo[m]->d_anchors.push_back(e); + d_anchor_to_measure_term[e] = m; + NodeManager* nm = NodeManager::currentNM(); + if (options::sygusFair() == SYGUS_FAIR_DT_SIZE) + { + // update constraints on the measure term + Node slem; + if (options::sygusFairMax()) + { + Node ds = nm->mkNode(DT_SIZE, e); + slem = nm->mkNode(LEQ, ds, d_szinfo[m]->getOrMkMeasureValue(lemmas)); }else{ - d_register_st[e] = false; + Node mt = d_szinfo[m]->getOrMkActiveMeasureValue(lemmas); + Node new_mt = d_szinfo[m]->getOrMkActiveMeasureValue(lemmas, true); + Node ds = nm->mkNode(DT_SIZE, e); + slem = mt.eqNode(nm->mkNode(PLUS, new_mt, ds)); + } + Trace("sygus-sb") << "...size lemma : " << slem << std::endl; + lemmas.push_back(slem); + } + if (d_tds->isVariableAgnosticEnumerator(e)) + { + // if it is variable agnostic, enforce top-level constraint that says no + // variables occur pre-traversal at top-level + Node varList = Node::fromExpr(dt.getSygusVarList()); + std::vector constraints; + for (const Node& v : varList) + { + unsigned sc = d_tds->getSubclassForVar(etn, v); + // no symmetry breaking occurs for variables in singleton subclasses + if (d_tds->getNumSubclassVars(etn, sc) > 1) + { + Node preRootOp = getTraversalPredicate(etn, v, true); + Node preRoot = nm->mkNode(APPLY_UF, preRootOp, e); + constraints.push_back(preRoot.negate()); + } + } + if (!constraints.empty()) + { + Node preNoVar = constraints.size() == 1 ? constraints[0] + : nm->mkNode(AND, constraints); + Node preNoVarProc = eliminateTraversalPredicates(preNoVar); + Trace("sygus-sb") << "...variable order : " << preNoVarProc << std::endl; + Trace("sygus-sb-tp") << "...variable order : " << preNoVarProc + << std::endl; + lemmas.push_back(preNoVarProc); } } } @@ -1290,13 +1537,9 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) { ->toStreamSygus(ss, progv); Trace("dt-sygus") << ss.str() << std::endl; } - // TODO : remove this step (ensure there is no way a sygus term cannot be assigned a tester before this point) - if (!checkTesters(prog, progv, 0, lemmas)) + // first check that the value progv for prog is what we expected + if (checkValue(prog, progv, 0, lemmas)) { - Trace("sygus-sb") << " SygusSymBreakNew::check: ...WARNING: considered missing split for " << prog << "." << std::endl; - // this should not happen generally, it is caused by a sygus term not being assigned a tester - //Assert( false ); - }else{ //debugging : ensure fairness was properly handled if( options::sygusFair()==SYGUS_FAIR_DT_SIZE ){ Node prog_sz = NodeManager::currentNM()->mkNode( kind::DT_SIZE, prog ); @@ -1316,6 +1559,8 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) { // register the search value ( prog -> progv ), this may invoke symmetry breaking if( options::sygusSymBreakDynamic() ){ + // check that it is unique up to theory-specific rewriting and + // conjecture-specific symmetry breaking. Node rsv = registerSearchValue(prog, prog, progv, 0, lemmas); SygusSymBreakExcAttribute ssbea; prog.setAttribute(ssbea, rsv.isNull()); @@ -1355,10 +1600,10 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) { } } -bool SygusSymBreakNew::checkTesters(Node n, - Node vn, - int ind, - std::vector& lemmas) +bool SygusSymBreakNew::checkValue(Node n, + Node vn, + int ind, + std::vector& lemmas) { if (vn.getKind() != kind::APPLY_CONSTRUCTOR) { @@ -1366,16 +1611,22 @@ bool SygusSymBreakNew::checkTesters(Node n, Assert(!vn.getType().isDatatype()); return true; } - if( Trace.isOn("sygus-sb-warn") ){ - Node prog_sz = NodeManager::currentNM()->mkNode( kind::DT_SIZE, n ); + NodeManager* nm = NodeManager::currentNM(); + if (Trace.isOn("sygus-sb-check-value")) + { + Node prog_sz = nm->mkNode(DT_SIZE, n); Node prog_szv = d_td->getValuation().getModel()->getValue( prog_sz ); for( int i=0; igetEqualityEngine()->hasTerm(tst); @@ -1386,18 +1637,27 @@ bool SygusSymBreakNew::checkTesters(Node n, } if (!hastst || tstrep != d_true) { - Trace("sygus-sb-warn") << "- has tester : " << tst << " : " << ( hastst ? "true" : "false" ); - Trace("sygus-sb-warn") << ", value=" << tstrep << std::endl; + Trace("sygus-check-value") << "- has tester : " << tst << " : " + << (hastst ? "true" : "false"); + Trace("sygus-check-value") << ", value=" << tstrep << std::endl; if( !hastst ){ + // This should not happen generally, it is caused by a sygus term not + // being assigned a tester. Node split = DatatypesRewriter::mkSplit(n, dt); + Trace("sygus-sb") << " SygusSymBreakNew::check: ...WARNING: considered " + "missing split for " + << n << "." << std::endl; Assert( !split.isNull() ); lemmas.push_back( split ); return false; } } for( unsigned i=0; imkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex].getSelectorInternal( tn.toType(), i ) ), n ); - if (!checkTesters(sel, vn[i], ind + 1, lemmas)) + Node sel = nm->mkNode( + APPLY_SELECTOR_TOTAL, + Node::fromExpr(dt[cindex].getSelectorInternal(tn.toType(), i)), + n); + if (!checkValue(sel, vn[i], ind + 1, lemmas)) { return false; } diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h index 99f9672e7..a38e7c5b8 100644 --- a/src/theory/datatypes/datatypes_sygus.h +++ b/src/theory/datatypes/datatypes_sygus.h @@ -207,6 +207,82 @@ private: }; /** An instance of the above cache, for each anchor */ std::map< Node, SearchCache > d_cache; + //-----------------------------------traversal predicates + /** pre/post traversal predicates for each type, variable + * + * This stores predicates (pre, post) whose semantics correspond to whether + * a variable has occurred by a (pre, post) traversal of a symbolic term, + * where index = 0 corresponds to pre, index = 1 corresponds to post. For + * details, see getTraversalPredicate below. + */ + std::map> d_traversal_pred[2]; + /** traversal applications to Boolean variables + * + * This maps each application of a traversal predicate pre_x( t ) or + * post_x( t ) to a fresh Boolean variable. + */ + std::map d_traversal_bool; + /** get traversal predicate + * + * Get the predicates (pre, post) whose semantics correspond to whether + * a variable has occurred by this point in a (pre, post) traversal of a term. + * The type of getTraversalPredicate(tn, n, _) is tn -> Bool. + * + * For example, consider the term: + * f( x_1, g( x_2, x_3 ) ) + * and a left-to-right, depth-first traversal of this term. Let e be + * a variable of the same type as this term. We say that for the above term: + * pre_{x_1} is false for e, e.1 and true for e.2, e.2.1, e.2.2 + * pre_{x_2} is false for e, e.1, e.2, e.2.1, and true for e.2.2 + * pre_{x_3} is false for e, e.1, e.2, e.2.1, e.2.2 + * post_{x_1} is true for e.1, e.2.1, e.2.2, e.2, e + * post_{x_2} is false for e.1 and true for e.2.1, e.2.2, e.2, e + * post_{x_3} is false for e.1, e.2.1 and true for e.2.2, e.2, e + * + * We enforce a symmetry breaking scheme for each enumerator e that is + * "variable-agnostic" (see argument isVarAgnostic in registerEnumerator) + * that ensures the variables are ordered. This scheme makes use of these + * predicates, described in the following: + * + * Let x_1, ..., x_m be variables that occur in the same subclass in the type + * of e (see TermDbSygus::getSubclassForVar). + * For i = 1, ..., m: + * // each variable does not occur initially in a traversal of e + * ~pre_{x_i}( e ) AND + * // for each subterm of e + * template z. + * // if this is variable x_i, then x_{i-1} must have already occurred + * is-x_i( z ) => pre_{x_{i-1}}( z ) AND + * for args a = 1...n + * // pre-definition for each argument of this term + * pre_{x_i}( z.a ) = a=0 ? pre_{x_i}( z ) : post_{x_i}( z.{a-1} ) AND + * // post-definition for this term + * post_{x_i}( z ) = post_{x_i}( z.n ) OR is-x_i( z ) + * + * For clarity, above we have written pre and post as first-order predicates. + * However, applications of pre/post should be seen as indexed Boolean + * variables. The reason for this is pre and post cannot be given a consistent + * semantics. For example, consider term f( x_1, x_1 ) and enumerator variable + * e of the same type over which we are encoding a traversal. We have that + * pre_{x_1}( e.1 ) is false and pre_{x_1}( e.2 ) is true, although the model + * values for e.1 and e.2 are equal. Instead, pre_{x_1}( e.1 ) should be seen + * as a Boolean variable V_pre_{x_1,e.1} indexed by x_1 and e.1. and likewise + * for e.2. We convert all applications of pre/post to Boolean variables in + * the method eliminateTraversalPredicates below. Nevertheless, it is + * important that applications pre and post are encoded as APPLY_UF + * applications so that they behave as expected under substitutions. For + * example, pre_{x_1}( z.1 ) { z -> e.2 } results in pre_{x_1}( e.2.1 ), which + * after eliminateTraversalPredicates is V_pre_{x_1, e.2.1}. + */ + Node getTraversalPredicate(TypeNode tn, Node n, bool isPre); + /** eliminate traversal predicates + * + * This replaces all applications of traversal predicates P( x ) in n with + * unique Boolean variables, given by d_traversal_bool[ P( x ) ], and + * returns the result. + */ + Node eliminateTraversalPredicates(Node n); + //-----------------------------------end traversal predicates /** a sygus sampler object for each (anchor, sygus type) pair * * This is used for the sygusRewVerify() option to verify the correctness of @@ -396,15 +472,23 @@ private: * where t is a search term, see registerSearchTerm for definition of search * term. * - * usingSymCons is whether we are using symbolic constructors for subterms in - * the type tn. This may affect the form of the predicate we construct. + * usingSymCons: whether we are using symbolic constructors for subterms in + * the type tn, + * isVarAgnostic: whether the terms we are enumerating are agnostic to + * variables. + * + * The latter two options may affect the form of the predicate we construct. */ - Node getSimpleSymBreakPred(TypeNode tn, + Node getSimpleSymBreakPred(Node e, + TypeNode tn, int tindex, unsigned depth, - bool usingSymCons); + bool usingSymCons, + bool isVarAgnostic); /** Cache of the above function */ - std::map>>> + std::map>>>> d_simple_sb_pred; /** * For each search term, this stores the maximum depth for which we have added @@ -579,7 +663,7 @@ private: */ Node getCurrentTemplate( Node n, std::map< TypeNode, int >& var_count ); //----------------------end search size information - /** check testers + /** check value * * This is called when we have a model assignment vn for n, where n is * a selector chain applied to an enumerator (a search term). This function @@ -602,7 +686,7 @@ private: * method should not ever add anything to lemmas. However, due to its * importance, we check this regardless. */ - bool checkTesters(Node n, Node vn, int ind, std::vector& lemmas); + bool checkValue(Node n, Node vn, int ind, std::vector& lemmas); /** * Get the current SAT status of the guard g. * In particular, this returns 1 if g is asserted true, -1 if it is asserted -- 2.30.2