diff options
Diffstat (limited to 'src/expr/node.h')
| -rw-r--r-- | src/expr/node.h | 30 |
1 files changed, 25 insertions, 5 deletions
diff --git a/src/expr/node.h b/src/expr/node.h index 218b9a3ea..4b1a0e5be 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -334,10 +334,30 @@ public: inline bool hasOperator() const; /** - * Returns the type of this node. - * @return the type + * Get the type for the node and optionally do type checking. + * + * Initial type computation will be near-constant time if + * type checking is not requested. Results are memoized, so that + * subsequent calls to getType() without type checking will be + * constant time. + * + * Initial type checking is linear in the size of the expression. + * Again, the results are memoized, so that subsequent calls to + * getType(), with or without type checking, will be constant + * time. + * + * NOTE: A TypeCheckingException can be thrown even when type + * checking is not requested. getType() will always return a + * valid and correct type and, thus, an exception will be thrown + * when no valid or correct type can be computed (e.g., if the + * arguments to a bit-vector operation aren't bit-vectors). When + * type checking is not requested, getType() will do the minimum + * amount of checking required to return a valid result. + * + * @param check whether we should check the type as we compute it + * (default: false) */ - TypeNode getType() const + TypeNode getType(bool check = false) const throw (CVC4::TypeCheckingExceptionPrivate, CVC4::AssertionException); /** @@ -893,7 +913,7 @@ inline bool NodeTemplate<ref_count>::hasOperator() const { } template <bool ref_count> -TypeNode NodeTemplate<ref_count>::getType() const +TypeNode NodeTemplate<ref_count>::getType(bool check) const throw (CVC4::TypeCheckingExceptionPrivate, CVC4::AssertionException) { Assert( NodeManager::currentNM() != NULL, "There is no current CVC4::NodeManager associated to this thread.\n" @@ -903,7 +923,7 @@ TypeNode NodeTemplate<ref_count>::getType() const Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" ); } - return NodeManager::currentNM()->getType(*this); + return NodeManager::currentNM()->getType(*this, check); } #ifdef CVC4_DEBUG |