Disallow let in sygus grammars, check for free variables in sygus constructors (#3259)

13 files changed, 76 insertions, 315 deletions

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 5e1343bb0..cd78728b1 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -25,10 +25,11 @@
 #include "expr/expr_manager_scope.h"
 #include "expr/matcher.h"
 #include "expr/node.h"
+#include "expr/node_algorithm.h"
 #include "expr/node_manager.h"
 #include "expr/type.h"
-#include "options/set_language.h"
 #include "options/datatypes_options.h"
+#include "options/set_language.h"
 
 using namespace std;
 
@@ -154,6 +155,36 @@ void Datatype::resolve(ExprManager* em,
     }
     d_record = new Record(fields);
   }
+
+  if (isSygus())
+  {
+    // all datatype constructors should be sygus and have sygus operators whose
+    // free variables are subsets of sygus bound var list.
+    Node sbvln = Node::fromExpr(d_sygus_bvl);
+    std::unordered_set<Node, NodeHashFunction> svs;
+    for (const Node& sv : sbvln)
+    {
+      svs.insert(sv);
+    }
+    for (unsigned i = 0, ncons = d_constructors.size(); i < ncons; i++)
+    {
+      Expr sop = d_constructors[i].getSygusOp();
+      PrettyCheckArgument(!sop.isNull(),
+                          this,
+                          "Sygus datatype contains a non-sygus constructor");
+      Node sopn = Node::fromExpr(sop);
+      std::unordered_set<Node, NodeHashFunction> fvs;
+      expr::getFreeVariables(sopn, fvs);
+      for (const Node& v : fvs)
+      {
+        PrettyCheckArgument(
+            svs.find(v) != svs.end(),
+            this,
+            "Sygus constructor has an operator with a free variable that is "
+            "not in the formal argument list of the function-to-synthesize");
+      }
+    }
+  }
 }
 
 void Datatype::addConstructor(const DatatypeConstructor& c) {
diff --git a/src/parser/parser.h b/src/parser/parser.h
index a1ee24bb6..28a033eb9 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -49,7 +49,6 @@ class CVC4_PUBLIC SygusGTerm {
 public:
   enum{
     gterm_op,
-    gterm_let,
     gterm_constant,
     gterm_variable,
     gterm_input_variable,
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 6a0bf2188..21e09317d 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -886,28 +886,12 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
   Type t;
   std::string sname;
   std::vector< Expr > let_vars;
-  bool readingLet = false;
   std::string s;
   CVC4::api::Term atomTerm;
 }
   : LPAREN_TOK
     //read operator
-    ( SYGUS_LET_TOK LPAREN_TOK {
-         sgt.d_name = std::string("let");
-         sgt.d_gterm_type = SygusGTerm::gterm_let;
-         PARSER_STATE->pushScope(true);
-         readingLet = true;
-       }
-       ( LPAREN_TOK
-        symbol[sname,CHECK_NONE,SYM_VARIABLE]
-        sortSymbol[t,CHECK_DECLARED] {
-          Expr v = PARSER_STATE->mkBoundVar(sname,t);
-          sgt.d_let_vars.push_back( v );
-          sgt.addChild();
-        }
-        sygusGTerm[sgt.d_children.back(), fun]
-        RPAREN_TOK )+ RPAREN_TOK
-    | SYGUS_CONSTANT_TOK sortSymbol[t,CHECK_DECLARED]
+    ( SYGUS_CONSTANT_TOK sortSymbol[t,CHECK_DECLARED]
       { sgt.d_gterm_type = SygusGTerm::gterm_constant;
         sgt.d_type = t;
         Debug("parser-sygus") << "Sygus grammar constant." << std::endl;
@@ -971,9 +955,6 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
     RPAREN_TOK {
       //pop last child index
       sgt.d_children.pop_back();
-      if( readingLet ){
-        PARSER_STATE->popScope();
-      }
     }
     | termAtomic[atomTerm]
       {
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 1ca9ee2c8..bbfaf186e 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -879,10 +879,9 @@ void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index,
                               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 ){
+  if (sgt.d_gterm_type == SygusGTerm::gterm_op)
+  {
     Debug("parser-sygus") << "Add " << sgt.d_expr << " to datatype " << index
-                          << ", isLet = "
-                          << (sgt.d_gterm_type == SygusGTerm::gterm_let)
                           << std::endl;
     Kind oldKind;
     Kind newKind = kind::UNDEFINED_KIND;
@@ -922,12 +921,9 @@ void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index,
                                          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 ){
+  }
+  else if (sgt.d_gterm_type == SygusGTerm::gterm_constant)
+  {
     if( sgt.getNumChildren()!=0 ){
       parseError("Bad syntax for Sygus Constant.");
     }
@@ -943,7 +939,10 @@ void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index,
       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 ){
+  }
+  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.");
     }
@@ -958,9 +957,13 @@ void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index,
         cargs[index].push_back( std::vector< CVC4::Type >() );
       }
     }
-  }else if( sgt.d_gterm_type==SygusGTerm::gterm_nested_sort ){
+  }
+  else if (sgt.d_gterm_type == SygusGTerm::gterm_nested_sort)
+  {
     ret = sgt.d_type;
-  }else if( sgt.d_gterm_type==SygusGTerm::gterm_unresolved ){
+  }
+  else if (sgt.d_gterm_type == SygusGTerm::gterm_unresolved)
+  {
     if( isNested ){
       if( isUnresolvedType(sgt.d_name) ){
         ret = getSort(sgt.d_name);
@@ -974,8 +977,10 @@ void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index,
       //will resolve when adding constructors
       unresolved_gterm_sym[index].push_back(sgt.d_name);
     }
-  }else if( sgt.d_gterm_type==SygusGTerm::gterm_ignore ){
-
+  }
+  else if (sgt.d_gterm_type == SygusGTerm::gterm_ignore)
+  {
+    // do nothing
   }
 }
 
@@ -1098,112 +1103,6 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st
   return t;
 }
 
-void Smt2::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 ) {
-  std::vector< CVC4::Expr > let_define_args;
-  Expr let_body;
-  int dindex = cargs[index].size()-1;
-  Debug("parser-sygus") << "Process let constructor for datatype " << datatypes[index].getName() << ", #subtypes = " << cargs[index][dindex].size() << std::endl;
-  for( unsigned i=0; i<cargs[index][dindex].size(); i++ ){
-    Debug("parser-sygus") << "  " << i << " : " << cargs[index][dindex][i] << std::endl;
-    if( i+1==cargs[index][dindex].size() ){
-      std::map< CVC4::Type, CVC4::Expr >::iterator it = sygus_to_builtin_expr.find( cargs[index][dindex][i] );
-      if( it!=sygus_to_builtin_expr.end() ){
-        let_body = it->second;
-      }else{
-        std::stringstream ss;
-        ss << datatypes[index].getName() << "_body";
-        let_body = mkBoundVar(ss.str(), sygus_to_builtin[cargs[index][dindex][i]]);
-        d_sygus_bound_var_type[let_body] = cargs[index][dindex][i];
-      }
-    }
-  }
-  Debug("parser-sygus") << std::endl;
-  Debug("parser-sygus") << "Body is " << let_body << std::endl;
-  Debug("parser-sygus") << "# let vars = " << let_vars.size() << std::endl;
-  for( unsigned i=0; i<let_vars.size(); i++ ){
-    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;
-    if( !cargs[i].empty() ){
-      Debug("parser-sygus") << "  operator 0 is " << ops[i][0] << std::endl;
-      Debug("parser-sygus") << "  cons 0 has " << cargs[i][0].size() << " sub fields." << std::endl;
-      for( unsigned j=0; j<cargs[i][0].size(); j++ ){
-        Type bt = sygus_to_builtin[cargs[i][0][j]];
-        Debug("parser-sygus") << "    cons 0, selector " << j << " : " << cargs[i][0][j] << " " << bt << std::endl;
-      }
-    }
-  }
-  */
-  //last argument is the return, pop
-  cargs[index][dindex].pop_back();
-  collectSygusLetArgs( let_body, cargs[index][dindex], let_define_args );
-
-  Debug("parser-sygus") << "Make define-fun with "
-                        << cargs[index][dindex].size()
-                        << " operator arguments and " << let_define_args.size()
-                        << " provided arguments..." << std::endl;
-  if (cargs[index][dindex].size() != let_define_args.size())
-  {
-    std::stringstream ss;
-    ss << "Wrong number of let body terms." << std::endl;
-    parseError(ss.str());
-  }
-  std::vector<CVC4::Type> fsorts;
-  for( unsigned i=0; i<cargs[index][dindex].size(); i++ ){
-    Debug("parser-sygus") << "  " << i << " : " << let_define_args[i] << " " << let_define_args[i].getType() << " " << cargs[index][dindex][i] << std::endl;
-    fsorts.push_back(let_define_args[i].getType());
-  }
-
-  Type ft = getExprManager()->mkFunctionType(fsorts, let_body.getType());
-  std::stringstream ss;
-  ss << datatypes[index].getName() << "_let";
-  Expr let_func = mkVar(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED);
-  d_sygus_defined_funs.push_back( let_func );
-  preemptCommand( new DefineFunctionCommand(ss.str(), let_func, let_define_args, let_body) );
-
-  ops[index].pop_back();
-  ops[index].push_back( let_func );
-  cnames[index].pop_back();
-  cnames[index].push_back(ss.str());
-
-  //mark function as let constructor
-  d_sygus_let_func_to_vars[let_func].insert( d_sygus_let_func_to_vars[let_func].end(), let_define_args.begin(), let_define_args.end() );
-  d_sygus_let_func_to_body[let_func] = let_body;
-  d_sygus_let_func_to_num_input_vars[let_func] = let_vars.size();
-}
-
-
-void Smt2::collectSygusLetArgs( CVC4::Expr e, std::vector< CVC4::Type >& sygusArgs, std::vector< CVC4::Expr >& builtinArgs ) {
-  if( e.getKind()==kind::BOUND_VARIABLE ){
-    if( std::find( builtinArgs.begin(), builtinArgs.end(), e )==builtinArgs.end() ){
-      builtinArgs.push_back( e );
-      sygusArgs.push_back( d_sygus_bound_var_type[e] );
-      if( d_sygus_bound_var_type[e].isNull() ){
-        std::stringstream ss;
-        ss << "While constructing body of let gterm, can't map " << e << " to sygus type." << std::endl;
-        parseError(ss.str());
-      }
-    }
-  }else{
-    for( unsigned i=0; i<e.getNumChildren(); i++ ){
-      collectSygusLetArgs( e[i], sygusArgs, builtinArgs );
-    }
-  }
-}
-
 void Smt2::setSygusStartIndex( std::string& fun, int startIndex,
                                std::vector< CVC4::Datatype >& datatypes,
                                std::vector< CVC4::Type>& sorts,
@@ -1303,31 +1202,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
       }
       else
       {
-        std::map<Expr, Expr>::iterator it =
-            d_sygus_let_func_to_body.find(ops[i]);
-        if (it != d_sygus_let_func_to_body.end())
-        {
-          Debug("parser-sygus") << "--> Let expression " << ops[i] << std::endl;
-          Expr let_body = it->second;
-          std::vector<Expr> let_args = d_sygus_let_func_to_vars[ops[i]];
-          unsigned let_num_input_args =
-              d_sygus_let_func_to_num_input_vars[ops[i]];
-          // the operator is just the body for the arguments
-          std::vector<Type> ltypes;
-          for (unsigned j = 0, size = let_args.size(); j < size; j++)
-          {
-            ltypes.push_back(let_args[j].getType());
-          }
-          std::vector<Expr> largs;
-          Expr lbvl = makeSygusBoundVarList(dt, i, ltypes, largs);
-          Expr sbody = let_body.substitute(let_args, largs);
-          ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, sbody);
-          Debug("parser-sygus") << "  ...replace op : " << ops[i] << std::endl;
-          // callback prints as a let expression
-          spc = std::make_shared<printer::SygusLetExprPrintCallback>(
-              let_body, let_args, let_num_input_args);
-        }
-        else if (ops[i].getType().isBitVector() && ops[i].isConst())
+        if (ops[i].getType().isBitVector() && ops[i].isConst())
         {
           Debug("parser-sygus") << "--> Bit-vector constant " << ops[i] << " ("
                                 << cnames[i] << ")" << std::endl;
@@ -1419,7 +1294,9 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
           ops.push_back( id_op );
         }
       }else{
-        Debug("parser-sygus") << "    ignore. (likely a free let variable)" << std::endl;
+        std::stringstream ss;
+        ss << "Unhandled sygus constructor " << unresolved_gterm_sym[i];
+        throw ParserException(ss.str());
       }
     }
   }
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 83628d215..178634693 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -508,13 +508,6 @@ class Smt2 : public Parser
   //------------------------- end processing parse operators
  private:
   std::map< CVC4::Expr, CVC4::Type > d_sygus_bound_var_type;
-  std::map< CVC4::Expr, std::vector< CVC4::Expr > > d_sygus_let_func_to_vars;
-  std::map< CVC4::Expr, CVC4::Expr > d_sygus_let_func_to_body;
-  std::map< CVC4::Expr, unsigned > d_sygus_let_func_to_num_input_vars;
-  //auxiliary define-fun functions introduced for production rules
-  std::vector< CVC4::Expr > d_sygus_defined_funs;
-
-  void collectSygusLetArgs( CVC4::Expr e, std::vector< CVC4::Type >& sygusArgs, std::vector< CVC4::Expr >& builtinArgs );
 
   Type processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector< CVC4::Datatype >& datatypes,
                                 std::vector< CVC4::Type>& sorts,
@@ -526,16 +519,6 @@ class Smt2 : public Parser
                                 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 );
-
   /** make sygus bound var list
    *
    * This is used for converting non-builtin sygus operators to lambda
diff --git a/src/printer/sygus_print_callback.cpp b/src/printer/sygus_print_callback.cpp
index e320d5dfd..2b6d5fc1e 100644
--- a/src/printer/sygus_print_callback.cpp
+++ b/src/printer/sygus_print_callback.cpp
@@ -96,79 +96,6 @@ void SygusExprPrintCallback::toStreamSygus(const Printer* p,
   }
 }
 
-SygusLetExprPrintCallback::SygusLetExprPrintCallback(
-    Expr let_body, std::vector<Expr>& let_args, unsigned ninput_args)
-    : SygusExprPrintCallback(let_body, let_args),
-      d_num_let_input_args(ninput_args)
-{
-}
-
-void SygusLetExprPrintCallback::toStreamSygus(const Printer* p,
-                                              std::ostream& out,
-                                              Expr e) const
-{
-  std::stringstream let_out;
-  // print as let term
-  if (d_num_let_input_args > 0)
-  {
-    let_out << "(let (";
-  }
-  std::vector<Node> subs_lvs;
-  std::vector<Node> new_lvs;
-  for (unsigned i = 0, size = d_args.size(); i < size; i++)
-  {
-    Node v = d_args[i];
-    subs_lvs.push_back(v);
-    std::stringstream ss;
-    ss << "_l_" << new_lvs.size();
-    Node lv = NodeManager::currentNM()->mkBoundVar(ss.str(), v.getType());
-    new_lvs.push_back(lv);
-    // map free variables to proper terms
-    if (i < d_num_let_input_args)
-    {
-      // it should be printed as a let argument
-      let_out << "(";
-      let_out << lv << " " << lv.getType() << " ";
-      p->toStreamSygus(let_out, e[i]);
-      let_out << ")";
-    }
-  }
-  if (d_num_let_input_args > 0)
-  {
-    let_out << ") ";
-  }
-  // print the body
-  Node slet_body = Node::fromExpr(d_body);
-  slet_body = slet_body.substitute(
-      subs_lvs.begin(), subs_lvs.end(), new_lvs.begin(), new_lvs.end());
-  // new_lvs.insert(new_lvs.end(), lvs.begin(), lvs.end());
-  p->toStreamSygus(let_out, slet_body);
-  if (d_num_let_input_args > 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, size = d_args.size(); i < size; i++)
-  {
-    std::stringstream old_str;
-    old_str << new_lvs[i];
-    std::stringstream new_str;
-    if (i >= d_num_let_input_args)
-    {
-      p->toStreamSygus(new_str, Node::fromExpr(e[i]));
-    }
-    else
-    {
-      new_str << d_args[i];
-    }
-    doStrReplace(lbody, old_str.str().c_str(), new_str.str().c_str());
-  }
-  out << lbody;
-}
-
 SygusNamedPrintCallback::SygusNamedPrintCallback(std::string name)
     : d_name(name)
 {
diff --git a/src/printer/sygus_print_callback.h b/src/printer/sygus_print_callback.h
index d956fd4c6..d10a312bd 100644
--- a/src/printer/sygus_print_callback.h
+++ b/src/printer/sygus_print_callback.h
@@ -68,45 +68,6 @@ class CVC4_PUBLIC SygusExprPrintCallback : public SygusPrintCallback
                     const std::string& newStr) const;
 };
 
-/** sygus let expression constructor printer
- *
- * This class is used for printing sygus
- * datatype constructor terms whose top symbol
- * is a let expression.
- * For example, for grammar:
- *   A -> (let ((x B)) (+ A 1)) | x | (+ A A) | 0
- *   B -> 0 | 1
- * the first constructor for A takes as arguments
- * (B,A) and has sygus operator
- *   (lambda ((y Int) (z Int)) (+ z 1))
- * CVC4's support for let expressions in grammars
- * is highly limited, since notice that the
- * argument y : B is unused.
- *
- * For the above constructor, we have that
- *   d_let_body is (+ z 1),
- *   d_sygus_let_args is { y, z },
- *   d_sygus_num_let_input_args is 1, since
- *     y is an original input argument of the
- *     let expression, but z is not.
- */
-class CVC4_PUBLIC SygusLetExprPrintCallback : public SygusExprPrintCallback
-{
- public:
-  SygusLetExprPrintCallback(Expr let_body,
-                            std::vector<Expr>& let_args,
-                            unsigned ninput_args);
-  ~SygusLetExprPrintCallback() {}
-  /** print sygus term e on output out using printer p */
-  virtual void toStreamSygus(const Printer* p,
-                             std::ostream& out,
-                             Expr e) const override;
-
- private:
-  /** number of arguments that are interpreted as input arguments */
-  unsigned d_num_let_input_args;
-};
-
 /** sygus named constructor printer
  *
  * This callback is used for explicitly naming
diff --git a/test/regress/regress0/sygus/let-ringer.sy b/test/regress/regress0/sygus/let-ringer.sy
index 0fe8dd05e..c02d2b31f 100644
--- a/test/regress/regress0/sygus/let-ringer.sy
+++ b/test/regress/regress0/sygus/let-ringer.sy
@@ -3,12 +3,14 @@
 ; COMMAND-LINE: --cegqi-si=all --sygus-unif --sygus-out=status
 (set-logic LIA)
 (define-fun g ((x Int)) Int (ite (= x 1) 15 19))
+(define-fun letf ((z Int) (w Int) (s Int) (x Int)) Int (+ z (+ x (+ x (+ s (+ 1 (+ (g w) z)))))))
+
 (synth-fun f ((x Int)) Int
     ((Start Int (x
                  0
                  1
                  (- Start Start)
-                 (let ((z Int Start) (w Int Start)) (+ z (+ x (+ x (+ Start (+ 1 (+ (g w) z)))))))))))
+                 (letf Start Start Start x)))))
                  
 (declare-var x Int)
 (constraint (= (f x) (+ (* 4 x) 15)))
diff --git a/test/regress/regress0/sygus/let-simp.sy b/test/regress/regress0/sygus/let-simp.sy
index 6f9d9fff9..7e191e312 100644
--- a/test/regress/regress0/sygus/let-simp.sy
+++ b/test/regress/regress0/sygus/let-simp.sy
@@ -1,12 +1,13 @@
 ; EXPECT: unsat
 ; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
+(define-fun letf ((z Int)) Int (+ z z))
 (synth-fun f ((x Int) (y Int)) Int
     ((Start Int (x
                  y
                  0
                  (- Start Start)
-                 (let ((z Int Start)) (+ z z))))))
+                 (letf Start)))))
 
 (declare-var x Int)
 (declare-var y Int)
diff --git a/test/regress/regress1/sygus/abv.sy b/test/regress/regress1/sygus/abv.sy
index 6ce1a011a..d9a8a019c 100644
--- a/test/regress/regress1/sygus/abv.sy
+++ b/test/regress/regress1/sygus/abv.sy
@@ -30,6 +30,10 @@
 	(select arrIn x)
 )
 
+(define-fun letf ((m MemSort) (v1 AddrSort) (v2 AddrSort)) ValSort
+  (bvadd 
+    (ReadArr v1 m) 
+    (ReadArr v2 m)))
 
 (synth-fun f 
 	; Args
@@ -45,12 +49,8 @@
 		(WriteArr (Variable AddrSort) (Variable ValSort) mem)))
 
 	(Start ValSort (
-		(let 
-			((m MemSort StartArray)) 
-			(bvadd 
-				(ReadArr (Variable AddrSort) m) 
-				(ReadArr (Variable AddrSort) m))))))
-)
+		(letf StartArray (Variable AddrSort) (Variable AddrSort))))
+))
 
 (declare-var a (BitVec 8))
 (declare-var b (BitVec 8))
diff --git a/test/regress/regress1/sygus/let-bug-simp.sy b/test/regress/regress1/sygus/let-bug-simp.sy
index d570d5a21..5c2dccff0 100644
--- a/test/regress/regress1/sygus/let-bug-simp.sy
+++ b/test/regress/regress1/sygus/let-bug-simp.sy
@@ -1,17 +1,15 @@
 ; EXPECT: unsat
 ; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
-
+(define-fun letf ((z Int) (v1 Int) (v2 Int)) Bool  
+  (or 
+    (= v1 z) 
+    (= v2 z)))
 (synth-fun f ((x0 Int) (x1 Int)) Bool
 (
 	(StartInt Int (5))
 
-	(Start Bool (
-		(let 
-			((z Int StartInt)) 
-			(or 
-				(= (Variable Int) z) 
-				(= (Variable Int) z)))))
+	(Start Bool (  (letf StartInt (Variable Int) (Variable Int)) ))
 )
 )
 
diff --git a/test/regress/regress1/sygus/tester.sy b/test/regress/regress1/sygus/tester.sy
index 261666dd4..bf1cd1576 100644
--- a/test/regress/regress1/sygus/tester.sy
+++ b/test/regress/regress1/sygus/tester.sy
@@ -11,7 +11,7 @@
 	(
 		(Start DT (ntDT))
 		(ntDT DT
-			( x1 x2
+			( x1
 				(JSBool ntBool)
 				(A ntInt)
 				(ite ntBool ntDT ntDT)
diff --git a/test/regress/regress1/sygus/twolets2-orig.sy b/test/regress/regress1/sygus/twolets2-orig.sy
index 50f7ad544..a92c0b014 100644
--- a/test/regress/regress1/sygus/twolets2-orig.sy
+++ b/test/regress/regress1/sygus/twolets2-orig.sy
@@ -1,10 +1,11 @@
 ; EXPECT: unsat
 ; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
+(define-fun letf ((x Int) (y Int) (z Int)) Int (+ (+ y x) z))
 (synth-fun f1 ((x Int)) Int
      (
      (Start Int (
-            (let ((y Int CInt) (z Int CInt)) (+ (+ y x) z))
+            (letf x CInt CInt)
             )
      )
      (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
@@ -14,7 +15,7 @@
 (synth-fun f2 ((x Int)) Int
      (
      (Start Int (x
-            (let ((y Int Start) (z Int CInt)) (+ (+ y x) z))
+            (letf x Start CInt)
             )
      )
      (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))