diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-05-04 03:42:56 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-05-04 03:42:56 +0000 |
commit | 1ce8e28d5976e1ab30099cb9e6943514497d2980 (patch) | |
tree | 1a9382fb62b38e3b5768da951b7c684f1b8688e7 /src/expr/node.h | |
parent | 69c2d3e702f8ec0bd0eec4a481a07571131aabeb (diff) |
Type-checking classes and hooks (not tested yet).
Diffstat (limited to 'src/expr/node.h')
-rw-r--r-- | src/expr/node.h | 43 |
1 files changed, 41 insertions, 2 deletions
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 ?" ); |