diff options
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 |