From: Tim King <taking@cs.nyu.edu>
Date: Thu, 15 Nov 2012 02:15:22 +0000 (+0000)
Subject: Fix for bug 447.
X-Git-Tag: cvc5-1.0.0~7593
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=936bf9eb1881b1fb5e80fd75eb7f81c512712b83;p=cvc5.git

Fix for bug 447.
---

diff --git a/src/util/result.cpp b/src/util/result.cpp
index f51bacee7..6a32747cb 100644
--- a/src/util/result.cpp
+++ b/src/util/result.cpp
@@ -92,6 +92,20 @@ bool Result::operator==(const Result& r) const throw() {
   return false;
 }
 
+bool operator==(enum Result::Sat sr, const Result& r) throw() {
+  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);
+}
+
 Result Result::asSatisfiabilityResult() const throw() {
   if(d_which == TYPE_SAT) {
     return *this;
diff --git a/src/util/result.h b/src/util/result.h
index 7d53f8add..fd1d82d9b 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -155,6 +155,12 @@ std::ostream& operator<<(std::ostream& out,
 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) throw() CVC4_PUBLIC;
+bool operator!=(enum Result::Validity v, const Result& r) throw() CVC4_PUBLIC;
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__RESULT_H */
diff --git a/test/system/boilerplate.cpp b/test/system/boilerplate.cpp
index b4e20d063..cea610b86 100644
--- a/test/system/boilerplate.cpp
+++ b/test/system/boilerplate.cpp
@@ -31,6 +31,6 @@ int main() {
   SmtEngine smt(&em);
   Result r = smt.query(em.mkConst(true));
 
-  return r == Result::VALID ? 0 : 1;
+  return (Result::VALID == r) ? 0 : 1;
 }