diff options
Diffstat (limited to 'src/util/result.h')
| -rw-r--r-- | src/util/result.h | 24 |
1 files changed, 22 insertions, 2 deletions
diff --git a/src/util/result.h b/src/util/result.h index 1e2b61738..8d9b93a1e 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -50,9 +50,11 @@ private: enum Validity d_validity; enum { TYPE_SAT, TYPE_VALIDITY } d_which; + friend std::ostream& CVC4::operator<<(std::ostream& out, Result r); + public: - Result(enum SAT); - Result(enum Validity); + Result(enum SAT s) : d_sat(s), d_validity(VALIDITY_UNKNOWN), d_which(TYPE_SAT) {} + Result(enum Validity v) : d_sat(SAT_UNKNOWN), d_validity(v), d_which(TYPE_VALIDITY) {} enum SAT isSAT(); enum Validity isValid(); @@ -60,6 +62,24 @@ public: };/* class Result */ +inline std::ostream& operator<<(std::ostream& out, Result r) { + if(r.d_which == Result::TYPE_SAT) { + switch(r.d_sat) { + case Result::UNSAT: out << "UNSAT"; break; + case Result::SAT: out << "SAT"; break; + case Result::SAT_UNKNOWN: out << "SAT_UNKNOWN"; break; + } + } else { + switch(r.d_validity) { + case Result::INVALID: out << "INVALID"; break; + case Result::VALID: out << "VALID"; break; + case Result::VALIDITY_UNKNOWN: out << "VALIDITY_UNKNOWN"; break; + } + } + + return out; +} + }/* CVC4 namespace */ #endif /* __CVC4__RESULT_H */ |