From e9499c41f405df8b42fd9ae10004b1b91a869106 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Tue, 17 Dec 2019 13:43:44 -0800 Subject: 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. --- src/theory/arith/error_set.h | 27 ++++++++++++++------------- 1 file changed, 14 insertions(+), 13 deletions(-) (limited to 'src/theory/arith/error_set.h') 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 -#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()); -- cgit v1.2.3