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

22 files changed, 740 insertions, 24 deletions

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index ef51b9c83..c3c3fccf6 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -10,6 +10,7 @@ libexpr_la_SOURCES = \
 	node.cpp \
 	type_node.h \
 	type_node.cpp \
+	builtin_type_rules.h \
 	node_builder.h \
 	@srcdir@/expr.h \
 	type.h \
diff --git a/src/expr/builtin_type_rules.h b/src/expr/builtin_type_rules.h
new file mode 100644
index 000000000..2a6b43b22
--- /dev/null
+++ b/src/expr/builtin_type_rules.h
@@ -0,0 +1,51 @@
+/*********************                                                        */
+/** builtin_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__BUILTIN_TYPE_RULES_H_
+#define __CVC4__BUILTIN_TYPE_RULES_H_
+
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "expr/expr.h"
+
+namespace CVC4 {
+
+class EqualityTypeRule {
+  public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n) throw (TypeCheckingException) {
+    if (n[0].getType() != n[1].getType()) {
+      throw TypeCheckingExceptionPrivate(n, "Left and right hand side of the equation are not of the same type");
+    }
+    return nodeManager->booleanType();
+  }
+};
+
+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");
+      }
+    }
+    return nodeManager->booleanType();
+  }
+};
+
+}
+
+#endif /* __CVC4__BUILTIN_TYPE_RULES_H_ */
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index b957019fb..03a54d49b 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -229,9 +229,15 @@ SortType ExprManager::mkSort(const std::string& name) {
   return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name)));
 }
 
-Type ExprManager::getType(const Expr& e) {
+Type ExprManager::getType(const Expr& e) throw (TypeCheckingException) {
   NodeManagerScope nms(d_nodeManager);
-  return Type(d_nodeManager, new TypeNode(d_nodeManager->getType(e.getNode())));
+  Type t;
+  try {
+    t = Type(d_nodeManager, new TypeNode(d_nodeManager->getType(e.getNode())));
+  } catch (const TypeCheckingExceptionPrivate& e) {
+    throw TypeCheckingException(Expr(this, new Node(e.getNode())), e.getMessage());
+  }
+  return t;
 }
 
 Expr ExprManager::mkVar(const std::string& name, const Type& type) {
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index b3a1b68df..16d1b4534 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -22,6 +22,7 @@
 
 #include "expr/kind.h"
 #include "expr/type.h"
+#include "expr/expr.h"
 
 ${includes}
 
@@ -208,7 +209,7 @@ public:
   SortType mkSort(const std::string& name);
 
   /** Get the type of an expression */
-  Type getType(const Expr& e);
+  Type getType(const Expr& e) throw (TypeCheckingException);
 
   // variables are special, because duplicates are permitted
   Expr mkVar(const std::string& name, const Type& type);
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index ba7032e34..a1be2ece8 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -14,6 +14,7 @@
  **/
 
 #include "expr/expr.h"
+#include "expr/expr_manager.h"
 #include "expr/node.h"
 #include "util/Assert.h"
 
@@ -26,7 +27,7 @@ ${includes}
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 30 "${template}"
+#line 31 "${template}"
 
 using namespace CVC4::kind;
 
@@ -37,6 +38,25 @@ std::ostream& operator<<(std::ostream& out, const Expr& e) {
   return out;
 }
 
+TypeCheckingException::TypeCheckingException(const Expr& expr, std::string message)
+: Exception(message), d_expr(new Expr(expr))
+{
+}
+
+TypeCheckingException::~TypeCheckingException() throw () {
+  delete d_expr;
+}
+
+std::string TypeCheckingException::toString() const {
+  std::stringstream ss;
+  ss << "Error type-checking " << d_expr << ": " << d_msg;
+  return ss.str();
+}
+
+Expr TypeCheckingException::getExpression() const {
+  return *d_expr;
+}
+
 Expr::Expr() :
   d_node(new Node),
   d_exprManager(NULL) {
@@ -129,7 +149,7 @@ Expr Expr::getOperator() const {
   return Expr(d_exprManager, new Node(d_node->getOperator()));
 }
 
-Type Expr::getType() const {
+Type Expr::getType() const throw (TypeCheckingException) {
   ExprManagerScope ems(*this);
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
   return d_exprManager->getType(*this);
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 0e960358f..914d47959 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -15,12 +15,10 @@
 
 #include "cvc4_public.h"
 
-// circular dependency: force expr_manager.h first
-#include "expr/expr_manager.h"
-
 #ifndef __CVC4__EXPR_H
 #define __CVC4__EXPR_H
 
+#include "expr/type.h"
 #include <string>
 #include <iostream>
 #include <stdint.h>
@@ -31,7 +29,7 @@ ${includes}
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 35 "${template}"
+#line 33 "${template}"
 
 namespace CVC4 {
 
@@ -39,6 +37,40 @@ namespace CVC4 {
 template <bool ref_count>
 class NodeTemplate;
 
+class Expr;
+
+/**
+ * Exception thrown in the case of type-checking errors.
+ */
+class TypeCheckingException : public Exception {
+
+private:
+
+  /** The expression responsible for the error */
+  Expr* d_expr;
+
+protected:
+
+  TypeCheckingException(): Exception() {}
+  TypeCheckingException(const Expr& expr, std::string message);
+
+public:
+
+  /** Destructor */
+  ~TypeCheckingException() throw ();
+
+  /**
+   * Get the Node that caused the type-checking to fail.
+   * @return the node
+   */
+  Expr getExpression() const;
+
+  /** Returns the message corresponding to the type-checking failure */
+  std::string toString() const;
+
+  friend class ExprManager;
+};
+
 /**
  * Class encapsulating CVC4 expressions and methods for constructing new
  * expressions.
@@ -144,7 +176,7 @@ public:
   /** Returns the type of the expression, if it has been computed.
    * Returns NULL if the type of the expression is not known.
    */
-  Type getType() const;
+  Type getType() const throw (TypeCheckingException);
 
   /**
    * Returns the string representation of the expression.
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index bf1997381..7ebea8a70 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -26,4 +26,25 @@ namespace expr {
 const int NodeSetDepth::s_iosIndex = std::ios_base::xalloc();
 
 }/* CVC4::expr namespace */
+
+
+TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node, std::string message)
+: Exception(message), d_node(new Node(node))
+{
+}
+
+TypeCheckingExceptionPrivate::~TypeCheckingExceptionPrivate() throw () {
+  delete d_node;
+}
+
+std::string TypeCheckingExceptionPrivate::toString() const {
+  std::stringstream ss;
+  ss << "Error type-checking " << d_node << ": " << d_msg;
+  return ss.str();
+}
+
+Node TypeCheckingExceptionPrivate::getNode() const {
+  return *d_node;
+}
+
 }/* CVC4 namespace */
diff --git a/src/expr/node.h b/src/expr/node.h
index f8d9117c7..d3e8792ed 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -26,8 +26,10 @@
 #include <iostream>
 #include <stdint.h>
 
+#include "type.h"
 #include "expr/kind.h"
 #include "expr/metakind.h"
+#include "expr/expr.h"
 #include "util/Assert.h"
 #include "util/output.h"
 
@@ -40,6 +42,43 @@ template <bool ref_count>
 class NodeTemplate;
 
 /**
+ * Exception thrown during the type-checking phase, it can be
+ * thrown by node.getType().
+ */
+class TypeCheckingExceptionPrivate : public Exception {
+
+private:
+
+  /** The node repsonsible for the failure */
+  NodeTemplate<true>* d_node;
+
+protected:
+
+  TypeCheckingExceptionPrivate(): Exception() {}
+
+public:
+
+  /**
+   * Construct the exception with the problematic node and the message
+   * @param node the problematic node
+   * @param message the message explaining the failure
+   */
+  TypeCheckingExceptionPrivate(NodeTemplate<false> node, std::string message);
+
+  /** Destructor */
+  ~TypeCheckingExceptionPrivate() throw ();
+
+  /**
+   * Get the Node that caused the type-checking to fail.
+   * @return the node
+   */
+  NodeTemplate<true> getNode() const;
+
+  /** Returns the message corresponding to the type-checking failure */
+  std::string toString() const;
+};
+
+/**
  * The Node class encapsulates the NodeValue with reference counting.
  */
 typedef NodeTemplate<true> Node;
@@ -247,7 +286,7 @@ public:
    * Returns the type of this node.
    * @return the type
    */
-  TypeNode getType() const;
+  TypeNode getType() const throw (CVC4::TypeCheckingExceptionPrivate);
 
   /**
    * Returns the kind of this node.
@@ -814,7 +853,7 @@ inline bool NodeTemplate<ref_count>::hasOperator() const {
 }
 
 template <bool ref_count>
-TypeNode NodeTemplate<ref_count>::getType() const {
+TypeNode NodeTemplate<ref_count>::getType() const throw (CVC4::TypeCheckingExceptionPrivate) {
   Assert( NodeManager::currentNM() != NULL,
           "There is no current CVC4::NodeManager associated to this thread.\n"
           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 4f0e0ff76..171c75186 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -17,6 +17,12 @@
 
 #include "node_manager.h"
 
+#include "expr/builtin_type_rules.h"
+#include "theory/booleans/theory_bool_type_rules.h"
+#include "theory/uf/theory_uf_type_rules.h"
+#include "theory/arith/theory_arith_type_rules.h"
+#include "theory/bv/theory_bv_type_rules.h"
+
 #include <ext/hash_set>
 
 using namespace std;
@@ -169,4 +175,189 @@ void NodeManager::reclaimZombies() {
   }
 }/* NodeManager::reclaimZombies() */
 
+TypeNode NodeManager::getType(TNode n) throw (TypeCheckingExceptionPrivate) {
+  TypeNode typeNode;
+  bool hasType = getAttribute(n, TypeAttr(), typeNode);
+  if (!hasType) {
+    // Infer the type
+    switch (n.getKind()) {
+    case kind::EQUAL:
+      typeNode = CVC4::EqualityTypeRule::computeType(this, n);
+      break;
+    case kind::DISTINCT:
+      typeNode = CVC4::DistinctTypeRule::computeType(this, n);
+      break;
+    case kind::CONST_BOOLEAN:
+      typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n);
+      break;
+    case kind::NOT:
+      typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n);
+      break;
+    case kind::AND:
+      typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n);
+      break;
+    case kind::IFF:
+      typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n);
+      break;
+    case kind::IMPLIES:
+      typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n);
+      break;
+    case kind::OR:
+      typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n);
+      break;
+    case kind::XOR:
+      typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n);
+      break;
+    case kind::ITE:
+      typeNode = CVC4::theory::boolean::IteTypeRule::computeType(this, n);
+      break;
+    case kind::APPLY_UF:
+      typeNode = CVC4::theory::uf::UfTypeRule::computeType(this, n);
+      break;
+    case kind::PLUS:
+      typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n);
+      break;
+    case kind::MULT:
+      typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n);
+      break;
+    case kind::MINUS:
+      typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n);
+      break;
+    case kind::UMINUS:
+      typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n);
+      break;
+    case kind::CONST_RATIONAL:
+      typeNode = CVC4::theory::arith::ArithConstantTypeRule::computeType(this, n);
+      break;
+    case kind::CONST_INTEGER:
+      typeNode = CVC4::theory::arith::ArithConstantTypeRule::computeType(this, n);
+      break;
+    case kind::LT:
+      typeNode = CVC4::theory::arith::ArithPredicateTypeRule::computeType(this, n);
+      break;
+    case kind::LEQ:
+      typeNode = CVC4::theory::arith::ArithPredicateTypeRule::computeType(this, n);
+      break;
+    case kind::GT:
+      typeNode = CVC4::theory::arith::ArithPredicateTypeRule::computeType(this, n);
+      break;
+    case kind::GEQ:
+      typeNode = CVC4::theory::arith::ArithPredicateTypeRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_CONST:
+      typeNode = CVC4::theory::bv::BitVectorConstantTypeRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_AND:
+      typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_OR:
+      typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_XOR:
+      typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_NOT:
+      typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_NAND:
+      typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_NOR:
+      typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_XNOR:
+      typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_COMP:
+      typeNode = CVC4::theory::bv::BitVectorCompRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_MULT:
+      typeNode = CVC4::theory::bv::BitVectorArithRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_PLUS:
+      typeNode = CVC4::theory::bv::BitVectorArithRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_SUB:
+      typeNode = CVC4::theory::bv::BitVectorArithRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_NEG:
+      typeNode = CVC4::theory::bv::BitVectorArithRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_UDIV:
+      typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_UREM:
+      typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_SDIV:
+      typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_SREM:
+      typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_SMOD:
+      typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_SHL:
+      typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_LSHR:
+      typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_ASHR:
+      typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_ROTATE_LEFT:
+      typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_ROTATE_RIGHT:
+      typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_ULT:
+      typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_ULE:
+      typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_UGT:
+      typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_UGE:
+      typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_SLT:
+      typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_SLE:
+      typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_SGT:
+      typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_SGE:
+      typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_EXTRACT:
+      typeNode = CVC4::theory::bv::BitVectorExtractTypeRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_CONCAT:
+      typeNode = CVC4::theory::bv::BitVectorConcatRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_REPEAT:
+      typeNode = CVC4::theory::bv::BitVectorRepeatTypeRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_ZERO_EXTEND:
+      typeNode = CVC4::theory::bv::BitVectorExtendTypeRule::computeType(this, n);
+      break;
+    case kind::BITVECTOR_SIGN_EXTEND:
+      typeNode = CVC4::theory::bv::BitVectorExtendTypeRule::computeType(this, n);
+      break;
+    default:
+     Unimplemented();
+    }
+    setAttribute(n, TypeAttr(), typeNode);
+  }
+  return typeNode;
+}
+
 }/* CVC4 namespace */
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 5cb19bc89..53abdb703 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -21,6 +21,7 @@
 #include "expr/attribute.h"
 #include "expr/node.h"
 #include "expr/type_node.h"
+#include "expr/expr.h"
 
 #ifndef __CVC4__NODE_MANAGER_H
 #define __CVC4__NODE_MANAGER_H
@@ -507,7 +508,7 @@ public:
   /**
    * Get the type for the given node.
    */
-  inline TypeNode getType(TNode n);
+  TypeNode getType(TNode n) throw (TypeCheckingExceptionPrivate);
 
   /**
    * Returns true if this node is atomic (has no more Boolean structure)
@@ -673,13 +674,6 @@ NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) {
   return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
 }
 
-inline TypeNode NodeManager::getType(TNode n)  {
-  TypeNode typeNode;
-  getAttribute(n, TypeAttr(), typeNode);
-  // TODO: Type computation
-  return typeNode;
-}
-
 inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const {
   NodeValuePool::const_iterator find = d_nodeValuePool.find(nv);
   if(find == d_nodeValuePool.end()) {
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index faadfb0a6..521e177d3 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -14,6 +14,7 @@
  **/
 
 #include "expr/node_manager.h"
+#include "expr/expr_manager.h"
 #include "expr/type.h"
 #include "expr/type_node.h"
 #include "expr/type_constant.h"
diff --git a/src/expr/type.h b/src/expr/type.h
index f513ef5de..137dbfff3 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -29,7 +29,10 @@
 namespace CVC4 {
 
 class NodeManager;
+class ExprManager;
 class TypeNode;
+template <bool ref_count>
+class NodeTemplate;
 
 class BooleanType;
 class IntegerType;
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_ */
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 1ab13230b..879680fd7 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -83,6 +83,10 @@ public:
   std::string toString(unsigned int base = 2) const {
     return d_value.get_str(base);
   }
+
+  unsigned getSize() const {
+    return d_size;
+  }
 };
 
 /**
diff --git a/src/util/exception.h b/src/util/exception.h
index 862597bae..48dcf1244 100644
--- a/src/util/exception.h
+++ b/src/util/exception.h
@@ -34,7 +34,8 @@ public:
   virtual ~Exception() throw() {}
   // NON-VIRTUAL METHOD for setting and printing the error message
   void setMessage(const std::string& msg) { d_msg = msg; }
-  // Printing: feel free to redefine toString().  When inherited,
+  std::string getMessage() const { return d_msg; }
+    // Printing: feel free to redefine toString().  When inherited,
   // it's recommended that this method print the type of exception
   // before the actual message.
   virtual std::string toString() const { return d_msg; }