Refactor mode options for Unif+PI (#3531)

6 files changed, 60 insertions, 17 deletions

diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 399a9576c..8da328eb6 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -151,7 +151,7 @@ bool CegisUnif::getEnumValues(const std::vector<Node>& enums,
         // set enums for condition enumerators
         if (index == 1)
         {
-          if (options::sygusUnifCondIndependent())
+          if (usingConditionPool())
           {
             Assert(es.size() == 1);
             // whether valueus exhausted
@@ -228,6 +228,11 @@ bool CegisUnif::getEnumValues(const std::vector<Node>& enums,
   return !addedUnifEnumSymBreakLemma;
 }
 
+bool CegisUnif::usingConditionPool() const
+{
+  return d_sygus_unif.usingConditionPool();
+}
+
 void CegisUnif::setConditions(
     const std::map<Node, std::vector<Node>>& unif_cenums,
     const std::map<Node, std::vector<Node>>& unif_cvalues,
@@ -250,7 +255,7 @@ void CegisUnif::setConditions(
       // d_sygus_unif.setConditions(e, cost_lit, unif_cenums[e],
       // unif_cvalues[e]); if condition enumerator had value and it is being
       // passively generated, exclude this value
-      if (options::sygusUnifCondIndependent() && !itc->second.empty())
+      if (usingConditionPool() && !itc->second.empty())
       {
         Node eu = itc->second[0];
         Assert(d_tds->isEnumerator(eu));
@@ -321,7 +326,7 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums,
     // if condition values are being indepedently enumerated, they should be
     // communicated to the decision tree strategies indepedently of we
     // proceeding to attempt solution building
-    if (options::sygusUnifCondIndependent())
+    if (usingConditionPool())
     {
       setConditions(unif_cenums, unif_cvalues, lems);
     }
@@ -353,7 +358,7 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums,
   }
 
   // TODO tie this to the lemma for getting a new condition value
-  Assert(options::sygusUnifCondIndependent() || !lemmas.empty());
+  Assert(usingConditionPool() || !lemmas.empty());
   for (const Node& lem : lemmas)
   {
     Trace("cegis-unif-lemma")
@@ -400,6 +405,9 @@ CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy(
 {
   d_initialized = false;
   d_tds = d_qe->getTermDatabaseSygus();
+  SygusUnifPiMode mode = options::sygusUnifPi();
+  d_useCondPool =
+      mode == SYGUS_UNIF_PI_CENUM || mode == SYGUS_UNIF_PI_CENUM_IGAIN;
 }
 
 Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n)
@@ -415,7 +423,7 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n)
     TypeNode ct = c.getType();
     Node eu = nm->mkSkolem("eu", ct);
     Node ceu;
-    if (!options::sygusUnifCondIndependent() && !ci.second.d_enums[0].empty())
+    if (!d_useCondPool && !ci.second.d_enums[0].empty())
     {
       // make a new conditional enumerator as well, starting the
       // second type around
@@ -554,7 +562,7 @@ void CegisUnifEnumDecisionStrategy::initialize(
       DecisionManager::STRAT_QUANT_CEGIS_UNIF_NUM_ENUMS, this);
 
   // create single condition enumerator for each decision tree strategy
-  if (options::sygusUnifCondIndependent())
+  if (d_useCondPool)
   {
     // allocate a condition enumerator for each candidate
     for (std::pair<const Node, StrategyPtInfo>& ci : d_ce_info)
@@ -576,7 +584,7 @@ void CegisUnifEnumDecisionStrategy::getEnumeratorsForStrategyPt(
   if (index == 1)
   {
     // we always use (cost-1) conditions, or 1 if in the indepedent case
-    num_enums = !options::sygusUnifCondIndependent() ? num_enums - 1 : 1;
+    num_enums = !d_useCondPool ? num_enums - 1 : 1;
   }
   if (num_enums > 0)
   {
@@ -622,7 +630,7 @@ void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e,
   // if we are using a single independent enumerator for conditions, then we
   // allocate an active guard, and are eligible to use variable-agnostic
   // enumeration.
-  if (options::sygusUnifCondIndependent() && index == 1)
+  if (d_useCondPool && index == 1)
   {
     erole = ROLE_ENUM_POOL;
   }
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index ac859750f..d476d5fb3 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -103,6 +103,11 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf
   TermDbSygus* d_tds;
   /** reference to the parent conjecture */
   SynthConjecture* d_parent;
+  /**
+   * Whether we are using condition pool enumeration (Section 4 of Barbosa et al
+   * FMCAD 2019). This is determined by option::sygusUnifPi().
+   */
+  bool d_useCondPool;
   /** whether this module has been initialized */
   bool d_initialized;
   /** null node */
@@ -294,6 +299,12 @@ class CegisUnif : public Cegis
                      std::map<Node, std::vector<Node>>& unif_cenums,
                      std::map<Node, std::vector<Node>>& unif_cvalues,
                      std::vector<Node>& lems);
+
+  /**
+   * Whether we are using condition pool enumeration (Section 4 of Barbosa et al
+   * FMCAD 2019). This is determined by option::sygusUnifPi().
+   */
+  bool usingConditionPool() const;
   /**
    * Sygus unif utility. This class implements the core algorithm (e.g. decision
    * tree learning) that this module relies upon.
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 5e4513ff3..84b160bb3 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -1187,7 +1187,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       // TODO #1935 ITEs are added to Boolean grammars so that we can infer
       // unification strategies. We can do away with this if we can infer
       // unification strategies from and/or/not
-      if (k == ITE && !options::sygusUnif())
+      if (k == ITE && options::sygusUnifPi() == SYGUS_UNIF_PI_NONE)
       {
         continue;
       }
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index 5d4aaf7ae..1a491394f 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -29,7 +29,10 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-SygusUnifRl::SygusUnifRl(SynthConjecture* p) : d_parent(p) {}
+SygusUnifRl::SygusUnifRl(SynthConjecture* p)
+    : d_parent(p), d_useCondPool(false), d_useCondPoolIGain(false)
+{
+}
 SygusUnifRl::~SygusUnifRl() {}
 void SygusUnifRl::initializeCandidate(
     QuantifiersEngine* qe,
@@ -57,6 +60,11 @@ void SygusUnifRl::initializeCandidate(
     d_cand_to_eval_hds[f].clear();
     d_cand_to_hd_count[f] = 0;
   }
+  // check whether we are using condition enumeration
+  SygusUnifPiMode mode = options::sygusUnifPi();
+  d_useCondPool =
+      mode == SYGUS_UNIF_PI_CENUM || mode == SYGUS_UNIF_PI_CENUM_IGAIN;
+  d_useCondPoolIGain = mode == SYGUS_UNIF_PI_CENUM_IGAIN;
 }
 
 void SygusUnifRl::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
@@ -348,8 +356,7 @@ Node SygusUnifRl::constructSol(
   }
   EnumTypeInfoStrat* etis = snode.d_strats[itd->second.getStrategyIndex()];
   Node sol = itd->second.buildSol(etis->d_cons, lemmas);
-  Assert(options::sygusUnifCondIndependent() || !sol.isNull()
-         || !lemmas.empty());
+  Assert(d_useCondPool || !sol.isNull() || !lemmas.empty());
   return sol;
 }
 
@@ -386,6 +393,11 @@ std::vector<Node> SygusUnifRl::getEvalPointHeads(Node c)
   return it->second;
 }
 
+bool SygusUnifRl::usingConditionPool() const { return d_useCondPool; }
+bool SygusUnifRl::usingConditionPoolInfoGain() const
+{
+  return d_useCondPoolIGain;
+}
 void SygusUnifRl::registerStrategy(
     Node f,
     std::vector<Node>& enums,
@@ -516,7 +528,7 @@ void SygusUnifRl::DecisionTreeInfo::setConditions(
   d_enums.insert(d_enums.end(), enums.begin(), enums.end());
   d_conds.insert(d_conds.end(), conds.begin(), conds.end());
   // add to condition pool
-  if (options::sygusUnifCondIndependent())
+  if (d_unif->usingConditionPool())
   {
     d_cond_mvs.insert(conds.begin(), conds.end());
     if (Trace.isOn("sygus-unif-cond-pool"))
@@ -552,8 +564,8 @@ Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons,
                           << " conditions..." << std::endl;
   // reset the trie
   d_pt_sep.d_trie.clear();
-  return options::sygusUnifCondIndependent() ? buildSolAllCond(cons, lemmas)
-                                             : buildSolMinCond(cons, lemmas);
+  return d_unif->usingConditionPool() ? buildSolAllCond(cons, lemmas)
+                                      : buildSolMinCond(cons, lemmas);
 }
 
 Node SygusUnifRl::DecisionTreeInfo::buildSolAllCond(Node cons,
@@ -840,7 +852,7 @@ Node SygusUnifRl::DecisionTreeInfo::extractSol(Node cons,
                                                std::map<Node, Node>& hd_mv)
 {
   // rebuild decision tree using heuristic learning
-  if (options::sygusUnifBooleanHeuristicDt())
+  if (d_unif->usingConditionPoolInfoGain())
   {
     recomputeSolHeuristically(hd_mv);
   }
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h
index c5b02a481..827919308 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h
@@ -103,9 +103,21 @@ class SygusUnifRl : public SygusUnif
   /** retrieve the head of evaluation points for candidate c, if any */
   std::vector<Node> getEvalPointHeads(Node c);
 
+  /**
+   * Whether we are using condition pool enumeration (Section 4 of Barbosa et al
+   * FMCAD 2019). This is determined by option::sygusUnifPi().
+   */
+  bool usingConditionPool() const;
+  /** Whether we are additionally using information gain.  */
+  bool usingConditionPoolInfoGain() const;
+
  protected:
   /** reference to the parent conjecture */
   SynthConjecture* d_parent;
+  /** Whether we are using condition pool enumeration */
+  bool d_useCondPool;
+  /** Whether we are additionally using information gain heuristics */
+  bool d_useCondPoolIGain;
   /* Functions-to-synthesize (a.k.a. candidates) with unification strategies */
   std::unordered_set<Node, NodeHashFunction> d_unif_candidates;
   /** construct sol */
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index da4275365..c980e5413 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -65,7 +65,7 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe, SynthEngine* p)
   {
     d_modules.push_back(d_ceg_pbe.get());
   }
-  if (options::sygusUnif())
+  if (options::sygusUnifPi() != SYGUS_UNIF_PI_NONE)
   {
     d_modules.push_back(d_ceg_cegisUnif.get());
   }