diff options
| author | Tim King <taking@cs.nyu.edu> | 2018-01-17 12:16:17 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-01-17 12:16:17 -0800 |
| commit | 248b977790b429ebfd22481462193e3e35c57ce2 (patch) | |
| tree | 9a59a408d113d6a3347f013c2492291769406e82 /src/expr/node_builder.h | |
| parent | 4538f5fe95758f2507c191ab39175491f24e6f67 (diff) | |
Removes yet more throw specifiers. Updating the documentation as needed. (#1518)
Diffstat (limited to 'src/expr/node_builder.h')
| -rw-r--r-- | src/expr/node_builder.h | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 45ac02f10..b0fdd0657 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -687,10 +687,11 @@ private: expr::NodeValue* constructNV() const; #ifdef CVC4_DEBUG - void maybeCheckType(const TNode n) const - throw(TypeCheckingExceptionPrivate, AssertionException); + // Throws a TypeCheckingExceptionPrivate on a failure. + void maybeCheckType(const TNode n) const; #else /* CVC4_DEBUG */ - inline void maybeCheckType(const TNode n) const throw() { } + // Do nothing if not in debug mode. + inline void maybeCheckType(const TNode n) const {} #endif /* CVC4_DEBUG */ public: @@ -1320,7 +1321,7 @@ void NodeBuilder<nchild_thresh>::internalCopy(const NodeBuilder<N>& nb) { #ifdef CVC4_DEBUG template <unsigned nchild_thresh> inline void NodeBuilder<nchild_thresh>::maybeCheckType(const TNode n) const - throw(TypeCheckingExceptionPrivate, AssertionException) { +{ /* force an immediate type check, if early type checking is enabled and the current node isn't a variable or constant */ if( d_nm->getOptions()[options::earlyTypeChecking] ) { |