Result ¶

class Result ¶

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

Public Functions

Result ( ) ¶

Constructor.

bool isNull ( ) const ¶

Return true if Result is empty, i.e., a nullary Result , and not an actual result returned from a checkSat() (and friends) query.

bool isSat ( ) const ¶

Return true if query was a satisfiable checkSat() or checkSatAssuming() query.

bool isUnsat ( ) const ¶

Return true if query was an unsatisfiable checkSat() or checkSatAssuming() query.

bool isUnknown ( ) const ¶

Return true if query was 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.