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.h | |
parent | 4538f5fe95758f2507c191ab39175491f24e6f67 (diff) |
Removes yet more throw specifiers. Updating the documentation as needed. (#1518)
Diffstat (limited to 'src/expr/expr_manager_template.h')
-rw-r--r-- | src/expr/expr_manager_template.h | 14 |
1 files changed, 9 insertions, 5 deletions
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 |