Result 

This class represents a cvc5::Solver result.

A cvc5::Result encapsulates a 3-valued solver result (sat, unsat, unknown). Explanations for unknown results are represented as enum class cvc5::UnknownExplanation and can be queried via cvc5::Result::getUnknownExplanation() .

• class cvc5::Result

• std::ostream& cvc5::operator<< (std::ostream& out, const Result& r)

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.

std :: ostream & cvc5 :: operator << ( std :: ostream & out , const Result & r ) 

Serialize a Result to given stream.

Parameters :

• out – The output stream.

• r – The result to be serialized to the given output stream.

Returns :

The output stream.