diff options
Diffstat (limited to 'src/expr/result.h')
-rw-r--r-- | src/expr/result.h | 69 |
1 files changed, 20 insertions, 49 deletions
diff --git a/src/expr/result.h b/src/expr/result.h index 74697eba6..8069f7ef9 100644 --- a/src/expr/result.h +++ b/src/expr/result.h @@ -75,49 +75,20 @@ private: std::string d_inputName; public: - Result() : - d_sat(SAT_UNKNOWN), - d_validity(VALIDITY_UNKNOWN), - d_which(TYPE_NONE), - d_unknownExplanation(UNKNOWN_REASON), - d_inputName("") { - } - Result(enum Sat s, std::string inputName = "") : - d_sat(s), - d_validity(VALIDITY_UNKNOWN), - d_which(TYPE_SAT), - d_unknownExplanation(UNKNOWN_REASON), - d_inputName(inputName) { - CheckArgument(s != SAT_UNKNOWN, - "Must provide a reason for satisfiability being unknown"); - } - Result(enum Validity v, std::string inputName = "") : - d_sat(SAT_UNKNOWN), - d_validity(v), - d_which(TYPE_VALIDITY), - d_unknownExplanation(UNKNOWN_REASON), - d_inputName(inputName) { - CheckArgument(v != VALIDITY_UNKNOWN, - "Must provide a reason for validity being unknown"); - } - Result(enum Sat s, enum UnknownExplanation unknownExplanation, std::string inputName = "") : - d_sat(s), - d_validity(VALIDITY_UNKNOWN), - d_which(TYPE_SAT), - d_unknownExplanation(unknownExplanation), - d_inputName(inputName) { - CheckArgument(s == SAT_UNKNOWN, - "improper use of unknown-result constructor"); - } - Result(enum Validity v, enum UnknownExplanation unknownExplanation, std::string inputName = "") : - d_sat(SAT_UNKNOWN), - d_validity(v), - d_which(TYPE_VALIDITY), - d_unknownExplanation(unknownExplanation), - d_inputName(inputName) { - CheckArgument(v == VALIDITY_UNKNOWN, - "improper use of unknown-result constructor"); - } + + Result(); + + Result(enum Sat s, std::string inputName = ""); + + Result(enum Validity v, std::string inputName = ""); + + Result(enum Sat s, + enum UnknownExplanation unknownExplanation, + std::string inputName = ""); + + Result(enum Validity v, enum UnknownExplanation unknownExplanation, + std::string inputName = ""); + Result(const std::string& s, std::string inputName = ""); Result(const Result& r, std::string inputName) { @@ -128,24 +99,24 @@ public: enum Sat isSat() const { return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN; } + enum Validity isValid() const { return d_which == TYPE_VALIDITY ? d_validity : VALIDITY_UNKNOWN; } + bool isUnknown() const { return isSat() == SAT_UNKNOWN && isValid() == VALIDITY_UNKNOWN; } + Type getType() const { return d_which; } + bool isNull() const { return d_which == TYPE_NONE; } - enum UnknownExplanation whyUnknown() const { - CheckArgument( isUnknown(), this, - "This result is not unknown, so the reason for " - "being unknown cannot be inquired of it" ); - return d_unknownExplanation; - } + + enum UnknownExplanation whyUnknown() const; bool operator==(const Result& r) const throw(); inline bool operator!=(const Result& r) const throw(); |