Make QEffort an enum (#1366)

* Make QEffort an enum.

* Format

* Minor

* Fix

1 files changed, 10 insertions, 17 deletions

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index ffede2a5b..37691488e 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -44,7 +44,11 @@ class InstantiationNotify {
 public:
   InstantiationNotify(){}
   virtual ~InstantiationNotify() {}
-  virtual bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) = 0;
+  virtual bool notifyInstantiation(QuantifiersModule::QEffort quant_e,
+                                   Node q,
+                                   Node lem,
+                                   std::vector<Node>& terms,
+                                   Node body) = 0;
   virtual void filterInstantiations() = 0;
 };
 
@@ -141,8 +145,6 @@ private:
   std::unique_ptr<quantifiers::Skolemize> d_skolemize;
   /** term enumeration utility */
   std::unique_ptr<quantifiers::TermEnumeration> d_term_enum;
-
- private:
   /** instantiation engine */
   quantifiers::InstantiationEngine* d_inst_engine;
   /** model engine */
@@ -174,26 +176,17 @@ private:
   /** quantifiers instantiation propagtor */
   quantifiers::InstPropagator * d_inst_prop;
 
- public:  // effort levels (TODO : make an enum and use everywhere #1293)
-  enum {
-    QEFFORT_CONFLICT,
-    QEFFORT_STANDARD,
-    QEFFORT_MODEL,
-    QEFFORT_LAST_CALL,
-    //none
-    QEFFORT_NONE,
-  };
-private:  //this information is reset during check
-  /** current effort level */
-  unsigned d_curr_effort_level;
+ private:  //this information is reset during check
+    /** current effort level */
+  QuantifiersModule::QEffort d_curr_effort_level;
   /** are we in conflict */
   bool d_conflict;
-  context::CDO< bool > d_conflict_c;
+  context::CDO<bool> d_conflict_c;
   /** has added lemma this round */
   bool d_hasAddedLemma;
   /** whether to use model equality engine */
   bool d_useModelEe;
-private:
+ private:
   /** list of all quantifiers seen */
   std::map< Node, bool > d_quants;
   /** quantifiers reduced */