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 | |
parent | 4538f5fe95758f2507c191ab39175491f24e6f67 (diff) |
Removes yet more throw specifiers. Updating the documentation as needed. (#1518)
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 10 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 14 | ||||
-rw-r--r-- | src/expr/expr_template.cpp | 13 | ||||
-rw-r--r-- | src/expr/expr_template.h | 8 | ||||
-rw-r--r-- | src/expr/node.h | 10 | ||||
-rw-r--r-- | src/expr/node_builder.h | 9 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 3 | ||||
-rw-r--r-- | src/expr/node_manager.h | 3 |
8 files changed, 36 insertions, 34 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index bc4205217..951b92e1c 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -869,7 +869,8 @@ SortConstructorType ExprManager::mkSortConstructor(const std::string& name, * @param check whether we should check the type as we compute it * (default: false) */ -Type ExprManager::getType(Expr e, bool check) throw (TypeCheckingException) { +Type ExprManager::getType(Expr e, bool check) +{ NodeManagerScope nms(d_nodeManager); Type t; try { @@ -995,12 +996,13 @@ unsigned ExprManager::maxArity(Kind kind) { NodeManager* ExprManager::getNodeManager() const { return d_nodeManager; } - -Statistics ExprManager::getStatistics() const throw() { +Statistics ExprManager::getStatistics() const +{ return Statistics(*d_nodeManager->getStatisticsRegistry()); } -SExpr ExprManager::getStatistic(const std::string& name) const throw() { +SExpr ExprManager::getStatistic(const std::string& name) const +{ return d_nodeManager->getStatisticsRegistry()->getStatistic(name); } diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 35a3b6a6e..5adb30ad6 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -436,9 +436,13 @@ public: SortConstructorType mkSortConstructor(const std::string& name, size_t arity) const; - /** Get the type of an expression */ - Type getType(Expr e, bool check = false) - throw(TypeCheckingException); + /** + * Get the type of an expression. + * + * Throws a TypeCheckingException on failures or if a Type cannot be + * computed. + */ + Type getType(Expr e, bool check = false); /** Bits for use in mkVar() flags. */ enum { @@ -524,10 +528,10 @@ public: Expr mkNullaryOperator( Type type, Kind k); /** Get a reference to the statistics registry for this ExprManager */ - Statistics getStatistics() const throw(); + Statistics getStatistics() const; /** Get a reference to the statistics registry for this ExprManager */ - SExpr getStatistic(const std::string& name) const throw(); + SExpr getStatistic(const std::string& name) const; /** * Flushes statistics for this ExprManager to a file descriptor. Safe to use diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 0ed3601fc..f4dd294a7 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -337,7 +337,8 @@ Expr Expr::getOperator() const { return Expr(d_exprManager, new Node(d_node->getOperator())); } -Type Expr::getType(bool check) const throw (TypeCheckingException) { +Type Expr::getType(bool check) const +{ ExprManagerScope ems(*this); Assert(d_node != NULL, "Unexpected NULL expression pointer!"); PrettyCheckArgument(!d_node->isNull(), this, @@ -499,14 +500,8 @@ void Expr::toStream(std::ostream& out, int depth, bool types, size_t dag, d_node->toStream(out, depth, types, dag, language); } -Node Expr::getNode() const throw() { - return *d_node; -} - -TNode Expr::getTNode() const throw() { - return *d_node; -} - +Node Expr::getNode() const { return *d_node; } +TNode Expr::getTNode() const { return *d_node; } Expr Expr::notExpr() const { Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!"); diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 9656781a8..cc9949c30 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -409,7 +409,7 @@ public: * @param check whether we should check the type as we compute it * (default: false) */ - Type getType(bool check = false) const throw (TypeCheckingException); + Type getType(bool check = false) const; /** * Substitute "replacement" in for "e". @@ -521,13 +521,13 @@ private: * Returns the actual internal node. * @return the internal node */ - NodeTemplate<true> getNode() const throw(); + NodeTemplate<true> getNode() const; /** * Returns the actual internal node as a TNode. * @return the internal node */ - NodeTemplate<false> getTNode() const throw(); + NodeTemplate<false> getTNode() const; // Friend to access the actual internal expr information and private methods friend class SmtEngine; @@ -545,7 +545,7 @@ private: ${getConst_instantiations} -#line 557 "${template}" +#line 549 "${template}" inline size_t ExprHashFunction::operator()(CVC4::Expr e) const { return (size_t) e.getId(); diff --git a/src/expr/node.h b/src/expr/node.h index fd3d20afa..92f905c8b 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -228,7 +228,10 @@ class NodeTemplate { */ void assignNodeValue(expr::NodeValue* ev); - inline void assertTNodeNotExpired() const throw(AssertionException) { + // May throw an AssertionException if the Node is not live, i.e. the ref count + // is not positive. + inline void assertTNodeNotExpired() const + { if(!ref_count) { Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" ); } @@ -525,8 +528,7 @@ public: * @param check whether we should check the type as we compute it * (default: false) */ - TypeNode getType(bool check = false) const - throw (CVC4::TypeCheckingExceptionPrivate, CVC4::AssertionException); + TypeNode getType(bool check = false) const; /** * Substitution of Nodes. @@ -1271,7 +1273,7 @@ inline bool NodeTemplate<ref_count>::hasOperator() const { template <bool ref_count> 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" "Perhaps a public-facing function is missing a NodeManagerScope ?" ); 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] ) { diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 85f5e3c75..3c79e96f2 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -400,8 +400,7 @@ std::vector<NodeValue*> NodeManager::TopologicalSort( } /* NodeManager::TopologicalSort() */ TypeNode NodeManager::getType(TNode n, bool check) - throw(TypeCheckingExceptionPrivate, AssertionException) { - +{ // Many theories' type checkers call Node::getType() directly. This // is incorrect, since "this" might not be the caller's curent node // manager. Rather than force the individual typecheckers not to do diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index d9345a5f5..e1ba28be9 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -902,8 +902,7 @@ public: * @param check whether we should check the type as we compute it * (default: false) */ - TypeNode getType(TNode n, bool check = false) - throw(TypeCheckingExceptionPrivate, AssertionException); + TypeNode getType(TNode n, bool check = false); /** * Convert a node to an expression. Uses the ExprManager |