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.