diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-12-03 14:59:30 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-12-03 14:59:30 +0000 |
commit | 7fb54afe126e5045fc6c5553c1aff3c3f73509aa (patch) | |
tree | 37f4f23af0eccd6c9615a5af9b2d219e305d1f78 /src/util/result.h | |
parent | bde1a14afc211c8f0f0521bb91feb562eaa9f9ea (diff) |
parsing/expr/command/result/various other fixes
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 */ |