From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 20 Jul 2015 17:46:21 +0000 (+0200)
Subject: Squashed merge of SygusComp 2015 branch.
X-Git-Tag: cvc5-1.0.0~6267^2~2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f62d9456b41bf17df1d339e46776c9213cb3705a;p=cvc5.git

Squashed merge of SygusComp 2015 branch.
---

diff --git a/src/Makefile.am b/src/Makefile.am
index 16ac45de2..b0d97754d 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -335,6 +335,8 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/local_theory_ext.cpp \
 	theory/quantifiers/fun_def_process.h \
 	theory/quantifiers/fun_def_process.cpp \
+	theory/quantifiers/fun_def_engine.h \
+	theory/quantifiers/fun_def_engine.cpp \
 	theory/quantifiers/options_handlers.h \
 	theory/arith/theory_arith_type_rules.h \
 	theory/arith/type_enumerator.h \
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 53241709d..9c2c7f7be 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -42,6 +42,33 @@ class FunctionType;
 class Type;
 class ResourceManager;
 
+//for sygus gterm two-pass parsing
+class CVC4_PUBLIC SygusGTerm {
+public:
+  enum{
+    gterm_op,
+    gterm_let,
+    gterm_constant,
+    gterm_variable,
+    gterm_input_variable,
+    gterm_local_variable,
+    gterm_nested_sort,
+    gterm_unresolved,
+    gterm_ignore,
+  };
+  Type d_type;
+  Expr d_expr;
+  std::vector< Expr > d_let_vars;
+  unsigned d_gterm_type;
+  std::string d_name;
+  std::vector< SygusGTerm > d_children;
+  
+  unsigned getNumChildren() { return d_children.size(); }
+  void addChild(){
+    d_children.push_back( SygusGTerm() );
+  }
+};
+
 namespace parser {
 
 class Input;
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;
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 5cc044272..822818c43 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -46,7 +46,7 @@ static void printBvParameterizedOp(std::ostream& out, TNode n) throw();
 static void printFpParameterizedOp(std::ostream& out, TNode n) throw();
 
 static void toStreamRational(std::ostream& out, const Rational& r, bool decimal) throw();
-  
+
 void Smt2Printer::toStream(std::ostream& out, TNode n,
                            int toDepth, bool types, size_t dag) const throw() {
   if(dag != 0) {
@@ -160,17 +160,22 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
       break;
     case kind::FLOATINGPOINT_TYPE:
       out << "(_ FloatingPoint "
-	  << n.getConst<FloatingPointSize>().exponent() << " "
-	  << n.getConst<FloatingPointSize>().significand()
-	  << ")";
+          << n.getConst<FloatingPointSize>().exponent() << " "
+          << n.getConst<FloatingPointSize>().significand()
+          << ")";
       break;
     case kind::CONST_BITVECTOR: {
       const BitVector& bv = n.getConst<BitVector>();
       const Integer& x = bv.getValue();
       unsigned n = bv.getSize();
-      out << "(_ ";
-      out << "bv" << x <<" " << n;
-      out << ")";
+      if(d_variant == sygus_variant ){
+        out << "#b" << bv.toString();
+      }else{
+        out << "(_ ";
+        out << "bv" << x <<" " << n;
+        out << ")";
+      }
+
       // //out << "#b";
 
       // while(n-- > 0) {
@@ -189,7 +194,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
       case roundTowardNegative : out << "roundTowardNegative"; break;
       case roundTowardZero : out << "roundTowardZero"; break;
       default :
-	Unreachable("Invalid value of rounding mode constant (%d)",n.getConst<RoundingMode>());
+        Unreachable("Invalid value of rounding mode constant (%d)",n.getConst<RoundingMode>());
       }
       break;
     case kind::CONST_BOOLEAN:
@@ -205,7 +210,15 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
       break;
     case kind::CONST_RATIONAL: {
       const Rational& r = n.getConst<Rational>();
-      toStreamRational(out, r, false);
+      if(d_variant == sygus_variant ){
+        if(r < 0) {
+          out << "-" << -r;
+        }else{
+          toStreamRational(out, r, false);
+        }
+      }else{
+        toStreamRational(out, r, false);
+      }
       // Rational r = n.getConst<Rational>();
       // if(r < 0) {
       //   if(r.isIntegral()) {
@@ -467,6 +480,8 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::BITVECTOR_SGT: out << "bvsgt "; break;
   case kind::BITVECTOR_SGE: out << "bvsge "; break;
   case kind::BITVECTOR_TO_NAT: out << "bv2nat "; break;
+  case kind::BITVECTOR_REDOR: out << "bvredor "; break;
+  case kind::BITVECTOR_REDAND: out << "bvredand "; break;
 
   case kind::BITVECTOR_EXTRACT:
   case kind::BITVECTOR_REPEAT:
@@ -540,13 +555,13 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
         // Special case, in model output integer constants that should be
         // Real-sorted are wrapped in a type ascription.  Handle that here.
 
-	// Note: This is Tim making a guess about Morgan's Code.
-	Assert(n[0].getKind() == kind::CONST_RATIONAL);	
-	toStreamRational(out, n[0].getConst<Rational>(), true);
+        // Note: This is Tim making a guess about Morgan's Code.
+        Assert(n[0].getKind() == kind::CONST_RATIONAL);
+        toStreamRational(out, n[0].getConst<Rational>(), true);
 
         //toStream(out, n[0], -1, false);
         //out << ".0";
-	
+
         return;
       }
       out << "(as ";
@@ -555,8 +570,8 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
       return;
     }
     break;
-  case kind::APPLY_TESTER:
   case kind::APPLY_CONSTRUCTOR:
+  case kind::APPLY_TESTER:
   case kind::APPLY_SELECTOR:
   case kind::APPLY_SELECTOR_TOTAL:
   case kind::PARAMETRIC_DATATYPE:
@@ -625,7 +640,18 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   if( n.getMetaKind() == kind::metakind::PARAMETERIZED &&
       stillNeedToPrintParams ) {
     if(toDepth != 0) {
-      toStream(out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types);
+      if( d_variant==sygus_variant && n.getKind()==kind::APPLY_CONSTRUCTOR ){
+        std::stringstream ss;
+        toStream(ss, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types);
+        std::string tmp = ss.str();
+        size_t pos = 0;
+        if((pos = tmp.find("__Enum__", pos)) != std::string::npos){
+           tmp.replace(pos, 8, "::");
+        }
+        out << tmp;
+      }else{
+        toStream(out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types);
+      }
     } else {
       out << "(...)";
     }
@@ -719,6 +745,7 @@ static string smtKindString(Kind k) throw() {
   case kind::BITVECTOR_PLUS: return "bvadd";
   case kind::BITVECTOR_SUB: return "bvsub";
   case kind::BITVECTOR_NEG: return "bvneg";
+  case kind::BITVECTOR_UDIV_TOTAL:
   case kind::BITVECTOR_UDIV: return "bvudiv";
   case kind::BITVECTOR_UREM: return "bvurem";
   case kind::BITVECTOR_SDIV: return "bvsdiv";
@@ -735,6 +762,8 @@ static string smtKindString(Kind k) throw() {
   case kind::BITVECTOR_SLE: return "bvsle";
   case kind::BITVECTOR_SGT: return "bvsgt";
   case kind::BITVECTOR_SGE: return "bvsge";
+  case kind::BITVECTOR_REDOR: return "bvredor";
+  case kind::BITVECTOR_REDAND: return "bvredand";
 
   case kind::BITVECTOR_EXTRACT: return "extract";
   case kind::BITVECTOR_REPEAT: return "repeat";
@@ -775,7 +804,7 @@ static string smtKindString(Kind k) throw() {
 
   case kind::FLOATINGPOINT_ISN: return "fp.isNormal";
   case kind::FLOATINGPOINT_ISSN: return "fp.isSubnormal";
-  case kind::FLOATINGPOINT_ISZ: return "fp.isZero";  
+  case kind::FLOATINGPOINT_ISZ: return "fp.isZero";
   case kind::FLOATINGPOINT_ISINF: return "fp.isInfinite";
   case kind::FLOATINGPOINT_ISNAN: return "fp.isNaN";
   case kind::FLOATINGPOINT_ISNEG: return "fp.isNegative";
@@ -1045,7 +1074,7 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
       }
     }
   } else if(dynamic_cast<const DeclareFunctionCommand*>(c) != NULL) {
-    const DeclareFunctionCommand* dfc = (const DeclareFunctionCommand*)c; 
+    const DeclareFunctionCommand* dfc = (const DeclareFunctionCommand*)c;
     Node n = Node::fromExpr( dfc->getFunction() );
     if(dfc->getPrintInModelSetByUser()) {
       if(!dfc->getPrintInModel()) {
@@ -1071,9 +1100,9 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
       out << "(define-fun " << n << " () "
           << n.getType() << " ";
       if(val.getType().isInteger() && n.getType().isReal() && !n.getType().isInteger()) {
-	//toStreamReal(out, val, true);
-	toStreamRational(out, val.getConst<Rational>(), true);
-	//out << val << ".0";	
+        //toStreamReal(out, val, true);
+        toStreamRational(out, val.getConst<Rational>(), true);
+        //out << val << ".0";
       } else {
         out << val;
       }
@@ -1228,16 +1257,16 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c) throw()
 
 static void toStreamRational(std::ostream& out, const Rational& r, bool decimal) throw() {
   bool neg = r.sgn() < 0;
-  
+
   // TODO:
   // We are currently printing (- (/ 5 3))
   // instead of (/ (- 5) 3) which is what is in the SMT-LIB value in the theory definition.
   // Before switching, I'll keep to what was there and send an email.
 
   // Tim: Apologies for the ifs on one line but in this case they are cleaner.
-  
+
   if (neg) { out << "(- "; }
-  
+
   if(r.isIntegral()) {
     if (neg) {
       out << (-r);
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index b4ecc1d3d..3cbc45cd1 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -70,6 +70,9 @@ operator BITVECTOR_SLE 2 "bit-vector signed less than or equal (the two bit-vect
 operator BITVECTOR_SGT 2 "bit-vector signed greater than (the two bit-vector parameters must have same width)"
 operator BITVECTOR_SGE 2 "bit-vector signed greater than or equal (the two bit-vector parameters must have same width)"
 
+operator BITVECTOR_REDOR 1 "bit-vector redor"
+operator BITVECTOR_REDAND 1 "bit-vector redand"
+
 operator BITVECTOR_EAGER_ATOM 1 "formula to be treated as a bv atom via eager bit-blasting (internal-only symbol)"
 operator BITVECTOR_ACKERMANIZE_UDIV 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvudiv (internal-only symbol)"
 operator BITVECTOR_ACKERMANIZE_UREM 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvurem (internal-only symbol)"
@@ -171,6 +174,10 @@ typerule BITVECTOR_SLE ::CVC4::theory::bv::BitVectorPredicateTypeRule
 typerule BITVECTOR_SGT ::CVC4::theory::bv::BitVectorPredicateTypeRule
 typerule BITVECTOR_SGE ::CVC4::theory::bv::BitVectorPredicateTypeRule
 
+typerule BITVECTOR_REDOR ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule
+typerule BITVECTOR_REDAND ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule
+
+
 typerule BITVECTOR_EAGER_ATOM ::CVC4::theory::bv::BitVectorEagerAtomTypeRule
 typerule BITVECTOR_ACKERMANIZE_UDIV ::CVC4::theory::bv::BitVectorAckermanizationUdivTypeRule
 typerule BITVECTOR_ACKERMANIZE_UREM ::CVC4::theory::bv::BitVectorAckermanizationUremTypeRule
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 3cc1c323c..768923ee6 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -49,6 +49,8 @@ enum RewriteRuleId {
   UgeEliminate,
   SgeEliminate,
   SgtEliminate,
+  RedorEliminate,
+  RedandEliminate,
   SubEliminate,
   SltEliminate,
   SleEliminate,
@@ -188,6 +190,8 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case SgtEliminate:        out << "SgtEliminate";        return out;
   case UgeEliminate:        out << "UgeEliminate";        return out;
   case SgeEliminate:        out << "SgeEliminate";        return out;
+  case RedorEliminate:      out << "RedorEliminate";      return out;
+  case RedandEliminate:     out << "RedandEliminate";     return out;
   case RepeatEliminate:     out << "RepeatEliminate";     return out;
   case RotateLeftEliminate: out << "RotateLeftEliminate"; return out;
   case RotateRightEliminate:out << "RotateRightEliminate";return out;
@@ -522,6 +526,8 @@ struct AllRewriteRules {
   RewriteRule<UltPlusOne> rule119;
   RewriteRule<ConcatToMult> rule120;
   RewriteRule<IsPowerOfTwo> rule121;
+  RewriteRule<RedorEliminate> rule122;
+  RewriteRule<RedandEliminate> rule123;
 };
 
 template<> inline
diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index 0442c47d9..cd173a6dd 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -479,6 +479,33 @@ Node RewriteRule<SignExtendEliminate>::apply(TNode node) {
   return utils::mkConcat(extension, node[0]);
 }
 
+template<>
+bool RewriteRule<RedorEliminate>::applies(TNode node) {
+  return (node.getKind() == kind::BITVECTOR_REDOR);
+}
+
+template<>
+Node RewriteRule<RedorEliminate>::apply(TNode node) {
+  Debug("bv-rewrite") << "RewriteRule<RedorEliminate>(" << node << ")" << std::endl;
+  TNode a = node[0];
+  unsigned size = utils::getSize(node[0]); 
+  Node result = NodeManager::currentNM()->mkNode(kind::EQUAL, a, utils::mkConst( size, 0 ) );
+  return result.negate();
+}
+
+template<>
+bool RewriteRule<RedandEliminate>::applies(TNode node) {
+  return (node.getKind() == kind::BITVECTOR_REDAND);
+}
+
+template<>
+Node RewriteRule<RedandEliminate>::apply(TNode node) {
+  Debug("bv-rewrite") << "RewriteRule<RedandEliminate>(" << node << ")" << std::endl;
+  TNode a = node[0];
+  unsigned size = utils::getSize(node[0]); 
+  Node result = NodeManager::currentNM()->mkNode(kind::EQUAL, a, utils::mkOnes( size ) );
+  return result;
+}
 
 }
 }
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 86f2c6760..f2adea411 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -553,6 +553,22 @@ RewriteResponse TheoryBVRewriter::RewriteRotateLeft(TNode node, bool prerewrite)
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
+RewriteResponse TheoryBVRewriter::RewriteRedor(TNode node, bool prerewrite){
+  Node resultNode = LinearRewriteStrategy
+    < RewriteRule<RedorEliminate>
+    >::apply(node);
+  
+  return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+}
+
+RewriteResponse TheoryBVRewriter::RewriteRedand(TNode node, bool prerewrite){
+  Node resultNode = LinearRewriteStrategy
+    < RewriteRule<RedandEliminate>
+    >::apply(node);
+  
+  return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+}
+
 RewriteResponse TheoryBVRewriter::RewriteBVToNat(TNode node, bool prerewrite) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<BVToNatEliminate>
@@ -651,6 +667,8 @@ void TheoryBVRewriter::initializeRewrites() {
   d_rewriteTable [ kind::BITVECTOR_SIGN_EXTEND ] = RewriteSignExtend;
   d_rewriteTable [ kind::BITVECTOR_ROTATE_RIGHT ] = RewriteRotateRight;
   d_rewriteTable [ kind::BITVECTOR_ROTATE_LEFT ] = RewriteRotateLeft;
+  d_rewriteTable [ kind::BITVECTOR_REDOR ] = RewriteRedor;
+  d_rewriteTable [ kind::BITVECTOR_REDAND ] = RewriteRedand;
 
   d_rewriteTable [ kind::BITVECTOR_TO_NAT ] = RewriteBVToNat;
   d_rewriteTable [ kind::INT_TO_BITVECTOR ] = RewriteIntToBV;
diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index 42bccb534..3f0fa8194 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -77,6 +77,8 @@ class TheoryBVRewriter {
   static RewriteResponse RewriteSignExtend(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteRotateRight(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteRotateLeft(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteRedor(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteRedand(TNode node, bool prerewrite = false);
 
   static RewriteResponse RewriteBVToNat(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteIntToBV(TNode node, bool prerewrite = false);
diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index 81a2d9a27..fbb285fe0 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -112,6 +112,20 @@ public:
   }
 };/* class BitVectorPredicateTypeRule */
 
+class BitVectorUnaryPredicateTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    if( check ) {
+      TypeNode type = n[0].getType(check);
+      if (!type.isBitVector()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
+      }
+    }
+    return nodeManager->booleanType();
+  }
+};/* class BitVectorUnaryPredicateTypeRule */
+
 class BitVectorEagerAtomTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 6ebc9db92..a8b6887e5 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -385,6 +385,8 @@ inline bool isBVPredicate(TNode node) {
       node.getKind() == kind::BITVECTOR_SGE ||
       node.getKind() == kind::BITVECTOR_ULE || 
       node.getKind() == kind::BITVECTOR_SLE ||
+      node.getKind() == kind::BITVECTOR_REDOR ||
+      node.getKind() == kind::BITVECTOR_REDAND ||
       ( node.getKind() == kind::NOT && (node[0].getKind() == kind::EQUAL ||
                                         node[0].getKind() == kind::BITVECTOR_ULT ||
                                         node[0].getKind() == kind::BITVECTOR_SLT ||
@@ -393,7 +395,9 @@ inline bool isBVPredicate(TNode node) {
                                         node[0].getKind() == kind::BITVECTOR_SGT ||
                                         node[0].getKind() == kind::BITVECTOR_SGE ||
                                         node[0].getKind() == kind::BITVECTOR_ULE || 
-                                        node[0].getKind() == kind::BITVECTOR_SLE)))
+                                        node[0].getKind() == kind::BITVECTOR_SLE ||
+                                        node[0].getKind() == kind::BITVECTOR_REDOR ||
+                                        node[0].getKind() == kind::BITVECTOR_REDAND)))
     {
       return true; 
     }
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index a8121b67d..3ab29f334 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -650,12 +650,22 @@ void SygusSymBreak::addTester( Node tst ) {
     std::map< Node, ProgSearch * >::iterator it = d_prog_search.find( a );
     ProgSearch * ps;
     if( it==d_prog_search.end() ){
-      ps = new ProgSearch( this, a, d_context );
+      //check if sygus type
+      TypeNode tn = a.getType();
+      Assert( DatatypesRewriter::isTypeDatatype( tn ) );
+      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+      if( dt.isSygus() ){
+        ps = new ProgSearch( this, a, d_context );
+      }else{
+        ps = NULL;
+      }
       d_prog_search[a] = ps;
     }else{
       ps = it->second;
     }
-    ps->addTester( tst );
+    if( ps ){
+      ps->addTester( tst );
+    }
   }
 }
 
@@ -781,7 +791,7 @@ bool SygusSymBreak::ProgSearch::processSubprograms( Node n, int depth, int odept
 Node SygusSymBreak::ProgSearch::getCandidateProgramAtDepth( int depth, Node prog, int curr_depth, Node parent, std::map< TypeNode, int >& var_count,
                                                             std::vector< Node >& testers, std::map< Node, std::vector< Node > >& testers_u ) {
   Assert( depth>=curr_depth );
-  Trace("sygus-sym-break-debug") << "Reconstructing program for " << prog << " at depth " << curr_depth << "/" << depth << std::endl;
+  Trace("sygus-sym-break-debug") << "Reconstructing program for " << prog << " at depth " << curr_depth << "/" << depth << " " << prog.getType() << std::endl;
   NodeMap::const_iterator it = d_testers.find( prog );
   if( it!=d_testers.end() ){
     Node tst = (*it).second;
@@ -823,7 +833,7 @@ bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node
     int tsize = d_tds->getSygusTermSize( prog );
     if( itnp==d_normalized_to_orig[at].end() ){
       d_normalized_to_orig[at][progr] = prog;
-      if( progr.getKind()==SKOLEM && d_tds->getSygusType( progr )==at ){
+      if( progr.getKind()==SKOLEM && d_tds->getSygusTypeForVar( progr )==at ){
         Trace("sygus-nf") << "* Sygus sym break : " << prog << " rewrites to variable " << progr << " of same type as self" << std::endl;
         d_redundant[at][prog] = true;
         red = true;
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 5f3498f49..045407bf0 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -70,7 +70,7 @@ void CegConjecture::assign( QuantifiersEngine * qe, Node q ) {
 }
 
 void CegConjecture::initializeGuard( QuantifiersEngine * qe ){
-  if( d_guard.isNull() ){
+  if( isAssigned() && d_guard.isNull() ){
     d_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) );
     //specify guard behavior
     d_guard = qe->getValuation().ensureLiteral( d_guard );
@@ -137,6 +137,10 @@ bool CegConjecture::isSingleInvocation() {
   return d_ceg_si->isSingleInvocation();
 }
 
+bool CegConjecture::needsCheck() {
+  return d_active && !d_infeasible && ( !isSingleInvocation() || d_ceg_si->needsCheck() );
+}
+
 CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ){
   d_conj = new CegConjecture( qe->getSatContext() );
   d_last_inst_si = false;
@@ -155,7 +159,7 @@ void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) {
     Trace("cegqi-engine") << "---Counterexample Guided Instantiation Engine---" << std::endl;
     Trace("cegqi-engine-debug") << std::endl;
     Trace("cegqi-engine-debug") << "Current conjecture status : active : " << d_conj->d_active << " feasible : " << !d_conj->d_infeasible << std::endl;
-    if( d_conj->d_active && !d_conj->d_infeasible ){
+    if( d_conj->needsCheck() ){
       checkCegConjecture( d_conj );
     }
     Trace("cegqi-engine") << "Finished Counterexample Guided Instantiation engine." << std::endl;
@@ -213,29 +217,32 @@ void CegInstantiation::assertNode( Node n ) {
 }
 
 Node CegInstantiation::getNextDecisionRequest() {
-  d_conj->initializeGuard( d_quantEngine );
-  bool value;
-  if( !d_quantEngine->getValuation().hasSatValue( d_conj->d_guard, value ) ) {
-    //if( d_conj->d_guard_split.isNull() ){
-    //  Node lem = NodeManager::currentNM()->mkNode( OR, d_conj->d_guard.negate(), d_conj->d_guard );
-    //  d_quantEngine->getOutputChannel().lemma( lem );
-    //}
-    Trace("cegqi-debug") << "CEGQI : Decide next on : " << d_conj->d_guard << "..." << std::endl;
-    return d_conj->d_guard;
-  }
   //enforce fairness
-  if( d_conj->isAssigned() && d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){
-    Node lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() );
-    if( d_quantEngine->getValuation().hasSatValue( lit, value ) ) {
-      if( !value ){
-        d_conj->d_curr_lit.set( d_conj->d_curr_lit.get() + 1 );
-        lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() );
-        Trace("cegqi-debug") << "CEGQI : Decide on next lit : " << lit << "..." << std::endl;
+  if( d_conj->isAssigned() ){
+    d_conj->initializeGuard( d_quantEngine );
+    bool value;
+    if( !d_quantEngine->getValuation().hasSatValue( d_conj->d_guard, value ) ) {
+      //if( d_conj->d_guard_split.isNull() ){
+      //  Node lem = NodeManager::currentNM()->mkNode( OR, d_conj->d_guard.negate(), d_conj->d_guard );
+      //  d_quantEngine->getOutputChannel().lemma( lem );
+      //}
+      Trace("cegqi-debug") << "CEGQI : Decide next on : " << d_conj->d_guard << "..." << std::endl;
+      return d_conj->d_guard;
+    }
+    
+    if( d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){
+      Node lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() );
+      if( d_quantEngine->getValuation().hasSatValue( lit, value ) ) {
+        if( !value ){
+          d_conj->d_curr_lit.set( d_conj->d_curr_lit.get() + 1 );
+          lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() );
+          Trace("cegqi-debug") << "CEGQI : Decide on next lit : " << lit << "..." << std::endl;
+          return lit;
+        }
+      }else{
+        Trace("cegqi-debug") << "CEGQI : Decide on current lit : " << lit << "..." << std::endl;
         return lit;
       }
-    }else{
-      Trace("cegqi-debug") << "CEGQI : Decide on current lit : " << lit << "..." << std::endl;
-      return lit;
     }
   }
 
@@ -484,7 +491,8 @@ void CegInstantiation::getMeasureLemmas( Node n, Node v, std::vector< Node >& le
 }
 
 void CegInstantiation::printSynthSolution( std::ostream& out ) {
-  if( d_conj ){
+  if( d_conj->isAssigned() ){
+    Trace("cegqi-debug") << "Printing synth solution..." << std::endl;
     //if( !(Trace.isOn("cegqi-stats")) ){
     //  out << "Solution:" << std::endl;
     //}
@@ -530,6 +538,8 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
         out << ")" << std::endl;
       }
     }
+  }else{
+    Assert( false );
   }
 }
 
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 74e9b0aba..5f393626c 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -83,6 +83,8 @@ public:  //for fairness
   CegqiFairMode getCegqiFairMode();
   /** is single invocation */
   bool isSingleInvocation();
+  /** needs check */
+  bool needsCheck();
 };
 
 
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 0a434e4ca..b7bbf8a93 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -742,29 +742,38 @@ CegConjectureSingleInv::CegConjectureSingleInv( CegConjecture * p ) : d_parent(
   d_sol = NULL;
   d_c_inst_match_trie = NULL;
   d_cinst = NULL;
+  d_has_ites = true;
 }
 
 Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) {
   if( !d_single_inv.isNull() ) {
-    Assert( d_single_inv.getKind()==FORALL );
     d_single_inv_var.clear();
     d_single_inv_sk.clear();
-    for( unsigned i=0; i<d_single_inv[0].getNumChildren(); i++ ){
-      std::stringstream ss;
-      ss << "k_" << d_single_inv[0][i];
-      Node k = NodeManager::currentNM()->mkSkolem( ss.str(), d_single_inv[0][i].getType(), "single invocation function skolem" );
-      d_single_inv_var.push_back( d_single_inv[0][i] );
-      d_single_inv_sk.push_back( k );
-      d_single_inv_sk_index[k] = i;
+    Node inst;
+    if( d_single_inv.getKind()==FORALL ){
+      for( unsigned i=0; i<d_single_inv[0].getNumChildren(); i++ ){
+        std::stringstream ss;
+        ss << "k_" << d_single_inv[0][i];
+        Node k = NodeManager::currentNM()->mkSkolem( ss.str(), d_single_inv[0][i].getType(), "single invocation function skolem" );
+        d_single_inv_var.push_back( d_single_inv[0][i] );
+        d_single_inv_sk.push_back( k );
+        d_single_inv_sk_index[k] = i;
+      }
+      inst = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
+    }else{
+      inst = d_single_inv;
     }
-    Node inst = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
     inst = TermDb::simpleNegate( inst );
     Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl;
 
     //initialize the instantiator for this
-    CegqiOutputSingleInv * cosi = new CegqiOutputSingleInv( this );
-    d_cinst = new CegInstantiator( d_qe, cosi );
-    d_cinst->d_vars.insert( d_cinst->d_vars.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
+    if( !d_single_inv_sk.empty() ){
+      CegqiOutputSingleInv * cosi = new CegqiOutputSingleInv( this );
+      d_cinst = new CegInstantiator( d_qe, cosi );
+      d_cinst->d_vars.insert( d_cinst->d_vars.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
+    }else{
+      d_cinst = NULL;
+    }
 
     return NodeManager::currentNM()->mkNode( OR, guard.negate(), inst );
   }else{
@@ -790,6 +799,14 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
   std::map< Node, std::map< Node, bool > > contains;
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
     progs.push_back( q[0][i] );
+    //check whether all types have ITE
+    TypeNode tn = q[0][i].getType();
+    d_qe->getTermDatabaseSygus()->registerSygusType( tn );
+    if( !d_qe->getTermDatabaseSygus()->sygusToBuiltinType( tn ).isBoolean() ){
+      if( !d_qe->getTermDatabaseSygus()->hasKind( tn, ITE ) ){
+        d_has_ites = false;
+      }
+    }
   }
   //collect information about conjunctions
   bool singleInvocation = false;
@@ -881,8 +898,10 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
       //construct the single invocation version of the property
       Trace("cegqi-si") << "Single invocation formula conjuncts are : " << std::endl;
       //std::vector< Node > si_conj;
-      Assert( !pbvs.empty() );
-      Node pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, pbvs );
+      Node pbvl;
+      if( !pbvs.empty() ){
+        pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, pbvs );
+      }
       for( std::map< Node, std::vector< Node > >::iterator it = children.begin(); it != children.end(); ++it ){
         //should hold since we prevent miniscoping
         Assert( d_single_inv.isNull() );
@@ -978,9 +997,14 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
 
         if( singleInvocation ){
           Node bd = conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts );
-          d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd );
+          if( pbvl.isNull() ){
+            d_single_inv = bd;
+          }else{
+            d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd );
+          }
           Trace("cegqi-si-debug") << "...formula is : " << d_single_inv << std::endl;
-          if( options::eMatching.wasSetByUser() ){
+          /*
+          if( options::eMatching() && options::eMatching.wasSetByUser() ){
             Node bd = d_qe->getTermDatabase()->getInstConstantBody( d_single_inv );
             std::vector< Node > patTerms;
             std::vector< Node > exclude;
@@ -992,6 +1016,7 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
               }
             }
           }
+          */
         }
       }
     }
@@ -999,9 +1024,68 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
   if( !singleInvocation ){
     Trace("cegqi-si") << "Property is not single invocation." << std::endl;
     if( options::cegqiSingleInvAbort() ){
-      Message() << "Property is not single invocation." << std::endl;
+      Notice() << "Property is not single invocation." << std::endl;
       exit( 0 );
     }
+  }else{
+    if( options::cegqiSingleInvPreRegInst() && d_single_inv.getKind()==FORALL ){
+      Trace("cegqi-si-presolve") << "Check " << d_single_inv << std::endl;
+      //at preregister time, add proxy of obvious instantiations up front, which helps learning during preprocessing
+      std::vector< Node > vars;
+      std::map< Node, std::vector< Node > > teq;
+      for( unsigned i=0; i<d_single_inv[0].getNumChildren(); i++ ){
+        vars.push_back( d_single_inv[0][i] );
+        teq[d_single_inv[0][i]].clear();
+      }
+      collectPresolveEqTerms( d_single_inv[1], teq );
+      std::vector< Node > terms;
+      std::vector< Node > conj;
+      getPresolveEqConjuncts( vars, terms, teq, d_single_inv, conj );
+
+      if( !conj.empty() ){
+        Node lem = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj );
+        Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() );
+        lem = NodeManager::currentNM()->mkNode( OR, g, lem );
+        d_qe->getOutputChannel().lemma( lem, false, true );
+      }
+    }
+  }
+}
+
+void CegConjectureSingleInv::collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq ) {
+  if( n.getKind()==EQUAL ){
+    for( unsigned i=0; i<2; i++ ){
+      std::map< Node, std::vector< Node > >::iterator it = teq.find( n[i] );
+      if( it!=teq.end() ){
+        Node nn = n[ i==0 ? 1 : 0 ];
+        if( std::find( it->second.begin(), it->second.end(), nn )==it->second.end() ){
+          it->second.push_back( nn );
+          Trace("cegqi-si-presolve") << "  - " << n[i] << " = " << nn << std::endl;
+        }
+      }
+    }
+  }
+  for( unsigned i=0; i<n.getNumChildren(); i++ ){
+    collectPresolveEqTerms( n[i], teq );
+  }
+}
+
+void CegConjectureSingleInv::getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& terms,
+                                                     std::map< Node, std::vector< Node > >& teq, Node f, std::vector< Node >& conj ) {
+  if( conj.size()<1000 ){
+    if( terms.size()==f[0].getNumChildren() ){
+      Node c = f[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
+      conj.push_back( c );
+    }else{
+      unsigned i = terms.size();
+      Node v = f[0][i];
+      terms.push_back( Node::null() );
+      for( unsigned j=0; j<teq[v].size(); j++ ){
+        terms[i] = teq[v][j];
+        getPresolveEqConjuncts( vars, terms, teq, f, conj );
+      }
+      terms.pop_back();
+    }
   }
 }
 
@@ -1171,8 +1255,7 @@ bool CegConjectureSingleInv::addLemma( Node n ) {
 }
 
 void CegConjectureSingleInv::check( std::vector< Node >& lems ) {
-  if( !d_single_inv.isNull() ) {
-    Assert( d_cinst!=NULL );
+  if( !d_single_inv.isNull() && d_cinst!=NULL ) {
     d_curr_lemmas.clear();
     //check if there are delta lemmas
     d_cinst->getDeltaLemmas( lems );
@@ -1186,20 +1269,61 @@ void CegConjectureSingleInv::check( std::vector< Node >& lems ) {
   }
 }
 
-Node CegConjectureSingleInv::constructSolution( unsigned i, unsigned index ) {
+Node CegConjectureSingleInv::constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index ) {
   Assert( index<d_inst.size() );
   Assert( i<d_inst[index].size() );
+  unsigned uindex = indices[index];
   if( index==d_inst.size()-1 ){
-    return d_inst[index][i];
+    return d_inst[uindex][i];
   }else{
-    Node cond = d_lemmas_produced[index];
+    Node cond = d_lemmas_produced[uindex];
     cond = TermDb::simpleNegate( cond );
-    Node ite1 = d_inst[index][i];
-    Node ite2 = constructSolution( i, index+1 );
+    Node ite1 = d_inst[uindex][i];
+    Node ite2 = constructSolution( indices, i, index+1 );
     return NodeManager::currentNM()->mkNode( ITE, cond, ite1, ite2 );
   }
 }
 
+//TODO: use term size?
+struct sortSiInstanceIndices {
+  CegConjectureSingleInv* d_ccsi;
+  int d_i;
+  bool operator() (unsigned i, unsigned j) {
+    if( d_ccsi->d_inst[i][d_i].isConst() && !d_ccsi->d_inst[j][d_i].isConst() ){
+      return true;
+    }else{
+      return false;
+    }
+  }
+};
+
+/*
+Node removeBooleanIte( Node n ){
+  if( n.getKind()==ITE && n.getType().isBoolean() ){
+    Node n1 = removeBooleanIte( n[1] );
+    Node n2 = removeBooleanIte( n[2] );
+    return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n[0], n1 ),
+                                                 NodeManager::currentNM()->mkNode( AND, n[0].negate(), n2 ) );
+  }else{
+    bool childChanged = false;
+    std::vector< Node > children;
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      Node nn = removeBooleanIte( n[i] );
+      children.push_back( nn );
+      childChanged = childChanged || nn!=n[i];
+    }
+    if( childChanged ){
+      if( n.hasOperator() ){
+        children.insert( children.begin(), n.getOperator() );
+      }
+      return NodeManager::currentNM()->mkNode( n.getKind(), children );
+    }else{
+      return n;
+    }
+  }
+}
+*/
+
 Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& reconstructed ){
   Assert( d_sol!=NULL );
   Assert( !d_lemmas_produced.empty() );
@@ -1225,7 +1349,21 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int&
     d_sol->d_varList.push_back( varList[i-1] );
   }
   //construct the solution
-  Node s = constructSolution( sol_index, 0 );
+  Trace("csi-sol") << "Sort solution return values " << sol_index << std::endl;
+  Assert( d_lemmas_produced.size()==d_inst.size() );
+  std::vector< unsigned > indices;
+  for( unsigned i=0; i<d_lemmas_produced.size(); i++ ){
+    Assert( sol_index<d_inst[i].size() );
+    indices.push_back( i );
+  }
+  //sort indices based on heuristic : currently, do all constant returns first (leads to simpler conditions)
+  // TODO : to minimize solution size, put the largest term last
+  sortSiInstanceIndices ssii;
+  ssii.d_ccsi = this;
+  ssii.d_i = sol_index;
+  std::sort( indices.begin(), indices.end(), ssii );
+  Trace("csi-sol") << "Construct solution" << std::endl;
+  Node s = constructSolution( indices, sol_index, 0 );
   s = s.substitute( vars.begin(), vars.end(), d_varList.begin(), d_varList.end() );
   d_orig_solution = s;
 
@@ -1242,6 +1380,10 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int&
     if( reconstructed==1 ){
       Trace("csi-sol") << "Solution (post-reconstruction into Sygus): " << d_sygus_solution << std::endl;
     }
+  }else{
+    ////remove boolean ITE (not allowed for sygus comp 2015)
+    //d_solution = removeBooleanIte( d_solution );
+    //Trace("csi-sol") << "Solution (after remove boolean ITE) : " << d_solution << std::endl;
   }
 
 
@@ -1278,4 +1420,13 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int&
   }
 }
 
+bool CegConjectureSingleInv::needsCheck() {
+  if( options::cegqiSingleInvMultiInstAbort() ){
+    if( !hasITEs() ){
+      return d_inst.empty();
+    }
+  }
+  return true;
+}
+
 }
\ No newline at end of file
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index eb33c479e..f8e3879ac 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -111,8 +111,11 @@ private:
   bool processSingleInvLiteral( Node lit, bool pol, std::map< Node, std::vector< Node > >& case_vals );
   bool doVariableElimination( Node v, std::vector< Node >& conjuncts );
   bool getVariableEliminationTerm( bool pol, bool active, Node v, Node n, TNode& s, int& status );
+  //presolve
+  void collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq );
+  void getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& terms, std::map< Node, std::vector< Node > >& teq, Node n, std::vector< Node >& conj );
   //constructing solution
-  Node constructSolution( unsigned i, unsigned index );
+  Node constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index );
 private:
   //map from programs to variables in single invocation property
   std::map< Node, Node > d_single_inv_map;
@@ -127,8 +130,6 @@ private:
   //list of skolems for each program
   std::vector< Node > d_single_inv_var;
   //lemmas produced
-  std::vector< Node > d_lemmas_produced;
-  std::vector< std::vector< Node > > d_inst;
   inst::InstMatchTrie d_inst_match_trie;
   inst::CDInstMatchTrie * d_c_inst_match_trie;
   // solution
@@ -136,6 +137,11 @@ private:
   Node d_orig_solution;
   Node d_solution;
   Node d_sygus_solution;
+  bool d_has_ites;
+public:
+  //lemmas produced
+  std::vector< Node > d_lemmas_produced;
+  std::vector< std::vector< Node > > d_inst; 
 private:
   std::vector< Node > d_curr_lemmas;
   //add instantiation
@@ -159,8 +165,12 @@ public:
   void check( std::vector< Node >& lems );
   //get solution
   Node getSolution( unsigned sol_index, TypeNode stn, int& reconstructed );
+  // has ites
+  bool hasITEs() { return d_has_ites; }
   // is single invocation
   bool isSingleInvocation() { return !d_single_inv.isNull(); }
+  //needs check
+  bool needsCheck();
 };
 
 }
diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
index 0429abac9..413fd9ba2 100644
--- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
@@ -86,8 +86,11 @@ Node CegConjectureSingleInvSol::pullITEs( Node s ) {
         Trace("csi-sol-debug") << "For " << s << ", can pull " << cond << " -> " << t << " with remainder " << rem << std::endl;
         t = pullITEs( t );
         rem = pullITEs( rem );
+        Trace("csi-pull-ite") << "PI: Rewrite : " << s << std::endl;
+        Node prev = s;
         s = NodeManager::currentNM()->mkNode( ITE, TermDb::simpleNegate( cond ), t, rem );
-        //Trace("csi-debug-sol") << "Now : " << s << std::endl;
+        Trace("csi-pull-ite") << "PI: Rewrite Now : " << s << std::endl;
+        Trace("csi-pull-ite") << "(= " << prev << " " << s << ")" << std::endl;
         success = true;
       }
     }while( success );
@@ -99,11 +102,13 @@ Node CegConjectureSingleInvSol::pullITEs( Node s ) {
 bool CegConjectureSingleInvSol::pullITECondition( Node root, Node n_ite, std::vector< Node >& conj, Node& t, Node& rem, int depth ) {
   Assert( n_ite.getKind()==ITE );
   std::vector< Node > curr_conj;
+  std::vector< Node > orig_conj;
   bool isAnd;
   if( n_ite[0].getKind()==AND || n_ite[0].getKind()==OR ){
     isAnd = n_ite[0].getKind()==AND;
     for( unsigned i=0; i<n_ite[0].getNumChildren(); i++ ){
       Node cond = n_ite[0][i];
+      orig_conj.push_back( cond );
       if( n_ite[0].getKind()==OR ){
         cond = TermDb::simpleNegate( cond );
       }
@@ -112,12 +117,15 @@ bool CegConjectureSingleInvSol::pullITECondition( Node root, Node n_ite, std::ve
   }else{
     Node neg = n_ite[0].negate();
     if( std::find( conj.begin(), conj.end(), neg )!=conj.end() ){
+      //if negation of condition exists, use it
       isAnd = false;
       curr_conj.push_back( neg );
     }else{
+      //otherwise, use condition
       isAnd = true;
       curr_conj.push_back( n_ite[0] );
     }
+    orig_conj.push_back( n_ite[0] );
   }
   // take intersection with current conditions
   std::vector< Node > new_conj;
@@ -162,13 +170,14 @@ bool CegConjectureSingleInvSol::pullITECondition( Node root, Node n_ite, std::ve
     //make remainder : strip out conditions in conj
     Assert( !conj.empty() );
     std::vector< Node > cond_c;
+    Assert( orig_conj.size()==curr_conj.size() );
     for( unsigned i=0; i<curr_conj.size(); i++ ){
       if( std::find( conj.begin(), conj.end(), curr_conj[i] )==conj.end() ){
-        cond_c.push_back( curr_conj[i] );
+        cond_c.push_back( orig_conj[i] );
       }
     }
     if( cond_c.empty() ){
-      rem = isAnd ? tval : rem;
+      rem = tval;
     }else{
       Node new_cond = cond_c.size()==1 ? cond_c[0] : NodeManager::currentNM()->mkNode( n_ite[0].getKind(), cond_c );
       rem = NodeManager::currentNM()->mkNode( ITE, new_cond, isAnd ? tval : rem, isAnd ? rem : tval );
@@ -437,7 +446,7 @@ Node CegConjectureSingleInvSol::simplifySolutionNode( Node sol, TypeNode stn, st
               ret = NodeManager::currentNM()->mkNode( ITE, exp_c, ret[1], ret[2] );
             }
             if( !d_qe->getTermDatabaseSygus()->hasKind( stnc[0], ret[0].getKind() ) ){
-              Trace("csi-sol") << "Flatten based on " << ret[0] << "." << std::endl;
+              Trace("csi-simp-debug") << "Flatten based on " << ret[0] << "." << std::endl;
               ret = flattenITEs( ret, false );
             }
           }
@@ -510,7 +519,7 @@ Node CegConjectureSingleInvSol::simplifySolutionNode( Node sol, TypeNode stn, st
       }
       if( !new_vars.empty() ){
         if( !inc.empty() ){
-          Node ret = inc.size()==1 ? sol[0] : NodeManager::currentNM()->mkNode( sol.getKind(), inc );
+          Node ret = inc.size()==1 ? inc[0] : NodeManager::currentNM()->mkNode( sol.getKind(), inc );
           Trace("csi-simp") << "Base return is : " << ret << std::endl;
           // apply substitution
           ret = ret.substitute( new_vars.begin(), new_vars.end(), new_subs.begin(), new_subs.end() );
@@ -848,12 +857,10 @@ int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, in
                     }
                   }while( !new_t.isNull() );
                 }
+                //get decompositions
                 for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
                   Kind k = d_qe->getTermDatabaseSygus()->getArgKind( stn, i );
-                  if( k==AND || k==OR ){
-                    equiv.push_back( NodeManager::currentNM()->mkNode( k, min_t, min_t ) );
-                    equiv.push_back( NodeManager::currentNM()->mkNode( k, min_t, NodeManager::currentNM()->mkConst( k==AND ) ) );
-                  }
+                  getEquivalentTerms( k, min_t, equiv );
                 }
                 //assign ids to terms
                 Trace("csi-rcons-debug") << "Term " << id << " is equivalent to " << equiv.size() << " terms : " << std::endl;
@@ -1046,4 +1053,62 @@ void CegConjectureSingleInvSol::setReconstructed( int id, Node n ) {
   }
 }
 
+void CegConjectureSingleInvSol::getEquivalentTerms( Kind k, Node n, std::vector< Node >& equiv ) {
+  if( k==AND || k==OR ){
+    equiv.push_back( NodeManager::currentNM()->mkNode( k, n, n ) );
+    equiv.push_back( NodeManager::currentNM()->mkNode( k, n, NodeManager::currentNM()->mkConst( k==AND ) ) );
+  }
+  //multiplication for integers
+  //TODO for bitvectors
+  Kind mk = ( k==PLUS || k==MINUS ) ? MULT : UNDEFINED_KIND;
+  if( mk!=UNDEFINED_KIND ){
+    if( n.getKind()==mk && n[0].isConst() && n[0].getType().isInteger() ){
+      bool success = true;
+      for( unsigned i=0; i<2; i++ ){
+        Node eq;
+        if( k==PLUS || k==MINUS ){
+          Node oth = NodeManager::currentNM()->mkConst( Rational(i==0 ? 1000 : -1000) );
+          eq = i==0 ? NodeManager::currentNM()->mkNode( LEQ, n[0], oth ) : NodeManager::currentNM()->mkNode( GEQ, n[0], oth );
+        }
+        if( !eq.isNull() ){
+          eq = Rewriter::rewrite( eq );
+          if( eq!=d_qe->getTermDatabase()->d_true ){
+            success = false;
+            break;
+          }
+        }
+      }
+      if( success ){
+        Node var = n[1];
+        Node rem;
+        if( k==PLUS || k==MINUS ){
+          int rem_coeff = (int)n[0].getConst<Rational>().getNumerator().getSignedInt();
+          if( rem_coeff>0 && k==PLUS ){
+            rem_coeff--;
+          }else if( rem_coeff<0 && k==MINUS ){
+            rem_coeff++;
+          }else{
+            success = false;
+          }
+          if( success ){
+            rem = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(rem_coeff) ), var );
+            rem = Rewriter::rewrite( rem );
+          }
+        }
+        if( !rem.isNull() ){
+          equiv.push_back( NodeManager::currentNM()->mkNode( k, rem, var ) );
+        }
+      }
+    }
+  }
+  //negative constants
+  if( k==MINUS ){
+    if( n.isConst() && n.getType().isInteger() && n.getConst<Rational>().getNumerator().strictlyNegative() ){
+      Node nn = NodeManager::currentNM()->mkNode( UMINUS, n );
+      nn = Rewriter::rewrite( nn );
+      equiv.push_back( NodeManager::currentNM()->mkNode( MINUS, NodeManager::currentNM()->mkConst( Rational(0) ), nn ) );
+    }
+  }  
+}
+  
 }
diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.h b/src/theory/quantifiers/ce_guided_single_inv_sol.h
index 6a4b6f90f..1d84986b4 100644
--- a/src/theory/quantifiers/ce_guided_single_inv_sol.h
+++ b/src/theory/quantifiers/ce_guided_single_inv_sol.h
@@ -78,6 +78,8 @@ private:
   bool collectReconstructNodes( int pid, std::vector< Node >& ts, const DatatypeConstructor& dtc, std::vector< int >& ids, int& status );
   bool getPathToRoot( int id );
   void setReconstructed( int id, Node n );
+  //get equivalent terms to n with top symbol k
+  void getEquivalentTerms( Kind k, Node n, std::vector< Node >& equiv );
 public:
   Node reconstructSolution( Node sol, TypeNode stn, int& reconstructed );
 public:
diff --git a/src/theory/quantifiers/fun_def_engine.cpp b/src/theory/quantifiers/fun_def_engine.cpp
new file mode 100644
index 000000000..56214f540
--- /dev/null
+++ b/src/theory/quantifiers/fun_def_engine.cpp
@@ -0,0 +1,54 @@
+/*********************                                                        */
+/*! \file fun_def_process.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** This class implements specialized techniques for (recursively) defined functions
+ **/
+
+#include <vector>
+
+#include "theory/quantifiers/fun_def_engine.h"
+#include "theory/rewriter.h"
+#include "theory/quantifiers/term_database.h"
+
+using namespace CVC4;
+using namespace std;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace CVC4::kind;
+
+FunDefEngine::FunDefEngine( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ) {
+  
+}
+
+/* whether this module needs to check this round */
+bool FunDefEngine::needsCheck( Theory::Effort e ) { 
+  return e>=Theory::EFFORT_LAST_CALL; 
+}
+
+/* reset at a round */
+void FunDefEngine::reset_round( Theory::Effort e ){
+  //TODO
+}
+
+/* Call during quantifier engine's check */
+void FunDefEngine::check( Theory::Effort e, unsigned quant_e ) {
+  //TODO
+}
+
+/* Called for new quantifiers */
+void FunDefEngine::registerQuantifier( Node q ) {
+  //TODO
+}
+
+/** called for everything that gets asserted */
+void FunDefEngine::assertNode( Node n ) {
+  //TODO
+}
diff --git a/src/theory/quantifiers/fun_def_engine.h b/src/theory/quantifiers/fun_def_engine.h
new file mode 100644
index 000000000..be73d51a9
--- /dev/null
+++ b/src/theory/quantifiers/fun_def_engine.h
@@ -0,0 +1,59 @@
+/*********************                                                        */
+/*! \file fun_def_engine.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Specialized techniques for (recursively) defined functions
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__QUANTIFIERS_FUN_DEF_ENGINE_H
+#define __CVC4__QUANTIFIERS_FUN_DEF_ENGINE_H
+
+#include <iostream>
+#include <string>
+#include <vector>
+#include <map>
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+//module for handling (recursively) defined functions
+class FunDefEngine : public QuantifiersModule {
+private:
+
+public:
+  FunDefEngine( QuantifiersEngine * qe, context::Context* c );
+  ~FunDefEngine(){}
+
+  /* whether this module needs to check this round */
+  bool needsCheck( Theory::Effort e );
+  /* reset at a round */
+  void reset_round( Theory::Effort e );
+  /* Call during quantifier engine's check */
+  void check( Theory::Effort e, unsigned quant_e );
+  /* Called for new quantifiers */
+  void registerQuantifier( Node q );
+  /** called for everything that gets asserted */
+  void assertNode( Node n );
+  /** Identify this module (for debugging, dynamic configuration, etc..) */
+  std::string identify() const { return "FunDefEngine"; }
+};
+
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 391abe9eb..ab0526471 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -220,8 +220,12 @@ option cegqiSingleInvReconstruct --cegqi-si-reconstruct bool :default true
   reconstruct solutions for single invocation conjectures in original grammar
 option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default true
   include constants when reconstruct solutions for single invocation conjectures in original grammar
+option cegqiSingleInvPreRegInst --cegqi-si-prereg-inst bool :default true
+  preregister ground instantiations when single invocation
 option cegqiSingleInvAbort --cegqi-si-abort bool :default false
-  abort if our synthesis conjecture is not single invocation
+  abort if synthesis conjecture is not single invocation
+option cegqiSingleInvMultiInstAbort --cegqi-si-multi-inst-abort bool :default false
+  abort if synthesis conjecture is single invocation with no ITE in grammar and multiple instantiations are tried
   
 option sygusNormalForm --sygus-nf bool :default true
   only search for sygus builtin terms that are in normal form
@@ -259,5 +263,10 @@ option lteRestrictInstClosure --lte-restrict-inst-closure bool :default false
 
 option quantAlphaEquiv --quant-alpha-equiv bool :default true
   infer alpha equivalence between quantified formulas
+
+### recursive function options
+
+#option funDefs --fun-defs bool :default false
+#  enable specialized techniques for recursive function definitions
  
 endmodule
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 0198e014f..6a95e243d 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -905,7 +905,21 @@ Node QuantifiersRewriter::computeSplit( Node f, Node body, std::vector< Node >&
 
 Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node ipl ){
   std::vector< Node > activeArgs;
-  computeArgVec2( args, activeArgs, body, ipl );
+  //if cegqi is on, may be synthesis conjecture, in which case we want to keep all variables 
+  if( options::ceGuidedInst() && !ipl.isNull() ){
+    for( unsigned i=0; i<ipl.getNumChildren(); i++ ){
+      Trace("quant-attr-debug") << "Check : " << ipl[i] << " " << ipl[i].getKind() << std::endl;
+      if( ipl[i].getKind()==INST_ATTRIBUTE ){
+        Node avar = ipl[i][0];
+        if( avar.getAttribute(SygusAttribute()) ){
+          activeArgs.insert( activeArgs.end(), args.begin(), args.end() );
+        }
+      }
+    }
+  }
+  if( activeArgs.empty() ){
+    computeArgVec2( args, activeArgs, body, ipl );
+  }
   if( activeArgs.empty() ){
     return body;
   }else{
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index cc8ae4db0..fa0e211b3 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -23,6 +23,7 @@
 #include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/quantifiers/ce_guided_instantiation.h"
 #include "theory/quantifiers/rewrite_engine.h"
+#include "theory/quantifiers/fun_def_engine.h"
 
 //for sygus
 #include "theory/bv/theory_bv_utils.h"
@@ -1431,6 +1432,7 @@ void TermDb::computeAttributes( Node q ) {
             exit( 0 );
           }
           d_fun_defs[f] = true;
+          d_quantEngine->setOwner( q, d_quantEngine->getFunDefEngine() );
         }
         if( avar.getAttribute(SygusAttribute()) ){
           //not necessarily nested existential
@@ -1578,7 +1580,7 @@ TNode TermDbSygus::getVarInc( TypeNode tn, std::map< TypeNode, int >& var_count
   }
 }
 
-TypeNode TermDbSygus::getSygusType( Node v ) {
+TypeNode TermDbSygus::getSygusTypeForVar( Node v ) {
   Assert( d_fv_stype.find( v )!=d_fv_stype.end() );
   return d_fv_stype[v];
 }
@@ -1740,7 +1742,7 @@ Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int
       Node n = NodeManager::currentNM()->mkNode( APPLY, children );
       //must expand definitions
       Node ne = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( n.toExpr() ) );
-      Trace("sygus-util-debug") << "Expanded definitions in " << n << " to " << ne << std::endl;
+      Trace("sygus-db-debug") << "Expanded definitions in " << n << " to " << ne << std::endl;
       return ne;
       */
     }
@@ -2093,10 +2095,10 @@ void TermDbSygus::registerSygusType( TypeNode tn ){
       d_register[tn] = TypeNode::null();
     }else{
       const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-      Trace("sygus-util") << "Register type " << dt.getName() << "..." << std::endl;
+      Trace("sygus-db") << "Register type " << dt.getName() << "..." << std::endl;
       d_register[tn] = TypeNode::fromType( dt.getSygusType() );
       if( d_register[tn].isNull() ){
-        Trace("sygus-util") << "...not sygus." << std::endl;
+        Trace("sygus-db") << "...not sygus." << std::endl;
       }else{
         //for constant reconstruction
         Kind ck = getComparisonKind( TypeNode::fromType( dt.getSygusType() ) );
@@ -2107,14 +2109,14 @@ void TermDbSygus::registerSygusType( TypeNode tn ){
           Expr sop = dt[i].getSygusOp();
           Assert( !sop.isNull() );
           Node n = Node::fromExpr( sop );
-          Trace("sygus-util") << "  Operator #" << i << " : " << sop;
+          Trace("sygus-db") << "  Operator #" << i << " : " << sop;
           if( sop.getKind() == kind::BUILTIN ){
             Kind sk = NodeManager::operatorToKind( n );
-            Trace("sygus-util") << ", kind = " << sk;
+            Trace("sygus-db") << ", kind = " << sk;
             d_kinds[tn][sk] = i;
             d_arg_kind[tn][i] = sk;
           }else if( sop.isConst() ){
-            Trace("sygus-util") << ", constant";
+            Trace("sygus-db") << ", constant";
             d_consts[tn][n] = i;
             d_arg_const[tn][i] = n;
             d_const_list[tn].push_back( n );
@@ -2127,7 +2129,7 @@ void TermDbSygus::registerSygusType( TypeNode tn ){
           }
           d_ops[tn][n] = i;
           d_arg_ops[tn][i] = n;
-          Trace("sygus-util") << std::endl;
+          Trace("sygus-db") << std::endl;
         }
         //sort the constant list
         if( !d_const_list[tn].empty() ){
@@ -2137,12 +2139,12 @@ void TermDbSygus::registerSygusType( TypeNode tn ){
             sc.d_tds = this;
             std::sort( d_const_list[tn].begin(), d_const_list[tn].end(), sc );
           }
-          Trace("sygus-util") << "Type has " << d_const_list[tn].size() << " constants..." << std::endl << "  ";
+          Trace("sygus-db") << "Type has " << d_const_list[tn].size() << " constants..." << std::endl << "  ";
           for( unsigned i=0; i<d_const_list[tn].size(); i++ ){
-            Trace("sygus-util") << d_const_list[tn][i] << " ";
+            Trace("sygus-db") << d_const_list[tn][i] << " ";
           }
-          Trace("sygus-util") << std::endl;
-          Trace("sygus-util") << "Of these, " << d_const_list_pos[tn] << " are marked as positive." << std::endl;
+          Trace("sygus-db") << std::endl;
+          Trace("sygus-db") << "Of these, " << d_const_list_pos[tn] << " are marked as positive." << std::endl;
         }
         //register connected types
         for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
@@ -2159,6 +2161,11 @@ bool TermDbSygus::isRegistered( TypeNode tn ) {
   return d_register.find( tn )!=d_register.end();
 }
 
+TypeNode TermDbSygus::sygusToBuiltinType( TypeNode tn ) {
+  Assert( isRegistered( tn ) );
+  return d_register[tn];
+}
+
 int TermDbSygus::getKindArg( TypeNode tn, Kind k ) {
   Assert( isRegistered( tn ) );
   std::map< TypeNode, std::map< Kind, int > >::iterator itt = d_kinds.find( tn );
@@ -2348,6 +2355,7 @@ bool TermDbSygus::doCompare( Node a, Node b, Kind k ) {
   return com==d_true;
 }
 
+
 void doStrReplace(std::string& str, const std::string& oldStr, const std::string& newStr){
   size_t pos = 0;
   while((pos = str.find(oldStr, pos)) != std::string::npos){
@@ -2367,7 +2375,20 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >
         if( n.getNumChildren()>0 ){
           out << "(";
         }
-        out << dt[cIndex].getSygusOp();
+        Node op = dt[cIndex].getSygusOp();
+        if( op.getType().isBitVector() && op.isConst() ){
+          //print in the style it was given
+          Trace("sygus-print-bvc") << "[Print " << op << " " << dt[cIndex].getName() << "]" << std::endl;
+          std::stringstream ss;
+          ss << dt[cIndex].getName();
+          std::string str = ss.str();
+          std::size_t found = str.find_last_of("_");
+          Assert( found!=std::string::npos );
+          std::string name = std::string( str.begin() + found +1, str.end() );
+          out << name;
+        }else{
+          out << op;
+        }
         if( n.getNumChildren()>0 ){
           for( unsigned i=0; i<n.getNumChildren(); i++ ){
             out << " ";
@@ -2376,9 +2397,10 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >
           out << ")";
         }
       }else{
+        std::stringstream let_out;
         //print as let term
         if( dt[cIndex].getNumSygusLetInputArgs()>0 ){
-          out << "(let (";
+          let_out << "(let (";
         }
         std::vector< Node > subs_lvs;
         std::vector< Node > new_lvs;
@@ -2392,22 +2414,25 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >
           //map free variables to proper terms
           if( i<dt[cIndex].getNumSygusLetInputArgs() ){
             //it should be printed as a let argument
-            out << "(";
-            out << lv << " " << lv.getType() << " ";
-            printSygusTerm( out, n[i], lvs );
-            out << ")";
+            let_out << "(";
+            let_out << lv << " " << lv.getType() << " ";
+            printSygusTerm( let_out, n[i], lvs );
+            let_out << ")";
           }
         }
         if( dt[cIndex].getNumSygusLetInputArgs()>0 ){
-          out << ") ";
+          let_out << ") ";
         }
         //print the body
         Node let_body = Node::fromExpr( dt[cIndex].getSygusLetBody() );
         let_body = let_body.substitute( subs_lvs.begin(), subs_lvs.end(), new_lvs.begin(), new_lvs.end() );
         new_lvs.insert( new_lvs.end(), lvs.begin(), lvs.end() );
-        std::stringstream body_out;
-        printSygusTerm( body_out, let_body, new_lvs );
-        std::string body = body_out.str();
+        printSygusTerm( let_out, let_body, new_lvs );
+        if( dt[cIndex].getNumSygusLetInputArgs()>0 ){
+          let_out << ")";
+        }
+        //do variable substitutions since ASSUMING : let_vars are interpreted literally and do not represent a class of variables
+        std::string lbody = let_out.str();
         for( unsigned i=0; i<dt[cIndex].getNumSygusLetArgs(); i++ ){
           std::stringstream old_str;
           old_str << new_lvs[i];
@@ -2417,12 +2442,9 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >
           }else{
             new_str << Node::fromExpr( dt[cIndex].getSygusLetArg( i ) );
           }
-          doStrReplace( body, old_str.str().c_str(), new_str.str().c_str() );
-        }
-        out << body;
-        if( dt[cIndex].getNumSygusLetInputArgs()>0 ){
-          out << ")";
+          doStrReplace( lbody, old_str.str().c_str(), new_str.str().c_str() );
         }
+        out << lbody;
       }
       return;
     }
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index e61552713..1ffe0e29e 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -433,7 +433,7 @@ public:
   bool getMatch( Node n, TypeNode st, int& index_found, std::vector< Node >& args, int index_exc = -1, int index_start = 0 );
 private:
   //information for sygus types
-  std::map< TypeNode, TypeNode > d_register;  //stores sygus type
+  std::map< TypeNode, TypeNode > d_register;  //stores sygus -> builtin type
   std::map< TypeNode, std::map< int, Kind > > d_arg_kind;
   std::map< TypeNode, std::map< Kind, int > > d_kinds;
   std::map< TypeNode, std::map< int, Node > > d_arg_const;
@@ -455,6 +455,7 @@ private:
 public:
   TermDbSygus();
   bool isRegistered( TypeNode tn );
+  TypeNode sygusToBuiltinType( TypeNode tn );
   int getKindArg( TypeNode tn, Kind k );
   int getConstArg( TypeNode tn, Node n );
   int getOpArg( TypeNode tn, Node n );
@@ -485,7 +486,7 @@ public:
   Node getTypeValueOffset( TypeNode tn, Node val, int offset, int& status );
   /** get value */
   Node getTypeMaxValue( TypeNode tn );
-  TypeNode getSygusType( Node v );
+  TypeNode getSygusTypeForVar( Node v );
   Node mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre );
   Node sygusToBuiltin( Node n, TypeNode tn );
   Node builtinToSygusConst( Node c, TypeNode tn, int rcons_depth = 0 );
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 9f8f0d6cf..ccbbd5bd5 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -37,6 +37,7 @@
 #include "theory/uf/theory_uf.h"
 #include "theory/quantifiers/full_model_check.h"
 #include "theory/quantifiers/ambqi_builder.h"
+#include "theory/quantifiers/fun_def_engine.h"
 
 using namespace std;
 using namespace CVC4;
@@ -169,6 +170,12 @@ d_lemmas_produced_c(u){
   }else{
     d_alpha_equiv = NULL;
   }
+  //if( options::funDefs() ){
+  //  d_fun_def_engine = new quantifiers::FunDefEngine( this, c );
+  //  d_modules.push_back( d_fun_def_engine );
+  //}else{
+  d_fun_def_engine = NULL;
+  //}
 
   if( needsBuilder ){
     Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl;
@@ -208,6 +215,7 @@ QuantifiersEngine::~QuantifiersEngine(){
   delete d_sg_gen;
   delete d_ceg_inst;
   delete d_lte_part_inst;
+  delete d_fun_def_engine;
   for(std::map< Node, QuantPhaseReq* >::iterator i = d_phase_reqs.begin(); i != d_phase_reqs.end(); ++i) {
     delete (*i).second;
   }
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 3040a35c7..54f63bfe0 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -93,6 +93,7 @@ namespace quantifiers {
   class CegInstantiation;
   class LtePartialInst;
   class AlphaEquivalence;
+  class FunDefEngine;
 }/* CVC4::theory::quantifiers */
 
 namespace inst {
@@ -142,6 +143,8 @@ private:
   quantifiers::CegInstantiation * d_ceg_inst;
   /** lte partial instantiation */
   quantifiers::LtePartialInst * d_lte_part_inst;
+  /** function definitions engine */
+  quantifiers::FunDefEngine * d_fun_def_engine;
 public: //effort levels
   enum {
     QEFFORT_CONFLICT,
@@ -228,6 +231,8 @@ public:  //modules
   quantifiers::CegInstantiation * getCegInstantiation() { return d_ceg_inst; }
   /** local theory ext partial inst */
   quantifiers::LtePartialInst * getLtePartialInst() { return d_lte_part_inst; }
+  /** function definition engine */
+  quantifiers::FunDefEngine * getFunDefEngine() { return d_fun_def_engine; }
 private:
   /** owner of quantified formulas */
   std::map< Node, QuantifiersModule * > d_owner;
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index dbef0494a..9d7155f78 100644
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -38,7 +38,12 @@ TESTS = commutative.sy \
         let-simp.sy \
         tl-type.sy \
         dup-op.sy \
-        nflat-fwd.sy
+        nflat-fwd.sy \
+        nflat-fwd-3.sy \
+        enum-test.sy \
+        no-syntax-test-bool.sy \
+        inv-example.sy \
+        uminus_one.sy
 
 # sygus tests currently taking too long for make regress
 EXTRA_DIST = $(TESTS) \
diff --git a/test/regress/regress0/sygus/enum-test.sy b/test/regress/regress0/sygus/enum-test.sy
new file mode 100644
index 000000000..52a72c07d
--- /dev/null
+++ b/test/regress/regress0/sygus/enum-test.sy
@@ -0,0 +1,8 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si
+(set-logic LIA)
+(define-sort D (Enum (a b)))
+(define-fun f ((x D)) Int (ite (= x D::a) 3 7))
+(synth-fun g () D ((Start D (D::a D::b))))
+(constraint (= (f g) 7))
+(check-synth)
\ No newline at end of file
diff --git a/test/regress/regress0/sygus/inv-example.sy b/test/regress/regress0/sygus/inv-example.sy
new file mode 100644
index 000000000..dda8e0ed5
--- /dev/null
+++ b/test/regress/regress0/sygus/inv-example.sy
@@ -0,0 +1,12 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si
+(set-logic LIA)
+(synth-inv inv-f ((x Int) (y Int) (b Bool)))
+(declare-primed-var x Int)
+(declare-primed-var y Int)
+(declare-primed-var b Bool)
+(define-fun pre-f ((x Int) (y Int) (b Bool)) Bool (and (and (>= x 5) (<= x 9)) (and (>= y 1) (<= y 3))))
+(define-fun trans-f ((x Int) (y Int) (b Bool) (x! Int) (y! Int) (b! Bool)) Bool (and (and (= b! b) (= y! x)) (ite b (= x! (+ x 10)) (= x! (+ x 12)))))
+(define-fun post-f ((x Int) (y Int) (b Bool)) Bool (<= y x))
+(inv-constraint inv-f pre-f trans-f post-f)
+(check-synth)
\ No newline at end of file
diff --git a/test/regress/regress0/sygus/nflat-fwd-3.sy b/test/regress/regress0/sygus/nflat-fwd-3.sy
new file mode 100644
index 000000000..bd7c79e3e
--- /dev/null
+++ b/test/regress/regress0/sygus/nflat-fwd-3.sy
@@ -0,0 +1,11 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si
+(set-logic LIA)
+(synth-fun f ((x Int)) Int
+    ((Start Int ((+ (+ Con Con) Con) x))
+     (Con Int (0 1))))
+
+(declare-var x Int)
+(constraint (= (f x) 2))
+(check-synth)
+
diff --git a/test/regress/regress0/sygus/no-syntax-test-bool.sy b/test/regress/regress0/sygus/no-syntax-test-bool.sy
new file mode 100644
index 000000000..cc3855ad1
--- /dev/null
+++ b/test/regress/regress0/sygus/no-syntax-test-bool.sy
@@ -0,0 +1,15 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si
+
+(set-logic LIA)
+
+(synth-fun f ((x Int) (y Int)) Bool)
+
+(declare-var x Int)
+(declare-var y Int)
+
+(constraint (= (f x y) (>= (+ x y) 500)))
+
+
+(check-synth)
+
diff --git a/test/regress/regress0/sygus/uminus_one.sy b/test/regress/regress0/sygus/uminus_one.sy
new file mode 100644
index 000000000..b020c0bee
--- /dev/null
+++ b/test/regress/regress0/sygus/uminus_one.sy
@@ -0,0 +1,7 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi
+(set-logic LIA)
+(synth-fun f ((x Int)) Int ((Start Int ((- 1)))))
+(declare-var x Int)
+(constraint (= (f x) (- 1)))
+(check-synth)
\ No newline at end of file