Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes decision procedure to share selectors of the same type across multiple constructors. Major rewrite of the SyGuS solver. Adds several new strategies for I/O example problems (PBE) and invariant synthesis. Major simplifications to sygus parsing and synthesis conjecture representation. Do not support check-synth in portfolio. Add sygus regressions.

3 files changed, 115 insertions, 581 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 8194e1933..5d24ec024 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -578,6 +578,7 @@ sygusCommand [CVC4::PtrCloser<CVC4::Command>* cmd]
   std::map< CVC4::Type, CVC4::Type > sygus_to_builtin;
   std::map< CVC4::Type, CVC4::Expr > sygus_to_builtin_expr;
   int startIndex = -1;
+  Expr synth_fun;
 }
   : /* declare-var */
     DECLARE_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); }
@@ -601,7 +602,25 @@ sygusCommand [CVC4::PtrCloser<CVC4::Command>* cmd]
     { PARSER_STATE->checkThatLogicIsSet(); }
     symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE]
     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
-    { seq.reset(new CommandSequence());
+    ( sortSymbol[range,CHECK_DECLARED] )? {
+      if( range.isNull() ){
+        PARSER_STATE->parseError("Must supply return type for synth-fun.");
+      }
+      seq.reset(new CommandSequence());
+      std::vector<Type> var_sorts;
+      for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
+            sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend;
+          ++i) {
+        var_sorts.push_back( (*i).second );
+      }
+      Debug("parser-sygus") << "Define synth fun : " << fun << std::endl;
+      Type synth_fun_type;
+      if( var_sorts.size()>0 ){
+        synth_fun_type = EXPR_MANAGER->mkFunctionType(var_sorts, range);
+      }else{
+        synth_fun_type = range;
+      }
+      synth_fun = PARSER_STATE->mkVar(fun, synth_fun_type);
       PARSER_STATE->pushScope(true);
       for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
             sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend;
@@ -616,11 +635,12 @@ sygusCommand [CVC4::PtrCloser<CVC4::Command>* cmd]
       }
       terms.clear();
       terms.push_back(bvl);
-    }
-    ( sortSymbol[range,CHECK_DECLARED] )? {
-      if( range.isNull() ){
-        PARSER_STATE->parseError("Must supply return type for synth-fun.");
-      }
+      // associate this variable list with the synth fun
+      std::vector< Expr > attr_val_bvl;
+      attr_val_bvl.push_back( bvl );
+      Command* cattr_bvl = new SetUserAttributeCommand("sygus-synth-fun-var-list", synth_fun, attr_val_bvl);
+      cattr_bvl->setMuted(true);
+      PARSER_STATE->preemptCommand(cattr_bvl);
     }
     ( LPAREN_TOK
     ( LPAREN_TOK
@@ -664,18 +684,11 @@ sygusCommand [CVC4::PtrCloser<CVC4::Command>* cmd]
     )+
     RPAREN_TOK { read_syntax = true; }
     )?
-    { 
+    { // the sygus sym type specifies the required grammar for synth_fun, expressed as a type
+      Type sygus_sym_type;
       if( !read_syntax ){
-        //create the default grammar
-        Debug("parser-sygus") << "Make default grammar..." << std::endl;
-        PARSER_STATE->mkSygusDefaultGrammar(
-            range, terms[0], fun, datatypes, sorts, ops, sygus_vars,
-            startIndex);
-        //set start index
-        Debug("parser-sygus") << "Set start index " << startIndex << "..."
-                              << std::endl;
-        PARSER_STATE->setSygusStartIndex(fun, startIndex, datatypes, sorts,
-                                         ops);        
+        sygus_sym_type = range;
+        PARSER_STATE->popScope();
       }else{
         Debug("parser-sygus") << "--- Process " << sgts.size()
                               << " sygus gterms..." << std::endl;
@@ -708,57 +721,32 @@ sygusCommand [CVC4::PtrCloser<CVC4::Command>* cmd]
               datatypes[i], ops[i], cnames[i], cargs[i],
               unresolved_gterm_sym[i], sygus_to_builtin );
         }
-        PARSER_STATE->setSygusStartIndex(fun, startIndex, datatypes, sorts,
-                                         ops);
-      }
-      //only care about datatypes/sorts/ops past here
-      PARSER_STATE->popScope();
-      Debug("parser-sygus") << "--- Make " << datatypes.size()
-                            << " mutual datatypes..." << std::endl;
-      for( unsigned i=0; i<datatypes.size(); i++ ){
-        Debug("parser-sygus") << "  " << i << " : " << datatypes[i].getName()
-                              << std::endl;
-      }
-      std::vector<DatatypeType> datatypeTypes =
-          PARSER_STATE->mkMutualDatatypeTypes(datatypes);
-      seq->addCommand(new DatatypeDeclarationCommand(datatypeTypes));
-      std::map<DatatypeType, Expr> evals;
-      if( sorts[0]!=range ){
-        PARSER_STATE->parseError(std::string("Bad return type in grammar for "
-                                             "SyGuS function ") + fun);
-      }
-      // make all the evals first, since they are mutually referential
-      for(size_t i = 0; i < datatypeTypes.size(); ++i) {
-        DatatypeType dtt = datatypeTypes[i];
-        const Datatype& dt = dtt.getDatatype();
-        Expr eval = dt.getSygusEvaluationFunc();
-        Debug("parser-sygus") << "Make eval " << eval << " for " << dt.getName()
-                              << std::endl;
-        evals.insert(std::make_pair(dtt, eval));
-        if(i == 0) {
-          PARSER_STATE->addSygusFun(fun, eval);
+        PARSER_STATE->setSygusStartIndex(fun, startIndex, datatypes, sorts, ops);
+        //only care about datatypes/sorts/ops past here
+        PARSER_STATE->popScope();
+        Debug("parser-sygus") << "--- Make " << datatypes.size()
+                              << " mutual datatypes..." << std::endl;
+        for( unsigned i=0; i<datatypes.size(); i++ ){
+          Debug("parser-sygus") << "  " << i << " : " << datatypes[i].getName() << std::endl;
         }
-      }
-      // now go through and settle everything
-      for(size_t i = 0; i < datatypeTypes.size(); ++i) {
-        DatatypeType dtt = datatypeTypes[i];
-        const Datatype& dt = dtt.getDatatype();
-        Expr eval = evals[dtt];
-        Debug("parser-sygus") << "Sygus : process grammar : " << dt
-                              << std::endl;
-        for(size_t j = 0; j < dt.getNumConstructors(); ++j) {
-          Expr assertion = PARSER_STATE->getSygusAssertion(
-              datatypeTypes, ops, evals, terms, eval, dt, i, j );
-          seq->addCommand(new AssertCommand(assertion));
+        std::vector<DatatypeType> datatypeTypes =
+            PARSER_STATE->mkMutualDatatypeTypes(datatypes);
+        seq->addCommand(new DatatypeDeclarationCommand(datatypeTypes));
+        if( sorts[0]!=range ){
+          PARSER_STATE->parseError(std::string("Bad return type in grammar for "
+                                               "SyGuS function ") + fun);
         }
+        sygus_sym_type = datatypeTypes[0];
       }
+      
+      // store a dummy variable which stands for second-order quantification, linked to synth fun by an attribute
+      PARSER_STATE->addSygusFunSymbol( sygus_sym_type, synth_fun );
       cmd->reset(seq.release());
     }
   | /* constraint */
     CONSTRAINT_TOK { 
       PARSER_STATE->checkThatLogicIsSet();
       Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl;
-      PARSER_STATE->defineSygusFuns(); 
       Debug("parser-sygus") << "Sygus : read constraint..." << std::endl;
     }
     term[expr, expr2]
@@ -769,7 +757,6 @@ sygusCommand [CVC4::PtrCloser<CVC4::Command>* cmd]
   | INV_CONSTRAINT_TOK {  
       PARSER_STATE->checkThatLogicIsSet();
       Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl;
-      PARSER_STATE->defineSygusFuns(); 
       Debug("parser-sygus") << "Sygus : read inv-constraint..." << std::endl;
     }
     ( symbol[name,CHECK_NONE,SYM_VARIABLE] { 
@@ -796,9 +783,8 @@ sygusCommand [CVC4::PtrCloser<CVC4::Command>* cmd]
       }
       //make relevant terms
       for( unsigned i=0; i<4; i++ ){
-        Debug("parser-sygus") << "Make inv-constraint term #" << i << "..."
-                              << std::endl;
         Expr op = terms[i];
+        Debug("parser-sygus") << "Make inv-constraint term #" << i << " : " << op  << "..." << std::endl;
         std::vector< Expr > children;
         children.push_back( op );
         if( i==2 ){
@@ -806,13 +792,13 @@ sygusCommand [CVC4::PtrCloser<CVC4::Command>* cmd]
         }else{
           children.insert( children.end(), primed[0].begin(), primed[0].end() );
         }
-        terms[i] = EXPR_MANAGER->mkExpr(kind::APPLY,children);
+        terms[i] = EXPR_MANAGER->mkExpr( i==0 ? kind::APPLY_UF : kind::APPLY,children);
         if( i==0 ){
           std::vector< Expr > children2;
           children2.push_back( op );
           children2.insert(children2.end(), primed[1].begin(),
                            primed[1].end());
-          terms.push_back( EXPR_MANAGER->mkExpr(kind::APPLY,children2) );
+          terms.push_back( EXPR_MANAGER->mkExpr(kind::APPLY_UF,children2) );
         }
       }
       //make constraints
@@ -832,7 +818,7 @@ sygusCommand [CVC4::PtrCloser<CVC4::Command>* cmd]
     }
   | /* check-synth */
     CHECK_SYNTH_TOK
-    { PARSER_STATE->checkThatLogicIsSet(); PARSER_STATE->defineSygusFuns(); }
+    { PARSER_STATE->checkThatLogicIsSet(); }
     { Expr sygusVar = EXPR_MANAGER->mkVar("sygus", EXPR_MANAGER->booleanType());
       Expr inst_attr =EXPR_MANAGER->mkExpr(kind::INST_ATTRIBUTE, sygusVar);
       Expr sygusAttr = EXPR_MANAGER->mkExpr(kind::INST_PATTERN_LIST, inst_attr);
@@ -900,6 +886,12 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
           k = CVC4::kind::BITVECTOR_UDIV_TOTAL;
         }else if( k==CVC4::kind::BITVECTOR_UREM ){
           k = CVC4::kind::BITVECTOR_UREM_TOTAL;
+        }else if( k==CVC4::kind::DIVISION ){
+          k = CVC4::kind::DIVISION_TOTAL;
+        }else if( k==CVC4::kind::INTS_DIVISION ){
+          k = CVC4::kind::INTS_DIVISION_TOTAL;
+        }else if( k==CVC4::kind::INTS_MODULUS ){
+          k = CVC4::kind::INTS_MODULUS_TOTAL;
         }
         sgt.d_name = kind::kindToString(k);
         sgt.d_gterm_type = SygusGTerm::gterm_op;
@@ -952,6 +944,12 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
             k = CVC4::kind::BITVECTOR_UDIV_TOTAL;
           }else if( k==CVC4::kind::BITVECTOR_UREM ){
             k = CVC4::kind::BITVECTOR_UREM_TOTAL;
+          }else if( k==CVC4::kind::DIVISION ){
+            k = CVC4::kind::DIVISION_TOTAL;
+          }else if( k==CVC4::kind::INTS_DIVISION ){
+            k = CVC4::kind::INTS_DIVISION_TOTAL;
+          }else if( k==CVC4::kind::INTS_MODULUS ){
+            k = CVC4::kind::INTS_MODULUS_TOTAL;
           }
           sgt.d_name = kind::kindToString(k);
           sgt.d_gterm_type = SygusGTerm::gterm_op;
@@ -2084,6 +2082,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
            if( args.size()!=dtc.getNumArgs() ){
              PARSER_STATE->parseError("Bad number of arguments for application of constructor in pattern.");
            }
+           //FIXME: make MATCH a kind and make this a rewrite
            // build a lambda
            std::vector<Expr> largs;
            largs.push_back( MK_EXPR( CVC4::kind::BOUND_VAR_LIST, args ) );
@@ -2092,7 +2091,8 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
            aargs.push_back( MK_EXPR( CVC4::kind::LAMBDA, largs ) );
            for( unsigned i=0; i<dtc.getNumArgs(); i++ ){
              //can apply total version since we will be guarded by ITE condition
-             aargs.push_back( MK_EXPR( CVC4::kind::APPLY_SELECTOR_TOTAL, dtc[i].getSelector(), expr ) );
+             // however, we need to apply partial version since we don't have the internal selector available
+             aargs.push_back( MK_EXPR( CVC4::kind::APPLY_SELECTOR, dtc[i].getSelector(), expr ) );
            }
            patexprs.push_back( MK_EXPR( CVC4::kind::APPLY, aargs ) );
            patconds.push_back( MK_EXPR( CVC4::kind::APPLY_TESTER, dtc.getTester(), expr ) );
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 7fa71890e..fe5eb3ac8 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -33,8 +33,7 @@ namespace parser {
 
 Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
   Parser(exprManager,input,strictMode,parseOnly),
-  d_logicSet(false),
-  d_nextSygusFun(0) {
+  d_logicSet(false) {
   d_unsatCoreNames.push(std::map<Expr, std::string>());
   if( !strictModeEnabled() ) {
     addTheory(Smt2::THEORY_CORE);
@@ -541,246 +540,6 @@ Expr Smt2::mkSygusVar(const std::string& name, const Type& type, bool isPrimed)
   return e;
 }
 
-void collectSygusGrammarTypesFor( Type range, std::vector< Type >& types, std::map< Type, std::vector< DatatypeConstructorArg > >& sels ){
-  if( !range.isBoolean() ){
-    if( std::find( types.begin(), types.end(), range )==types.end() ){
-      Debug("parser-sygus") << "...will make grammar for " << range << std::endl;
-      types.push_back( range );
-      if( range.isDatatype() ){
-        const Datatype& dt = ((DatatypeType)range).getDatatype();
-        for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-          for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
-            Type crange = ((SelectorType)dt[i][j].getType()).getRangeType();
-            sels[crange].push_back( dt[i][j] );
-            collectSygusGrammarTypesFor( crange, types, sels );
-          }
-        }
-      }
-    }
-  }
-}
-
-void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::string& fun, std::vector<CVC4::Datatype>& datatypes,
-                                  std::vector<Type>& sorts, std::vector< std::vector<Expr> >& ops, std::vector<Expr> sygus_vars, int& startIndex ) {
-
-  //if( !range.isBoolean() && !range.isInteger() && !range.isBitVector() && !range.isDatatype() ){
-  //  parseError("No default grammar for type.");
-  //}
-  startIndex = -1;
-  Debug("parser-sygus") << "Construct default grammar for " << fun << " " << range << std::endl;
-  std::map< CVC4::Type, CVC4::Type > sygus_to_builtin;
-
-  std::vector< Type > types;
-  std::map< Type, std::vector< DatatypeConstructorArg > > sels;
-  //types for each of the variables
-  for( unsigned i=0; i<sygus_vars.size(); i++ ){
-    collectSygusGrammarTypesFor( sygus_vars[i].getType(), types, sels );
-  }
-  //types connected to range
-  collectSygusGrammarTypesFor( range, types, sels );
-
-  //name of boolean sort
-  std::stringstream ssb;
-  ssb << fun << "_Bool";
-  std::string dbname = ssb.str();
-  Type unres_bt = mkUnresolvedType(ssb.str());
-
-  std::vector< Type > unres_types;
-  std::map< Type, Type > type_to_unres;
-  for( unsigned i=0; i<types.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>());
-    //make unresolved type
-    Type unres_t = mkUnresolvedType(dname);
-    unres_types.push_back(unres_t);
-    type_to_unres[types[i]] = unres_t;
-    sygus_to_builtin[unres_t] = types[i];
-  }
-  for( unsigned i=0; i<types.size(); i++ ){
-    Debug("parser-sygus") << "Make grammar for " << types[i] << " " << unres_types[i] << std::endl;
-    std::vector<std::string> cnames;
-    std::vector<std::vector<CVC4::Type> > cargs;
-    std::vector<std::string> unresolved_gterm_sym;
-    Type unres_t = unres_types[i];
-    //add variables
-    for( unsigned j=0; j<sygus_vars.size(); j++ ){
-      if( sygus_vars[j].getType()==types[i] ){
-        std::stringstream ss;
-        ss << sygus_vars[j];
-        Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl;
-        ops[i].push_back( sygus_vars[j] );
-        cnames.push_back( ss.str() );
-        cargs.push_back( std::vector< CVC4::Type >() );
-      }
-    }
-    //add constants
-    std::vector< Expr > consts;
-    mkSygusConstantsForType( types[i], consts );
-    for( unsigned j=0; j<consts.size(); j++ ){
-      std::stringstream ss;
-      ss << consts[j];
-      Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl;
-      ops[i].push_back( consts[j] );
-      cnames.push_back( ss.str() );
-      cargs.push_back( std::vector< CVC4::Type >() );
-    }
-    //ITE
-    CVC4::Kind k = kind::ITE;
-    Debug("parser-sygus") << "...add for " << k << std::endl;
-    ops[i].push_back(getExprManager()->operatorOf(k));
-    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);
-
-    if( types[i].isInteger() ){
-      for( unsigned j=0; j<2; j++ ){
-        CVC4::Kind k = j==0 ? kind::PLUS : kind::MINUS;
-        Debug("parser-sygus") << "...add for " << k << std::endl;
-        ops[i].push_back(getExprManager()->operatorOf(k));
-        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);
-      }
-    }else if( types[i].isDatatype() ){
-      Debug("parser-sygus") << "...add for constructors" << std::endl;
-      const Datatype& dt = ((DatatypeType)types[i]).getDatatype();
-      for( unsigned k=0; k<dt.getNumConstructors(); k++ ){
-        Debug("parser-sygus") << "...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++ ){
-          Type crange = ((SelectorType)dt[k][j].getType()).getRangeType();
-          //Assert( type_to_unres.find(crange)!=type_to_unres.end() );
-          cargs.back().push_back( type_to_unres[crange] );
-        }
-      }
-    }else{
-      std::stringstream sserr;
-      sserr << "No implementation for default Sygus grammar of type " << types[i] << std::endl;
-      warning(sserr.str());
-    }
-    //add for all selectors to this type
-    if( !sels[types[i]].empty() ){
-      Debug("parser-sygus") << "...add for selectors" << std::endl;
-      for( unsigned j=0; j<sels[types[i]].size(); j++ ){
-        Debug("parser-sygus") << "...for " << sels[types[i]][j].getName() << std::endl;
-        Type arg_type = ((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] );
-      }
-    }
-    Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl;
-    datatypes[i].setSygus( types[i], bvl, true, true );
-    mkSygusDatatype( datatypes[i], ops[i], cnames, cargs, unresolved_gterm_sym, sygus_to_builtin );
-    sorts.push_back( types[i] );
-    //set start index if applicable
-    if( types[i]==range ){
-      startIndex = i;
-    }
-  }
-
-  //make Boolean type
-  Type btype = getExprManager()->booleanType();
-  datatypes.push_back(Datatype(dbname));
-  ops.push_back(std::vector<Expr>());
-  std::vector<std::string> cnames;
-  std::vector<std::vector<CVC4::Type> > cargs;
-  std::vector<std::string> unresolved_gterm_sym;
-  Debug("parser-sygus") << "Make grammar for " << btype << " " << datatypes.back() << std::endl;
-  //add variables
-  for( unsigned i=0; i<sygus_vars.size(); i++ ){
-    if( sygus_vars[i].getType().isBoolean() ){
-      std::stringstream ss;
-      ss << sygus_vars[i];
-      Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl;
-      ops.back().push_back( sygus_vars[i] );
-      cnames.push_back( ss.str() );
-      cargs.push_back( std::vector< CVC4::Type >() );
-    }
-  }
-  //add constants if no variables and no connected types
-  if( ops.back().empty() && types.empty() ){
-    std::vector< Expr > consts;
-    mkSygusConstantsForType( btype, consts );
-    for( unsigned j=0; j<consts.size(); j++ ){
-      std::stringstream ss;
-      ss << consts[j];
-      Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl;
-      ops.back().push_back( consts[j] );
-      cnames.push_back( ss.str() );
-      cargs.push_back( std::vector< CVC4::Type >() );
-    }
-  }
-  //add operators
-  for( unsigned i=0; i<3; i++ ){
-    CVC4::Kind k = i==0 ? kind::NOT : ( i==1 ? kind::AND : kind::OR );
-    Debug("parser-sygus") << "...add for " << k << std::endl;
-    ops.back().push_back(getExprManager()->operatorOf(k));
-    cnames.push_back(kind::kindToString(k));
-    cargs.push_back( std::vector< CVC4::Type >() );
-    if( k==kind::NOT ){
-      cargs.back().push_back(unres_bt);
-    }else if( k==kind::AND || k==kind::OR ){
-      cargs.back().push_back(unres_bt);
-      cargs.back().push_back(unres_bt);
-    }
-  }
-  //add predicates for types
-  for( unsigned i=0; i<types.size(); i++ ){
-    Debug("parser-sygus") << "...add predicates for " << types[i] << std::endl;
-    //add equality per type
-    CVC4::Kind k = kind::EQUAL;
-    Debug("parser-sygus") << "...add for " << k << std::endl;
-    ops.back().push_back(getExprManager()->operatorOf(k));
-    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]);
-    //type specific predicates
-    if( types[i].isInteger() ){
-      CVC4::Kind k = kind::LEQ;
-      Debug("parser-sygus") << "...add for " << k << std::endl;
-      ops.back().push_back(getExprManager()->operatorOf(k));
-      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]);
-    }else if( types[i].isDatatype() ){
-      //add for testers
-      Debug("parser-sygus") << "...add for testers" << std::endl;
-      const Datatype& dt = ((DatatypeType)types[i]).getDatatype();
-      for( unsigned k=0; k<dt.getNumConstructors(); k++ ){
-        Debug("parser-sygus") << "...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]);
-      }
-    }
-  }
-  if( range==btype ){
-    startIndex = sorts.size();
-  }
-  Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl;
-  datatypes.back().setSygus( btype, bvl, true, true );
-  mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs, unresolved_gterm_sym, sygus_to_builtin );
-  sorts.push_back( btype );
-
-  Debug("parser-sygus") << "...finished make default grammar for " << fun << " " << range << std::endl;
-}
-
 void Smt2::mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops ) {
   if( type.isInteger() ){
     ops.push_back(getExprManager()->mkConst(Rational(0)));
@@ -1152,77 +911,22 @@ void Smt2::setSygusStartIndex( std::string& fun, int startIndex,
   }
 }
 
-void Smt2::defineSygusFuns() {
-  // only define each one once
-  while(d_nextSygusFun < d_sygusFuns.size()) {
-    std::pair<std::string, Expr> p = d_sygusFuns[d_nextSygusFun];
-    std::string fun = p.first;
-    Debug("parser-sygus") << "Sygus : define fun " << fun << std::endl;
-    Expr eval = p.second;
-    FunctionType evalType = eval.getType();
-    std::vector<Type> argTypes = evalType.getArgTypes();
-    Type rangeType = evalType.getRangeType();
-    Debug("parser-sygus") << "...eval type : " << evalType << ", #args=" << argTypes.size() << std::endl;
-
-    // first make the function type
-    std::vector<Expr> sygusVars;
-    std::vector<Type> funType;
-    for(size_t j = 1; j < argTypes.size(); ++j) {
-      funType.push_back(argTypes[j]);
-      std::stringstream ss;
-      ss << fun << "_v_" << j;
-      sygusVars.push_back(getExprManager()->mkBoundVar(ss.str(), argTypes[j]));
-    }
-    Type funt;
-    if( !funType.empty() ){
-      funt = getExprManager()->mkFunctionType(funType, rangeType);
-      Debug("parser-sygus") << "...eval function type : " << funt << std::endl;
-
-      // copy the bound vars
-      /*
-      std::vector<Expr> sygusVars;
-      //std::vector<Type> types;
-      for(size_t i = 0; i < d_sygusVars.size(); ++i) {
-        std::stringstream ss;
-        ss << d_sygusVars[i];
-        Type type = d_sygusVars[i].getType();
-        sygusVars.push_back(getExprManager()->mkBoundVar(ss.str(), type));
-        //types.push_back(type);
-      }
-      Debug("parser-sygus") << "...made vars, #vars=" << sygusVars.size() << std::endl;
-      */
-
-      //Type t = getExprManager()->mkFunctionType(types, rangeType);
-      //Debug("parser-sygus") << "...function type : " << t << std::endl;
-    }else{
-      funt = rangeType;
-    }
-    Expr lambda = mkFunction(fun, funt, ExprManager::VAR_FLAG_DEFINED);
-    Debug("parser-sygus") << "...made function : " << lambda << std::endl;
-    std::vector<Expr> applyv;
-    Expr funbv = getExprManager()->mkBoundVar(std::string("f") + fun, argTypes[0]);
-    d_sygusFunSymbols.push_back(funbv);
-    applyv.push_back(eval);
-    applyv.push_back(funbv);
-    for(size_t i = 0; i < sygusVars.size(); ++i) {
-      applyv.push_back(sygusVars[i]);
-    }
-    Expr apply = getExprManager()->mkExpr(kind::APPLY_UF, applyv);
-    Debug("parser-sygus") << "...made apply " << apply << std::endl;
-    Debug("parser-sygus") << "--> Define " << fun << " as " << lambda << " " << apply << std::endl;
-    Command* cmd = new DefineFunctionCommand(fun, lambda, sygusVars, apply);
-    preemptCommand(cmd);
-
-    ++d_nextSygusFun;
-  }
-}
-
 void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
                             std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs,
                             std::vector<std::string>& unresolved_gterm_sym,
                             std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin ) {
   Debug("parser-sygus") << "Making sygus datatype " << dt.getName() << std::endl;
   Debug("parser-sygus") << "  add constructors..." << std::endl;
+  std::vector<std::string> df_name; 
+  std::vector<CVC4::Expr> df_op;
+  std::vector< std::vector<Expr> > df_let_args;
+  std::vector< Expr > df_let_body;
+  //dt.mkSygusConstructors( ops, cnames, cargs, sygus_to_builtin, 
+  //                        d_sygus_let_func_to_vars, d_sygus_let_func_to_body, d_sygus_let_func_to_num_input_vars, 
+  //                        df_name, df_op, df_let_args, df_let_body );
+  
+  Debug("parser-sygus") << "SMT2 sygus parser : Making constructors for sygus datatype " << dt.getName() << std::endl;
+  Debug("parser-sygus") << "  add constructors..." << std::endl;
   for( int i=0; i<(int)cnames.size(); i++ ){
     bool is_dup = false;
     bool is_dup_op = false;
@@ -1283,9 +987,15 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
       //replace operator and name
       ops[i] = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED);
       cnames[i] = ss.str();
-      d_sygus_defined_funs.push_back( ops[i] );
-      preemptCommand( new DefineFunctionCommand(ss.str(), ops[i], let_args, let_body) );
-      addSygusDatatypeConstructor( dt, ops[i], cnames[i], cargs[i], let_body, let_args, 0 );
+      // indicate we need a define function
+      df_name.push_back( ss.str() );
+      df_op.push_back( ops[i] );
+      df_let_args.push_back( let_args );
+      df_let_body.push_back( let_body );
+      
+      //d_sygus_defined_funs.push_back( ops[i] );
+      //preemptCommand( new DefineFunctionCommand(ss.str(), ops[i], let_args, let_body) );
+      dt.addSygusConstructor( ops[i], cnames[i], cargs[i], let_body, let_args, 0 );
     }else{
       std::map< CVC4::Expr, CVC4::Expr >::iterator it = d_sygus_let_func_to_body.find( ops[i] );
       if( it!=d_sygus_let_func_to_body.end() ){
@@ -1293,9 +1003,10 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
         let_args.insert( let_args.end(), d_sygus_let_func_to_vars[ops[i]].begin(), d_sygus_let_func_to_vars[ops[i]].end() );
         let_num_input_args = d_sygus_let_func_to_num_input_vars[ops[i]];
       }
-      addSygusDatatypeConstructor( dt, ops[i], cnames[i], cargs[i], let_body, let_args, let_num_input_args );
+      dt.addSygusConstructor( ops[i], cnames[i], cargs[i], let_body, let_args, let_num_input_args );
     }
   }
+
   Debug("parser-sygus") << "  add constructors for unresolved symbols..." << std::endl;
   if( !unresolved_gterm_sym.empty() ){
     std::vector< Type > types;
@@ -1320,12 +1031,18 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
           std::stringstream ssid;
           ssid << unresolved_gterm_sym[i] << "_id";
           Expr id_op = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED);
-          d_sygus_defined_funs.push_back( id_op );
-          preemptCommand( new DefineFunctionCommand(ssid.str(), id_op, let_args, let_body) );
+          // indicate we need a define function
+          df_name.push_back( ssid.str() );
+          df_op.push_back( id_op );
+          df_let_args.push_back( let_args );
+          df_let_body.push_back( let_body );
+          
+          //d_sygus_defined_funs.push_back( id_op );
+          //preemptCommand( new DefineFunctionCommand(ssid.str(), id_op, let_args, let_body) );
           //make the sygus argument list
           std::vector< Type > id_carg;
           id_carg.push_back( t );
-          addSygusDatatypeConstructor( dt, id_op, unresolved_gterm_sym[i], id_carg, let_body, let_args, 0 );
+          dt.addSygusConstructor( id_op, unresolved_gterm_sym[i], id_carg, let_body, let_args, 0 );
           //add to operators
           ops.push_back( id_op );
         }
@@ -1334,187 +1051,12 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
       }
     }
   }
-
-}
-
-void Smt2::addSygusDatatypeConstructor( CVC4::Datatype& dt, CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs,
-                                        CVC4::Expr& let_body, std::vector< CVC4::Expr >& let_args, unsigned let_num_input_args ) {
-  Debug("parser-sygus") << "--> Add constructor " << cname << " to " << dt.getName() << std::endl;
-  if( !let_body.isNull() ){
-    Debug("parser-sygus") << "    let body = " << let_body << ", args = " << let_args.size() << "," << let_num_input_args << std::endl;
-    //TODO : remove arguments not occurring in body
-    //if this is a self identity function, ignore
-    if( let_args.size()==0 && let_args[0]==let_body ){
-      Debug("parser-sygus") << "    identity function " << cargs[0] << " to " << dt.getName() << std::endl;
-      //TODO
-    }
-  }
-  std::string name = dt.getName() + "_" + cname;
-  std::string testerId("is-");
-  testerId.append(name);
-  checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
-  checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
-  CVC4::DatatypeConstructor c(name, testerId );
-  c.setSygus( op, let_body, let_args, let_num_input_args );
-  for( unsigned j=0; j<cargs.size(); j++ ){
-    Debug("parser-sygus-debug") << "  arg " << j << " : " << cargs[j] << std::endl;
-    std::stringstream sname;
-    sname << name << "_" << j;
-    c.addArg(sname.str(), cargs[j]);
-  }
-  dt.addConstructor(c);
-}
-
-
-// i is index in datatypes/ops
-// j is index is datatype
-Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vector< std::vector<Expr> >& ops,
-                              std::map<DatatypeType, Expr>& evals, std::vector<Expr>& terms,
-                              Expr eval, const Datatype& dt, size_t i, size_t j ) {
-  const DatatypeConstructor& ctor = dt[j];
-  Debug("parser-sygus") << "Sygus : process constructor " << j << " : " << dt[j] << std::endl;
-  std::vector<Expr> bvs, extraArgs;
-  for(size_t k = 0; k < ctor.getNumArgs(); ++k) {
-    std::string vname = "v_" + ctor[k].getName();
-    Expr bv = getExprManager()->mkBoundVar(vname, SelectorType(ctor[k].getType()).getRangeType());
-    bvs.push_back(bv);
-    extraArgs.push_back(bv);
-  }
-  if( !terms[0].isNull() ){
-    bvs.insert(bvs.end(), terms[0].begin(), terms[0].end());
-  }
-  Expr bvl;
-  if( !bvs.empty() ){
-    bvl = getExprManager()->mkExpr(kind::BOUND_VAR_LIST, bvs);
-  }
-  Debug("parser-sygus") << "...made bv list " << bvl << std::endl;
-  std::vector<Expr> patv;
-  patv.push_back(eval);
-  std::vector<Expr> applyv;
-  applyv.push_back(ctor.getConstructor());
-  applyv.insert(applyv.end(), extraArgs.begin(), extraArgs.end());
-  for(size_t k = 0; k < applyv.size(); ++k) {
-  }
-  Expr cpatv = getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, applyv);
-  Debug("parser-sygus") << "...made eval ctor apply " << cpatv << std::endl;
-  patv.push_back(cpatv);
-  if( !terms[0].isNull() ){
-    patv.insert(patv.end(), terms[0].begin(), terms[0].end());
-  }
-  Expr evalApply = getExprManager()->mkExpr(kind::APPLY_UF, patv);
-  Debug("parser-sygus") << "...made eval apply " << evalApply << std::endl;
-  std::vector<Expr> builtApply;
-  for(size_t k = 0; k < extraArgs.size(); ++k) {
-    std::vector<Expr> patvb;
-    patvb.push_back(evals[DatatypeType(extraArgs[k].getType())]);
-    patvb.push_back(extraArgs[k]);
-    if( !terms[0].isNull() ){
-      patvb.insert(patvb.end(), terms[0].begin(), terms[0].end());
-    }
-    Debug("parser-sygus-debug") << "...add to built apply " << evals[DatatypeType(extraArgs[k].getType())] << " " << extraArgs[k] << " " << extraArgs[k].getType() << std::endl;
-    builtApply.push_back(getExprManager()->mkExpr(kind::APPLY_UF, patvb));
-    Debug("parser-sygus-debug") << "...added " << builtApply.back() << std::endl;
-  }
-  for(size_t k = 0; k < builtApply.size(); ++k) {
-  }
-  Expr builtTerm;
-  Debug("parser-sygus") << "...operator is : " << ops[i][j] << ", type = " << ops[i][j].getType() << ", kind = " << ops[i][j].getKind() << ", is defined = " << isDefinedFunction( ops[i][j] ) << std::endl;
-  if( ops[i][j].getKind() != kind::BUILTIN ){
-    Kind ok = kind::UNDEFINED_KIND;
-    if( isDefinedFunction( ops[i][j] ) || std::find( d_sygus_defined_funs.begin(), d_sygus_defined_funs.end(), ops[i][j] )!=d_sygus_defined_funs.end() ){
-      ok = kind::APPLY;
-    }else{
-      Type t = ops[i][j].getType();
-      if( t.isConstructor() ){
-        ok = kind::APPLY_CONSTRUCTOR;
-      }else if( t.isSelector() ){
-        ok = kind::APPLY_SELECTOR;
-      }else if( t.isTester() ){
-        ok = kind::APPLY_TESTER;
-      }else{
-        ok = getExprManager()->operatorToKind( ops[i][j] );
-      }
-    }
-    Debug("parser-sygus") << "...processed operator kind : " << ok << std::endl;
-    if( ok!=kind::UNDEFINED_KIND ){
-      builtTerm = getExprManager()->mkExpr(ok, ops[i][j], builtApply);
-    }else{
-      builtTerm = ops[i][j];
-    }
-  }else{
-    if( !builtApply.empty() ){
-      builtTerm = getExprManager()->mkExpr(ops[i][j], builtApply);
-    }else{
-      builtTerm = ops[i][j];
-    }
-  }
-  Debug("parser-sygus") << "...made built term " << builtTerm << std::endl;
-  Expr assertion = getExprManager()->mkExpr(kind::EQUAL, evalApply, builtTerm);
-  if( !bvl.isNull() ){
-    Expr pattern = getExprManager()->mkExpr(kind::INST_PATTERN, evalApply);
-    pattern = getExprManager()->mkExpr(kind::INST_PATTERN_LIST, pattern);
-    assertion = getExprManager()->mkExpr(kind::FORALL, bvl, assertion, pattern);
-  }
-  Debug("parser-sygus") << "...made assertion " << assertion << std::endl;
-
-  //linearize multiplication if possible
-  if( builtTerm.getKind()==kind::MULT ){
-    for(size_t k = 0; k < ctor.getNumArgs(); ++k) {
-      Type at = SelectorType(ctor[k].getType()).getRangeType();
-      if( at.isDatatype() ){
-        DatatypeType atd = (DatatypeType)SelectorType(ctor[k].getType()).getRangeType();
-        Debug("parser-sygus") << "Argument " << k << " " << atd << std::endl;
-        std::vector<DatatypeType>::iterator itd = std::find( datatypeTypes.begin(), datatypeTypes.end(), atd );
-        if( itd!=datatypeTypes.end() ){
-          Debug("parser-sygus2") << "Exists in datatypeTypes." << std::endl;
-          unsigned index = itd-datatypeTypes.begin();
-          Debug("parser-sygus2") << "index = " << index << std::endl;
-          bool isConst = true;
-          for( unsigned cc = 0; cc < ops[index].size(); cc++ ){
-            Debug("parser-sygus2") << "ops[" << cc << "]=" << ops[index][cc] << std::endl;
-            if( ops[index][cc].getKind() != kind::CONST_RATIONAL ){
-              isConst = false;
-              break;
-            }
-          }
-          if( isConst ){
-            Debug("parser-sygus") << "Linearize multiplication " << ctor << " based on argument " << k << std::endl;
-            const Datatype & atdd = atd.getDatatype();
-            std::vector<Expr> assertions;
-            std::vector<Expr> nbvs;
-            for( unsigned a=0; a<bvl.getNumChildren(); a++ ){
-              if( a!=k ){
-                nbvs.push_back( bvl[a] );
-              }
-            }
-            Expr nbvl = getExprManager()->mkExpr( kind::BOUND_VAR_LIST, nbvs );
-            for( unsigned cc = 0; cc < ops[index].size(); cc++ ){
-              //Make new assertion based on partially instantiating existing
-              applyv[k+1] = getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, atdd[cc].getConstructor());
-              Debug("parser-sygus") << "applyv " << applyv[k+1] << std::endl;
-              cpatv = getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, applyv);
-              Debug("parser-sygus") << "cpatv " << cpatv << std::endl;
-              patv[1] = cpatv;
-              evalApply = getExprManager()->mkExpr(kind::APPLY_UF, patv);
-              Debug("parser-sygus") << "evalApply " << evalApply << std::endl;
-              builtApply[k] = ops[index][cc];
-              Debug("parser-sygus") << "builtApply " << builtApply[k] << std::endl;
-              builtTerm = getExprManager()->mkExpr(ops[i][j], builtApply);
-              Debug("parser-sygus") << "builtTerm " << builtTerm << std::endl;
-              Expr eassertion = getExprManager()->mkExpr(kind::EQUAL, evalApply, builtTerm);
-              Expr epattern = getExprManager()->mkExpr(kind::INST_PATTERN, evalApply);
-              epattern = getExprManager()->mkExpr(kind::INST_PATTERN_LIST, epattern);
-              eassertion = getExprManager()->mkExpr(kind::FORALL, nbvl, eassertion, epattern);
-              assertions.push_back( eassertion );
-            }
-            assertion = assertions.size()==1 ? assertions[0] : getExprManager()->mkExpr( kind::AND, assertions );
-            Debug("parser-sygus") << "...(linearized) assertion is: " << assertion << std::endl;
-          }
-        }
-      }
-    }
+  
+  
+  for( unsigned i=0; i<df_name.size(); i++ ){
+    d_sygus_defined_funs.push_back( df_op[i] );
+    preemptCommand( new DefineFunctionCommand(df_name[i], df_op[i], df_let_args[i], df_let_body[i]) );
   }
-  return assertion;
 }
 
 const void Smt2::getSygusPrimedVars( std::vector<Expr>& vars, bool isPrimed ) {
@@ -1531,5 +1073,16 @@ const void Smt2::getSygusPrimedVars( std::vector<Expr>& vars, bool isPrimed ) {
   }
 }
 
+const void Smt2::addSygusFunSymbol( Type t, Expr synth_fun ){
+  Expr sym = mkBoundVar("sfproxy", t);
+  d_sygusFunSymbols.push_back(sym);
+  
+  std::vector< Expr > attr_value;
+  attr_value.push_back( synth_fun );
+  Command* cattr = new SetUserAttributeCommand("sygus-synth-fun", sym, attr_value);
+  cattr->setMuted(true);
+  preemptCommand(cattr);
+}
+
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 8222ac3a3..3eed0e871 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -62,10 +62,9 @@ private:
   std::pair<Expr, std::string> d_lastNamedTerm;
   // this is a user-context stack
   std::stack< std::map<Expr, std::string> > d_unsatCoreNames;
+  // for sygus
   std::vector<Expr> d_sygusVars, d_sygusConstraints, d_sygusFunSymbols;
-  std::vector< std::pair<std::string, Expr> > d_sygusFuns;
   std::map< Expr, bool > d_sygusVarPrimed;
-  size_t d_nextSygusFun;
 
 protected:
   Smt2(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false);
@@ -179,9 +178,6 @@ public:
 
   Expr mkSygusVar(const std::string& name, const Type& type, bool isPrimed = false);
 
-  void mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::string& fun, std::vector<CVC4::Datatype>& datatypes,
-                              std::vector<Type>& sorts, std::vector< std::vector<Expr> >& ops, std::vector<Expr> sygus_vars, int& startIndex );
-
   void mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops );
 
   void processSygusGTerm( CVC4::SygusGTerm& sgt, int index,
@@ -218,24 +214,11 @@ public:
                            std::vector< CVC4::Type>& sorts,
                            std::vector< std::vector<CVC4::Expr> >& ops );
 
-  void addSygusFun(const std::string& fun, Expr eval) {
-    d_sygusFuns.push_back(std::make_pair(fun, eval));
-  }
-
-  void defineSygusFuns();
-
   void mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
                         std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs,
                         std::vector<std::string>& unresolved_gterm_sym,
                         std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin );
 
-  // i is index in datatypes/ops
-  // j is index is datatype
-  Expr getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vector< std::vector<Expr> >& ops,
-                          std::map<DatatypeType, Expr>& evals, std::vector<Expr>& terms,
-                          Expr eval, const Datatype& dt, size_t i, size_t j );
-
-
 
   void addSygusConstraint(Expr constraint) {
     d_sygusConstraints.push_back(constraint);
@@ -254,6 +237,7 @@ public:
   }
   const void getSygusPrimedVars( std::vector<Expr>& vars, bool isPrimed );
 
+  const void addSygusFunSymbol( Type t, Expr synth_fun );
   const std::vector<Expr>& getSygusFunSymbols() {
     return d_sygusFunSymbols;
   }
@@ -327,9 +311,6 @@ private:
 
   void collectSygusLetArgs( CVC4::Expr e, std::vector< CVC4::Type >& sygusArgs, std::vector< CVC4::Expr >& builtinArgs );
 
-  void addSygusDatatypeConstructor( CVC4::Datatype& dt, CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs,
-                                    CVC4::Expr& let_body, std::vector< CVC4::Expr >& let_args, unsigned let_num_input_args );
-
   Type processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector< CVC4::Datatype >& datatypes,
                                 std::vector< CVC4::Type>& sorts,
                                 std::vector< std::vector<CVC4::Expr> >& ops,