Remove --ite-remove-quant; support pulling ground ITEs out of quantifier bodies; fix bug 551, improper ITE removal under quantifiers.

7 files changed, 29 insertions, 62 deletions

diff --git a/src/theory/ite_utilities.cpp b/src/theory/ite_utilities.cpp
index 1b4e096f2..a4af4f26f 100644
--- a/src/theory/ite_utilities.cpp
+++ b/src/theory/ite_utilities.cpp
@@ -28,6 +28,7 @@ namespace CVC4 {
 namespace theory {
 
 namespace ite {
+
 inline static bool isTermITE(TNode e) {
   return (e.getKind() == kind::ITE && !e.getType().isBoolean());
 }
@@ -77,9 +78,7 @@ struct CTIVStackElement {
 
 } /* CVC4::theory::ite */
 
-
-
-ITEUtilities::ITEUtilities(ContainsTermITEVistor* containsVisitor)
+ITEUtilities::ITEUtilities(ContainsTermITEVisitor* containsVisitor)
   : d_containsVisitor(containsVisitor)
   , d_compressor(NULL)
   , d_simplifier(NULL)
@@ -144,11 +143,11 @@ void ITEUtilities::clear(){
 }
 
 /*********************                                                        */
-/* ContainsTermITEVistor
+/* ContainsTermITEVisitor
  */
-ContainsTermITEVistor::ContainsTermITEVistor(): d_cache() {}
-ContainsTermITEVistor::~ContainsTermITEVistor(){}
-bool ContainsTermITEVistor::containsTermITE(TNode e){
+ContainsTermITEVisitor::ContainsTermITEVisitor(): d_cache() {}
+ContainsTermITEVisitor::~ContainsTermITEVisitor(){}
+bool ContainsTermITEVisitor::containsTermITE(TNode e){
   /* throughout execution skip through NOT nodes. */
   e = (e.getKind() == kind::NOT) ? e[0] : e;
   if(ite::triviallyContainsNoTermITEs(e)){ return false; }
@@ -197,7 +196,7 @@ bool ContainsTermITEVistor::containsTermITE(TNode e){
   }
   return foundTermIte;
 }
-void ContainsTermITEVistor::garbageCollect() {
+void ContainsTermITEVisitor::garbageCollect() {
   d_cache.clear();
 }
 
@@ -249,7 +248,7 @@ void IncomingArcCounter::clear() {
 /*********************                                                        */
 /* ITECompressor
  */
-ITECompressor::ITECompressor(ContainsTermITEVistor* contains)
+ITECompressor::ITECompressor(ContainsTermITEVisitor* contains)
   : d_contains(contains)
   , d_assertions(NULL)
   , d_incoming(true, true)
@@ -547,7 +546,7 @@ uint32_t TermITEHeightCounter::termITEHeight(TNode e){
 
 
 
-ITESimplifier::ITESimplifier(ContainsTermITEVistor* contains)
+ITESimplifier::ITESimplifier(ContainsTermITEVisitor* contains)
   : d_containsVisitor(contains)
   , d_termITEHeight()
   , d_constantLeaves()
@@ -1608,6 +1607,5 @@ Node ITECareSimplifier::simplifyWithCare(TNode e)
   return substitute(e, substTable, cache);
 }
 
-
 } /* namespace theory */
 } /* namespace CVC4 */
diff --git a/src/theory/ite_utilities.h b/src/theory/ite_utilities.h
index d9e6120aa..7f0986ecb 100644
--- a/src/theory/ite_utilities.h
+++ b/src/theory/ite_utilities.h
@@ -31,7 +31,7 @@
 namespace CVC4 {
 namespace theory {
 
-class ContainsTermITEVistor;
+class ContainsTermITEVisitor;
 class IncomingArcCounter;
 class TermITEHeightCounter;
 class ITECompressor;
@@ -40,7 +40,7 @@ class ITECareSimplifier;
 
 class ITEUtilities {
 public:
-  ITEUtilities(ContainsTermITEVistor* containsVisitor);
+  ITEUtilities(ContainsTermITEVisitor* containsVisitor);
   ~ITEUtilities();
 
   Node simpITE(TNode assertion);
@@ -55,7 +55,7 @@ public:
   void clear();
 
 private:
-  ContainsTermITEVistor* d_containsVisitor;
+  ContainsTermITEVisitor* d_containsVisitor;
   ITECompressor* d_compressor;
   ITESimplifier* d_simplifier;
   ITECareSimplifier* d_careSimp;
@@ -64,10 +64,10 @@ private:
 /**
  * A caching visitor that computes whether a node contains a term ite.
  */
-class ContainsTermITEVistor {
+class ContainsTermITEVisitor {
 public:
-  ContainsTermITEVistor();
-  ~ContainsTermITEVistor();
+  ContainsTermITEVisitor();
+  ~ContainsTermITEVisitor();
 
   /** returns true if a node contains a term ite. */
   bool containsTermITE(TNode n);
@@ -140,7 +140,7 @@ private:
  */
 class ITECompressor {
 public:
-  ITECompressor(ContainsTermITEVistor* contains);
+  ITECompressor(ContainsTermITEVisitor* contains);
   ~ITECompressor();
 
   /* returns false if an assertion is discovered to be equal to false. */
@@ -153,7 +153,7 @@ private:
 
   Node d_true; /* Copy of true. */
   Node d_false; /* Copy of false. */
-  ContainsTermITEVistor* d_contains;
+  ContainsTermITEVisitor* d_contains;
   std::vector<Node>* d_assertions;
   IncomingArcCounter d_incoming;
 
@@ -180,7 +180,7 @@ private:
 
 class ITESimplifier {
 public:
-  ITESimplifier(ContainsTermITEVistor* d_containsVisitor);
+  ITESimplifier(ContainsTermITEVisitor* d_containsVisitor);
   ~ITESimplifier();
 
   Node simpITE(TNode assertion);
@@ -192,7 +192,7 @@ private:
   Node d_true;
   Node d_false;
 
-  ContainsTermITEVistor* d_containsVisitor;
+  ContainsTermITEVisitor* d_containsVisitor;
   inline bool containsTermITE(TNode n) {
     return d_containsVisitor->containsTermITE(n);
   }
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 78f989807..e59874429 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -274,7 +274,7 @@ void BoundedIntegers::registerQuantifier( Node f ) {
       for( unsigned i=0; i<d_set[f].size(); i++) {
         Node v = d_set[f][i];
         Node r = d_range[f][v];
-        if( quantifiers::TermDb::hasBoundVarAttr(r) ){
+        if( r.hasBoundVar() ){
           //introduce a new bound
           Node new_range = NodeManager::currentNM()->mkSkolem( "bir_$$", r.getType(), "bound for term" );
           d_nground_range[f][v] = d_range[f][v];
@@ -384,5 +384,5 @@ void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node
 }
 
 bool BoundedIntegers::isGroundRange(Node f, Node v) {
-  return isBoundVar(f,v) && !quantifiers::TermDb::hasBoundVarAttr(getLowerBound(f,v)) && !quantifiers::TermDb::hasBoundVarAttr(getUpperBound(f,v));
+  return isBoundVar(f,v) && !getLowerBound(f,v).hasBoundVar() && !getUpperBound(f,v).hasBoundVar();
 }
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 6d333521b..2967c77c8 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -42,8 +42,6 @@ option clauseSplit --clause-split bool :default false
 #   forall x. P( x ) => f( S( x ) ) = x
 option preSkolemQuant --pre-skolem-quant bool :read-write :default false
  apply skolemization eagerly to bodies of quantified formulas
-option iteRemoveQuant --ite-remove-quant bool :default false
- apply ite removal to bodies of quantifiers
 # Whether to perform agressive miniscoping
 option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false
  perform aggressive miniscoping for quantifiers
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index ced4e1997..ae5a35a00 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -128,7 +128,7 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant )
     registerNode( n[1], hasPol, pol, true );

   }else{

     if( n.getKind()!=OR && n.getKind()!=AND && n.getKind()!=IFF && n.getKind()!=NOT ){

-      if( quantifiers::TermDb::hasBoundVarAttr( n ) ){

+      if( n.hasBoundVar() ){

         //literals

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

           for( unsigned i=0; i<n.getNumChildren(); i++ ){

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

 void QuantInfo::flatten( Node n, bool beneathQuant ) {

   Trace("qcf-qregister-debug2") << "Flatten : " << n << std::endl;

-  if( quantifiers::TermDb::hasBoundVarAttr( n ) ){

+  if( n.hasBoundVar() ){

     if( d_var_num.find( n )==d_var_num.end() ){

       Trace("qcf-qregister-debug2") << "Add FLATTEN VAR : " << n << std::endl;

       d_var_num[n] = d_vars.size();

@@ -647,7 +647,7 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){
       d_type = typ_invalid;

     }

   }else{

-    if( quantifiers::TermDb::hasBoundVarAttr( n ) ){

+    if( n.hasBoundVar() ){

       d_type_not = false;

       d_n = n;

       if( d_n.getKind()==NOT ){

@@ -693,7 +693,7 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){
         //literals

         if( d_n.getKind()==EQUAL ){

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

-            if( quantifiers::TermDb::hasBoundVarAttr( d_n[i] ) ){

+            if( d_n[i].hasBoundVar() ){

               if( !qi->isVar( d_n[i] ) ){

                 Trace("qcf-qregister-debug")  << "ERROR : not var " << d_n[i] << std::endl;

               }else if( d_n[i].getKind()==BOUND_VARIABLE && !beneathQuant ){

@@ -844,7 +844,7 @@ void MatchGen::reset_round( QuantConflictFind * p ) {
     }

   }else if( d_type==typ_eq ){

     for( unsigned i=0; i<d_n.getNumChildren(); i++ ){

-      if( !quantifiers::TermDb::hasBoundVarAttr( d_n[i] ) ){

+      if( !d_n[i].hasBoundVar() ){

         d_ground_eval[i] = p->evaluateTerm( d_n[i] );

       }

     }

@@ -1904,7 +1904,7 @@ void QuantConflictFind::computeRelevantEqr() {
     eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );

     while( !eqc_i.isFinished() ){

       TNode n = (*eqc_i);

-      if( quantifiers::TermDb::hasBoundVarAttr( n ) ){

+      if( n.hasBoundVar() ){

         std::cout << "BAD TERM IN DB : " << n << std::endl;

         exit( 199 );

       }

@@ -1945,7 +1945,7 @@ void QuantConflictFind::computeRelevantEqr() {
         //    std::cout << n.getKind() << " " << n.getOperator() << " " << n << std::endl;

         //  }

         //}

-        if( !quantifiers::TermDb::hasBoundVarAttr( n ) ){    //temporary

+        if( !n.hasBoundVar() ){    //temporary

 

           bool isRedundant;

           std::map< TNode, std::vector< TNode > >::iterator it_na;

@@ -2095,4 +2095,4 @@ QuantConflictFind::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_partial_inst);

 }

 

-}
\ No newline at end of file
+}

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 39ba3e8af..9a912130f 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -348,28 +348,6 @@ bool TermDb::hasInstConstAttr( Node n ) {
   return !getInstConstAttr(n).isNull();
 }
 
-bool TermDb::hasBoundVarAttr( Node n ) {
-  if( !n.getAttribute(HasBoundVarComputedAttribute()) ){
-    bool hasBv = false;
-    if( n.getKind()==BOUND_VARIABLE ){
-      hasBv = true;
-    }else{
-      for (unsigned i=0; i<n.getNumChildren(); i++) {
-        if( hasBoundVarAttr(n[i]) ){
-          hasBv = true;
-          break;
-        }
-      }
-    }
-    HasBoundVarAttribute hbva;
-    n.setAttribute(hbva, hasBv);
-    HasBoundVarComputedAttribute hbvca;
-    n.setAttribute(hbvca, true);
-    Trace("bva") << n << " has bva : " << n.getAttribute(HasBoundVarAttribute()) << std::endl;
-  }
-  return n.getAttribute(HasBoundVarAttribute());
-}
-
 void TermDb::getBoundVars( Node n, std::vector< Node >& bvs) {
   if (n.getKind()==BOUND_VARIABLE ){
     if ( std::find( bvs.begin(), bvs.end(), n)==bvs.end() ){
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 860f087dd..66b45be2f 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -60,11 +60,6 @@ typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
 struct ModelBasisArgAttributeId {};
 typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> ModelBasisArgAttribute;
 
-struct HasBoundVarAttributeId {};
-typedef expr::Attribute<HasBoundVarAttributeId, bool> HasBoundVarAttribute;
-struct HasBoundVarComputedAttributeId {};
-typedef expr::Attribute<HasBoundVarComputedAttributeId, bool> HasBoundVarComputedAttribute;
-
 //for rewrite rules
 struct QRewriteRuleAttributeId {};
 typedef expr::Attribute<QRewriteRuleAttributeId, Node> QRewriteRuleAttribute;
@@ -210,8 +205,6 @@ public:
   static bool hasInstConstAttr( Node n );
 //for bound variables
 public:
-  //does n have bound variables?
-  static bool hasBoundVarAttr( Node n );
   //get bound variables in n
   static void getBoundVars( Node n, std::vector< Node >& bvs);
 //for skolem