summaryrefslogtreecommitdiff
path: root/src/util/result.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/util/result.h')
-rw-r--r--src/util/result.h15
1 files changed, 15 insertions, 0 deletions
diff --git a/src/util/result.h b/src/util/result.h
index ccc36973d..f1f6ae1c2 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -86,6 +86,21 @@ public:
}
enum UnknownExplanation whyUnknown();
+ inline bool operator==(Result r) {
+ if(d_which != r.d_which) {
+ return false;
+ }
+ if(d_which == TYPE_SAT) {
+ return d_sat == r.d_sat;
+ }
+ if(d_which == TYPE_VALIDITY) {
+ return d_validity == r.d_validity;
+ }
+ return false;
+ }
+ inline bool operator!=(Result r) {
+ return !(*this == r);
+ }
inline Result asSatisfiabilityResult() const;
inline Result asValidityResult() const;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback