diff options
| author | Tim King <taking@cs.nyu.edu> | 2012-11-15 02:15:22 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2012-11-15 02:15:22 +0000 |
| commit | 936bf9eb1881b1fb5e80fd75eb7f81c512712b83 (patch) | |
| tree | 7d3a8f0b6fd31b6b107c7b838c8402892d12b570 /src/util/result.h | |
| parent | dc0372a91ae46e6fc5ead1f51a1fe033cfd19944 (diff) | |
Fix for bug 447.
Diffstat (limited to 'src/util/result.h')
| -rw-r--r-- | src/util/result.h | 6 |
1 files changed, 6 insertions, 0 deletions
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 */ |