Merge branch 'master' into rewrite_concatrewrite_concat

3 files changed, 481 insertions, 351 deletions

diff --git a/.travis.yml b/.travis.yml
index 94cee00ab..d1f72f955 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -77,7 +77,7 @@ script:
      exit 1;
    }
    makeDistcheck() {
-     make V=1 -j2 distcheck CVC4_REGRESSION_ARGS='--no-early-exit' ||
+     make V=1 -j2 distcheck REGRESSION_LEVEL=0 CVC4_REGRESSION_ARGS='--no-early-exit' ||
        error "DISTCHECK (WITH NEWTHEORY TESTS) FAILED";
    }
    makeCheck() {
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index 1c61544e1..528f47624 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -1252,11 +1252,12 @@ void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >&
                 itv->second.setSolved( v );
                 // it subsumes everything
                 itv->second.d_term_trie.clear();
-                itv->second.d_term_trie.addTerm( this, v, results, true, subsume );
+                itv->second.d_term_trie.addTerm(v, results, true, subsume);
               }
               keep = true;
             }else{
-              Node val = itv->second.d_term_trie.addTerm( this, v, results, true, subsume );
+              Node val =
+                  itv->second.d_term_trie.addTerm(v, results, true, subsume);
               if( val==v ){
                 Trace("sygus-pbe-enum") << "  ...success"; 
                 if( !subsume.empty() ){
@@ -1275,7 +1276,7 @@ void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >&
           }
         }else{
           // must be unique up to examples
-          Node val = itv->second.d_term_trie.addCond(this, v, results, true);
+          Node val = itv->second.d_term_trie.addCond(v, results, true);
           if (val == v)
           {
             Trace("sygus-pbe-enum") << "  ...success!   add to PBE pool : "
@@ -1473,238 +1474,264 @@ bool CegConjecturePbe::CandidateInfo::isNonTrivial() {
 }
 
 // status : 0 : exact, -1 : vals is subset, 1 : vals is superset
-Node CegConjecturePbe::SubsumeTrie::addTermInternal( CegConjecturePbe * pbe, Node t, std::vector< Node >& vals, bool pol, 
-                                                     std::vector< Node >& subsumed, bool spol, IndexFilter * f, 
-                                                     unsigned index, int status, bool checkExistsOnly, bool checkSubsume ) {
-  if( index==vals.size() ){
-    if( status==0 ){
+Node CegConjecturePbe::SubsumeTrie::addTermInternal(
+    Node t,
+    const std::vector<Node>& vals,
+    bool pol,
+    std::vector<Node>& subsumed,
+    bool spol,
+    unsigned index,
+    int status,
+    bool checkExistsOnly,
+    bool checkSubsume)
+{
+  if (index == vals.size())
+  {
+    if (status == 0)
+    {
       // set the term if checkExistsOnly = false
-      if( d_term.isNull() && !checkExistsOnly ){
+      if (d_term.isNull() && !checkExistsOnly)
+      {
         d_term = t;
       }
-    }else if( status==1 ){
-      Assert( checkSubsume );
+    }
+    else if (status == 1)
+    {
+      Assert(checkSubsume);
       // found a subsumed term
-      if( !d_term.isNull() ){
-        subsumed.push_back( d_term );
-        if( !checkExistsOnly ){
+      if (!d_term.isNull())
+      {
+        subsumed.push_back(d_term);
+        if (!checkExistsOnly)
+        {
           // remove it if checkExistsOnly = false
           d_term = Node::null();
         }
       }
-    }else{
-      Assert( !checkExistsOnly && checkSubsume );
+    }
+    else
+    {
+      Assert(!checkExistsOnly && checkSubsume);
     }
     return d_term;
-  }else{
-    // the current value 
-    Assert( pol || ( vals[index].isConst() && vals[index].getType().isBoolean() ) );
-    Node cv = pol ? vals[index] : ( vals[index]==pbe->d_true ? pbe->d_false : pbe->d_true );
-    // if checkExistsOnly = false, check if the current value is subsumed if checkSubsume = true, if so, don't add
-    if( !checkExistsOnly && checkSubsume ){
-      std::vector< bool > check_subsumed_by;
-      if( status==0 ){
-        if( cv==pbe->d_false ){
-          check_subsumed_by.push_back( spol );
-        }
-      }else if( status==-1 ){
-        check_subsumed_by.push_back( spol );
-        if( cv==pbe->d_false ){
-          check_subsumed_by.push_back( !spol );
-        }
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  // the current value
+  Assert(pol || (vals[index].isConst() && vals[index].getType().isBoolean()));
+  Node cv = pol ? vals[index] : nm->mkConst(!vals[index].getConst<bool>());
+  // if checkExistsOnly = false, check if the current value is subsumed if
+  // checkSubsume = true, if so, don't add
+  if (!checkExistsOnly && checkSubsume)
+  {
+    Assert(cv.isConst() && cv.getType().isBoolean());
+    std::vector<bool> check_subsumed_by;
+    if (status == 0)
+    {
+      if (!cv.getConst<bool>())
+      {
+        check_subsumed_by.push_back(spol);
       }
-      // check for subsumed nodes
-      for( unsigned i=0; i<check_subsumed_by.size(); i++ ){
-        Node csval = check_subsumed_by[i] ? pbe->d_true : pbe->d_false;
-        // check if subsumed
-        std::map< Node, SubsumeTrie >::iterator itc = d_children.find( csval );
-        if( itc!=d_children.end() ){
-          unsigned next_index = f ? f->next( index ) : index+1;
-          Node ret = itc->second.addTermInternal( pbe, t, vals, pol, subsumed, spol, f, next_index, -1, checkExistsOnly, checkSubsume );
-          // ret subsumes t
-          if( !ret.isNull() ){
-            return ret;
-          }
-        }
+    }
+    else if (status == -1)
+    {
+      check_subsumed_by.push_back(spol);
+      if (!cv.getConst<bool>())
+      {
+        check_subsumed_by.push_back(!spol);
       }
     }
-    Node ret;
-    std::vector< bool > check_subsume;
-    if( status==0 ){
-      unsigned next_index = f ? f->next( index ) : index+1;
-      if( checkExistsOnly ){
-        std::map< Node, SubsumeTrie >::iterator itc = d_children.find( cv );
-        if( itc!=d_children.end() ){
-          ret = itc->second.addTermInternal( pbe, t, vals, pol, subsumed, spol, f, next_index, 0, checkExistsOnly, checkSubsume );
-        }
-      }else{
-        Assert( spol );
-        ret = d_children[cv].addTermInternal( pbe, t, vals, pol, subsumed, spol, f, next_index, 0, checkExistsOnly, checkSubsume );
-        if( ret!=t ){
-          // we were subsumed by ret, return
+    // check for subsumed nodes
+    for (unsigned i = 0, size = check_subsumed_by.size(); i < size; i++)
+    {
+      bool csbi = check_subsumed_by[i];
+      Node csval = nm->mkConst(csbi);
+      // check if subsumed
+      std::map<Node, SubsumeTrie>::iterator itc = d_children.find(csval);
+      if (itc != d_children.end())
+      {
+        Node ret = itc->second.addTermInternal(t,
+                                               vals,
+                                               pol,
+                                               subsumed,
+                                               spol,
+                                               index + 1,
+                                               -1,
+                                               checkExistsOnly,
+                                               checkSubsume);
+        // ret subsumes t
+        if (!ret.isNull())
+        {
           return ret;
         }
       }
-      if( checkSubsume ){
-        // check for subsuming
-        if( cv==pbe->d_true ){
-          check_subsume.push_back( !spol );
-        }
+    }
+  }
+  Node ret;
+  std::vector<bool> check_subsume;
+  if (status == 0)
+  {
+    if (checkExistsOnly)
+    {
+      std::map<Node, SubsumeTrie>::iterator itc = d_children.find(cv);
+      if (itc != d_children.end())
+      {
+        ret = itc->second.addTermInternal(t,
+                                          vals,
+                                          pol,
+                                          subsumed,
+                                          spol,
+                                          index + 1,
+                                          0,
+                                          checkExistsOnly,
+                                          checkSubsume);
       }
-    }else if( status==1 ){
-      Assert( checkSubsume );
-      check_subsume.push_back( !spol );
-      if( cv==pbe->d_true ){
-        check_subsume.push_back( spol );
+    }
+    else
+    {
+      Assert(spol);
+      ret = d_children[cv].addTermInternal(t,
+                                           vals,
+                                           pol,
+                                           subsumed,
+                                           spol,
+                                           index + 1,
+                                           0,
+                                           checkExistsOnly,
+                                           checkSubsume);
+      if (ret != t)
+      {
+        // we were subsumed by ret, return
+        return ret;
       }
     }
-    if( checkSubsume ){
-      // check for subsumed terms
-      for( unsigned i=0; i<check_subsume.size(); i++ ){
-        Node csval = check_subsume[i] ? pbe->d_true : pbe->d_false;
-        std::map< Node, SubsumeTrie >::iterator itc = d_children.find( csval );
-        if( itc!=d_children.end() ){
-          unsigned next_index = f ? f->next( index ) : index+1;
-          itc->second.addTermInternal( pbe, t, vals, pol, subsumed, spol, f, next_index, 1, checkExistsOnly, checkSubsume );
-          // clean up
-          if( itc->second.isEmpty() ){
-            Assert( !checkExistsOnly );
-            d_children.erase( csval );
-          }
+    if (checkSubsume)
+    {
+      Assert(cv.isConst() && cv.getType().isBoolean());
+      // check for subsuming
+      if (cv.getConst<bool>())
+      {
+        check_subsume.push_back(!spol);
+      }
+    }
+  }
+  else if (status == 1)
+  {
+    Assert(checkSubsume);
+    Assert(cv.isConst() && cv.getType().isBoolean());
+    check_subsume.push_back(!spol);
+    if (cv.getConst<bool>())
+    {
+      check_subsume.push_back(spol);
+    }
+  }
+  if (checkSubsume)
+  {
+    // check for subsumed terms
+    for (unsigned i = 0, size = check_subsume.size(); i < size; i++)
+    {
+      Node csval = nm->mkConst<bool>(check_subsume[i]);
+      std::map<Node, SubsumeTrie>::iterator itc = d_children.find(csval);
+      if (itc != d_children.end())
+      {
+        itc->second.addTermInternal(t,
+                                    vals,
+                                    pol,
+                                    subsumed,
+                                    spol,
+                                    index + 1,
+                                    1,
+                                    checkExistsOnly,
+                                    checkSubsume);
+        // clean up
+        if (itc->second.isEmpty())
+        {
+          Assert(!checkExistsOnly);
+          d_children.erase(csval);
         }
       }
     }
-    return ret;
   }
+  return ret;
 }
 
-Node CegConjecturePbe::SubsumeTrie::addTerm( CegConjecturePbe * pbe, Node t, std::vector< Node >& vals, bool pol, std::vector< Node >& subsumed, IndexFilter * f ) {
-  unsigned start_index = f ? f->start() : 0;
-  return addTermInternal( pbe, t, vals, pol, subsumed, true, f, start_index, 0, false, true );
+Node CegConjecturePbe::SubsumeTrie::addTerm(Node t,
+                                            const std::vector<Node>& vals,
+                                            bool pol,
+                                            std::vector<Node>& subsumed)
+{
+  return addTermInternal(t, vals, pol, subsumed, true, 0, 0, false, true);
 }
 
-Node CegConjecturePbe::SubsumeTrie::addCond( CegConjecturePbe * pbe, Node c, std::vector< Node >& vals, bool pol, IndexFilter * f ) {
-  unsigned start_index = f ? f->start() : 0;
-  std::vector< Node > subsumed;
-  return addTermInternal( pbe, c, vals, pol, subsumed, true, f, start_index, 0, false, false );
+Node CegConjecturePbe::SubsumeTrie::addCond(Node c,
+                                            const std::vector<Node>& vals,
+                                            bool pol)
+{
+  std::vector<Node> subsumed;
+  return addTermInternal(c, vals, pol, subsumed, true, 0, 0, false, false);
 }
 
-void CegConjecturePbe::SubsumeTrie::getSubsumed( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::vector< Node >& subsumed, IndexFilter * f ){
-  unsigned start_index = f ? f->start() : 0;
-  addTermInternal( pbe, Node::null(), vals, pol, subsumed, true, f, start_index, 1, true, true );
+void CegConjecturePbe::SubsumeTrie::getSubsumed(const std::vector<Node>& vals,
+                                                bool pol,
+                                                std::vector<Node>& subsumed)
+{
+  addTermInternal(Node::null(), vals, pol, subsumed, true, 0, 1, true, true);
 }
 
-void CegConjecturePbe::SubsumeTrie::getSubsumedBy( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::vector< Node >& subsumed_by, IndexFilter * f ){
+void CegConjecturePbe::SubsumeTrie::getSubsumedBy(
+    const std::vector<Node>& vals, bool pol, std::vector<Node>& subsumed_by)
+{
   // flip polarities
-  unsigned start_index = f ? f->start() : 0;
-  addTermInternal( pbe, Node::null(), vals, !pol, subsumed_by, false, f, start_index, 1, true, true );
+  addTermInternal(
+      Node::null(), vals, !pol, subsumed_by, false, 0, 1, true, true);
 }
 
-void CegConjecturePbe::SubsumeTrie::getLeavesInternal( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::map< int, std::vector< Node > >& v, 
-                                                       IndexFilter * f, unsigned index, int status ) {
-  if( index==vals.size() ){
-    Assert( !d_term.isNull() );
-    Assert( std::find( v[status].begin(), v[status].end(), d_term )==v[status].end() );
-    v[status].push_back( d_term );
-  }else{
-    Assert( vals[index].isConst() && vals[index].getType().isBoolean() );
-    // filter should be for cv
-    Assert( f==NULL || vals[index]==( pol ? pbe->d_true : pbe->d_false ) );
-    for( std::map< Node, SubsumeTrie >::iterator it = d_children.begin(); it != d_children.end(); ++it ){
+void CegConjecturePbe::SubsumeTrie::getLeavesInternal(
+    const std::vector<Node>& vals,
+    bool pol,
+    std::map<int, std::vector<Node> >& v,
+    unsigned index,
+    int status)
+{
+  if (index == vals.size())
+  {
+    Assert(!d_term.isNull());
+    Assert(std::find(v[status].begin(), v[status].end(), d_term)
+           == v[status].end());
+    v[status].push_back(d_term);
+  }
+  else
+  {
+    Assert(vals[index].isConst() && vals[index].getType().isBoolean());
+    bool curr_val_true = vals[index].getConst<bool>() == pol;
+    for (std::map<Node, SubsumeTrie>::iterator it = d_children.begin();
+         it != d_children.end();
+         ++it)
+    {
       int new_status = status;
       // if the current value is true
-      if( vals[index]==( pol ? pbe->d_true : pbe->d_false ) ){
-        if( status!=0 ){
-          new_status = ( it->first == pbe->d_true ? 1 : -1 );
-          if( status!=-2 && new_status!=status ){
+      if (curr_val_true)
+      {
+        if (status != 0)
+        {
+          Assert(it->first.isConst() && it->first.getType().isBoolean());
+          new_status = (it->first.getConst<bool>() ? 1 : -1);
+          if (status != -2 && new_status != status)
+          {
             new_status = 0;
           }
         }
       }
-      unsigned next_index = f ? f->next( index ) : index+1;
-      it->second.getLeavesInternal( pbe, vals, pol, v, f, next_index, new_status );
+      it->second.getLeavesInternal(vals, pol, v, index + 1, new_status);
     }
   }
 }
 
-void CegConjecturePbe::SubsumeTrie::getLeaves( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::map< int, std::vector< Node > >& v, IndexFilter * f ) {
-  unsigned start_index = f ? f->start() : 0;
-  getLeavesInternal( pbe, vals, pol, v, f, start_index, -2 );
-}
-
-void CegConjecturePbe::IndexFilter::mk( std::vector< Node >& vals, bool pol ) {
-  Trace("sygus-pbe-debug") << "Make for : ";
-  print_val( "sygus-pbe-debug", vals, pol );
-  Trace("sygus-pbe-debug") << std::endl;
-  Node poln = NodeManager::currentNM()->mkConst( pol );
-  
-  unsigned curr_index = 0;
-  while( curr_index<vals.size() && vals[curr_index]!=poln ){
-    curr_index++;
-  }
-  d_next[0] = curr_index;
-  Trace("sygus-pbe-debug") << "0 -> " << curr_index << std::endl;
-  unsigned i = curr_index;
-  while( i<vals.size() ){
-    while( i<vals.size() && vals[i]!=poln ){
-      i++;
-    }
-    i++;
-    d_next[curr_index+1] = i;
-    Trace("sygus-pbe-debug") << curr_index+1 << " -> " << i << std::endl;
-    curr_index = i;
-  }
-  
-  // verify it is correct
-  unsigned j = start();
-  for( unsigned k=0; k<j; k++ ){
-    AlwaysAssert( vals[k]!=poln );
-  }
-  Trace("sygus-pbe-debug") << "...start : " << j << std::endl;
-  unsigned counter = 0;
-  while( j<vals.size() ){
-    Trace("sygus-pbe-debug") << "...at : " << j << std::endl;
-    AlwaysAssert( vals[j]==poln );
-    unsigned jj = next( j );
-    AlwaysAssert( jj>j );
-    for( unsigned k=(j+1); k<jj; k++ ){
-      AlwaysAssert( vals[k]!=poln );
-    }
-    AlwaysAssert( counter<=vals.size() );
-    counter++;
-    j = jj;
-  }
-  
-  
-}
-
-unsigned CegConjecturePbe::IndexFilter::start() {
-  std::map< unsigned, unsigned >::iterator it = d_next.find( 0 );
-  if( it==d_next.end() ){
-    return 0;
-  }else{
-    return it->second;
-  }
-}
-
-unsigned CegConjecturePbe::IndexFilter::next( unsigned i ) {
-  std::map< unsigned, unsigned >::iterator it = d_next.find( i+1 );
-  if( it==d_next.end() ){
-    return i+1;
-  }else{
-    return it->second;
-  }      
-}
-
-bool CegConjecturePbe::IndexFilter::isEq( std::vector< Node >& vals, Node v ) {
-  unsigned index = start();
-  while( index<vals.size() ){
-    if( vals[index]!=v ){
-      return false;
-    }
-    index = next( index );
-  }
-  return true;
+void CegConjecturePbe::SubsumeTrie::getLeaves(
+    const std::vector<Node>& vals,
+    bool pol,
+    std::map<int, std::vector<Node> >& v)
+{
+  getLeavesInternal(vals, pol, v, 0, -2);
 }
 
 Node CegConjecturePbe::constructSolution( Node c ){
@@ -1839,7 +1866,7 @@ Node CegConjecturePbe::constructSolution(
       {
         // could be conditionally solved
         std::vector<Node> subsumed_by;
-        einfo.d_term_trie.getSubsumedBy(this, x.d_vals, true, subsumed_by);
+        einfo.d_term_trie.getSubsumedBy(x.d_vals, true, subsumed_by);
         if (!subsumed_by.empty())
         {
           ret_dt = constructBestSolvedTerm(subsumed_by, x);
@@ -2016,7 +2043,7 @@ Node CegConjecturePbe::constructSolution(
         // get an eligible strategy index
         unsigned sindex = 0;
         while (sindex < snode.d_strats.size()
-               && !x.isValidStrategy(snode.d_strats[sindex]))
+               && !snode.d_strats[sindex]->isValid(this, x))
         {
           sindex++;
         }
@@ -2117,7 +2144,6 @@ Node CegConjecturePbe::constructSolution(
                     Node cond = einfo_child.d_enum_vals[k];
                     std::vector<Node> solved;
                     itnt->second.d_term_trie.getSubsumedBy(
-                        this,
                         einfo_child.d_enum_vals_res[k],
                         branch_pol,
                         solved);
@@ -2145,8 +2171,7 @@ Node CegConjecturePbe::constructSolution(
             // distinguishable
             std::map<int, std::vector<Node> > possible_cond;
             std::map<Node, int> solved_cond;  // stores branch
-            einfo_child.d_term_trie.getLeaves(
-                this, x.d_vals, true, possible_cond);
+            einfo_child.d_term_trie.getLeaves(x.d_vals, true, possible_cond);
 
             std::map<int, std::vector<Node> >::iterator itpc =
                 possible_cond.find(0);
@@ -2289,14 +2314,34 @@ Node CegConjecturePbe::constructSolution(
   return ret_dt;
 }
 
+bool CegConjecturePbe::EnumTypeInfoStrat::isValid(CegConjecturePbe* pbe,
+                                                  UnifContext& x)
+{
+  if ((x.d_has_string_pos == role_string_prefix
+       && d_this == strat_CONCAT_SUFFIX)
+      || (x.d_has_string_pos == role_string_suffix
+          && d_this == strat_CONCAT_PREFIX))
+  {
+    return false;
+  }
+  return true;
+}
+
+CegConjecturePbe::UnifContext::UnifContext() : d_has_string_pos(role_invalid)
+{
+  d_true = NodeManager::currentNM()->mkConst(true);
+  d_false = NodeManager::currentNM()->mkConst(false);
+}
+
 bool CegConjecturePbe::UnifContext::updateContext( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol ) {
   Assert( d_vals.size()==vals.size() );
   bool changed = false;
-  Node poln = pol ? pbe->d_true : pbe->d_false;
+  Node poln = pol ? d_true : d_false;
   for( unsigned i=0; i<vals.size(); i++ ){
     if( vals[i]!=poln ){
-      if( d_vals[i]==pbe->d_true ){
-        d_vals[i] = pbe->d_false;
+      if (d_vals[i] == d_true)
+      {
+        d_vals[i] = d_false;
         changed = true;
       }
     }
@@ -2332,20 +2377,6 @@ bool CegConjecturePbe::UnifContext::isReturnValueModified() {
   return false;
 }
 
-bool CegConjecturePbe::UnifContext::isValidStrategy(EnumTypeInfoStrat* etis)
-{
-  StrategyType st = etis->d_this;
-  if (d_has_string_pos == role_string_prefix && st == strat_CONCAT_SUFFIX)
-  {
-    return false;
-  }
-  if (d_has_string_pos == role_string_suffix && st == strat_CONCAT_PREFIX)
-  {
-    return false;
-  }
-  return true;
-}
-
 void CegConjecturePbe::UnifContext::initialize( CegConjecturePbe * pbe, Node c ) {
   Assert( d_vals.empty() );
   Assert( d_str_pos.empty() );
@@ -2354,7 +2385,7 @@ void CegConjecturePbe::UnifContext::initialize( CegConjecturePbe * pbe, Node c )
   Assert( pbe->d_examples.find( c )!=pbe->d_examples.end() );
   unsigned sz = pbe->d_examples[c].size();
   for( unsigned i=0; i<sz; i++ ){
-    d_vals.push_back( pbe->d_true );
+    d_vals.push_back(d_true);
   }
   
   if( !pbe->d_examples_out[c].empty() ){
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h
index 2b800db81..38a170fbe 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.h
+++ b/src/theory/quantifiers/sygus/sygus_pbe.h
@@ -322,37 +322,73 @@ class CegConjecturePbe : public SygusModule
   //--------------------------------- end PBE search values
 
   // -------------------------------- decision tree learning
-  // index filter
-  class IndexFilter {
-  public:
-    IndexFilter(){}
-    void mk( std::vector< Node >& vals, bool pol = true );
-    std::map< unsigned, unsigned > d_next;
-    unsigned start();
-    unsigned next( unsigned i );
-    void clear() { d_next.clear(); }
-    bool isEq( std::vector< Node >& vs, Node v );
-  };
-  // subsumption trie
-  class SubsumeTrie {
-  public:
-    SubsumeTrie(){}
-    // adds term to the trie, removes based on subsumption
-    Node addTerm( CegConjecturePbe * pbe, Node t, std::vector< Node >& vals, bool pol, std::vector< Node >& subsumed, IndexFilter * f = NULL );
-    // adds condition to the trie (does not do subsumption)
-    Node addCond( CegConjecturePbe * pbe, Node c, std::vector< Node >& vals, bool pol, IndexFilter * f = NULL );
-    // returns the set of terms that are subsets of vals
-    void getSubsumed( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::vector< Node >& subsumed, IndexFilter * f = NULL );
-    // returns the set of terms that are supersets of vals
-    void getSubsumedBy( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::vector< Node >& subsumed_by, IndexFilter * f = NULL );
-    // v[-1,1,0] -> children always false, always true, both
-    void getLeaves( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::map< int, std::vector< Node > >& v, IndexFilter * f = NULL );
+  /** Subsumption trie
+  *
+  * This class manages a set of terms for a PBE sygus enumerator.
+  *
+  * In PBE sygus, we are interested in, for each term t, the set of I/O examples
+  * that it satisfies, which can be represented by a vector of Booleans.
+  * For example, given conjecture:
+  *   f( 1 ) = 2 ^ f( 3 ) = 4 ^ f( -1 ) = 1 ^ f( 5 ) = 5
+  * If solutions for f are of the form (lambda x. [term]), then:
+  *   Term x satisfies 0001,
+  *   Term x+1 satisfies 1100,
+  *   Term 2 satisfies 0100.
+  * Above, term 2 is subsumed by term x+1, since the set of I/O examples that
+  * x+1 satisfies are a superset of those satisfied by 2.
+  */
+  class SubsumeTrie
+  {
+   public:
+    SubsumeTrie() {}
+    /**
+    * Adds term t to the trie, removes all terms that are subsumed by t from the
+    * trie and adds them to subsumed. The set of I/O examples that t satisfies
+    * is given by (pol ? vals : !vals).
+    */
+    Node addTerm(Node t,
+                 const std::vector<Node>& vals,
+                 bool pol,
+                 std::vector<Node>& subsumed);
+    /**
+    * Adds term c to the trie, without calculating/updating based on
+    * subsumption. This is useful for using this class to store conditionals
+    * in ITE strategies, where any conditional whose set of vals is unique
+    * (as opposed to not subsumed) is useful.
+    */
+    Node addCond(Node c, const std::vector<Node>& vals, bool pol);
+    /**
+     * Returns the set of terms that are subsumed by (pol ? vals : !vals).
+     */
+    void getSubsumed(const std::vector<Node>& vals,
+                     bool pol,
+                     std::vector<Node>& subsumed);
+    /**
+     * Returns the set of terms that subsume (pol ? vals : !vals). This
+     * is for instance useful when determining whether there exists a term
+     * that satisfies all active examples in the decision tree learning
+     * algorithm.
+     */
+    void getSubsumedBy(const std::vector<Node>& vals,
+                       bool pol,
+                       std::vector<Node>& subsumed_by);
+    /**
+    * Get the leaves of the trie, which we store in the map v.
+    * v[-1] stores the children that always evaluate to !pol,
+    * v[1] stores the children that always evaluate to pol,
+    * v[0] stores the children that both evaluate to true and false for at least
+    * one example.
+    */
+    void getLeaves(const std::vector<Node>& vals,
+                   bool pol,
+                   std::map<int, std::vector<Node> >& v);
     /** is this trie empty? */
     bool isEmpty() { return d_term.isNull() && d_children.empty(); }
     /** clear this trie */
-    void clear() {
+    void clear()
+    {
       d_term = Node::null();
-      d_children.clear(); 
+      d_children.clear();
     }
 
    private:
@@ -361,40 +397,43 @@ class CegConjecturePbe : public SygusModule
     /** the children nodes of this trie */
     std::map<Node, SubsumeTrie> d_children;
     /** helper function for above functions */
-    Node addTermInternal(CegConjecturePbe* pbe,
-                         Node t,
-                         std::vector<Node>& vals,
+    Node addTermInternal(Node t,
+                         const std::vector<Node>& vals,
                          bool pol,
                          std::vector<Node>& subsumed,
                          bool spol,
-                         IndexFilter* f,
                          unsigned index,
                          int status,
                          bool checkExistsOnly,
                          bool checkSubsume);
     /** helper function for above functions */
-    void getLeavesInternal(CegConjecturePbe* pbe,
-                           std::vector<Node>& vals,
+    void getLeavesInternal(const std::vector<Node>& vals,
                            bool pol,
                            std::map<int, std::vector<Node> >& v,
-                           IndexFilter* f,
                            unsigned index,
                            int status);
   };
   // -------------------------------- end decision tree learning
 
   //------------------------------ representation of a enumeration strategy
-
-  /** information about an enumerator
-   *
-   * We say an enumerator is a master enumerator if it is the variable that
-   * we use to enumerate values for its sort. Master enumerators may have
-   * (possibly multiple) slave enumerators, stored in d_enum_slave,
-   */
-  class EnumInfo {
+  /**
+  * This class stores information regarding an enumerator, including:
+  * - Information regarding the role of this enumerator (see EnumRole), its
+  * parent, whether it is templated, its slave enumerators, and so on, and
+  * - A database of values that have been enumerated for this enumerator.
+  *
+  * We say an enumerator is a master enumerator if it is the variable that
+  * we use to enumerate values for its sort. Master enumerators may have
+  * (possibly multiple) slave enumerators, stored in d_enum_slave. We make
+  * the first enumerator for each type a master enumerator, and any additional
+  * ones slaves of it.
+  */
+  class EnumInfo
+  {
    public:
     EnumInfo() : d_role(enum_io), d_is_conditional(false) {}
     /** initialize this class
+    *
     * c is the parent function-to-synthesize
     * role is the "role" the enumerator plays in the high-level strategy,
     *   which is one of enum_* above.
@@ -412,36 +451,78 @@ class CegConjecturePbe : public SygusModule
     void setConditional() { d_is_conditional = true; }
     /** is conditional */
     bool isConditional() { return d_is_conditional; }
-    void addEnumValue(CegConjecturePbe* pbe,
-                      Node v,
-                      std::vector<Node>& results);
-    void setSolved(Node slv);
-    bool isSolved() { return !d_enum_solved.isNull(); }
-    Node getSolved() { return d_enum_solved; }
+    /** get the role of this enumerator */
     EnumRole getRole() { return d_role; }
+    /**
+    * The candidate variable that this enumerator is for (see sygus_pbe.h).
+    */
     Node d_parent_candidate;
-    // for template
+    /** enumerator template
+    *
+    * If d_template non-null, enumerated values V are immediately transformed to
+    * d_template { d_template_arg -> V }.
+    */
     Node d_template;
     Node d_template_arg;
-
+    /**
+    * The active guard of this enumerator (see
+    * TermDbSygus::d_enum_to_active_guard).
+    */
     Node d_active_guard;
+    /**
+    * Slave enumerators of this enumerator. These are other enumerators that
+    * have the same type, but a different role in the strategy tree. We
+    * generally
+    * only use one enumerator per type, and hence these slaves are notified when
+    * values are enumerated for this enumerator.
+    */
     std::vector<Node> d_enum_slave;
-    /** values we have enumerated */
+
+    //---------------------------enumerated values
+    /**
+    * Notify this class that the term v has been enumerated for this enumerator.
+    * Its evaluation under the set of examples in pbe are stored in results.
+    */
+    void addEnumValue(CegConjecturePbe* pbe,
+                      Node v,
+                      std::vector<Node>& results);
+    /**
+    * Notify this class that slv is the complete solution to the synthesis
+    * conjecture. This occurs rarely, for instance, when during an ITE strategy
+    * we find that a single enumerated term covers all examples.
+    */
+    void setSolved(Node slv);
+    /** Have we been notified that a complete solution exists? */
+    bool isSolved() { return !d_enum_solved.isNull(); }
+    /** Get the complete solution to the synthesis conjecture. */
+    Node getSolved() { return d_enum_solved; }
+    /** Values that have been enumerated for this enumerator */
     std::vector<Node> d_enum_vals;
     /**
       * This either stores the values of f( I ) for inputs
       * or the value of f( I ) = O if d_role==enum_io
       */
     std::vector<std::vector<Node> > d_enum_vals_res;
+    /**
+    * The set of values in d_enum_vals that have been "subsumed" by others
+    * (see SubsumeTrie for explanation of subsumed).
+    */
     std::vector<Node> d_enum_subsume;
+    /** Map from values to their index in d_enum_vals. */
     std::map<Node, unsigned> d_enum_val_to_index;
+    /**
+    * A subsumption trie containing the values in d_enum_vals. Depending on the
+    * role of this enumerator, values may either be added to d_term_trie with
+    * subsumption (if role=enum_io), or without (if role=enum_ite_condition or
+    * enum_concat_term).
+    */
     SubsumeTrie d_term_trie;
-
+    //---------------------------end enumerated values
    private:
     /**
-     * Whether an enumerated value for this conjecture has solved the entire
-     * conjecture.
-     */
+      * Whether an enumerated value for this conjecture has solved the entire
+      * conjecture.
+      */
     Node d_enum_solved;
     /** the role of this enumerator (one of enum_* above). */
     EnumRole d_role;
@@ -452,37 +533,7 @@ class CegConjecturePbe : public SygusModule
   std::map< Node, EnumInfo > d_einfo;
 
   class CandidateInfo;
-
-  /** represents a strategy for a SyGuS datatype type
-   *
-   * This represents a possible strategy to apply when processing a strategy
-   * node in constructSolution. When applying the strategy represented by this
-   * class, we may make recursive calls to the children of the strategy,
-   * given in d_cenum. If all recursive calls to constructSolution are
-   * successful, say:
-   *   constructSolution( c, d_cenum[1], ... ) = t1,
-   *    ...,
-   *   constructSolution( c, d_cenum[n], ... ) = tn,
-   * Then, the solution returned by this strategy is
-   *   d_sol_templ * { d_sol_templ_args -> (t1,...,tn) }
-   */
-  class EnumTypeInfoStrat {
-   public:
-    /** the type of strategy this represents */
-    StrategyType d_this;
-    /** the sygus datatype constructor that induced this strategy
-     *
-     * For example, this may be a sygus datatype whose sygus operator is ITE,
-     * if the strategy type above is strat_ITE.
-     */
-    Node d_cons;
-    /** children of this strategy */
-    std::vector<std::pair<Node, NodeRole> > d_cenum;
-    /** the arguments for the (templated) solution */
-    std::vector<Node> d_sol_templ_args;
-    /** the template for the solution */
-    Node d_sol_templ;
-  };
+  class EnumTypeInfoStrat;
 
   /** represents a node in the strategy graph
    *
@@ -636,31 +687,40 @@ class CegConjecturePbe : public SygusModule
   //------------------------------ end strategy registration
 
   //------------------------------ constructing solutions
-  class UnifContext {
-  public:
-   UnifContext() : d_has_string_pos(role_invalid) {}
-   /** this intiializes this context for function-to-synthesize c */
-   void initialize(CegConjecturePbe* pbe, Node c);
+  /** Unification context
+   *
+   * This class maintains state information during calls to
+   * CegConjecturePbe::constructSolution, which implements unification-based
+   * approaches for construction solutions to synthesis conjectures.
+   */
+  class UnifContext
+  {
+   public:
+    UnifContext();
+    /** this intiializes this context for function-to-synthesize c */
+    void initialize(CegConjecturePbe* pbe, Node c);
 
-   //----------for ITE strategy
-   /** the value of the context conditional
+    //----------for ITE strategy
+    /** the value of the context conditional
     *
     * This stores a list of Boolean constants that is the same length of the
     * number of input/output example pairs we are considering. For each i,
     * if d_vals[i] = true, i/o pair #i is active according to this context
     * if d_vals[i] = false, i/o pair #i is inactive according to this context
     */
-   std::vector<Node> d_vals;
-   /** update the examples
+    std::vector<Node> d_vals;
+    /** update the examples
     *
     * if pol=true, this method updates d_vals to d_vals & vals
     * if pol=false, this method updates d_vals to d_vals & ( ~vals )
     */
-   bool updateContext(CegConjecturePbe* pbe, std::vector<Node>& vals, bool pol);
-   //----------end for ITE strategy
+    bool updateContext(CegConjecturePbe* pbe,
+                       std::vector<Node>& vals,
+                       bool pol);
+    //----------end for ITE strategy
 
-   //----------for CONCAT strategies
-   /** the position in the strings
+    //----------for CONCAT strategies
+    /** the position in the strings
     *
     * For each i/o example pair, this stores the length of the current solution
     * for the input of the pair, where the solution for that input is a prefix
@@ -673,30 +733,31 @@ class CegConjecturePbe : public SygusModule
     *   str.++( "abc", "c" ) is a prefix of "abcdcd" and
     *   str.++( "aa", "c" ) is a prefix of "aacd".
     */
-   std::vector<unsigned> d_str_pos;
-   /** has string position
+    std::vector<unsigned> d_str_pos;
+    /** has string position
     *
     * Whether the solution positions indicate a prefix or suffix of the output
     * examples. If this is role_invalid, then we have not updated the string
     * position.
     */
-   NodeRole d_has_string_pos;
-   /** update the string examples
+    NodeRole d_has_string_pos;
+    /** update the string examples
     *
     * This method updates d_str_pos to d_str_pos + pos.
     */
-   bool updateStringPosition(CegConjecturePbe* pbe, std::vector<unsigned>& pos);
-   /** get current strings
+    bool updateStringPosition(CegConjecturePbe* pbe,
+                              std::vector<unsigned>& pos);
+    /** get current strings
     *
     * This returns the prefix/suffix of the string constants stored in vals
     * of size d_str_pos, and stores the result in ex_vals. For example, if vals
     * is (abcdcd", "aacde") and d_str_pos = ( 5, 3 ), then we add
     * "d" and "de" to ex_vals.
     */
-   void getCurrentStrings(CegConjecturePbe* pbe,
-                          const std::vector<Node>& vals,
-                          std::vector<String>& ex_vals);
-   /** get string increment
+    void getCurrentStrings(CegConjecturePbe* pbe,
+                           const std::vector<Node>& vals,
+                           std::vector<String>& ex_vals);
+    /** get string increment
     *
     * If this method returns true, then inc and tot are updated such that
     *   for all active indices i,
@@ -706,40 +767,38 @@ class CegConjecturePbe : public SygusModule
     * We set tot to the sum of inc[i] for i=1,...,n. This indicates the total
     * number of characters incremented across all examples.
     */
-   bool getStringIncrement(CegConjecturePbe* pbe,
-                           bool isPrefix,
-                           const std::vector<String>& ex_vals,
-                           const std::vector<Node>& vals,
-                           std::vector<unsigned>& inc,
-                           unsigned& tot);
-   /** returns true if ex_vals[i] = vals[i] for all active indices i. */
-   bool isStringSolved(CegConjecturePbe* pbe,
-                       const std::vector<String>& ex_vals,
-                       const std::vector<Node>& vals);
-   //----------end for CONCAT strategies
-
-   /** is return value modified?
+    bool getStringIncrement(CegConjecturePbe* pbe,
+                            bool isPrefix,
+                            const std::vector<String>& ex_vals,
+                            const std::vector<Node>& vals,
+                            std::vector<unsigned>& inc,
+                            unsigned& tot);
+    /** returns true if ex_vals[i] = vals[i] for all active indices i. */
+    bool isStringSolved(CegConjecturePbe* pbe,
+                        const std::vector<String>& ex_vals,
+                        const std::vector<Node>& vals);
+    //----------end for CONCAT strategies
+
+    /** is return value modified?
     *
     * This returns true if we are currently in a state where the return value
     * of the solution has been modified, e.g. by a previous node that solved
     * for a prefix.
     */
-   bool isReturnValueModified();
-   /** returns true if argument is valid strategy in this context */
-   bool isValidStrategy(EnumTypeInfoStrat* etis);
-   /** visited role
+    bool isReturnValueModified();
+    /** visited role
     *
     * This is the current set of enumerator/node role pairs we are currently
     * visiting. This set is cleared when the context is updated.
     */
-   std::map<Node, std::map<NodeRole, bool> > d_visit_role;
-
-   /** unif context enumerator information */
-   class UEnumInfo
-   {
-    public:
-     UEnumInfo() {}
-     /** map from conditions and branch positions to a solved node
+    std::map<Node, std::map<NodeRole, bool> > d_visit_role;
+
+    /** unif context enumerator information */
+    class UEnumInfo
+    {
+     public:
+      UEnumInfo() {}
+      /** map from conditions and branch positions to a solved node
       *
       * For example, if we have:
       *   f( 1 ) = 2 ^ f( 3 ) = 4 ^ f( -1 ) = 1
@@ -752,10 +811,15 @@ class CegConjecturePbe : public SygusModule
       * resulting in 2 and 4, are equal to the output value for the respective
       * pairs.
       */
-     std::map<Node, std::map<unsigned, Node> > d_look_ahead_sols;
+      std::map<Node, std::map<unsigned, Node> > d_look_ahead_sols;
     };
     /** map from enumerators to the above info class */
-    std::map< Node, UEnumInfo > d_uinfo;
+    std::map<Node, UEnumInfo> d_uinfo;
+
+   private:
+    /** true and false nodes */
+    Node d_true;
+    Node d_false;
   };
 
   /** construct solution
@@ -799,6 +863,41 @@ class CegConjecturePbe : public SygusModule
                                     std::map< Node, std::vector< unsigned > > incr,
                                     UnifContext& x );
   //------------------------------ end constructing solutions
+
+  /** represents a strategy for a SyGuS datatype type
+   *
+   * This represents a possible strategy to apply when processing a strategy
+   * node in constructSolution. When applying the strategy represented by this
+   * class, we may make recursive calls to the children of the strategy,
+   * given in d_cenum. If all recursive calls to constructSolution for these
+   * children are successful, say:
+   *   constructSolution( c, d_cenum[1], ... ) = t1,
+   *    ...,
+   *   constructSolution( c, d_cenum[n], ... ) = tn,
+   * Then, the solution returned by this strategy is
+   *   d_sol_templ * { d_sol_templ_args -> (t1,...,tn) }
+   * where * is application of substitution.
+   */
+  class EnumTypeInfoStrat
+  {
+   public:
+    /** the type of strategy this represents */
+    StrategyType d_this;
+    /** the sygus datatype constructor that induced this strategy
+     *
+     * For example, this may be a sygus datatype whose sygus operator is ITE,
+     * if the strategy type above is strat_ITE.
+     */
+    Node d_cons;
+    /** children of this strategy */
+    std::vector<std::pair<Node, NodeRole> > d_cenum;
+    /** the arguments for the (templated) solution */
+    std::vector<Node> d_sol_templ_args;
+    /** the template for the solution */
+    Node d_sol_templ;
+    /** Returns true if argument is valid strategy in context x */
+    bool isValid(CegConjecturePbe* pbe, UnifContext& x);
+  };
 };
 
 }/* namespace CVC4::theory::quantifiers */