19 #ifndef __CVC4__RESULT_H 20 #define __CVC4__RESULT_H 74 std::string d_inputName;
79 d_validity(VALIDITY_UNKNOWN),
81 d_unknownExplanation(UNKNOWN_REASON),
86 d_validity(VALIDITY_UNKNOWN),
88 d_unknownExplanation(UNKNOWN_REASON),
89 d_inputName(inputName) {
91 "Must provide a reason for satisfiability being unknown");
96 d_which(TYPE_VALIDITY),
97 d_unknownExplanation(UNKNOWN_REASON),
98 d_inputName(inputName) {
100 "Must provide a reason for validity being unknown");
104 d_validity(VALIDITY_UNKNOWN),
106 d_unknownExplanation(unknownExplanation),
107 d_inputName(inputName) {
109 "improper use of unknown-result constructor");
114 d_which(TYPE_VALIDITY),
115 d_unknownExplanation(unknownExplanation),
116 d_inputName(inputName) {
118 "improper use of unknown-result constructor");
120 Result(
const std::string& s, std::string inputName =
"");
124 d_inputName = inputName;
128 return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN;
131 return d_which == TYPE_VALIDITY ? d_validity : VALIDITY_UNKNOWN;
134 return isSat() == SAT_UNKNOWN && isValid() == VALIDITY_UNKNOWN;
140 return d_which == TYPE_NONE;
144 "This result is not unknown, so the reason for " 145 "being unknown cannot be inquired of it" );
146 return d_unknownExplanation;
151 Result asSatisfiabilityResult()
const throw();
152 Result asValidityResult()
const throw();
154 std::string toString()
const;
161 return !(*
this == r);
Result(const Result &r, std::string inputName)
void CheckArgument(bool cond, const T &arg, const char *fmt,...)
CVC4's exception base class and some associated utilities.
std::string getInputName() const
bool operator!=(const Result &r) const
Macros that should be defined everywhere during the building of the libraries and driver binary...
Three-valued SMT result, with optional explanation.
Result(enum Validity v, std::string inputName="")
Result(enum Sat s, std::string inputName="")
Result(enum Sat s, enum UnknownExplanation unknownExplanation, std::string inputName="")
struct CVC4::options::out__option_t out
std::ostream & operator<<(std::ostream &out, SimplificationMode mode)
bool operator!=(enum Result::Sat s, const Result &r)
bool operator==(enum Result::Sat s, const Result &r)
Result(enum Validity v, enum UnknownExplanation unknownExplanation, std::string inputName="")