Names the Effort enum of QuantConflictFind class. (#1354)

* Changes the Effort level of QuantConflictFind to an enum class. Adding a third value to the enum to indicate not being set. Minor refactoring related to this change. Resolves CID 1172043.

* Fixing a missed assertion. Fixing a few compiler warnings.

* Switching back to an enum from an enum class.

1 files changed, 21 insertions, 8 deletions

diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 0e5fe3c18..8a1043ded 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -17,6 +17,9 @@
 #ifndef QUANT_CONFLICT_FIND
 #define QUANT_CONFLICT_FIND
 
+#include <ostream>
+#include <vector>
+
 #include "context/cdhashmap.h"
 #include "context/cdchunk_list.h"
 #include "theory/quantifiers_engine.h"
@@ -202,7 +205,6 @@ private:
   void setIrrelevantFunction( TNode f );
 private:
   std::map< Node, Node > d_op_node;
-  int d_fid_count;
   std::map< Node, int > d_fid;
   Node mkEqNode( Node a, Node b );
 public:  //for ground terms
@@ -214,14 +216,23 @@ private:
 private:  //for equivalence classes
   // type -> list(eqc)
   std::map< TypeNode, std::vector< TNode > > d_eqcs;
-public:
-  enum {
-    effort_conflict,
-    effort_prop_eq,
+
+ public:
+  enum Effort : unsigned {
+    EFFORT_CONFLICT,
+    EFFORT_PROP_EQ,
+    EFFORT_INVALID,
   };
-  short d_effort;
-  void setEffort( int e ) { d_effort = e; }
-  static short getMaxQcfEffort();
+  void setEffort(Effort e) { d_effort = e; }
+
+  inline bool atConflictEffort() const {
+    return d_effort == QuantConflictFind::EFFORT_CONFLICT;
+  }
+
+ private:
+  Effort d_effort;
+
+ public:
   bool areMatchEqual( TNode n1, TNode n2 );
   bool areMatchDisequal( TNode n1, TNode n2 );
 public:
@@ -270,6 +281,8 @@ public:
   std::string identify() const { return "QcfEngine"; }
 };
 
+std::ostream& operator<<(std::ostream& os, const QuantConflictFind::Effort& e);
+
 } /* namespace CVC4::theory::quantifiers */
 } /* namespace CVC4::theory */
 } /* namespace CVC4 */