cvc4-1.4
CVC4::Result Class Reference

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
 

Detailed Description

Three-valued SMT result, with optional explanation.

Definition at line 36 of file result.h.

Member Enumeration Documentation

Enumerator
UNSAT 
SAT 
SAT_UNKNOWN 

Definition at line 38 of file result.h.

Enumerator
TYPE_SAT 
TYPE_VALIDITY 
TYPE_NONE 

Definition at line 50 of file result.h.

Enumerator
REQUIRES_FULL_CHECK 
INCOMPLETE 
TIMEOUT 
RESOURCEOUT 
MEMOUT 
INTERRUPTED 
NO_STATUS 
UNSUPPORTED 
OTHER 
UNKNOWN_REASON 

Definition at line 56 of file result.h.

Enumerator
INVALID 
VALID 
VALIDITY_UNKNOWN 

Definition at line 44 of file result.h.

Constructor & Destructor Documentation

CVC4::Result::Result ( )
inline

Definition at line 77 of file result.h.

CVC4::Result::Result ( enum Sat  s,
std::string  inputName = "" 
)
inline

Definition at line 84 of file result.h.

References CVC4::CheckArgument().

CVC4::Result::Result ( enum Validity  v,
std::string  inputName = "" 
)
inline

Definition at line 93 of file result.h.

References CVC4::CheckArgument().

CVC4::Result::Result ( enum Sat  s,
enum UnknownExplanation  unknownExplanation,
std::string  inputName = "" 
)
inline

Definition at line 102 of file result.h.

References CVC4::CheckArgument().

CVC4::Result::Result ( enum Validity  v,
enum UnknownExplanation  unknownExplanation,
std::string  inputName = "" 
)
inline

Definition at line 111 of file result.h.

References CVC4::CheckArgument().

CVC4::Result::Result ( const std::string &  s,
std::string  inputName = "" 
)
CVC4::Result::Result ( const Result r,
std::string  inputName 
)
inline

Definition at line 122 of file result.h.

Member Function Documentation

Result CVC4::Result::asSatisfiabilityResult ( ) const
throw (
)
Result CVC4::Result::asValidityResult ( ) const
throw (
)
std::string CVC4::Result::getInputName ( ) const
inline

Definition at line 156 of file result.h.

Type CVC4::Result::getType ( ) const
inline

Definition at line 136 of file result.h.

bool CVC4::Result::isNull ( ) const
inline

Definition at line 139 of file result.h.

enum Sat CVC4::Result::isSat ( ) const
inline

Definition at line 127 of file result.h.

bool CVC4::Result::isUnknown ( ) const
inline

Definition at line 133 of file result.h.

enum Validity CVC4::Result::isValid ( ) const
inline

Definition at line 130 of file result.h.

bool CVC4::Result::operator!= ( const Result r) const
throw (
)
inline
bool CVC4::Result::operator== ( const Result r) const
throw (
)
std::string CVC4::Result::toString ( ) const
enum UnknownExplanation CVC4::Result::whyUnknown ( ) const
inline

Definition at line 142 of file result.h.

References CVC4::CheckArgument(), CVC4::operator!=(), and CVC4::operator==().


The documentation for this class was generated from the following file: