Decision strategy: incorporate cegis unif (#2482)

7 files changed, 139 insertions, 251 deletions

diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
index dafcab5de..30c0a3ae1 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
@@ -615,23 +615,6 @@ Node CegConjecture::getStreamGuardedLemma(Node n) const
   return n;
 }
 
-Node CegConjecture::getNextDecisionRequest(unsigned& priority)
-{
-  // 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();
-}
-
 CegConjecture::SygusStreamDecisionStrategy::SygusStreamDecisionStrategy(
     context::Context* satContext, Valuation valuation)
     : DecisionStrategyFmf(satContext, valuation)
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.h b/src/theory/quantifiers/sygus/ce_guided_conjecture.h
index 41ec6ab9e..adc75056e 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.h
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.h
@@ -50,8 +50,6 @@ public:
   Node getConjecture() { return d_quant; }
   /** get deep embedding version of conjecture */
   Node getEmbeddedConjecture() { return d_embed_quant; }
-  /** get next decision request */
-  Node getNextDecisionRequest( unsigned& priority );
   //-------------------------------for counterexample-guided check/refine
   /** increment the number of times we have successfully done candidate
    * refinement */
diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
index c59195746..d30cccd87 100644
--- a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
@@ -255,17 +255,6 @@ void CegInstantiation::registerQuantifier(Node q)
   }
 }
 
-Node CegInstantiation::getNextDecisionRequest( unsigned& priority ) {
-  if( d_conj->isAssigned() ){
-    Node dec_req = d_conj->getNextDecisionRequest( priority );
-    if( !dec_req.isNull() ){
-      Trace("cegqi-debug") << "CEGQI : Decide next on : " << dec_req << "..." << std::endl;
-      return dec_req;
-    }
-  }
-  return Node::null();
-}
-
 void CegInstantiation::checkConjecture(CegConjecture* conj)
 {
   Node q = conj->getEmbeddedConjecture();
diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.h b/src/theory/quantifiers/sygus/ce_guided_instantiation.h
index 9c81b6978..6bf33effb 100644
--- a/src/theory/quantifiers/sygus/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.h
@@ -60,8 +60,6 @@ public:
  void check(Theory::Effort e, QEffort quant_e) override;
  /* Called for new quantifiers */
  void registerQuantifier(Node q) override;
- /** get the next decision request */
- Node getNextDecisionRequest(unsigned& priority) override;
  /** Identify this module (for debugging, dynamic configuration, etc..) */
  std::string identify() const override { return "CegInstantiation"; }
  /** print solution for synthesis conjectures */
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 19b0ad717..56cc40244 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -20,6 +20,7 @@
 #include "theory/quantifiers/sygus/ce_guided_conjecture.h"
 #include "theory/quantifiers/sygus/sygus_unif_rl.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/theory_engine.h"
 
 using namespace CVC4::kind;
 
@@ -122,7 +123,7 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums,
   NodeManager* nm = NodeManager::currentNM();
   Valuation& valuation = d_qe->getValuation();
   bool addedUnifEnumSymBreakLemma = false;
-  Node cost_lit = d_u_enum_manager.getCurrentLiteral();
+  Node cost_lit = d_u_enum_manager.getAssertedLiteral();
   std::map<Node, std::vector<Node>> unif_enums[2];
   std::map<Node, std::vector<Node>> unif_values[2];
   for (const Node& c : d_unif_candidates)
@@ -171,7 +172,7 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums,
         if (index == 0)
         {
           // given a pool of unification enumerators eu_1, ..., eu_n,
-          // CegisUnifEnumManager insists that size(eu_1) <= ... <= size(eu_n).
+          // CegisUnifEnumDecisionStrategy insists that size(eu_1) <= ... <= size(eu_n).
           // We additionally insist that M(eu_i) < M(eu_{i+1}) when
           // size(eu_i) = size(eu_{i+1}), where < is pointer comparison.
           // We enforce this below by adding symmetry breaking lemmas of the
@@ -298,23 +299,112 @@ 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,
+CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy(QuantifiersEngine* qe,
                                            CegConjecture* parent)
-    : d_qe(qe),
-      d_parent(parent),
-      d_ret_dec(qe->getSatContext(), false),
-      d_curr_guq_val(qe->getSatContext(), 0)
+    : DecisionStrategyFmf(qe->getSatContext(), qe->getValuation()),
+      d_qe(qe),
+      d_parent(parent)
 {
   d_initialized = false;
   d_tds = d_qe->getTermDatabaseSygus();
 }
 
-void CegisUnifEnumManager::initialize(
+Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  Node new_lit = nm->mkSkolem("G_cost", nm->booleanType());
+  unsigned new_size = n + 1;
+
+  // allocate an enumerator for each candidate
+  for (std::pair<const Node, StrategyPtInfo>& ci : d_ce_info)
+  {
+    Node c = ci.first;
+    TypeNode ct = c.getType();
+    Node eu = nm->mkSkolem("eu", ct);
+    Node ceu;
+    if (!options::sygusUnifCondIndependent() && !ci.second.d_enums[0].empty())
+    {
+      // make a new conditional enumerator as well, starting the
+      // second type around
+      ceu = nm->mkSkolem("cu", ci.second.d_ce_type);
+    }
+    // register the new enumerators
+    for (unsigned index = 0; index < 2; index++)
+    {
+      Node e = index == 0 ? eu : ceu;
+      if (e.isNull())
+      {
+        continue;
+      }
+      setUpEnumerator(e, ci.second, index);
+    }
+  }
+  // register the evaluation points at the new value
+  for (std::pair<const Node, StrategyPtInfo>& ci : d_ce_info)
+  {
+    Node c = ci.first;
+    for (const Node& ei : ci.second.d_eval_points)
+    {
+      Trace("cegis-unif-enum") << "...increasing enum number for hd " << ei
+                               << " to new size " << new_size << "\n";
+      registerEvalPtAtSize(c, ei, new_lit, new_size);
+    }
+  }
+  // enforce fairness between number of enumerators and enumerator size
+  if (new_size > 1)
+  {
+    // construct the "virtual enumerator"
+    if (d_virtual_enum.isNull())
+    {
+      // we construct the default integer grammar with no variables, e.g.:
+      //   A -> 0 | 1 | A+A
+      TypeNode intTn = nm->integerType();
+      // use a null variable list
+      Node bvl;
+      std::stringstream ss;
+      ss << "_virtual_enum_grammar";
+      std::string virtualEnumName(ss.str());
+      std::map<TypeNode, std::vector<Node>> extra_cons;
+      std::map<TypeNode, std::vector<Node>> exclude_cons;
+      // do not include "-", which is included by default for integers
+      exclude_cons[intTn].push_back(nm->operatorOf(MINUS));
+      std::unordered_set<Node, NodeHashFunction> term_irrelevant;
+      TypeNode vtn = CegGrammarConstructor::mkSygusDefaultType(intTn,
+                                                               bvl,
+                                                               virtualEnumName,
+                                                               extra_cons,
+                                                               exclude_cons,
+                                                               term_irrelevant);
+      d_virtual_enum = nm->mkSkolem("_ve", vtn);
+      d_tds->registerEnumerator(d_virtual_enum, Node::null(), d_parent);
+    }
+    // if new_size is a power of two, then isPow2 returns log2(new_size)+1
+    // otherwise, this returns 0. In the case it returns 0, we don't care
+    // since the floor( log2( i ) ) = floor( log2( i - 1 ) ) and we do not
+    // increase our size bound.
+    unsigned pow_two = Integer(new_size).isPow2();
+    if (pow_two > 0)
+    {
+      Node size_ve = nm->mkNode(DT_SIZE, d_virtual_enum);
+      Node fair_lemma =
+          nm->mkNode(GEQ, size_ve, nm->mkConst(Rational(pow_two - 1)));
+      fair_lemma = nm->mkNode(OR, new_lit, fair_lemma);
+      Trace("cegis-unif-enum-lemma")
+          << "CegisUnifEnum::lemma, fairness size:" << fair_lemma << "\n";
+      // this lemma relates the number of conditions we enumerate and the
+      // maximum size of a term that is part of our solution. It is of the
+      // form:
+      //   G_uq_i => size(ve) >= log_2( i-1 )
+      // In other words, if we use i conditions, then we allow terms in our
+      // solution whose size is at most log_2(i-1).
+      d_qe->getOutputChannel().lemma(fair_lemma);
+    }
+  }
+
+  return new_lit;
+}
+
+void CegisUnifEnumDecisionStrategy::initialize(
     const std::vector<Node>& es,
     const std::map<Node, Node>& e_to_cond,
     const std::map<Node, std::vector<Node>>& strategy_lemmas)
@@ -360,8 +450,11 @@ void CegisUnifEnumManager::initialize(
           std::pair<Node, Node>(d_sbt_lemma, sp);
     }
   }
-  // initialize the current literal
-  incrementNumEnumerators();
+
+  // register this strategy
+  d_qe->getTheoryEngine()->getDecisionManager()->registerStrategy(
+      DecisionManager::STRAT_QUANT_CEGIS_UNIF_NUM_ENUMS, this);
+
   // create single condition enumerator for each decision tree strategy
   if (options::sygusUnifCondIndependent())
   {
@@ -375,13 +468,15 @@ void CegisUnifEnumManager::initialize(
   }
 }
 
-void CegisUnifEnumManager::getEnumeratorsForStrategyPt(Node e,
+void CegisUnifEnumDecisionStrategy::getEnumeratorsForStrategyPt(Node e,
                                                        std::vector<Node>& es,
                                                        unsigned index) const
 {
   // the number of active enumerators is related to the current cost value
-  unsigned num_enums = d_curr_guq_val.get();
-  Assert(num_enums > 0);
+  unsigned num_enums = 0;
+  bool has_num_enums = getAssertedLiteralIndex(num_enums);
+  AlwaysAssert(has_num_enums);
+  num_enums = num_enums + 1;
   if (index == 1)
   {
     // we always use (cost-1) conditions, or 1 if in the indepedent case
@@ -398,13 +493,13 @@ void CegisUnifEnumManager::getEnumeratorsForStrategyPt(Node e,
   }
 }
 
-Node CegisUnifEnumManager::getActiveGuardForEnumerator(Node e)
+Node CegisUnifEnumDecisionStrategy::getActiveGuardForEnumerator(Node e)
 {
   Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end());
   return d_enum_to_active_guard[e];
 }
 
-void CegisUnifEnumManager::setUpEnumerator(Node e,
+void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e,
                                            StrategyPtInfo& si,
                                            unsigned index)
 {
@@ -439,7 +534,7 @@ void CegisUnifEnumManager::setUpEnumerator(Node e,
       e, si.d_pt, d_parent, options::sygusUnifCondIndependent() && index == 1);
 }
 
-void CegisUnifEnumManager::registerEvalPts(const std::vector<Node>& eis, Node e)
+void CegisUnifEnumDecisionStrategy::registerEvalPts(const std::vector<Node>& eis, Node e)
 {
   // candidates of the same type are managed
   std::map<Node, StrategyPtInfo>::iterator it = d_ce_info.find(e);
@@ -450,163 +545,17 @@ void CegisUnifEnumManager::registerEvalPts(const std::vector<Node>& eis, Node e)
   for (const Node& ei : eis)
   {
     Assert(ei.getType() == e.getType());
-    for (const std::pair<const unsigned, Node>& p : d_guq_lit)
+    for (unsigned j = 0, size = d_literals.size(); j < size; j++)
     {
       Trace("cegis-unif-enum") << "...for cand " << e << " adding hd " << ei
-                               << " at size " << p.first << "\n";
-      registerEvalPtAtSize(e, ei, p.second, p.first);
+                               << " at size " << j << "\n";
+      registerEvalPtAtSize(e, ei, d_literals[j], j + 1);
     }
   }
 }
 
-Node CegisUnifEnumManager::getNextDecisionRequest(unsigned& priority)
-{
-  // are we not initialized or have we returned our decision in the current SAT
-  // context?
-  if (!d_initialized || d_ret_dec.get())
-  {
-    return Node::null();
-  }
-  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))
-  {
-    priority = 1;
-    return lit;
-  }
-  else if (!value)
-  {
-    // propagated false, increment
-    incrementNumEnumerators();
-    return getNextDecisionRequest(priority);
-  }
-  d_ret_dec = true;
-  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 Node, StrategyPtInfo>& ci : d_ce_info)
-    {
-      Node c = ci.first;
-      TypeNode ct = c.getType();
-      Node eu = nm->mkSkolem("eu", ct);
-      Node ceu;
-      if (!options::sygusUnifCondIndependent() && !ci.second.d_enums[0].empty())
-      {
-        // make a new conditional enumerator as well, starting the
-        // second type around
-        ceu = nm->mkSkolem("cu", ci.second.d_ce_type);
-      }
-      // register the new enumerators
-      for (unsigned index = 0; index < 2; index++)
-      {
-        Node e = index == 0 ? eu : ceu;
-        if (e.isNull())
-        {
-          continue;
-        }
-        setUpEnumerator(e, ci.second, index);
-      }
-    }
-    // register the evaluation points at the new value
-    for (std::pair<const Node, StrategyPtInfo>& ci : d_ce_info)
-    {
-      Node c = ci.first;
-      for (const Node& ei : ci.second.d_eval_points)
-      {
-        Trace("cegis-unif-enum") << "...increasing enum number for hd " << ei
-                                 << " to new size " << new_size << "\n";
-        registerEvalPtAtSize(c, ei, new_lit, new_size);
-      }
-    }
-    // enforce fairness between number of enumerators and enumerator size
-    if (new_size > 1)
-    {
-      // construct the "virtual enumerator"
-      if (d_virtual_enum.isNull())
-      {
-        // we construct the default integer grammar with no variables, e.g.:
-        //   A -> 0 | 1 | A+A
-        TypeNode intTn = nm->integerType();
-        // use a null variable list
-        Node bvl;
-        std::stringstream ss;
-        ss << "_virtual_enum_grammar";
-        std::string virtualEnumName(ss.str());
-        std::map<TypeNode, std::vector<Node>> extra_cons;
-        std::map<TypeNode, std::vector<Node>> exclude_cons;
-        // do not include "-", which is included by default for integers
-        exclude_cons[intTn].push_back(nm->operatorOf(MINUS));
-        std::unordered_set<Node, NodeHashFunction> term_irrelevant;
-        TypeNode vtn =
-            CegGrammarConstructor::mkSygusDefaultType(intTn,
-                                                      bvl,
-                                                      virtualEnumName,
-                                                      extra_cons,
-                                                      exclude_cons,
-                                                      term_irrelevant);
-        d_virtual_enum = nm->mkSkolem("_ve", vtn);
-        d_tds->registerEnumerator(d_virtual_enum, Node::null(), d_parent);
-      }
-      // if new_size is a power of two, then isPow2 returns log2(new_size)+1
-      // otherwise, this returns 0. In the case it returns 0, we don't care
-      // since the floor( log2( i ) ) = floor( log2( i - 1 ) ) and we do not
-      // increase our size bound.
-      unsigned pow_two = Integer(new_size).isPow2();
-      if (pow_two > 0)
-      {
-        Node size_ve = nm->mkNode(DT_SIZE, d_virtual_enum);
-        Node fair_lemma =
-            nm->mkNode(GEQ, size_ve, nm->mkConst(Rational(pow_two - 1)));
-        fair_lemma = nm->mkNode(OR, new_lit, fair_lemma);
-        Trace("cegis-unif-enum-lemma")
-            << "CegisUnifEnum::lemma, fairness size:" << fair_lemma << "\n";
-        // this lemma relates the number of conditions we enumerate and the
-        // maximum size of a term that is part of our solution. It is of the
-        // form:
-        //   G_uq_i => size(ve) >= log_2( i-1 )
-        // In other words, if we use i conditions, then we allow terms in our
-        // solution whose size is at most log_2(i-1).
-        d_qe->getOutputChannel().lemma(fair_lemma);
-      }
-    }
-  }
-}
-
-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(Node e,
+void CegisUnifEnumDecisionStrategy::registerEvalPtAtSize(Node e,
                                                 Node ei,
                                                 Node guq_lit,
                                                 unsigned n)
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 */
diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h
index 52b6aea0a..e2a9fae80 100644
--- a/src/theory/quantifiers/sygus/sygus_module.h
+++ b/src/theory/quantifiers/sygus/sygus_module.h
@@ -114,14 +114,6 @@ 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();
-  }
   /**
    * Are we trying to repair constants in candidate solutions?
    * If we return true for usingRepairConst is true, then this module has