Support for SyGuS PBE + recursive functions (#3433)

7 files changed, 337 insertions, 32 deletions

diff --git a/src/theory/quantifiers/fun_def_evaluator.cpp b/src/theory/quantifiers/fun_def_evaluator.cpp
new file mode 100644
index 000000000..83debe0d9
--- /dev/null
+++ b/src/theory/quantifiers/fun_def_evaluator.cpp
@@ -0,0 +1,187 @@
+/*********************                                                        */
+/*! \file fun_def_evaluator.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of techniques for evaluating terms with recursively
+ ** defined functions.
+ **/
+
+#include "theory/quantifiers/fun_def_evaluator.h"
+
+#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/rewriter.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+FunDefEvaluator::FunDefEvaluator() {}
+
+void FunDefEvaluator::assertDefinition(Node q)
+{
+  Trace("fd-eval") << "FunDefEvaluator: assertDefinition " << q << std::endl;
+  Node h = QuantAttributes::getFunDefHead(q);
+  if (h.isNull())
+  {
+    // not a function definition
+    return;
+  }
+  // h possibly with zero arguments?
+  Node f = h.hasOperator() ? h.getOperator() : h;
+  Assert(d_funDefMap.find(f) == d_funDefMap.end())
+      << "FunDefEvaluator::assertDefinition: function already defined";
+  FunDefInfo& fdi = d_funDefMap[f];
+  fdi.d_body = QuantAttributes::getFunDefBody(q);
+  Assert(!fdi.d_body.isNull());
+  fdi.d_args.insert(fdi.d_args.end(), q[0].begin(), q[0].end());
+  Trace("fd-eval") << "FunDefEvaluator: function " << f << " is defined with "
+                   << fdi.d_args << " / " << fdi.d_body << std::endl;
+}
+
+Node FunDefEvaluator::evaluate(Node n) const
+{
+  // should do standard rewrite before this call
+  Assert(Rewriter::rewrite(n) == n);
+  Trace("fd-eval") << "FunDefEvaluator: evaluate " << n << std::endl;
+  NodeManager* nm = NodeManager::currentNM();
+  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
+  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+  std::map<Node, FunDefInfo>::const_iterator itf;
+  std::vector<TNode> visit;
+  TNode cur;
+  TNode curEval;
+  Node f;
+  visit.push_back(n);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    it = visited.find(cur);
+    Trace("fd-eval-debug") << "evaluate subterm " << cur << std::endl;
+
+    if (it == visited.end())
+    {
+      if (cur.isConst())
+      {
+        Trace("fd-eval-debug") << "constant " << cur << std::endl;
+        visited[cur] = cur;
+      }
+      else
+      {
+        Trace("fd-eval-debug") << "recurse " << cur << std::endl;
+        visited[cur] = Node::null();
+        visit.push_back(cur);
+        for (const Node& cn : cur)
+        {
+          visit.push_back(cn);
+        }
+      }
+    }
+    else
+    {
+      curEval = it->second;
+      if (curEval.isNull())
+      {
+        Trace("fd-eval-debug") << "from arguments " << cur << std::endl;
+        Node ret = cur;
+        bool childChanged = false;
+        std::vector<Node> children;
+        Kind ck = cur.getKind();
+        // If a parameterized node that is not APPLY_UF (which is handled below,
+        // we add it to the children vector.
+        if (ck != APPLY_UF && cur.getMetaKind() == metakind::PARAMETERIZED)
+        {
+          children.push_back(cur.getOperator());
+        }
+        for (const Node& cn : cur)
+        {
+          it = visited.find(cn);
+          Assert(it != visited.end());
+          Assert(!it->second.isNull());
+          childChanged = childChanged || cn != it->second;
+          children.push_back(it->second);
+        }
+        if (cur.getKind() == APPLY_UF)
+        {
+          // need to evaluate it
+          f = cur.getOperator();
+          itf = d_funDefMap.find(f);
+          if (itf == d_funDefMap.end())
+          {
+            Trace("fd-eval") << "FunDefEvaluator: no definition for " << f
+                             << ", FAIL" << std::endl;
+            return Node::null();
+          }
+          // get the function definition
+          Node sbody = itf->second.d_body;
+          const std::vector<Node>& args = itf->second.d_args;
+          if (!args.empty())
+          {
+            // invoke it on arguments
+            sbody = sbody.substitute(
+                args.begin(), args.end(), children.begin(), children.end());
+            // rewrite it
+            sbody = Rewriter::rewrite(sbody);
+          }
+          // our result is the result of the body
+          visited[cur] = sbody;
+          // If its not constant, we push back self and the substituted body.
+          // Thus, we evaluate the body first; our result will be the result of
+          // evaluating the body.
+          if (!sbody.isConst())
+          {
+            visit.push_back(cur);
+            visit.push_back(sbody);
+          }
+        }
+        else
+        {
+          if (childChanged)
+          {
+            ret = nm->mkNode(cur.getKind(), children);
+            ret = Rewriter::rewrite(ret);
+          }
+          if (!ret.isConst())
+          {
+            Trace("fd-eval") << "FunDefEvaluator: non-constant subterm " << ret
+                             << ", FAIL" << std::endl;
+            // failed, possibly due to free variable
+            return Node::null();
+          }
+          visited[cur] = ret;
+        }
+      }
+      else if (!curEval.isConst())
+      {
+        Trace("fd-eval-debug") << "from body " << cur << std::endl;
+        // we had to evaluate our body, which should have a definition now
+        it = visited.find(curEval);
+        Assert(it != visited.end());
+        // our definition is the result of the body
+        visited[cur] = it->second;
+        Assert(it->second.isConst());
+      }
+    }
+  } while (!visit.empty());
+  Assert(visited.find(n) != visited.end());
+  Assert(!visited.find(n)->second.isNull());
+  Assert(visited.find(n)->second.isConst());
+  Trace("fd-eval") << "FunDefEvaluator: return SUCCESS " << visited[n]
+                   << std::endl;
+  return visited[n];
+}
+
+bool FunDefEvaluator::hasDefinitions() const { return !d_funDefMap.empty(); }
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/fun_def_evaluator.h b/src/theory/quantifiers/fun_def_evaluator.h
new file mode 100644
index 000000000..ad08dfa84
--- /dev/null
+++ b/src/theory/quantifiers/fun_def_evaluator.h
@@ -0,0 +1,72 @@
+/*********************                                                        */
+/*! \file fun_def_evaluator.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Techniques for evaluating terms with recursively defined functions.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__QUANTIFIERS_FUN_DEF_EVALUATOR_H
+#define CVC4__QUANTIFIERS_FUN_DEF_EVALUATOR_H
+
+#include <map>
+#include <vector>
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/**
+ * Techniques for evaluating recursively defined functions.
+ */
+class FunDefEvaluator
+{
+ public:
+  FunDefEvaluator();
+  ~FunDefEvaluator() {}
+  /**
+   * Assert definition of a (recursive) function definition given by quantified
+   * formula q.
+   */
+  void assertDefinition(Node q);
+  /**
+   * Simplify node based on the (recursive) function definitions known by this
+   * class. If n cannot be simplified to a constant, then this method returns
+   * null.
+   */
+  Node evaluate(Node n) const;
+  /**
+   * Has a call to assertDefinition been made? If this returns false, then
+   * the evaluate method is the same as calling the rewriter, and returning
+   * false if the result is non-constant.
+   */
+  bool hasDefinitions() const;
+
+ private:
+  /** information cached per function definition */
+  class FunDefInfo
+  {
+   public:
+    /** the body */
+    Node d_body;
+    /** the formal argument list */
+    std::vector<Node> d_args;
+  };
+  /** maps functions to the above information */
+  std::map<Node, FunDefInfo> d_funDefMap;
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 5edd18464..6e69715ef 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -539,7 +539,8 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
     return false;
   }
 
-  lem = Rewriter::rewrite(lem);
+  // simplify the lemma based on the term database sygus utility
+  lem = d_tds->rewriteNode(lem);
   // eagerly unfold applications of evaluation function
   Trace("cegqi-debug") << "pre-unfold counterexample : " << lem << std::endl;
   // record the instantiation
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index 88d00ce3a..9f6954416 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -33,7 +33,7 @@ namespace theory {
 namespace quantifiers {
 
 SynthEngine::SynthEngine(QuantifiersEngine* qe, context::Context* c)
-    : QuantifiersModule(qe)
+    : QuantifiersModule(qe), d_tds(qe->getTermDatabaseSygus())
 {
   d_conjs.push_back(std::unique_ptr<SynthConjecture>(
       new SynthConjecture(d_quantEngine, this)));
@@ -274,6 +274,8 @@ void SynthEngine::assignConjecture(Node q)
 
 void SynthEngine::registerQuantifier(Node q)
 {
+  Trace("cegqi-debug") << "SynthEngine: Register quantifier : " << q
+                       << std::endl;
   if (d_quantEngine->getOwner(q) == this)
   {
     Trace("cegqi") << "Register conjecture : " << q << std::endl;
@@ -287,9 +289,15 @@ void SynthEngine::registerQuantifier(Node q)
       assignConjecture(q);
     }
   }
-  else
+  if (options::sygusRecFun())
   {
-    Trace("cegqi-debug") << "Register quantifier : " << q << std::endl;
+    if (d_quantEngine->getQuantAttributes()->isFunDef(q))
+    {
+      // If it is a recursive function definition, add it to the function
+      // definition evaluator class.
+      FunDefEvaluator* fde = d_tds->getFunDefEvaluator();
+      fde->assertDefinition(q);
+    }
   }
 }
 
diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h
index 20e4deec6..1eca56959 100644
--- a/src/theory/quantifiers/sygus/synth_engine.h
+++ b/src/theory/quantifiers/sygus/synth_engine.h
@@ -30,33 +30,6 @@ class SynthEngine : public QuantifiersModule
 {
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
 
- private:
-  /** the conjecture formula(s) we are waiting to assign */
-  std::vector<Node> d_waiting_conj;
-  /** The synthesis conjectures that this class is managing. */
-  std::vector<std::unique_ptr<SynthConjecture> > d_conjs;
-  /**
-   * The first conjecture in the above vector. We track this conjecture
-   * so that a synthesis conjecture can be preregistered during a call to
-   * preregisterAssertion.
-   */
-  SynthConjecture* d_conj;
-  /** assign quantified formula q as a conjecture
-   *
-   * This method either assigns q to a synthesis conjecture object in d_conjs,
-   * or otherwise reduces q to an equivalent form. This method does the latter
-   * if this class determines that it would rather rewrite q to an equivalent
-   * form r (in which case this method returns the lemma q <=> r). An example of
-   * this is the quantifier elimination step option::sygusQePreproc().
-   */
-  void assignConjecture(Node q);
-  /** check conjecture
-   *
-   * This method returns true if the conjecture is finished processing solutions
-   * for this call to SynthEngine::check().
-   */
-  bool checkConjecture(SynthConjecture* conj);
-
  public:
   SynthEngine(QuantifiersEngine* qe, context::Context* c);
   ~SynthEngine();
@@ -113,6 +86,35 @@ class SynthEngine : public QuantifiersModule
     ~Statistics();
   }; /* class SynthEngine::Statistics */
   Statistics d_statistics;
+
+ private:
+  /** term database sygus of d_qe */
+  TermDbSygus* d_tds;
+  /** the conjecture formula(s) we are waiting to assign */
+  std::vector<Node> d_waiting_conj;
+  /** The synthesis conjectures that this class is managing. */
+  std::vector<std::unique_ptr<SynthConjecture> > d_conjs;
+  /**
+   * The first conjecture in the above vector. We track this conjecture
+   * so that a synthesis conjecture can be preregistered during a call to
+   * preregisterAssertion.
+   */
+  SynthConjecture* d_conj;
+  /** assign quantified formula q as a conjecture
+   *
+   * This method either assigns q to a synthesis conjecture object in d_conjs,
+   * or otherwise reduces q to an equivalent form. This method does the latter
+   * if this class determines that it would rather rewrite q to an equivalent
+   * form r (in which case this method returns the lemma q <=> r). An example of
+   * this is the quantifier elimination step option::sygusQePreproc().
+   */
+  void assignConjecture(Node q);
+  /** check conjecture
+   *
+   * This method returns true if the conjecture is finished processing solutions
+   * for this call to SynthEngine::check().
+   */
+  bool checkConjecture(SynthConjecture* conj);
 }; /* class SynthEngine */
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index d17c343f4..84a9c2405 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -50,6 +50,7 @@ TermDbSygus::TermDbSygus(context::Context* c, QuantifiersEngine* qe)
       d_syexp(new SygusExplain(this)),
       d_ext_rw(new ExtendedRewriter(true)),
       d_eval(new Evaluator),
+      d_funDefEval(new FunDefEvaluator),
       d_eval_unfold(new SygusEvalUnfold(this))
 {
   d_true = NodeManager::currentNM()->mkConst( true );
@@ -725,6 +726,28 @@ SygusTypeInfo& TermDbSygus::getTypeInfo(TypeNode tn)
   return d_tinfo[tn];
 }
 
+Node TermDbSygus::rewriteNode(Node n) const
+{
+  Node res = Rewriter::rewrite(n);
+  if (options::sygusRecFun())
+  {
+    if (d_funDefEval->hasDefinitions())
+    {
+      // If recursive functions are enabled, then we use the recursive function
+      // evaluation utility.
+      Node fres = d_funDefEval->evaluate(res);
+      if (!fres.isNull())
+      {
+        return fres;
+      }
+      // It may have failed, in which case there are undefined symbols in res.
+      // In this case, we revert to the result of rewriting in the return
+      // statement below.
+    }
+  }
+  return res;
+}
+
 unsigned TermDbSygus::getSelectorWeight(TypeNode tn, Node sel)
 {
   std::map<TypeNode, std::map<Node, unsigned> >::iterator itsw =
@@ -1061,7 +1084,9 @@ Node TermDbSygus::evaluateBuiltin(TypeNode tn,
     return res;
   }
   res = bn.substitute(varlist.begin(), varlist.end(), args.begin(), args.end());
-  return Rewriter::rewrite(res);
+  // Call the rewrite node function, which may involve recursive function
+  // evaluation.
+  return rewriteNode(res);
 }
 
 Node TermDbSygus::evaluateWithUnfolding(
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index c591400e1..0ec883537 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -21,6 +21,7 @@
 
 #include "theory/evaluator.h"
 #include "theory/quantifiers/extended_rewrite.h"
+#include "theory/quantifiers/fun_def_evaluator.h"
 #include "theory/quantifiers/sygus/sygus_eval_unfold.h"
 #include "theory/quantifiers/sygus/sygus_explain.h"
 #include "theory/quantifiers/sygus/type_info.h"
@@ -77,6 +78,8 @@ class TermDbSygus {
   ExtendedRewriter* getExtRewriter() { return d_ext_rw.get(); }
   /** get the evaluator */
   Evaluator* getEvaluator() { return d_eval.get(); }
+  /** (recursive) function evaluator utility */
+  FunDefEvaluator* getFunDefEvaluator() { return d_funDefEval.get(); }
   /** evaluation unfolding utility */
   SygusEvalUnfold* getEvalUnfold() { return d_eval_unfold.get(); }
   //------------------------------end utilities
@@ -302,6 +305,11 @@ class TermDbSygus {
    * (a subfield type of) a type that has been registered to this class.
    */
   SygusTypeInfo& getTypeInfo(TypeNode tn);
+  /**
+   * Rewrite the given node using the utilities in this class. This may
+   * involve (recursive function) evaluation.
+   */
+  Node rewriteNode(Node n) const;
 
   /** print to sygus stream n on trace c */
   static void toStreamSygus(const char* c, Node n);
@@ -317,6 +325,8 @@ class TermDbSygus {
   std::unique_ptr<ExtendedRewriter> d_ext_rw;
   /** evaluator */
   std::unique_ptr<Evaluator> d_eval;
+  /** (recursive) function evaluator utility */
+  std::unique_ptr<FunDefEvaluator> d_funDefEval;
   /** evaluation function unfolding utility */
   std::unique_ptr<SygusEvalUnfold> d_eval_unfold;
   //------------------------------end utilities