diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-20 04:09:50 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-20 04:09:50 +0000 |
commit | daad722774087de1cf35714868d3762b3ea7cb21 (patch) | |
tree | 60c088f7a81b956c86a2439a5ffb255e07181498 /src/util | |
parent | bfdb4be24bfa474e6036a993e5afac16e77b4d2a (diff) |
fix bug #220 (assertion fails if no query/check-sat); add bug220.smt2 and bug217.smt2 as regressions; fix to build system to only run regressions (not units) if you "make -C test regress", for example (this matches behavior elsewhere)
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/result.cpp | 63 | ||||
-rw-r--r-- | src/util/result.h | 11 |
2 files changed, 41 insertions, 33 deletions
diff --git a/src/util/result.cpp b/src/util/result.cpp index b8f34f47f..9760eaefb 100644 --- a/src/util/result.cpp +++ b/src/util/result.cpp @@ -47,9 +47,6 @@ Result::Result(const string& instr) : } else if(s == "invalid") { d_which = TYPE_VALIDITY; d_validity = INVALID; - } else if(s == "unknown") { - d_which = TYPE_SAT; - d_sat = SAT_UNKNOWN; } else if(s == "incomplete") { d_which = TYPE_SAT; d_sat = SAT_UNKNOWN; @@ -62,13 +59,16 @@ Result::Result(const string& instr) : d_which = TYPE_SAT; d_sat = SAT_UNKNOWN; d_unknownExplanation = MEMOUT; + } else if(s.size() >= 7 && s.compare(0, 7, "unknown") == 0) { + d_which = TYPE_SAT; + d_sat = SAT_UNKNOWN; } else { IllegalArgument(s, "expected satisfiability/validity result, " "instead got `%s'", s.c_str()); } } -bool Result::operator==(const Result& r) const { +bool Result::operator==(const Result& r) const throw() { if(d_which != r.d_which) { return false; } @@ -85,50 +85,56 @@ bool Result::operator==(const Result& r) const { return false; } -Result Result::asSatisfiabilityResult() const { +Result Result::asSatisfiabilityResult() const throw() { if(d_which == TYPE_SAT) { return *this; } - Assert(d_which == TYPE_VALIDITY); - - switch(d_validity) { + if(d_which == TYPE_VALIDITY) { + switch(d_validity) { - case INVALID: - return Result(SAT); + case INVALID: + return Result(SAT); - case VALID: - return Result(UNSAT); + case VALID: + return Result(UNSAT); - case VALIDITY_UNKNOWN: - return Result(SAT_UNKNOWN, d_unknownExplanation); + case VALIDITY_UNKNOWN: + return Result(SAT_UNKNOWN, d_unknownExplanation); - default: - Unhandled(d_validity); + default: + Unhandled(d_validity); + } } + + // TYPE_NONE + return Result(SAT_UNKNOWN, NO_STATUS); } -Result Result::asValidityResult() const { +Result Result::asValidityResult() const throw() { if(d_which == TYPE_VALIDITY) { return *this; } - Assert(d_which == TYPE_SAT); - - switch(d_sat) { + if(d_which == TYPE_SAT) { + switch(d_sat) { - case SAT: - return Result(INVALID); + case SAT: + return Result(INVALID); - case UNSAT: - return Result(VALID); + case UNSAT: + return Result(VALID); - case SAT_UNKNOWN: - return Result(VALIDITY_UNKNOWN, d_unknownExplanation); + case SAT_UNKNOWN: + return Result(VALIDITY_UNKNOWN, d_unknownExplanation); - default: - Unhandled(d_sat); + default: + Unhandled(d_sat); + } } + + // TYPE_NONE + return Result(VALIDITY_UNKNOWN, NO_STATUS); } string Result::toString() const { @@ -164,6 +170,7 @@ ostream& operator<<(ostream& out, case Result::INCOMPLETE: out << "INCOMPLETE"; break; case Result::TIMEOUT: out << "TIMEOUT"; break; case Result::MEMOUT: out << "MEMOUT"; break; + case Result::NO_STATUS: out << "NO_STATUS"; break; case Result::OTHER: out << "OTHER"; break; case Result::UNKNOWN_REASON: out << "UNKNOWN_REASON"; break; default: Unhandled(e); diff --git a/src/util/result.h b/src/util/result.h index 62ddc74d0..1e0729332 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -60,6 +60,7 @@ public: INCOMPLETE, TIMEOUT, MEMOUT, + NO_STATUS, OTHER, UNKNOWN_REASON }; @@ -132,16 +133,16 @@ public: return d_unknownExplanation; } - bool operator==(const Result& r) const; - inline bool operator!=(const Result& r) const; - Result asSatisfiabilityResult() const; - Result asValidityResult() const; + bool operator==(const Result& r) const throw(); + inline bool operator!=(const Result& r) const throw(); + Result asSatisfiabilityResult() const throw(); + Result asValidityResult() const throw(); std::string toString() const; };/* class Result */ -inline bool Result::operator!=(const Result& r) const { +inline bool Result::operator!=(const Result& r) const throw() { return !(*this == r); } |