Merge branch 'master' into fix_win_gmpfix_win_gmp

2 files changed, 78 insertions, 77 deletions

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<Type>& 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<Type>& 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);
 }