Type-checking classes and hooks (not tested yet).

8 files changed, 354 insertions, 3 deletions

diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index 7c3e76d0a..0428bf84e 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -8,6 +8,7 @@ noinst_LTLIBRARIES = libarith.la
 libarith_la_SOURCES = \
 	theory_arith.h \
 	theory_arith.cpp \
+	theory_arith_type_rules.h \
 	arith_rewriter.h \
 	arith_rewriter.cpp \
 	arith_utilities.h \
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
new file mode 100644
index 000000000..e97af08ee
--- /dev/null
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -0,0 +1,74 @@
+/*********************                                                        */
+/** theory_arith_type_rules.cpp
+ ** Original author: dejan
+ ** Major contributors: none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY_ARITH_TYPE_RULES_H_
+#define __CVC4__THEORY_ARITH_TYPE_RULES_H_
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+
+class ArithConstantTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+      throw (TypeCheckingException) {
+    if (n.getKind() == kind::CONST_RATIONAL) return nodeManager->realType();
+    return nodeManager->integerType();
+  }
+};
+
+class ArithOperatorTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+      throw (TypeCheckingException) {
+    TypeNode integerType = nodeManager->integerType();
+    TypeNode realType = nodeManager->realType();
+    TNode::iterator child_it = n.begin();
+    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");
+      }
+    }
+    return (isInteger ? integerType : realType);
+  }
+};
+
+class ArithPredicateTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+      throw (TypeCheckingException) {
+    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");
+    }
+    return nodeManager->booleanType();
+  }
+};
+
+}
+}
+}
+
+#endif /* THEORY_ARITH_TYPE_RULES_H_ */
diff --git a/src/theory/booleans/Makefile.am b/src/theory/booleans/Makefile.am
index 690299630..a1b3e097a 100644
--- a/src/theory/booleans/Makefile.am
+++ b/src/theory/booleans/Makefile.am
@@ -6,6 +6,7 @@ AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
 noinst_LTLIBRARIES = libbooleans.la
 
 libbooleans_la_SOURCES = \
-	theory_bool.h
+	theory_bool.h \
+	theory_bool_type_rules.h
 
 EXTRA_DIST = kinds
diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h
new file mode 100644
index 000000000..4cfc2f87f
--- /dev/null
+++ b/src/theory/booleans/theory_bool_type_rules.h
@@ -0,0 +1,56 @@
+/*********************                                                        */
+/** theory_bool_type_rules.cpp
+ ** Original author: dejan
+ ** Major contributors: none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY_BOOL_TYPE_RULES_H_
+#define __CVC4__THEORY_BOOL_TYPE_RULES_H_
+
+namespace CVC4 {
+namespace theory {
+namespace boolean {
+
+class BooleanTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+      throw (TypeCheckingException) {
+    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");
+      }
+    return booleanType;
+  }
+};
+
+class IteTypeRule {
+  public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n) throw (TypeCheckingException) {
+    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");
+    }
+    return iteType;
+  }
+};
+
+} // boolean namespace
+} // theory namespace
+} // CVC4 namespace
+
+#endif /* __CVC4__THEORY_BOOL_TYPE_RULES_H_ */
diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am
index d90472fd3..6f9a51dc3 100644
--- a/src/theory/bv/Makefile.am
+++ b/src/theory/bv/Makefile.am
@@ -6,6 +6,7 @@ AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
 noinst_LTLIBRARIES = libbv.la
 
 libbv_la_SOURCES = \
-	theory_bv.h
+	theory_bv.h \
+	theory_bv_type_rules.h
 
 EXTRA_DIST = kinds
diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
new file mode 100644
index 000000000..c9a7c1f2c
--- /dev/null
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -0,0 +1,170 @@
+/*********************                                                        */
+/** theory_bv_types.h
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Bitvector theory.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__EXPR_TYPE_THEORY_BV_TYPE_RULES_H_
+#define __CVC4__EXPR_TYPE_THEORY_BV_TYPE_RULES_H_
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+class BitVectorConstantTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+      throw (TypeCheckingException) {
+    return nodeManager->bitVectorType(n.getConst<BitVector>().getSize());
+  }
+};
+
+class BitVectorCompRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+      throw (TypeCheckingException) {
+    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");
+    }
+    return nodeManager->bitVectorType(1);
+  }
+};
+
+class BitVectorArithRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+      throw (TypeCheckingException) {
+    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()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
+      }
+      if (maxWidth < t.getBitVectorSize()) maxWidth = t.getBitVectorSize();
+    }
+    return nodeManager->bitVectorType(maxWidth);
+  }
+};
+
+class BitVectorFixedWidthTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+      throw (TypeCheckingException) {
+    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");
+      }
+    }
+    return t;
+  }
+};
+
+class BitVectorPredicateTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+      throw (TypeCheckingException) {
+    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");
+    }
+    return nodeManager->booleanType();
+  }
+};
+
+class BitVectorExtractTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+      throw (TypeCheckingException) {
+    TypeNode t = n[0].getType();
+    if (!t.isBitVector()) {
+      throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
+    }
+    BitVectorExtract extractInfo = n.getOperator().getConst<BitVectorExtract>();
+    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");
+    }
+    return nodeManager->bitVectorType(extractInfo.high - extractInfo.low + 1);
+  }
+};
+
+class BitVectorConcatRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+      throw (TypeCheckingException) {
+    unsigned size = 0;
+    TNode::iterator it = n.begin();
+    TNode::iterator it_end = n.end();
+    for (; it != it_end; ++ it) {
+       TypeNode t = n[0].getType();
+       if (!t.isBitVector()) {
+         throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
+       }
+       size += t.getBitVectorSize();
+    }
+    return nodeManager->bitVectorType(size);
+  }
+};
+
+class BitVectorRepeatTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+      throw (TypeCheckingException) {
+    TypeNode t = n[0].getType();
+    if (!t.isBitVector()) {
+      throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
+    }
+    unsigned repeatAmount = n.getOperator().getConst<BitVectorRepeat>();
+    return nodeManager->bitVectorType(repeatAmount * t.getBitVectorSize());
+  }
+};
+
+class BitVectorExtendTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+      throw (TypeCheckingException) {
+    TypeNode t = n[0].getType();
+    if (!t.isBitVector()) {
+      throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
+    }
+    unsigned extendAmount = n.getKind() == kind::BITVECTOR_SIGN_EXTEND ?
+        (unsigned) n.getOperator().getConst<BitVectorSignExtend>() :
+        (unsigned) n.getOperator().getConst<BitVectorZeroExtend>();
+
+    return nodeManager->bitVectorType(extendAmount +  t.getBitVectorSize());
+  }
+};
+
+}
+}
+}
+
+#endif /* __CVC4__EXPR_TYPE_THEORY_BV_TYPE_RULES_H_ */
diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am
index e0aa3a1df..e40359521 100644
--- a/src/theory/uf/Makefile.am
+++ b/src/theory/uf/Makefile.am
@@ -9,6 +9,7 @@ libuf_la_SOURCES = \
 	ecdata.h \
 	ecdata.cpp \
 	theory_uf.h \
-	theory_uf.cpp
+	theory_uf.cpp \
+	theory_uf_type_rules.h 
 
 EXTRA_DIST = kinds
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
new file mode 100644
index 000000000..8c05591d6
--- /dev/null
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -0,0 +1,47 @@
+/*********************                                                        */
+/** theory_uf_type_rules.h
+ ** Original author: dejan
+ ** Major contributors: none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY_UF_TYPE_RULES_H_
+#define __CVC4__THEORY_UF_TYPE_RULES_H_
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
+
+class UfTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+      throw (TypeCheckingException) {
+    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");
+    }
+    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();
+  }
+};
+
+}
+}
+}
+
+
+#endif /* THEORY_UF_TYPE_RULES_H_ */