Link cegis unif with the enumeration manager (#1859)

4 files changed, 216 insertions, 146 deletions

diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
index db641a82e..d5a430229 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
@@ -479,51 +479,74 @@ Node CegConjecture::getNextDecisionRequest( unsigned& priority ) {
   if( !d_qe->getValuation().hasSatValue( feasible_guard, value ) ) {
     priority = 0;
     return feasible_guard;
-  }else{
-    if( value ){  
-      // the conjecture is feasible
-      if( options::sygusStream() ){
-        Assert( !isSingleInvocation() );
-        // if we are in sygus streaming mode, then get the "next guard" 
-        // which denotes "we have not yet generated the next solution to the conjecture"
-        Node curr_stream_guard = getCurrentStreamGuard();
-        bool needs_new_stream_guard = false;
-        if( curr_stream_guard.isNull() ){
-          needs_new_stream_guard = true;
-        }else{
-          // check the polarity of the guard
-          if( !d_qe->getValuation().hasSatValue( curr_stream_guard, value ) ) {
-            priority = 0;
-            return curr_stream_guard;
-          }else{
-            if( !value ){
-              Trace("cegqi-debug") << "getNextDecision : we have a new solution since stream guard was propagated false: " << curr_stream_guard << std::endl;
-              // need to make the next stream guard
-              needs_new_stream_guard = true;
-              // the guard has propagated false, indicating that a verify
-              // lemma was unsatisfiable. Hence, the previous candidate is
-              // an actual solution. We print and continue the stream.
-              printAndContinueStream();
-            }
-          }
-        }
-        if( needs_new_stream_guard ){
-          // generate a new stream guard
-          curr_stream_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G_Stream", NodeManager::currentNM()->booleanType() ) );
-          curr_stream_guard = d_qe->getValuation().ensureLiteral( curr_stream_guard );
-          AlwaysAssert( !curr_stream_guard.isNull() );
-          d_qe->getOutputChannel().requirePhase( curr_stream_guard, true );
-          d_stream_guards.push_back( curr_stream_guard );
-          Trace("cegqi-debug") << "getNextDecision : allocate new stream guard : " << curr_stream_guard << std::endl;
-          // return it as a decision
-          priority = 0;
-          return curr_stream_guard;
-        }
-      }
+  }
+  if (!value)
+  {
+    Trace("cegqi-debug") << "getNextDecision : conjecture is infeasible."
+                         << std::endl;
+    return Node::null();
+  }
+  // the conjecture is feasible
+  if (options::sygusStream())
+  {
+    Assert(!isSingleInvocation());
+    // if we are in sygus streaming mode, then get the "next guard"
+    // which denotes "we have not yet generated the next solution to the
+    // conjecture"
+    Node curr_stream_guard = getCurrentStreamGuard();
+    bool needs_new_stream_guard = false;
+    if (curr_stream_guard.isNull())
+    {
+      needs_new_stream_guard = true;
     }else{
-      Trace("cegqi-debug") << "getNextDecision : conjecture is infeasible." << std::endl;
-    } 
+      // check the polarity of the guard
+      if (!d_qe->getValuation().hasSatValue(curr_stream_guard, value))
+      {
+        priority = 0;
+        return curr_stream_guard;
+      }
+      if (!value)
+      {
+        Trace("cegqi-debug") << "getNextDecision : we have a new solution "
+                                "since stream guard was propagated false: "
+                             << curr_stream_guard << std::endl;
+        // need to make the next stream guard
+        needs_new_stream_guard = true;
+        // the guard has propagated false, indicating that a verify
+        // lemma was unsatisfiable. Hence, the previous candidate is
+        // an actual solution. We print and continue the stream.
+        printAndContinueStream();
+      }
+    }
+    if (needs_new_stream_guard)
+    {
+      // generate a new stream guard
+      curr_stream_guard = Rewriter::rewrite(NodeManager::currentNM()->mkSkolem(
+          "G_Stream", NodeManager::currentNM()->booleanType()));
+      curr_stream_guard = d_qe->getValuation().ensureLiteral(curr_stream_guard);
+      AlwaysAssert(!curr_stream_guard.isNull());
+      d_qe->getOutputChannel().requirePhase(curr_stream_guard, true);
+      d_stream_guards.push_back(curr_stream_guard);
+      Trace("cegqi-debug") << "getNextDecision : allocate new stream guard : "
+                           << curr_stream_guard << std::endl;
+      // return it as a decision
+      priority = 0;
+      return curr_stream_guard;
+    }
   }
+  // see if the master module has a decision
+  if (!isSingleInvocation())
+  {
+    Assert(d_master != nullptr);
+    Node mlit = d_master->getNextDecisionRequest(priority);
+    if (!mlit.isNull())
+    {
+      Trace("cegqi-debug") << "getNextDecision : master module returned : "
+                           << mlit << std::endl;
+      return mlit;
+    }
+  }
+
   return Node::null();
 }
 
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 14a5bedf5..ee8fb6f12 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -26,7 +26,7 @@ namespace theory {
 namespace quantifiers {
 
 CegisUnif::CegisUnif(QuantifiersEngine* qe, CegConjecture* p)
-    : Cegis(qe, p), d_sygus_unif(p)
+    : Cegis(qe, p), d_sygus_unif(p), d_u_enum_manager(qe, p)
 {
   d_tds = d_qe->getTermDatabaseSygus();
 }
@@ -39,16 +39,24 @@ bool CegisUnif::initialize(Node n,
   Trace("cegis-unif") << "Initialize CegisUnif : " << n << std::endl;
   /* Init UNIF util */
   d_sygus_unif.initialize(d_qe, candidates, d_cond_enums, lemmas);
-  /* TODO initialize unif enumerators */
   Trace("cegis-unif") << "Initializing enums for pure Cegis case\n";
+  std::vector<Node> unif_candidates;
   /* Initialize enumerators for non-unif functions-to-synhesize */
   for (const Node& c : candidates)
   {
     if (!d_sygus_unif.usingUnif(c))
     {
+      Trace("cegis-unif") << "* non-unification candidate : " << c << std::endl;
       d_tds->registerEnumerator(c, c, d_parent);
     }
+    else
+    {
+      Trace("cegis-unif") << "* unification candidate : " << c << std::endl;
+      unif_candidates.push_back(c);
+    }
   }
+  // initialize the enumeration manager
+  d_u_enum_manager.initialize(unif_candidates);
   return true;
 }
 
@@ -158,15 +166,27 @@ void CegisUnif::registerRefinementLemma(const std::vector<Node>& vars,
       OR, d_parent->getGuard().negate(), plem));
 }
 
+Node CegisUnif::getNextDecisionRequest(unsigned& priority)
+{
+  return d_u_enum_manager.getNextDecisionRequest(priority);
+}
+
 CegisUnifEnumManager::CegisUnifEnumManager(QuantifiersEngine* qe,
                                            CegConjecture* parent)
-    : d_qe(qe), d_parent(parent), d_curr_guq_val(qe->getSatContext(), 0)
+    : d_qe(qe),
+      d_parent(parent),
+      d_ret_dec(qe->getSatContext(), false),
+      d_curr_guq_val(qe->getSatContext(), 0)
 {
   d_tds = d_qe->getTermDatabaseSygus();
 }
 
 void CegisUnifEnumManager::initialize(std::vector<Node>& cs)
 {
+  if (cs.empty())
+  {
+    return;
+  }
   for (const Node& c : cs)
   {
     // currently, we allocate the same enumerators for candidates of the same
@@ -199,10 +219,23 @@ void CegisUnifEnumManager::registerEvalPts(std::vector<Node>& eis, Node c)
 
 Node CegisUnifEnumManager::getNextDecisionRequest(unsigned& priority)
 {
+  // have we returned our decision in the current SAT context?
+  if (d_ret_dec.get())
+  {
+    return Node::null();
+  }
+  // only call this after initialization
+  if (d_ce_info.empty())
+  {
+    // if no enumerators, the decision is null
+    d_ret_dec = true;
+    return Node::null();
+  }
   Node lit = getCurrentLiteral();
   bool value;
   if (!d_qe->getValuation().hasSatValue(lit, value))
   {
+    d_ret_dec = true;
     priority = 0;
     return lit;
   }
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index ab2192ff8..2b1f1584a 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -26,6 +26,108 @@ namespace CVC4 {
 namespace theory {
 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.
+ *
+ * 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;
+  /** Have we returned a decision in the current SAT context? */
+  context::CDO<bool> d_ret_dec;
+  /**
+   * 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);
+};
+
 /** Synthesizes functions in a data-driven SyGuS approach
  *
  * Data is derived from refinement lemmas generated through the regular CEGIS
@@ -110,6 +212,8 @@ class CegisUnif : public Cegis
   void registerRefinementLemma(const std::vector<Node>& vars,
                                Node lem,
                                std::vector<Node>& lems) override;
+  /** get next decision request */
+  Node getNextDecisionRequest(unsigned& priority) override;
 
  private:
   /** sygus term database of d_qe */
@@ -119,6 +223,8 @@ class CegisUnif : public Cegis
    * tree learning) that this module relies upon.
    */
   SygusUnifRl d_sygus_unif;
+  /** enumerator manager utility */
+  CegisUnifEnumManager d_u_enum_manager;
   /**
    * list of conditonal enumerators to build solutions for candidates being
    * synthesized with unification techniques
@@ -130,106 +236,6 @@ class CegisUnif : public Cegis
   Node d_null;
 }; /* 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
diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h
index 0a3fa9995..07f5aec9d 100644
--- a/src/theory/quantifiers/sygus/sygus_module.h
+++ b/src/theory/quantifiers/sygus/sygus_module.h
@@ -114,6 +114,14 @@ class SygusModule
                                        std::vector<Node>& lems)
   {
   }
+  /** get next decision request
+   *
+   * This has the same contract as Theory::getNextDecisionRequest.
+   */
+  virtual Node getNextDecisionRequest(unsigned& priority)
+  {
+    return Node::null();
+  }
 
  protected:
   /** reference to quantifier engine */