Minor optimizations to datatypes, revert to checkClash not mod eq. Minor clean up.

1 files changed, 12 insertions, 9 deletions

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 2f399be33..7c71313de 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -137,7 +137,7 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant )
   Trace("qcf-qregister-debug2") << "Register : " << n << std::endl;

   if( n.getKind()==FORALL ){

     registerNode( n[1], hasPol, pol, true );

-  }else{
+  }else{

     if( !MatchGen::isHandledBoolConnective( n ) ){

       if( n.hasBoundVar() ){

         //literals

@@ -147,7 +147,7 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant )
           }

         }else if( MatchGen::isHandledUfTerm( n ) ){

           flatten( n, beneathQuant );

-        }else if( n.getKind()==ITE ){
+        }else if( n.getKind()==ITE ){

           for( unsigned i=1; i<=2; i++ ){

             flatten( n[i], beneathQuant );

           }

@@ -2110,7 +2110,7 @@ void QuantConflictFind::check( Theory::Effort level ) {
         Trace("qcf-debug") << std::endl;

         debugPrint("qcf-debug");

         Trace("qcf-debug") << std::endl;

-      }
+      }

       short end_e = getMaxQcfEffort();

       for( short e = effort_conflict; e<=end_e; e++ ){

         d_effort = e;

@@ -2223,7 +2223,7 @@ void QuantConflictFind::check( Theory::Effort level ) {
                 }

               }else{

                 Trace("qcf-check") << "   ... Spurious instantiation (match is inconsistent)" << std::endl;

-              }
+              }

             }

             if( d_conflict ){

               break;

@@ -2244,7 +2244,9 @@ void QuantConflictFind::check( Theory::Effort level ) {
         }

         Trace("qcf-engine") << std::endl;

         int currEt = d_statistics.d_entailment_checks.getData();

-        Trace("qcf-engine") << "  Entailment checks = " << ( currEt - prevEt ) << std::endl;

+        if( currEt!=prevEt ){

+          Trace("qcf-engine") << "  Entailment checks = " << ( currEt - prevEt ) << std::endl;

+        }

       }

     }

     Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;

@@ -2310,7 +2312,7 @@ void QuantConflictFind::computeRelevantEqr() {
         }

       }else{

         d_eqcs[rtn].push_back( r );

-      }
+      }

       /*

       eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );

       while( !eqc_i.isFinished() ){

@@ -2320,9 +2322,10 @@ void QuantConflictFind::computeRelevantEqr() {
           exit( 199 );

         }

         ++eqc_i;

-      }
-
      */

-
+      }

+

+      */

+

       //if( r.getType().isInteger() ){

       //  Trace("qcf-mv") << "Model value for eqc(" << r << ") : " << d_quantEngine->getValuation().getModelValue( r ) << std::endl;

       //}