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.

6 files changed, 90 insertions, 46 deletions

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index baf499d67..442e3b230 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -560,7 +560,7 @@ bool QuantInfo::isMatchSpurious( QuantConflictFind * p ) {
   for( int i=0; i<getNumVars(); i++ ){
     //std::map< int, TNode >::iterator it = d_match.find( i );
     if( !d_match[i].isNull() ){
-      if( !getCurrentCanBeEqual( p, i, d_match[i], p->d_effort==QuantConflictFind::effort_conflict ) ){
+      if (!getCurrentCanBeEqual(p, i, d_match[i], p->atConflictEffort())) {
         return true;
       }
     }
@@ -571,7 +571,7 @@ bool QuantInfo::isMatchSpurious( QuantConflictFind * p ) {
 bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node >& terms ) {
   if( options::qcfEagerTest() ){
     //check whether the instantiation evaluates as expected
-    if( p->d_effort==QuantConflictFind::effort_conflict ){
+    if (p->atConflictEffort()) {
       Trace("qcf-instance-check") << "Possible conflict instance for " << d_q << " : " << std::endl;
       std::map< TNode, TNode > subs;
       for( unsigned i=0; i<terms.size(); i++ ){
@@ -612,7 +612,7 @@ bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node
       Node cons =
           p->getTermUtil()->substituteBoundVariables(it->first, d_q, terms);
       cons = it->second ? cons : cons.negate();
-      if( !entailmentTest( p, cons, p->d_effort==QuantConflictFind::effort_conflict ) ){
+      if (!entailmentTest(p, cons, p->atConflictEffort())) {
         return true;
       }
     }
@@ -721,7 +721,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
               if( slv_v==-1 ){
                 Trace("qcf-tconstraint-debug") << "...will solve for var #" << vn << std::endl;
                 slv_v = vn;
-                if( p->d_effort!=QuantConflictFind::effort_conflict ){
+                if (!p->atConflictEffort()) {
                   break;
                 }
               }else{
@@ -758,7 +758,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
             if( v==d_vars[index] ){
               sum = lhs;
             }else{
-              if( p->d_effort==QuantConflictFind::effort_conflict ){
+              if (p->atConflictEffort()) {
                 Kind kn = k;
                 if( d_vars[index].getKind()==PLUS ){
                   kn = MINUS;
@@ -1334,7 +1334,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
       if( d_tgt ){
         success = p->areMatchEqual( nn[0], nn[1] );
       }else{
-        if( p->d_effort==QuantConflictFind::effort_conflict ){
+        if (p->atConflictEffort()) {
           success = p->areDisequal( nn[0], nn[1] );
         }else{
           success = p->areMatchDisequal( nn[0], nn[1] );
@@ -1377,7 +1377,8 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
     }else{
       if( d_tgt && d_n.getKind()==FORALL ){
         //fail
-      }else if( d_n.getKind()==FORALL && p->d_effort==QuantConflictFind::effort_conflict && !options::qcfNestedConflict() ){
+      } else if (d_n.getKind() == FORALL && p->atConflictEffort() &&
+                 !options::qcfNestedConflict()) {
         //fail
       }else{
         //reset the first child to d_tgt
@@ -1898,14 +1899,13 @@ bool MatchGen::isHandled( TNode n ) {
   return true;
 }
 
-
-QuantConflictFind::QuantConflictFind( QuantifiersEngine * qe, context::Context* c ) :
-QuantifiersModule( qe ),
-d_conflict( c, false ) {
-  d_fid_count = 0;
-  d_true = NodeManager::currentNM()->mkConst<bool>(true);
-  d_false = NodeManager::currentNM()->mkConst<bool>(false);
-}
+QuantConflictFind::QuantConflictFind(QuantifiersEngine* qe, context::Context* c)
+    : QuantifiersModule(qe),
+      d_conflict(c, false),
+      d_true(NodeManager::currentNM()->mkConst<bool>(true)),
+      d_false(NodeManager::currentNM()->mkConst<bool>(false)),
+      d_effort(EFFORT_INVALID),
+      d_needs_computeRelEqr() {}
 
 Node QuantConflictFind::mkEqNode( Node a, Node b ) {
   return a.eqNode( b );
@@ -1945,16 +1945,6 @@ void QuantConflictFind::registerQuantifier( Node q ) {
   }
 }
 
-short QuantConflictFind::getMaxQcfEffort() {
-  if( options::qcfMode()==QCF_CONFLICT_ONLY ){
-    return effort_conflict;
-  }else if( options::qcfMode()==QCF_PROP_EQ || options::qcfMode()==QCF_PARTIAL ){
-    return effort_prop_eq;
-  }else{
-    return 0;
-  }
-}
-
 bool QuantConflictFind::areMatchEqual( TNode n1, TNode n2 ) {
   //if( d_effort==QuantConflictFind::effort_mc ){
   //  return n1==n2 || !areDisequal( n1, n2 );
@@ -1964,7 +1954,7 @@ bool QuantConflictFind::areMatchEqual( TNode n1, TNode n2 ) {
 }
 
 bool QuantConflictFind::areMatchDisequal( TNode n1, TNode n2 ) {
-  //if( d_effort==QuantConflictFind::effort_conflict ){
+  // if( d_effort==QuantConflictFind::Effort::Conflict ){
   //  return areDisequal( n1, n2 );
   //}else{
   return n1!=n2;
@@ -2030,6 +2020,29 @@ void QuantConflictFind::setIrrelevantFunction( TNode f ) {
   }
 }
 
+namespace {
+
+// Returns the beginning of a range of efforts. The range can be iterated
+// through as unsigned using operator++.
+inline QuantConflictFind::Effort QcfEffortStart() {
+  return QuantConflictFind::EFFORT_CONFLICT;
+}
+
+// Returns the beginning of a range of efforts. The value returned is included
+// in the range.
+inline QuantConflictFind::Effort QcfEffortEnd() {
+  switch (options::qcfMode()) {
+    case QCF_PROP_EQ:
+    case QCF_PARTIAL:
+      return QuantConflictFind::EFFORT_PROP_EQ;
+    case QCF_CONFLICT_ONLY:
+    default:
+      return QuantConflictFind::EFFORT_PROP_EQ;
+  }
+}
+
+}  // namespace
+
 /** check */
 void QuantConflictFind::check(Theory::Effort level, QEffort quant_e)
 {
@@ -2063,10 +2076,9 @@ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e)
         debugPrint("qcf-debug");
         Trace("qcf-debug") << std::endl;
       }
-      short end_e = getMaxQcfEffort();
       bool isConflict = false;
-      for( short e = effort_conflict; e<=end_e; e++ ){
-        d_effort = e;
+      for (unsigned e = QcfEffortStart(), end = QcfEffortEnd(); e <= end; ++e) {
+        d_effort = static_cast<Effort>(e);
         Trace("qcf-check") << "Checking quantified formulas at effort " << e << "..." << std::endl;
         for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
           Node q = d_quantEngine->getModel()->getAssertedQuantifier( i, true );
@@ -2104,7 +2116,8 @@ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e)
                             Node inst = d_quantEngine->getInstantiation( q, terms );
                             Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;
                             Assert( !getTermDatabase()->isEntailed( inst, true ) );
-                            Assert( getTermDatabase()->isEntailed( inst, false ) || e>effort_conflict );
+                            Assert(getTermDatabase()->isEntailed(inst, false) ||
+                                   e > EFFORT_CONFLICT);
                           }
                           if( d_quantEngine->addInstantiation( q, terms ) ){
                             Trace("qcf-check") << "   ... Added instantiation" << std::endl;
@@ -2112,7 +2125,7 @@ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e)
                             qi->debugPrintMatch("qcf-inst");
                             Trace("qcf-inst") << std::endl;
                             ++addedLemmas;
-                            if( e==effort_conflict ){
+                            if (e == EFFORT_CONFLICT) {
                               d_quantEngine->markRelevant( q );
                               ++(d_quantEngine->d_statistics.d_instantiations_qcf);
                               if( options::qcfAllConflict() ){
@@ -2121,7 +2134,7 @@ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e)
                                 d_conflict.set( true );
                               }
                               break;
-                            }else if( e==effort_prop_eq ){
+                            } else if (e == EFFORT_PROP_EQ) {
                               d_quantEngine->markRelevant( q );
                               ++(d_quantEngine->d_statistics.d_instantiations_qcf);
                             }
@@ -2164,7 +2177,11 @@ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e)
         double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
         Trace("qcf-engine") << "Finished conflict find engine, time = " << (clSet2-clSet);
         if( addedLemmas>0 ){
-          Trace("qcf-engine") << ", effort = " << ( d_effort==effort_conflict ? "conflict" : ( d_effort==effort_prop_eq ? "prop_eq" : "mc" ) );
+          Trace("qcf-engine")
+              << ", effort = "
+              << (d_effort == EFFORT_CONFLICT
+                      ? "conflict"
+                      : (d_effort == EFFORT_PROP_EQ ? "prop_eq" : "mc"));
           Trace("qcf-engine") << ", addedLemmas = " << addedLemmas;
         }
         Trace("qcf-engine") << std::endl;
@@ -2276,6 +2293,21 @@ TNode QuantConflictFind::getZero( Kind k ) {
   }
 }
 
+std::ostream& operator<<(std::ostream& os, const QuantConflictFind::Effort& e) {
+  switch (e) {
+    case QuantConflictFind::EFFORT_INVALID:
+      os << "Invalid";
+      break;
+    case QuantConflictFind::EFFORT_CONFLICT:
+      os << "Conflict";
+      break;
+    case QuantConflictFind::EFFORT_PROP_EQ:
+      os << "PropEq";
+      break;
+  }
+  return os;
+}
+
 } /* namespace CVC4::theory::quantifiers */
 } /* namespace CVC4::theory */
 } /* namespace CVC4 */
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 */
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index d1f819726..b179110e7 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -26,7 +26,7 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-class QAttributes;
+struct QAttributes;
 
 class QuantifiersRewriter {
 private:
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index 2c85bceb8..337d61976 100644
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -119,7 +119,7 @@ int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) {
   if( qcf ){
     //reset QCF module
     qcf->computeRelevantEqr();
-    qcf->setEffort( QuantConflictFind::effort_conflict );
+    qcf->setEffort(QuantConflictFind::EFFORT_CONFLICT);
     //get the proper quantifiers info
     std::map< Node, QuantInfo >::iterator it = d_qinfo.find( f );
     if( it!=d_qinfo.end() ){
diff --git a/src/theory/quantifiers/sygus_process_conj.cpp b/src/theory/quantifiers/sygus_process_conj.cpp
index 06ce99007..4c0e992e0 100644
--- a/src/theory/quantifiers/sygus_process_conj.cpp
+++ b/src/theory/quantifiers/sygus_process_conj.cpp
@@ -519,7 +519,7 @@ void CegConjectureProcessFun::getIrrelevantArgs(
   }
 }
 
-CegConjectureProcess::CegConjectureProcess(QuantifiersEngine* qe) : d_qe(qe) {}
+CegConjectureProcess::CegConjectureProcess(QuantifiersEngine* qe) {}
 CegConjectureProcess::~CegConjectureProcess() {}
 Node CegConjectureProcess::preSimplify(Node q)
 {
diff --git a/src/theory/quantifiers/sygus_process_conj.h b/src/theory/quantifiers/sygus_process_conj.h
index f5966c55f..0b9a25532 100644
--- a/src/theory/quantifiers/sygus_process_conj.h
+++ b/src/theory/quantifiers/sygus_process_conj.h
@@ -353,8 +353,7 @@ class CegConjectureProcess
                          NodeHashFunction>& free_vars);
   /** for each synth-fun, information that is specific to this conjecture */
   std::map<Node, CegConjectureProcessFun> d_sf_info;
-  /** reference to quantifier engine */
-  QuantifiersEngine* d_qe;
+
   /** get component vector */
   void getComponentVector(Kind k, Node n, std::vector<Node>& args);
 };