Squashed merge of SygusComp 2015 branch.

4 files changed, 552 insertions, 332 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 0edd8bc46..1564e6f3e 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -492,6 +492,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
   std::vector<std::pair<std::string, Type> > sortedVarNames;
   SExpr sexpr;
   CommandSequence* seq;
+  std::vector< std::vector< CVC4::SygusGTerm > > sgts;
   std::vector< CVC4::Datatype > datatypes;
   std::vector< std::vector<Expr> > ops;
   std::vector< std::vector< std::string > > cnames;
@@ -499,7 +500,6 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
   std::vector< bool > allow_const;
   std::vector< std::vector< std::string > > unresolved_gterm_sym;
   bool read_syntax = false;
-  int sygus_dt_index = 0;
   Type sygus_ret;
   std::map< CVC4::Type, CVC4::Type > sygus_to_builtin;
   std::map< CVC4::Type, CVC4::Expr > sygus_to_builtin_expr;
@@ -522,22 +522,27 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
     DEFINE_SORT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     symbol[name,CHECK_UNDECLARED,SYM_SORT]
     { PARSER_STATE->checkUserSymbol(name); }
-    LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK
-    { PARSER_STATE->pushScope(true);
-      for(std::vector<std::string>::const_iterator i = names.begin(),
-            iend = names.end();
-          i != iend;
-          ++i) {
-        sorts.push_back(PARSER_STATE->mkSort(*i));
+    ( LPAREN_TOK SYGUS_ENUM_TOK LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK RPAREN_TOK {
+        Debug("parser-sygus") << "Defining enum datatype " << name << " with " << names.size() << " constructors." << std::endl;
+        //make datatype
+        datatypes.push_back(Datatype(name));
+        for( unsigned i=0; i<names.size(); i++ ){
+          std::string cname = name + "__Enum__" + names[i];
+          std::string testerId("is-");
+          testerId.append(cname);
+          PARSER_STATE->checkDeclaration(cname, CHECK_UNDECLARED, SYM_VARIABLE);
+          PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
+          CVC4::DatatypeConstructor c(cname, testerId);
+          datatypes[0].addConstructor(c);
+        }
+        std::vector<DatatypeType> datatypeTypes = PARSER_STATE->mkMutualDatatypeTypes(datatypes);
+        $cmd = new DatatypeDeclarationCommand(datatypeTypes);
       }
-    }
-    sortSymbol[t,CHECK_DECLARED]
-    { PARSER_STATE->popScope();
-      // Do NOT call mkSort, since that creates a new sort!
-      // This name is not its own distinct sort, it's an alias.
-      PARSER_STATE->defineParameterizedType(name, sorts, t);
-      $cmd = new DefineTypeCommand(name, sorts, t);
-    }
+      | sortSymbol[t,CHECK_DECLARED] { 
+        PARSER_STATE->defineParameterizedType(name, sorts, t);
+        $cmd = new DefineTypeCommand(name, sorts, t);
+      }
+    )
   | /* declare-var */
     DECLARE_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
@@ -545,6 +550,13 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
     sortSymbol[t,CHECK_DECLARED]
     { PARSER_STATE->mkSygusVar(name, t);
       $cmd = new EmptyCommand(); }
+  | /* declare-primed-var */
+    DECLARE_PRIMED_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
+    { PARSER_STATE->checkUserSymbol(name); }
+    sortSymbol[t,CHECK_DECLARED]
+    { PARSER_STATE->mkSygusVar(name, t, true);
+      $cmd = new EmptyCommand(); }
   | /* declare-fun */
     DECLARE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
@@ -595,7 +607,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
       $cmd = new DefineFunctionCommand(name, func, terms, expr);
     }
   | /* synth-fun */
-    SYNTH_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    ( SYNTH_FUN_TOK | SYNTH_INV_TOK { range = EXPR_MANAGER->booleanType(); } ) { PARSER_STATE->checkThatLogicIsSet(); }
     symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE]
     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
     { seq = new CommandSequence();
@@ -615,7 +627,11 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
       terms.clear();
       terms.push_back(bvl);
     }
-    sortSymbol[range,CHECK_DECLARED]
+    ( sortSymbol[range,CHECK_DECLARED] )? {
+      if( range.isNull() ){
+        PARSER_STATE->parseError("Must supply return type for synth-fun.");
+      }
+    }
     ( LPAREN_TOK
     ( LPAREN_TOK
       symbol[name,CHECK_NONE,SYM_VARIABLE] 
@@ -626,25 +642,28 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
           startIndex = datatypes.size();
         }
         std::string dname = ss.str();
+        sgts.push_back( std::vector< CVC4::SygusGTerm >() );
+        sgts.back().push_back( CVC4::SygusGTerm() );
         PARSER_STATE->pushSygusDatatypeDef(t, dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym);
         Type unres_t;
         if(!PARSER_STATE->isUnresolvedType(dname)) {
           // if not unresolved, must be undeclared
+          Debug("parser-sygus") << "Make unresolved type : " << dname << std::endl;
           PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT);
           unres_t = PARSER_STATE->mkUnresolvedType(dname);
         }else{
+          Debug("parser-sygus") << "Get sort : " << dname << std::endl;
           unres_t = PARSER_STATE->getSort(dname);
         }
         sygus_to_builtin[unres_t] = t;
-        sygus_dt_index = datatypes.size()-1;
         Debug("parser-sygus") << "--- Read sygus grammar " << name << " under function " << fun << "..." << std::endl;
         Debug("parser-sygus") << "    type to resolve " << unres_t << std::endl;
         Debug("parser-sygus") << "    builtin type " << t << std::endl;
       }
       // Note the official spec for NTDef is missing the ( parens )
       // but they are necessary to parse SyGuS examples
-      LPAREN_TOK sygusGTerm[sygus_dt_index, datatypes, sorts, fun, ops, cnames, cargs, allow_const, unresolved_gterm_sym, 
-                            sygus_vars, sygus_to_builtin, sygus_to_builtin_expr, sygus_ret, -1]+ RPAREN_TOK
+      LPAREN_TOK ( sygusGTerm[ sgts.back().back(), fun] { sgts.back().push_back( CVC4::SygusGTerm() ); } )+ 
+      RPAREN_TOK { sgts.back().pop_back(); }
       RPAREN_TOK 
     )+
     RPAREN_TOK { read_syntax = true; }
@@ -652,10 +671,22 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
     { 
       if( !read_syntax ){
         //create the default grammar
-        PARSER_STATE->mkSygusDefaultGrammar( range, terms[0], fun, datatypes, sorts, ops, sygus_vars );
+        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 );        
       }else{
+        Debug("parser-sygus") << "--- Process " << sgts.size() << " sygus gterms..." << std::endl;
+        for( unsigned i=0; i<sgts.size(); i++ ){
+          for( unsigned j=0; j<sgts[i].size(); j++ ){
+            Type sub_ret;
+            PARSER_STATE->processSygusGTerm( sgts[i][j], i, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym, 
+                                             sygus_vars, sygus_to_builtin, sygus_to_builtin_expr, sub_ret );
+          }
+        }
         //swap index if necessary
-        Debug("parser-sygus") << "Making sygus datatypes..." << std::endl;
+        Debug("parser-sygus") << "--- Making sygus datatypes..." << std::endl;
         for( unsigned i=0; i<datatypes.size(); i++ ){
           Debug("parser-sygus") << "..." << datatypes[i].getName() << " has builtin sort " << sorts[i] << std::endl;
         }
@@ -667,25 +698,11 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
           datatypes[i].setSygus( sorts[i], terms[0], allow_const[i], false );
           PARSER_STATE->mkSygusDatatype( datatypes[i], ops[i], cnames[i], cargs[i], unresolved_gterm_sym[i], sygus_to_builtin );
         }
-        //only care about datatypes/sorts/ops past here
-        if( startIndex>0 ){
-         // PARSER_STATE->swapSygusStart( startIndex, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
-          CVC4::Datatype tmp_dt = datatypes[0];
-          Type tmp_sort = sorts[0];
-          std::vector< Expr > tmp_ops;
-          tmp_ops.insert( tmp_ops.end(), ops[0].begin(), ops[0].end() );
-          datatypes[0] = datatypes[startIndex];
-          sorts[0] = sorts[startIndex];
-          ops[0].clear();
-          ops[0].insert( ops[0].end(), ops[startIndex].begin(), ops[startIndex].end() );
-          datatypes[startIndex] = tmp_dt;
-          sorts[startIndex] = tmp_sort;
-          ops[startIndex].clear();
-          ops[startIndex].insert( ops[startIndex].begin(), tmp_ops.begin(), tmp_ops.end() );
-        }
+        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;
+      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;
       }
@@ -730,8 +747,9 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
       $cmd = seq;
     }
   | /* constraint */
-    CONSTRAINT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    { Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl;
+    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;
     }
@@ -740,6 +758,62 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
       PARSER_STATE->addSygusConstraint(expr);
       $cmd = new EmptyCommand();
     }
+  | 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] { 
+        if( !terms.empty() ){
+          if( !PARSER_STATE->isDefinedFunction(name) ){
+            std::stringstream ss;
+            ss << "Function " << name << " in inv-constraint is not defined.";
+            PARSER_STATE->parseError(ss.str());
+          }
+        }
+        terms.push_back( PARSER_STATE->getVariable(name) );
+      }
+    )+ {
+      if( terms.size()!=4 ){
+        PARSER_STATE->parseError("Bad syntax for inv-constraint: expected 4 arguments.");
+      }
+      //get primed variables
+      std::vector< Expr > primed[2];
+      std::vector< Expr > all;
+      for( unsigned i=0; i<2; i++ ){
+        PARSER_STATE->getSygusPrimedVars( primed[i], i==1 );
+        all.insert( all.end(), primed[i].begin(), primed[i].end() );
+      }
+      //make relevant terms
+      for( unsigned i=0; i<4; i++ ){
+        Debug("parser-sygus") << "Make inv-constraint term #" << i << "..." << std::endl;
+        Expr op = terms[i];
+        std::vector< Expr > children;
+        children.push_back( op );
+        if( i==2 ){
+          children.insert( children.end(), all.begin(), all.end() );
+        }else{
+          children.insert( children.end(), primed[0].begin(), primed[0].end() );
+        }
+        terms[i] = EXPR_MANAGER->mkExpr(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) );
+        }
+      }
+      //make constraints
+      std::vector< Expr > conj;
+      conj.push_back( EXPR_MANAGER->mkExpr(kind::IMPLIES, terms[1], terms[0] ) );
+      conj.push_back( EXPR_MANAGER->mkExpr(kind::IMPLIES, EXPR_MANAGER->mkExpr(kind::AND, terms[0], terms[2] ), terms[4] ) );
+      conj.push_back( EXPR_MANAGER->mkExpr(kind::IMPLIES, terms[0], terms[3] ) );
+      Expr ic = EXPR_MANAGER->mkExpr( kind::AND, conj );
+      Debug("parser-sygus") << "...read invariant constraint " << ic << std::endl;
+      PARSER_STATE->addSygusConstraint(ic);
+      $cmd = new EmptyCommand();
+    }
   | /* check-synth */
     CHECK_SYNTH_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     { Expr sygusVar = EXPR_MANAGER->mkVar("sygus", EXPR_MANAGER->booleanType());
@@ -775,102 +849,63 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
 //  fun is the name of the synth-fun this grammar term is for.
 //  This method adds N operators to ops[index], N names to cnames[index] and N type argument vectors to cargs[index] (where typically N=1)
 //  This method may also add new elements pairwise into datatypes/sorts/ops/cnames/cargs in the case of non-flat gterms.
-sygusGTerm[int index, 
-           std::vector< CVC4::Datatype >& datatypes,
-           std::vector< CVC4::Type>& sorts,
-           std::string& fun, 
-           std::vector< std::vector<CVC4::Expr> >& ops, 
-           std::vector< std::vector<std::string> >& cnames, 
-           std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, 
-           std::vector< bool > allow_const,
-           std::vector< std::vector< std::string > >& unresolved_gterm_sym,
-           std::vector<CVC4::Expr>& sygus_vars, 
-           std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr,
-           CVC4::Type& ret, int gtermType]
+sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
 @declarations {
-  std::string name;
+  std::string name, name2;
+  bool readEnum = false;
   Kind k;
   Type t;
   CVC4::DatatypeConstructor* ctor = NULL;
-  unsigned count = 0;
   std::string sname;
-  // 0 builtin operator, 1 defined operator, 2 any constant, 3 any variable, 4 ignore, 5 let, -1 none
-  int sub_gtermType = -1;
-  Type sub_ret;
-  int sub_dt_index = -1;
-  std::string sub_dname;
-  Type null_type;
-  Expr null_expr;
   std::vector< Expr > let_vars;
-  int let_start_index = -1;
-  //int let_end_index = -1;
-  int let_end_arg_index = -1;
-  Expr let_func;
+  bool readingLet = false;
 }
   : LPAREN_TOK
-    ( builtinOp[k]
-      { Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : " << name << std::endl;
+    //read operator
+    ( builtinOp[k]{ 
+        Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : " << name << std::endl;
         //since we enforce satisfaction completeness, immediately convert to total version
         if( k==CVC4::kind::BITVECTOR_UDIV ){
           k = CVC4::kind::BITVECTOR_UDIV_TOTAL;
         }
-        name = kind::kindToString(k);
-        sub_gtermType = 0;
-        ops[index].push_back(EXPR_MANAGER->operatorOf(k));
-        cnames[index].push_back( name );
+        sgt.d_name = kind::kindToString(k);
+        sgt.d_gterm_type = SygusGTerm::gterm_op;
+        sgt.d_expr = EXPR_MANAGER->operatorOf(k);
       }
      | LET_TOK LPAREN_TOK { 
-         name = std::string("let");
-         sub_gtermType = 5; 
-         ops[index].push_back( null_expr );
-         cnames[index].push_back( name );
-         cargs[index].push_back( std::vector< CVC4::Type >() );
+         sgt.d_name = std::string("let");
+         sgt.d_gterm_type = SygusGTerm::gterm_let;
          PARSER_STATE->pushScope(true);
-         let_start_index = datatypes.size();
+         readingLet = true;
        }
        ( LPAREN_TOK 
         symbol[sname,CHECK_NONE,SYM_VARIABLE] 
         sortSymbol[t,CHECK_DECLARED] { 
           Expr v = PARSER_STATE->mkBoundVar(sname,t); 
-          let_vars.push_back( v ); 
-          std::stringstream ss;
-          ss << datatypes[index].getName() << "_" << ops[index].size() << "_lv_" << let_vars.size();
-          sub_dname = ss.str();
-          PARSER_STATE->pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
-          sub_dt_index = datatypes.size()-1;
-          sub_ret = null_type;
+          sgt.d_let_vars.push_back( v ); 
+          sgt.addChild();
         } 
-        sygusGTerm[sub_dt_index,datatypes,sorts,fun,ops,cnames,cargs,allow_const,unresolved_gterm_sym,
-                   sygus_vars,sygus_to_builtin,sygus_to_builtin_expr,sub_ret,sub_gtermType] {
-          Debug("parser-sygus") << "Process argument #" << let_vars.size() << "..." << std::endl;
-          Type tt = PARSER_STATE->processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym, 
-                                                           sygus_to_builtin, sygus_to_builtin_expr, sub_ret );
-          cargs[index].back().push_back(tt);
-        }
-        RPAREN_TOK )+ RPAREN_TOK { 
-          //let_end_index = datatypes.size();
-          let_end_arg_index = cargs[index].back().size();
-        }
+        sygusGTerm[sgt.d_children.back(), fun]
+        RPAREN_TOK )+ RPAREN_TOK
     | SYGUS_CONSTANT_TOK sortSymbol[t,CHECK_DECLARED] 
-      { sub_gtermType = 2; allow_const[index] = true;Debug("parser-sygus") << "Sygus grammar constant." << std::endl; }
+      { sgt.d_gterm_type = SygusGTerm::gterm_constant; sgt.d_type = t;Debug("parser-sygus") << "Sygus grammar constant." << std::endl; }
     | SYGUS_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED]
-      { sub_gtermType = 3; Debug("parser-sygus") << "Sygus grammar variable." << std::endl; }
+      { sgt.d_gterm_type = SygusGTerm::gterm_variable; sgt.d_type = t;Debug("parser-sygus") << "Sygus grammar variable." << std::endl; }
     | SYGUS_LOCAL_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED]
-      { sub_gtermType = 4; Debug("parser-sygus") << "Sygus grammar local variable...ignore." << std::endl; }
+      { sgt.d_gterm_type = SygusGTerm::gterm_local_variable; sgt.d_type = t;Debug("parser-sygus") << "Sygus grammar local variable...ignore." << std::endl; }
     | SYGUS_INPUT_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED]
-      { sub_gtermType = 3; Debug("parser-sygus") << "Sygus grammar (input) variable." << std::endl; }
-    | symbol[name,CHECK_NONE,SYM_VARIABLE]
-      { 
+      { sgt.d_gterm_type = SygusGTerm::gterm_input_variable; sgt.d_type = t;Debug("parser-sygus") << "Sygus grammar (input) variable." << std::endl; }
+    | symbol[name,CHECK_NONE,SYM_VARIABLE] { 
         bool isBuiltinOperator = PARSER_STATE->isOperatorEnabled(name);
         if(isBuiltinOperator) {
+          Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : " << name << std::endl;
           k = PARSER_STATE->getOperatorKind(name);
           if( k==CVC4::kind::BITVECTOR_UDIV ){
             k = CVC4::kind::BITVECTOR_UDIV_TOTAL;
           }
-          name = kind::kindToString(k);
-          ops[index].push_back(EXPR_MANAGER->operatorOf(k));
-          cnames[index].push_back( name );
-          sub_gtermType = 0;
+          sgt.d_name = kind::kindToString(k);
+          sgt.d_gterm_type = SygusGTerm::gterm_op;
+          sgt.d_expr = EXPR_MANAGER->operatorOf(k);
         }else{
           // what is this sygus term trying to accomplish here, if the
           // symbol isn't yet declared?!  probably the following line will
@@ -880,148 +915,81 @@ sygusGTerm[int index,
           if( !PARSER_STATE->isDefinedFunction(name) ){
             PARSER_STATE->parseError(std::string("Functions in sygus grammars must be defined."));
           }
-          ops[index].push_back( PARSER_STATE->getVariable(name) );
-          cnames[index].push_back( name );
-          sub_gtermType = 1;
+          sgt.d_name = name;
+          sgt.d_gterm_type = SygusGTerm::gterm_op;
+          sgt.d_expr = PARSER_STATE->getVariable(name) ;
         }
       }
     )
-    { Debug("parser-sygus") << "Read arguments under " << name << ", gtermType = " << sub_gtermType << std::endl;
-      if( sub_gtermType!=5 ){
-        cargs[index].push_back( std::vector< CVC4::Type >() );
-        if( !ops[index].empty()  ){
-          Debug("parser-sygus") << "Operator " << ops[index].back() << std::endl;
-        }
-      }
-      //add datatype definition for argument
-      count++;
-      std::stringstream ss;
-      ss << datatypes[index].getName() << "_" << ops[index].size() << "_arg_" << count;
-      sub_dname = ss.str();
-      PARSER_STATE->pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
-      sub_dt_index = datatypes.size()-1;
-      sub_ret = null_type;
-    }
-    ( sygusGTerm[sub_dt_index,datatypes,sorts,fun,ops,cnames,cargs,allow_const,unresolved_gterm_sym,
-                 sygus_vars,sygus_to_builtin,sygus_to_builtin_expr,sub_ret,sub_gtermType]
-      { Debug("parser-sygus") << "Process argument #" << count << "..." << std::endl;
-        Type tt = PARSER_STATE->processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym, 
-                                                         sygus_to_builtin, sygus_to_builtin_expr, sub_ret );
-        cargs[index].back().push_back(tt);
-        //add next datatype definition for argument
-        count++;
-        std::stringstream ss;
-        ss << datatypes[index].getName() << "_" << ops[index].size() << "_arg_" << count;
-        sub_dname = ss.str();
-        PARSER_STATE->pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
-        sub_dt_index = datatypes.size()-1;
-        sub_ret = null_type;
-      } )* RPAREN_TOK
-      {
-        //pop argument datatype definition
-        PARSER_STATE->popSygusDatatypeDef( datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );       
-        //process constant/variable case 
-        if( sub_gtermType==2 || sub_gtermType==3 || sub_gtermType==4 ){
-          if( !cargs[index].back().empty() ){
-            PARSER_STATE->parseError(std::string("Must provide single sort for constant/variable Sygus constructor."));
-          }
-          cargs[index].pop_back();
-          Debug("parser-sygus") << "Make constructors for Constant/Variable of type " << t << ", gterm type=" << sub_gtermType << std::endl;
-          if( sub_gtermType==2 ){
-            std::vector< Expr > consts;
-            PARSER_STATE->mkSygusConstantsForType( t, consts );
-            Debug("parser-sygus") << "...made " << consts.size() << " constants." << std::endl;
-            for( unsigned i=0; i<consts.size(); i++ ){
-              std::stringstream ss;
-              ss << consts[i];
-              Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl;
-              ops[index].push_back( consts[i] );
-              cnames[index].push_back( ss.str() );
-              cargs[index].push_back( std::vector< CVC4::Type >() );
-            }
-          }else if( sub_gtermType==3 ){
-            Debug("parser-sygus") << "...process " << sygus_vars.size() << " variables." << std::endl;
-            for( unsigned i=0; i<sygus_vars.size(); i++ ){
-              if( sygus_vars[i].getType()==t ){
-                std::stringstream ss;
-                ss << sygus_vars[i];
-                Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl;
-                ops[index].push_back( sygus_vars[i] );
-                cnames[index].push_back( ss.str() );
-                cargs[index].push_back( std::vector< CVC4::Type >() );
-              }
-            }
-          }else if( sub_gtermType==4 ){
-            //local variable, TODO?
-          }
-        }else if( sub_gtermType==5 ){
-          if( (cargs[index].back().size()-let_end_arg_index)!=1 ){
-            PARSER_STATE->parseError(std::string("Must provide single body for let Sygus constructor."));
-          }
-          PARSER_STATE->processSygusLetConstructor( let_vars, index, let_start_index, datatypes, sorts, ops, cnames, cargs, 
-                                                    sygus_vars, sygus_to_builtin, sygus_to_builtin_expr );
-          PARSER_STATE->popScope();
-          //remove datatypes defining body
-          //while( (int)datatypes.size()>let_end_index ){
-          //  Debug("parser-sygus") << "Removing let body datatype " << datatypes[datatypes.size()-1].getName() << std::endl;
-          //  PARSER_STATE->popSygusDatatypeDef( datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
-          //}
-          //Debug("parser-sygus") << "Done let body datatypes" << std::endl;
-        }else{
-          if( cargs[index].back().empty() ){
-            PARSER_STATE->parseError(std::string("Must provide argument for Sygus constructor."));
-          }
-        }
+    //read arguments
+    { Debug("parser-sygus") << "Read arguments under " << sgt.d_name << std::endl;
+      sgt.addChild();
+    }
+    ( sygusGTerm[sgt.d_children.back(), fun]
+      { Debug("parser-sygus") << "Finished read argument #" << sgt.d_children.size() << "..." << std::endl;
+        sgt.addChild();
+      } )* 
+    RPAREN_TOK {
+      //pop last child index 
+      sgt.d_children.pop_back();   
+      if( readingLet ){
+        PARSER_STATE->popScope();
       }
+    }
   | INTEGER_LITERAL
     { Debug("parser-sygus") << "Sygus grammar " << fun << " : integer literal " << AntlrInput::tokenText($INTEGER_LITERAL) << std::endl;
-      ops[index].push_back(MK_CONST(Rational(AntlrInput::tokenText($INTEGER_LITERAL))));
-      cnames[index].push_back( AntlrInput::tokenText($INTEGER_LITERAL) );
-      cargs[index].push_back( std::vector< CVC4::Type >() );
+      sgt.d_expr = MK_CONST(Rational(AntlrInput::tokenText($INTEGER_LITERAL)));
+      sgt.d_name = AntlrInput::tokenText($INTEGER_LITERAL);
+      sgt.d_gterm_type = SygusGTerm::gterm_op;
     }
   | HEX_LITERAL
     { Debug("parser-sygus") << "Sygus grammar " << fun << " : hex literal " << AntlrInput::tokenText($HEX_LITERAL) << std::endl;
       assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 );
       std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
-      ops[index].push_back(MK_CONST( BitVector(hexString, 16) ));
-      cnames[index].push_back( AntlrInput::tokenText($HEX_LITERAL) );
-      cargs[index].push_back( std::vector< CVC4::Type >() );
+      sgt.d_expr = MK_CONST( BitVector(hexString, 16) );
+      sgt.d_name = AntlrInput::tokenText($HEX_LITERAL);
+      sgt.d_gterm_type = SygusGTerm::gterm_op;
     }
   | BINARY_LITERAL
     { Debug("parser-sygus") << "Sygus grammar " << fun << " : binary literal " << AntlrInput::tokenText($BINARY_LITERAL) << std::endl;
       assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 );
       std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
-      ops[index].push_back(MK_CONST( BitVector(binString, 2) ));
-      cnames[index].push_back( AntlrInput::tokenText($BINARY_LITERAL) );
-      cargs[index].push_back( std::vector< CVC4::Type >() );
-    }
-  | symbol[name,CHECK_NONE,SYM_VARIABLE]
-    { if( name[0] == '-' ){  //hack for unary minus
-        Debug("parser-sygus") << "Sygus grammar " << fun << " : unary minus integer literal " << name << std::endl;
-        ops[index].push_back(MK_CONST(Rational(name)));
-        cnames[index].push_back( name );
-        cargs[index].push_back( std::vector< CVC4::Type >() );
-      }else if( PARSER_STATE->isDeclared(name,SYM_VARIABLE) ){
-        Debug("parser-sygus") << "Sygus grammar " << fun << " : symbol " << name << std::endl;
-        Expr bv = PARSER_STATE->getVariable(name);
-        ops[index].push_back(bv);
-        cnames[index].push_back( name );
-        cargs[index].push_back( std::vector< CVC4::Type >() );
+      sgt.d_expr = MK_CONST( BitVector(binString, 2) );
+      sgt.d_name = AntlrInput::tokenText($BINARY_LITERAL);
+      sgt.d_gterm_type = SygusGTerm::gterm_op;
+    }
+  | symbol[name,CHECK_NONE,SYM_VARIABLE] ( SYGUS_ENUM_CONS_TOK symbol[name2,CHECK_NONE,SYM_VARIABLE] { readEnum = true; } )?
+    { if( readEnum ){
+        name = name + "__Enum__" + name2;
+        Debug("parser-sygus") << "Sygus grammar " << fun << " : Enum constant " << name << std::endl;
+        Expr c = PARSER_STATE->getVariable(name);
+        sgt.d_expr = MK_EXPR(kind::APPLY_CONSTRUCTOR,c);
+        sgt.d_name = name;
+        sgt.d_gterm_type = SygusGTerm::gterm_op;
       }else{
-        //prepend function name to base sorts when reading an operator
-        std::stringstream ss;
-        ss << fun << "_" << name;
-        name = ss.str();
-        if( PARSER_STATE->isDeclared(name, SYM_SORT) ){
-          Debug("parser-sygus") << "Sygus grammar " << fun << " : nested sort " << name << std::endl;
-          ret = PARSER_STATE->getSort(name);
+        if( name[0] == '-' ){  //hack for unary minus
+          Debug("parser-sygus") << "Sygus grammar " << fun << " : unary minus integer literal " << name << std::endl;
+          sgt.d_expr = MK_CONST(Rational(name));
+          sgt.d_name = name;
+          sgt.d_gterm_type = SygusGTerm::gterm_op;
+        }else if( PARSER_STATE->isDeclared(name,SYM_VARIABLE) ){
+          Debug("parser-sygus") << "Sygus grammar " << fun << " : symbol " << name << std::endl;
+          sgt.d_expr = PARSER_STATE->getVariable(name);
+          sgt.d_name = name;
+          sgt.d_gterm_type = SygusGTerm::gterm_op;
         }else{
-          if( gtermType==-1 ){
-            Debug("parser-sygus") << "Sygus grammar " << fun << " : unresolved symbol " << name << std::endl;
-            unresolved_gterm_sym[index].push_back(name);
+          //prepend function name to base sorts when reading an operator
+          std::stringstream ss;
+          ss << fun << "_" << name;
+          name = ss.str();
+          if( PARSER_STATE->isDeclared(name, SYM_SORT) ){
+            Debug("parser-sygus") << "Sygus grammar " << fun << " : nested sort " << name << std::endl;
+            sgt.d_type = PARSER_STATE->getSort(name);
+            sgt.d_gterm_type = SygusGTerm::gterm_nested_sort;
           }else{
-            Debug("parser-sygus") << "Sygus grammar " << fun << " : unresolved " << name << std::endl;
-            ret = PARSER_STATE->mkUnresolvedType(name);
+            Debug("parser-sygus") << "Sygus grammar " << fun << " : unresolved symbol " << name << std::endl;
+            sgt.d_gterm_type = SygusGTerm::gterm_unresolved;
+            sgt.d_name = name;
           }
         }
       }
@@ -1612,7 +1580,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
   Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
   Kind kind = kind::NULL_EXPR;
   Expr op;
-  std::string name;
+  std::string name, name2;
   std::vector<Expr> args;
   std::vector< std::pair<std::string, Type> > sortedVarNames;
   Expr f, f2, f3, f4;
@@ -1624,6 +1592,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
   Type type;
   std::string s;
   bool isBuiltinOperator = false;
+  bool readLetSort = false;
 }
   : /* a built-in operator application */
     LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK
@@ -1824,10 +1793,12 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
   | /* a let binding */
     LPAREN_TOK LET_TOK LPAREN_TOK
     { PARSER_STATE->pushScope(true); }
-    ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] term[expr, f2] RPAREN_TOK
+    ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] (term[expr, f2] | sortSymbol[type,CHECK_DECLARED] { readLetSort = true; } term[expr, f2] ) RPAREN_TOK
       // this is a parallel let, so we have to save up all the contributions
       // of the let and define them only later on
-      { if(names.count(name) == 1) {
+      { if( readLetSort!=PARSER_STATE->sygus() ){
+          PARSER_STATE->parseError("Bad syntax for let term.");
+        }else if(names.count(name) == 1) {
           std::stringstream ss;
           ss << "warning: symbol `" << name << "' bound multiple times by let; the last binding will be used, shadowing earlier ones";
           PARSER_STATE->warning(ss.str());
@@ -1844,7 +1815,13 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
     term[expr, f2]
     RPAREN_TOK
     { PARSER_STATE->popScope(); }
-
+  | symbol[name,CHECK_NONE,SYM_VARIABLE] SYGUS_ENUM_CONS_TOK symbol[name2,CHECK_NONE,SYM_VARIABLE] {
+      std::string cname = name + "__Enum__" + name2;
+      Debug("parser-sygus") << "Check for enum const " << cname << std::endl;
+      expr = PARSER_STATE->getVariable(cname);
+      //expr.getType().isConstructor() && ConstructorType(expr.getType()).getArity()==0;
+      expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, expr);
+    }
     /* a variable */
   | symbol[name,CHECK_DECLARED,SYM_VARIABLE]
     { if( PARSER_STATE->sygus() && name[0]=='-' && 
@@ -2502,8 +2479,11 @@ symbol[std::string& id,
      * use as symbols in SMT-LIB */
     | SET_OPTIONS_TOK { id = "set-options"; }
     | DECLARE_VAR_TOK { id = "declare-var"; }
+    | DECLARE_PRIMED_VAR_TOK { id = "declare-primed-var"; }
     | SYNTH_FUN_TOK { id = "synth-fun"; }
+    | SYNTH_INV_TOK { id = "synth-inv"; }
     | CONSTRAINT_TOK { id = "constraint"; }
+    | INV_CONSTRAINT_TOK { id = "inv-constraint"; }
     | CHECK_SYNTH_TOK { id = "check-synth"; }
     )
     { PARSER_STATE->checkDeclaration(id, check, type); }
@@ -2653,10 +2633,15 @@ INCLUDE_TOK : 'include';
 
 // SyGuS commands
 SYNTH_FUN_TOK : 'synth-fun';
+SYNTH_INV_TOK : 'synth-inv';
 CHECK_SYNTH_TOK : 'check-synth';
 DECLARE_VAR_TOK : 'declare-var';
+DECLARE_PRIMED_VAR_TOK : 'declare-primed-var';
 CONSTRAINT_TOK : 'constraint';
+INV_CONSTRAINT_TOK : 'inv-constraint';
 SET_OPTIONS_TOK : 'set-options';
+SYGUS_ENUM_TOK : { PARSER_STATE->sygus() }? 'Enum';
+SYGUS_ENUM_CONS_TOK : { PARSER_STATE->sygus() }? '::';
 SYGUS_CONSTANT_TOK : { PARSER_STATE->sygus() }? 'Constant';
 SYGUS_VARIABLE_TOK : { PARSER_STATE->sygus() }? 'Variable';
 SYGUS_INPUT_VARIABLE_TOK : { PARSER_STATE->sygus() }? 'InputVariable';
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 3420a3e7f..b8c4793d4 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -81,6 +81,8 @@ void Smt2::addBitvectorOperators() {
   addOperator(kind::BITVECTOR_SLE, "bvsle");
   addOperator(kind::BITVECTOR_SGT, "bvsgt");
   addOperator(kind::BITVECTOR_SGE, "bvsge");
+  addOperator(kind::BITVECTOR_REDOR, "bvredor");
+  addOperator(kind::BITVECTOR_REDAND, "bvredand");
 
   Parser::addOperator(kind::BITVECTOR_BITOF);
   Parser::addOperator(kind::BITVECTOR_EXTRACT);
@@ -347,9 +349,6 @@ void Smt2::setLogic(std::string name) {
       ss << "Unknown SyGuS background logic `" << name << "'";
       parseError(ss.str());
     }
-    //TODO : add additional non-standard define-funs here
-    
-    
   }
 
   d_logicSet = true;
@@ -499,27 +498,120 @@ void Smt2::includeFile(const std::string& filename) {
   }
 }
 
-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 ) {
+Expr Smt2::mkSygusVar(const std::string& name, const Type& type, bool isPrimed) {
+  Expr e = mkBoundVar(name, type);
+  d_sygusVars.push_back(e);
+  d_sygusVarPrimed[e] = false;
+  if( isPrimed ){
+    std::stringstream ss;
+    ss << name << "'";
+    Expr ep = mkBoundVar(ss.str(), type);
+    d_sygusVars.push_back(ep);
+    d_sygusVarPrimed[ep] = true;
+  }
+  return e;
+}
 
+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 ) {
+  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;
+  for( unsigned i=0; i<sygus_vars.size(); i++ ){
+    Type t = sygus_vars[i].getType();
+    if( !t.isBoolean() && std::find( types.begin(), types.end(), t )==types.end() ){
+      types.push_back( t );
+    }
+  }
+  
+  //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;
+  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>());
+    std::vector<std::string> cnames;
+    std::vector<std::vector<CVC4::Type> > cargs;
+    std::vector<std::string> unresolved_gterm_sym;
+    //make unresolved type
+    Type unres_t = mkUnresolvedType(dname);
+    unres_types.push_back(unres_t);
+    //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.back().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.back().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.back().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.back().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{
+      std::stringstream sserr;
+      sserr << "No implementation for default Sygus grammar of type " << types[i] << std::endl;
+      warning(sserr.str());
+    }
+    Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl;
+    datatypes.back().setSygus( types[i], bvl, true, true );
+    mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs, unresolved_gterm_sym, sygus_to_builtin );
+    sorts.push_back( types[i] );
+    //set start index if applicable
+    if( types[i]==range ){
+      startIndex = i;
+    }
+  }
 
-  std::stringstream ss;
-  ss << fun << "_" << range;
-  std::string dname = ss.str();
-  datatypes.push_back(Datatype(dname));
+  //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;
-  //variables
+  //add variables
   for( unsigned i=0; i<sygus_vars.size(); i++ ){
-    if( sygus_vars[i].getType()==range ){
+    if( sygus_vars[i].getType().isBoolean() ){
       std::stringstream ss;
       ss << sygus_vars[i];
       Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl;
@@ -528,79 +620,60 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin
       cargs.push_back( std::vector< CVC4::Type >() );
     }
   }
-  //constants
-  std::vector< Expr > consts;
-  mkSygusConstantsForType( range, consts );
-  for( unsigned i=0; i<consts.size(); i++ ){
-    std::stringstream ss;
-    ss << consts[i];
-    Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl;
-    ops.back().push_back( consts[i] );
-    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.back().push_back(getExprManager()->operatorOf(k));
-  cnames.push_back( kind::kindToString(k) );
-  cargs.push_back( std::vector< CVC4::Type >() );
-  cargs.back().push_back(mkUnresolvedType(ssb.str()));
-  cargs.back().push_back(mkUnresolvedType(ss.str()));
-  cargs.back().push_back(mkUnresolvedType(ss.str()));
-
-  if( range.isInteger() ){
-    for( unsigned i=0; i<2; i++ ){
-      CVC4::Kind k = i==0 ? kind::PLUS : kind::MINUS;
-      Debug("parser-sygus") << "...add for " << k << std::endl;
-      ops.back().push_back(getExprManager()->operatorOf(k));
-      cnames.push_back(kind::kindToString(k));
+  //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 >() );
-      cargs.back().push_back(mkUnresolvedType(ss.str()));
-      cargs.back().push_back(mkUnresolvedType(ss.str()));
     }
-  }else{
-    std::stringstream sserr;
-    sserr << "Don't know default Sygus grammar for type " << range << std::endl;
-    parseError(sserr.str());
   }
-  Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl;
-  datatypes.back().setSygus( range, bvl, true, true );
-  mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs, unresolved_gterm_sym, sygus_to_builtin );
-  sorts.push_back( range );
-
-  //Boolean type
-  datatypes.push_back(Datatype(dbname));
-  ops.push_back(std::vector<Expr>());
-  cnames.clear();
-  cargs.clear();
-  for( unsigned i=0; i<4; i++ ){
-    CVC4::Kind k = i==0 ? kind::NOT : ( i==1 ? kind::AND : ( i==2 ? kind::OR : kind::EQUAL ) );
+  //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(mkUnresolvedType(ssb.str()));
+      cargs.back().push_back(unres_bt);
     }else if( k==kind::AND || k==kind::OR ){
-      cargs.back().push_back(mkUnresolvedType(ssb.str()));
-      cargs.back().push_back(mkUnresolvedType(ssb.str()));
-    }else if( k==kind::EQUAL ){
-      cargs.back().push_back(mkUnresolvedType(ss.str()));
-      cargs.back().push_back(mkUnresolvedType(ss.str()));
+      cargs.back().push_back(unres_bt);
+      cargs.back().push_back(unres_bt);
     }
   }
-  if( range.isInteger() ){
-    CVC4::Kind k = kind::LEQ;
+  //add predicates for types
+  for( unsigned i=0; i<types.size(); i++ ){
+    //add equality per type
+    CVC4::Kind k = kind::EQUAL;
     Debug("parser-sygus") << "...add for " << k << std::endl;
     ops.back().push_back(getExprManager()->operatorOf(k));
-    cnames.push_back(kind::kindToString(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(mkUnresolvedType(ss.str()));
-    cargs.back().push_back(mkUnresolvedType(ss.str()));
+    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]);
+    }
+  }
+  if( range==btype ){
+    startIndex = sorts.size();
   }
   Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl;
-  Type btype = getExprManager()->booleanType();
   datatypes.back().setSygus( btype, bvl, true, true );
   mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs, unresolved_gterm_sym, sygus_to_builtin );
   sorts.push_back( btype );
@@ -618,10 +691,109 @@ void Smt2::mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& o
     ops.push_back( getExprManager()->mkConst(bval0) );
     BitVector bval1(sz, (unsigned int)1);
     ops.push_back( getExprManager()->mkConst(bval1) );
+  }else if( type.isBoolean() ){
+    ops.push_back(getExprManager()->mkConst(true));
+    ops.push_back(getExprManager()->mkConst(false));
   }
   //TODO : others?
 }
 
+//  This method adds N operators to ops[index], N names to cnames[index] and N type argument vectors to cargs[index] (where typically N=1)
+//  This method may also add new elements pairwise into datatypes/sorts/ops/cnames/cargs in the case of non-flat gterms.
+void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index,                               
+                              std::vector< CVC4::Datatype >& datatypes,
+                              std::vector< CVC4::Type>& sorts,
+                              std::vector< std::vector<CVC4::Expr> >& ops,
+                              std::vector< std::vector<std::string> >& cnames,
+                              std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
+                              std::vector< bool >& allow_const,
+                              std::vector< std::vector< std::string > >& unresolved_gterm_sym,
+                              std::vector<CVC4::Expr>& sygus_vars, 
+                              std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, 
+                              CVC4::Type& ret, bool isNested ){
+  if( sgt.d_gterm_type==SygusGTerm::gterm_op || sgt.d_gterm_type==SygusGTerm::gterm_let ){
+    Debug("parser-sygus") << "Add " << sgt.d_expr << " to datatype " << index << std::endl;
+    //convert to UMINUS if one child of -
+    if( sgt.d_children.size()==1 && sgt.d_expr==getExprManager()->operatorOf(kind::MINUS) ){
+      sgt.d_expr = getExprManager()->operatorOf(kind::UMINUS);
+    }
+    ops[index].push_back( sgt.d_expr );
+    cnames[index].push_back( sgt.d_name );
+    cargs[index].push_back( std::vector< CVC4::Type >() );
+    for( unsigned i=0; i<sgt.d_children.size(); i++ ){
+      std::stringstream ss;
+      ss << datatypes[index].getName() << "_" << ops[index].size() << "_arg_" << i;
+      std::string sub_dname = ss.str();
+      //add datatype for child
+      Type null_type;
+      pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
+      int sub_dt_index = datatypes.size()-1;
+      //process child
+      Type sub_ret;
+      processSygusGTerm( sgt.d_children[i], sub_dt_index, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym, 
+                         sygus_vars, sygus_to_builtin, sygus_to_builtin_expr, sub_ret, true );
+      //process the nested gterm (either pop the last datatype, or flatten the argument)
+      Type tt = processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym, 
+                                         sygus_to_builtin, sygus_to_builtin_expr, sub_ret );
+      cargs[index].back().push_back(tt);
+    }
+    //if let, must create operator
+    if( sgt.d_gterm_type==SygusGTerm::gterm_let ){
+      processSygusLetConstructor( sgt.d_let_vars, index, datatypes, sorts, ops, cnames, cargs, 
+                                  sygus_vars, sygus_to_builtin, sygus_to_builtin_expr );
+    }
+  }else if( sgt.d_gterm_type==SygusGTerm::gterm_constant ){
+    if( sgt.getNumChildren()!=0 ){
+      parseError("Bad syntax for Sygus Constant.");
+    }
+    std::vector< Expr > consts;
+    mkSygusConstantsForType( sgt.d_type, consts );
+    Debug("parser-sygus") << "...made " << consts.size() << " constants." << std::endl;
+    for( unsigned i=0; i<consts.size(); i++ ){
+      std::stringstream ss;
+      ss << consts[i];
+      Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl;
+      ops[index].push_back( consts[i] );
+      cnames[index].push_back( ss.str() );
+      cargs[index].push_back( std::vector< CVC4::Type >() );
+    }
+    allow_const[index] = true;
+  }else if( sgt.d_gterm_type==SygusGTerm::gterm_variable || sgt.d_gterm_type==SygusGTerm::gterm_input_variable ){
+    if( sgt.getNumChildren()!=0 ){
+      parseError("Bad syntax for Sygus Variable.");
+    }
+    Debug("parser-sygus") << "...process " << sygus_vars.size() << " variables." << std::endl;
+    for( unsigned i=0; i<sygus_vars.size(); i++ ){
+      if( sygus_vars[i].getType()==sgt.d_type ){
+        std::stringstream ss;
+        ss << sygus_vars[i];
+        Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl;
+        ops[index].push_back( sygus_vars[i] );
+        cnames[index].push_back( ss.str() );
+        cargs[index].push_back( std::vector< CVC4::Type >() );
+      }
+    }
+  }else if( sgt.d_gterm_type==SygusGTerm::gterm_nested_sort ){
+    ret = sgt.d_type;
+  }else if( sgt.d_gterm_type==SygusGTerm::gterm_unresolved ){
+    if( isNested ){
+      if( isUnresolvedType(sgt.d_name) ){
+        ret = getSort(sgt.d_name);
+      }else{
+        //nested, unresolved symbol...fail
+        std::stringstream ss;
+        ss << "Cannot handle nested unresolved symbol " << sgt.d_name << std::endl;
+        parseError(ss.str());
+      }
+    }else{
+      //will resolve when adding constructors
+      unresolved_gterm_sym[index].push_back(sgt.d_name);
+    }
+  }else if( sgt.d_gterm_type==SygusGTerm::gterm_ignore ){
+    
+  }
+}
+
 bool Smt2::pushSygusDatatypeDef( Type t, std::string& dname,
                                   std::vector< CVC4::Datatype >& datatypes,
                                   std::vector< CVC4::Type>& sorts,
@@ -694,6 +866,15 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st
       for( unsigned i=0; i<cargs[sub_dt_index][0].size(); i++ ){
         std::map< CVC4::Type, CVC4::Expr >::iterator it = sygus_to_builtin_expr.find( cargs[sub_dt_index][0][i] );
         if( it==sygus_to_builtin_expr.end() ){
+          if( sygus_to_builtin.find( cargs[sub_dt_index][0][i] )==sygus_to_builtin.end() ){
+            std::stringstream ss;
+            ss << "Missing builtin type for type " << cargs[sub_dt_index][0][i] << "!" << std::endl;
+            ss << "Builtin types are currently : " << std::endl;
+            for( std::map< CVC4::Type, CVC4::Type >::iterator itb = sygus_to_builtin.begin(); itb != sygus_to_builtin.end(); ++itb ){
+              ss << "  " << itb->first << " -> " << itb->second << std::endl;
+            }
+            parseError(ss.str());
+          }
           Type bt = sygus_to_builtin[cargs[sub_dt_index][0][i]];
           Debug("parser-sygus") << ":  child " << i << " introduce type elem for " << cargs[sub_dt_index][0][i] << " " << bt << std::endl;
           std::stringstream ss;
@@ -726,7 +907,7 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st
 }
 
 void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars,
-                                       int index, int start_index,
+                                       int index, 
                                        std::vector< CVC4::Datatype >& datatypes,
                                        std::vector< CVC4::Type>& sorts,
                                        std::vector< std::vector<CVC4::Expr> >& ops,
@@ -760,6 +941,7 @@ void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars,
     Debug("parser-sygus") << "  let var " << i << " : " << let_vars[i] << " " << let_vars[i].getType() << std::endl;
     let_define_args.push_back( let_vars[i] );
   }
+  /*
   Debug("parser-sygus") << "index = " << index << ", start index = " << start_index << ", #Current datatypes = " << datatypes.size() << std::endl;
   for( unsigned i=start_index; i<datatypes.size(); i++ ){
     Debug("parser-sygus") << "  datatype " << i << " : " << datatypes[i].getName() << ", #cons = " << cargs[i].size() << std::endl;
@@ -772,6 +954,7 @@ void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars,
       }
     }
   } 
+  */
   //last argument is the return, pop
   cargs[index][dindex].pop_back();
   collectSygusLetArgs( let_body, cargs[index][dindex], let_define_args );  
@@ -819,6 +1002,29 @@ void Smt2::collectSygusLetArgs( CVC4::Expr e, std::vector< CVC4::Type >& sygusAr
   }
 }
 
+void Smt2::setSygusStartIndex( std::string& fun, int startIndex, 
+                               std::vector< CVC4::Datatype >& datatypes,
+                               std::vector< CVC4::Type>& sorts,
+                               std::vector< std::vector<CVC4::Expr> >& ops ) {
+  if( startIndex>0 ){
+    CVC4::Datatype tmp_dt = datatypes[0];
+    Type tmp_sort = sorts[0];
+    std::vector< Expr > tmp_ops;
+    tmp_ops.insert( tmp_ops.end(), ops[0].begin(), ops[0].end() );
+    datatypes[0] = datatypes[startIndex];
+    sorts[0] = sorts[startIndex];
+    ops[0].clear();
+    ops[0].insert( ops[0].end(), ops[startIndex].begin(), ops[startIndex].end() );
+    datatypes[startIndex] = tmp_dt;
+    sorts[startIndex] = tmp_sort;
+    ops[startIndex].clear();
+    ops[startIndex].insert( ops[startIndex].begin(), tmp_ops.begin(), tmp_ops.end() );
+  }else if( startIndex<0 ){
+    std::stringstream ss;
+    ss << "warning: no symbol named Start for synth-fun " << fun << std::endl;
+    warning(ss.str());
+  }
+}
 
 void Smt2::defineSygusFuns() {
   // only define each one once
@@ -877,6 +1083,7 @@ void Smt2::defineSygusFuns() {
     }
     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);
 
@@ -1159,6 +1366,19 @@ Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vec
   return assertion;
 }
 
+const void Smt2::getSygusPrimedVars( std::vector<Expr>& vars, bool isPrimed ) {
+  for( unsigned i=0; i<d_sygusVars.size(); i++ ){
+    Expr v = d_sygusVars[i];
+    std::map< Expr, bool >::iterator it = d_sygusVarPrimed.find( v );
+    if( it!=d_sygusVarPrimed.end() ){
+      if( it->second==isPrimed ){
+        vars.push_back( v );
+      }
+    }else{
+      //should never happen
+    }
+  }
+}
 
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 275c8a83a..c88f7cd8f 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -35,7 +35,7 @@ namespace CVC4 {
 class SExpr;
 
 namespace parser {
-
+  
 class Smt2 : public Parser {
   friend class ParserBuilder;
 
@@ -64,6 +64,7 @@ private:
   std::stack< std::map<Expr, std::string> > d_unsatCoreNames;
   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:
@@ -172,17 +173,25 @@ public:
     return getExprManager()->mkConst(AbstractValue(Integer(name.substr(1))));
   }
 
-  Expr mkSygusVar(const std::string& name, const Type& type) {
-    Expr e = mkBoundVar(name, type);
-    d_sygusVars.push_back(e);
-    return e;
-  }
+  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 );
+                              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,                                
+                          std::vector< CVC4::Datatype >& datatypes,
+                          std::vector< CVC4::Type>& sorts,
+                          std::vector< std::vector<CVC4::Expr> >& ops,
+                          std::vector< std::vector<std::string> >& cnames,
+                          std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
+                          std::vector< bool >& allow_const,
+                          std::vector< std::vector< std::string > >& unresolved_gterm_sym,
+                          std::vector<CVC4::Expr>& sygus_vars, 
+                          std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, 
+                          CVC4::Type& ret, bool isNested = false );
+  
   static bool pushSygusDatatypeDef( Type t, std::string& dname,
                                     std::vector< CVC4::Datatype >& datatypes,
                                     std::vector< CVC4::Type>& sorts,
@@ -199,28 +208,11 @@ public:
                                    std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
                                    std::vector< bool >& allow_const,
                                    std::vector< std::vector< std::string > >& unresolved_gterm_sym );
-
-  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,
-                                std::vector< std::vector<std::string> >& cnames,
-                                std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
-                                std::vector< bool >& allow_const,
-                                std::vector< std::vector< std::string > >& unresolved_gterm_sym,
-                                std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin,
-                                std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, Type sub_ret );
-
-  void processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars,
-                                   int index, int start_index,
-                                   std::vector< CVC4::Datatype >& datatypes,
-                                   std::vector< CVC4::Type>& sorts,
-                                   std::vector< std::vector<CVC4::Expr> >& ops,
-                                   std::vector< std::vector<std::string> >& cnames,
-                                   std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
-                                   std::vector<CVC4::Expr>& sygus_vars, 
-                                   std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin,
-                                   std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr );
   
+  void setSygusStartIndex( std::string& fun, int startIndex, 
+                           std::vector< CVC4::Datatype >& datatypes,
+                           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));
@@ -238,6 +230,8 @@ public:
   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 +248,7 @@ public:
   const std::vector<Expr>& getSygusVars() {
     return d_sygusVars;
   }
+  const void getSygusPrimedVars( std::vector<Expr>& vars, bool isPrimed );
 
   const std::vector<Expr>& getSygusFunSymbols() {
     return d_sygusFunSymbols;
@@ -322,6 +317,26 @@ private:
   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,
+                                std::vector< std::vector<std::string> >& cnames,
+                                std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
+                                std::vector< bool >& allow_const,
+                                std::vector< std::vector< std::string > >& unresolved_gterm_sym,
+                                std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin,
+                                std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, Type sub_ret );
+
+  void processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars, int index, 
+                                   std::vector< CVC4::Datatype >& datatypes,
+                                   std::vector< CVC4::Type>& sorts,
+                                   std::vector< std::vector<CVC4::Expr> >& ops,
+                                   std::vector< std::vector<std::string> >& cnames,
+                                   std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
+                                   std::vector<CVC4::Expr>& sygus_vars, 
+                                   std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin,
+                                   std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr );
+  
   void addArithmeticOperators();
 
   void addBitvectorOperators();
diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h
index c6a94f07a..a1baa98cb 100644
--- a/src/parser/smt2/smt2_input.h
+++ b/src/parser/smt2/smt2_input.h
@@ -26,7 +26,7 @@
 // extern void Smt2ParserSetAntlrParser(CVC4::parser::AntlrParser* newAntlrParser);
 
 namespace CVC4 {
-
+  
 class Command;
 class Expr;
 class ExprManager;