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, 65 insertions, 33 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 */