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

4 files changed, 312 insertions, 31 deletions

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
@@ -464,6 +464,39 @@ public:
 };/* 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