Adding optional 'check' parameter to getType() methods

6 files changed, 156 insertions, 104 deletions

diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index 9fb30bdb4..b8fa85c03 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -28,7 +28,7 @@ namespace arith {
 
 class ArithConstantTypeRule {
 public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate) {
     if (n.getKind() == kind::CONST_RATIONAL) return nodeManager->realType();
     return nodeManager->integerType();
@@ -37,7 +37,7 @@ public:
 
 class ArithOperatorTypeRule {
 public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate) {
     TypeNode integerType = nodeManager->integerType();
     TypeNode realType = nodeManager->realType();
@@ -45,10 +45,17 @@ public:
     TNode::iterator child_it_end = n.end();
     bool isInteger = true;
     for(; child_it != child_it_end; ++child_it) {
-      TypeNode childType = (*child_it).getType();
-      if (!childType.isInteger()) isInteger = false;
-      if(childType != integerType && childType != realType) {
-        throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic subterm");
+      TypeNode childType = (*child_it).getType(check);
+      if (!childType.isInteger()) {
+        isInteger = false;
+        if( !check ) { // if we're not checking, nothing left to do
+          break;
+        }
+      }
+      if( check ) {
+        if(childType != integerType && childType != realType) {
+          throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic subterm");
+        }
       }
     }
     return (isInteger ? integerType : realType);
@@ -57,17 +64,19 @@ public:
 
 class ArithPredicateTypeRule {
 public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate) {
-    TypeNode integerType = nodeManager->integerType();
-    TypeNode realType = nodeManager->realType();
-    TypeNode lhsType = n[0].getType();
-    if (lhsType != integerType && lhsType != realType) {
-      throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term on the left-hand-side");
-    }
-    TypeNode rhsType = n[1].getType();
-    if (rhsType != integerType && rhsType != realType) {
-      throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term on the right-hand-side");
+    if( check ) {
+      TypeNode integerType = nodeManager->integerType();
+      TypeNode realType = nodeManager->realType();
+      TypeNode lhsType = n[0].getType(check);
+      if (lhsType != integerType && lhsType != realType) {
+        throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term on the left-hand-side");
+      }
+      TypeNode rhsType = n[1].getType(check);
+      if (rhsType != integerType && rhsType != realType) {
+        throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term on the right-hand-side");
+      }
     }
     return nodeManager->booleanType();
   }
diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h
index 0eb88d800..5d0713a89 100644
--- a/src/theory/arrays/theory_arrays_type_rules.h
+++ b/src/theory/arrays/theory_arrays_type_rules.h
@@ -26,30 +26,34 @@ namespace theory {
 namespace arrays {
 
 struct ArraySelectTypeRule {
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
     throw (TypeCheckingExceptionPrivate) {
     Assert(n.getKind() == kind::SELECT);
-    TypeNode arrayType = n[0].getType();
-    TypeNode indexType = n[1].getType();
-    if(arrayType.getArrayIndexType() != indexType) {
-      throw TypeCheckingExceptionPrivate(n, "array select not indexed with correct type for array");
+    TypeNode arrayType = n[0].getType(check);
+    if( check ) {
+      TypeNode indexType = n[1].getType(check);
+      if(arrayType.getArrayIndexType() != indexType) {
+        throw TypeCheckingExceptionPrivate(n, "array select not indexed with correct type for array");
+      }
     }
     return arrayType.getArrayConstituentType();
   }
 };/* struct ArraySelectTypeRule */
 
 struct ArrayStoreTypeRule {
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
     throw (TypeCheckingExceptionPrivate) {
     Assert(n.getKind() == kind::STORE);
-    TypeNode arrayType = n[0].getType();
-    TypeNode indexType = n[1].getType();
-    TypeNode valueType = n[2].getType();
-    if(arrayType.getArrayIndexType() != indexType) {
-      throw TypeCheckingExceptionPrivate(n, "array store not indexed with correct type for array");
-    }
-    if(arrayType.getArrayConstituentType() != valueType) {
-      throw TypeCheckingExceptionPrivate(n, "array store not assigned with correct type for array");
+    TypeNode arrayType = n[0].getType(check);
+    if( check ) {
+      TypeNode indexType = n[1].getType(check);
+      TypeNode valueType = n[2].getType(check);
+      if(arrayType.getArrayIndexType() != indexType) {
+        throw TypeCheckingExceptionPrivate(n, "array store not indexed with correct type for array");
+      }
+      if(arrayType.getArrayConstituentType() != valueType) {
+        throw TypeCheckingExceptionPrivate(n, "array store not assigned with correct type for array");
+      }
     }
     return arrayType;
   }
diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h
index b947cee10..fddced8ef 100644
--- a/src/theory/booleans/theory_bool_type_rules.h
+++ b/src/theory/booleans/theory_bool_type_rules.h
@@ -27,30 +27,35 @@ namespace boolean {
 
 class BooleanTypeRule {
 public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate) {
     TypeNode booleanType = nodeManager->booleanType();
-    TNode::iterator child_it = n.begin();
-    TNode::iterator child_it_end = n.end();
-    for(; child_it != child_it_end; ++child_it)
-      if((*child_it).getType() != booleanType) {
-        throw TypeCheckingExceptionPrivate(n, "expecting a Boolean subexpression");
+    if( check ) {
+      TNode::iterator child_it = n.begin();
+      TNode::iterator child_it_end = n.end();
+      for(; child_it != child_it_end; ++child_it) {
+        if((*child_it).getType(check) != booleanType) {
+          throw TypeCheckingExceptionPrivate(n, "expecting a Boolean subexpression");
+        }
       }
+    }
     return booleanType;
   }
 };
 
 class IteTypeRule {
   public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate) {
-    TypeNode booleanType = nodeManager->booleanType();
-    if (n[0].getType() != booleanType) {
-      throw TypeCheckingExceptionPrivate(n, "condition of ITE is not Boolean");
-    }
-    TypeNode iteType = n[1].getType();
-    if (iteType != n[2].getType()) {
-      throw TypeCheckingExceptionPrivate(n, "both branches of the ITE must be of the same type");
+    TypeNode iteType = n[1].getType(check);
+    if( check ) {
+      TypeNode booleanType = nodeManager->booleanType();
+      if (n[0].getType(check) != booleanType) {
+        throw TypeCheckingExceptionPrivate(n, "condition of ITE is not Boolean");
+      }
+      if (iteType != n[2].getType(check)) {
+        throw TypeCheckingExceptionPrivate(n, "both branches of the ITE must be of the same type");
+      }
     }
     return iteType;
   }
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 19d6e268b..4458931a9 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -31,9 +31,11 @@ namespace builtin {
 
 class EqualityTypeRule {
   public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n) throw (TypeCheckingExceptionPrivate) {
-    if (n[0].getType() != n[1].getType()) {
-      throw TypeCheckingExceptionPrivate(n, "Left and right hand side of the equation are not of the same type");
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate) {
+    if( check ) {
+      if (n[0].getType(check) != n[1].getType(check)) {
+        throw TypeCheckingExceptionPrivate(n, "Left and right hand side of the equation are not of the same type");
+      }
     }
     return nodeManager->booleanType();
   }
@@ -41,13 +43,15 @@ class EqualityTypeRule {
 
 class DistinctTypeRule {
 public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n) {
-    TNode::iterator child_it = n.begin();
-    TNode::iterator child_it_end = n.end();
-    TypeNode firstType = (*child_it).getType();
-    for (++child_it; child_it != child_it_end; ++child_it) {
-      if ((*child_it).getType() != firstType) {
-        throw TypeCheckingExceptionPrivate(n, "Not all arguments are of the same type");
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
+    if( check ) {
+      TNode::iterator child_it = n.begin();
+      TNode::iterator child_it_end = n.end();
+      TypeNode firstType = (*child_it).getType(check);
+      for (++child_it; child_it != child_it_end; ++child_it) {
+        if ((*child_it).getType() != firstType) {
+          throw TypeCheckingExceptionPrivate(n, "Not all arguments are of the same type");
+        }
       }
     }
     return nodeManager->booleanType();
diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index 7aaae7349..9bb9e61df 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -18,6 +18,8 @@
 
 #include "cvc4_private.h"
 
+#include <algorithm>
+
 #ifndef __CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H
 #define __CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H
 
@@ -27,7 +29,7 @@ namespace bv {
 
 class BitVectorConstantTypeRule {
 public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate) {
     return nodeManager->mkBitVectorType(n.getConst<BitVector>().getSize());
   }
@@ -35,12 +37,14 @@ public:
 
 class BitVectorCompRule {
 public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate) {
-    TypeNode lhs = n[0].getType();
-    TypeNode rhs = n[1].getType();
-    if (!lhs.isBitVector() || lhs != rhs) {
-      throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms of the same width");
+    if( check ) {
+      TypeNode lhs = n[0].getType(check);
+      TypeNode rhs = n[1].getType(check);
+      if (!lhs.isBitVector() || lhs != rhs) {
+        throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms of the same width");
+      }
     }
     return nodeManager->mkBitVectorType(1);
   }
@@ -48,18 +52,18 @@ public:
 
 class BitVectorArithRule {
 public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate) {
     unsigned maxWidth = 0;
     TNode::iterator it = n.begin();
     TNode::iterator it_end = n.end();
     // TODO: optimize unary neg
     for (; it != it_end; ++ it) {
-      TypeNode t = (*it).getType();
-      if (!t.isBitVector()) {
+      TypeNode t = (*it).getType(check);
+      if (check && !t.isBitVector()) {
         throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
       }
-      if (maxWidth < t.getBitVectorSize()) maxWidth = t.getBitVectorSize();
+      maxWidth = std::max( maxWidth, t.getBitVectorSize() );
     }
     return nodeManager->mkBitVectorType(maxWidth);
   }
@@ -67,17 +71,19 @@ public:
 
 class BitVectorFixedWidthTypeRule {
 public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate) {
     TNode::iterator it = n.begin();
-    TNode::iterator it_end = n.end();
-    TypeNode t = (*it).getType();
-    if (!t.isBitVector()) {
-      throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
-    }
-    for (++ it; it != it_end; ++ it) {
-      if ((*it).getType() != t) {
-        throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms of the same width");
+    TypeNode t = (*it).getType(check);
+    if( check ) {
+      if (!t.isBitVector()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
+      }
+      TNode::iterator it_end = n.end();
+      for (++ it; it != it_end; ++ it) {
+        if ((*it).getType(check) != t) {
+          throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms of the same width");
+        }
       }
     }
     return t;
@@ -86,15 +92,17 @@ public:
 
 class BitVectorPredicateTypeRule {
 public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate) {
-    TypeNode lhsType = n[0].getType();
-    if (!lhsType.isBitVector()) {
-      throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
-    }
-    TypeNode rhsType = n[1].getType();
-    if (lhsType != rhsType) {
-      throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms of the same width");
+    if( check ) {
+      TypeNode lhsType = n[0].getType(check);
+      if (!lhsType.isBitVector()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
+      }
+      TypeNode rhsType = n[1].getType(check);
+      if (lhsType != rhsType) {
+        throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms of the same width");
+      }
     }
     return nodeManager->booleanType();
   }
@@ -102,18 +110,25 @@ public:
 
 class BitVectorExtractTypeRule {
 public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate) {
-    TypeNode t = n[0].getType();
-    if (!t.isBitVector()) {
-      throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
-    }
     BitVectorExtract extractInfo = n.getOperator().getConst<BitVectorExtract>();
+
+    // NOTE: We're throwing a type-checking exception here even
+    // if check is false, bc if we allow high < low the resulting
+    // type will be illegal
     if (extractInfo.high < extractInfo.low) {
       throw TypeCheckingExceptionPrivate(n, "high extract index is smaller than the low extract index");
     }
-    if (extractInfo.high >= t.getBitVectorSize()) {
-      throw TypeCheckingExceptionPrivate(n, "high extract index is bigger than the size of the bit-vector");
+
+    if( check ) {
+      TypeNode t = n[0].getType(check);
+      if (!t.isBitVector()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
+      }
+      if (extractInfo.high >= t.getBitVectorSize()) {
+        throw TypeCheckingExceptionPrivate(n, "high extract index is bigger than the size of the bit-vector");
+      }
     }
     return nodeManager->mkBitVectorType(extractInfo.high - extractInfo.low + 1);
   }
@@ -121,13 +136,16 @@ public:
 
 class BitVectorConcatRule {
 public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate) {
     unsigned size = 0;
     TNode::iterator it = n.begin();
     TNode::iterator it_end = n.end();
     for (; it != it_end; ++ it) {
-       TypeNode t = n[0].getType();
+       TypeNode t = n[0].getType(check);
+       // NOTE: We're throwing a type-checking exception here even
+       // when check is false, bc if we don't check that the arguments
+       // are bit-vectors the result type will be inaccurate
        if (!t.isBitVector()) {
          throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
        }
@@ -139,9 +157,12 @@ public:
 
 class BitVectorRepeatTypeRule {
 public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate) {
-    TypeNode t = n[0].getType();
+    TypeNode t = n[0].getType(check);
+    // NOTE: We're throwing a type-checking exception here even
+    // when check is false, bc if the argument isn't a bit-vector
+    // the result type will be inaccurate
     if (!t.isBitVector()) {
       throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
     }
@@ -152,9 +173,12 @@ public:
 
 class BitVectorExtendTypeRule {
 public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate) {
-    TypeNode t = n[0].getType();
+    TypeNode t = n[0].getType(check);
+    // NOTE: We're throwing a type-checking exception here even
+    // when check is false, bc if the argument isn't a bit-vector
+    // the result type will be inaccurate
     if (!t.isBitVector()) {
       throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
     }
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index f09a44d50..38018112a 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -27,20 +27,26 @@ namespace uf {
 
 class UfTypeRule {
 public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate) {
     TNode f = n.getOperator();
-    TypeNode fType = f.getType();
-    if (n.getNumChildren() != fType.getNumChildren() - 1) {
-      throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type");
+    TypeNode fType = f.getType(check);
+    if( !fType.isFunction() ) {
+      throw TypeCheckingExceptionPrivate(n, "operator does not have function type");
     }
-    TNode::iterator argument_it = n.begin();
-    TNode::iterator argument_it_end = n.end();
-    TypeNode::iterator argument_type_it = fType.begin();
-    for(; argument_it != argument_it_end; ++argument_it)
-      if((*argument_it).getType() != *argument_type_it) {
-        throw TypeCheckingExceptionPrivate(n, "argument types do not match the function type");
+    if( check ) {
+      if (n.getNumChildren() != fType.getNumChildren() - 1) {
+        throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type");
       }
+      TNode::iterator argument_it = n.begin();
+      TNode::iterator argument_it_end = n.end();
+      TypeNode::iterator argument_type_it = fType.begin();
+      for(; argument_it != argument_it_end; ++argument_it) {
+        if((*argument_it).getType() != *argument_type_it) {
+          throw TypeCheckingExceptionPrivate(n, "argument types do not match the function type");
+        }
+      }
+    }
     return fType.getRangeType();
   }
 };/* class UfTypeRule */