Removing throw specifiers from Type. (#1511)

diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 8bcb0f8d542cfd1c2975a3155daa0f60c5f0f9b3..503a5802a9659a54d46a3289dcfc4ab54025b6e2 100644 (file)
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -400,93 +400,92 @@ SortType SortConstructorType::instantiate(const std::vector<Type>& params) const
   return SortType(makeType(d_nodeManager->mkSort(*d_typeNode, paramsNodes)));
 }
 
-BooleanType::BooleanType(const Type& t) throw(IllegalArgumentException) :
-  Type(t) {
+BooleanType::BooleanType(const Type& t) : Type(t)
+{
   PrettyCheckArgument(isNull() || isBoolean(), this);
 }
 
-IntegerType::IntegerType(const Type& t) throw(IllegalArgumentException) :
-  Type(t) {
+IntegerType::IntegerType(const Type& t) : Type(t)
+{
   PrettyCheckArgument(isNull() || isInteger(), this);
 }
 
-RealType::RealType(const Type& t) throw(IllegalArgumentException) :
-  Type(t) {
+RealType::RealType(const Type& t) : Type(t)
+{
   PrettyCheckArgument(isNull() || isReal(), this);
 }
 
-StringType::StringType(const Type& t) throw(IllegalArgumentException) :
-  Type(t) {
+StringType::StringType(const Type& t) : Type(t)
+{
   PrettyCheckArgument(isNull() || isString(), this);
 }
 
-RegExpType::RegExpType(const Type& t) throw(IllegalArgumentException) :
-  Type(t) {
+RegExpType::RegExpType(const Type& t) : Type(t)
+{
   PrettyCheckArgument(isNull() || isRegExp(), this);
 }
 
-RoundingModeType::RoundingModeType(const Type& t) throw(IllegalArgumentException) :
-  Type(t) {
+RoundingModeType::RoundingModeType(const Type& t) : Type(t)
+{
   PrettyCheckArgument(isNull() || isRoundingMode(), this);
 }
 
-BitVectorType::BitVectorType(const Type& t) throw(IllegalArgumentException) :
-  Type(t) {
+BitVectorType::BitVectorType(const Type& t) : Type(t)
+{
   PrettyCheckArgument(isNull() || isBitVector(), this);
 }
 
-FloatingPointType::FloatingPointType(const Type& t) throw(IllegalArgumentException) :
-  Type(t) {
+FloatingPointType::FloatingPointType(const Type& t) : Type(t)
+{
   PrettyCheckArgument(isNull() || isFloatingPoint(), this);
 }
 
-DatatypeType::DatatypeType(const Type& t) throw(IllegalArgumentException) :
-  Type(t) {
+DatatypeType::DatatypeType(const Type& t) : Type(t)
+{
   PrettyCheckArgument(isNull() || isDatatype(), this);
 }
 
-ConstructorType::ConstructorType(const Type& t) throw(IllegalArgumentException) :
-  Type(t) {
+ConstructorType::ConstructorType(const Type& t) : Type(t)
+{
   PrettyCheckArgument(isNull() || isConstructor(), this);
 }
 
-SelectorType::SelectorType(const Type& t) throw(IllegalArgumentException) :
-  Type(t) {
+SelectorType::SelectorType(const Type& t) : Type(t)
+{
   PrettyCheckArgument(isNull() || isSelector(), this);
 }
 
-TesterType::TesterType(const Type& t) throw(IllegalArgumentException)
-    : Type(t) {
+TesterType::TesterType(const Type& t) : Type(t)
+{
   PrettyCheckArgument(isNull() || isTester(), this);
 }
 
-FunctionType::FunctionType(const Type& t) throw(IllegalArgumentException)
-    : Type(t) {
+FunctionType::FunctionType(const Type& t) : Type(t)
+{
   PrettyCheckArgument(isNull() || isFunction(), this);
 }
 
-SExprType::SExprType(const Type& t) throw(IllegalArgumentException)
-    : Type(t) {
+SExprType::SExprType(const Type& t) : Type(t)
+{
   PrettyCheckArgument(isNull() || isSExpr(), this);
 }
 
-ArrayType::ArrayType(const Type& t) throw(IllegalArgumentException)
-    : Type(t) {
+ArrayType::ArrayType(const Type& t) : Type(t)
+{
   PrettyCheckArgument(isNull() || isArray(), this);
 }
 
-SetType::SetType(const Type& t) throw(IllegalArgumentException)
-    : Type(t) {
+SetType::SetType(const Type& t) : Type(t)
+{
   PrettyCheckArgument(isNull() || isSet(), this);
 }
 
-SortType::SortType(const Type& t) throw(IllegalArgumentException)
-    : Type(t) {
+SortType::SortType(const Type& t) : Type(t)
+{
   PrettyCheckArgument(isNull() || isSort(), this);
 }
 
 SortConstructorType::SortConstructorType(const Type& t)
-  throw(IllegalArgumentException)
     : Type(t) {
   PrettyCheckArgument(isNull() || isSortConstructor(), this);
 }

diff --git a/src/expr/type.h b/src/expr/type.h
index f52658a03380b1b4d59f9b3c67dea4f084b6c01d..67fece0343e745c99fd4556109abd9d697b1b775 100644 (file)
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -19,10 +19,10 @@
 #ifndef __CVC4__TYPE_H
 #define __CVC4__TYPE_H
 
+#include <climits>
+#include <cstdint>
 #include <string>
 #include <vector>
-#include <limits.h>
-#include <stdint.h>
 
 #include "util/cardinality.h"
 
@@ -114,10 +114,8 @@ protected:
   Type(NodeManager* em, TypeNode* typeNode);
 
   /** Accessor for derived classes */
-  static TypeNode* getTypeNode(const Type& t) throw() { return t.d_typeNode; }
-
-public:
-
+  static TypeNode* getTypeNode(const Type& t) { return t.d_typeNode; }
+ public:
   /** Force a virtual destructor for safety. */
   virtual ~Type();
 
@@ -382,84 +380,53 @@ public:
   std::string toString() const;
 };/* class Type */
 
-/**
- * Singleton class encapsulating the Boolean type.
- */
+/** Singleton class encapsulating the Boolean type. */
 class CVC4_PUBLIC BooleanType : public Type {
-
-public:
-
+ public:
   /** Construct from the base type */
-  BooleanType(const Type& type = Type()) throw(IllegalArgumentException);
+  BooleanType(const Type& type = Type());
 };/* class BooleanType */
 
-/**
- * Singleton class encapsulating the integer type.
- */
+/** Singleton class encapsulating the integer type. */
 class CVC4_PUBLIC IntegerType : public Type {
-
-public:
-
+ public:
   /** Construct from the base type */
-  IntegerType(const Type& type = Type()) throw(IllegalArgumentException);
+  IntegerType(const Type& type = Type());
 };/* class IntegerType */
 
-/**
- * Singleton class encapsulating the real type.
- */
+/** Singleton class encapsulating the real type. */
 class CVC4_PUBLIC RealType : public Type {
-
-public:
-
+ public:
   /** Construct from the base type */
-  RealType(const Type& type = Type()) throw(IllegalArgumentException);
+  RealType(const Type& type = Type());
 };/* class RealType */
 
-/**
- * Singleton class encapsulating the string type.
- */
+/** Singleton class encapsulating the string type. */
 class CVC4_PUBLIC StringType : public Type {
-
-public:
-
+ public:
   /** Construct from the base type */
-  StringType(const Type& type) throw(IllegalArgumentException);
+  StringType(const Type& type);
 };/* class StringType */
 
-/**
- * Singleton class encapsulating the string type.
- */
+/** Singleton class encapsulating the string type. */
 class CVC4_PUBLIC RegExpType : public Type {
-
-public:
-
+ public:
   /** Construct from the base type */
-  RegExpType(const Type& type) throw(IllegalArgumentException);
+  RegExpType(const Type& type);
 };/* class RegExpType */
 
-
-/**
- * Singleton class encapsulating the rounding mode type.
- */
+/** Singleton class encapsulating the rounding mode type. */
 class CVC4_PUBLIC RoundingModeType : public Type {
-
-public:
-
+ public:
   /** Construct from the base type */
-  RoundingModeType(const Type& type = Type()) throw(IllegalArgumentException);
+  RoundingModeType(const Type& type = Type());
 };/* class RoundingModeType */
 
-
-
-/**
- * Class encapsulating a function type.
- */
+/** Class encapsulating a function type. */
 class CVC4_PUBLIC FunctionType : public Type {
-
-public:
-
+ public:
   /** Construct from the base type */
-  FunctionType(const Type& type = Type()) throw(IllegalArgumentException);
+  FunctionType(const Type& type = Type());
 
   /** Get the arity of the function type */
   size_t getArity() const;
@@ -471,29 +438,21 @@ public:
   Type getRangeType() const;
 };/* class FunctionType */
 
-/**
- * Class encapsulating a sexpr type.
- */
+/** Class encapsulating a sexpr type. */
 class CVC4_PUBLIC SExprType : public Type {
-
-public:
-
+ public:
   /** Construct from the base type */
-  SExprType(const Type& type = Type()) throw(IllegalArgumentException);
+  SExprType(const Type& type = Type());
 
   /** Get the constituent types */
   std::vector<Type> getTypes() const;
 };/* class SExprType */
 
-/**
- * Class encapsulating an array type.
- */
+/** Class encapsulating an array type. */
 class CVC4_PUBLIC ArrayType : public Type {
-
-public:
-
+ public:
   /** Construct from the base type */
-  ArrayType(const Type& type = Type()) throw(IllegalArgumentException);
+  ArrayType(const Type& type = Type());
 
   /** Get the index type */
   Type getIndexType() const;
@@ -502,29 +461,21 @@ public:
   Type getConstituentType() const;
 };/* class ArrayType */
 
-/**
- * Class encapsulating an set type.
- */
+/** Class encapsulating an set type. */
 class CVC4_PUBLIC SetType : public Type {
-
-public:
-
+ public:
   /** Construct from the base type */
-  SetType(const Type& type = Type()) throw(IllegalArgumentException);
+  SetType(const Type& type = Type());
 
   /** Get the index type */
   Type getElementType() const;
 };/* class SetType */
 
-/**
- * Class encapsulating a user-defined sort.
- */
+/** Class encapsulating a user-defined sort. */
 class CVC4_PUBLIC SortType : public Type {
-
-public:
-
+ public:
   /** Construct from the base type */
-  SortType(const Type& type = Type()) throw(IllegalArgumentException);
+  SortType(const Type& type = Type());
 
   /** Get the name of the sort */
   std::string getName() const;
@@ -537,15 +488,11 @@ public:
 
 };/* class SortType */
 
-/**
- * Class encapsulating a user-defined sort constructor.
- */
+/** Class encapsulating a user-defined sort constructor. */
 class CVC4_PUBLIC SortConstructorType : public Type {
-
-public:
-
+ public:
   /** Construct from the base type */
-  SortConstructorType(const Type& type = Type()) throw(IllegalArgumentException);
+  SortConstructorType(const Type& type = Type());
 
   /** Get the name of the sort constructor */
   std::string getName() const;
@@ -558,39 +505,11 @@ public:
 
 };/* class SortConstructorType */
 
-// not in release 1.0
-#if 0
-/**
- * Class encapsulating a predicate subtype.
- */
-class CVC4_PUBLIC PredicateSubtype : public Type {
-
-public:
-
-  /** Construct from the base type */
-  PredicateSubtype(const Type& type = Type()) throw(IllegalArgumentException);
-
-  /** Get the LAMBDA defining this predicate subtype */
-  Expr getPredicate() const;
-
-  /**
-   * Get the parent type of this predicate subtype; note that this
-   * could be another predicate subtype.
-   */
-  Type getParentType() const;
-
-};/* class PredicateSubtype */
-#endif /* 0 */
-
-/**
- * Class encapsulating the bit-vector type.
- */
+/** Class encapsulating the bit-vector type. */
 class CVC4_PUBLIC BitVectorType : public Type {
-
-public:
-
+ public:
   /** Construct from the base type */
-  BitVectorType(const Type& type = Type()) throw(IllegalArgumentException);
+  BitVectorType(const Type& type = Type());
 
   /**
    * Returns the size of the bit-vector type.
@@ -600,16 +519,11 @@ public:
 
 };/* class BitVectorType */
 
-
-/**
- * Class encapsulating the floating point type.
- */
+/** Class encapsulating the floating point type. */
 class CVC4_PUBLIC FloatingPointType : public Type {
-
-public:
-
+ public:
   /** Construct from the base type */
-  FloatingPointType(const Type& type = Type()) throw(IllegalArgumentException);
+  FloatingPointType(const Type& type = Type());
 
   /**
    * Returns the size of the floating-point exponent type.
@@ -625,16 +539,11 @@ public:
 
 };/* class FloatingPointType */
 
-
-/**
- * Class encapsulating the datatype type
- */
+/** Class encapsulating the datatype type */
 class CVC4_PUBLIC DatatypeType : public Type {
-
-public:
-
+ public:
   /** Construct from the base type */
-  DatatypeType(const Type& type = Type()) throw(IllegalArgumentException);
+  DatatypeType(const Type& type = Type());
 
   /** Get the underlying datatype */
   const Datatype& getDatatype() const;
@@ -656,9 +565,7 @@ public:
    */
   bool isInstantiated() const;
 
-  /**
-   * Has this datatype been instantiated for parameter N ?
-   */
+  /** Has this datatype been instantiated for parameter `n` ? */
   bool isParameterInstantiated(unsigned n) const;
 
   /** Get the parameter types */
@@ -681,15 +588,11 @@ public:
 
 };/* class DatatypeType */
 
-/**
- * Class encapsulating the constructor type
- */
+/** Class encapsulating the constructor type. */
 class CVC4_PUBLIC ConstructorType : public Type {
-
-public:
-
+ public:
   /** Construct from the base type */
-  ConstructorType(const Type& type = Type()) throw(IllegalArgumentException);
+  ConstructorType(const Type& type = Type());
 
   /** Get the range type */
   DatatypeType getRangeType() const;
@@ -702,16 +605,11 @@ public:
 
 };/* class ConstructorType */
 
-
-/**
- * Class encapsulating the Selector type
- */
+/** Class encapsulating the Selector type. */
 class CVC4_PUBLIC SelectorType : public Type {
-
-public:
-
+ public:
   /** Construct from the base type */
-  SelectorType(const Type& type = Type()) throw(IllegalArgumentException);
+  SelectorType(const Type& type = Type());
 
   /** Get the domain type for this selector (the datatype type) */
   DatatypeType getDomain() const;
@@ -721,15 +619,11 @@ public:
 
 };/* class SelectorType */
 
-/**
- * Class encapsulating the Tester type
- */
+/** Class encapsulating the Tester type. */
 class CVC4_PUBLIC TesterType : public Type {
-
-public:
-
+ public:
   /** Construct from the base type */
-  TesterType(const Type& type = Type()) throw(IllegalArgumentException);
+  TesterType(const Type& type = Type());
 
   /** Get the type that this tester tests (the datatype type) */
   DatatypeType getDomain() const;