Ho parsing and regressions (#1350)

5 files changed, 314 insertions, 84 deletions

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index c8b4ac966..0d8cc1fcb 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -448,6 +448,58 @@ std::vector<DatatypeType> Parser::mkMutualDatatypeTypes(
   }
 }
 
+Type Parser::mkFlatFunctionType(std::vector<Type>& sorts,
+                                Type range,
+                                std::vector<Expr>& flattenVars)
+{
+  if (range.isFunction())
+  {
+    std::vector<Type> domainTypes =
+        (static_cast<FunctionType>(range)).getArgTypes();
+    for (unsigned i = 0, size = domainTypes.size(); i < size; i++)
+    {
+      sorts.push_back(domainTypes[i]);
+      // the introduced variable is internal (not parsable)
+      std::stringstream ss;
+      ss << "__flatten_var_" << i;
+      Expr v = d_exprManager->mkBoundVar(ss.str(), domainTypes[i]);
+      flattenVars.push_back(v);
+    }
+    range = static_cast<FunctionType>(range).getRangeType();
+  }
+  if (sorts.empty())
+  {
+    return range;
+  }
+  return d_exprManager->mkFunctionType(sorts, range);
+}
+
+Type Parser::mkFlatFunctionType(std::vector<Type>& sorts, Type range)
+{
+  if (sorts.empty())
+  {
+    // no difference
+    return range;
+  }
+  while (range.isFunction())
+  {
+    std::vector<Type> domainTypes =
+        static_cast<FunctionType>(range).getArgTypes();
+    sorts.insert(sorts.end(), domainTypes.begin(), domainTypes.end());
+    range = static_cast<FunctionType>(range).getRangeType();
+  }
+  return d_exprManager->mkFunctionType(sorts, range);
+}
+
+Expr Parser::mkHoApply(Expr expr, std::vector<Expr>& args, unsigned startIndex)
+{
+  for (unsigned i = startIndex; i < args.size(); i++)
+  {
+    expr = d_exprManager->mkExpr(HO_APPLY, expr, args[i]);
+  }
+  return expr;
+}
+
 bool Parser::isDeclared(const std::string& name, SymbolType type) {
   switch (type) {
     case SYM_VARIABLE:
diff --git a/src/parser/parser.h b/src/parser/parser.h
index e1518f9ca..f2044c7ef 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -573,6 +573,71 @@ public:
   std::vector<DatatypeType>
   mkMutualDatatypeTypes(std::vector<Datatype>& datatypes, bool doOverload=false);
 
+  /** make flat function type
+   *
+   * Returns the "flat" function type corresponding to the function taking
+   * argument types "sorts" and range type "range".  A flat function type is
+   * one whose range is not a function. Notice that if sorts is empty and range
+   * is not a function, then this function returns range itself.
+   *
+   * If range is a function type, we add its function argument sorts to sorts
+   * and consider its function range as the new range. For each sort S added
+   * to sorts in this process, we add a new bound variable of sort S to
+   * flattenVars.
+   *
+   * For example:
+   * mkFlattenFunctionType( { Int, (-> Real Real) }, (-> Int Bool), {} ):
+   * - returns the the function type (-> Int (-> Real Real) Int Bool)
+   * - updates sorts to { Int, (-> Real Real), Int },
+   * - updates flattenVars to { x }, where x is bound variable of type Int.
+   *
+   * Notice that this method performs only one level of flattening, for example,
+   * mkFlattenFunctionType({ Int, (-> Real Real) }, (-> Int (-> Int Bool)), {}):
+   * - returns the the function type (-> Int (-> Real Real) Int (-> Int Bool))
+   * - updates sorts to { Int, (-> Real Real), Int },
+   * - updates flattenVars to { x }, where x is bound variable of type Int.
+   *
+   * This method is required so that we do not return functions
+   * that have function return type (these give an unhandled exception
+   * in the ExprManager). For examples of the equivalence between function
+   * definitions in the proposed higher-order extension of the smt2 language,
+   * see page 3 of http://matryoshka.gforge.inria.fr/pubs/PxTP2017.pdf.
+   *
+   * The argument flattenVars is needed in the case of defined functions
+   * with function return type. These have implicit arguments, for instance:
+   *    (define-fun Q ((x Int)) (-> Int Int) (lambda y (P x)))
+   * is equivalent to the command:
+   *    (define-fun Q ((x Int) (z Int)) Int (@ (lambda y (P x)) z))
+   * where @ is (higher-order) application. In this example, z is added to
+   * flattenVars.
+   */
+  Type mkFlatFunctionType(std::vector<Type>& sorts,
+                          Type range,
+                          std::vector<Expr>& flattenVars);
+
+  /** make flat function type
+   *
+   * Same as above, but does not take argument flattenVars.
+   * This is used when the arguments of the function are not important (for
+   * instance, if we are only using this type in a declare-fun).
+   */
+  Type mkFlatFunctionType(std::vector<Type>& sorts, Type range);
+
+  /** make higher-order apply
+   *
+   * This returns the left-associative curried application of (function) expr to
+   * the arguments in args, starting at index startIndex.
+   *
+   * For example, mkHoApply( f, { a, b }, 0 ) returns
+   *  (HO_APPLY (HO_APPLY f a) b)
+   *
+   * If args is non-empty, the expected type of expr is (-> T0 ... Tn T), where
+   *    args[i-startIndex].getType() = Ti
+   * for each i where startIndex <= i < args.size(). If expr is not of this
+   * type, the expression returned by this method will not be well typed.
+   */
+  Expr mkHoApply(Expr expr, std::vector<Expr>& args, unsigned startIndex = 0);
+
   /**
    * Add an operator to the current legal set.
    *
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 4d39c7635..5351bae15 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -266,6 +266,7 @@ command [std::unique_ptr<CVC4::Command>* cmd]
   std::vector<Expr> terms;
   std::vector<Type> sorts;
   std::vector<std::pair<std::string, Type> > sortedVarNames;
+  std::vector<Expr> flattenVars;
 }
   : /* set the logic */
     SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT]
@@ -344,12 +345,12 @@ command [std::unique_ptr<CVC4::Command>* cmd]
     LPAREN_TOK sortList[sorts] RPAREN_TOK
     sortSymbol[t,CHECK_DECLARED]
     { Debug("parser") << "declare fun: '" << name << "'" << std::endl;
-      if( sorts.size() > 0 ) {
-        if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) {
-          PARSER_STATE->parseErrorLogic("Functions (of non-zero arity) cannot "
-                                        "be declared in logic ");
-        }
-        t = EXPR_MANAGER->mkFunctionType(sorts, t);
+      if( !sorts.empty() ) {
+        t = PARSER_STATE->mkFlatFunctionType(sorts, t);
+      }
+      if(t.isFunction() && !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) {
+        PARSER_STATE->parseErrorLogic("Functions (of non-zero arity) cannot "
+                                      "be declared in logic ");
       }
       // we allow overloading for function declarations
       Expr func = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true);
@@ -364,7 +365,6 @@ command [std::unique_ptr<CVC4::Command>* cmd]
     { /* add variables to parser state before parsing term */
       Debug("parser") << "define fun: '" << name << "'" << std::endl;
       if( sortedVarNames.size() > 0 ) {
-        std::vector<CVC4::Type> sorts;
         sorts.reserve(sortedVarNames.size());
         for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
               sortedVarNames.begin(), iend = sortedVarNames.end();
@@ -372,7 +372,7 @@ command [std::unique_ptr<CVC4::Command>* cmd]
             ++i) {
           sorts.push_back((*i).second);
         }
-        t = EXPR_MANAGER->mkFunctionType(sorts, t);
+        t = PARSER_STATE->mkFlatFunctionType(sorts, t, flattenVars);
       }
       PARSER_STATE->pushScope(true);
       for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
@@ -383,7 +383,14 @@ command [std::unique_ptr<CVC4::Command>* cmd]
       }
     }
     term[expr, expr2]
-    { PARSER_STATE->popScope();
+    {
+      if( !flattenVars.empty() ){
+        // if this function has any implicit variables flattenVars,
+        // we apply the body of the definition to the flatten vars
+        expr = PARSER_STATE->mkHoApply(expr, flattenVars);
+        terms.insert(terms.end(), flattenVars.begin(), flattenVars.end());
+      }
+      PARSER_STATE->popScope();
       // declare the name down here (while parsing term, signature
       // must not be extended with the name itself; no recursion
       // permitted)
@@ -608,6 +615,9 @@ sygusCommand [std::unique_ptr<CVC4::Command>* cmd]
       if( range.isNull() ){
         PARSER_STATE->parseError("Must supply return type for synth-fun.");
       }
+      if( range.isFunction() ){
+        PARSER_STATE->parseError("Cannot use synth-fun with function return type.");
+      }
       seq.reset(new CommandSequence());
       std::vector<Type> var_sorts;
       for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
@@ -1140,13 +1150,17 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
   std::vector<std::pair<std::string, Type> > sortedVarNames;
   SExpr sexpr;
   Type t;
+  Expr func;
   Expr func_app;
   std::vector<Expr> bvs;
   std::vector< std::vector<std::pair<std::string, Type> > > sortedVarNamesList;
+  std::vector<std::vector<Expr>> flattenVarsList;
   std::vector<Expr> funcs;
   std::vector<Expr> func_defs;
   Expr aexpr;
   std::unique_ptr<CVC4::CommandSequence> seq;
+  std::vector<Type> sorts;
+  std::vector<Expr> flattenVars;
 }
     /* meta-info */
   : META_INFO_TOK metaInfoInternal[cmd]
@@ -1191,37 +1205,16 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
     { PARSER_STATE->checkUserSymbol(fname); }
     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
     sortSymbol[t,CHECK_DECLARED]
-    { if( sortedVarNames.size() > 0 ) {
-        std::vector<CVC4::Type> sorts;
-        sorts.reserve(sortedVarNames.size());
-        for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
-            sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend;
-            ++i) {
-          sorts.push_back((*i).second);
-        }
-        t = EXPR_MANAGER->mkFunctionType(sorts, t);
-      }
-      // allow overloading
-      Expr func = PARSER_STATE->mkVar(fname, t, ExprManager::VAR_FLAG_NONE, true);
+    {
+      func = PARSER_STATE->mkDefineFunRec(fname, sortedVarNames, t, flattenVars);
       seq->addCommand(new DeclareFunctionCommand(fname, func, t));
-      if( sortedVarNames.empty() ){
-        func_app = func;
-      }else{
-        std::vector< Expr > f_app;
-        f_app.push_back( func );
-        PARSER_STATE->pushScope(true);
-        for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
-              sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend;
-            ++i) {
-          Expr v = PARSER_STATE->mkBoundVar((*i).first, (*i).second);
-          bvs.push_back( v );
-          f_app.push_back( v );
-        }
-        func_app = MK_EXPR( kind::APPLY_UF, f_app );
-      }
+      PARSER_STATE->pushDefineFunRecScope(sortedVarNames, func, flattenVars, func_app, bvs, true );
     }
     term[expr, expr2]
     { PARSER_STATE->popScope(); 
+      if( !flattenVars.empty() ){
+        expr = PARSER_STATE->mkHoApply( expr, flattenVars );
+      }
       Expr as = MK_EXPR( kind::EQUAL, func_app, expr);
       if( !bvs.empty() ){
         std::string attr_name("fun-def");
@@ -1246,23 +1239,19 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
       { PARSER_STATE->checkUserSymbol(fname); }
       LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
       sortSymbol[t,CHECK_DECLARED]
-      { sortedVarNamesList.push_back( sortedVarNames );
-        if( sortedVarNamesList[0].size() > 0 ) {
-          if( !sortedVarNames.empty() ){
-            std::vector<CVC4::Type> sorts;
-            for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator
-                    i = sortedVarNames.begin(), iend = sortedVarNames.end();
-                i != iend; ++i) {
-              sorts.push_back((*i).second);
-            }
-            t = EXPR_MANAGER->mkFunctionType(sorts, t);
-          }
-        }
-        sortedVarNames.clear();
-        // allow overloading
-        Expr func = PARSER_STATE->mkVar(fname, t, ExprManager::VAR_FLAG_NONE, true);
+      {
+        flattenVars.clear();
+        func = PARSER_STATE->mkDefineFunRec( fname, sortedVarNames, t, flattenVars );
         seq->addCommand(new DeclareFunctionCommand(fname, func, t));
         funcs.push_back( func );
+
+        // add to lists (need to remember for when parsing the bodies)
+        sortedVarNamesList.push_back( sortedVarNames );
+        flattenVarsList.push_back( flattenVars );
+
+        // set up parsing the next variable list block
+        sortedVarNames.clear();
+        flattenVars.clear();
       }
       RPAREN_TOK
     )+
@@ -1274,27 +1263,19 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
         PARSER_STATE->parseError("Must define at least one function in "
                                  "define-funs-rec");
       }
-      PARSER_STATE->pushScope(true);
       bvs.clear();
-      if( sortedVarNamesList[0].empty() ){
-        func_app = funcs[0];
-      }else{
-        std::vector< Expr > f_app;
-        f_app.push_back( funcs[0] );
-        for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator
-              i = sortedVarNamesList[0].begin(),
-              iend = sortedVarNamesList[0].end(); i != iend; ++i) {
-          Expr v = PARSER_STATE->mkBoundVar((*i).first, (*i).second);
-          bvs.push_back( v );
-          f_app.push_back( v );
-        }
-        func_app = MK_EXPR( kind::APPLY_UF, f_app );
-      }
+      PARSER_STATE->pushDefineFunRecScope( sortedVarNamesList[0], funcs[0],
+                                           flattenVarsList[0], func_app, bvs, true);
     }
     (
     term[expr,expr2]
     { 
+      unsigned j = func_defs.size();
+      if( !flattenVarsList[j].empty() ){
+        expr = PARSER_STATE->mkHoApply( expr, flattenVarsList[j] );
+      }
       func_defs.push_back( expr );
+      j++;
       Expr as = MK_EXPR( kind::EQUAL, func_app, expr );
       if( !bvs.empty() ){
         std::string attr_name("fun-def");
@@ -1311,23 +1292,9 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
       //set up the next scope 
       PARSER_STATE->popScope();
       if( func_defs.size()<funcs.size() ){
-        PARSER_STATE->pushScope(true);
         bvs.clear();
-        unsigned j = func_defs.size();
-        if( sortedVarNamesList[j].empty() ){
-          func_app = funcs[j];
-        }else{
-          std::vector< Expr > f_app;
-          f_app.push_back( funcs[j] );
-          for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator
-                  i = sortedVarNamesList[j].begin(),
-                  iend = sortedVarNamesList[j].end(); i != iend; ++i) {
-            Expr v = PARSER_STATE->mkBoundVar((*i).first, (*i).second);
-            bvs.push_back( v );
-            f_app.push_back( v );
-          }
-          func_app = MK_EXPR( kind::APPLY_UF, f_app );
-        }
+        PARSER_STATE->pushDefineFunRecScope( sortedVarNamesList[j], funcs[j], 
+                                             flattenVarsList[j], func_app, bvs, true);
       }
     }
     )+
@@ -1398,7 +1365,10 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
             PARSER_STATE->parseErrorLogic("Functions (of non-zero arity) "
                                           "cannot be declared in logic ");
           }
-          t = EXPR_MANAGER->mkFunctionType(sorts);
+          // must flatten
+          Type range = sorts.back();
+          sorts.pop_back();
+          t = PARSER_STATE->mkFlatFunctionType(sorts, range);
         } else {
           t = sorts[0];
         }
@@ -2008,7 +1978,18 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
       if(isBuiltinOperator) {
         PARSER_STATE->checkOperator(kind, args.size());
       }
-      expr = MK_EXPR(kind, args); 
+      // may be partially applied function, in this case we should use HO_APPLY
+      if( args.size()>=2 && args[0].getType().isFunction() &&
+          (args.size()-1)<((FunctionType)args[0].getType()).getArity() ){
+        Debug("parser") << "Partial application of " << args[0];
+        Debug("parser") << " : #argTypes = " << ((FunctionType)args[0].getType()).getArity();
+        Debug("parser") << ", #args = " << args.size()-1 << std::endl;
+        // must curry the application
+        expr = args[0];
+        expr = PARSER_STATE->mkHoApply( expr, args, 1 );
+      }else{
+        expr = MK_EXPR(kind, args);
+      }
     }
 
   | LPAREN_TOK
@@ -2270,6 +2251,24 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
         expr2 = f2;
       }
     }
+  | /* lambda */
+    LPAREN_TOK HO_LAMBDA_TOK
+    LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
+    {
+      PARSER_STATE->pushScope(true);
+      for(const std::pair<std::string, CVC4::Type>& svn : sortedVarNames){
+        args.push_back(PARSER_STATE->mkBoundVar(svn.first, svn.second));
+      }
+      Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, args);
+      args.clear();
+      args.push_back(bvl);
+    }
+    term[f, f2] RPAREN_TOK
+    {
+      args.push_back( f );
+      PARSER_STATE->popScope();
+      expr = MK_EXPR( CVC4::kind::LAMBDA, args );
+    }
     /* constants */
   | INTEGER_LITERAL
     { expr = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); }
@@ -2877,6 +2876,16 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check]
         }
       }
     ) RPAREN_TOK
+  | LPAREN_TOK HO_ARROW_TOK sortList[args] RPAREN_TOK
+    {
+      if(args.size()<2) {
+        PARSER_STATE->parseError("Arrow types must have at least 2 arguments");
+      }
+      //flatten the type
+      Type rangeType = args.back();
+      args.pop_back();
+      t = PARSER_STATE->mkFlatFunctionType( args, rangeType );
+    }
   ;
 
 /**
@@ -3171,6 +3180,9 @@ FP_RTP_FULL_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'roundTowa
 FP_RTN_FULL_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'roundTowardNegative';
 FP_RTZ_FULL_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'roundTowardZero';
 
+HO_ARROW_TOK : { PARSER_STATE->getLogic().isHigherOrder() }? '->';
+HO_LAMBDA_TOK : { PARSER_STATE->getLogic().isHigherOrder() }? 'lambda';
+
 /**
  * A sequence of printable ASCII characters (except backslash) that starts
  * and ends with | and does not otherwise contain |.
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 7a681f327..c542e5917 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -349,6 +349,61 @@ Expr Smt2::getExpressionForNameAndType(const std::string& name, Type t) {
   }
 }
 
+Expr Smt2::mkDefineFunRec(
+    const std::string& fname,
+    const std::vector<std::pair<std::string, Type> >& sortedVarNames,
+    Type t,
+    std::vector<Expr>& flattenVars)
+{
+  std::vector<Type> sorts;
+  for (const std::pair<std::string, CVC4::Type>& svn : sortedVarNames)
+  {
+    sorts.push_back(svn.second);
+  }
+
+  // make the flattened function type, add bound variables
+  // to flattenVars if the defined function was given a function return type.
+  Type ft = mkFlatFunctionType(sorts, t, flattenVars);
+
+  // allow overloading
+  return mkVar(fname, ft, ExprManager::VAR_FLAG_NONE, true);
+}
+
+void Smt2::pushDefineFunRecScope(
+    const std::vector<std::pair<std::string, Type> >& sortedVarNames,
+    Expr func,
+    const std::vector<Expr>& flattenVars,
+    Expr& func_app,
+    std::vector<Expr>& bvs,
+    bool bindingLevel)
+{
+  pushScope(bindingLevel);
+
+  std::vector<Expr> f_app;
+  f_app.push_back(func);
+  // bound variables are those that are explicitly named in the preamble
+  // of the define-fun(s)-rec command, we define them here
+  for (const std::pair<std::string, CVC4::Type>& svn : sortedVarNames)
+  {
+    Expr v = mkBoundVar(svn.first, svn.second);
+    bvs.push_back(v);
+    f_app.push_back(v);
+  }
+
+  bvs.insert(bvs.end(), flattenVars.begin(), flattenVars.end());
+
+  // make the function application
+  if (bvs.empty())
+  {
+    // it has no arguments
+    func_app = func;
+  }
+  else
+  {
+    func_app = getExprManager()->mkExpr(kind::APPLY_UF, f_app);
+  }
+}
+
 void Smt2::reset() {
   d_logicSet = false;
   d_logic = LogicInfo();
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 84c049ce9..835ff2b58 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -91,6 +91,52 @@ public:
    */
   virtual Expr getExpressionForNameAndType(const std::string& name, Type t);
 
+  /** Make function defined by a define-fun(s)-rec command.
+  *
+  * fname : the name of the function.
+  * sortedVarNames : the list of variable arguments for the function.
+  * t : the range type of the function we are defining.
+  *
+  * This function will create a bind a new function term to name fname.
+  * The type of this function is
+  * Parser::mkFlatFunctionType(sorts,t,flattenVars),
+  * where sorts are the types in the second components of sortedVarNames.
+  * As descibed in Parser::mkFlatFunctionType, new bound variables may be
+  * added to flattenVars in this function if the function is given a function
+  * range type.
+  */
+  Expr mkDefineFunRec(
+      const std::string& fname,
+      const std::vector<std::pair<std::string, Type> >& sortedVarNames,
+      Type t,
+      std::vector<Expr>& flattenVars);
+
+  /** Push scope for define-fun-rec
+   *
+  * This calls Parser::pushScope(bindingLevel) and sets up
+  * initial information for reading a body of a function definition
+  * in the define-fun-rec and define-funs-rec command.
+  * The input parameters func/flattenVars are the result
+  * of a call to mkDefineRec above.
+  *
+  * func : the function whose body we are defining.
+  * sortedVarNames : the list of variable arguments for the function.
+  * flattenVars : the implicit variables introduced when defining func.
+  *
+  * This function:
+  * (1) Calls Parser::pushScope(bindingLevel).
+  * (2) Computes the bound variable list for the quantified formula
+  *     that defined this definition and stores it in bvs.
+  * (3) Sets func_app to the APPLY_UF with func applied to bvs.
+  */
+  void pushDefineFunRecScope(
+      const std::vector<std::pair<std::string, Type> >& sortedVarNames,
+      Expr func,
+      const std::vector<Expr>& flattenVars,
+      Expr& func_app,
+      std::vector<Expr>& bvs,
+      bool bindingLevel = false);
+
   void reset();
 
   void resetAssertions();