From 936bf9eb1881b1fb5e80fd75eb7f81c512712b83 Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 15 Nov 2012 02:15:22 +0000 Subject: Fix for bug 447. --- src/util/result.cpp | 14 ++++++++++++++ src/util/result.h | 6 ++++++ 2 files changed, 20 insertions(+) (limited to 'src') 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 */ -- cgit v1.2.3