Symmetry breaking for variable agnostic enumerators (#2527)

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<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")
@@ -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<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;
   }
@@ -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<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)
     {
@@ -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<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);
     }
   }
 }
@@ -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<Node>& lemmas)
+bool SygusSymBreakNew::checkValue(Node n,
+                                  Node vn,
+                                  int ind,
+                                  std::vector<Node>& 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; 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);
@@ -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; 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;
     }
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<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
@@ -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<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
@@ -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<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