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/expr_manager_template.cpp | |
parent | 4538f5fe95758f2507c191ab39175491f24e6f67 (diff) |
Removes yet more throw specifiers. Updating the documentation as needed. (#1518)
Diffstat (limited to 'src/expr/expr_manager_template.cpp')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 10 |
1 files changed, 6 insertions, 4 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); } |