bug fixes for types, old unit tests for types work now

4 files changed, 16 insertions, 15 deletions

diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index e97af08ee..b21ed0d6f 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -23,7 +23,7 @@ namespace arith {
 class ArithConstantTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
-      throw (TypeCheckingException) {
+      throw (TypeCheckingExceptionPrivate) {
     if (n.getKind() == kind::CONST_RATIONAL) return nodeManager->realType();
     return nodeManager->integerType();
   }
@@ -32,7 +32,7 @@ public:
 class ArithOperatorTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
-      throw (TypeCheckingException) {
+      throw (TypeCheckingExceptionPrivate) {
     TypeNode integerType = nodeManager->integerType();
     TypeNode realType = nodeManager->realType();
     TNode::iterator child_it = n.begin();
@@ -52,7 +52,7 @@ public:
 class ArithPredicateTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
-      throw (TypeCheckingException) {
+      throw (TypeCheckingExceptionPrivate) {
     TypeNode integerType = nodeManager->integerType();
     TypeNode realType = nodeManager->realType();
     TypeNode lhsType = n[0].getType();
diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h
index 4cfc2f87f..95d0f3bf6 100644
--- a/src/theory/booleans/theory_bool_type_rules.h
+++ b/src/theory/booleans/theory_bool_type_rules.h
@@ -22,7 +22,7 @@ namespace boolean {
 class BooleanTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
-      throw (TypeCheckingException) {
+      throw (TypeCheckingExceptionPrivate) {
     TypeNode booleanType = nodeManager->booleanType();
     TNode::iterator child_it = n.begin();
     TNode::iterator child_it_end = n.end();
@@ -36,7 +36,8 @@ public:
 
 class IteTypeRule {
   public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n) throw (TypeCheckingException) {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+      throw (TypeCheckingExceptionPrivate) {
     TypeNode booleanType = nodeManager->booleanType();
     if (n[0].getType() != booleanType) {
       throw TypeCheckingExceptionPrivate(n, "condition of ITE is not Boolean");
diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index c9a7c1f2c..9c245b67a 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -25,7 +25,7 @@ namespace bv {
 class BitVectorConstantTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
-      throw (TypeCheckingException) {
+      throw (TypeCheckingExceptionPrivate) {
     return nodeManager->bitVectorType(n.getConst<BitVector>().getSize());
   }
 };
@@ -33,7 +33,7 @@ public:
 class BitVectorCompRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
-      throw (TypeCheckingException) {
+      throw (TypeCheckingExceptionPrivate) {
     TypeNode lhs = n[0].getType();
     TypeNode rhs = n[1].getType();
     if (!lhs.isBitVector() || lhs != rhs) {
@@ -46,7 +46,7 @@ public:
 class BitVectorArithRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
-      throw (TypeCheckingException) {
+      throw (TypeCheckingExceptionPrivate) {
     unsigned maxWidth = 0;
     TNode::iterator it = n.begin();
     TNode::iterator it_end = n.end();
@@ -65,7 +65,7 @@ public:
 class BitVectorFixedWidthTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
-      throw (TypeCheckingException) {
+      throw (TypeCheckingExceptionPrivate) {
     TNode::iterator it = n.begin();
     TNode::iterator it_end = n.end();
     TypeNode t = (*it).getType();
@@ -84,7 +84,7 @@ public:
 class BitVectorPredicateTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
-      throw (TypeCheckingException) {
+      throw (TypeCheckingExceptionPrivate) {
     TypeNode lhsType = n[0].getType();
     if (!lhsType.isBitVector()) {
       throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
@@ -100,7 +100,7 @@ public:
 class BitVectorExtractTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
-      throw (TypeCheckingException) {
+      throw (TypeCheckingExceptionPrivate) {
     TypeNode t = n[0].getType();
     if (!t.isBitVector()) {
       throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
@@ -119,7 +119,7 @@ public:
 class BitVectorConcatRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
-      throw (TypeCheckingException) {
+      throw (TypeCheckingExceptionPrivate) {
     unsigned size = 0;
     TNode::iterator it = n.begin();
     TNode::iterator it_end = n.end();
@@ -137,7 +137,7 @@ public:
 class BitVectorRepeatTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
-      throw (TypeCheckingException) {
+      throw (TypeCheckingExceptionPrivate) {
     TypeNode t = n[0].getType();
     if (!t.isBitVector()) {
       throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
@@ -150,7 +150,7 @@ public:
 class BitVectorExtendTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
-      throw (TypeCheckingException) {
+      throw (TypeCheckingExceptionPrivate) {
     TypeNode t = n[0].getType();
     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 8c05591d6..4028c3022 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -22,7 +22,7 @@ namespace uf {
 class UfTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
-      throw (TypeCheckingException) {
+      throw (TypeCheckingExceptionPrivate) {
     TNode f = n.getOperator();
     TypeNode fType = f.getType();
     if (n.getNumChildren() != fType.getNumChildren() - 1) {