From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 7 Dec 2017 02:57:44 +0000 (-0600)
Subject: Add command for define-fun-rec and add to API (#1412)
X-Git-Tag: cvc5-1.0.0~5424
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=691abe521ea8a7e87db51e22880cf101d59bf3e7;p=cvc5.git

Add command for define-fun-rec and add to API (#1412)
---

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 5351bae15..1135d6dd4 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1151,10 +1151,10 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
   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<std::vector<Expr>> formals;
   std::vector<Expr> funcs;
   std::vector<Expr> func_defs;
   Expr aexpr;
@@ -1198,41 +1198,24 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
       PARSER_STATE->resetAssertions();
     }
   | DEFINE_FUN_REC_TOK
-    { PARSER_STATE->checkThatLogicIsSet();
-      seq.reset(new CVC4::CommandSequence());
-    }
+    { PARSER_STATE->checkThatLogicIsSet(); }
     symbol[fname,CHECK_NONE,SYM_VARIABLE]
     { PARSER_STATE->checkUserSymbol(fname); }
     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
     sortSymbol[t,CHECK_DECLARED]
     {
       func = PARSER_STATE->mkDefineFunRec(fname, sortedVarNames, t, flattenVars);
-      seq->addCommand(new DeclareFunctionCommand(fname, func, t));
-      PARSER_STATE->pushDefineFunRecScope(sortedVarNames, func, flattenVars, func_app, bvs, true );
+      PARSER_STATE->pushDefineFunRecScope(sortedVarNames, func, flattenVars, 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");
-        aexpr = MK_EXPR(kind::INST_ATTRIBUTE, func_app);
-        aexpr = MK_EXPR(kind::INST_PATTERN_LIST, aexpr);
-        //set the attribute to denote this is a function definition
-        seq->addCommand( new SetUserAttributeCommand( attr_name, func_app ) );
-        //assert it
-        Expr boundVars = EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, bvs);
-        as = EXPR_MANAGER->mkExpr(kind::FORALL, boundVars, as, aexpr);
-      }
-      seq->addCommand( new AssertCommand(as, false) );
-      cmd->reset(seq.release());
+      cmd->reset(new DefineFunctionRecCommand(func,bvs,expr));
     }
   | DEFINE_FUNS_REC_TOK
-    { PARSER_STATE->checkThatLogicIsSet();
-      seq.reset(new CVC4::CommandSequence());
-    }
+    { PARSER_STATE->checkThatLogicIsSet();}
     LPAREN_TOK
     ( LPAREN_TOK
       symbol[fname,CHECK_UNDECLARED,SYM_VARIABLE]
@@ -1242,7 +1225,6 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
       {
         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)
@@ -1265,7 +1247,7 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
       }
       bvs.clear();
       PARSER_STATE->pushDefineFunRecScope( sortedVarNamesList[0], funcs[0],
-                                           flattenVarsList[0], func_app, bvs, true);
+                                           flattenVarsList[0], bvs, true);
     }
     (
     term[expr,expr2]
@@ -1275,26 +1257,14 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
         expr = PARSER_STATE->mkHoApply( expr, flattenVarsList[j] );
       }
       func_defs.push_back( expr );
+      formals.push_back(bvs);
       j++;
-      Expr as = MK_EXPR( kind::EQUAL, func_app, expr );
-      if( !bvs.empty() ){
-        std::string attr_name("fun-def");
-        aexpr = MK_EXPR(kind::INST_ATTRIBUTE, func_app);
-        aexpr = MK_EXPR(kind::INST_PATTERN_LIST, aexpr );
-        //set the attribute to denote these are function definitions
-        seq->addCommand( new SetUserAttributeCommand( attr_name, func_app ) );
-        //assert it
-        as = EXPR_MANAGER->mkExpr( kind::FORALL,
-                      EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, bvs),
-                      as, aexpr);
-      }
-      seq->addCommand( new AssertCommand(as, false) );
       //set up the next scope 
       PARSER_STATE->popScope();
       if( func_defs.size()<funcs.size() ){
         bvs.clear();
         PARSER_STATE->pushDefineFunRecScope( sortedVarNamesList[j], funcs[j], 
-                                             flattenVarsList[j], func_app, bvs, true);
+                                             flattenVarsList[j], bvs, true);
       }
     }
     )+
@@ -1304,7 +1274,7 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
             "Number of functions defined does not match number listed in "
             "define-funs-rec"));
       }
-      cmd->reset(seq.release());
+      cmd->reset( new DefineFunctionRecCommand(funcs,formals,func_defs));
     }
   // CHECK_SAT_ASSUMING still being discussed
   // GET_UNSAT_ASSUMPTIONS
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 032fdc673..381a60fa8 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -373,7 +373,6 @@ 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)
 {
@@ -391,17 +390,6 @@ void Smt2::pushDefineFunRecScope(
   }
 
   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() {
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 835ff2b58..4832fc6b5 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -127,13 +127,11 @@ public:
   * (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);
 
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 19adba6da..c13c519ae 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1113,38 +1113,39 @@ void Smt2Printer::toStream(std::ostream& out,
   expr::ExprPrintTypes::Scope ptScope(out, types);
   expr::ExprDag::Scope dagScope(out, dag);
 
-  if(tryToStream<AssertCommand>(out, c) ||
-     tryToStream<PushCommand>(out, c) ||
-     tryToStream<PopCommand>(out, c) ||
-     tryToStream<CheckSatCommand>(out, c) ||
-     tryToStream<QueryCommand>(out, c) ||
-     tryToStream<ResetCommand>(out, c) ||
-     tryToStream<ResetAssertionsCommand>(out, c) ||
-     tryToStream<QuitCommand>(out, c) ||
-     tryToStream<DeclarationSequence>(out, c) ||
-     tryToStream<CommandSequence>(out, c) ||
-     tryToStream<DeclareFunctionCommand>(out, c) ||
-     tryToStream<DeclareTypeCommand>(out, c) ||
-     tryToStream<DefineTypeCommand>(out, c) ||
-     tryToStream<DefineNamedFunctionCommand>(out, c) ||
-     tryToStream<DefineFunctionCommand>(out, c) ||
-     tryToStream<SimplifyCommand>(out, c) ||
-     tryToStream<GetValueCommand>(out, c) ||
-     tryToStream<GetModelCommand>(out, c) ||
-     tryToStream<GetAssignmentCommand>(out, c) ||
-     tryToStream<GetAssertionsCommand>(out, c) ||
-     tryToStream<GetProofCommand>(out, c) ||
-     tryToStream<GetUnsatCoreCommand>(out, c) ||
-     tryToStream<SetBenchmarkStatusCommand>(out, c, d_variant) ||
-     tryToStream<SetBenchmarkLogicCommand>(out, c, d_variant) ||
-     tryToStream<SetInfoCommand>(out, c, d_variant) ||
-     tryToStream<GetInfoCommand>(out, c) ||
-     tryToStream<SetOptionCommand>(out, c) ||
-     tryToStream<GetOptionCommand>(out, c) ||
-     tryToStream<DatatypeDeclarationCommand>(out, c, d_variant) ||
-     tryToStream<CommentCommand>(out, c, d_variant) ||
-     tryToStream<EmptyCommand>(out, c) ||
-     tryToStream<EchoCommand>(out, c, d_variant)) {
+  if (tryToStream<AssertCommand>(out, c) || tryToStream<PushCommand>(out, c)
+      || tryToStream<PopCommand>(out, c)
+      || tryToStream<CheckSatCommand>(out, c)
+      || tryToStream<QueryCommand>(out, c)
+      || tryToStream<ResetCommand>(out, c)
+      || tryToStream<ResetAssertionsCommand>(out, c)
+      || tryToStream<QuitCommand>(out, c)
+      || tryToStream<DeclarationSequence>(out, c)
+      || tryToStream<CommandSequence>(out, c)
+      || tryToStream<DeclareFunctionCommand>(out, c)
+      || tryToStream<DeclareTypeCommand>(out, c)
+      || tryToStream<DefineTypeCommand>(out, c)
+      || tryToStream<DefineNamedFunctionCommand>(out, c)
+      || tryToStream<DefineFunctionCommand>(out, c)
+      || tryToStream<DefineFunctionRecCommand>(out, c)
+      || tryToStream<SimplifyCommand>(out, c)
+      || tryToStream<GetValueCommand>(out, c)
+      || tryToStream<GetModelCommand>(out, c)
+      || tryToStream<GetAssignmentCommand>(out, c)
+      || tryToStream<GetAssertionsCommand>(out, c)
+      || tryToStream<GetProofCommand>(out, c)
+      || tryToStream<GetUnsatCoreCommand>(out, c)
+      || tryToStream<SetBenchmarkStatusCommand>(out, c, d_variant)
+      || tryToStream<SetBenchmarkLogicCommand>(out, c, d_variant)
+      || tryToStream<SetInfoCommand>(out, c, d_variant)
+      || tryToStream<GetInfoCommand>(out, c)
+      || tryToStream<SetOptionCommand>(out, c)
+      || tryToStream<GetOptionCommand>(out, c)
+      || tryToStream<DatatypeDeclarationCommand>(out, c, d_variant)
+      || tryToStream<CommentCommand>(out, c, d_variant)
+      || tryToStream<EmptyCommand>(out, c)
+      || tryToStream<EchoCommand>(out, c, d_variant))
+  {
     return;
   }
 
@@ -1501,6 +1502,74 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c)
   out << ") " << type << " " << formula << ")";
 }
 
+static void toStream(std::ostream& out, const DefineFunctionRecCommand* c)
+{
+  const vector<Expr>& funcs = c->getFunctions();
+  const vector<vector<Expr> >& formals = c->getFormals();
+  out << "(define-fun";
+  if (funcs.size() > 1)
+  {
+    out << "s";
+  }
+  out << "-rec ";
+  if (funcs.size() > 1)
+  {
+    out << "(";
+  }
+  for (unsigned i = 0, size = funcs.size(); i < size; i++)
+  {
+    if (funcs.size() > 1)
+    {
+      if (i > 0)
+      {
+        out << " ";
+      }
+      out << "(";
+    }
+    out << funcs[i] << " (";
+    // print its type signature
+    vector<Expr>::const_iterator itf = formals[i].begin();
+    for (;;)
+    {
+      out << "(" << (*itf) << " " << (*itf).getType() << ")";
+      ++itf;
+      if (itf != formals[i].end())
+      {
+        out << " ";
+      }
+      else
+      {
+        break;
+      }
+    }
+    Type type = funcs[i].getType();
+    type = static_cast<FunctionType>(type).getRangeType();
+    out << ") " << type;
+    if (funcs.size() > 1)
+    {
+      out << ")";
+    }
+  }
+  if (funcs.size() > 1)
+  {
+    out << ") (";
+  }
+  const vector<Expr>& formulas = c->getFormulas();
+  for (unsigned i = 0, size = formulas.size(); i < size; i++)
+  {
+    if (i > 0)
+    {
+      out << " ";
+    }
+    out << formulas[i];
+  }
+  if (funcs.size() > 1)
+  {
+    out << ")";
+  }
+  out << ")";
+}
+
 static void toStreamRational(std::ostream& out, const Rational& r, bool decimal)
 {
   bool neg = r.sgn() < 0;
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index aea6365b7..ad7fd9af0 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -890,6 +890,94 @@ Command* DefineNamedFunctionCommand::clone() const {
   return new DefineNamedFunctionCommand(d_symbol, d_func, d_formals, d_formula);
 }
 
+/* class DefineFunctionRecCommand */
+
+DefineFunctionRecCommand::DefineFunctionRecCommand(
+    Expr func, const std::vector<Expr>& formals, Expr formula) throw()
+{
+  d_funcs.push_back(func);
+  d_formals.push_back(formals);
+  d_formulas.push_back(formula);
+}
+
+DefineFunctionRecCommand::DefineFunctionRecCommand(
+    const std::vector<Expr>& funcs,
+    const std::vector<std::vector<Expr> >& formals,
+    const std::vector<Expr>& formulas) throw()
+{
+  d_funcs.insert(d_funcs.end(), funcs.begin(), funcs.end());
+  d_formals.insert(d_formals.end(), formals.begin(), formals.end());
+  d_formulas.insert(d_formulas.end(), formulas.begin(), formulas.end());
+}
+
+const std::vector<Expr>& DefineFunctionRecCommand::getFunctions() const throw()
+{
+  return d_funcs;
+}
+
+const std::vector<std::vector<Expr> >& DefineFunctionRecCommand::getFormals()
+    const throw()
+{
+  return d_formals;
+}
+
+const std::vector<Expr>& DefineFunctionRecCommand::getFormulas() const throw()
+{
+  return d_formulas;
+}
+
+void DefineFunctionRecCommand::invoke(SmtEngine* smtEngine)
+{
+  try
+  {
+    smtEngine->defineFunctionsRec(d_funcs, d_formals, d_formulas);
+    d_commandStatus = CommandSuccess::instance();
+  }
+  catch (exception& e)
+  {
+    d_commandStatus = new CommandFailure(e.what());
+  }
+}
+
+Command* DefineFunctionRecCommand::exportTo(
+    ExprManager* exprManager, ExprManagerMapCollection& variableMap)
+{
+  std::vector<Expr> funcs;
+  for (unsigned i = 0, size = d_funcs.size(); i < size; i++)
+  {
+    Expr func = d_funcs[i].exportTo(
+        exprManager, variableMap, /* flags = */ ExprManager::VAR_FLAG_DEFINED);
+    funcs.push_back(func);
+  }
+  std::vector<std::vector<Expr> > formals;
+  for (unsigned i = 0, size = d_formals.size(); i < size; i++)
+  {
+    std::vector<Expr> formals_c;
+    transform(d_formals[i].begin(),
+              d_formals[i].end(),
+              back_inserter(formals_c),
+              ExportTransformer(exprManager, variableMap));
+    formals.push_back(formals_c);
+  }
+  std::vector<Expr> formulas;
+  for (unsigned i = 0, size = d_formulas.size(); i < size; i++)
+  {
+    Expr formula = d_formulas[i].exportTo(exprManager, variableMap);
+    formulas.push_back(formula);
+  }
+  return new DefineFunctionRecCommand(funcs, formals, formulas);
+}
+
+Command* DefineFunctionRecCommand::clone() const
+{
+  return new DefineFunctionRecCommand(d_funcs, d_formals, d_formulas);
+}
+
+std::string DefineFunctionRecCommand::getCommandName() const throw()
+{
+  return "define-fun-rec";
+}
+
 /* class SetUserAttribute */
 
 SetUserAttributeCommand::SetUserAttributeCommand(
diff --git a/src/smt/command.h b/src/smt/command.h
index 33f58aa99..ba7baa738 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -463,6 +463,39 @@ public:
   Command* clone() const;
 };/* class DefineNamedFunctionCommand */
 
+/**
+ * The command when parsing define-fun-rec or define-funs-rec.
+ * This command will assert a set of quantified formulas that specify
+ * the (mutually recursive) function definitions provided to it.
+ */
+class CVC4_PUBLIC DefineFunctionRecCommand : public Command
+{
+ public:
+  DefineFunctionRecCommand(Expr func,
+                           const std::vector<Expr>& formals,
+                           Expr formula) throw();
+  DefineFunctionRecCommand(const std::vector<Expr>& funcs,
+                           const std::vector<std::vector<Expr> >& formals,
+                           const std::vector<Expr>& formula) throw();
+  ~DefineFunctionRecCommand() throw() {}
+  const std::vector<Expr>& getFunctions() const throw();
+  const std::vector<std::vector<Expr> >& getFormals() const throw();
+  const std::vector<Expr>& getFormulas() const throw();
+  void invoke(SmtEngine* smtEngine) override;
+  Command* exportTo(ExprManager* exprManager,
+                    ExprManagerMapCollection& variableMap) override;
+  Command* clone() const override;
+  std::string getCommandName() const throw() override;
+
+ protected:
+  /** functions we are defining */
+  std::vector<Expr> d_funcs;
+  /** formal arguments for each of the functions we are defining */
+  std::vector<std::vector<Expr> > d_formals;
+  /** formulas corresponding to the bodies of the functions we are defining */
+  std::vector<Expr> d_formulas;
+}; /* class DefineFunctionRecCommand */
+
 /**
  * The command when an attribute is set by a user.  In SMT-LIBv2 this is done
  *  via the syntax (! expr :attr)
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3cbb3252e..12f822503 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2263,12 +2263,8 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const {
   }
 }
 
-void SmtEngine::defineFunction(Expr func,
-                               const std::vector<Expr>& formals,
-                               Expr formula) {
-  SmtScope smts(this);
-  doPendingPops();
-  Trace("smt") << "SMT defineFunction(" << func << ")" << endl;
+void SmtEngine::debugCheckFormals(const std::vector<Expr>& formals, Expr func)
+{
   for(std::vector<Expr>::const_iterator i = formals.begin(); i != formals.end(); ++i) {
     if((*i).getKind() != kind::BOUND_VARIABLE) {
       stringstream ss;
@@ -2279,25 +2275,13 @@ void SmtEngine::defineFunction(Expr func,
       throw TypeCheckingException(func, ss.str());
     }
   }
+}
 
-  stringstream ss;
-  ss << language::SetLanguage(language::SetLanguage::getLanguage(Dump.getStream()))
-     << func;
-  DefineFunctionCommand c(ss.str(), func, formals, formula);
-  addToModelCommandAndDump(c, ExprManager::VAR_FLAG_DEFINED, true, "declarations");
-
-
-  PROOF( if (options::checkUnsatCores()) {
-      d_defineCommands.push_back(c.clone());
-    });
-
-
-  // Substitute out any abstract values in formula
-  Expr form = d_private->substituteAbstractValues(Node::fromExpr(formula)).toExpr();
-
-  // type check body
-  Type formulaType = form.getType(options::typeChecking());
-
+void SmtEngine::debugCheckFunctionBody(Expr formula,
+                                       const std::vector<Expr>& formals,
+                                       Expr func)
+{
+  Type formulaType = formula.getType(options::typeChecking());
   Type funcType = func.getType();
   // We distinguish here between definitions of constants and functions,
   // because the type checking for them is subtly different.  Perhaps we
@@ -2326,6 +2310,36 @@ void SmtEngine::defineFunction(Expr func,
       throw TypeCheckingException(func, ss.str());
     }
   }
+}
+
+void SmtEngine::defineFunction(Expr func,
+                               const std::vector<Expr>& formals,
+                               Expr formula)
+{
+  SmtScope smts(this);
+  doPendingPops();
+  Trace("smt") << "SMT defineFunction(" << func << ")" << endl;
+  debugCheckFormals(formals, func);
+
+  stringstream ss;
+  ss << language::SetLanguage(
+            language::SetLanguage::getLanguage(Dump.getStream()))
+     << func;
+  DefineFunctionCommand c(ss.str(), func, formals, formula);
+  addToModelCommandAndDump(
+      c, ExprManager::VAR_FLAG_DEFINED, true, "declarations");
+
+  PROOF(if (options::checkUnsatCores()) {
+    d_defineCommands.push_back(c.clone());
+  });
+
+  // type check body
+  debugCheckFunctionBody(formula, formals, func);
+
+  // Substitute out any abstract values in formula
+  Expr form =
+      d_private->substituteAbstractValues(Node::fromExpr(formula)).toExpr();
+
   TNode funcNode = func.getTNode();
   vector<Node> formalsNodes;
   for(vector<Expr>::const_iterator i = formals.begin(),
@@ -2343,6 +2357,97 @@ void SmtEngine::defineFunction(Expr func,
   d_definedFunctions->insert(funcNode, def);
 }
 
+void SmtEngine::defineFunctionsRec(
+    const std::vector<Expr>& funcs,
+    const std::vector<std::vector<Expr> >& formals,
+    const std::vector<Expr>& formulas)
+{
+  SmtScope smts(this);
+  finalOptionsAreSet();
+  doPendingPops();
+  Trace("smt") << "SMT defineFunctionsRec(...)" << endl;
+
+  if (funcs.size() != formals.size() && funcs.size() != formulas.size())
+  {
+    stringstream ss;
+    ss << "Number of functions, formals, and function bodies passed to "
+          "defineFunctionsRec do not match:"
+       << "\n"
+       << "        #functions : " << funcs.size() << "\n"
+       << "        #arg lists : " << formals.size() << "\n"
+       << "  #function bodies : " << formulas.size() << "\n";
+    throw ModalException(ss.str());
+  }
+  for (unsigned i = 0, size = funcs.size(); i < size; i++)
+  {
+    // check formal argument list
+    debugCheckFormals(formals[i], funcs[i]);
+    // type check body
+    debugCheckFunctionBody(formulas[i], formals[i], funcs[i]);
+  }
+
+  if (Dump.isOn("raw-benchmark"))
+  {
+    Dump("raw-benchmark") << DefineFunctionRecCommand(funcs, formals, formulas);
+  }
+
+  ExprManager* em = getExprManager();
+  for (unsigned i = 0, size = funcs.size(); i < size; i++)
+  {
+    // we assert a quantified formula
+    Expr func_app;
+    // make the function application
+    if (formals[i].empty())
+    {
+      // it has no arguments
+      func_app = funcs[i];
+    }
+    else
+    {
+      std::vector<Expr> children;
+      children.push_back(funcs[i]);
+      children.insert(children.end(), formals[i].begin(), formals[i].end());
+      func_app = em->mkExpr(kind::APPLY_UF, children);
+    }
+    Expr lem = em->mkExpr(kind::EQUAL, func_app, formulas[i]);
+    if (!formals[i].empty())
+    {
+      // set the attribute to denote this is a function definition
+      std::string attr_name("fun-def");
+      Expr aexpr = em->mkExpr(kind::INST_ATTRIBUTE, func_app);
+      aexpr = em->mkExpr(kind::INST_PATTERN_LIST, aexpr);
+      std::vector<Expr> expr_values;
+      std::string str_value;
+      setUserAttribute(attr_name, func_app, expr_values, str_value);
+      // make the quantified formula
+      Expr boundVars = em->mkExpr(kind::BOUND_VAR_LIST, formals[i]);
+      lem = em->mkExpr(kind::FORALL, boundVars, lem, aexpr);
+    }
+    // assert the quantified formula
+    //   notice we don't call assertFormula directly, since this would
+    //   duplicate the output on raw-benchmark.
+    Expr e = d_private->substituteAbstractValues(Node::fromExpr(lem)).toExpr();
+    if (d_assertionList != NULL)
+    {
+      d_assertionList->push_back(e);
+    }
+    d_private->addFormula(e.getNode(), false);
+  }
+}
+
+void SmtEngine::defineFunctionRec(Expr func,
+                                  const std::vector<Expr>& formals,
+                                  Expr formula)
+{
+  std::vector<Expr> funcs;
+  funcs.push_back(func);
+  std::vector<std::vector<Expr> > formals_multi;
+  formals_multi.push_back(formals);
+  std::vector<Expr> formulas;
+  formulas.push_back(formula);
+  defineFunctionsRec(funcs, formals_multi, formulas);
+}
+
 bool SmtEngine::isDefinedFunction( Expr func ){
   Node nf = Node::fromExpr( func );
   Debug("smt") << "isDefined function " << nf << "?" << std::endl;
@@ -5684,7 +5789,11 @@ void SmtEngine::safeFlushStatistics(int fd) const {
   d_statisticsRegistry->safeFlushInformation(fd);
 }
 
-void SmtEngine::setUserAttribute(const std::string& attr, Expr expr, std::vector<Expr> expr_values, std::string str_value) {
+void SmtEngine::setUserAttribute(const std::string& attr,
+                                 Expr expr,
+                                 const std::vector<Expr>& expr_values,
+                                 const std::string& str_value)
+{
   SmtScope smts(this);
   std::vector<Node> node_values;
   for( unsigned i=0; i<expr_values.size(); i++ ){
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 18fc39857..404c9ebe1 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -380,7 +380,24 @@ class CVC4_PUBLIC SmtEngine {
 
   //check satisfiability (for query and check-sat)
   Result checkSatisfiability(const Expr& e, bool inUnsatCore, bool isQuery);
-public:
+
+  /**
+   * Check that all Expr in formals are of BOUND_VARIABLE kind, where func is
+   * the function that the formal argument list is for. This method is used
+   * as a helper function when defining (recursive) functions.
+   */
+  void debugCheckFormals(const std::vector<Expr>& formals, Expr func);
+
+  /**
+   * Checks whether formula is a valid function body for func whose formal
+   * argument list is stored in formals. This method is
+   * used as a helper function when defining (recursive) functions.
+   */
+  void debugCheckFunctionBody(Expr formula,
+                              const std::vector<Expr>& formals,
+                              Expr func);
+
+ public:
 
   /**
    * Construct an SmtEngine with the given expression manager.
@@ -436,10 +453,15 @@ public:
     throw(OptionException);
 
   /**
-   * Add a formula to the current context: preprocess, do per-theory
-   * setup, use processAssertionList(), asserting to T-solver for
-   * literals and conjunction of literals.  Returns false if
-   * immediately determined to be inconsistent.
+   * Define function func in the current context to be:
+   *   (lambda (formals) formula)
+   * This adds func to the list of defined functions, which indicates that
+   * all occurrences of func should be expanded during expandDefinitions.
+   * This method expects input such that:
+   * - func : a variable of function type that expects the arguments in
+   *          formals,
+   * - formals : a list of BOUND_VARIABLE expressions,
+   * - formula does not contain func.
    */
   void defineFunction(Expr func,
                       const std::vector<Expr>& formals,
@@ -448,6 +470,32 @@ public:
   /** is defined function */
   bool isDefinedFunction(Expr func);
 
+  /** Define functions recursive
+   *
+   * For each i, this constrains funcs[i] in the current context to be:
+   *   (lambda (formals[i]) formulas[i])
+   * where formulas[i] may contain variables from funcs. Unlike defineFunction
+   * above, we do not add funcs[i] to the set of defined functions. Instead,
+   * we consider funcs[i] to be a free uninterpreted function, and add:
+   *   forall formals[i]. f(formals[i]) = formulas[i]
+   * to the set of assertions in the current context.
+   * This method expects input such that for each i:
+   * - func[i] : a variable of function type that expects the arguments in
+   *             formals[i], and
+   * - formals[i] : a list of BOUND_VARIABLE expressions.
+   */
+  void defineFunctionsRec(const std::vector<Expr>& funcs,
+                          const std::vector<std::vector<Expr> >& formals,
+                          const std::vector<Expr>& formulas);
+
+  /** Define function recursive
+   *
+   * Same as above, but for a single function.
+   */
+  void defineFunctionRec(Expr func,
+                         const std::vector<Expr>& formals,
+                         Expr formula);
+
   /**
    * Add a formula to the current context: preprocess, do per-theory
    * setup, use processAssertionList(), asserting to T-solver for
@@ -769,7 +817,10 @@ public:
    * This function is called when an attribute is set by a user.
    * In SMT-LIBv2 this is done via the syntax (! expr :attr)
    */
-  void setUserAttribute(const std::string& attr, Expr expr, std::vector<Expr> expr_values, std::string str_value);
+  void setUserAttribute(const std::string& attr,
+                        Expr expr,
+                        const std::vector<Expr>& expr_values,
+                        const std::string& str_value);
 
   /**
    * Set print function in model
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index d01bd537e..944185b31 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -2193,8 +2193,11 @@ void TheoryEngine::ppUnconstrainedSimp(vector<Node>& assertions)
   d_unconstrainedSimp->processAssertions(assertions);
 }
 
-
-void TheoryEngine::setUserAttribute(const std::string& attr, Node n, std::vector<Node>& node_values, std::string str_value) {
+void TheoryEngine::setUserAttribute(const std::string& attr,
+                                    Node n,
+                                    const std::vector<Node>& node_values,
+                                    const std::string& str_value)
+{
   Trace("te-attr") << "set user attribute " << attr << " " << n << endl;
   if( d_attr_handle.find( attr )!=d_attr_handle.end() ){
     for( size_t i=0; i<d_attr_handle[attr].size(); i++ ){
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 91a88274e..179530240 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -855,17 +855,20 @@ private:
   std::set< std::string > d_theoryAlternatives;
 
   std::map< std::string, std::vector< theory::Theory* > > d_attr_handle;
-public:
 
-  /**
-   * Set user attribute.
-   * This function is called when an attribute is set by a user.  In SMT-LIBv2 this is done
-   * via the syntax (! n :attr)
+ public:
+  /** Set user attribute.
+   * 
+   * This function is called when an attribute is set by a user.  In SMT-LIBv2
+   * this is done via the syntax (! n :attr)
    */
-  void setUserAttribute(const std::string& attr, Node n, std::vector<Node>& node_values, std::string str_value);
+  void setUserAttribute(const std::string& attr,
+                        Node n,
+                        const std::vector<Node>& node_values,
+                        const std::string& str_value);
 
-  /**
-   * Handle user attribute.
+  /** Handle user attribute.
+   * 
    * Associates theory t with the attribute attr.  Theory t will be
    * notified whenever an attribute of name attr is set.
    */
@@ -877,7 +880,7 @@ public:
    */
   void checkTheoryAssertionsWithModel(bool hardFailure);
 
-private:
+ private:
   IntStat d_arithSubstitutionsAdded;
 
 };/* class TheoryEngine */