Cvc5Result

This class represents a Cvc5 result.

A Cvc5Result encapsulates a 3-valued solver result (sat, unsat, unknown). Explanations for unknown results are represented as enum class Cvc5UnknownExplanation and can be queried via cvc5_result_get_unknown_explanation().

typedef struct cvc5_result_t *Cvc5Result: Encapsulation of a three-valued solver result, with explanations.

Cvc5Result cvc5_result_copy(Cvc5Result result)

Make copy of result, increases reference counter of result.

Note

This step is optional and allows users to manage resources in a more fine-grained manner.

Parameters:: result – The result to copy.
Returns:: The same result with its reference count increased by one.

void cvc5_result_release(Cvc5Result result)

Release copy of result, decrements reference counter of result.

Note

This step is optional and allows users to release resources in a more fine-grained manner. Further, any API function that returns a copy that is owned by the callee of the function and thus, can be released.

Parameters:: result – The result to release.

bool cvc5_result_is_null(const Cvc5Result result)

Determine if a given result is empty (a nullary result) and not an actual result returned from a cvc5_check_sat() (and friends) query.

Parameters:: result – The result.
Returns:: True if the given result is a nullary result.

bool cvc5_result_is_sat(const Cvc5Result result)

Determine if given result is from a satisfiable cvc5_check_sat() or cvc5_check_sat_ssuming() query.

Parameters:: result – The result.
Returns:: True if result is from a satisfiable query.

bool cvc5_result_is_unsat(const Cvc5Result result)

Determine if given result is from an unsatisfiable cvc5_check_sat() or cvc5_check_sat_assuming() query.

Parameters:: result – The result.
Returns:: True if result is from an unsatisfiable query.

bool cvc5_result_is_unknown(const Cvc5Result result)

Determine if given result is from a cvc5_check_sat() or cvc5_check_sat_assuming() query and cvc5 was not able to determine (un)satisfiability.

Parameters:: result – The result.
Returns:: True if result is from a query where cvc5 was not able to determine (un)satisfiability.

bool cvc5_result_is_equal(const Cvc5Result a, const Cvc5Result b)

Determine equality of two results.

Parameters:

a – The first result to compare to for equality.
b – The second result to compare to for equality.

Returns:

True if the results are equal.

bool cvc5_result_is_disequal(const Cvc5Result a, const Cvc5Result b)

Operator overloading for disequality of two results.

Parameters:

a – The first result to compare to for disequality.
b – The second result to compare to for disequality.

Returns:

True if the results are disequal.

Cvc5UnknownExplanation cvc5_result_get_unknown_explanation(const Cvc5Result result)

Get the explanation for an unknown result.

Parameters:: result – The result.
Returns:: An explanation for an unknown query result.

const char *cvc5_result_to_string(const Cvc5Result result)

Get the string representation of a given result.

Note

The returned char* pointer is only valid until the next call to this function.

Parameters:: result – The result.
Returns:: The string representation.

size_t cvc5_result_hash(Cvc5Result result)

Compute the hash value of a result.

Parameters:: result – The result.
Returns:: The hash value of the result.