Result

class cvc5.Result

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

Wrapper class for cvc5::Result.

getUnknownExplanation()

Returns:

An explanation for an unknown query result.

isNull()

Returns:

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

isSat()

Returns:

True if query was a satisfiable Solver.checkSat() or Solver.checkSatAssuming() query.

isUnknown()

Returns:

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

isUnsat()

Returns:

True if query was an usatisfiable Solver.checkSat() or Solver.checkSatAssuming() query.