From: Tim King <taking@google.com>
Date: Mon, 3 Oct 2016 01:08:29 +0000 (-0700)
Subject: Removing the throw specifiers from Cardinality.
X-Git-Tag: cvc5-1.0.0~6028^2~7
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d93074af065327e49fb4e5160670334618f88284;p=cvc5.git

Removing the throw specifiers from Cardinality.
---

diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp
index 2eea4c040..17c790731 100644
--- a/src/util/cardinality.cpp
+++ b/src/util/cardinality.cpp
@@ -18,77 +18,72 @@
 
 #include "base/cvc4_assert.h"
 
-
 namespace CVC4 {
 
 const Integer Cardinality::s_unknownCard(0);
 const Integer Cardinality::s_intCard(-1);
 const Integer Cardinality::s_realCard(-2);
-const Integer Cardinality::s_largeFiniteCard(Integer("18446744073709551617")); // 2^64 + 1
+const Integer Cardinality::s_largeFiniteCard(
+    Integer("18446744073709551617"));  // 2^64 + 1
 
 const Cardinality Cardinality::INTEGERS(CardinalityBeth(0));
 const Cardinality Cardinality::REALS(CardinalityBeth(1));
 const Cardinality Cardinality::UNKNOWN_CARD((CardinalityUnknown()));
 
-CardinalityBeth::CardinalityBeth(const Integer& beth)
-    : d_index(beth)
-{
+CardinalityBeth::CardinalityBeth(const Integer& beth) : d_index(beth) {
   PrettyCheckArgument(beth >= 0, beth,
                       "Beth index must be a nonnegative integer, not %s.",
                       beth.toString().c_str());
 }
 
-Cardinality::Cardinality(long card)
-    : d_card(card)
-{
+Cardinality::Cardinality(long card) : d_card(card) {
   PrettyCheckArgument(card >= 0, card,
                       "Cardinality must be a nonnegative integer, not %ld.",
                       card);
   d_card += 1;
 }
 
-Cardinality::Cardinality(const Integer& card)
-    : d_card(card)
-{
+Cardinality::Cardinality(const Integer& card) : d_card(card) {
   PrettyCheckArgument(card >= 0, card,
                       "Cardinality must be a nonnegative integer, not %s.",
                       card.toString().c_str());
   d_card += 1;
 }
 
-
-Integer Cardinality::getFiniteCardinality() const throw(IllegalArgumentException) {
+Integer Cardinality::getFiniteCardinality() const {
   PrettyCheckArgument(isFinite(), *this, "This cardinality is not finite.");
-  PrettyCheckArgument(!isLargeFinite(), *this, "This cardinality is finite, but too large to represent.");
+  PrettyCheckArgument(
+      !isLargeFinite(), *this,
+      "This cardinality is finite, but too large to represent.");
   return d_card - 1;
 }
 
-Integer Cardinality::getBethNumber() const throw(IllegalArgumentException) {
+Integer Cardinality::getBethNumber() const {
   PrettyCheckArgument(!isFinite() && !isUnknown(), *this,
                       "This cardinality is not infinite (or is unknown).");
   return -d_card - 1;
 }
 
-Cardinality& Cardinality::operator+=(const Cardinality& c) throw() {
-  if(isUnknown()) {
+Cardinality& Cardinality::operator+=(const Cardinality& c) {
+  if (isUnknown()) {
     return *this;
-  } else if(c.isUnknown()) {
+  } else if (c.isUnknown()) {
     d_card = s_unknownCard;
     return *this;
   }
 
-  if(c.isFinite() && isLargeFinite()) {
+  if (c.isFinite() && isLargeFinite()) {
     return *this;
-  } else if(isFinite() && c.isLargeFinite()) {
+  } else if (isFinite() && c.isLargeFinite()) {
     d_card = s_largeFiniteCard;
     return *this;
   }
 
-  if(isFinite() && c.isFinite()) {
+  if (isFinite() && c.isFinite()) {
     d_card += c.d_card - 1;
     return *this;
   }
-  if(compare(c) == LESS) {
+  if (compare(c) == LESS) {
     return *this = c;
   } else {
     return *this;
@@ -98,25 +93,25 @@ Cardinality& Cardinality::operator+=(const Cardinality& c) throw() {
 }
 
 /** Assigning multiplication of this cardinality with another. */
-Cardinality& Cardinality::operator*=(const Cardinality& c) throw() {
-  if(isUnknown()) {
+Cardinality& Cardinality::operator*=(const Cardinality& c) {
+  if (isUnknown()) {
     return *this;
-  } else if(c.isUnknown()) {
+  } else if (c.isUnknown()) {
     d_card = s_unknownCard;
     return *this;
   }
 
-  if(c.isFinite() && isLargeFinite()) {
+  if (c.isFinite() && isLargeFinite()) {
     return *this;
-  } else if(isFinite() && c.isLargeFinite()) {
+  } else if (isFinite() && c.isLargeFinite()) {
     d_card = s_largeFiniteCard;
     return *this;
   }
 
-  if(compare(0) == EQUAL || c.compare(0) == EQUAL) {
+  if (compare(0) == EQUAL || c.compare(0) == EQUAL) {
     return *this = 0;
-  } else if(!isFinite() || !c.isFinite()) {
-    if(compare(c) == LESS) {
+  } else if (!isFinite() || !c.isFinite()) {
+    if (compare(c) == LESS) {
       return *this = c;
     } else {
       return *this;
@@ -132,50 +127,50 @@ Cardinality& Cardinality::operator*=(const Cardinality& c) throw() {
 }
 
 /** Assigning exponentiation of this cardinality with another. */
-Cardinality& Cardinality::operator^=(const Cardinality& c) throw() {
-  if(isUnknown()) {
+Cardinality& Cardinality::operator^=(const Cardinality& c) {
+  if (isUnknown()) {
     return *this;
-  } else if(c.isUnknown()) {
+  } else if (c.isUnknown()) {
     d_card = s_unknownCard;
     return *this;
   }
 
-  if(c.isFinite() && isLargeFinite()) {
+  if (c.isFinite() && isLargeFinite()) {
     return *this;
-  } else if(isFinite() && c.isLargeFinite()) {
+  } else if (isFinite() && c.isLargeFinite()) {
     d_card = s_largeFiniteCard;
     return *this;
   }
 
-  if(c.compare(0) == EQUAL) {
+  if (c.compare(0) == EQUAL) {
     // (anything) ^ 0 == 1
-    d_card = 2; // remember, +1 for finite cardinalities
+    d_card = 2;  // remember, +1 for finite cardinalities
     return *this;
-  } else if(compare(0) == EQUAL) {
+  } else if (compare(0) == EQUAL) {
     // 0 ^ (>= 1) == 0
     return *this;
-  } else if(compare(1) == EQUAL) {
+  } else if (compare(1) == EQUAL) {
     // 1 ^ (>= 1) == 1
     return *this;
-  } else if(c.compare(1) == EQUAL) {
+  } else if (c.compare(1) == EQUAL) {
     // (anything) ^ 1 == (that thing)
     return *this;
-  } else if(isFinite() && c.isFinite()) {
+  } else if (isFinite() && c.isFinite()) {
     // finite ^ finite == finite
     try {
       // Note: can throw an assertion if c is too big for
       // exponentiation
-      if(d_card - 1 >= 2 && c.d_card - 1 >= 64) {
+      if (d_card - 1 >= 2 && c.d_card - 1 >= 64) {
         // don't bother, it's too large anyways
         d_card = s_largeFiniteCard;
       } else {
         d_card = (d_card - 1).pow(c.d_card.getUnsignedLong() - 1) + 1;
       }
-    } catch(IllegalArgumentException&) {
+    } catch (IllegalArgumentException&) {
       d_card = s_largeFiniteCard;
     }
     return *this;
-  } else if(!isFinite() && c.isFinite()) {
+  } else if (!isFinite() && c.isFinite()) {
     // inf ^ finite == inf
     return *this;
   } else {
@@ -184,7 +179,7 @@ Cardinality& Cardinality::operator^=(const Cardinality& c) throw() {
            this->toString().c_str(), c.toString().c_str());
     // (>= 2) ^ beth_k == beth_(k+1)
     // unless the base is already > the exponent
-    if(compare(c) == GREATER) {
+    if (compare(c) == GREATER) {
       return *this;
     }
     d_card = c.d_card - 1;
@@ -194,70 +189,67 @@ Cardinality& Cardinality::operator^=(const Cardinality& c) throw() {
   Unreachable();
 }
 
-Cardinality::CardinalityComparison Cardinality::compare(const Cardinality& c) const throw() {
-  if(isUnknown() || c.isUnknown()) {
+Cardinality::CardinalityComparison Cardinality::compare(
+    const Cardinality& c) const {
+  if (isUnknown() || c.isUnknown()) {
     return UNKNOWN;
-  } else if(isLargeFinite()) {
-    if(c.isLargeFinite()) {
+  } else if (isLargeFinite()) {
+    if (c.isLargeFinite()) {
       return UNKNOWN;
-    } else if(c.isFinite()) {
-        return GREATER;
+    } else if (c.isFinite()) {
+      return GREATER;
     } else {
       Assert(c.isInfinite());
       return LESS;
     }
-  } else if(c.isLargeFinite()) {
-    if(isLargeFinite()) {
+  } else if (c.isLargeFinite()) {
+    if (isLargeFinite()) {
       return UNKNOWN;
-    } else if(isFinite()) {
+    } else if (isFinite()) {
       return LESS;
     } else {
       Assert(isInfinite());
       return GREATER;
     }
-  } else if(isInfinite()) {
-    if(c.isFinite()) {
+  } else if (isInfinite()) {
+    if (c.isFinite()) {
       return GREATER;
     } else {
-      return d_card < c.d_card ? GREATER :
-               (d_card == c.d_card ? EQUAL : LESS);
+      return d_card < c.d_card ? GREATER : (d_card == c.d_card ? EQUAL : LESS);
     }
-  } else if(c.isInfinite()) {
+  } else if (c.isInfinite()) {
     Assert(isFinite());
     return LESS;
   } else {
     Assert(isFinite() && !isLargeFinite());
     Assert(c.isFinite() && !c.isLargeFinite());
-    return d_card < c.d_card ? LESS :
-             (d_card == c.d_card ? EQUAL : GREATER);
+    return d_card < c.d_card ? LESS : (d_card == c.d_card ? EQUAL : GREATER);
   }
 
   Unreachable();
 }
 
-bool Cardinality::knownLessThanOrEqual(const Cardinality& c) const throw() {
+bool Cardinality::knownLessThanOrEqual(const Cardinality& c) const {
   CardinalityComparison cmp = this->compare(c);
   return cmp == LESS || cmp == EQUAL;
 }
 
-std::string Cardinality::toString() const throw() {
+std::string Cardinality::toString() const {
   std::stringstream ss;
   ss << *this;
   return ss.str();
 }
 
-
-std::ostream& operator<<(std::ostream& out, CardinalityBeth b) throw() {
+std::ostream& operator<<(std::ostream& out, CardinalityBeth b) {
   out << "beth[" << b.getNumber() << ']';
 
   return out;
 }
 
-
-std::ostream& operator<<(std::ostream& out, const Cardinality& c) throw() {
-  if(c.isUnknown()) {
+std::ostream& operator<<(std::ostream& out, const Cardinality& c) {
+  if (c.isUnknown()) {
     out << "Cardinality::UNKNOWN";
-  } else if(c.isFinite()) {
+  } else if (c.isFinite()) {
     out << c.getFiniteCardinality();
   } else {
     out << CardinalityBeth(c.getBethNumber());
@@ -266,5 +258,4 @@ std::ostream& operator<<(std::ostream& out, const Cardinality& c) throw() {
   return out;
 }
 
-
-}/* CVC4 namespace */
+} /* CVC4 namespace */
diff --git a/src/util/cardinality.h b/src/util/cardinality.h
index 93b4ca618..b16f84324 100644
--- a/src/util/cardinality.h
+++ b/src/util/cardinality.h
@@ -35,23 +35,21 @@ namespace CVC4 {
 class CVC4_PUBLIC CardinalityBeth {
   Integer d_index;
 
-public:
+ public:
   CardinalityBeth(const Integer& beth);
 
-  const Integer& getNumber() const throw() {
-    return d_index;
-  }
+  const Integer& getNumber() const { return d_index; }
 
-};/* class CardinalityBeth */
+}; /* class CardinalityBeth */
 
 /**
  * Representation for an unknown cardinality.
  */
 class CVC4_PUBLIC CardinalityUnknown {
-public:
-  CardinalityUnknown() throw() {}
-  ~CardinalityUnknown() throw() {}
-};/* class CardinalityUnknown */
+ public:
+  CardinalityUnknown() {}
+  ~CardinalityUnknown() {}
+}; /* class CardinalityUnknown */
 
 /**
  * A simple representation of a cardinality.  We store an
@@ -83,8 +81,7 @@ class CVC4_PUBLIC Cardinality {
    */
   Integer d_card;
 
-public:
-
+ public:
   /** The cardinality of the set of integers. */
   static const Cardinality INTEGERS;
 
@@ -100,7 +97,7 @@ public:
     EQUAL,
     GREATER,
     UNKNOWN
-  };/* enum CardinalityComparison */
+  }; /* enum CardinalityComparison */
 
   /**
    * Construct a finite cardinality equal to the integer argument.
@@ -119,14 +116,12 @@ public:
   /**
    * Construct an infinite cardinality equal to the given Beth number.
    */
-  Cardinality(CardinalityBeth beth) : d_card(-beth.getNumber() - 1) {
-  }
+  Cardinality(CardinalityBeth beth) : d_card(-beth.getNumber() - 1) {}
 
   /**
    * Construct an unknown cardinality.
    */
-  Cardinality(CardinalityUnknown) : d_card(0) {
-  }
+  Cardinality(CardinalityUnknown) : d_card(0) {}
 
   /**
    * Returns true iff this cardinality is unknown.  "Unknown" in this
@@ -135,72 +130,60 @@ public:
    * at the "ceiling" return "false" for isUnknown() and true for
    * isFinite() and isLargeFinite().
    */
-  bool isUnknown() const throw() {
-    return d_card == 0;
-  }
+  bool isUnknown() const { return d_card == 0; }
 
   /** Returns true iff this cardinality is finite. */
-  bool isFinite() const throw() {
-    return d_card > 0;
-  }
+  bool isFinite() const { return d_card > 0; }
   /** Returns true iff this cardinality is one */
-  bool isOne() const throw() {
-    return d_card == 1;
-  }
+  bool isOne() const { return d_card == 1; }
 
   /**
    * Returns true iff this cardinality is finite and large (i.e.,
    * at the ceiling of representable finite cardinalities).
    */
-  bool isLargeFinite() const throw() {
-    return d_card >= s_largeFiniteCard;
-  }
+  bool isLargeFinite() const { return d_card >= s_largeFiniteCard; }
 
   /** Returns true iff this cardinality is infinite. */
-  bool isInfinite() const throw() {
-    return d_card < 0;
-  }
+  bool isInfinite() const { return d_card < 0; }
 
   /**
    * Returns true iff this cardinality is finite or countably
    * infinite.
    */
-  bool isCountable() const throw() {
-    return isFinite() || d_card == s_intCard;
-  }
+  bool isCountable() const { return isFinite() || d_card == s_intCard; }
 
   /**
    * In the case that this cardinality is finite, return its
    * cardinality.  (If this cardinality is infinite, this function
    * throws an IllegalArgumentException.)
    */
-  Integer getFiniteCardinality() const throw(IllegalArgumentException);
+  Integer getFiniteCardinality() const;
 
   /**
    * In the case that this cardinality is infinite, return its Beth
    * number.  (If this cardinality is finite, this function throws an
    * IllegalArgumentException.)
    */
-  Integer getBethNumber() const throw(IllegalArgumentException);
+  Integer getBethNumber() const;
 
   /** Assigning addition of this cardinality with another. */
-  Cardinality& operator+=(const Cardinality& c) throw();
+  Cardinality& operator+=(const Cardinality& c);
 
   /** Assigning multiplication of this cardinality with another. */
-  Cardinality& operator*=(const Cardinality& c) throw();
+  Cardinality& operator*=(const Cardinality& c);
 
   /** Assigning exponentiation of this cardinality with another. */
-  Cardinality& operator^=(const Cardinality& c) throw();
+  Cardinality& operator^=(const Cardinality& c);
 
   /** Add two cardinalities. */
-  Cardinality operator+(const Cardinality& c) const throw() {
+  Cardinality operator+(const Cardinality& c) const {
     Cardinality card(*this);
     card += c;
     return card;
   }
 
   /** Multiply two cardinalities. */
-  Cardinality operator*(const Cardinality& c) const throw() {
+  Cardinality operator*(const Cardinality& c) const {
     Cardinality card(*this);
     card *= c;
     return card;
@@ -209,7 +192,7 @@ public:
   /**
    * Exponentiation of two cardinalities.
    */
-  Cardinality operator^(const Cardinality& c) const throw() {
+  Cardinality operator^(const Cardinality& c) const {
     Cardinality card(*this);
     card ^= c;
     return card;
@@ -221,30 +204,26 @@ public:
    * represented), or if one or the other is the special "unknown"
    * cardinality.
    */
-  Cardinality::CardinalityComparison compare(const Cardinality& c) const throw();
+  Cardinality::CardinalityComparison compare(const Cardinality& c) const;
 
   /**
    * Return a string representation of this cardinality.
    */
-  std::string toString() const throw();
+  std::string toString() const;
 
   /**
    * Compare two cardinalities and if it is known that the current
    * cardinality is smaller or equal to c, it returns true.
    */
-  bool knownLessThanOrEqual(const Cardinality& c) const throw();
-};/* class Cardinality */
-
+  bool knownLessThanOrEqual(const Cardinality& c) const;
+}; /* class Cardinality */
 
 /** Print an element of the InfiniteCardinality enumeration. */
-std::ostream& operator<<(std::ostream& out, CardinalityBeth b)
-  throw() CVC4_PUBLIC;
-
+std::ostream& operator<<(std::ostream& out, CardinalityBeth b) CVC4_PUBLIC;
 
 /** Print a cardinality in a human-readable fashion. */
-std::ostream& operator<<(std::ostream& out, const Cardinality& c)
-  throw() CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out, const Cardinality& c) CVC4_PUBLIC;
 
-}/* CVC4 namespace */
+} /* CVC4 namespace */
 
 #endif /* __CVC4__CARDINALITY_H */
diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp
index aa6cb03af..a7412b503 100644
--- a/src/util/integer_cln_imp.cpp
+++ b/src/util/integer_cln_imp.cpp
@@ -145,4 +145,14 @@ bool Integer::fitsUnsignedLong() const {
   return sgn() >= 0 && d_value <= s_unsignedLongMax;
 }
 
+Integer Integer::pow(unsigned long int exp) const {
+  if (exp == 0) {
+    return Integer(1);
+  } else {
+    Assert(exp > 0);
+    cln::cl_I result = cln::expt_pos(d_value, exp);
+    return Integer(result);
+  }
+}
+
 } /* namespace CVC4 */
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 6bfebbaf1..12619520f 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -321,16 +321,7 @@ public:
    *
    * @param exp the exponent
    */
-  Integer pow(unsigned long int exp) const {
-    if(exp > 0){
-      cln::cl_I result= cln::expt_pos(d_value,exp);
-      return Integer( result );
-    }else if(exp == 0){
-      return Integer( 1 );
-    }else{
-      throw Exception("Negative exponent in Integer::pow()");
-    }
-  }
+  Integer pow(unsigned long int exp) const;
 
   /**
    * Return the greatest common divisor of this integer with another.
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index 3a95c6b85..5af902ac6 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -361,8 +361,8 @@ public:
    */
   Integer pow(unsigned long int exp) const {
     mpz_class result;
-    mpz_pow_ui(result.get_mpz_t(),d_value.get_mpz_t(),exp);
-    return Integer( result );
+    mpz_pow_ui(result.get_mpz_t(), d_value.get_mpz_t(), exp);
+    return Integer(result);
   }
 
   /**