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.

1 files changed, 14 insertions, 13 deletions

diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h
index 9e3e7c630..5599cd268 100644
--- a/src/theory/arith/error_set.h
+++ b/src/theory/arith/error_set.h
@@ -22,7 +22,7 @@
 
 #include <vector>
 
-#include "options/arith_heuristic_pivot_rule.h"
+#include "options/arith_options.h"
 #include "theory/arith/arithvar.h"
 #include "theory/arith/bound_counts.h"
 #include "theory/arith/callbacks.h"
@@ -69,13 +69,14 @@ class ComparatorPivotRule {
 private:
   const ErrorSet* d_errorSet;
 
-  ErrorSelectionRule d_rule;
-public:
+  options::ErrorSelectionRule d_rule;
+
+ public:
   ComparatorPivotRule();
-  ComparatorPivotRule(const ErrorSet* es, ErrorSelectionRule r);
+  ComparatorPivotRule(const ErrorSet* es, options::ErrorSelectionRule r);
 
   bool operator()(ArithVar v, ArithVar u) const;
-  ErrorSelectionRule getRule() const { return d_rule; }
+  options::ErrorSelectionRule getRule() const { return d_rule; }
 };
 
 // typedef boost::heap::d_ary_heap<
@@ -225,7 +226,7 @@ private:
    */
   ErrorInfoMap d_errInfo;
 
-  ErrorSelectionRule d_selectionRule;
+  options::ErrorSelectionRule d_selectionRule;
   /**
    * The ordered heap for the variables that are in ErrorSet.
    */
@@ -259,12 +260,12 @@ private:
 public:
   DeltaRational computeDiff(ArithVar x) const;
 private:
-  void recomputeAmount(ErrorInformation& ei, ErrorSelectionRule r);
+ void recomputeAmount(ErrorInformation& ei, options::ErrorSelectionRule r);
 
-  void update(ErrorInformation& ei);
-  void transitionVariableOutOfError(ArithVar v);
-  void transitionVariableIntoError(ArithVar v);
-  void addBackIntoFocus(ArithVar v);
+ void update(ErrorInformation& ei);
+ void transitionVariableOutOfError(ArithVar v);
+ void transitionVariableIntoError(ArithVar v);
+ void addBackIntoFocus(ArithVar v);
 
 public:
 
@@ -291,8 +292,8 @@ public:
   void pushErrorInto(ArithVarVec& vec) const;
   void pushFocusInto(ArithVarVec& vec) const;
 
-  ErrorSelectionRule getSelectionRule() const;
-  void setSelectionRule(ErrorSelectionRule rule);
+  options::ErrorSelectionRule getSelectionRule() const;
+  void setSelectionRule(options::ErrorSelectionRule rule);
 
   inline ArithVar topFocusVariable() const{
     Assert(!focusEmpty());