Cvc5SynthResult

This struct represents a Cvc5 SyGus synthesis result.

typedef struct cvc5_synth_result_t *Cvc5SynthResult

Encapsulation of a solver synth result.

This is the return value of the API functions:

• cvc5_check_synth()

• cvc5_check_synth_next()

which we call “synthesis queries”. This class indicates whether the synthesis query has a solution, has no solution, or is unknown.

bool cvc5_synth_result_is_null(const Cvc5SynthResult result)

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

Parameters:

result – The result.

Returns:

True if the given result is a nullary result.

bool cvc5_synth_result_has_solution(const Cvc5SynthResult result)

Determine if the given result is from a synthesis query that has a solution.

Parameters:

result – The result.

Returns:

True if the synthesis query has a solution.

bool cvc5_synth_result_has_no_solution(const Cvc5SynthResult result)

Determine if the given result is from a synthesis query that has no solution.

Parameters:

result – The result.

Returns:

True if the synthesis query has no solution. In this case, it was determined that there was no solution.

bool cvc5_synth_result_is_unknown(const Cvc5SynthResult result)

Determine if the given result is from a synthesis query where its result could not be determined.

Parameters:

result – The result.

Returns:

True if the result of the synthesis query could not be determined.

bool cvc5_synth_result_is_equal(const Cvc5SynthResult a, const Cvc5SynthResult b)

Determine equality of two synthesis results.

Parameters:

• a – The first synthesis result to compare to for equality.

• b – The second synthesis result to compare to for equality.

Returns:

True if the synthesis results are equal.

bool cvc5_synth_result_is_disequal(const Cvc5SynthResult a, const Cvc5SynthResult b)

Operator overloading for disequality of two synthesis results.

Parameters:

• a – The first synthesis result to compare to for disequality.

• b – The second synthesis result to compare to for disequality.

Returns:

True if the synthesis results are disequal.

const char *cvc5_synth_result_to_string(const Cvc5SynthResult 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:

A string representation of the given synthesis result.

size_t cvc5_synth_result_hash(Cvc5SynthResult result)

Compute the hash value of a synthesis result.

Parameters:

result – The synthesis result.

Returns:

The hash value of the synthesis result.

Cvc5SynthResult cvc5_synth_result_copy(Cvc5SynthResult result)

Make copy of synthesis 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 synthesis result to copy.

Returns:

The same result with its reference count increased by one.

void cvc5_synth_result_release(Cvc5SynthResult result)

Release copy of synthesis 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.