summaryrefslogtreecommitdiff
path: root/src/util/result.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/util/result.cpp')
-rw-r--r--src/util/result.cpp383
1 files changed, 200 insertions, 183 deletions
diff --git a/src/util/result.cpp b/src/util/result.cpp
index 51b1a8de1..af28269f1 100644
--- a/src/util/result.cpp
+++ b/src/util/result.cpp
@@ -28,167 +28,152 @@ using namespace std;
namespace CVC4 {
Result::Result()
- : d_sat(SAT_UNKNOWN)
- , d_validity(VALIDITY_UNKNOWN)
- , d_which(TYPE_NONE)
- , d_unknownExplanation(UNKNOWN_REASON)
- , d_inputName("")
-{ }
-
+ : d_sat(SAT_UNKNOWN),
+ d_validity(VALIDITY_UNKNOWN),
+ d_which(TYPE_NONE),
+ d_unknownExplanation(UNKNOWN_REASON),
+ d_inputName("") {}
Result::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)
-{
+ : d_sat(s),
+ d_validity(VALIDITY_UNKNOWN),
+ d_which(TYPE_SAT),
+ d_unknownExplanation(UNKNOWN_REASON),
+ d_inputName(inputName) {
PrettyCheckArgument(s != SAT_UNKNOWN,
"Must provide a reason for satisfiability being unknown");
}
Result::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)
-{
+ : d_sat(SAT_UNKNOWN),
+ d_validity(v),
+ d_which(TYPE_VALIDITY),
+ d_unknownExplanation(UNKNOWN_REASON),
+ d_inputName(inputName) {
PrettyCheckArgument(v != VALIDITY_UNKNOWN,
"Must provide a reason for validity being unknown");
}
-
Result::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)
-{
+ : d_sat(s),
+ d_validity(VALIDITY_UNKNOWN),
+ d_which(TYPE_SAT),
+ d_unknownExplanation(unknownExplanation),
+ d_inputName(inputName) {
PrettyCheckArgument(s == SAT_UNKNOWN,
"improper use of unknown-result constructor");
}
Result::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)
-{
+ : d_sat(SAT_UNKNOWN),
+ d_validity(v),
+ d_which(TYPE_VALIDITY),
+ d_unknownExplanation(unknownExplanation),
+ d_inputName(inputName) {
PrettyCheckArgument(v == VALIDITY_UNKNOWN,
"improper use of unknown-result constructor");
}
-Result::Result(const std::string& instr, std::string inputName) :
- d_sat(SAT_UNKNOWN),
- d_validity(VALIDITY_UNKNOWN),
- d_which(TYPE_NONE),
- d_unknownExplanation(UNKNOWN_REASON),
- d_inputName(inputName) {
+Result::Result(const std::string& instr, std::string inputName)
+ : d_sat(SAT_UNKNOWN),
+ d_validity(VALIDITY_UNKNOWN),
+ d_which(TYPE_NONE),
+ d_unknownExplanation(UNKNOWN_REASON),
+ d_inputName(inputName) {
string s = instr;
transform(s.begin(), s.end(), s.begin(), ::tolower);
- if(s == "sat" || s == "satisfiable") {
+ if (s == "sat" || s == "satisfiable") {
d_which = TYPE_SAT;
d_sat = SAT;
- } else if(s == "unsat" || s == "unsatisfiable") {
+ } else if (s == "unsat" || s == "unsatisfiable") {
d_which = TYPE_SAT;
d_sat = UNSAT;
- } else if(s == "valid") {
+ } else if (s == "valid") {
d_which = TYPE_VALIDITY;
d_validity = VALID;
- } else if(s == "invalid") {
+ } else if (s == "invalid") {
d_which = TYPE_VALIDITY;
d_validity = INVALID;
- } else if(s == "incomplete") {
+ } else if (s == "incomplete") {
d_which = TYPE_SAT;
d_sat = SAT_UNKNOWN;
d_unknownExplanation = INCOMPLETE;
- } else if(s == "timeout") {
+ } else if (s == "timeout") {
d_which = TYPE_SAT;
d_sat = SAT_UNKNOWN;
d_unknownExplanation = TIMEOUT;
- } else if(s == "resourceout") {
+ } else if (s == "resourceout") {
d_which = TYPE_SAT;
d_sat = SAT_UNKNOWN;
d_unknownExplanation = RESOURCEOUT;
- } else if(s == "memout") {
+ } else if (s == "memout") {
d_which = TYPE_SAT;
d_sat = SAT_UNKNOWN;
d_unknownExplanation = MEMOUT;
- } else if(s == "interrupted") {
+ } else if (s == "interrupted") {
d_which = TYPE_SAT;
d_sat = SAT_UNKNOWN;
d_unknownExplanation = INTERRUPTED;
- } else if(s.size() >= 7 && s.compare(0, 7, "unknown") == 0) {
+ } 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());
+ IllegalArgument(s,
+ "expected satisfiability/validity result, "
+ "instead got `%s'",
+ s.c_str());
}
}
Result::UnknownExplanation Result::whyUnknown() const {
- PrettyCheckArgument( isUnknown(), this,
- "This result is not unknown, so the reason for "
- "being unknown cannot be inquired of it" );
+ PrettyCheckArgument(isUnknown(), this,
+ "This result is not unknown, so the reason for "
+ "being unknown cannot be inquired of it");
return d_unknownExplanation;
}
-bool Result::operator==(const Result& r) const throw() {
- if(d_which != r.d_which) {
+bool Result::operator==(const Result& r) const {
+ if (d_which != r.d_which) {
return false;
}
- if(d_which == TYPE_SAT) {
- return d_sat == r.d_sat &&
- ( d_sat != SAT_UNKNOWN ||
- d_unknownExplanation == r.d_unknownExplanation );
+ if (d_which == TYPE_SAT) {
+ return d_sat == r.d_sat && (d_sat != SAT_UNKNOWN ||
+ d_unknownExplanation == r.d_unknownExplanation);
}
- if(d_which == TYPE_VALIDITY) {
+ if (d_which == TYPE_VALIDITY) {
return d_validity == r.d_validity &&
- ( d_validity != VALIDITY_UNKNOWN ||
- d_unknownExplanation == r.d_unknownExplanation );
+ (d_validity != VALIDITY_UNKNOWN ||
+ d_unknownExplanation == r.d_unknownExplanation);
}
return false;
}
-bool operator==(enum Result::Sat sr, const Result& r) throw() {
- return r == sr;
-}
+bool operator==(enum Result::Sat sr, const Result& r) { return r == sr; }
-bool operator==(enum Result::Validity vr, const Result& r) throw() {
- return r == vr;
-}
-bool operator!=(enum Result::Sat s, const Result& r) throw(){
- return !(s == r);
-}
-bool operator!=(enum Result::Validity v, const Result& r) throw(){
- return !(v == r);
-}
+bool operator==(enum Result::Validity vr, const Result& r) { return r == vr; }
+bool operator!=(enum Result::Sat s, const Result& r) { return !(s == r); }
+bool operator!=(enum Result::Validity v, const Result& r) { return !(v == r); }
-Result Result::asSatisfiabilityResult() const throw() {
- if(d_which == TYPE_SAT) {
+Result Result::asSatisfiabilityResult() const {
+ if (d_which == TYPE_SAT) {
return *this;
}
- if(d_which == TYPE_VALIDITY) {
- switch(d_validity) {
-
- case INVALID:
- return Result(SAT, d_inputName);
+ if (d_which == TYPE_VALIDITY) {
+ switch (d_validity) {
+ case INVALID:
+ return Result(SAT, d_inputName);
- case VALID:
- return Result(UNSAT, d_inputName);
+ case VALID:
+ return Result(UNSAT, d_inputName);
- case VALIDITY_UNKNOWN:
- return Result(SAT_UNKNOWN, d_unknownExplanation, d_inputName);
+ case VALIDITY_UNKNOWN:
+ return Result(SAT_UNKNOWN, d_unknownExplanation, d_inputName);
- default:
- Unhandled(d_validity);
+ default:
+ Unhandled(d_validity);
}
}
@@ -196,25 +181,24 @@ Result Result::asSatisfiabilityResult() const throw() {
return Result(SAT_UNKNOWN, NO_STATUS, d_inputName);
}
-Result Result::asValidityResult() const throw() {
- if(d_which == TYPE_VALIDITY) {
+Result Result::asValidityResult() const {
+ if (d_which == TYPE_VALIDITY) {
return *this;
}
- if(d_which == TYPE_SAT) {
- switch(d_sat) {
-
- case SAT:
- return Result(INVALID, d_inputName);
+ if (d_which == TYPE_SAT) {
+ switch (d_sat) {
+ case SAT:
+ return Result(INVALID, d_inputName);
- case UNSAT:
- return Result(VALID, d_inputName);
+ case UNSAT:
+ return Result(VALID, d_inputName);
- case SAT_UNKNOWN:
- return Result(VALIDITY_UNKNOWN, d_unknownExplanation, d_inputName);
+ case SAT_UNKNOWN:
+ return Result(VALIDITY_UNKNOWN, d_unknownExplanation, d_inputName);
- default:
- Unhandled(d_sat);
+ default:
+ Unhandled(d_sat);
}
}
@@ -229,38 +213,73 @@ string Result::toString() const {
}
ostream& operator<<(ostream& out, enum Result::Sat s) {
- switch(s) {
- case Result::UNSAT: out << "UNSAT"; break;
- case Result::SAT: out << "SAT"; break;
- case Result::SAT_UNKNOWN: out << "SAT_UNKNOWN"; break;
- default: Unhandled(s);
+ switch (s) {
+ case Result::UNSAT:
+ out << "UNSAT";
+ break;
+ case Result::SAT:
+ out << "SAT";
+ break;
+ case Result::SAT_UNKNOWN:
+ out << "SAT_UNKNOWN";
+ break;
+ default:
+ Unhandled(s);
}
return out;
}
ostream& operator<<(ostream& out, enum Result::Validity v) {
- switch(v) {
- case Result::INVALID: out << "INVALID"; break;
- case Result::VALID: out << "VALID"; break;
- case Result::VALIDITY_UNKNOWN: out << "VALIDITY_UNKNOWN"; break;
- default: Unhandled(v);
+ switch (v) {
+ case Result::INVALID:
+ out << "INVALID";
+ break;
+ case Result::VALID:
+ out << "VALID";
+ break;
+ case Result::VALIDITY_UNKNOWN:
+ out << "VALIDITY_UNKNOWN";
+ break;
+ default:
+ Unhandled(v);
}
return out;
}
ostream& operator<<(ostream& out, enum Result::UnknownExplanation e) {
- switch(e) {
- case Result::REQUIRES_FULL_CHECK: out << "REQUIRES_FULL_CHECK"; break;
- case Result::INCOMPLETE: out << "INCOMPLETE"; break;
- case Result::TIMEOUT: out << "TIMEOUT"; break;
- case Result::RESOURCEOUT: out << "RESOURCEOUT"; break;
- case Result::MEMOUT: out << "MEMOUT"; break;
- case Result::INTERRUPTED: out << "INTERRUPTED"; break;
- case Result::NO_STATUS: out << "NO_STATUS"; break;
- case Result::UNSUPPORTED: out << "UNSUPPORTED"; break;
- case Result::OTHER: out << "OTHER"; break;
- case Result::UNKNOWN_REASON: out << "UNKNOWN_REASON"; break;
- default: Unhandled(e);
+ switch (e) {
+ case Result::REQUIRES_FULL_CHECK:
+ out << "REQUIRES_FULL_CHECK";
+ break;
+ case Result::INCOMPLETE:
+ out << "INCOMPLETE";
+ break;
+ case Result::TIMEOUT:
+ out << "TIMEOUT";
+ break;
+ case Result::RESOURCEOUT:
+ out << "RESOURCEOUT";
+ break;
+ case Result::MEMOUT:
+ out << "MEMOUT";
+ break;
+ case Result::INTERRUPTED:
+ out << "INTERRUPTED";
+ break;
+ case Result::NO_STATUS:
+ out << "NO_STATUS";
+ break;
+ case Result::UNSUPPORTED:
+ out << "UNSUPPORTED";
+ break;
+ case Result::OTHER:
+ out << "OTHER";
+ break;
+ case Result::UNKNOWN_REASON:
+ out << "UNKNOWN_REASON";
+ break;
+ default:
+ Unhandled(e);
}
return out;
}
@@ -268,61 +287,59 @@ ostream& operator<<(ostream& out, enum Result::UnknownExplanation e) {
ostream& operator<<(ostream& out, const Result& r) {
r.toStream(out, language::SetLanguage::getLanguage(out));
return out;
-}/* operator<<(ostream&, const Result&) */
-
-
-void Result::toStreamDefault(std::ostream& out) const throw() {
- if(getType() == Result::TYPE_SAT) {
- switch(isSat()) {
- case Result::UNSAT:
- out << "unsat";
- break;
- case Result::SAT:
- out << "sat";
- break;
- case Result::SAT_UNKNOWN:
- out << "unknown";
- if(whyUnknown() != Result::UNKNOWN_REASON) {
- out << " (" << whyUnknown() << ")";
- }
- break;
+} /* operator<<(ostream&, const Result&) */
+
+void Result::toStreamDefault(std::ostream& out) const {
+ if (getType() == Result::TYPE_SAT) {
+ switch (isSat()) {
+ case Result::UNSAT:
+ out << "unsat";
+ break;
+ case Result::SAT:
+ out << "sat";
+ break;
+ case Result::SAT_UNKNOWN:
+ out << "unknown";
+ if (whyUnknown() != Result::UNKNOWN_REASON) {
+ out << " (" << whyUnknown() << ")";
+ }
+ break;
}
} else {
- switch(isValid()) {
- case Result::INVALID:
- out << "invalid";
- break;
- case Result::VALID:
- out << "valid";
- break;
- case Result::VALIDITY_UNKNOWN:
- out << "unknown";
- if(whyUnknown() != Result::UNKNOWN_REASON) {
- out << " (" << whyUnknown() << ")";
- }
- break;
+ switch (isValid()) {
+ case Result::INVALID:
+ out << "invalid";
+ break;
+ case Result::VALID:
+ out << "valid";
+ break;
+ case Result::VALIDITY_UNKNOWN:
+ out << "unknown";
+ if (whyUnknown() != Result::UNKNOWN_REASON) {
+ out << " (" << whyUnknown() << ")";
+ }
+ break;
}
}
-}/* Result::toStreamDefault() */
+} /* Result::toStreamDefault() */
-
-void Result::toStreamSmt2(ostream& out) const throw(){
- if(getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN) {
+void Result::toStreamSmt2(ostream& out) const {
+ if (getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN) {
out << "unknown";
} else {
toStreamDefault(out);
}
}
-void Result::toStreamTptp(std::ostream& out) const throw() {
+void Result::toStreamTptp(std::ostream& out) const {
out << "% SZS status ";
- if(isSat() == Result::SAT) {
+ if (isSat() == Result::SAT) {
out << "Satisfiable";
- } else if(isSat() == Result::UNSAT) {
+ } else if (isSat() == Result::UNSAT) {
out << "Unsatisfiable";
- } else if(isValid() == Result::VALID) {
+ } else if (isValid() == Result::VALID) {
out << "Theorem";
- } else if(isValid() == Result::INVALID) {
+ } else if (isValid() == Result::INVALID) {
out << "CounterSatisfiable";
} else {
out << "GaveUp";
@@ -330,27 +347,27 @@ void Result::toStreamTptp(std::ostream& out) const throw() {
out << " for " << getInputName();
}
-void Result::toStream(std::ostream& out, OutputLanguage language) const throw() {
- switch(language) {
- case language::output::LANG_SMTLIB_V2_0:
- case language::output::LANG_SMTLIB_V2_5:
- case language::output::LANG_SYGUS:
- case language::output::LANG_Z3STR:
- toStreamSmt2(out);
- break;
- case language::output::LANG_TPTP:
- toStreamTptp(out);
- break;
- case language::output::LANG_AST:
- case language::output::LANG_AUTO:
- case language::output::LANG_CVC3:
- case language::output::LANG_CVC4:
- case language::output::LANG_MAX:
- case language::output::LANG_SMTLIB_V1:
- default:
- toStreamDefault(out);
- break;
+void Result::toStream(std::ostream& out, OutputLanguage language) const {
+ switch (language) {
+ case language::output::LANG_SMTLIB_V2_0:
+ case language::output::LANG_SMTLIB_V2_5:
+ case language::output::LANG_SYGUS:
+ case language::output::LANG_Z3STR:
+ toStreamSmt2(out);
+ break;
+ case language::output::LANG_TPTP:
+ toStreamTptp(out);
+ break;
+ case language::output::LANG_AST:
+ case language::output::LANG_AUTO:
+ case language::output::LANG_CVC3:
+ case language::output::LANG_CVC4:
+ case language::output::LANG_MAX:
+ case language::output::LANG_SMTLIB_V1:
+ default:
+ toStreamDefault(out);
+ break;
};
}
-}/* CVC4 namespace */
+} /* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback