Removing the throw specifiers from Result.

1 files changed, 26 insertions, 49 deletions

diff --git a/src/util/result.h b/src/util/result.h
index 8303ad0e8..80fbc0cf7 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -35,24 +35,12 @@ std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_PUBLIC;
  * Three-valued SMT result, with optional explanation.
  */
 class CVC4_PUBLIC Result {
-public:
-  enum Sat {
-    UNSAT = 0,
-    SAT = 1,
-    SAT_UNKNOWN = 2
-  };
+ public:
+  enum Sat { UNSAT = 0, SAT = 1, SAT_UNKNOWN = 2 };
 
-  enum Validity {
-    INVALID = 0,
-    VALID = 1,
-    VALIDITY_UNKNOWN = 2
-  };
+  enum Validity { INVALID = 0, VALID = 1, VALIDITY_UNKNOWN = 2 };
 
-  enum Type {
-    TYPE_SAT,
-    TYPE_VALIDITY,
-    TYPE_NONE
-  };
+  enum Type { TYPE_SAT, TYPE_VALIDITY, TYPE_NONE };
 
   enum UnknownExplanation {
     REQUIRES_FULL_CHECK,
@@ -67,23 +55,21 @@ public:
     UNKNOWN_REASON
   };
 
-private:
+ private:
   enum Sat d_sat;
   enum Validity d_validity;
   enum Type d_which;
   enum UnknownExplanation d_unknownExplanation;
   std::string d_inputName;
 
-public:
-
+ public:
   Result();
 
   Result(enum Sat s, std::string inputName = "");
 
   Result(enum Validity v, std::string inputName = "");
 
-  Result(enum Sat s,
-         enum UnknownExplanation unknownExplanation,
+  Result(enum Sat s, enum UnknownExplanation unknownExplanation,
          std::string inputName = "");
 
   Result(enum Validity v, enum UnknownExplanation unknownExplanation,
@@ -96,9 +82,7 @@ public:
     d_inputName = inputName;
   }
 
-  enum Sat isSat() const {
-    return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN;
-  }
+  enum Sat isSat() const { return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN; }
 
   enum Validity isValid() const {
     return d_which == TYPE_VALIDITY ? d_validity : VALIDITY_UNKNOWN;
@@ -108,20 +92,16 @@ public:
     return isSat() == SAT_UNKNOWN && isValid() == VALIDITY_UNKNOWN;
   }
 
-  Type getType() const {
-    return d_which;
-  }
+  Type getType() const { return d_which; }
 
-  bool isNull() const {
-    return d_which == TYPE_NONE;
-  }
+  bool isNull() const { return d_which == TYPE_NONE; }
 
   enum UnknownExplanation whyUnknown() const;
 
-  bool operator==(const Result& r) const throw();
-  inline bool operator!=(const Result& r) const throw();
-  Result asSatisfiabilityResult() const throw();
-  Result asValidityResult() const throw();
+  bool operator==(const Result& r) const;
+  inline bool operator!=(const Result& r) const;
+  Result asSatisfiabilityResult() const;
+  Result asValidityResult() const;
 
   std::string toString() const;
 
@@ -130,19 +110,19 @@ public:
   /**
    * Write a Result out to a stream in this language.
    */
-  void toStream(std::ostream& out, OutputLanguage language) const throw();
+  void toStream(std::ostream& out, OutputLanguage language) const;
 
   /**
    * This is mostly the same the default
    * If getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN,
    *
    */
-  void toStreamSmt2(std::ostream& out) const throw();
+  void toStreamSmt2(std::ostream& out) const;
 
   /**
    * Write a Result out to a stream in the Tptp format
    */
-  void toStreamTptp(std::ostream& out) const throw();
+  void toStreamTptp(std::ostream& out) const;
 
   /**
    * Write a Result out to a stream.
@@ -152,26 +132,23 @@ public:
    * is overridable by each Printer, since sometimes an output language
    * has a particular preference for how results should appear.
    */
-  void toStreamDefault(std::ostream& out) const throw();
-};/* class Result */
+  void toStreamDefault(std::ostream& out) const;
+}; /* class Result */
 
-inline bool Result::operator!=(const Result& r) const throw() {
-  return !(*this == r);
-}
+inline bool Result::operator!=(const Result& r) const { return !(*this == r); }
 
-std::ostream& operator<<(std::ostream& out,
-                         enum Result::Sat s) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out, enum Result::Sat s) CVC4_PUBLIC;
 std::ostream& operator<<(std::ostream& out,
                          enum Result::Validity v) CVC4_PUBLIC;
 std::ostream& operator<<(std::ostream& out,
                          enum Result::UnknownExplanation e) CVC4_PUBLIC;
 
-bool operator==(enum Result::Sat s, const Result& r) throw() CVC4_PUBLIC;
-bool operator==(enum Result::Validity v, const Result& r) throw() CVC4_PUBLIC;
+bool operator==(enum Result::Sat s, const Result& r) CVC4_PUBLIC;
+bool operator==(enum Result::Validity v, const Result& r) CVC4_PUBLIC;
 
-bool operator!=(enum Result::Sat s, const Result& r) throw() CVC4_PUBLIC;
-bool operator!=(enum Result::Validity v, const Result& r) throw() CVC4_PUBLIC;
+bool operator!=(enum Result::Sat s, const Result& r) CVC4_PUBLIC;
+bool operator!=(enum Result::Validity v, const Result& r) CVC4_PUBLIC;
 
-}/* CVC4 namespace */
+} /* CVC4 namespace */
 
 #endif /* __CVC4__RESULT_H */