diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-10 22:15:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-10 22:15:38 +0000 |
commit | d6b37239a2e525e7878d3bb0b4372a8dabc340a9 (patch) | |
tree | 3db6b54c8b5873db1e6c91b1577d431d74632c66 /src/util/result.h | |
parent | 7a059452ebf5729723f610da9258a47007e38253 (diff) |
additional model gen and SMT-LIBv2 compliance work: (get-assignment) now supported; work on Result type (biggest noticeable change is that CVC4 now outputs lowercase "sat" and "unsat"), Options class moved to src/smt, to allow for future work on runtime configuration via (set-option) command
Diffstat (limited to 'src/util/result.h')
-rw-r--r-- | src/util/result.h | 161 |
1 files changed, 72 insertions, 89 deletions
diff --git a/src/util/result.h b/src/util/result.h index f1f6ae1c2..fc2fa4522 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -21,20 +21,29 @@ #ifndef __CVC4__RESULT_H #define __CVC4__RESULT_H +#include <iostream> +#include <string> + +#include "util/Assert.h" + namespace CVC4 { -// TODO: perhaps best to templatize Result on its Kind (SAT/Validity), -// but this requires doing the same for Prover and needs discussion. +// TODO: either templatize Result on its Kind (Sat/Validity) or subclass. +// TODO: INVALID/SAT provide models, etc?---perhaps just by linking back +// into the SmtEngine that produced the Result? +// TODO: make unconstructible except by SmtEngine? That would ensure that +// any Result in the system is bona fide. -// TODO: subclass to provide models, etc. This is really just -// intended as a three-valued response code. +class Result; + +std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_PUBLIC; /** - * Three-valued, immutable SMT result, with optional explanation. + * Three-valued SMT result, with optional explanation. */ class CVC4_PUBLIC Result { public: - enum SAT { + enum Sat { UNSAT = 0, SAT = 1, SAT_UNKNOWN = 2 @@ -50,121 +59,95 @@ public: REQUIRES_FULL_CHECK, INCOMPLETE, TIMEOUT, - BAIL, - OTHER + MEMOUT, + OTHER, + UNKNOWN_REASON }; private: - enum SAT d_sat; + enum Sat d_sat; enum Validity d_validity; enum { TYPE_SAT, TYPE_VALIDITY, TYPE_NONE } d_which; + enum UnknownExplanation d_unknownExplanation; - friend std::ostream& CVC4::operator<<(std::ostream& out, Result r); + friend std::ostream& CVC4::operator<<(std::ostream& out, const Result& r); public: Result() : d_sat(SAT_UNKNOWN), d_validity(VALIDITY_UNKNOWN), - d_which(TYPE_NONE) { + d_which(TYPE_NONE), + d_unknownExplanation(UNKNOWN_REASON) { } - Result(enum SAT s) : + Result(enum Sat s) : d_sat(s), d_validity(VALIDITY_UNKNOWN), - d_which(TYPE_SAT) { + d_which(TYPE_SAT), + d_unknownExplanation(UNKNOWN_REASON) { + CheckArgument(s != SAT_UNKNOWN, + "Must provide a reason for satisfiability being unknown"); } Result(enum Validity v) : d_sat(SAT_UNKNOWN), d_validity(v), - d_which(TYPE_VALIDITY) { + d_which(TYPE_VALIDITY), + d_unknownExplanation(UNKNOWN_REASON) { + CheckArgument(v != VALIDITY_UNKNOWN, + "Must provide a reason for validity being unknown"); + } + Result(enum Sat s, enum UnknownExplanation unknownExplanation) : + d_sat(s), + d_validity(VALIDITY_UNKNOWN), + d_which(TYPE_SAT), + d_unknownExplanation(unknownExplanation) { + CheckArgument(s == SAT_UNKNOWN, + "improper use of unknown-result constructor"); + } + Result(enum Validity v, enum UnknownExplanation unknownExplanation) : + d_sat(SAT_UNKNOWN), + d_validity(v), + d_which(TYPE_VALIDITY), + d_unknownExplanation(unknownExplanation) { + CheckArgument(v == VALIDITY_UNKNOWN, + "improper use of unknown-result constructor"); } + Result(const std::string& s); - enum SAT isSAT() { + enum Sat isSat() const { return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN; } - enum Validity isValid() { + enum Validity isValid() const { return d_which == TYPE_VALIDITY ? d_validity : VALIDITY_UNKNOWN; } - enum UnknownExplanation whyUnknown(); - - inline bool operator==(Result r) { - if(d_which != r.d_which) { - return false; - } - if(d_which == TYPE_SAT) { - return d_sat == r.d_sat; - } - if(d_which == TYPE_VALIDITY) { - return d_validity == r.d_validity; - } - return false; - } - inline bool operator!=(Result r) { - return !(*this == r); - } - 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); + bool isUnknown() const { + return isSat() == SAT_UNKNOWN && isValid() == VALIDITY_UNKNOWN; } -} - -inline Result Result::asValidityResult() const { - if(d_which == TYPE_VALIDITY) { - return *this; + enum UnknownExplanation whyUnknown() const { + AlwaysAssert( isUnknown(), + "This result is not unknown, so the reason for " + "being unknown cannot be inquired of it" ); + return d_unknownExplanation; } - switch(d_sat) { - - case SAT: - return Result(INVALID); + bool operator==(const Result& r) const; + inline bool operator!=(const Result& r) const; + Result asSatisfiabilityResult() const; + Result asValidityResult() const; - case UNSAT: - return Result(VALID); + std::string toString() const; - case SAT_UNKNOWN: - return Result(VALIDITY_UNKNOWN); +};/* class Result */ - default: - Unhandled(d_sat); - } +inline bool Result::operator!=(const Result& r) const { + return !(*this == r); } -inline std::ostream& operator<<(std::ostream& out, Result r) { - if(r.d_which == Result::TYPE_SAT) { - switch(r.d_sat) { - case Result::UNSAT: out << "UNSAT"; break; - case Result::SAT: out << "SAT"; break; - case Result::SAT_UNKNOWN: out << "SAT_UNKNOWN"; break; - } - } else { - switch(r.d_validity) { - case Result::INVALID: out << "INVALID"; break; - case Result::VALID: out << "VALID"; break; - case Result::VALIDITY_UNKNOWN: out << "VALIDITY_UNKNOWN"; break; - } - } - - return out; -} +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; }/* CVC4 namespace */ |