Refactor default grammars construction (#2681)

2 files changed, 208 insertions, 173 deletions

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 47c701cf6..d6dfb3d26 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -374,18 +374,24 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type,
   // TODO #1178 : add other missing types
 }
 
-void CegGrammarConstructor::collectSygusGrammarTypesFor( TypeNode range, std::vector< TypeNode >& types, std::map< TypeNode, std::vector< DatatypeConstructorArg > >& sels ){
+void CegGrammarConstructor::collectSygusGrammarTypesFor(
+    TypeNode range, std::vector<TypeNode>& types)
+{
   if( !range.isBoolean() ){
     if( std::find( types.begin(), types.end(), range )==types.end() ){
       Trace("sygus-grammar-def") << "...will make grammar for " << range << std::endl;
       types.push_back( range );
       if( range.isDatatype() ){
-        const Datatype& dt = ((DatatypeType)range.toType()).getDatatype();
-        for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-          for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
-            TypeNode crange = TypeNode::fromType( ((SelectorType)dt[i][j].getType()).getRangeType() );
-            sels[crange].push_back( dt[i][j] );
-            collectSygusGrammarTypesFor( crange, types, sels );
+        const Datatype& dt = range.getDatatype();
+        for (unsigned i = 0, size = dt.getNumConstructors(); i < size; ++i)
+        {
+          for (unsigned j = 0, size_args = dt[i].getNumArgs(); j < size_args;
+               ++j)
+          {
+            collectSygusGrammarTypesFor(
+                TypeNode::fromType(static_cast<SelectorType>(dt[i][j].getType())
+                                       .getRangeType()),
+                types);
           }
         }
       }
@@ -408,76 +414,87 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
                              << range << std::endl;
   // collect the variables
   std::vector<Node> sygus_vars;
-  if( !bvl.isNull() ){
-    for( unsigned i=0; i<bvl.getNumChildren(); i++ ){
+  if (!bvl.isNull())
+  {
+    for (unsigned i = 0, size = bvl.getNumChildren(); i < size; ++i)
+    {
       if (term_irrelevant.find(bvl[i]) == term_irrelevant.end())
       {
         sygus_vars.push_back(bvl[i]);
       }
       else
       {
-        Trace("sygus-grammar-def") << "...synth var " << bvl[i]
-                                   << " has been marked irrelevant."
-                                   << std::endl;
+        Trace("sygus-grammar-def")
+            << "...synth var " << bvl[i] << " has been marked irrelevant."
+            << std::endl;
       }
     }
   }
-  //if( !range.isBoolean() && !range.isInteger() && !range.isBitVector() && !range.isDatatype() ){
-  //  parseError("No default grammar for type.");
-  //}
-  std::vector< std::vector< Expr > > ops;
+  // operators for each constructor in type
+  std::vector<std::vector<Expr>> ops;
+  // names for the operators
+  std::vector<std::vector<std::string>> cnames;
+  // argument types of operators
+  std::vector<std::vector<std::vector<Type>>> cargs;
+  // set of callbacks for each constructor
+  std::vector<std::vector<std::shared_ptr<SygusPrintCallback>>> pcs;
+  // weights for each constructor
+  std::vector<std::vector<int>> weights;
+  // index of top datatype, i.e. the datatype for the range type
   int startIndex = -1;
   std::map< Type, Type > sygus_to_builtin;
 
-  std::vector< TypeNode > types;
-  std::map< TypeNode, std::vector< DatatypeConstructorArg > > sels;
-  //types for each of the variables of parametric sort
-  for( unsigned i=0; i<sygus_vars.size(); i++ ){
-    collectSygusGrammarTypesFor( sygus_vars[i].getType(), types, sels );
+  std::vector<TypeNode> types;
+  // collect connected types for each of the variables
+  for (unsigned i = 0, size = sygus_vars.size(); i < size; ++i)
+  {
+    collectSygusGrammarTypesFor(sygus_vars[i].getType(), types);
   }
-  //types connected to range
-  collectSygusGrammarTypesFor( range, types, sels );
+  // collect connected types to range
+  collectSygusGrammarTypesFor(range, types);
 
-  //name of boolean sort
+  // create placeholder for boolean type (kept apart since not collected)
   std::stringstream ssb;
   ssb << fun << "_Bool";
   std::string dbname = ssb.str();
   Type unres_bt = mkUnresolvedType(ssb.str(), unres).toType();
 
+  // create placeholders for collected types
   std::vector< Type > unres_types;
   std::map< TypeNode, Type > type_to_unres;
-  for( unsigned i=0; i<types.size(); i++ ){
+  for (unsigned i = 0, size = types.size(); i < size; ++i)
+  {
     std::stringstream ss;
     ss << fun << "_" << types[i];
     std::string dname = ss.str();
     datatypes.push_back(Datatype(dname));
     ops.push_back(std::vector< Expr >());
+    cnames.push_back(std::vector<std::string>());
+    cargs.push_back(std::vector<std::vector<Type>>());
+    pcs.push_back(std::vector<std::shared_ptr<SygusPrintCallback>>());
+    weights.push_back(std::vector<int>());
     //make unresolved type
     Type unres_t = mkUnresolvedType(dname, unres).toType();
     unres_types.push_back(unres_t);
     type_to_unres[types[i]] = unres_t;
     sygus_to_builtin[unres_t] = types[i].toType();
   }
-  for( unsigned i=0; i<types.size(); i++ ){
+  for (unsigned i = 0, size = types.size(); i < size; ++i)
+  {
     Trace("sygus-grammar-def") << "Make grammar for " << types[i] << " " << unres_types[i] << std::endl;
-    std::vector<std::string> cnames;
-    std::vector<std::vector<CVC4::Type> > cargs;
-    /* Print callbacks for each constructor */
-    std::vector<std::shared_ptr<SygusPrintCallback>> pcs;
-    /* Weights for each constructor */
-    std::vector<int> weights;
     Type unres_t = unres_types[i];
     //add variables
-    for( unsigned j=0; j<sygus_vars.size(); j++ ){
+    for (unsigned j = 0, size_j = sygus_vars.size(); j < size_j; ++j)
+    {
       if( sygus_vars[j].getType()==types[i] ){
         std::stringstream ss;
         ss << sygus_vars[j];
         Trace("sygus-grammar-def") << "...add for variable " << ss.str() << std::endl;
         ops[i].push_back( sygus_vars[j].toExpr() );
-        cnames.push_back( ss.str() );
-        cargs.push_back( std::vector< CVC4::Type >() );
-        pcs.push_back(nullptr);
-        weights.push_back(-1);
+        cnames[i].push_back(ss.str());
+        cargs[i].push_back(std::vector<Type>());
+        pcs[i].push_back(nullptr);
+        weights[i].push_back(-1);
       }
     }
     //add constants
@@ -486,33 +503,35 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     std::map< TypeNode, std::vector< Node > >::iterator itec = extra_cons.find( types[i] );
     if( itec!=extra_cons.end() ){
       //consts.insert( consts.end(), itec->second.begin(), itec->second.end() );
-      for( unsigned j=0; j<itec->second.size(); j++ ){
+      for (unsigned j = 0, size_j = itec->second.size(); j < size_j; ++j)
+      {
         if( std::find( consts.begin(), consts.end(), itec->second[j] )==consts.end() ){
           consts.push_back( itec->second[j] );
         }
       }
     }
-    for( unsigned j=0; j<consts.size(); j++ ){
+    for (unsigned j = 0, size_j = consts.size(); j < size_j; ++j)
+    {
       std::stringstream ss;
       ss << consts[j];
       Trace("sygus-grammar-def") << "...add for constant " << ss.str() << std::endl;
       ops[i].push_back( consts[j].toExpr() );
-      cnames.push_back( ss.str() );
-      cargs.push_back( std::vector< CVC4::Type >() );
-      pcs.push_back(nullptr);
-      weights.push_back(-1);
+      cnames[i].push_back(ss.str());
+      cargs[i].push_back(std::vector<Type>());
+      pcs[i].push_back(nullptr);
+      weights[i].push_back(-1);
     }
-    //ITE
-    CVC4::Kind k = kind::ITE;
+    // ITE
+    Kind k = ITE;
     Trace("sygus-grammar-def") << "...add for " << k << std::endl;
     ops[i].push_back(nm->operatorOf(k).toExpr());
-    cnames.push_back( kind::kindToString(k) );
-    cargs.push_back( std::vector< CVC4::Type >() );
-    cargs.back().push_back(unres_bt);
-    cargs.back().push_back(unres_t);
-    cargs.back().push_back(unres_t);
-    pcs.push_back(nullptr);
-    weights.push_back(-1);
+    cnames[i].push_back(kindToString(k));
+    cargs[i].push_back(std::vector<Type>());
+    cargs[i].back().push_back(unres_bt);
+    cargs[i].back().push_back(unres_t);
+    cargs[i].back().push_back(unres_t);
+    pcs[i].push_back(nullptr);
+    weights[i].push_back(-1);
 
     if (types[i].isReal())
     {
@@ -521,16 +540,17 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
         Kind k = j == 0 ? PLUS : MINUS;
         Trace("sygus-grammar-def") << "...add for " << k << std::endl;
         ops[i].push_back(nm->operatorOf(k).toExpr());
-        cnames.push_back(kind::kindToString(k));
-        cargs.push_back(std::vector<CVC4::Type>());
-        cargs.back().push_back(unres_t);
-        cargs.back().push_back(unres_t);
-        pcs.push_back(nullptr);
-        weights.push_back(-1);
+        cnames[i].push_back(kindToString(k));
+        cargs[i].push_back(std::vector<Type>());
+        cargs[i].back().push_back(unres_t);
+        cargs[i].back().push_back(unres_t);
+        pcs[i].push_back(nullptr);
+        weights[i].push_back(-1);
       }
       if (!types[i].isInteger())
       {
-        Trace("sygus-grammar-def") << "...Dedicate to Real\n";
+        Trace("sygus-grammar-def")
+            << "  ...create auxiliary Positive Integers grammar\n";
         /* Creating type for positive integers */
         std::stringstream ss;
         ss << fun << "_PosInt";
@@ -546,7 +566,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
         /* Add operator 1 */
         Trace("sygus-grammar-def") << "\t...add for 1 to Pos_Int\n";
         ops_pos_int.push_back(nm->mkConst(Rational(1)).toExpr());
-        ss << "_1";
+        ss.str("");
+        ss << "1";
         cnames_pos_int.push_back(ss.str());
         cargs_pos_int.push_back(std::vector<Type>());
         /* Add operator PLUS */
@@ -558,23 +579,23 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
         cargs_pos_int.back().push_back(unres_pos_int_t);
         cargs_pos_int.back().push_back(unres_pos_int_t);
         datatypes.back().setSygus(types[i].toType(), bvl.toExpr(), true, true);
-        for (unsigned j = 0; j < ops_pos_int.size(); j++)
+        for (unsigned j = 0, size_j = ops_pos_int.size(); j < size_j; ++j)
         {
           datatypes.back().addSygusConstructor(
               ops_pos_int[j], cnames_pos_int[j], cargs_pos_int[j]);
         }
         Trace("sygus-grammar-def")
-            << "...built datatype " << datatypes.back() << " ";
+            << "  ...built datatype " << datatypes.back() << " ";
         /* Adding division at root */
         k = DIVISION;
         Trace("sygus-grammar-def") << "\t...add for " << k << std::endl;
         ops[i].push_back(nm->operatorOf(k).toExpr());
-        cnames.push_back(kindToString(k));
-        cargs.push_back(std::vector<Type>());
-        cargs.back().push_back(unres_t);
-        cargs.back().push_back(unres_pos_int_t);
-        pcs.push_back(nullptr);
-        weights.push_back(-1);
+        cnames[i].push_back(kindToString(k));
+        cargs[i].push_back(std::vector<Type>());
+        cargs[i].back().push_back(unres_t);
+        cargs[i].back().push_back(unres_pos_int_t);
+        pcs[i].push_back(nullptr);
+        weights[i].push_back(-1);
       }
     }
     else if (types[i].isBitVector())
@@ -585,11 +606,11 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       {
         Trace("sygus-grammar-def") << "...add for " << k << std::endl;
         ops[i].push_back(nm->operatorOf(k).toExpr());
-        cnames.push_back(kindToString(k));
-        cargs.push_back(std::vector<Type>());
-        cargs.back().push_back(unres_t);
-        pcs.push_back(nullptr);
-        weights.push_back(-1);
+        cnames[i].push_back(kindToString(k));
+        cargs[i].push_back(std::vector<Type>());
+        cargs[i].back().push_back(unres_t);
+        pcs[i].push_back(nullptr);
+        weights[i].push_back(-1);
       }
       // binary apps
       std::vector<Kind> bin_kinds = {BITVECTOR_AND,
@@ -609,56 +630,65 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       {
         Trace("sygus-grammar-def") << "...add for " << k << std::endl;
         ops[i].push_back(nm->operatorOf(k).toExpr());
-        cnames.push_back(kindToString(k));
-        cargs.push_back(std::vector<Type>());
-        cargs.back().push_back(unres_t);
-        cargs.back().push_back(unres_t);
-        pcs.push_back(nullptr);
-        weights.push_back(-1);
+        cnames[i].push_back(kindToString(k));
+        cargs[i].push_back(std::vector<Type>());
+        cargs[i].back().push_back(unres_t);
+        cargs[i].back().push_back(unres_t);
+        pcs[i].push_back(nullptr);
+        weights[i].push_back(-1);
       }
     }
     else if (types[i].isDatatype())
     {
       Trace("sygus-grammar-def") << "...add for constructors" << std::endl;
-      const Datatype& dt = ((DatatypeType)types[i].toType()).getDatatype();
-      for( unsigned k=0; k<dt.getNumConstructors(); k++ ){
+      const Datatype& dt = types[i].getDatatype();
+      for (unsigned k = 0, size_k = dt.getNumConstructors(); k < size_k; ++k)
+      {
         Trace("sygus-grammar-def") << "...for " << dt[k].getName() << std::endl;
         ops[i].push_back( dt[k].getConstructor() );
-        cnames.push_back( dt[k].getName() );
-        cargs.push_back( std::vector< CVC4::Type >() );
-        for( unsigned j=0; j<dt[k].getNumArgs(); j++ ){
-          TypeNode crange = TypeNode::fromType( ((SelectorType)dt[k][j].getType()).getRangeType() );
-          //Assert( type_to_unres.find(crange)!=type_to_unres.end() );
-          cargs.back().push_back( type_to_unres[crange] );
+        cnames[i].push_back(dt[k].getName());
+        cargs[i].push_back(std::vector<Type>());
+        Trace("sygus-grammar-def") << "...add for selectors" << std::endl;
+        for (unsigned j = 0, size_j = dt[k].getNumArgs(); j < size_j; ++j)
+        {
+          Trace("sygus-grammar-def")
+              << "...for " << dt[k][j].getName() << std::endl;
+          TypeNode crange = TypeNode::fromType(
+              static_cast<SelectorType>(dt[k][j].getType()).getRangeType());
+          Assert(type_to_unres.find(crange) != type_to_unres.end());
+          cargs[i].back().push_back(type_to_unres[crange]);
+          // add to the selector type the selector operator
+
+          Assert(std::find(types.begin(), types.end(), crange) != types.end());
+          unsigned i_selType = std::distance(
+              types.begin(), std::find(types.begin(), types.end(), crange));
+          TypeNode arg_type = TypeNode::fromType(
+              static_cast<SelectorType>(dt[k][j].getType()).getDomain());
+          ops[i_selType].push_back(dt[k][j].getSelector());
+          cnames[i_selType].push_back(dt[k][j].getName());
+          cargs[i_selType].push_back(std::vector<Type>());
+          Assert(type_to_unres.find(arg_type) != type_to_unres.end());
+          cargs[i_selType].back().push_back(type_to_unres[arg_type]);
+          pcs[i_selType].push_back(nullptr);
+          weights[i_selType].push_back(-1);
         }
-        pcs.push_back(nullptr);
-        weights.push_back(-1);
+        pcs[i].push_back(nullptr);
+        weights[i].push_back(-1);
       }
     }else{
       std::stringstream sserr;
       sserr << "No implementation for default Sygus grammar of type " << types[i] << std::endl;
       throw LogicException(sserr.str());
     }
-    //add for all selectors to this type
-    if( !sels[types[i]].empty() ){
-      Trace("sygus-grammar-def") << "...add for selectors" << std::endl;
-      for( unsigned j=0; j<sels[types[i]].size(); j++ ){
-        Trace("sygus-grammar-def") << "...for " << sels[types[i]][j].getName() << std::endl;
-        TypeNode arg_type = TypeNode::fromType( ((SelectorType)sels[types[i]][j].getType()).getDomain() );
-        ops[i].push_back( sels[types[i]][j].getSelector() );
-        cnames.push_back( sels[types[i]][j].getName() );
-        cargs.push_back( std::vector< CVC4::Type >() );
-        //Assert( type_to_unres.find(arg_type)!=type_to_unres.end() );
-        cargs.back().push_back( type_to_unres[arg_type] );
-        pcs.push_back(nullptr);
-        weights.push_back(-1);
-      }
-    }
+  }
+  // make datatypes
+  for (unsigned i = 0, size = types.size(); i < size; ++i)
+  {
     Trace("sygus-grammar-def") << "...make datatype " << datatypes[i] << std::endl;
     datatypes[i].setSygus( types[i].toType(), bvl.toExpr(), true, true );
     std::map<TypeNode, std::vector<Node>>::iterator itexc =
         exc_cons.find(types[i]);
-    for (unsigned j = 0, size = ops[i].size(); j < size; j++)
+    for (unsigned j = 0, size = ops[i].size(); j < size; ++j)
     {
       // add the constructor if it is not excluded
       Node opn = Node::fromExpr(ops[i][j]);
@@ -667,12 +697,10 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
                  == itexc->second.end())
       {
         datatypes[i].addSygusConstructor(
-            ops[i][j], cnames[j], cargs[j], pcs[j], weights[j]);
+            ops[i][j], cnames[i][j], cargs[i][j], pcs[i][j], weights[i][j]);
       }
     }
-    Trace("sygus-grammar-def")
-        << "...built datatype " << datatypes[i] << " ";
-    //sorts.push_back( types[i] );
+    Trace("sygus-grammar-def") << "...built datatype " << datatypes[i] << " ";
     //set start index if applicable
     if( types[i]==range ){
       startIndex = i;
@@ -683,94 +711,96 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
   TypeNode btype = nm->booleanType();
   datatypes.push_back(Datatype(dbname));
   ops.push_back(std::vector<Expr>());
-  std::vector<std::string> cnames;
-  std::vector<std::vector< Type > > cargs;
-  /* Print callbacks for each constructor */
-  std::vector<std::shared_ptr<SygusPrintCallback>> pcs;
-  /* Weights for each constructor */
-  std::vector<int> weights;
+  cnames.push_back(std::vector<std::string>());
+  cargs.push_back(std::vector<std::vector<Type>>());
+  pcs.push_back(std::vector<std::shared_ptr<SygusPrintCallback>>());
+  weights.push_back(std::vector<int>());
   Trace("sygus-grammar-def") << "Make grammar for " << btype << " " << datatypes.back() << std::endl;
   //add variables
-  for( unsigned i=0; i<sygus_vars.size(); i++ ){
+  for (unsigned i = 0, size = sygus_vars.size(); i < size; ++i)
+  {
     if( sygus_vars[i].getType().isBoolean() ){
       std::stringstream ss;
       ss << sygus_vars[i];
       Trace("sygus-grammar-def") << "...add for variable " << ss.str() << std::endl;
       ops.back().push_back( sygus_vars[i].toExpr() );
-      cnames.push_back( ss.str() );
-      cargs.push_back( std::vector< CVC4::Type >() );
-      pcs.push_back(nullptr);
-      weights.push_back(1);
+      cnames.back().push_back(ss.str());
+      cargs.back().push_back(std::vector<Type>());
+      pcs.back().push_back(nullptr);
+      // make boolean variables weight as non-nullary constructors
+      weights.back().push_back(1);
     }
   }
-  //add constants
+  // add constants
   std::vector<Node> consts;
   mkSygusConstantsForType(btype, consts);
-  for (unsigned j = 0; j < consts.size(); j++)
+  for (unsigned i = 0, size = consts.size(); i < size; ++i)
   {
     std::stringstream ss;
-    ss << consts[j];
+    ss << consts[i];
     Trace("sygus-grammar-def") << "...add for constant " << ss.str()
                                << std::endl;
-    ops.back().push_back(consts[j].toExpr());
-    cnames.push_back(ss.str());
-    cargs.push_back(std::vector<CVC4::Type>());
-    pcs.push_back(nullptr);
-    weights.push_back(-1);
+    ops.back().push_back(consts[i].toExpr());
+    cnames.back().push_back(ss.str());
+    cargs.back().push_back(std::vector<Type>());
+    pcs.back().push_back(nullptr);
+    weights.back().push_back(-1);
   }
-  //add predicates for types
-  for( unsigned i=0; i<types.size(); i++ ){
+  // add predicates for types
+  for (unsigned i = 0, size = types.size(); i < size; ++i)
+  {
     Trace("sygus-grammar-def") << "...add predicates for " << types[i] << std::endl;
     //add equality per type
-    CVC4::Kind k = kind::EQUAL;
+    Kind k = EQUAL;
     Trace("sygus-grammar-def") << "...add for " << k << std::endl;
     ops.back().push_back(nm->operatorOf(k).toExpr());
     std::stringstream ss;
-    ss << kind::kindToString(k) << "_" << types[i];
-    cnames.push_back(ss.str());
-    cargs.push_back( std::vector< CVC4::Type >() );
-    cargs.back().push_back(unres_types[i]);
-    cargs.back().push_back(unres_types[i]);
-    pcs.push_back(nullptr);
-    weights.push_back(-1);
-    //type specific predicates
+    ss << kindToString(k) << "_" << types[i];
+    cnames.back().push_back(ss.str());
+    cargs.back().push_back(std::vector<Type>());
+    cargs.back().back().push_back(unres_types[i]);
+    cargs.back().back().push_back(unres_types[i]);
+    pcs.back().push_back(nullptr);
+    weights.back().push_back(-1);
+    // type specific predicates
     if (types[i].isReal())
     {
-      CVC4::Kind k = kind::LEQ;
+      Kind k = LEQ;
       Trace("sygus-grammar-def") << "...add for " << k << std::endl;
       ops.back().push_back(nm->operatorOf(k).toExpr());
-      cnames.push_back(kind::kindToString(k));
-      cargs.push_back( std::vector< CVC4::Type >() );
-      cargs.back().push_back(unres_types[i]);
-      cargs.back().push_back(unres_types[i]);
-      pcs.push_back(nullptr);
-      weights.push_back(-1);
+      cnames.back().push_back(kindToString(k));
+      cargs.back().push_back(std::vector<Type>());
+      cargs.back().back().push_back(unres_types[i]);
+      cargs.back().back().push_back(unres_types[i]);
+      pcs.back().push_back(nullptr);
+      weights.back().push_back(-1);
     }
     else if (types[i].isBitVector())
     {
       Kind k = BITVECTOR_ULT;
       Trace("sygus-grammar-def") << "...add for " << k << std::endl;
       ops.back().push_back(nm->operatorOf(k).toExpr());
-      cnames.push_back(kindToString(k));
-      cargs.push_back(std::vector<Type>());
-      cargs.back().push_back(unres_types[i]);
-      cargs.back().push_back(unres_types[i]);
-      pcs.push_back(nullptr);
-      weights.push_back(-1);
+      cnames.back().push_back(kindToString(k));
+      cargs.back().push_back(std::vector<Type>());
+      cargs.back().back().push_back(unres_types[i]);
+      cargs.back().back().push_back(unres_types[i]);
+      pcs.back().push_back(nullptr);
+      weights.back().push_back(-1);
     }
     else if (types[i].isDatatype())
     {
       //add for testers
       Trace("sygus-grammar-def") << "...add for testers" << std::endl;
-      const Datatype& dt = ((DatatypeType)types[i].toType()).getDatatype();
-      for( unsigned k=0; k<dt.getNumConstructors(); k++ ){
+      const Datatype& dt = types[i].getDatatype();
+      for (unsigned k = 0, size_k = dt.getNumConstructors(); k < size_k; ++k)
+      {
         Trace("sygus-grammar-def") << "...for " << dt[k].getTesterName() << std::endl;
         ops.back().push_back(dt[k].getTester());
-        cnames.push_back(dt[k].getTesterName());
-        cargs.push_back( std::vector< CVC4::Type >() );
-        cargs.back().push_back(unres_types[i]);
-        pcs.push_back(nullptr);
-        weights.push_back(-1);
+        cnames.back().push_back(dt[k].getTesterName());
+        cargs.back().push_back(std::vector<Type>());
+        cargs.back().back().push_back(unres_types[i]);
+        pcs.back().push_back(nullptr);
+        weights.back().push_back(-1);
       }
     }
   }
@@ -790,19 +820,19 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       }
       Trace("sygus-grammar-def") << "...add for " << k << std::endl;
       ops.back().push_back(nm->operatorOf(k).toExpr());
-      cnames.push_back(kindToString(k));
-      cargs.push_back(std::vector<CVC4::Type>());
-      cargs.back().push_back(unres_bt);
+      cnames.back().push_back(kindToString(k));
+      cargs.back().push_back(std::vector<Type>());
+      cargs.back().back().push_back(unres_bt);
       if (k != NOT)
       {
-        cargs.back().push_back(unres_bt);
+        cargs.back().back().push_back(unres_bt);
         if (k == ITE)
         {
-          cargs.back().push_back(unres_bt);
+          cargs.back().back().push_back(unres_bt);
         }
       }
-      pcs.push_back(nullptr);
-      weights.push_back(-1);
+      pcs.back().push_back(nullptr);
+      weights.back().push_back(-1);
     }
   }
   if( range==btype ){
@@ -810,15 +840,19 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
   }
   Trace("sygus-grammar-def") << "...make datatype " << datatypes.back() << std::endl;
   datatypes.back().setSygus( btype.toType(), bvl.toExpr(), true, true );
-  for( unsigned j=0; j<ops.back().size(); j++ ){
-    datatypes.back().addSygusConstructor(
-        ops.back()[j], cnames[j], cargs[j], pcs[j], weights[j]);
+  for (unsigned i = 0, size = ops.back().size(); i < size; ++i)
+  {
+    datatypes.back().addSygusConstructor(ops.back()[i],
+                                         cnames.back()[i],
+                                         cargs.back()[i],
+                                         pcs.back()[i],
+                                         weights.back()[i]);
   }
-  //sorts.push_back( btype );
+  Trace("sygus-grammar-def") << "...built datatype " << datatypes.back() << " ";
   Trace("sygus-grammar-def") << "...finished make default grammar for " << fun << " " << range << std::endl;
-
+  // make first datatype be the top level datatype
   if( startIndex>0 ){
-    CVC4::Datatype tmp_dt = datatypes[0];
+    Datatype tmp_dt = datatypes[0];
     datatypes[0] = datatypes[startIndex];
     datatypes[startIndex] = tmp_dt;
   }
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
index 0c5b67656..3afc4c689 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
@@ -131,7 +131,8 @@ public:
   // helper for mkSygusDefaultGrammar (makes unresolved type for mutually recursive datatype construction)
   static TypeNode mkUnresolvedType(const std::string& name, std::set<Type>& unres);
   // collect the list of types that depend on type range
-  static void collectSygusGrammarTypesFor( TypeNode range, std::vector< TypeNode >& types, std::map< TypeNode, std::vector< DatatypeConstructorArg > >& sels );
+  static void collectSygusGrammarTypesFor(TypeNode range,
+                                          std::vector<TypeNode>& types);
   /** helper function for function mkSygusDefaultType
   * Collects a set of mutually recursive datatypes "datatypes" corresponding to
   * encoding type "range" to SyGuS.