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.