Result 

class Result 

Encapsulation of a three-valued solver result, with explanations.

Public Functions

Result ( ) 

Constructor.

bool isNull ( ) const 

Determine if this Result is a nullary Result .

Returns :

True if Result is empty (a nullary Result ) and not an actual result returned from a checkSat() (and friends) query.

bool isSat ( ) const 

Returns :

True if this result is from a satisfiable checkSat() or checkSatAssuming() query.

bool isUnsat ( ) const 

Returns :

True if this result is from an unsatisfiable checkSat() or checkSatAssuming() query.

bool isUnknown ( ) const 

Returns :

True if result is from a checkSat() or checkSatAssuming() query and cvc5 was not able to determine (un)satisfiability.

bool operator == ( const Result & r ) const 

Operator overloading for equality of two results.

Parameters :

r – The result to compare to for equality.

Returns :

True if the results are equal.

bool operator != ( const Result & r ) const 

Operator overloading for disequality of two results.

Parameters :

r – The result to compare to for disequality.

Returns :

True if the results are disequal.

UnknownExplanation getUnknownExplanation ( ) const 

Returns :

An explanation for an unknown query result.

std :: string toString ( ) const 

Returns :

A string representation of this result.