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

1 files changed, 37 insertions, 5 deletions

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.