diff options
author | Tim King <taking@cs.nyu.edu> | 2018-01-09 06:20:52 -0800 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-01-09 08:20:51 -0600 |
commit | e6c966990ee7d166c421b6ba8ec39ac2e05ee62a (patch) | |
tree | 4310e1345ed7b5a536dd545ddd772c26cd7c1e31 /src/expr/uninterpreted_constant.h | |
parent | 3c6398194b01372720964590b2b07d93590e511d (diff) |
Removing throw specifiers from miscellaneous src/expr/ classes. (#1503)
Diffstat (limited to 'src/expr/uninterpreted_constant.h')
-rw-r--r-- | src/expr/uninterpreted_constant.h | 36 |
1 files changed, 17 insertions, 19 deletions
diff --git a/src/expr/uninterpreted_constant.h b/src/expr/uninterpreted_constant.h index 06747e1af..16800391c 100644 --- a/src/expr/uninterpreted_constant.h +++ b/src/expr/uninterpreted_constant.h @@ -25,42 +25,40 @@ namespace CVC4 { class CVC4_PUBLIC UninterpretedConstant { -public: + public: + UninterpretedConstant(Type type, Integer index); - UninterpretedConstant(Type type, Integer index) throw(IllegalArgumentException); - - ~UninterpretedConstant() throw() { } - - Type getType() const throw() { - return d_type; - } - const Integer& getIndex() const throw() { - return d_index; - } - - bool operator==(const UninterpretedConstant& uc) const throw() { + Type getType() const { return d_type; } + const Integer& getIndex() const { return d_index; } + bool operator==(const UninterpretedConstant& uc) const + { return d_type == uc.d_type && d_index == uc.d_index; } - bool operator!=(const UninterpretedConstant& uc) const throw() { + bool operator!=(const UninterpretedConstant& uc) const + { return !(*this == uc); } - bool operator<(const UninterpretedConstant& uc) const throw() { + bool operator<(const UninterpretedConstant& uc) const + { return d_type < uc.d_type || (d_type == uc.d_type && d_index < uc.d_index); } - bool operator<=(const UninterpretedConstant& uc) const throw() { + bool operator<=(const UninterpretedConstant& uc) const + { return d_type < uc.d_type || (d_type == uc.d_type && d_index <= uc.d_index); } - bool operator>(const UninterpretedConstant& uc) const throw() { + bool operator>(const UninterpretedConstant& uc) const + { return !(*this <= uc); } - bool operator>=(const UninterpretedConstant& uc) const throw() { + bool operator>=(const UninterpretedConstant& uc) const + { return !(*this < uc); } -private: + private: const Type d_type; const Integer d_index; };/* class UninterpretedConstant */ |