Minor fixes post-merge of RR.

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 79948a063fc40b78995211fed53cb00318a24da4..51d69ace4b2a483f2b7ed9448507229177fa40a1 100755 (executable)
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -95,7 +95,7 @@ void QuantInfo::initialize( Node q, Node qn ) {
       if( d_vars[j].getKind()!=BOUND_VARIABLE ){\r
         bool beneathQuant = d_nbeneathQuant.find( d_vars[j] )==d_nbeneathQuant.end();\r
         d_var_mg[j] = new MatchGen( this, d_vars[j], true, beneathQuant );\r
-        if( !d_var_mg[j]->isValid() && options::qcfMode()<QCF_PARTIAL ){\r
+        if( !d_var_mg[j]->isValid() ){\r
           d_mg->setInvalid();\r
           break;\r
         }else{\r
@@ -669,7 +669,7 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){
           Node nn = n.eqNode( n[i] );\r
           d_children.push_back( MatchGen( qi, nn ) );\r
           d_children[d_children.size()-1].d_qni_bound_except.push_back( 0 );\r
-          if( !d_children[d_children.size()-1].isValid() && options::qcfMode()<QCF_PARTIAL ){\r
+          if( !d_children[d_children.size()-1].isValid() ){\r
             setInvalid();\r
             break;\r
           }\r
@@ -697,7 +697,7 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){
         for( unsigned i=0; i<d_n.getNumChildren(); i++ ){\r
           if( d_n.getKind()!=FORALL || i==1 ){\r
             d_children.push_back( MatchGen( qi, d_n[i], false, nBeneathQuant ) );\r
-            if( !d_children[d_children.size()-1].isValid() && options::qcfMode()<QCF_PARTIAL ){\r
+            if( !d_children[d_children.size()-1].isValid() ){\r
               setInvalid();\r
               break;\r
             }\r
@@ -900,9 +900,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
 \r
   //set up processing matches\r
   if( d_type==typ_invalid ){\r
-    if( p->d_effort==QuantConflictFind::effort_partial ){\r
-      d_child_counter = 0;\r
-    }\r
+    //do nothing : return success once?\r
   }else if( d_type==typ_ground ){\r
     if( d_ground_eval[0]==( d_tgt ? p->d_true : p->d_false ) ){\r
       d_child_counter = 0;\r
@@ -1008,10 +1006,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
       d_qn.push_back( NULL );\r
     }else{\r
       if( d_tgt && d_n.getKind()==FORALL ){\r
-        //return success once\r
-        if( p->d_effort==QuantConflictFind::effort_partial ){\r
-          d_child_counter = -2;\r
-        }\r
+        //do nothing\r
       }else{\r
         //reset the first child to d_tgt\r
         d_child_counter = 0;\r
@@ -1651,8 +1646,6 @@ short QuantConflictFind::getMaxQcfEffort() {
     return effort_conflict;\r
   }else if( options::qcfMode()==QCF_PROP_EQ ){\r
     return effort_prop_eq;\r
-  }else if( options::qcfMode()==QCF_PARTIAL ){\r
-    return effort_partial;\r
   }else if( options::qcfMode()==QCF_MC ){\r
     return effort_mc;\r
   }else{\r
@@ -1906,8 +1899,6 @@ void QuantConflictFind::check( Theory::Effort level ) {
         }\r
       }\r
 \r
-\r
-\r
       if( Trace.isOn("qcf-debug") ){\r
         Trace("qcf-debug") << std::endl;\r
         debugPrint("qcf-debug");\r
@@ -2035,7 +2026,7 @@ void QuantConflictFind::check( Theory::Effort level ) {
         double clSet2 = double(clock())/double(CLOCKS_PER_SEC);\r
         Trace("qcf-engine") << "Finished conflict find engine, time = " << (clSet2-clSet);\r
         if( addedLemmas>0 ){\r
-          Trace("qcf-engine") << ", effort = " << ( d_effort==effort_conflict ? "conflict" : ( d_effort==effort_prop_eq ? "prop_eq" : (d_effort==effort_partial ? "partial" : "mc" ) ) );\r
+          Trace("qcf-engine") << ", effort = " << ( d_effort==effort_conflict ? "conflict" : ( d_effort==effort_prop_eq ? "prop_eq" : "mc" ) );\r
           Trace("qcf-engine") << ", addedLemmas = " << addedLemmas;\r
         }\r
         Trace("qcf-engine") << std::endl;\r
@@ -2105,6 +2096,7 @@ void QuantConflictFind::computeRelevantEqr() {
       }else{\r
         d_eqcs[rtn].push_back( r );\r
       }
+      /*\r
       eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );\r
       while( !eqc_i.isFinished() ){\r
         TNode n = (*eqc_i);\r
@@ -2114,7 +2106,8 @@ void QuantConflictFind::computeRelevantEqr() {
         }\r
         ++eqc_i;\r
       }
-\r
+\r      */\r
+
       //if( r.getType().isInteger() ){\r
       //  Trace("qcf-mv") << "Model value for eqc(" << r << ") : " << d_quantEngine->getValuation().getModelValue( r ) << std::endl;\r
       //}\r

diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 090af8143bebdc55a42c3cc46388855482d804d8..62bd347c76a0d9cf114992f37a41ea0ed4a2fa1d 100755 (executable)
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -226,7 +226,6 @@ public:
   enum {\r
     effort_conflict,\r
     effort_prop_eq,\r
-    effort_partial,\r
     effort_mc,\r
   };\r
   short d_effort;\r

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index db61b046fad2623ba9f84183a8f4a8fd922ea8b0..a079dbaab3522f47f2adc975e9ecc584742517ad 100644 (file)
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -834,11 +834,11 @@ Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args,
       }
     }
   }
-  if( body==f[1] ){
-    return f;
-  }else{
-    return mkForAll( args, body, ipl );
-  }
+  //if( body==f[1] ){
+  //  return f;
+  //}else{
+  return mkForAll( args, body, ipl );
+  //}
 }
 
 Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& args, Node body, bool isNested ){