From: Tim King <taking@google.com>
Date: Sat, 1 Oct 2016 22:40:30 +0000 (-0700)
Subject: Removing the throw specifiers from Result.
X-Git-Tag: cvc5-1.0.0~6028^2~8
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f95488791b2d14e0710fea09202bb5638e66e93d;p=cvc5.git

Removing the throw specifiers from Result.
---

diff --git a/src/util/result.cpp b/src/util/result.cpp
index 51b1a8de1..af28269f1 100644
--- a/src/util/result.cpp
+++ b/src/util/result.cpp
@@ -28,167 +28,152 @@ using namespace std;
 namespace CVC4 {
 
 Result::Result()
-    : d_sat(SAT_UNKNOWN)
-    , d_validity(VALIDITY_UNKNOWN)
-    , d_which(TYPE_NONE)
-    , d_unknownExplanation(UNKNOWN_REASON)
-    , d_inputName("")
-{ }
-
+    : d_sat(SAT_UNKNOWN),
+      d_validity(VALIDITY_UNKNOWN),
+      d_which(TYPE_NONE),
+      d_unknownExplanation(UNKNOWN_REASON),
+      d_inputName("") {}
 
 Result::Result(enum Sat s, std::string inputName)
-    : d_sat(s)
-    , d_validity(VALIDITY_UNKNOWN)
-    , d_which(TYPE_SAT)
-    , d_unknownExplanation(UNKNOWN_REASON)
-    , d_inputName(inputName)
-{
+    : d_sat(s),
+      d_validity(VALIDITY_UNKNOWN),
+      d_which(TYPE_SAT),
+      d_unknownExplanation(UNKNOWN_REASON),
+      d_inputName(inputName) {
   PrettyCheckArgument(s != SAT_UNKNOWN,
                       "Must provide a reason for satisfiability being unknown");
 }
 
 Result::Result(enum Validity v, std::string inputName)
-    : d_sat(SAT_UNKNOWN)
-    , d_validity(v)
-    , d_which(TYPE_VALIDITY)
-    , d_unknownExplanation(UNKNOWN_REASON)
-    , d_inputName(inputName)
-{
+    : d_sat(SAT_UNKNOWN),
+      d_validity(v),
+      d_which(TYPE_VALIDITY),
+      d_unknownExplanation(UNKNOWN_REASON),
+      d_inputName(inputName) {
   PrettyCheckArgument(v != VALIDITY_UNKNOWN,
                       "Must provide a reason for validity being unknown");
 }
 
-
 Result::Result(enum Sat s, enum UnknownExplanation unknownExplanation,
                std::string inputName)
-    : d_sat(s)
-    , d_validity(VALIDITY_UNKNOWN)
-    , d_which(TYPE_SAT)
-    , d_unknownExplanation(unknownExplanation)
-    , d_inputName(inputName)
-{
+    : d_sat(s),
+      d_validity(VALIDITY_UNKNOWN),
+      d_which(TYPE_SAT),
+      d_unknownExplanation(unknownExplanation),
+      d_inputName(inputName) {
   PrettyCheckArgument(s == SAT_UNKNOWN,
                       "improper use of unknown-result constructor");
 }
 
 Result::Result(enum Validity v, enum UnknownExplanation unknownExplanation,
                std::string inputName)
-    : d_sat(SAT_UNKNOWN)
-    , d_validity(v)
-    , d_which(TYPE_VALIDITY)
-    , d_unknownExplanation(unknownExplanation)
-    , d_inputName(inputName)
-{
+    : d_sat(SAT_UNKNOWN),
+      d_validity(v),
+      d_which(TYPE_VALIDITY),
+      d_unknownExplanation(unknownExplanation),
+      d_inputName(inputName) {
   PrettyCheckArgument(v == VALIDITY_UNKNOWN,
                       "improper use of unknown-result constructor");
 }
 
-Result::Result(const std::string& instr, std::string inputName) :
-  d_sat(SAT_UNKNOWN),
-  d_validity(VALIDITY_UNKNOWN),
-  d_which(TYPE_NONE),
-  d_unknownExplanation(UNKNOWN_REASON),
-  d_inputName(inputName) {
+Result::Result(const std::string& instr, std::string inputName)
+    : d_sat(SAT_UNKNOWN),
+      d_validity(VALIDITY_UNKNOWN),
+      d_which(TYPE_NONE),
+      d_unknownExplanation(UNKNOWN_REASON),
+      d_inputName(inputName) {
   string s = instr;
   transform(s.begin(), s.end(), s.begin(), ::tolower);
-  if(s == "sat" || s == "satisfiable") {
+  if (s == "sat" || s == "satisfiable") {
     d_which = TYPE_SAT;
     d_sat = SAT;
-  } else if(s == "unsat" || s == "unsatisfiable") {
+  } else if (s == "unsat" || s == "unsatisfiable") {
     d_which = TYPE_SAT;
     d_sat = UNSAT;
-  } else if(s == "valid") {
+  } else if (s == "valid") {
     d_which = TYPE_VALIDITY;
     d_validity = VALID;
-  } else if(s == "invalid") {
+  } else if (s == "invalid") {
     d_which = TYPE_VALIDITY;
     d_validity = INVALID;
-  } else if(s == "incomplete") {
+  } else if (s == "incomplete") {
     d_which = TYPE_SAT;
     d_sat = SAT_UNKNOWN;
     d_unknownExplanation = INCOMPLETE;
-  } else if(s == "timeout") {
+  } else if (s == "timeout") {
     d_which = TYPE_SAT;
     d_sat = SAT_UNKNOWN;
     d_unknownExplanation = TIMEOUT;
-  } else if(s == "resourceout") {
+  } else if (s == "resourceout") {
     d_which = TYPE_SAT;
     d_sat = SAT_UNKNOWN;
     d_unknownExplanation = RESOURCEOUT;
-  } else if(s == "memout") {
+  } else if (s == "memout") {
     d_which = TYPE_SAT;
     d_sat = SAT_UNKNOWN;
     d_unknownExplanation = MEMOUT;
-  } else if(s == "interrupted") {
+  } else if (s == "interrupted") {
     d_which = TYPE_SAT;
     d_sat = SAT_UNKNOWN;
     d_unknownExplanation = INTERRUPTED;
-  } else if(s.size() >= 7 && s.compare(0, 7, "unknown") == 0) {
+  } else if (s.size() >= 7 && s.compare(0, 7, "unknown") == 0) {
     d_which = TYPE_SAT;
     d_sat = SAT_UNKNOWN;
   } else {
-    IllegalArgument(s, "expected satisfiability/validity result, "
-                    "instead got `%s'", s.c_str());
+    IllegalArgument(s,
+                    "expected satisfiability/validity result, "
+                    "instead got `%s'",
+                    s.c_str());
   }
 }
 
 Result::UnknownExplanation Result::whyUnknown() const {
-  PrettyCheckArgument( isUnknown(), this,
-                       "This result is not unknown, so the reason for "
-                       "being unknown cannot be inquired of it" );
+  PrettyCheckArgument(isUnknown(), this,
+                      "This result is not unknown, so the reason for "
+                      "being unknown cannot be inquired of it");
   return d_unknownExplanation;
 }
 
-bool Result::operator==(const Result& r) const throw() {
-  if(d_which != r.d_which) {
+bool Result::operator==(const Result& r) const {
+  if (d_which != r.d_which) {
     return false;
   }
-  if(d_which == TYPE_SAT) {
-    return d_sat == r.d_sat &&
-      ( d_sat != SAT_UNKNOWN ||
-        d_unknownExplanation == r.d_unknownExplanation );
+  if (d_which == TYPE_SAT) {
+    return d_sat == r.d_sat && (d_sat != SAT_UNKNOWN ||
+                                d_unknownExplanation == r.d_unknownExplanation);
   }
-  if(d_which == TYPE_VALIDITY) {
+  if (d_which == TYPE_VALIDITY) {
     return d_validity == r.d_validity &&
-      ( d_validity != VALIDITY_UNKNOWN ||
-        d_unknownExplanation == r.d_unknownExplanation );
+           (d_validity != VALIDITY_UNKNOWN ||
+            d_unknownExplanation == r.d_unknownExplanation);
   }
   return false;
 }
 
-bool operator==(enum Result::Sat sr, const Result& r) throw() {
-  return r == sr;
-}
+bool operator==(enum Result::Sat sr, const Result& r) { return r == sr; }
 
-bool operator==(enum Result::Validity vr, const Result& r) throw() {
-  return r == vr;
-}
-bool operator!=(enum Result::Sat s, const Result& r) throw(){
-  return !(s == r);
-}
-bool operator!=(enum Result::Validity v, const Result& r) throw(){
-  return !(v == r);
-}
+bool operator==(enum Result::Validity vr, const Result& r) { return r == vr; }
+bool operator!=(enum Result::Sat s, const Result& r) { return !(s == r); }
+bool operator!=(enum Result::Validity v, const Result& r) { return !(v == r); }
 
-Result Result::asSatisfiabilityResult() const throw() {
-  if(d_which == TYPE_SAT) {
+Result Result::asSatisfiabilityResult() const {
+  if (d_which == TYPE_SAT) {
     return *this;
   }
 
-  if(d_which == TYPE_VALIDITY) {
-    switch(d_validity) {
-
-    case INVALID:
-      return Result(SAT, d_inputName);
+  if (d_which == TYPE_VALIDITY) {
+    switch (d_validity) {
+      case INVALID:
+        return Result(SAT, d_inputName);
 
-    case VALID:
-      return Result(UNSAT, d_inputName);
+      case VALID:
+        return Result(UNSAT, d_inputName);
 
-    case VALIDITY_UNKNOWN:
-      return Result(SAT_UNKNOWN, d_unknownExplanation, d_inputName);
+      case VALIDITY_UNKNOWN:
+        return Result(SAT_UNKNOWN, d_unknownExplanation, d_inputName);
 
-    default:
-      Unhandled(d_validity);
+      default:
+        Unhandled(d_validity);
     }
   }
 
@@ -196,25 +181,24 @@ Result Result::asSatisfiabilityResult() const throw() {
   return Result(SAT_UNKNOWN, NO_STATUS, d_inputName);
 }
 
-Result Result::asValidityResult() const throw() {
-  if(d_which == TYPE_VALIDITY) {
+Result Result::asValidityResult() const {
+  if (d_which == TYPE_VALIDITY) {
     return *this;
   }
 
-  if(d_which == TYPE_SAT) {
-    switch(d_sat) {
-
-    case SAT:
-      return Result(INVALID, d_inputName);
+  if (d_which == TYPE_SAT) {
+    switch (d_sat) {
+      case SAT:
+        return Result(INVALID, d_inputName);
 
-    case UNSAT:
-      return Result(VALID, d_inputName);
+      case UNSAT:
+        return Result(VALID, d_inputName);
 
-    case SAT_UNKNOWN:
-      return Result(VALIDITY_UNKNOWN, d_unknownExplanation, d_inputName);
+      case SAT_UNKNOWN:
+        return Result(VALIDITY_UNKNOWN, d_unknownExplanation, d_inputName);
 
-    default:
-      Unhandled(d_sat);
+      default:
+        Unhandled(d_sat);
     }
   }
 
@@ -229,38 +213,73 @@ string Result::toString() const {
 }
 
 ostream& operator<<(ostream& out, enum Result::Sat s) {
-  switch(s) {
-  case Result::UNSAT: out << "UNSAT"; break;
-  case Result::SAT: out << "SAT"; break;
-  case Result::SAT_UNKNOWN: out << "SAT_UNKNOWN"; break;
-  default: Unhandled(s);
+  switch (s) {
+    case Result::UNSAT:
+      out << "UNSAT";
+      break;
+    case Result::SAT:
+      out << "SAT";
+      break;
+    case Result::SAT_UNKNOWN:
+      out << "SAT_UNKNOWN";
+      break;
+    default:
+      Unhandled(s);
   }
   return out;
 }
 
 ostream& operator<<(ostream& out, enum Result::Validity v) {
-  switch(v) {
-  case Result::INVALID: out << "INVALID"; break;
-  case Result::VALID: out << "VALID"; break;
-  case Result::VALIDITY_UNKNOWN: out << "VALIDITY_UNKNOWN"; break;
-  default: Unhandled(v);
+  switch (v) {
+    case Result::INVALID:
+      out << "INVALID";
+      break;
+    case Result::VALID:
+      out << "VALID";
+      break;
+    case Result::VALIDITY_UNKNOWN:
+      out << "VALIDITY_UNKNOWN";
+      break;
+    default:
+      Unhandled(v);
   }
   return out;
 }
 
 ostream& operator<<(ostream& out, enum Result::UnknownExplanation e) {
-  switch(e) {
-  case Result::REQUIRES_FULL_CHECK: out << "REQUIRES_FULL_CHECK"; break;
-  case Result::INCOMPLETE: out << "INCOMPLETE"; break;
-  case Result::TIMEOUT: out << "TIMEOUT"; break;
-  case Result::RESOURCEOUT: out << "RESOURCEOUT"; break;
-  case Result::MEMOUT: out << "MEMOUT"; break;
-  case Result::INTERRUPTED: out << "INTERRUPTED"; break;
-  case Result::NO_STATUS: out << "NO_STATUS"; break;
-  case Result::UNSUPPORTED: out << "UNSUPPORTED"; break;
-  case Result::OTHER: out << "OTHER"; break;
-  case Result::UNKNOWN_REASON: out << "UNKNOWN_REASON"; break;
-  default: Unhandled(e);
+  switch (e) {
+    case Result::REQUIRES_FULL_CHECK:
+      out << "REQUIRES_FULL_CHECK";
+      break;
+    case Result::INCOMPLETE:
+      out << "INCOMPLETE";
+      break;
+    case Result::TIMEOUT:
+      out << "TIMEOUT";
+      break;
+    case Result::RESOURCEOUT:
+      out << "RESOURCEOUT";
+      break;
+    case Result::MEMOUT:
+      out << "MEMOUT";
+      break;
+    case Result::INTERRUPTED:
+      out << "INTERRUPTED";
+      break;
+    case Result::NO_STATUS:
+      out << "NO_STATUS";
+      break;
+    case Result::UNSUPPORTED:
+      out << "UNSUPPORTED";
+      break;
+    case Result::OTHER:
+      out << "OTHER";
+      break;
+    case Result::UNKNOWN_REASON:
+      out << "UNKNOWN_REASON";
+      break;
+    default:
+      Unhandled(e);
   }
   return out;
 }
@@ -268,61 +287,59 @@ ostream& operator<<(ostream& out, enum Result::UnknownExplanation e) {
 ostream& operator<<(ostream& out, const Result& r) {
   r.toStream(out, language::SetLanguage::getLanguage(out));
   return out;
-}/* operator<<(ostream&, const Result&) */
-
-
-void Result::toStreamDefault(std::ostream& out) const throw() {
-  if(getType() == Result::TYPE_SAT) {
-    switch(isSat()) {
-    case Result::UNSAT:
-      out << "unsat";
-      break;
-    case Result::SAT:
-      out << "sat";
-      break;
-    case Result::SAT_UNKNOWN:
-      out << "unknown";
-      if(whyUnknown() != Result::UNKNOWN_REASON) {
-        out << " (" << whyUnknown() << ")";
-      }
-      break;
+} /* operator<<(ostream&, const Result&) */
+
+void Result::toStreamDefault(std::ostream& out) const {
+  if (getType() == Result::TYPE_SAT) {
+    switch (isSat()) {
+      case Result::UNSAT:
+        out << "unsat";
+        break;
+      case Result::SAT:
+        out << "sat";
+        break;
+      case Result::SAT_UNKNOWN:
+        out << "unknown";
+        if (whyUnknown() != Result::UNKNOWN_REASON) {
+          out << " (" << whyUnknown() << ")";
+        }
+        break;
     }
   } else {
-    switch(isValid()) {
-    case Result::INVALID:
-      out << "invalid";
-      break;
-    case Result::VALID:
-      out << "valid";
-      break;
-    case Result::VALIDITY_UNKNOWN:
-      out << "unknown";
-      if(whyUnknown() != Result::UNKNOWN_REASON) {
-        out << " (" << whyUnknown() << ")";
-      }
-      break;
+    switch (isValid()) {
+      case Result::INVALID:
+        out << "invalid";
+        break;
+      case Result::VALID:
+        out << "valid";
+        break;
+      case Result::VALIDITY_UNKNOWN:
+        out << "unknown";
+        if (whyUnknown() != Result::UNKNOWN_REASON) {
+          out << " (" << whyUnknown() << ")";
+        }
+        break;
     }
   }
-}/* Result::toStreamDefault() */
+} /* Result::toStreamDefault() */
 
-
-void Result::toStreamSmt2(ostream& out) const throw(){
-  if(getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN) {
+void Result::toStreamSmt2(ostream& out) const {
+  if (getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN) {
     out << "unknown";
   } else {
     toStreamDefault(out);
   }
 }
 
-void Result::toStreamTptp(std::ostream& out) const throw() {
+void Result::toStreamTptp(std::ostream& out) const {
   out << "% SZS status ";
-  if(isSat() == Result::SAT) {
+  if (isSat() == Result::SAT) {
     out << "Satisfiable";
-  } else if(isSat() == Result::UNSAT) {
+  } else if (isSat() == Result::UNSAT) {
     out << "Unsatisfiable";
-  } else if(isValid() == Result::VALID) {
+  } else if (isValid() == Result::VALID) {
     out << "Theorem";
-  } else if(isValid() == Result::INVALID) {
+  } else if (isValid() == Result::INVALID) {
     out << "CounterSatisfiable";
   } else {
     out << "GaveUp";
@@ -330,27 +347,27 @@ void Result::toStreamTptp(std::ostream& out) const throw() {
   out << " for " << getInputName();
 }
 
-void Result::toStream(std::ostream& out, OutputLanguage language) const throw() {
-  switch(language) {
-  case language::output::LANG_SMTLIB_V2_0:
-  case language::output::LANG_SMTLIB_V2_5:
-  case language::output::LANG_SYGUS:
-  case language::output::LANG_Z3STR:
-    toStreamSmt2(out);
-    break;
-  case language::output::LANG_TPTP:
-    toStreamTptp(out);
-    break;
-  case language::output::LANG_AST:
-  case language::output::LANG_AUTO:
-  case language::output::LANG_CVC3:
-  case language::output::LANG_CVC4:
-  case language::output::LANG_MAX:
-  case language::output::LANG_SMTLIB_V1:
-  default:
-    toStreamDefault(out);
-    break;
+void Result::toStream(std::ostream& out, OutputLanguage language) const {
+  switch (language) {
+    case language::output::LANG_SMTLIB_V2_0:
+    case language::output::LANG_SMTLIB_V2_5:
+    case language::output::LANG_SYGUS:
+    case language::output::LANG_Z3STR:
+      toStreamSmt2(out);
+      break;
+    case language::output::LANG_TPTP:
+      toStreamTptp(out);
+      break;
+    case language::output::LANG_AST:
+    case language::output::LANG_AUTO:
+    case language::output::LANG_CVC3:
+    case language::output::LANG_CVC4:
+    case language::output::LANG_MAX:
+    case language::output::LANG_SMTLIB_V1:
+    default:
+      toStreamDefault(out);
+      break;
   };
 }
 
-}/* CVC4 namespace */
+} /* CVC4 namespace */
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 */
diff --git a/src/util/sexpr.h b/src/util/sexpr.h
index 2948cba4b..0b517570e 100644
--- a/src/util/sexpr.h
+++ b/src/util/sexpr.h
@@ -39,11 +39,12 @@
 namespace CVC4 {
 
 class CVC4_PUBLIC SExprKeyword {
-  std::string d_str;
-
  public:
   SExprKeyword(const std::string& s) : d_str(s) {}
   const std::string& getString() const { return d_str; }
+
+ private:
+  std::string d_str;
 }; /* class SExpr::Keyword */
 
 /**