Result 

class cvc5 :: 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.