diff options
Diffstat (limited to 'src/util/result.h')
-rw-r--r-- | src/util/result.h | 75 |
1 files changed, 26 insertions, 49 deletions
diff --git a/src/util/result.h b/src/util/result.h index 8303ad0e8..80fbc0cf7 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -35,24 +35,12 @@ std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_PUBLIC; * Three-valued SMT result, with optional explanation. */ class CVC4_PUBLIC Result { -public: - enum Sat { - UNSAT = 0, - SAT = 1, - SAT_UNKNOWN = 2 - }; + public: + enum Sat { UNSAT = 0, SAT = 1, SAT_UNKNOWN = 2 }; - enum Validity { - INVALID = 0, - VALID = 1, - VALIDITY_UNKNOWN = 2 - }; + enum Validity { INVALID = 0, VALID = 1, VALIDITY_UNKNOWN = 2 }; - enum Type { - TYPE_SAT, - TYPE_VALIDITY, - TYPE_NONE - }; + enum Type { TYPE_SAT, TYPE_VALIDITY, TYPE_NONE }; enum UnknownExplanation { REQUIRES_FULL_CHECK, @@ -67,23 +55,21 @@ public: UNKNOWN_REASON }; -private: + private: enum Sat d_sat; enum Validity d_validity; enum Type d_which; enum UnknownExplanation d_unknownExplanation; std::string d_inputName; -public: - + public: Result(); Result(enum Sat s, std::string inputName = ""); Result(enum Validity v, std::string inputName = ""); - Result(enum Sat s, - enum UnknownExplanation unknownExplanation, + Result(enum Sat s, enum UnknownExplanation unknownExplanation, std::string inputName = ""); Result(enum Validity v, enum UnknownExplanation unknownExplanation, @@ -96,9 +82,7 @@ public: d_inputName = inputName; } - enum Sat isSat() const { - return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN; - } + 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; @@ -108,20 +92,16 @@ public: return isSat() == SAT_UNKNOWN && isValid() == VALIDITY_UNKNOWN; } - Type getType() const { - return d_which; - } + Type getType() const { return d_which; } - bool isNull() const { - return d_which == TYPE_NONE; - } + bool isNull() const { return d_which == TYPE_NONE; } enum UnknownExplanation whyUnknown() const; - bool operator==(const Result& r) const throw(); - inline bool operator!=(const Result& r) const throw(); - Result asSatisfiabilityResult() const throw(); - Result asValidityResult() const throw(); + bool operator==(const Result& r) const; + inline bool operator!=(const Result& r) const; + Result asSatisfiabilityResult() const; + Result asValidityResult() const; std::string toString() const; @@ -130,19 +110,19 @@ public: /** * Write a Result out to a stream in this language. */ - void toStream(std::ostream& out, OutputLanguage language) const throw(); + void toStream(std::ostream& out, OutputLanguage language) const; /** * This is mostly the same the default * If getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN, * */ - void toStreamSmt2(std::ostream& out) const throw(); + void toStreamSmt2(std::ostream& out) const; /** * Write a Result out to a stream in the Tptp format */ - void toStreamTptp(std::ostream& out) const throw(); + void toStreamTptp(std::ostream& out) const; /** * Write a Result out to a stream. @@ -152,26 +132,23 @@ public: * is overridable by each Printer, since sometimes an output language * has a particular preference for how results should appear. */ - void toStreamDefault(std::ostream& out) const throw(); -};/* class Result */ + void toStreamDefault(std::ostream& out) const; +}; /* class Result */ -inline bool Result::operator!=(const Result& r) const throw() { - return !(*this == r); -} +inline bool Result::operator!=(const Result& r) const { return !(*this == r); } -std::ostream& operator<<(std::ostream& out, - enum Result::Sat s) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, enum Result::Sat s) CVC4_PUBLIC; std::ostream& operator<<(std::ostream& out, enum Result::Validity v) CVC4_PUBLIC; std::ostream& operator<<(std::ostream& out, enum Result::UnknownExplanation e) CVC4_PUBLIC; -bool operator==(enum Result::Sat s, const Result& r) throw() CVC4_PUBLIC; -bool operator==(enum Result::Validity v, const Result& r) throw() CVC4_PUBLIC; +bool operator==(enum Result::Sat s, const Result& r) CVC4_PUBLIC; +bool operator==(enum Result::Validity v, const Result& r) CVC4_PUBLIC; -bool operator!=(enum Result::Sat s, const Result& r) throw() CVC4_PUBLIC; -bool operator!=(enum Result::Validity v, const Result& r) throw() CVC4_PUBLIC; +bool operator!=(enum Result::Sat s, const Result& r) CVC4_PUBLIC; +bool operator!=(enum Result::Validity v, const Result& r) CVC4_PUBLIC; -}/* CVC4 namespace */ +} /* CVC4 namespace */ #endif /* __CVC4__RESULT_H */ |