if( min_depth<=max_depth ){
TNode x = getFreeVar( ntn );
std::vector<Node> sb_lemmas;
+ // symmetry breaking lemmas requiring predicate elimination
+ std::map<Node, bool> 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")
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);
}
}
-Node SygusSymBreakNew::getSimpleSymBreakPred(TypeNode tn,
+Node SygusSymBreakNew::getTraversalPredicate(TypeNode tn, Node n, bool isPre)
+{
+ unsigned index = isPre ? 0 : 1;
+ std::map<Node, Node>::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<TypeNode> 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<TNode, Node, TNodeHashFunction> visited;
+ std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+ std::map<Node, Node>::iterator ittb;
+ std::vector<TNode> 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<Node> 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<unsigned, Node>::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;
}
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
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<int>(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)
{
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;
}
}
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<Node, std::unique_ptr<DecisionStrategy>>::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<Node, std::unique_ptr<DecisionStrategy>>::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<Node> 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);
}
}
}
->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 );
// 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());
}
}
-bool SygusSymBreakNew::checkTesters(Node n,
- Node vn,
- int ind,
- std::vector<Node>& lemmas)
+bool SygusSymBreakNew::checkValue(Node n,
+ Node vn,
+ int ind,
+ std::vector<Node>& lemmas)
{
if (vn.getKind() != kind::APPLY_CONSTRUCTOR)
{
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; i<ind; i++ ){
- Trace("sygus-sb-warn") << " ";
+ Trace("sygus-sb-check-value") << " ";
}
- Trace("sygus-sb-warn") << n << " : " << vn << " : " << prog_szv << std::endl;
+ Trace("sygus-sb-check-value") << n << " : " << vn << " : " << prog_szv
+ << std::endl;
}
TypeNode tn = n.getType();
- const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype();
+ const Datatype& dt = tn.getDatatype();
+ Assert(dt.isSygus());
+
+ // ensure that the expected size bound is met
int cindex = DatatypesRewriter::indexOf(vn.getOperator());
Node tst = DatatypesRewriter::mkTester( n, cindex, dt );
bool hastst = d_td->getEqualityEngine()->hasTerm(tst);
}
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; i<vn.getNumChildren(); i++ ){
- Node sel = NodeManager::currentNM()->mkNode( 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;
}
};
/** 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<TypeNode, std::map<Node, Node>> 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<Node, Node> 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
* 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<TypeNode, std::map<int, std::map<bool, std::map<unsigned, Node>>>>
+ std::map<Node,
+ std::map<TypeNode,
+ std::map<int, std::map<bool, std::map<unsigned, Node>>>>>
d_simple_sb_pred;
/**
* For each search term, this stores the maximum depth for which we have added
*/
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
* 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<Node>& lemmas);
+ bool checkValue(Node n, Node vn, int ind, std::vector<Node>& 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
projects / cvc5.git / commitdiff