Generate code for options with modes. (#3561)

This commit adds support for code generation of options with modes (enums). From now on option enums can be specified in the corresponding *.toml files without the need of extra code. All option enums are now in the options namespace.

7 files changed, 62 insertions, 46 deletions

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 69e0ef70a..e36047e67 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -109,7 +109,7 @@ void CegSingleInv::initialize(Node q)
   {
     // We are fully single invocation, set single invocation if we haven't
     // disabled single invocation techniques.
-    if (options::cegqiSingleInvMode() != CEGQI_SI_MODE_NONE)
+    if (options::cegqiSingleInvMode() != options::CegqiSingleInvMode::NONE)
     {
       d_single_invocation = true;
       return;
@@ -118,25 +118,25 @@ void CegSingleInv::initialize(Node q)
   // We are processing without single invocation techniques, now check if
   // we should fix an invariant template (post-condition strengthening or
   // pre-condition weakening).
-  SygusInvTemplMode tmode = options::sygusInvTemplMode();
-  if (tmode != SYGUS_INV_TEMPL_MODE_NONE)
+  options::SygusInvTemplMode tmode = options::sygusInvTemplMode();
+  if (tmode != options::SygusInvTemplMode::NONE)
   {
     // currently only works for single predicate synthesis
     if (q[0].getNumChildren() > 1 || !q[0][0].getType().isPredicate())
     {
-      tmode = SYGUS_INV_TEMPL_MODE_NONE;
+      tmode = options::SygusInvTemplMode::NONE;
     }
     else if (!options::sygusInvTemplWhenSyntax())
     {
       // only use invariant templates if no syntactic restrictions
       if (CegGrammarConstructor::hasSyntaxRestrictions(q))
       {
-        tmode = SYGUS_INV_TEMPL_MODE_NONE;
+        tmode = options::SygusInvTemplMode::NONE;
       }
     }
   }
 
-  if (tmode == SYGUS_INV_TEMPL_MODE_NONE)
+  if (tmode == options::SygusInvTemplMode::NONE)
   {
     // not processing invariant templates
     return;
@@ -243,13 +243,13 @@ void CegSingleInv::initialize(Node q)
                      << std::endl;
   if (templ.isNull())
   {
-    if (tmode == SYGUS_INV_TEMPL_MODE_PRE)
+    if (tmode == options::SygusInvTemplMode::PRE)
     {
       templ = nm->mkNode(OR, d_trans_pre[prog], d_templ_arg[prog]);
     }
     else
     {
-      Assert(tmode == SYGUS_INV_TEMPL_MODE_POST);
+      Assert(tmode == options::SygusInvTemplMode::POST);
       templ = nm->mkNode(AND, d_trans_post[prog], d_templ_arg[prog]);
     }
   }
@@ -269,8 +269,11 @@ void CegSingleInv::initialize(Node q)
 void CegSingleInv::finishInit(bool syntaxRestricted)
 {
   Trace("cegqi-si-debug") << "Single invocation: finish init" << std::endl;
-  // do not do single invocation if grammar is restricted and CEGQI_SI_MODE_ALL is not enabled
-  if( options::cegqiSingleInvMode()==CEGQI_SI_MODE_USE && d_single_invocation && syntaxRestricted ){
+  // do not do single invocation if grammar is restricted and
+  // options::CegqiSingleInvMode::ALL is not enabled
+  if (options::cegqiSingleInvMode() == options::CegqiSingleInvMode::USE
+      && d_single_invocation && syntaxRestricted)
+  {
     d_single_invocation = false;
     Trace("cegqi-si") << "...grammar is restricted, do not use single invocation techniques." << std::endl;
   }
@@ -551,17 +554,19 @@ Node CegSingleInv::reconstructToSyntax(Node s,
 
   //reconstruct the solution into sygus if necessary
   reconstructed = 0;
-  if (options::cegqiSingleInvReconstruct() != CEGQI_SI_RCONS_MODE_NONE
+  if (options::cegqiSingleInvReconstruct()
+          != options::CegqiSingleInvRconsMode::NONE
       && !dt.getSygusAllowAll() && !stn.isNull() && rconsSygus)
   {
     d_sol->preregisterConjecture( d_orig_conjecture );
     int enumLimit = -1;
-    if (options::cegqiSingleInvReconstruct() == CEGQI_SI_RCONS_MODE_TRY)
+    if (options::cegqiSingleInvReconstruct()
+        == options::CegqiSingleInvRconsMode::TRY)
     {
       enumLimit = 0;
     }
     else if (options::cegqiSingleInvReconstruct()
-             == CEGQI_SI_RCONS_MODE_ALL_LIMIT)
+             == options::CegqiSingleInvRconsMode::ALL_LIMIT)
     {
       enumLimit = options::cegqiSingleInvReconstructLimit();
     }
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index a4dc241b8..78ea5b22f 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -52,7 +52,7 @@ bool Cegis::initialize(Node conj,
   }
 
   // assign the cegis sampler if applicable
-  if (options::cegisSample() != CEGIS_SAMPLE_NONE)
+  if (options::cegisSample() != options::CegisSampleMode::NONE)
   {
     Trace("cegis-sample") << "Initialize sampler for " << d_base_body << "..."
                           << std::endl;
@@ -81,7 +81,8 @@ bool Cegis::processInitialize(Node conj,
     // grammar construction was not simple.
     bool useSymCons = false;
     if (options::sygusRepairConst()
-        || options::sygusGrammarConsMode() != SYGUS_GCONS_SIMPLE)
+        || options::sygusGrammarConsMode()
+               != options::SygusGrammarConsMode::SIMPLE)
     {
       TypeNode ctn = candidates[i].getType();
       d_tds->registerSygusType(ctn);
@@ -305,7 +306,7 @@ bool Cegis::constructCandidates(const std::vector<Node>& enums,
     return false;
   }
 
-  if (options::cegisSample() != CEGIS_SAMPLE_NONE && lems.empty())
+  if (options::cegisSample() != options::CegisSampleMode::NONE && lems.empty())
   {
     // if we didn't add a lemma, trying sampling to add a refinement lemma
     // that immediately refutes the candidate we just constructed
@@ -636,7 +637,7 @@ bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates,
           Trace("cegqi-engine") << "  *** Refine by sampling" << std::endl;
           addRefinementLemma(rlem);
           // if trust, we are not interested in sending out refinement lemmas
-          if (options::cegisSample() != CEGIS_SAMPLE_TRUST)
+          if (options::cegisSample() != options::CegisSampleMode::TRUST)
           {
             Node lem = nm->mkNode(OR, d_parent->getGuard().negate(), rlem);
             lems.push_back(lem);
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 2bc412361..8812032ba 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -405,9 +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;
+  options::SygusUnifPiMode mode = options::sygusUnifPi();
+  d_useCondPool = mode == options::SygusUnifPiMode::CENUM
+                  || mode == options::SygusUnifPiMode::CENUM_IGAIN;
 }
 
 Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n)
@@ -639,7 +639,8 @@ void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e,
   }
   Trace("cegis-unif-enum") << "* Registering new enumerator " << e
                            << " to strategy point " << si.d_pt << "\n";
-  bool useSymCons = options::sygusGrammarConsMode() != SYGUS_GCONS_SIMPLE;
+  bool useSymCons =
+      options::sygusGrammarConsMode() != options::SygusGrammarConsMode::SIMPLE;
   d_tds->registerEnumerator(e, si.d_pt, d_parent, erole, useSymCons);
 }
 
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 8c005bd3c..78fbc48f3 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -538,7 +538,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       itc;
   // maps types to the index of its "any term" grammar construction
   std::map<TypeNode, unsigned> typeToGAnyTerm;
-  SygusGrammarConsMode sgcm = options::sygusGrammarConsMode();
+  options::SygusGrammarConsMode sgcm = options::sygusGrammarConsMode();
   for (unsigned i = 0, size = types.size(); i < size; ++i)
   {
     std::stringstream ss;
@@ -571,15 +571,16 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
   {
     Trace("sygus-grammar-def") << "Make grammar for " << types[i] << " " << unres_types[i] << std::endl;
     TypeNode unres_t = unres_types[i];
-    SygusGrammarConsMode tsgcm = sgcm;
-    if (tsgcm == SYGUS_GCONS_ANY_TERM || tsgcm == SYGUS_GCONS_ANY_TERM_CONCISE)
+    options::SygusGrammarConsMode tsgcm = sgcm;
+    if (tsgcm == options::SygusGrammarConsMode::ANY_TERM
+        || tsgcm == options::SygusGrammarConsMode::ANY_TERM_CONCISE)
     {
       // If the type does not support any term, we do any constant instead.
       // We also fall back on any constant construction if the type has no
       // constructors at this point (e.g. it simply encodes all constants).
       if (!types[i].isReal())
       {
-        tsgcm = SYGUS_GCONS_ANY_CONST;
+        tsgcm = options::SygusGrammarConsMode::ANY_CONST;
       }
       else
       {
@@ -629,7 +630,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     //add constants
     std::vector<Node> consts;
     mkSygusConstantsForType(types[i], consts);
-    if (tsgcm == SYGUS_GCONS_ANY_CONST)
+    if (tsgcm == options::SygusGrammarConsMode::ANY_CONST)
     {
       // Use the any constant constructor. Notice that for types that don't
       // have constants (e.g. uninterpreted or function types), we don't add
@@ -923,7 +924,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     // the references).
     const SygusDatatype& sdti = sdts[i].d_sdt;
     // whether we will use the polynomial grammar
-    bool polynomialGrammar = sgcm == SYGUS_GCONS_ANY_TERM_CONCISE;
+    bool polynomialGrammar =
+        sgcm == options::SygusGrammarConsMode::ANY_TERM_CONCISE;
     // A set of constructor indices that will be used in the overall sum we
     // are constructing; indices of constructors corresponding to builtin
     // arithmetic operators will be excluded from this set.
@@ -1198,7 +1200,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::sygusUnifPi() == SYGUS_UNIF_PI_NONE)
+      if (k == ITE && options::sygusUnifPi() == options::SygusUnifPiMode::NONE)
       {
         continue;
       }
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index 47975d4b7..2b85595cd 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -61,10 +61,10 @@ void SygusUnifRl::initializeCandidate(
     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;
+  options::SygusUnifPiMode mode = options::sygusUnifPi();
+  d_useCondPool = mode == options::SygusUnifPiMode::CENUM
+                  || mode == options::SygusUnifPiMode::CENUM_IGAIN;
+  d_useCondPoolIGain = mode == options::SygusUnifPiMode::CENUM_IGAIN;
 }
 
 void SygusUnifRl::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index e30f9771c..03449589b 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -66,7 +66,7 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe, SynthEngine* p)
   {
     d_modules.push_back(d_ceg_pbe.get());
   }
-  if (options::sygusUnifPi() != SYGUS_UNIF_PI_NONE)
+  if (options::sygusUnifPi() != options::SygusUnifPiMode::NONE)
   {
     d_modules.push_back(d_ceg_cegisUnif.get());
   }
@@ -483,7 +483,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
   bool sk_refine = (!isGround() || d_refine_count == 0) && constructed_cand;
   if (sk_refine)
   {
-    if (options::cegisSample() == CEGIS_SAMPLE_TRUST)
+    if (options::cegisSample() == options::CegisSampleMode::TRUST)
     {
       // we have that the current candidate passed a sample test
       // since we trust sampling in this mode, we assert there is no
@@ -799,14 +799,17 @@ Node SynthConjecture::getEnumeratedValue(Node e, bool& activeIncomplete)
       // or basic. The auto mode always prefers the optimized enumerator over
       // the basic one.
       Assert(d_tds->isBasicEnumerator(e));
-      if (options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_ENUM_BASIC)
+      if (options::sygusActiveGenMode()
+          == options::SygusActiveGenMode::ENUM_BASIC)
       {
         d_evg[e].reset(new EnumValGeneratorBasic(d_tds, e.getType()));
       }
       else
       {
-        Assert(options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_ENUM
-               || options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_AUTO);
+        Assert(options::sygusActiveGenMode()
+                   == options::SygusActiveGenMode::ENUM
+               || options::sygusActiveGenMode()
+                      == options::SygusActiveGenMode::AUTO);
         d_evg[e].reset(new SygusEnumerator(d_tds, this));
       }
     }
@@ -1061,7 +1064,8 @@ void SynthConjecture::printSynthSolution(std::ostream& out)
 
       if (status != 0
           && (options::sygusRewSynth() || options::sygusQueryGen()
-              || options::sygusFilterSolMode() != SYGUS_FILTER_SOL_NONE))
+              || options::sygusFilterSolMode()
+                     != options::SygusFilterSolMode::NONE))
       {
         Trace("cegqi-sol-debug") << "Run expression mining..." << std::endl;
         std::map<Node, ExpressionMinerManager>::iterator its =
@@ -1078,13 +1082,16 @@ void SynthConjecture::printSynthSolution(std::ostream& out)
           {
             d_exprm[prog].enableQueryGeneration(options::sygusQueryGenThresh());
           }
-          if (options::sygusFilterSolMode() != SYGUS_FILTER_SOL_NONE)
+          if (options::sygusFilterSolMode()
+              != options::SygusFilterSolMode::NONE)
           {
-            if (options::sygusFilterSolMode() == SYGUS_FILTER_SOL_STRONG)
+            if (options::sygusFilterSolMode()
+                == options::SygusFilterSolMode::STRONG)
             {
               d_exprm[prog].enableFilterStrongSolutions();
             }
-            else if (options::sygusFilterSolMode() == SYGUS_FILTER_SOL_WEAK)
+            else if (options::sygusFilterSolMode()
+                     == options::SygusFilterSolMode::WEAK)
             {
               d_exprm[prog].enableFilterWeakSolutions();
             }
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 0279ca531..1fda55172 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -453,7 +453,7 @@ void TermDbSygus::registerEnumerator(Node e,
 
   // determine if we are actively-generated
   bool isActiveGen = false;
-  if (options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE)
+  if (options::sygusActiveGenMode() != options::SygusActiveGenMode::NONE)
   {
     if (erole == ROLE_ENUM_MULTI_SOLUTION || erole == ROLE_ENUM_CONSTRAINED)
     {
@@ -481,7 +481,7 @@ void TermDbSygus::registerEnumerator(Node e,
     {
       // If the enumerator is the single function-to-synthesize, if auto is
       // enabled, we infer whether it is better to enable active generation.
-      if (options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_AUTO)
+      if (options::sygusActiveGenMode() == options::SygusActiveGenMode::AUTO)
       {
         // We use active generation if the grammar of the enumerator does not
         // have ITE and is not Boolean. Experimentally, it is better to
@@ -513,9 +513,9 @@ void TermDbSygus::registerEnumerator(Node e,
                     << " returned " << isActiveGen << std::endl;
   // Currently, actively-generated enumerators are either basic or variable
   // agnostic.
-  bool isVarAgnostic =
-      isActiveGen
-      && options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_VAR_AGNOSTIC;
+  bool isVarAgnostic = isActiveGen
+                       && options::sygusActiveGenMode()
+                              == options::SygusActiveGenMode::VAR_AGNOSTIC;
   d_enum_var_agnostic[e] = isVarAgnostic;
   if (isVarAgnostic)
   {