Decision strategy: incorporate cegis unif (#2482)

1 files changed, 19 insertions, 40 deletions

diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index 69d6ee25f..ae2d7964b 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -26,9 +26,9 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-/** Cegis Unif Enumeration Manager
+/** Cegis Unif Enumerators Decision Strategy
  *
- * This class enforces a decision heuristic that limits the number of
+ * This class enforces a decision strategy that limits the number of
  * unique values given to the set of heads of evaluation points and conditions
  * enumerators for these points, which are variables of sygus datatype type that
  * are introduced by CegisUnif.
@@ -42,12 +42,24 @@ namespace quantifiers {
  * To enforce this, we introduce sygus enumerator(s) of the same type as the
  * heads of evaluation points and condition enumerators registered to this class
  * and add lemmas that enforce that these terms are equal to at least one
- * enumerator (see registerEvalPtAtValue).
+ * enumerator (see registerEvalPtAtSize).
  */
-class CegisUnifEnumManager
+class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf
 {
  public:
-  CegisUnifEnumManager(QuantifiersEngine* qe, CegConjecture* parent);
+  CegisUnifEnumDecisionStrategy(QuantifiersEngine* qe, CegConjecture* parent);
+  /** Make the n^th literal of this strategy (G_uq_n).
+   *
+   * This call may add new lemmas of the form described above
+   * registerEvalPtAtValue on the output channel of d_qe.
+   */
+  Node mkLiteral(unsigned n) override;
+  /** identify */
+  std::string identify() const override
+  {
+    return std::string("cegis_unif_num_enums");
+  }
+
   /** initialize candidates
    *
    * Notify this class that it will be managing enumerators for the vector
@@ -73,29 +85,11 @@ class CegisUnifEnumManager
    * for strategy point e, where e was passed to initialize in the vector es.
    *
    * This may add new lemmas of the form described above
-   * registerEvalPtAtValue on the output channel of d_qe.
+   * registerEvalPtAtSize on the output channel of d_qe.
    */
   void registerEvalPts(const std::vector<Node>& eis, Node e);
   /** Retrieves active guard for enumerator */
   Node getActiveGuardForEnumerator(Node e);
-  /** 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);
-  /**
-   * 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;
-
  private:
   /** reference to quantifier engine */
   QuantifiersEngine* d_qe;
@@ -143,10 +137,6 @@ class CegisUnifEnumManager
   };
   /** map strategy points to the above info */
   std::map<Node, StrategyPtInfo> 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 "virtual" enumerator
    *
    * This enumerator is used for enforcing fairness. In particular, we relate
@@ -165,11 +155,6 @@ class CegisUnifEnumManager
    *   (0,8), ..., (0,15), (1,8), ..., (1,15), ...              [size 3]
    */
   Node d_virtual_enum;
-  /**
-   * The minimal n such that G_uq_n is not asserted negatively in the
-   * current SAT context.
-   */
-  context::CDO<unsigned> d_curr_guq_val;
   /** Registers an enumerator and adds symmetry breaking lemmas
    *
    * The symmetry breaking lemmas are generated according to the stored
@@ -179,10 +164,6 @@ class CegisUnifEnumManager
    * order of size.
    */
   void setUpEnumerator(Node e, StrategyPtInfo& si, unsigned index);
-  /** increment the number of enumerators */
-  void incrementNumEnumerators();
-  /** get literal G_uq_n */
-  Node getLiteral(unsigned n) const;
   /** register evaluation point at size
    *
    * This sends a lemma of the form:
@@ -246,8 +227,6 @@ 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:
   /** do cegis-implementation-specific initialization for this class */
@@ -288,7 +267,7 @@ class CegisUnif : public Cegis
    */
   SygusUnifRl d_sygus_unif;
   /** enumerator manager utility */
-  CegisUnifEnumManager d_u_enum_manager;
+  CegisUnifEnumDecisionStrategy d_u_enum_manager;
   /* The null node */
   Node d_null;
   /** the unification candidates */