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.

5 files changed, 148 insertions, 76 deletions

diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index 3420f282d..40216f7c9 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -85,14 +85,17 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
   if( e==0 ){
     return STATUS_UNFINISHED;
   }else{
-    int peffort = d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT ? 2 : 1;
+    int peffort =
+        d_quantEngine->getInstUserPatMode() == options::UserPatMode::RESORT ? 2
+                                                                            : 1;
     if( e<peffort ){
       return STATUS_UNFINISHED;
     }else if( e==peffort ){
       d_counter[f]++;
 
       Trace("inst-alg") << "-> User-provided instantiate " << f << "..." << std::endl;
-      if( d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT  ){
+      if (d_quantEngine->getInstUserPatMode() == options::UserPatMode::RESORT)
+      {
         for( unsigned i=0; i<d_user_gen_wait[f].size(); i++ ){
           Trigger * t = Trigger::mkTrigger( d_quantEngine, f, d_user_gen_wait[f][i], true, Trigger::TR_RETURN_NULL );
           if( t ){
@@ -142,9 +145,12 @@ void InstStrategyUserPatterns::addUserPattern( Node q, Node pat ){
   if( usable ){
     Trace("user-pat") << "Add user pattern: " << pat << " for " << q << std::endl;
     //check match option
-    if( d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT ){
+    if (d_quantEngine->getInstUserPatMode() == options::UserPatMode::RESORT)
+    {
       d_user_gen_wait[q].push_back( nodes );
-    }else{
+    }
+    else
+    {
       Trigger * t = Trigger::mkTrigger( d_quantEngine, q, nodes, true, Trigger::TR_MAKE_NEW );
       if( t ){
         d_user_gen[q].push_back( t );
@@ -187,11 +193,17 @@ void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort
 }
 
 int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ){
-  UserPatMode upMode = d_quantEngine->getInstUserPatMode();
-  if( hasUserPatterns( f ) && upMode==USER_PAT_MODE_TRUST ){
+  options::UserPatMode upMode = d_quantEngine->getInstUserPatMode();
+  if (hasUserPatterns(f) && upMode == options::UserPatMode::TRUST)
+  {
     return STATUS_UNKNOWN;
-  }else{
-    int peffort = ( hasUserPatterns( f ) && upMode!=USER_PAT_MODE_IGNORE && upMode!=USER_PAT_MODE_RESORT ) ? 2 : 1;
+  }
+  else
+  {
+    int peffort = (hasUserPatterns(f) && upMode != options::UserPatMode::IGNORE
+                   && upMode != options::UserPatMode::RESORT)
+                      ? 2
+                      : 1;
     if( e<peffort ){
       return STATUS_UNFINISHED;
     }else{
@@ -219,17 +231,22 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
       //  d_processed_trigger.clear();
       //  d_quantEngine->getEqualityQuery()->setLiberal( true );
       //}
-      if( options::triggerActiveSelMode()!=TRIGGER_ACTIVE_SEL_ALL ){
+      if (options::triggerActiveSelMode() != options::TriggerActiveSelMode::ALL)
+      {
         int max_score = -1;
         Trigger * max_trigger = NULL;
         for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[0][f].begin(); itt != d_auto_gen_trigger[0][f].end(); ++itt ){
           int score = itt->first->getActiveScore();
-          if( options::triggerActiveSelMode()==TRIGGER_ACTIVE_SEL_MIN ){
+          if (options::triggerActiveSelMode()
+              == options::TriggerActiveSelMode::MIN)
+          {
             if( score>=0 && ( score<max_score || max_score<0 ) ){
               max_score = score;
               max_trigger = itt->first;
-            } 
-          }else{
+            }
+          }
+          else
+          {
             if( score>max_score ){
               max_score = score;
               max_trigger = itt->first;
@@ -241,7 +258,7 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
           d_auto_gen_trigger[0][f][max_trigger] = true;
         }
       }
-      
+
       bool hasInst = false;
       for( unsigned r=0; r<2; r++ ){
         for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[r][f].begin(); itt != d_auto_gen_trigger[r][f].end(); ++itt ){
@@ -374,20 +391,28 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
           }else{
             Assert(Trigger::isAtomicTrigger(pat));
             if( pat.getType().isBoolean() && rpoleq.isNull() ){
-              if( options::literalMatchMode()==LITERAL_MATCH_USE ){
+              if (options::literalMatchMode() == options::LiteralMatchMode::USE)
+              {
                 pat = NodeManager::currentNM()->mkNode( EQUAL, pat, NodeManager::currentNM()->mkConst( rpol==-1 ) ).negate();
-              }else if( options::literalMatchMode()!=LITERAL_MATCH_NONE ){
+              }
+              else if (options::literalMatchMode()
+                       != options::LiteralMatchMode::NONE)
+              {
                 pat = NodeManager::currentNM()->mkNode( EQUAL, pat, NodeManager::currentNM()->mkConst( rpol==1 ) );
               }
             }else{
               Assert(!rpoleq.isNull());
               if( rpol==-1 ){
-                if( options::literalMatchMode()!=LITERAL_MATCH_NONE ){
+                if (options::literalMatchMode()
+                    != options::LiteralMatchMode::NONE)
+                {
                   //all equivalence classes except rpoleq
                   pat = NodeManager::currentNM()->mkNode( EQUAL, pat, rpoleq ).negate();
                 }
               }else if( rpol==1 ){
-                if( options::literalMatchMode()==LITERAL_MATCH_AGG ){
+                if (options::literalMatchMode()
+                    == options::LiteralMatchMode::AGG)
+                {
                   //only equivalence class rpoleq
                   pat = NodeManager::currentNM()->mkNode( EQUAL, pat, rpoleq );
                 }
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
index 1a014939f..052bc910c 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
@@ -54,63 +54,67 @@ public:
   std::string identify() const override { return std::string("UserPatterns"); }
 };/* class InstStrategyUserPatterns */
 
-class InstStrategyAutoGenTriggers : public InstStrategy {
-public:
-  enum {
+class InstStrategyAutoGenTriggers : public InstStrategy
+{
+ public:
+  enum
+  {
     RELEVANCE_NONE,
     RELEVANCE_DEFAULT,
   };
-private:
+
+ private:
   /** trigger generation strategy */
-  TriggerSelMode d_tr_strategy;
+  options::TriggerSelMode d_tr_strategy;
   /** regeneration */
   bool d_regenerate;
   int d_regenerate_frequency;
   /** (single,multi) triggers for each quantifier */
-  std::map< Node, std::map< inst::Trigger*, bool > > d_auto_gen_trigger[2];
-  std::map< Node, int > d_counter;
+  std::map<Node, std::map<inst::Trigger*, bool> > d_auto_gen_trigger[2];
+  std::map<Node, int> d_counter;
   /** single, multi triggers for each quantifier */
-  std::map< Node, std::vector< Node > > d_patTerms[2];
-  std::map< Node, std::map< Node, bool > > d_patReqPol;
+  std::map<Node, std::vector<Node> > d_patTerms[2];
+  std::map<Node, std::map<Node, bool> > d_patReqPol;
   /** information about triggers */
-  std::map< Node, bool > d_is_single_trigger;
-  std::map< Node, bool > d_single_trigger_gen;
-  std::map< Node, bool > d_made_multi_trigger;
-  //processed trigger this round
-  std::map< Node, std::map< inst::Trigger*, bool > > d_processed_trigger;
-  //instantiation no patterns
-  std::map< Node, std::vector< Node > > d_user_no_gen;
+  std::map<Node, bool> d_is_single_trigger;
+  std::map<Node, bool> d_single_trigger_gen;
+  std::map<Node, bool> d_made_multi_trigger;
+  // processed trigger this round
+  std::map<Node, std::map<inst::Trigger*, bool> > d_processed_trigger;
+  // instantiation no patterns
+  std::map<Node, std::vector<Node> > d_user_no_gen;
   // number of trigger variables per quantifier
-  std::map< Node, unsigned > d_num_trigger_vars;
-  std::map< Node, Node > d_vc_partition[2];
-  std::map< Node, Node > d_pat_to_mpat;
-private:
+  std::map<Node, unsigned> d_num_trigger_vars;
+  std::map<Node, Node> d_vc_partition[2];
+  std::map<Node, Node> d_pat_to_mpat;
+
+ private:
   /** process functions */
- void processResetInstantiationRound(Theory::Effort effort) override;
- int process(Node q, Theory::Effort effort, int e) override;
- /** generate triggers */
- void generateTriggers(Node q);
- void addPatternToPool(Node q, Node pat, unsigned num_fv, Node mpat);
- void addTrigger(inst::Trigger* tr, Node f);
- /** has user patterns */
- bool hasUserPatterns(Node q);
- /** has user patterns */
- std::map<Node, bool> d_hasUserPatterns;
+  void processResetInstantiationRound(Theory::Effort effort) override;
+  int process(Node q, Theory::Effort effort, int e) override;
+  /** generate triggers */
+  void generateTriggers(Node q);
+  void addPatternToPool(Node q, Node pat, unsigned num_fv, Node mpat);
+  void addTrigger(inst::Trigger* tr, Node f);
+  /** has user patterns */
+  bool hasUserPatterns(Node q);
+  /** has user patterns */
+  std::map<Node, bool> d_hasUserPatterns;
 
-public:
- InstStrategyAutoGenTriggers(QuantifiersEngine* qe, QuantRelevance* qr);
- ~InstStrategyAutoGenTriggers() {}
+ public:
+  InstStrategyAutoGenTriggers(QuantifiersEngine* qe, QuantRelevance* qr);
+  ~InstStrategyAutoGenTriggers() {}
 
-public:
+ public:
   /** get auto-generated trigger */
-  inst::Trigger* getAutoGenTrigger( Node q );
+  inst::Trigger* getAutoGenTrigger(Node q);
   /** identify */
   std::string identify() const override
   {
     return std::string("AutoGenTriggers");
   }
   /** add pattern */
-  void addUserNoPattern( Node q, Node pat );
+  void addUserNoPattern(Node q, Node pat);
 
  private:
   /**
@@ -118,9 +122,7 @@ public:
    * owned by the instantiation engine that owns this class.
    */
   QuantRelevance* d_quant_rel;
-};/* class InstStrategyAutoGenTriggers */
-
-
+}; /* class InstStrategyAutoGenTriggers */
 }
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index 23b1ff6c9..b91a9ba63 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -46,7 +46,8 @@ InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe)
   if (options::eMatching()) {
     // these are the instantiation strategies for E-matching
     // user-provided patterns
-    if (options::userPatternsQuant() != USER_PAT_MODE_IGNORE) {
+    if (options::userPatternsQuant() != options::UserPatMode::IGNORE)
+    {
       d_isup.reset(new InstStrategyUserPatterns(d_quantEngine));
       d_instStrategies.push_back(d_isup.get());
     }
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index f539bccf5..e177e24a6 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -429,9 +429,19 @@ bool Trigger::isSimpleTrigger( Node n ){
 }
 
 //store triggers in reqPol, indicating their polarity (if any) they must appear to falsify the quantified formula
-void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Node > >& visited, std::map< Node, TriggerTermInfo >& tinfo, 
-                                quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::vector< Node >& added,
-                                bool pol, bool hasPol, bool epol, bool hasEPol, bool knowIsUsable ){
+void Trigger::collectPatTerms2(Node q,
+                               Node n,
+                               std::map<Node, std::vector<Node> >& visited,
+                               std::map<Node, TriggerTermInfo>& tinfo,
+                               options::TriggerSelMode tstrt,
+                               std::vector<Node>& exclude,
+                               std::vector<Node>& added,
+                               bool pol,
+                               bool hasPol,
+                               bool epol,
+                               bool hasEPol,
+                               bool knowIsUsable)
+{
   std::map< Node, std::vector< Node > >::iterator itv = visited.find( n );
   if( itv==visited.end() ){
     visited[ n ].clear();
@@ -488,7 +498,10 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Nod
           Assert(added2[i] != nu);
           // if child was not already removed
           if( tinfo.find( added2[i] )!=tinfo.end() ){
-            if( tstrt==quantifiers::TRIGGER_SEL_MAX || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX && !nu_single ) ){
+            if (tstrt == options::TriggerSelMode::MAX
+                || (tstrt == options::TriggerSelMode::MIN_SINGLE_MAX
+                    && !nu_single))
+            {
               // discard all subterms
               // do not remove if it has smaller weight
               if (tinfo[nu].d_weight <= tinfo[added2[i]].d_weight)
@@ -498,7 +511,9 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Nod
                 visited[added2[i]].clear();
                 tinfo.erase(added2[i]);
               }
-            }else{
+            }
+            else
+            {
               if( tinfo[ nu ].d_fv.size()==tinfo[ added2[i] ].d_fv.size() ){
                 if (tinfo[nu].d_weight >= tinfo[added2[i]].d_weight)
                 {
@@ -516,9 +531,15 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Nod
             }
           }
         }
-        if( rm_nu && ( tstrt==quantifiers::TRIGGER_SEL_MIN || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_ALL && nu_single ) ) ){
+        if (rm_nu
+            && (tstrt == options::TriggerSelMode::MIN
+                || (tstrt == options::TriggerSelMode::MIN_SINGLE_ALL
+                    && nu_single)))
+        {
           tinfo.erase( nu );
-        }else{
+        }
+        else
+        {
           if( std::find( added.begin(), added.end(), nu )==added.end() ){
             added.push_back( nu );
           }
@@ -593,14 +614,21 @@ bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector<
   return true;
 }
 
-void Trigger::collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, 
-                               std::map< Node, TriggerTermInfo >& tinfo, bool filterInst ){
+void Trigger::collectPatTerms(Node q,
+                              Node n,
+                              std::vector<Node>& patTerms,
+                              options::TriggerSelMode tstrt,
+                              std::vector<Node>& exclude,
+                              std::map<Node, TriggerTermInfo>& tinfo,
+                              bool filterInst)
+{
   std::map< Node, std::vector< Node > > visited;
   if( filterInst ){
     //immediately do not consider any term t for which another term is an instance of t
     std::vector< Node > patTerms2;
     std::map< Node, TriggerTermInfo > tinfo2;
-    collectPatTerms( q, n, patTerms2, quantifiers::TRIGGER_SEL_ALL, exclude, tinfo2, false );
+    collectPatTerms(
+        q, n, patTerms2, options::TriggerSelMode::ALL, exclude, tinfo2, false);
     std::vector< Node > temp;
     temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() );
     filterTriggerInstances(temp);
@@ -623,7 +651,8 @@ void Trigger::collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, qu
         Trace("trigger-filter-instance") << std::endl;
       }
     }
-    if( tstrt==quantifiers::TRIGGER_SEL_ALL ){
+    if (tstrt == options::TriggerSelMode::ALL)
+    {
       for( unsigned i=0; i<temp.size(); i++ ){
         //copy information
         tinfo[temp[i]].d_fv.insert( tinfo[temp[i]].d_fv.end(), tinfo2[temp[i]].d_fv.begin(), tinfo2[temp[i]].d_fv.end() );
@@ -632,7 +661,9 @@ void Trigger::collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, qu
         patTerms.push_back( temp[i] );
       }
       return;
-    }else{
+    }
+    else
+    {
       //do not consider terms that have instances
       for( unsigned i=0; i<patTerms2.size(); i++ ){
         if( std::find( temp.begin(), temp.end(), patTerms2[i] )==temp.end() ){
@@ -875,7 +906,7 @@ void Trigger::getTriggerVariables(Node n, Node q, std::vector<Node>& t_vars)
   std::map< Node, TriggerTermInfo > tinfo;
   // collect all patterns from n
   std::vector< Node > exclude;
-  collectPatTerms(q, n, patTerms, quantifiers::TRIGGER_SEL_ALL, exclude, tinfo);
+  collectPatTerms(q, n, patTerms, options::TriggerSelMode::ALL, exclude, tinfo);
   //collect all variables from all patterns in patTerms, add to t_vars
   for (const Node& pat : patTerms)
   {
diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h
index d47ea72ee..e955543db 100644
--- a/src/theory/quantifiers/ematching/trigger.h
+++ b/src/theory/quantifiers/ematching/trigger.h
@@ -273,9 +273,13 @@ class Trigger {
    *     in the vector we are returning, e.g. we do not return f( x ) if we are
    *     also returning f( f( x ) ). TODO: revisit this (issue #1211)
    */
-  static void collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt,
-                               std::vector< Node >& exclude, std::map< Node, TriggerTermInfo >& tinfo,
-                               bool filterInst = false );
+  static void collectPatTerms(Node q,
+                              Node n,
+                              std::vector<Node>& patTerms,
+                              options::TriggerSelMode tstrt,
+                              std::vector<Node>& exclude,
+                              std::map<Node, TriggerTermInfo>& tinfo,
+                              bool filterInst = false);
 
   /** Is n a usable trigger in quantified formula q?
    *
@@ -380,9 +384,18 @@ class Trigger {
    *
    * We add the triggers we collected recursively in n into added.
    */
-  static void collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Node > >& visited, std::map< Node, TriggerTermInfo >& tinfo, 
-                                quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::vector< Node >& added,
-                                bool pol, bool hasPol, bool epol, bool hasEPol, bool knowIsUsable = false );
+  static void collectPatTerms2(Node q,
+                               Node n,
+                               std::map<Node, std::vector<Node> >& visited,
+                               std::map<Node, TriggerTermInfo>& tinfo,
+                               options::TriggerSelMode tstrt,
+                               std::vector<Node>& exclude,
+                               std::vector<Node>& added,
+                               bool pol,
+                               bool hasPol,
+                               bool epol,
+                               bool hasEPol,
+                               bool knowIsUsable = false);
 
   /** filter all nodes that have trigger instances
    *