From e2aa4e37c93749bd186071e38874a7ba5a70b97e Mon Sep 17 00:00:00 2001 From: Tim King Date: Mon, 8 Jan 2018 07:49:23 -0800 Subject: Remove throw specifiers from datatype. (#1489) --- src/expr/datatype.cpp | 15 ++++-- src/expr/datatype.h | 140 ++++++++++++++++++++++++-------------------------- 2 files changed, 78 insertions(+), 77 deletions(-) (limited to 'src/expr') diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index f96066e80..8f5b503fe 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -520,7 +520,8 @@ DatatypeType Datatype::getDatatypeType(const std::vector& params) return DatatypeType(d_self).instantiate(params); } -bool Datatype::operator==(const Datatype& other) const throw() { +bool Datatype::operator==(const Datatype& other) const +{ // two datatypes are == iff the name is the same and they have // exactly matching constructors (in the same order) @@ -840,11 +841,13 @@ void DatatypeConstructor::addArg(std::string selectorName, DatatypeSelfType) { d_args.push_back(DatatypeConstructorArg(selectorName + '\0', Expr())); } -std::string DatatypeConstructor::getName() const throw() { +std::string DatatypeConstructor::getName() const +{ return d_name.substr(0, d_name.find('\0')); } -std::string DatatypeConstructor::getTesterName() const throw() { +std::string DatatypeConstructor::getTesterName() const +{ return d_name.substr(d_name.find('\0') + 1); } @@ -1134,7 +1137,8 @@ DatatypeConstructorArg::DatatypeConstructorArg(std::string name, Expr selector) PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor arg without a name"); } -std::string DatatypeConstructorArg::getName() const throw() { +std::string DatatypeConstructorArg::getName() const +{ string name = d_name; const size_t nul = name.find('\0'); if(nul != string::npos) { @@ -1193,7 +1197,8 @@ Type DatatypeConstructorArg::getRangeType() const { return getType().getRangeType(); } -bool DatatypeConstructorArg::isUnresolvedSelf() const throw() { +bool DatatypeConstructorArg::isUnresolvedSelf() const +{ return d_selector.isNull() && d_name.size() == d_name.find('\0') + 1; } diff --git a/src/expr/datatype.h b/src/expr/datatype.h index b3c81911f..59941f174 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -113,7 +113,7 @@ class CVC4_PUBLIC DatatypeUnresolvedType { std::string d_name; public: inline DatatypeUnresolvedType(std::string name); - inline std::string getName() const throw(); + inline std::string getName() const; };/* class DatatypeUnresolvedType */ /** @@ -122,10 +122,10 @@ public: class CVC4_PUBLIC DatatypeConstructorArg { friend class DatatypeConstructor; friend class Datatype; -public: + public: /** Get the name of this constructor argument. */ - std::string getName() const throw(); + std::string getName() const; /** * Get the selector for this constructor argument; this call is @@ -161,7 +161,7 @@ public: /** * Returns true iff this constructor argument has been resolved. */ - bool isResolved() const throw(); + bool isResolved() const; private: /** the name of this selector */ @@ -173,7 +173,7 @@ public: /** whether this class has been resolved */ bool d_resolved; /** is this selector unresolved? */ - bool isUnresolvedSelf() const throw(); + bool isUnresolvedSelf() const; /** constructor */ DatatypeConstructorArg(std::string name, Expr selector); };/* class DatatypeConstructorArg */ @@ -269,7 +269,7 @@ class CVC4_PUBLIC DatatypeConstructor { void addArg(std::string selectorName, DatatypeSelfType); /** Get the name of this Datatype constructor. */ - std::string getName() const throw(); + std::string getName() const; /** * Get the constructor operator of this Datatype constructor. The @@ -317,12 +317,12 @@ class CVC4_PUBLIC DatatypeConstructor { /** * Get the tester name for this Datatype constructor. */ - std::string getTesterName() const throw(); + std::string getTesterName() const; /** * Get the number of arguments (so far) of this Datatype constructor. */ - inline size_t getNumArgs() const throw(); + inline size_t getNumArgs() const; /** * Get the specialized constructor type for a parametric @@ -362,16 +362,16 @@ class CVC4_PUBLIC DatatypeConstructor { * Returns true iff this Datatype constructor has already been * resolved. */ - inline bool isResolved() const throw(); + inline bool isResolved() const; /** Get the beginning iterator over DatatypeConstructor args. */ - inline iterator begin() throw(); + inline iterator begin(); /** Get the ending iterator over DatatypeConstructor args. */ - inline iterator end() throw(); + inline iterator end(); /** Get the beginning const_iterator over DatatypeConstructor args. */ - inline const_iterator begin() const throw(); + inline const_iterator begin() const; /** Get the ending const_iterator over DatatypeConstructor args. */ - inline const_iterator end() const throw(); + inline const_iterator end() const; /** Get the ith DatatypeConstructor arg. */ const DatatypeConstructorArg& operator[](size_t index) const; @@ -692,16 +692,16 @@ public: void setRecord(); /** Get the name of this Datatype. */ - inline std::string getName() const throw(); + inline std::string getName() const; /** Get the number of constructors (so far) for this Datatype. */ - inline size_t getNumConstructors() const throw(); + inline size_t getNumConstructors() const; /** Is this datatype parametric? */ - inline bool isParametric() const throw(); + inline bool isParametric() const; /** Get the nubmer of type parameters */ - inline size_t getNumParameters() const throw(); + inline size_t getNumParameters() const; /** Get parameter */ inline Type getParameter( unsigned int i ) const; @@ -836,21 +836,21 @@ public: * RB tree directly, so maybe we can consider adding these * comparison operators later on. */ - bool operator==(const Datatype& other) const throw(); + bool operator==(const Datatype& other) const; /** Return true iff the two Datatypes are not the same. */ - inline bool operator!=(const Datatype& other) const throw(); + inline bool operator!=(const Datatype& other) const; /** Return true iff this Datatype has already been resolved. */ - inline bool isResolved() const throw(); + inline bool isResolved() const; /** Get the beginning iterator over DatatypeConstructors. */ - inline iterator begin() throw(); + inline iterator begin(); /** Get the ending iterator over DatatypeConstructors. */ - inline iterator end() throw(); + inline iterator end(); /** Get the beginning const_iterator over DatatypeConstructors. */ - inline const_iterator begin() const throw(); + inline const_iterator begin() const; /** Get the ending const_iterator over DatatypeConstructors. */ - inline const_iterator end() const throw(); + inline const_iterator end() const; /** Get the ith DatatypeConstructor. */ const DatatypeConstructor& operator[](size_t index) const; @@ -1085,27 +1085,30 @@ public: DatatypeIndexConstant(unsigned index) throw(IllegalArgumentException); - ~DatatypeIndexConstant() throw() { } - - const unsigned getIndex() const throw() { - return d_index; - } - bool operator==(const DatatypeIndexConstant& uc) const throw() { + ~DatatypeIndexConstant() {} + const unsigned getIndex() const { return d_index; } + bool operator==(const DatatypeIndexConstant& uc) const + { return d_index == uc.d_index; } - bool operator!=(const DatatypeIndexConstant& uc) const throw() { + bool operator!=(const DatatypeIndexConstant& uc) const + { return !(*this == uc); } - bool operator<(const DatatypeIndexConstant& uc) const throw() { + bool operator<(const DatatypeIndexConstant& uc) const + { return d_index < uc.d_index; } - bool operator<=(const DatatypeIndexConstant& uc) const throw() { + bool operator<=(const DatatypeIndexConstant& uc) const + { return d_index <= uc.d_index; } - bool operator>(const DatatypeIndexConstant& uc) const throw() { + bool operator>(const DatatypeIndexConstant& uc) const + { return !(*this <= uc); } - bool operator>=(const DatatypeIndexConstant& uc) const throw() { + bool operator>=(const DatatypeIndexConstant& uc) const + { return !(*this < uc); } private: @@ -1138,10 +1141,7 @@ inline DatatypeUnresolvedType::DatatypeUnresolvedType(std::string name) : d_name(name) { } -inline std::string DatatypeUnresolvedType::getName() const throw() { - return d_name; -} - +inline std::string DatatypeUnresolvedType::getName() const { return d_name; } inline Datatype::Datatype(std::string name, bool isCo) : d_name(name), d_params(), @@ -1177,22 +1177,14 @@ inline Datatype::Datatype(std::string name, const std::vector& params, d_card(CardinalityUnknown()), d_well_founded(0) {} -inline std::string Datatype::getName() const throw() { - return d_name; -} - -inline size_t Datatype::getNumConstructors() const throw() { +inline std::string Datatype::getName() const { return d_name; } +inline size_t Datatype::getNumConstructors() const +{ return d_constructors.size(); } -inline bool Datatype::isParametric() const throw() { - return d_params.size() > 0; -} - -inline size_t Datatype::getNumParameters() const throw() { - return d_params.size(); -} - +inline bool Datatype::isParametric() const { return d_params.size() > 0; } +inline size_t Datatype::getNumParameters() const { return d_params.size(); } inline Type Datatype::getParameter( unsigned int i ) const { CheckArgument(isParametric(), this, "Cannot get type parameter of a non-parametric datatype."); @@ -1226,40 +1218,40 @@ inline bool Datatype::isRecord() const { inline Record * Datatype::getRecord() const { return d_record; } - -inline bool Datatype::operator!=(const Datatype& other) const throw() { +inline bool Datatype::operator!=(const Datatype& other) const +{ return !(*this == other); } -inline bool Datatype::isResolved() const throw() { - return d_resolved; -} - -inline Datatype::iterator Datatype::begin() throw() { +inline bool Datatype::isResolved() const { return d_resolved; } +inline Datatype::iterator Datatype::begin() +{ return iterator(d_constructors, true); } -inline Datatype::iterator Datatype::end() throw() { +inline Datatype::iterator Datatype::end() +{ return iterator(d_constructors, false); } -inline Datatype::const_iterator Datatype::begin() const throw() { +inline Datatype::const_iterator Datatype::begin() const +{ return const_iterator(d_constructors, true); } -inline Datatype::const_iterator Datatype::end() const throw() { +inline Datatype::const_iterator Datatype::end() const +{ return const_iterator(d_constructors, false); } -inline bool DatatypeConstructor::isResolved() const throw() { +inline bool DatatypeConstructor::isResolved() const +{ return !d_tester.isNull(); } -inline size_t DatatypeConstructor::getNumArgs() const throw() { - return d_args.size(); -} - -inline bool DatatypeConstructorArg::isResolved() const throw() { +inline size_t DatatypeConstructor::getNumArgs() const { return d_args.size(); } +inline bool DatatypeConstructorArg::isResolved() const +{ // We could just write: // // return !d_selector.isNull() && d_selector.getType().isSelector(); @@ -1276,19 +1268,23 @@ inline bool DatatypeConstructorArg::isResolved() const throw() { return d_resolved; } -inline DatatypeConstructor::iterator DatatypeConstructor::begin() throw() { +inline DatatypeConstructor::iterator DatatypeConstructor::begin() +{ return iterator(d_args, true); } -inline DatatypeConstructor::iterator DatatypeConstructor::end() throw() { +inline DatatypeConstructor::iterator DatatypeConstructor::end() +{ return iterator(d_args, false); } -inline DatatypeConstructor::const_iterator DatatypeConstructor::begin() const throw() { +inline DatatypeConstructor::const_iterator DatatypeConstructor::begin() const +{ return const_iterator(d_args, true); } -inline DatatypeConstructor::const_iterator DatatypeConstructor::end() const throw() { +inline DatatypeConstructor::const_iterator DatatypeConstructor::end() const +{ return const_iterator(d_args, false); } -- cgit v1.2.3