Cegis unif enumerator manager (#1837)

2 files changed, 232 insertions, 0 deletions

diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 256955bbd..cbd9358e0 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -235,6 +235,138 @@ void CegisUnif::registerRefinementLemma(const std::vector<Node>& vars,
       NodeManager::currentNM()->mkNode(OR, d_parent->getGuard().negate(), lem));
 }
 
+CegisUnifEnumManager::CegisUnifEnumManager(QuantifiersEngine* qe,
+                                           CegConjecture* parent)
+    : d_qe(qe), d_parent(parent), d_curr_guq_val(qe->getSatContext(), 0)
+{
+  d_tds = d_qe->getTermDatabaseSygus();
+}
+
+void CegisUnifEnumManager::initialize(std::vector<Node>& cs)
+{
+  for (const Node& c : cs)
+  {
+    // currently, we allocate the same enumerators for candidates of the same
+    // type
+    TypeNode tn = c.getType();
+    d_ce_info[tn].d_candidates.push_back(c);
+  }
+  // initialize the current literal
+  incrementNumEnumerators();
+}
+
+void CegisUnifEnumManager::registerEvalPts(std::vector<Node>& eis, Node c)
+{
+  // candidates of the same type are managed
+  TypeNode ct = c.getType();
+  std::map<TypeNode, TypeInfo>::iterator it = d_ce_info.find(ct);
+  Assert(it != d_ce_info.end());
+  it->second.d_eval_points.insert(
+      it->second.d_eval_points.end(), eis.begin(), eis.end());
+  // register at all already allocated sizes
+  for (const std::pair<const unsigned, Node>& p : d_guq_lit)
+  {
+    for (const Node& ei : eis)
+    {
+      Assert(ei.getType() == ct);
+      registerEvalPtAtSize(ct, ei, p.second, p.first);
+    }
+  }
+}
+
+Node CegisUnifEnumManager::getNextDecisionRequest(unsigned& priority)
+{
+  Node lit = getCurrentLiteral();
+  bool value;
+  if (!d_qe->getValuation().hasSatValue(lit, value))
+  {
+    priority = 0;
+    return lit;
+  }
+  else if (!value)
+  {
+    // propagated false, increment
+    incrementNumEnumerators();
+    return getNextDecisionRequest(priority);
+  }
+  return Node::null();
+}
+
+void CegisUnifEnumManager::incrementNumEnumerators()
+{
+  unsigned new_size = d_curr_guq_val.get() + 1;
+  d_curr_guq_val.set(new_size);
+  // ensure that the literal has been allocated
+  std::map<unsigned, Node>::iterator itc = d_guq_lit.find(new_size);
+  if (itc == d_guq_lit.end())
+  {
+    // allocate the new literal
+    NodeManager* nm = NodeManager::currentNM();
+    Node new_lit = Rewriter::rewrite(nm->mkSkolem("G_cost", nm->booleanType()));
+    new_lit = d_qe->getValuation().ensureLiteral(new_lit);
+    AlwaysAssert(!new_lit.isNull());
+    d_qe->getOutputChannel().requirePhase(new_lit, true);
+    d_guq_lit[new_size] = new_lit;
+    // allocate an enumerator for each candidate
+    for (std::pair<const TypeNode, TypeInfo>& ci : d_ce_info)
+    {
+      TypeNode ct = ci.first;
+      Node eu = nm->mkSkolem("eu", ct);
+      if (!ci.second.d_enums.empty())
+      {
+        Node eu_prev = ci.second.d_enums.back();
+        // symmetry breaking
+        Node size_eu = nm->mkNode(DT_SIZE, eu);
+        Node size_eu_prev = nm->mkNode(DT_SIZE, eu_prev);
+        Node sym_break = nm->mkNode(GEQ, size_eu, size_eu_prev);
+        d_qe->getOutputChannel().lemma(sym_break);
+      }
+      ci.second.d_enums.push_back(eu);
+      d_tds->registerEnumerator(eu, d_null, d_parent);
+    }
+    // register the evaluation points at the new value
+    for (std::pair<const TypeNode, TypeInfo>& ci : d_ce_info)
+    {
+      TypeNode ct = ci.first;
+      for (const Node& ei : ci.second.d_eval_points)
+      {
+        registerEvalPtAtSize(ct, ei, new_lit, new_size);
+      }
+    }
+  }
+}
+
+Node CegisUnifEnumManager::getCurrentLiteral() const
+{
+  return getLiteral(d_curr_guq_val.get());
+}
+
+Node CegisUnifEnumManager::getLiteral(unsigned n) const
+{
+  std::map<unsigned, Node>::const_iterator itc = d_guq_lit.find(n);
+  Assert(itc != d_guq_lit.end());
+  return itc->second;
+}
+
+void CegisUnifEnumManager::registerEvalPtAtSize(TypeNode ct,
+                                                Node ei,
+                                                Node guq_lit,
+                                                unsigned n)
+{
+  // must be equal to one of the first n enums
+  std::map<TypeNode, TypeInfo>::iterator itc = d_ce_info.find(ct);
+  Assert(itc != d_ce_info.end());
+  Assert(itc->second.d_enums.size() >= n);
+  std::vector<Node> disj;
+  disj.push_back(guq_lit.negate());
+  for (unsigned i = 0; i < n; i++)
+  {
+    disj.push_back(ei.eqNode(itc->second.d_enums[i]));
+  }
+  Node lem = NodeManager::currentNM()->mkNode(OR, disj);
+  d_qe->getOutputChannel().lemma(lem);
+}
+
 }  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index 78586cd9c..3100d7d0d 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -152,6 +152,106 @@ class CegisUnif : public SygusModule
 
 }; /* class CegisUnif */
 
+/** 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.
+ *
+ * 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".
+ *
+ * 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).
+ */
+class CegisUnifEnumManager
+{
+ public:
+  CegisUnifEnumManager(QuantifiersEngine* qe, CegConjecture* parent);
+  /** initialize candidates
+   *
+   * Notify this class that it will be managing enumerators for the vector
+   * of functions-to-synthesize (candidate variables) in candidates. This
+   * function should only be called once.
+   *
+   * 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);
+  /** 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 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);
+  /** get next decision request
+   *
+   * This function has the same contract as Theory::getNextDecisionRequest.
+   *
+   * If no guard G_uq_* is asserted positively, then this method returns the
+   * minimal G_uq_i that is not asserted negatively. It allocates this guard
+   * if necessary.
+   *
+   * This call may add new lemmas of the form described above
+   * registerEvalPtAtValue on the output channel of d_qe.
+   */
+  Node getNextDecisionRequest(unsigned& priority);
+
+ private:
+  /** reference to quantifier engine */
+  QuantifiersEngine* d_qe;
+  /** sygus term database of d_qe */
+  TermDbSygus* d_tds;
+  /** reference to the parent conjecture */
+  CegConjecture* d_parent;
+  /** null node */
+  Node d_null;
+  /** information per initialized type */
+  class TypeInfo
+  {
+   public:
+    TypeInfo() {}
+    /** candidates for this type */
+    std::vector<Node> d_candidates;
+    /** the set of enumerators we have allocated for this candidate */
+    std::vector<Node> d_enums;
+    /** the set of evaluation points of this type */
+    std::vector<Node> d_eval_points;
+  };
+  /** map types to the above info */
+  std::map<TypeNode, TypeInfo> d_ce_info;
+  /** literals of the form G_uq_n for each n */
+  std::map<unsigned, Node> d_guq_lit;
+  /**
+   * The minimal n such that G_uq_n is not asserted negatively in the
+   * current SAT context.
+   */
+  context::CDO<unsigned> d_curr_guq_val;
+  /** increment the number of enumerators */
+  void incrementNumEnumerators();
+  /**
+   * Get the "current" literal G_uq_n, where n is the minimal n such that G_uq_n
+   * is not asserted negatively in the current SAT context.
+   */
+  Node getCurrentLiteral() const;
+  /** get literal G_uq_n */
+  Node getLiteral(unsigned n) const;
+  /** register evaluation point at size
+   *
+   * This sends a lemma of the form:
+   *   G_uq_n => ei = d1 V ... V ei = dn
+   * on the output channel of d_qe, where d1...dn are sygus enumerators of the
+   * same type (ct) as ei.
+   */
+  void registerEvalPtAtSize(TypeNode ct, Node ei, Node guq_lit, unsigned n);
+};
+
 }  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4