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

2 files changed, 34 insertions, 0 deletions

diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index c88fd187d..34a72e106 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -55,8 +55,13 @@ UnknownTypeException::UnknownTypeException(TNode n) throw() :
 /** Is this node constant? (and has that been computed yet?) */
 struct IsConstTag { };
 struct IsConstComputedTag { };
+struct HasBoundVarTag { };
+struct HasBoundVarComputedTag { };
 typedef expr::Attribute<IsConstTag, bool> IsConstAttr;
 typedef expr::Attribute<IsConstComputedTag, bool> IsConstComputedAttr;
+/** Attribute true for expressions with bound variables in them */
+typedef expr::Attribute<HasBoundVarTag, bool> HasBoundVarAttr;
+typedef expr::Attribute<HasBoundVarComputedTag, bool> HasBoundVarComputedAttr;
 
 template <bool ref_count>
 bool NodeTemplate<ref_count>::isConst() const {
@@ -91,7 +96,29 @@ bool NodeTemplate<ref_count>::isConst() const {
   }
 }
 
+template <bool ref_count>
+bool NodeTemplate<ref_count>::hasBoundVar() {
+  assertTNodeNotExpired();
+  if(! getAttribute(HasBoundVarComputedAttr())) {
+    bool hasBv = false;
+    if(getKind() == kind::BOUND_VARIABLE) {
+      hasBv = true;
+    } else {
+      for(iterator i = begin(); i != end() && !hasBv; ++i) {
+        hasBv = (*i).hasBoundVar();
+      }
+    }
+    setAttribute(HasBoundVarAttr(), hasBv);
+    setAttribute(HasBoundVarComputedAttr(), true);
+    Debug("bva") << *this << " has bva : " << getAttribute(HasBoundVarAttr()) << std::endl;
+    return hasBv;
+  }
+  return getAttribute(HasBoundVarAttr());
+}
+
 template bool NodeTemplate<true>::isConst() const;
 template bool NodeTemplate<false>::isConst() const;
+template bool NodeTemplate<true>::hasBoundVar();
+template bool NodeTemplate<false>::hasBoundVar();
 
 }/* CVC4 namespace */
diff --git a/src/expr/node.h b/src/expr/node.h
index 9ada7879c..ba139748e 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -424,6 +424,13 @@ public:
   // bool properlyContainsDecision(); // maybe not atomic but all children are
 
   /**
+   * Returns true iff this node contains a bound variable.  This bound
+   * variable may or may not be free.
+   * @return true iff this node contains a bound variable.
+   */
+  bool hasBoundVar();
+
+  /**
    * Convert this Node into an Expr using the currently-in-scope
    * manager.  Essentially this is like an "operator Expr()" but we
    * don't want it to compete with implicit conversions between e.g.