From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 11 Jun 2015 13:03:52 +0000 (+0200)
Subject: Update experimental scripts.  Support top-level non-terminals in sygus grammars.... 
X-Git-Tag: cvc5-1.0.0~6295
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f1f79835adeac5c22fb744c38a83fef01d0002ad;p=cvc5.git

Update experimental scripts.  Support top-level non-terminals in sygus grammars.  Allow -N in sygus terms.  Minor bug fix in datatypes_sygus. Add regression.
---

diff --git a/contrib/run-script-smtcomp2015-application-experimental b/contrib/run-script-smtcomp2015-application-experimental
index dac870c75..81d05c774 100755
--- a/contrib/run-script-smtcomp2015-application-experimental
+++ b/contrib/run-script-smtcomp2015-application-experimental
@@ -36,7 +36,7 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA)
   runcvc4 --incremental
   ;;
 LIA|LRA|NIA|NRA)
-  runcvc4 --incremental --cbqi
+  runcvc4 --incremental --cbqi2
   ;;
 QF_BV)
   runcvc4 --incremental --unconstrained-simp --bv-eq-slicer=auto --bv-div-zero-const --bv-intro-pow2
diff --git a/contrib/run-script-smtcomp2015-experimental b/contrib/run-script-smtcomp2015-experimental
index 8aee209e0..02766943f 100755
--- a/contrib/run-script-smtcomp2015-experimental
+++ b/contrib/run-script-smtcomp2015-experimental
@@ -67,10 +67,14 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA)
   finishwith --full-saturate-quant
   ;;
 LIA|LRA|NIA|NRA)
-  trywith 180 --cbqi --full-saturate-quant
+  trywith 240 --cbqi2 --full-saturate-quant
   trywith 60 --full-saturate-quant
+  trywith 180 --cbqi --cbqi-recurse --full-saturate-quant
+  trywith 180 --cbqi2 --decision=internal --full-saturate-quant
   trywith 180 --qcf-tconstraint --full-saturate-quant
-  finishwith --cbqi --cbqi-recurse --full-saturate-quant
+  trywith 180 --cbqi --decision=internal --full-saturate-quant
+  trywith 180 --cbqi --full-saturate-quant
+  finishwith --cbqi2 --cbqi-recurse --full-saturate-quant
   ;;
 QF_AUFBV)
   trywith 600
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index aa56d1f2e..0f020c36e 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -496,7 +496,8 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
   std::vector< std::vector<Expr> > ops;
   std::vector< std::vector< std::string > > cnames;
   std::vector< std::vector< std::vector< CVC4::Type > > > cargs;
-  bool allow_const = false;
+  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;
@@ -609,30 +610,21 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
       { std::stringstream ss;
         ss << fun << "_" << name;
         std::string dname = ss.str();
-        PARSER_STATE->pushSygusDatatypeDef(t, dname, datatypes, sorts, ops, cnames, cargs);
+        PARSER_STATE->pushSygusDatatypeDef(t, dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym);
         if(!PARSER_STATE->isUnresolvedType(dname)) {
           // if not unresolved, must be undeclared
           PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT);
         }
         Type unres_t = PARSER_STATE->mkUnresolvedType(dname);
         sygus_to_builtin[unres_t] = t;
-        sygus_dt_index = ops.size()-1;
+        sygus_dt_index = datatypes.size()-1;
         Debug("parser-sygus") << "Read sygus grammar " << name << " under function " << fun << "..." << 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, sygus_vars, sygus_to_builtin, sygus_to_builtin_expr, allow_const, sygus_ret, -1]+ RPAREN_TOK
-      RPAREN_TOK
-      { Debug("parser-sygus") << "Making sygus datatypes..." << std::endl;
-        for( unsigned i=sygus_dt_index; i<datatypes.size(); i++ ){
-          Debug("parser-sygus") << "...make " << datatypes[i].getName() << " with builtin sort " << sorts[i] << std::endl;
-          if( sorts[i].isNull() ){
-            PARSER_STATE->parseError(std::string("Internal error : could not infer builtin sort for nested gterm."));
-          }
-          datatypes[i].setSygus( sorts[i], terms[0], sygus_dt_index==(int)i ? allow_const : false, false );
-          PARSER_STATE->mkSygusDatatype( datatypes[i], ops[i], cnames[i], cargs[i] );
-        }
-        PARSER_STATE->popScope(); }
+      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
+      RPAREN_TOK { PARSER_STATE->popScope(); }
     )+
     RPAREN_TOK { read_syntax = true; }
     )?
@@ -640,6 +632,20 @@ 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 );
+      }else{
+        Debug("parser-sygus") << "Making sygus datatypes..." << std::endl;
+        //make unresolved types to recognize 
+        for( unsigned i=0; i<datatypes.size(); i++ ){
+          PARSER_STATE->mkUnresolvedType(datatypes[i].getName());
+        }
+        for( unsigned i=0; i<datatypes.size(); i++ ){
+          Debug("parser-sygus") << "...make " << datatypes[i].getName() << " with builtin sort " << sorts[i] << std::endl;
+          if( sorts[i].isNull() ){
+            PARSER_STATE->parseError(std::string("Internal error : could not infer builtin sort for nested gterm."));
+          }
+          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] );
+        }
       }
       PARSER_STATE->popScope();
       Debug("parser-sygus") << "Make " << datatypes.size() << " mutual datatypes..." << std::endl;
@@ -739,9 +745,11 @@ sygusGTerm[int index,
            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,
-           bool& allow_const, CVC4::Type& ret, int gtermType]
+           CVC4::Type& ret, int gtermType]
 @declarations {
   std::string name;
   Kind k;
@@ -751,7 +759,6 @@ sygusGTerm[int index,
   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;
-  bool sub_allow_const = false;
   Type sub_ret;
   int sub_dt_index = -1;
   std::string sub_dname;
@@ -759,7 +766,7 @@ sygusGTerm[int index,
   Expr null_expr;
   std::vector< Expr > let_vars;
   int let_start_index = -1;
-  int let_end_index = -1;
+  //int let_end_index = -1;
   int let_end_arg_index = -1;
   Expr let_func;
 }
@@ -792,21 +799,23 @@ sygusGTerm[int index,
           std::stringstream ss;
           ss << datatypes[index].getName() << "_let_var_" << let_vars.size();
           sub_dname = ss.str();
-          PARSER_STATE->pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs );
+          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,sygus_vars,sygus_to_builtin,sygus_to_builtin_expr,sub_allow_const,sub_ret,sub_gtermType] {
+        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, sygus_to_builtin, sygus_to_builtin_expr, sub_ret );
+          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_index = datatypes.size();
           let_end_arg_index = cargs[index].back().size();
         }
     | SYGUS_CONSTANT_TOK sortSymbol[t,CHECK_DECLARED] 
-      { sub_gtermType = 2; allow_const = true;Debug("parser-sygus") << "Sygus grammar constant." << std::endl; }
+      { sub_gtermType = 2; allow_const[index] = true;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; }
     | SYGUS_LOCAL_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED]
@@ -852,26 +861,28 @@ sygusGTerm[int index,
       std::stringstream ss;
       ss << datatypes[index].getName() << "_" << name << "_arg_" << count;
       sub_dname = ss.str();
-      PARSER_STATE->pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs );
+      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,sygus_vars,sygus_to_builtin,sygus_to_builtin_expr,sub_allow_const,sub_ret,sub_gtermType]
+    ( 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, sygus_to_builtin, sygus_to_builtin_expr, sub_ret );
+        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() << "_" << name << "_arg_" << count;
         sub_dname = ss.str();
-        PARSER_STATE->pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs );
+        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 );       
+        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() ){
@@ -916,7 +927,7 @@ sygusGTerm[int index,
           //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 );
+          //  PARSER_STATE->popSygusDatatypeDef( datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
           //}
           //Debug("parser-sygus") << "Done let body datatypes" << std::endl;
         }else{
@@ -969,7 +980,8 @@ sygusGTerm[int index,
           ret = PARSER_STATE->getSort(name);
         }else{
           if( gtermType==-1 ){
-            //if we don't know what this symbol is, and it is top level, just ignore it
+            Debug("parser-sygus") << "Sygus grammar " << fun << " : unresolved symbol " << name << std::endl;
+            unresolved_gterm_sym[index].push_back(name);
           }else{
             Debug("parser-sygus") << "Sygus grammar " << fun << " : unresolved " << name << std::endl;
             ret = PARSER_STATE->mkUnresolvedType(name);
@@ -1783,19 +1795,23 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
 
     /* a variable */
   | symbol[name,CHECK_DECLARED,SYM_VARIABLE]
-    { const bool isDefinedFunction =
-        PARSER_STATE->isDefinedFunction(name);
-      if(PARSER_STATE->isAbstractValue(name)) {
-        expr = PARSER_STATE->mkAbstractValue(name);
-      } else if(isDefinedFunction) {
-        expr = MK_EXPR(CVC4::kind::APPLY,
-                       PARSER_STATE->getFunction(name));
-      } else {
-        expr = PARSER_STATE->getVariable(name);
-        Type t = PARSER_STATE->getType(name);
-        if(t.isConstructor() && ConstructorType(t).getArity() == 0) {
-          // don't require parentheses, immediately turn it into an apply
-          expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, expr);
+    { if( PARSER_STATE->sygus() && name[0]=='-' ){ //allow unary minus in sygus
+        expr = MK_CONST(Rational(name));
+      }else{
+        const bool isDefinedFunction =
+          PARSER_STATE->isDefinedFunction(name);
+        if(PARSER_STATE->isAbstractValue(name)) {
+          expr = PARSER_STATE->mkAbstractValue(name);
+        } else if(isDefinedFunction) {
+          expr = MK_EXPR(CVC4::kind::APPLY,
+                        PARSER_STATE->getFunction(name));
+        } else {
+          expr = PARSER_STATE->getVariable(name);
+          Type t = PARSER_STATE->getType(name);
+          if(t.isConstructor() && ConstructorType(t).getArity() == 0) {
+            // don't require parentheses, immediately turn it into an apply
+            expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, expr);
+          }
         }
       }
     }
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 7db87d579..ceab0a779 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -500,7 +500,7 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin
                                   std::vector<Type>& sorts, std::vector< std::vector<Expr> >& ops, std::vector<Expr> sygus_vars ) {
 
   Debug("parser-sygus") << "Construct default grammar for " << fun << " " << range << std::endl;
-
+  
   std::stringstream ssb;
   ssb << fun << "_Bool";
   std::string dbname = ssb.str();
@@ -512,6 +512,7 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin
   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
   for( unsigned i=0; i<sygus_vars.size(); i++ ){
     if( sygus_vars[i].getType()==range ){
@@ -561,7 +562,7 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin
   }
   Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl;
   datatypes.back().setSygus( range, bvl, true, true );
-  mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs );
+  mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs, unresolved_gterm_sym );
   sorts.push_back( range );
 
   //Boolean type
@@ -597,7 +598,7 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin
   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 );
+  mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs, unresolved_gterm_sym );
   sorts.push_back( btype );
 
   Debug("parser-sygus") << "...finished make default grammar for " << fun << " " << range << std::endl;
@@ -622,12 +623,16 @@ bool Smt2::pushSygusDatatypeDef( Type t, std::string& dname,
                                   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< std::vector< std::vector< CVC4::Type > > >& cargs,
+                                  std::vector< bool >& allow_const,
+                                  std::vector< std::vector< std::string > >& unresolved_gterm_sym ){
   sorts.push_back(t);
   datatypes.push_back(Datatype(dname));
   ops.push_back(std::vector<Expr>());
   cnames.push_back(std::vector<std::string>());
   cargs.push_back(std::vector<std::vector<CVC4::Type> >());
+  allow_const.push_back(false);
+  unresolved_gterm_sym.push_back(std::vector< std::string >());
   return true;
 }
 
@@ -635,12 +640,16 @@ bool Smt2::popSygusDatatypeDef( 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< std::vector< std::vector< CVC4::Type > > >& cargs,
+                                 std::vector< bool >& allow_const,
+                                 std::vector< std::vector< std::string > >& unresolved_gterm_sym ){
   sorts.pop_back();
   datatypes.pop_back();
   ops.pop_back();
   cnames.pop_back();
   cargs.pop_back();
+  allow_const.pop_back();
+  unresolved_gterm_sym.pop_back();
   return true;
 }
 
@@ -649,6 +658,8 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st
                                     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 ) {
   Type t = sub_ret;
@@ -705,7 +716,7 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st
     Debug("parser-sygus") << "...removing " << datatypes.back().getName() << std::endl;
     //otherwise, datatype was unecessary
     //pop argument datatype definition
-    popSygusDatatypeDef( datatypes, sorts, ops, cnames, cargs );
+    popSygusDatatypeDef( datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
   }
   return t;
 }
@@ -870,7 +881,10 @@ void Smt2::defineSygusFuns() {
 }
 
 void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
-                            std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs ) {
+                            std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs,
+                            std::vector<std::string>& unresolved_gterm_sym ) {
+  Debug("parser-sygus") << "Making sygus datatype " << dt.getName() << std::endl;
+  Debug("parser-sygus") << "  add constructors..." << std::endl;
   for( int i=0; i<(int)cnames.size(); i++ ){
     bool is_dup = false;
     //FIXME : should allow multiple operators with different sygus type arguments
@@ -899,13 +913,6 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
       cargs.erase( cargs.begin() + i, cargs.begin() + i + 1 );
       i--;
     }else{
-      std::string name = dt.getName() + "_" + cnames[i];
-      std::string testerId("is-");
-      testerId.append(name);
-      checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
-      checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
-      CVC4::DatatypeConstructor c(name, testerId );
-      Debug("parser-sygus") << "--> Add constructor " << cnames[i] << " to " << dt.getName() << std::endl;
       Expr let_body;
       std::vector< Expr > let_args;
       unsigned let_num_input_args = 0;
@@ -914,19 +921,73 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
         let_body = it->second;
         let_args.insert( let_args.end(), d_sygus_let_func_to_vars[ops[i]].begin(), d_sygus_let_func_to_vars[ops[i]].end() );
         let_num_input_args = d_sygus_let_func_to_num_input_vars[ops[i]];
-        Debug("parser-sygus") << "    it is a let gterm with body " << let_body << std::endl;
       }
-      c.setSygus( ops[i], let_body, let_args, let_num_input_args );
-      for( unsigned j=0; j<cargs[i].size(); j++ ){
-        std::stringstream sname;
-        sname << name << "_" << j;
-        c.addArg(sname.str(), cargs[i][j]);
+      addSygusDatatypeConstructor( dt, ops[i], cnames[i], cargs[i], let_body, let_args, let_num_input_args );
+    }
+  }
+  Debug("parser-sygus") << "  add constructors for unresolved symbols..." << std::endl;
+  if( !unresolved_gterm_sym.empty() ){
+    std::vector< Type > types;
+    Debug("parser-sygus") << "...resolve " << unresolved_gterm_sym.size() << " symbols..." << std::endl;
+    for( unsigned i=0; i<unresolved_gterm_sym.size(); i++ ){
+      Debug("parser-sygus") << "  resolve : " << unresolved_gterm_sym[i] << std::endl;
+      if( isUnresolvedType(unresolved_gterm_sym[i]) ){
+        Debug("parser-sygus") << "    it is an unresolved type." << std::endl;
+        Type t = getSort(unresolved_gterm_sym[i]);
+        if( std::find( types.begin(), types.end(), t )==types.end() ){
+          types.push_back( t );
+          //identity element
+          Type bt = dt.getSygusType();
+          Debug("parser-sygus") << ":  make identity function for " << bt << ", argument type " << t << std::endl;
+          std::stringstream ss;
+          ss << t << "_x_id";
+          Expr let_body = mkBoundVar(ss.str(), bt);
+          std::vector< Expr > let_args;
+          let_args.push_back( let_body );
+          //make the identity function
+          Type ft = getExprManager()->mkFunctionType(bt, bt);
+          std::stringstream ssid;
+          ssid << unresolved_gterm_sym[i] << "_id";
+          Expr id_op = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED);
+          preemptCommand( new DefineFunctionCommand(ssid.str(), id_op, let_args, let_body) );
+          //make the sygus argument list
+          std::vector< Type > id_carg;
+          id_carg.push_back( t );
+          addSygusDatatypeConstructor( dt, id_op, unresolved_gterm_sym[i], id_carg, let_body, let_args, 0 );
+          //add to operators
+          ops.push_back( id_op );
+        }
+      }else{
+        Debug("parser-sygus") << "    ignore. (likely a free let variable)" << std::endl;
       }
-      dt.addConstructor(c);
     }
   }
+  
 }
 
+void Smt2::addSygusDatatypeConstructor( CVC4::Datatype& dt, CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs,
+                                        CVC4::Expr& let_body, std::vector< CVC4::Expr >& let_args, unsigned let_num_input_args ) {
+  
+  std::string name = dt.getName() + "_" + cname;
+  std::string testerId("is-");
+  testerId.append(name);
+  checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
+  checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
+  CVC4::DatatypeConstructor c(name, testerId );
+  Debug("parser-sygus") << "--> Add constructor " << cname << " to " << dt.getName() << std::endl;
+  if( !let_body.isNull() ){
+    Debug("parser-sygus") << "    let body = " << let_body << ", args = " << let_args.size() << "," << let_num_input_args << std::endl;
+  }
+  c.setSygus( op, let_body, let_args, let_num_input_args );
+  for( unsigned j=0; j<cargs.size(); j++ ){
+    std::stringstream sname;
+    sname << name << "_" << j;
+    c.addArg(sname.str(), cargs[j]);
+  }
+  dt.addConstructor(c);
+}
+
+
 // i is index in datatypes/ops
 // j is index is datatype
 Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vector< std::vector<Expr> >& ops,
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 428977e0b..cfd062457 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -188,19 +188,25 @@ public:
                                     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< std::vector< std::vector< CVC4::Type > > >& cargs,
+                                    std::vector< bool >& allow_const,
+                                    std::vector< std::vector< std::string > >& unresolved_gterm_sym );
 
   static bool popSygusDatatypeDef( 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< 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 );
 
@@ -223,7 +229,8 @@ public:
   void defineSygusFuns();
 
   void mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
-                        std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs );
+                        std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs,
+                        std::vector<std::string>& unresolved_gterm_sym );
 
   // i is index in datatypes/ops
   // j is index is datatype
@@ -265,6 +272,12 @@ public:
         name.find_first_not_of("0123456789", 1) != std::string::npos ) {
       this->Parser::checkDeclaration(name, check, type, notes);
       return;
+    }else{
+      //it is allowable in sygus
+      if( sygus() && name[0]=='-' ){
+        //do not check anything
+        return;
+      }
     }
 
     std::stringstream ss;
@@ -304,6 +317,9 @@ private:
   std::map< CVC4::Expr, unsigned > d_sygus_let_func_to_num_input_vars;
   
   void collectSygusLetArgs( CVC4::Expr e, std::vector< CVC4::Type >& sygusArgs, std::vector< CVC4::Expr >& builtinArgs );
+  
+  void addSygusDatatypeConstructor( CVC4::Datatype& dt, CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs,
+                                    CVC4::Expr& let_body, std::vector< CVC4::Expr >& let_args, unsigned let_num_input_args );
 
   void addArithmeticOperators();
 
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index a9e6b3a78..d08c92dd9 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -1114,12 +1114,13 @@ bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node
 }
 
 bool SygusSymBreak::isSeparation( Node rep_prog, Node tst_curr, std::map< Node, std::vector< Node > >& testers_u, std::vector< Node >& rlv_testers ) {
-  Trace("sygus-nf-gen-debug") << "is separation " << rep_prog << " " << tst_curr << std::endl;
   TypeNode tn = tst_curr[0].getType();
+  Trace("sygus-nf-gen-debug") << "is separation " << rep_prog << " " << tst_curr << " " << tn << std::endl;
   Node rop = rep_prog.getNumChildren()==0 ? rep_prog : rep_prog.getOperator();
   //we can continue if the tester in question is relevant
   if( std::find( rlv_testers.begin(), rlv_testers.end(), tst_curr )!=rlv_testers.end() ){
     unsigned tindex = Datatype::indexOf( tst_curr.getOperator().toExpr() );
+    d_tds->registerSygusType( tn );
     Node op = d_tds->getArgOp( tn, tindex );
     if( op!=rop ){
       Trace("sygus-nf-gen-debug") << "mismatch, success." << std::endl;
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 79199d8b4..60573a7fc 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -2070,7 +2070,9 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >
         }
       }else{
         //print as let term
-        out << "(let (";
+        if( dt[cIndex].getNumSygusLetInputArgs()>0 ){
+          out << "(let (";
+        }
         std::vector< Node > subs_lvs;
         std::vector< Node > new_lvs;
         for( unsigned i=0; i<dt[cIndex].getNumSygusLetArgs(); i++ ){
@@ -2089,7 +2091,9 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >
             out << ")";
           }
         }
-        out << ") ";
+        if( dt[cIndex].getNumSygusLetInputArgs()>0 ){
+          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() );
@@ -2104,7 +2108,10 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >
           printSygusTerm( new_str, n[i], lvs );
           doReplace( body, old_str.str().c_str(), new_str.str().c_str() );
         }
-        out << body << ")";
+        out << body;
+        if( dt[cIndex].getNumSygusLetInputArgs()>0 ){
+          out << ")";
+        }
       }
       return;
     }
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index dc6a1e0d1..abf51d992 100644
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -35,7 +35,8 @@ TESTS = commutative.sy \
         no-flat-simp.sy \
         twolets2-orig.sy \
         let-ringer.sy \
-        let-simp.sy
+        let-simp.sy \
+        tl-type.sy
 
 # sygus tests currently taking too long for make regress
 EXTRA_DIST = $(TESTS) \
diff --git a/test/regress/regress0/sygus/tl-type.sy b/test/regress/regress0/sygus/tl-type.sy
new file mode 100644
index 000000000..a8da13742
--- /dev/null
+++ b/test/regress/regress0/sygus/tl-type.sy
@@ -0,0 +1,11 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi --no-cegqi-si
+(set-logic LIA)
+(synth-fun f ((x Int)) Int
+    ((Start Int (Term (+ Start Start)))
+     (Term Int (x 0))))
+
+(declare-var x Int)
+(constraint (= (f x) (* 3 x)))
+(check-synth)
+