Document datatypes sygus (#1818)

4 files changed, 300 insertions, 175 deletions

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 4d3584596..6f660642e 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -40,7 +40,6 @@ SygusSymBreakNew::SygusSymBreakNew(TheoryDatatypes* td,
     : d_td(td),
       d_tds(tds),
       d_testers(c),
-      d_is_const(c),
       d_testers_exp(c),
       d_active_terms(c),
       d_currTermSize(c) {
@@ -100,21 +99,15 @@ void SygusSymBreakNew::assertTester( int tindex, TNode n, Node exp, std::vector<
 }
 
 void SygusSymBreakNew::assertFact( Node n, bool polarity, std::vector< Node >& lemmas ) {
-  if( n.getKind()==kind::DT_SYGUS_TERM_ORDER ){
-    if( polarity ){
-      Trace("sygus-sb-torder") << "Sygus term order : " << n[0] << " < " << n[1] << std::endl;
-      Node comm_sb = getTermOrderPredicate( n[0], n[1] );
-      Node comm_lem = NodeManager::currentNM()->mkNode( kind::OR, n.negate(), comm_sb );
-      lemmas.push_back( comm_lem );
-    }
-  }else if( n.getKind()==kind::DT_SYGUS_BOUND ){
+  if (n.getKind() == kind::DT_SYGUS_BOUND)
+  {
     Node m = n[0];
     Trace("sygus-fair") << "Have sygus bound : " << n << ", polarity=" << polarity << " on measure " << m << std::endl;
     registerMeasureTerm( m );
     if( options::sygusFair()==SYGUS_FAIR_DT_SIZE ){
       std::map< Node, SearchSizeInfo * >::iterator its = d_szinfo.find( m );
       Assert( its!=d_szinfo.end() );
-      Node mt = its->second->getOrMkSygusMeasureTerm( lemmas );
+      Node mt = its->second->getOrMkMeasureValue(lemmas);
       //it relates the measure term to arithmetic
       Node blem = n.eqNode( NodeManager::currentNM()->mkNode( kind::LEQ, mt, n[1] ) );
       lemmas.push_back( blem );
@@ -123,57 +116,12 @@ void SygusSymBreakNew::assertFact( Node n, bool polarity, std::vector< Node >& l
       unsigned s = n[1].getConst<Rational>().getNumerator().toUnsignedInt();
       notifySearchSize( m, s, n, lemmas );
     }
-  }else if( n.getKind() == kind::DT_SYGUS_IS_CONST ){
-    assertIsConst( n[0], polarity, lemmas );
   }else if( n.getKind() == kind::DT_HEIGHT_BOUND || n.getKind()==DT_SIZE_BOUND ){
     //reduce to arithmetic TODO ?
 
   }
 }
 
-void SygusSymBreakNew::assertIsConst( Node n, bool polarity, std::vector< Node >& lemmas ) {
-  if( d_active_terms.find( n )!=d_active_terms.end() ) {
-    // what kind of constructor is n?
-    IntMap::const_iterator itt = d_testers.find( n );
-    Assert( itt!=d_testers.end() );
-    int tindex = (*itt).second;
-    TypeNode tn = n.getType();
-    const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype();
-    Node lem;
-    if( dt[tindex].getNumArgs()==0 ){
-      // is this a constant?
-      Node sygus_op = Node::fromExpr( dt[tindex].getSygusOp() );
-      if( sygus_op.isConst()!=polarity ){
-        lem = NodeManager::currentNM()->mkNode( kind::DT_SYGUS_IS_CONST, n );
-        if( polarity ){
-          lem.negate();
-        }
-      }
-    }else{
-      // reduce
-      std::vector< Node > child_conj;
-      for( unsigned j=0; j<dt[tindex].getNumArgs(); j++ ){
-        Node sel = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[tindex].getSelectorInternal( tn.toType(), j ) ), n );
-        child_conj.push_back( NodeManager::currentNM()->mkNode( kind::DT_SYGUS_IS_CONST, sel ) );
-      }
-      lem = child_conj.size()==1 ? child_conj[0] : NodeManager::currentNM()->mkNode( kind::AND, child_conj );
-      // only an implication (TODO : strengthen?)
-      lem = NodeManager::currentNM()->mkNode( kind::OR, lem.negate(), NodeManager::currentNM()->mkNode( kind::DT_SYGUS_IS_CONST, n ) );
-    }
-    if( !lem.isNull() ){
-      Trace("sygus-isc") << "Sygus is-const lemma : " << lem << std::endl;
-      Node rlv = getRelevancyCondition( n );
-      if( !rlv.isNull() ){
-        lem = NodeManager::currentNM()->mkNode( kind::OR, rlv.negate(), lem );
-      }
-      lemmas.push_back( lem );
-    }
-  }else{
-    // lazy
-    d_is_const[n] = polarity ? 1 : -1;
-  }
-}
-
 Node SygusSymBreakNew::getTermOrderPredicate( Node n1, Node n2 ) {
   NodeManager* nm = NodeManager::currentNM();
   std::vector< Node > comm_disj;
@@ -269,13 +217,6 @@ void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std:
   d_active_terms.insert( n );
   Trace("sygus-sb-debug2") << "Sygus : activate term : " << n << " : " << exp << std::endl;  
   
-  /* TODO
-  IntMap::const_iterator itisc = d_is_const.find( n );
-  if( itisc != d_is_const.end() ){
-    assertIsConst( n, (*itisc).second==1, lemmas );
-  }
-  */
-  
   TypeNode ntn = n.getType();
   const Datatype& dt = ((DatatypeType)ntn.toType()).getDatatype();
   
@@ -502,21 +443,8 @@ Node SygusSymBreakNew::getSimpleSymBreakPred( TypeNode tn, int tindex, unsigned
             if( quantifiers::TermUtil::isComm( nk ) ){
               if( children.size()==2 ){
                 if( children[0].getType()==children[1].getType() ){
-  #if 0
-                  Node order_pred = NodeManager::currentNM()->mkNode( DT_SYGUS_TERM_ORDER, children[0], children[1] );
-                  sbp_conj.push_back( order_pred );
-                  Node child11 = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[tindex].getSelectorInternal( tn.toType(), 1 ) ), children[0] );
-                  Assert( child11.getType()==children[1].getType() );
-                  //chainable
-                  if( children[0].getType()==tn ){
-                    Node order_pred_trans = NodeManager::currentNM()->mkNode( OR, DatatypesRewriter::mkTester( children[0], tindex, dt ).negate(),
-                                                                              NodeManager::currentNM()->mkNode( DT_SYGUS_TERM_ORDER, child11, children[1] ) );
-                    sbp_conj.push_back( order_pred_trans );
-                  }
-  #else   
                   Node order_pred = getTermOrderPredicate( children[0], children[1] );
                   sbp_conj.push_back( order_pred );
-  #endif
                 }
               }
             }
@@ -672,23 +600,6 @@ TNode SygusSymBreakNew::getFreeVar( TypeNode tn ) {
   return d_tds->getFreeVar(tn, 0);
 }
 
-unsigned SygusSymBreakNew::processSelectorChain( Node n, std::map< TypeNode, Node >& top_level, std::map< Node, unsigned >& tdepth, std::vector< Node >& lemmas ) {
-  unsigned ret = 0;
-  if( n.getKind()==APPLY_SELECTOR_TOTAL ){
-    ret = processSelectorChain( n[0], top_level, tdepth, lemmas );
-  }
-  TypeNode tn = n.getType();
-  if( top_level.find( tn )==top_level.end() ){
-    top_level[tn] = n;
-    //tdepth[n] = ret;
-    registerSearchTerm( tn, ret, n, true, lemmas );
-  }else{
-    registerSearchTerm( tn, ret, n, false, lemmas );
-  }
-  tdepth[n] = ret;
-  return ret+1;
-}
-
 void SygusSymBreakNew::registerSearchTerm( TypeNode tn, unsigned d, Node n, bool topLevel, std::vector< Node >& lemmas ) {
   //register this term
   std::unordered_map<Node, Node, NodeHashFunction>::iterator ita =
@@ -1001,21 +912,17 @@ void SygusSymBreakNew::registerSizeTerm( Node e, std::vector< Node >& lemmas ) {
           if( options::sygusFair()==SYGUS_FAIR_DT_SIZE ){
             // update constraints on the measure term
             if( options::sygusFairMax() ){
-              if( options::sygusFair()==SYGUS_FAIR_DT_SIZE ){
-                Node ds = NodeManager::currentNM()->mkNode( kind::DT_SIZE, e );
-                Node slem = NodeManager::currentNM()->mkNode( kind::LEQ, ds, d_szinfo[m]->getOrMkSygusMeasureTerm( lemmas ) );
-                lemmas.push_back( slem );
-              }
+              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]->getOrMkSygusActiveMeasureTerm( lemmas );
-              Node new_mt = NodeManager::currentNM()->mkSkolem( "mt", NodeManager::currentNM()->integerType() );
-              lemmas.push_back( NodeManager::currentNM()->mkNode( kind::GEQ, new_mt, d_zero ) );
-              if( options::sygusFair()==SYGUS_FAIR_DT_SIZE ){
-                Node ds = NodeManager::currentNM()->mkNode( kind::DT_SIZE, e );
-                lemmas.push_back( mt.eqNode( NodeManager::currentNM()->mkNode( kind::PLUS, new_mt, ds ) ) );
-                //lemmas.push_back( NodeManager::currentNM()->mkNode( kind::GEQ, ds, d_zero ) );
-              }
-              d_szinfo[m]->d_sygus_measure_term_active = new_mt;
+              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{
@@ -1166,7 +1073,8 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) {
         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( !debugTesters( prog, progv, 0, lemmas ) ){
+      if (!checkTesters(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 );
@@ -1221,7 +1129,11 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) {
   }
 }
 
-bool SygusSymBreakNew::debugTesters( Node n, Node vn, int ind, std::vector< Node >& lemmas ) {
+bool SygusSymBreakNew::checkTesters(Node n,
+                                    Node vn,
+                                    int ind,
+                                    std::vector<Node>& lemmas)
+{
   Assert( vn.getKind()==kind::APPLY_CONSTRUCTOR );
   if( Trace.isOn("sygus-sb-warn") ){
     Node prog_sz = NodeManager::currentNM()->mkNode( kind::DT_SIZE, n );
@@ -1249,7 +1161,8 @@ bool SygusSymBreakNew::debugTesters( Node n, Node vn, int ind, std::vector< Node
   }
   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( !debugTesters( sel, vn[i], ind+1, lemmas ) ){
+    if (!checkTesters(sel, vn[i], ind + 1, lemmas))
+    {
       return false;
     }
   }
@@ -1278,19 +1191,37 @@ Node SygusSymBreakNew::getCurrentTemplate( Node n, std::map< TypeNode, int >& va
   }
 }
 
-Node SygusSymBreakNew::SearchSizeInfo::getOrMkSygusMeasureTerm( std::vector< Node >& lemmas ) {
-  if( d_sygus_measure_term.isNull() ){
-    d_sygus_measure_term = NodeManager::currentNM()->mkSkolem( "mt", NodeManager::currentNM()->integerType() );
-    lemmas.push_back( NodeManager::currentNM()->mkNode( kind::GEQ, d_sygus_measure_term, NodeManager::currentNM()->mkConst( Rational(0) ) ) );
+Node SygusSymBreakNew::SearchSizeInfo::getOrMkMeasureValue(
+    std::vector<Node>& lemmas)
+{
+  if (d_measure_value.isNull())
+  {
+    d_measure_value = NodeManager::currentNM()->mkSkolem(
+        "mt", NodeManager::currentNM()->integerType());
+    lemmas.push_back(NodeManager::currentNM()->mkNode(
+        kind::GEQ,
+        d_measure_value,
+        NodeManager::currentNM()->mkConst(Rational(0))));
   }
-  return d_sygus_measure_term;
+  return d_measure_value;
 }
 
-Node SygusSymBreakNew::SearchSizeInfo::getOrMkSygusActiveMeasureTerm( std::vector< Node >& lemmas ) {
-  if( d_sygus_measure_term_active.isNull() ){
-    d_sygus_measure_term_active = getOrMkSygusMeasureTerm( lemmas );
+Node SygusSymBreakNew::SearchSizeInfo::getOrMkActiveMeasureValue(
+    std::vector<Node>& lemmas, bool mkNew)
+{
+  if (mkNew)
+  {
+    Node new_mt = NodeManager::currentNM()->mkSkolem(
+        "mt", NodeManager::currentNM()->integerType());
+    lemmas.push_back(NodeManager::currentNM()->mkNode(
+        kind::GEQ, new_mt, NodeManager::currentNM()->mkConst(Rational(0))));
+    d_measure_value_active = new_mt;
+  }
+  else if (d_measure_value_active.isNull())
+  {
+    d_measure_value_active = getOrMkMeasureValue(lemmas);
   }
-  return d_sygus_measure_term_active;
+  return d_measure_value_active;
 }
 
 Node SygusSymBreakNew::SearchSizeInfo::getFairnessLiteral( unsigned s, TheoryDatatypes * d, std::vector< Node >& lemmas ) {
diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h
index 2936c1561..e0b29efd2 100644
--- a/src/theory/datatypes/datatypes_sygus.h
+++ b/src/theory/datatypes/datatypes_sygus.h
@@ -40,6 +40,17 @@ namespace datatypes {
 
 class TheoryDatatypes;
 
+/**
+ * This is the sygus extension of the decision procedure for quantifier-free
+ * inductive datatypes. At a high level, this class takes as input a
+ * set of asserted testers is-C1( x ), is-C2( x.1 ), is-C3( x.2 ), and
+ * generates lemmas that restrict the models of x, if x is a "sygus enumerator"
+ * (see TermDbSygus::registerEnumerator).
+ *
+ * Some of these techniques are described in these papers:
+ * "Refutation-Based Synthesis in SMT", Reynolds et al 2017.
+ * "Sygus Techniques in the Core of an SMT Solver", Reynolds et al 2017.
+ */
 class SygusSymBreakNew
 {
   typedef context::CDHashMap< Node, int, NodeHashFunction > IntMap;
@@ -52,11 +63,53 @@ class SygusSymBreakNew
                    quantifiers::TermDbSygus* tds,
                    context::Context* c);
   ~SygusSymBreakNew();
-  /** add tester */
+  /**
+   * Notify this class that tester for constructor tindex has been asserted for
+   * n. Exp is the literal corresponding to this tester. This method may add
+   * lemmas to the vector lemmas, for details see assertTesterInternal below.
+   * These lemmas are sent out on the output channel of datatypes by the caller.
+   */
   void assertTester(int tindex, TNode n, Node exp, std::vector<Node>& lemmas);
+  /**
+   * Notify this class that literal n has been asserted with the given
+   * polarity. This method may add lemmas to the vector lemmas, for instance
+   * based on inferring consequences of (not) n. One example is if n is
+   * (DT_SIZE_BOUND x n), we add the lemma:
+   *   (DT_SIZE_BOUND x n) <=> ((DT_SIZE x) <= n )
+   */
   void assertFact(Node n, bool polarity, std::vector<Node>& lemmas);
+  /** pre-register term n
+   *
+   * This is called when n is pre-registered with the theory of datatypes.
+   * If n is a sygus enumerator, then we may add lemmas to the vector lemmas
+   * that are used to enforce fairness regarding the size of n.
+   */
   void preRegisterTerm(TNode n, std::vector<Node>& lemmas);
+  /** check
+   *
+   * This is called at last call effort, when the current model assignment is
+   * satisfiable according to the quantifier-free decision procedures and a
+   * model is built. This method may add lemmas to the vector lemmas based
+   * on dynamic symmetry breaking techniques, based on the model values of
+   * all preregistered enumerators.
+   */
   void check(std::vector<Node>& lemmas);
+  /** get next decision request
+   *
+   * This function has the same interface as Theory::getNextDecisionRequest.
+   *
+   * The decisions returned by this method are of one of two forms:
+   * (1) Positive decisions on the active guards G of enumerators e registered
+   * to this class. These assert "there are more values to enumerate for e".
+   * (2) Positive bounds (DT_SYGUS_BOUND m n) for "measure terms" m (see below),
+   * where n is a non-negative integer. This asserts "the measure of terms
+   * we are enumerating for enumerators whose measure term m is at most n",
+   * where measure is commonly term size, but can also be height.
+   *
+   * We prioritize decisions of form (1) before (2). For both decisions,
+   * we set the priority argument to "1", indicating that the decision is
+   * critical for solution completeness.
+   */
   Node getNextDecisionRequest(unsigned& priority, std::vector<Node>& lemmas);
 
  private:
@@ -64,11 +117,33 @@ class SygusSymBreakNew
   TheoryDatatypes* d_td;
   /** Pointer to the sygus term database */
   quantifiers::TermDbSygus* d_tds;
+  /**
+   * Map from terms to the index of the tester that is asserted for them in
+   * the current SAT context. In other words, if d_testers[n] = 2, then the
+   * tester is-C_2(n) is asserted in this SAT context.
+   */
   IntMap d_testers;
-  IntMap d_is_const;
+  /**
+   * Map from terms to the tester asserted for them. In the example above,
+   * d_testers[n] = is-C_2(n).
+   */
   NodeMap d_testers_exp;
+  /**
+   * The set of (selector chain) terms that are active in the current SAT
+   * context. A selector chain term S_n( ... S_1( x )... ) is active if either:
+   * (1) n=0 and x is a sygus enumerator,
+   *   or:
+   * (2.1) S_{n-1}( ... S_1( x )) is active,
+   * (2.2) is-C( S_{n-1}( ... S_1( x )) ) is asserted in this SAT context, and
+   * (2.3) S_n is a selector for constructor C.
+   */
   NodeSet d_active_terms;
+  /**
+   * Map from enumerators to a lower bound on their size in the current SAT
+   * context.
+   */
   IntMap d_currTermSize;
+  /** zero */
   Node d_zero;
   /**
    * Map from terms (selector chains) to their anchors. The anchor of a
@@ -96,7 +171,6 @@ class SygusSymBreakNew
    *   S4 : T1 -> T3
    * Then, x, S1( x ), and S4( S3( S2( S1( x ) ) ) ) are top-level terms,
    * whereas S2( S1( x ) ) and S3( S2( S1( x ) ) ) are not.
-   *
    */
   std::unordered_map<Node, bool, NodeHashFunction> d_is_top_level;
   /**
@@ -330,59 +404,207 @@ private:
 
   /** Get the canonical free variable for type tn */
   TNode getFreeVar( TypeNode tn );
+  /** get term order predicate
+   *
+   * Assuming that n1 and n2 are children of a commutative operator, this
+   * returns a symmetry breaking predicate that can be instantiated for n1 and
+   * n2 while preserving satisfiability. By default, this is the predicate
+   *   ( DT_SIZE n1 ) >= ( DT_SIZE n2 )
+   */
   Node getTermOrderPredicate( Node n1, Node n2 );
-private:
- /**
-  * Map from registered variables to whether they are a sygus enumerator.
-  *
-  * This should be user context-dependent if sygus is updated to work in
-  * incremental mode.
-  */
- std::map<Node, bool> d_register_st;
- void registerSizeTerm(Node e, std::vector<Node>& lemmas);
- class SearchSizeInfo
- {
-  public:
+
+ private:
+  /**
+   * Map from registered variables to whether they are a sygus enumerator.
+   *
+   * This should be user context-dependent if sygus is updated to work in
+   * incremental mode.
+   */
+  std::map<Node, bool> d_register_st;
+  //----------------------search size information
+  /**
+   * Checks whether e is a sygus enumerator, that is, a term for which this
+   * class will track size for.
+   *
+   * We associate each sygus enumerator e with a "measure term", which is used
+   * for bounding the size of terms for the models of e. The measure term for a
+   * sygus enumerator may be e itself (if e has an active guard), or an
+   * arbitrary sygus variable otherwise. A measure term m is one for which our
+   * decision strategy decides on literals of the form (DT_SYGUS_BOUND m n).
+   *
+   * After determining the measure term m for e, if applicable, we initialize
+   * SearchSizeInfo for m below. This may result in lemmas
+   */
+  void registerSizeTerm(Node e, std::vector<Node>& lemmas);
+  /** information for each measure term allocated by this class */
+  class SearchSizeInfo
+  {
+   public:
     SearchSizeInfo( Node t, context::Context* c ) : d_this( t ), d_curr_search_size(0), d_curr_lit( c, 0 ) {}
+    /** the measure term */
     Node d_this;
+    /**
+     * For each size n, an explanation for why this measure term has size at
+     * most n. This is typically the literal (DT_SYGUS_BOUND m n), which
+     * we call the (n^th) "fairness literal" for m.
+     */
     std::map< unsigned, Node > d_search_size_exp;
+    /**
+     * For each size, whether we have called SygusSymBreakNew::notifySearchSize.
+     */
     std::map< unsigned, bool > d_search_size;
+    /**
+     * The current search size. This corresponds to the number of times
+     * incrementCurrentSearchSize has been called for this measure term.
+     */
     unsigned d_curr_search_size;
-    Node d_sygus_measure_term;
-    Node d_sygus_measure_term_active;
+    /** the list of all enumerators whose measure term is this */
     std::vector< Node > d_anchors;
-    Node getOrMkSygusMeasureTerm( std::vector< Node >& lemmas );
-    Node getOrMkSygusActiveMeasureTerm( std::vector< Node >& lemmas );
-  public:
-    /** current cardinality */
+    /** get or make the measure value
+     *
+     * The measure value is an integer variable v that is a (symbolic) integer
+     * value that is constrained to be less than or equal to the current search
+     * size. For example, if we are using the fairness strategy
+     * SYGUS_FAIR_DT_SIZE (see options/datatype_options.h), then we constrain:
+     *   (DT_SYGUS_BOUND m n) <=> (v <= n)
+     * for all asserted fairness literals. Then, if we are enforcing fairness
+     * based on the maximum size, we assert:
+     *   (DT_SIZE e) <= v
+     * for all enumerators e.
+     */
+    Node getOrMkMeasureValue(std::vector<Node>& lemmas);
+    /** get or make the active measure value
+     *
+     * The active measure value av is an integer variable that corresponds to
+     * the (symbolic) value of the sum of enumerators that are yet to be
+     * registered. This is to enforce the "sum of measures" strategy. For
+     * example, if we are using the fairness strategy SYGUS_FAIR_DT_SIZE,
+     * then initially av is equal to the measure value v, and the constraints
+     *   (DT_SYGUS_BOUND m n) <=> (v <= n)
+     * are added as before. When an enumerator e is registered, we add the
+     * lemma:
+     *   av = (DT_SIZE e) + av'
+     * and update the active measure value to av'. This ensures that the sum
+     * of sizes of active enumerators is at most n.
+     *
+     * If the flag mkNew is set to true, then we return a fresh variable and
+     * update the active measure value.
+     */
+    Node getOrMkActiveMeasureValue(std::vector<Node>& lemmas,
+                                   bool mkNew = false);
+    /**
+     * The current search size literal for this measure term. This corresponds
+     * to the minimial n such that (DT_SYGUS_BOUND d_this n) is asserted in
+     * this SAT context.
+     */
     context::CDO< unsigned > d_curr_lit;
+    /**
+     * Map from integers n to the fairness literal, for each n such that this
+     * literal has been allocated (by getFairnessLiteral below).
+     */
     std::map< unsigned, Node > d_lits;
+    /**
+     * Returns the s^th fairness literal for this measure term. This adds a
+     * split on this literal to lemmas.
+     */
     Node getFairnessLiteral( unsigned s, TheoryDatatypes * d, std::vector< Node >& lemmas );
+    /** get the current fairness literal */
     Node getCurrentFairnessLiteral( TheoryDatatypes * d, std::vector< Node >& lemmas ) { 
       return getFairnessLiteral( d_curr_lit.get(), d, lemmas ); 
     }
     /** increment current term size */
     void incrementCurrentLiteral() { d_curr_lit.set( d_curr_lit.get() + 1 ); }
+
+   private:
+    /** the measure value */
+    Node d_measure_value;
+    /** the sygus measure value */
+    Node d_measure_value_active;
   };
+  /** the above information for each registered measure term */
   std::map< Node, SearchSizeInfo * > d_szinfo;
+  /** map from enumerators (anchors) to their associated measure term */
   std::map< Node, Node > d_anchor_to_measure_term;
+  /** map from enumerators (anchors) to their active guard*/
   std::map< Node, Node > d_anchor_to_active_guard;
+  /** generic measure term
+   *
+   * This is a global term that is used as the measure term for all sygus
+   * enumerators that do not have active guards. This class enforces that
+   * all enumerators have size at most n, where n is the minimal integer
+   * such that (DT_SYGUS_BOUND d_generic_measure_term n) is asserted.
+   */
   Node d_generic_measure_term;
+  /**
+   * This increments the current search size for measure term m. This may
+   * cause lemmas to be added to lemmas based on the fact that symmetry
+   * breaking lemmas are now relevant for new search terms, see discussion
+   * of how search size affects which lemmas are relevant above
+   * addSymBreakLemmasFor.
+   */
   void incrementCurrentSearchSize( Node m, std::vector< Node >& lemmas );
+  /**
+   * Notify this class that we are currently searching for terms of size at
+   * most s as model values for measure term m. Literal exp corresponds to the
+   * explanation of why the measure term has size at most n. This calls
+   * incrementSearchSize above, until the total number of times we have called
+   * incrementSearchSize so far is at least s.
+   */
   void notifySearchSize( Node m, unsigned s, Node exp, std::vector< Node >& lemmas );
+  /** Allocates a SearchSizeInfo object in d_szinfo. */
   void registerMeasureTerm( Node m );
+  /**
+   * Return the current search size for arbitrary term n. This is the current
+   * search size of the anchor of n.
+   */
   unsigned getSearchSizeFor( Node n );
-  unsigned getSearchSizeForAnchor( Node n );
+  /** return the current search size for enumerator (anchor) e */
+  unsigned getSearchSizeForAnchor(Node e);
+  /** Get the current search size for measure term m in this SAT context. */
   unsigned getSearchSizeForMeasureTerm(Node m);
-
- private:
-  unsigned processSelectorChain( Node n, std::map< TypeNode, Node >& top_level, 
-                                 std::map< Node, unsigned >& tdepth, std::vector< Node >& lemmas );
-  bool debugTesters( Node n, Node vn, int ind, std::vector< Node >& lemmas );
+  /** get current template
+   *
+   * For debugging. This returns a term that corresponds to the current
+   * inferred shape of n. For example, if the testers
+   *   is-C1( n ) and is-C2( n.1 )
+   * have been asserted where C1 and C2 are binary constructors, then this
+   * method may return a term of the form:
+   *   C1( C2( x1, x2 ), x3 )
+   * for fresh variables x1, x2, x3. The map var_count maintains the variable
+   * count for generating these fresh variables.
+   */
   Node getCurrentTemplate( Node n, std::map< TypeNode, int >& var_count );
+  //----------------------end search size information
+  /** check testers
+   *
+   * 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
+   * ensures that testers have been asserted for each subterm of vn. This is
+   * critical for ensuring that the proper steps have been taken by this class
+   * regarding whether or not vn is a legal value for n (not greater than the
+   * current search size and not a value that can be blocked by symmetry
+   * breaking).
+   *
+   * For example, if vn = +( x(), x() ), then we ensure that the testers
+   *   is-+( n ), is-x( n.1 ), is-x( n.2 )
+   * have been asserted to this class. If a tester is not asserted for some
+   * relevant selector chain S( n ) of n, then we add a lemma L for that
+   * selector chain to lemmas, where L is the "splitting lemma" for S( n ), that
+   * states that the top symbol of S( n ) must be one of the constructors of
+   * its type.
+   *
+   * Notice that this function is a sanity check. Typically, it should be the
+   * case that testers are asserted for all subterms of vn, and hence this
+   * 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);
+  /**
+   * Get the current SAT status of the guard g.
+   * In particular, this returns 1 if g is asserted true, -1 if it is asserted
+   * false, and 0 if it is not asserted.
+   */
   int getGuardStatus( Node g );
-private:
-  void assertIsConst( Node n, bool polarity, std::vector< Node >& lemmas );
 };
 
 }
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index 3ce416b40..65f258de1 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -114,10 +114,4 @@ typerule DT_SIZE_BOUND ::CVC4::theory::datatypes::DtBoundTypeRule
 operator DT_SYGUS_BOUND 2 "datatypes sygus bound"
 typerule DT_SYGUS_BOUND ::CVC4::theory::datatypes::DtSygusBoundTypeRule
 
-operator DT_SYGUS_TERM_ORDER 2 "datatypes sygus term order"
-typerule DT_SYGUS_TERM_ORDER ::CVC4::theory::datatypes::DtSygusPredTypeRule
-
-operator DT_SYGUS_IS_CONST 1 "datatypes sygus is constant"
-typerule DT_SYGUS_IS_CONST ::CVC4::theory::datatypes::DtSygusPredTypeRule
-
 endtheory
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index d6045404d..6ba64d8dd 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -359,28 +359,6 @@ class DtSygusBoundTypeRule {
   }
 }; /* class DtSygusBoundTypeRule */
 
-
-class DtSygusPredTypeRule {
- public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
-                                     bool check) {
-    if (check) {
-      TypeNode tn = n[0].getType();
-      if (!tn.isDatatype() || !((DatatypeType)tn.toType()).getDatatype().isSygus()) {
-        throw TypeCheckingExceptionPrivate(
-            n, "datatype sygus predicate expecting terms of sygus type");
-      }
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        if (tn!=n[i].getType()) {
-          throw TypeCheckingExceptionPrivate(
-              n, "datatype sygus predicate expecting two terms of the same type");
-        }
-      }
-    }
-    return nodeManager->booleanType();
-  }
-}; /* class DtSygusPredTypeRule */
-
 } /* CVC4::theory::datatypes namespace */
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */