From: Tim King 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; }