diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-02-03 22:20:25 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-02-03 22:20:25 +0000 |
commit | 64d530e5b9096e66398f92d93cf7bc4268df0e70 (patch) | |
tree | 189d63541053faca0c778b0c92d84db8d2b1e0ff /src/util/result.h | |
parent | 842fd54de1da122f4c7274796550c2fe21c11db2 (diff) |
Addressed many of the concerns of bug 10 (build system code review).
Some parts split into other bugs: 19, 20, 21.
Addressed concerns of bug 11 (util package code review).
Slight parser source file modifications: file comments, #included
headers in generated parsers/lexers
Added CVC4::Result propagation back through
MiniSat->PropEngine->SmtEngine->main(). Silenced MiniSat when
verbosity is not requested.
Diffstat (limited to 'src/util/result.h')
-rw-r--r-- | src/util/result.h | 66 |
1 files changed, 63 insertions, 3 deletions
diff --git a/src/util/result.h b/src/util/result.h index 87686d59c..d4980c776 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -16,6 +16,8 @@ #ifndef __CVC4__RESULT_H #define __CVC4__RESULT_H +#include "util/Assert.h" + namespace CVC4 { // TODO: perhaps best to templatize Result on its Kind (SAT/Validity), @@ -52,20 +54,78 @@ public: private: enum SAT d_sat; enum Validity d_validity; - enum { TYPE_SAT, TYPE_VALIDITY } d_which; + enum { TYPE_SAT, TYPE_VALIDITY, TYPE_NONE } d_which; friend std::ostream& CVC4::operator<<(std::ostream& out, Result r); public: - 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) {} + Result() : + d_sat(SAT_UNKNOWN), + d_validity(VALIDITY_UNKNOWN), + d_which(TYPE_NONE) { + } + 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(); enum UnknownExplanation whyUnknown(); + inline Result asSatisfiabilityResult() const; + inline Result asValidityResult() const; + };/* class Result */ +inline Result Result::asSatisfiabilityResult() const { + if(d_which == TYPE_SAT) { + return *this; + } + + switch(d_validity) { + + case INVALID: + return Result(SAT); + + case VALID: + return Result(UNSAT); + + case VALIDITY_UNKNOWN: + return Result(SAT_UNKNOWN); + + default: + Unhandled(d_validity); + } +} + +inline Result Result::asValidityResult() const { + if(d_which == TYPE_VALIDITY) { + return *this; + } + + switch(d_sat) { + + case SAT: + return Result(INVALID); + + case UNSAT: + return Result(VALID); + + case SAT_UNKNOWN: + return Result(VALIDITY_UNKNOWN); + + default: + Unhandled(d_sat); + } +} + inline std::ostream& operator<<(std::ostream& out, Result r) { if(r.d_which == Result::TYPE_SAT) { switch(r.d_sat) { |