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.