Cegis unif register evaluation points (#1878)

4 files changed, 68 insertions, 27 deletions

diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index cc477fa62..8fa4af99c 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -171,9 +171,15 @@ void CegisUnif::registerRefinementLemma(const std::vector<Node>& vars,
                                         Node lem,
                                         std::vector<Node>& lems)
 {
-  /* Notify lemma to unification utility and get its purified form */
-  Node plem = d_sygus_unif.addRefLemma(lem);
+  // Notify lemma to unification utility and get its purified form
+  std::map<Node, std::vector<Node> > eval_pts;
+  Node plem = d_sygus_unif.addRefLemma(lem, eval_pts);
   d_refinement_lemmas.push_back(plem);
+  // Notify the enumeration manager if there are new evaluation points
+  for (const std::pair<const Node, std::vector<Node> >& ep : eval_pts)
+  {
+    d_u_enum_manager.registerEvalPts(ep.second, ep.first);
+  }
   /* Make the refinement lemma and add it to lems. This lemma is guarded by the
      parent's guard, which has the semantics "this conjecture has a solution",
      hence this lemma states: if the parent conjecture has a solution, it
@@ -197,7 +203,7 @@ CegisUnifEnumManager::CegisUnifEnumManager(QuantifiersEngine* qe,
   d_tds = d_qe->getTermDatabaseSygus();
 }
 
-void CegisUnifEnumManager::initialize(std::vector<Node>& cs)
+void CegisUnifEnumManager::initialize(const std::vector<Node>& cs)
 {
   if (cs.empty())
   {
@@ -214,7 +220,7 @@ void CegisUnifEnumManager::initialize(std::vector<Node>& cs)
   incrementNumEnumerators();
 }
 
-void CegisUnifEnumManager::registerEvalPts(std::vector<Node>& eis, Node c)
+void CegisUnifEnumManager::registerEvalPts(const std::vector<Node>& eis, Node c)
 {
   // candidates of the same type are managed
   TypeNode ct = c.getType();
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index 2b1f1584a..93ab69668 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -29,16 +29,17 @@ namespace quantifiers {
 /** Cegis Unif Enumeration Manager
  *
  * This class enforces a decision heuristic that limits the number of
- * unique values given to the set of "evaluation points", which are variables
- * of sygus datatype type that are introduced by CegisUnif.
+ * unique values given to the set of heads of evaluation points, which are
+ * variables of sygus datatype type that are introduced by CegisUnif.
  *
  * It maintains a set of guards, call them G_uq_1 ... G_uq_n, where the
- * semantics of G_uq_i is "for each type, the evaluation points of that type
- * are interpreted as a value in a set whose cardinality is at most i".
+ * semantics of G_uq_i is "for each type, the heads of evaluation points of that
+ * type are interpreted as a value in a set whose cardinality is at most i".
  *
  * To enforce this, we introduce sygus enumerator(s) of the same type as the
- * evaluation points registered to this class and add lemmas that enforce that
- * points are equal to at least one enumerator (see registerEvalPtAtValue).
+ * heads of evaluation points registered to this class and add lemmas that
+ * enforce that these terms are equal to at least one enumerator (see
+ * registerEvalPtAtValue).
  */
 class CegisUnifEnumManager
 {
@@ -53,17 +54,17 @@ class CegisUnifEnumManager
    * Each candidate c in cs should be such that we are using a
    * synthesis-by-unification approach for c.
    */
-  void initialize(std::vector<Node>& cs);
+  void initialize(const std::vector<Node>& cs);
   /** register evaluation point for candidate
    *
-   * This notifies this class that eis is a set of evaluation points for
-   * candidate c, where c should be a candidate that was passed to initialize
-   * in the vector cs.
+   * This notifies this class that eis is a set of heads of evaluation points
+   * for candidate c, where c should be a candidate that was passed to
+   * initialize in the vector cs.
    *
    * This may add new lemmas of the form described above
    * registerEvalPtAtValue on the output channel of d_qe.
    */
-  void registerEvalPts(std::vector<Node>& eis, Node c);
+  void registerEvalPts(const std::vector<Node>& eis, Node c);
   /** get next decision request
    *
    * This function has the same contract as Theory::getNextDecisionRequest.
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index 2cf751927..2f0460c64 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -31,7 +31,7 @@ void SygusUnifRl::initialize(QuantifiersEngine* qe,
                              std::vector<Node>& lemmas)
 {
   d_ecache.clear();
-  d_cand_to_pt_enum.clear();
+  d_cand_to_eval_hds.clear();
   // initialize
   std::vector<Node> all_enums;
   SygusUnif::initialize(qe, funs, all_enums, lemmas);
@@ -46,7 +46,7 @@ void SygusUnifRl::initialize(QuantifiersEngine* qe,
   for (const Node& c : d_unif_candidates)
   {
     d_app_to_pt[c].clear();
-    d_cand_to_pt_enum[c].clear();
+    d_cand_to_eval_hds[c].clear();
     d_purified_count[c] = 0;
   }
 }
@@ -153,7 +153,7 @@ Node SygusUnifRl::purifyLemma(Node n,
       /* Adds new enumerator to map from candidate */
       Trace("sygus-unif-rl-purify") << "...new enum " << new_f
                                         << " for candidate " << nb[0] << "\n";
-      d_cand_to_pt_enum[nb[0]].push_back(new_f);
+      d_cand_to_eval_hds[nb[0]].push_back(new_f);
       /* Maps new enumerator to its respective tuple of arguments */
       d_app_to_pt[new_f] =
           std::vector<Node>(children.begin() + 2, children.end());
@@ -199,12 +199,20 @@ Node SygusUnifRl::purifyLemma(Node n,
   return nb;
 }
 
-Node SygusUnifRl::addRefLemma(Node lemma)
+Node SygusUnifRl::addRefLemma(Node lemma,
+                              std::map<Node, std::vector<Node>>& eval_hds)
 {
   Trace("sygus-unif-rl-purify") << "Registering lemma at SygusUnif : " << lemma
                                << "\n";
   std::vector<Node> model_guards;
   BoolNodePairMap cache;
+  // cache previous sizes
+  std::map<Node, unsigned> prev_n_eval_hds;
+  for (const std::pair<const Node, std::vector<Node>>& cp : d_cand_to_eval_hds)
+  {
+    prev_n_eval_hds[cp.first] = cp.second.size();
+  }
+
   /* Make the purified lemma which will guide the unification utility. */
   Node plem = purifyLemma(lemma, false, model_guards, cache);
   if (!model_guards.empty())
@@ -214,6 +222,23 @@ Node SygusUnifRl::addRefLemma(Node lemma)
   }
   plem = Rewriter::rewrite(plem);
   Trace("sygus-unif-rl-purify") << "Purified lemma : " << plem << "\n";
+
+  Trace("sygus-unif-rl-purify") << "Collect new evaluation points...\n";
+  for (const std::pair<const Node, std::vector<Node>>& cp : d_cand_to_eval_hds)
+  {
+    Node c = cp.first;
+    unsigned prevn = 0;
+    std::map<Node, unsigned>::iterator itp = prev_n_eval_hds.find(c);
+    if (itp != prev_n_eval_hds.end())
+    {
+      prevn = itp->second;
+    }
+    for (unsigned j = prevn, size = cp.second.size(); j < size; j++)
+    {
+      eval_hds[c].push_back(cp.second[j]);
+    }
+  }
+
   return plem;
 }
 
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h
index b8ead4986..29c67aa81 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h
@@ -55,12 +55,21 @@ class SygusUnifRl : public SygusUnif
   void notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) override;
   /** Construct solution */
   bool constructSolution(std::vector<Node>& sols) override;
-  Node constructSol(Node f, Node e, NodeRole nrole, int ind) override;
   /** add refinement lemma
    *
-   * This adds a lemma to the specification for f.
+   * This adds a lemma to the specification. It returns the purified form
+   * of the lemma based on the method purifyLemma below. The method adds the
+   * head of "evaluation points" to the map eval_hds, where an evaluation point
+   * is a term of the form:
+   *   ev( e1, c1...cn )
+   * where ev is an evaluation function for the sygus deep embedding, e1 is of
+   * sygus datatype type (the "head" of the evaluation point), and c1...cn are
+   * constants. If ev( e1, c1...cn ) is the purified form of ev( e, t1...tn ),
+   * then e1 is added to eval_hds[e]. We add evaluation points to eval_hds only
+   * for those terms that are newly generated by this call (and have not been
+   * returned by a previous call to this method).
    */
-  Node addRefLemma(Node lemma);
+  Node addRefLemma(Node lemma, std::map<Node, std::vector<Node>>& eval_hds);
   /**
    * whether f is being synthesized with unification strategies. This can be
    * checked through wehether f has conditional or point enumerators (we use the
@@ -75,8 +84,7 @@ class SygusUnifRl : public SygusUnif
   std::unordered_set<Node, NodeHashFunction> d_unif_candidates;
   /**
    * This class stores information regarding an enumerator, including: a
-   * database
-   * of values that have been enumerated for this enumerator.
+   * database of values that have been enumerated for this enumerator.
    */
   class EnumCache
   {
@@ -88,7 +96,8 @@ class SygusUnifRl : public SygusUnif
   };
   /** maps enumerators to the information above */
   std::map<Node, EnumCache> d_ecache;
-
+  /** construct sol */
+  Node constructSol(Node f, Node e, NodeRole nrole, int ind) override;
   /** collects data from refinement lemmas to drive solution construction
    *
    * In particular it rebuilds d_app_to_pt whenever d_prev_rlemmas is different
@@ -102,8 +111,8 @@ class SygusUnifRl : public SygusUnif
         Purification
     --------------------------------------------------------------
   */
-  /* Maps unif candidates to their point enumerators */
-  std::map<Node, std::vector<Node>> d_cand_to_pt_enum;
+  /* Maps unif candidates to heads of their evaluation points */
+  std::map<Node, std::vector<Node>> d_cand_to_eval_hds;
   /**
    * maps applications of the function-to-synthesize to their tuple of arguments
    * (which constitute a "data point") */