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

enum CVC4::Result::Sat

Enumerator
UNSAT
SAT
SAT_UNKNOWN

Definition at line 38 of file result.h.

enum CVC4::Result::Type

Enumerator
TYPE_SAT
TYPE_VALIDITY
TYPE_NONE

Definition at line 50 of file result.h.

enum CVC4::Result::UnknownExplanation

Enumerator
REQUIRES_FULL_CHECK
INCOMPLETE
TIMEOUT
RESOURCEOUT
MEMOUT
INTERRUPTED
NO_STATUS
UNSUPPORTED
OTHER
UNKNOWN_REASON

Definition at line 56 of file result.h.

enum CVC4::Result::Validity

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

Definition at line 160 of file result.h.

References CVC4_PUBLIC, CVC4::operator!=(), CVC4::operator<<(), CVC4::operator==(), and CVC4::options::out.

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:

• src/util/result.h