cvc4-1.3
|
Three-valued SMT result, with optional explanation. More...
#include <result.h>
Public Types | |
enum | Sat { UNSAT, SAT, SAT_UNKNOWN } |
enum | Validity { INVALID, VALID, VALIDITY_UNKNOWN } |
enum | Type { TYPE_SAT, TYPE_VALIDITY, TYPE_NONE } |
enum | UnknownExplanation { REQUIRES_FULL_CHECK, INCOMPLETE, TIMEOUT, RESOURCEOUT, MEMOUT, INTERRUPTED, NO_STATUS, UNSUPPORTED, OTHER, UNKNOWN_REASON } |
Public Member Functions | |
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) | |
enum Sat | isSat () const |
enum Validity | isValid () const |
bool | isUnknown () const |
Type | getType () const |
bool | isNull () const |
enum UnknownExplanation | whyUnknown () const |
bool | operator== (const Result &r) const throw () |
bool | operator!= (const Result &r) const throw () |
Result | asSatisfiabilityResult () const throw () |
Result | asValidityResult () const throw () |
std::string | toString () const |
std::string | getInputName () const |
enum CVC4::Result::Sat |
enum CVC4::Result::Type |
|
inline |
Definition at line 84 of file result.h.
References CVC4::CheckArgument().
|
inline |
Definition at line 93 of file result.h.
References CVC4::CheckArgument().
|
inline |
Definition at line 102 of file result.h.
References CVC4::CheckArgument().
|
inline |
Definition at line 111 of file result.h.
References CVC4::CheckArgument().
CVC4::Result::Result | ( | const std::string & | s, |
std::string | inputName = "" |
||
) |
|
inline |
Result CVC4::Result::asSatisfiabilityResult | ( | ) | const | |
throw | ( | |||
) |
Result CVC4::Result::asValidityResult | ( | ) | const | |
throw | ( | |||
) |
|
inline |
bool CVC4::Result::operator== | ( | const Result & | r | ) | const |
throw | ( | ||||
) |
std::string CVC4::Result::toString | ( | ) | const |
|
inline |
Definition at line 142 of file result.h.
References CVC4::CheckArgument().