Cvc5Grammar

This struct encapsulates a SyGuS grammar. It is created via cvc5_mk_grammar() and allows to define a context-free grammar of terms, according to the definition of grammars in the SyGuS IF 2.1 standard.

typedef struct cvc5_grammar_t *Cvc5Grammar

A Sygus Grammar. This can be used to define a context-free grammar of terms. Its interface coincides with the definition of grammars (GrammarDef) in the SyGuS IF 2.1 standard.

void cvc5_grammar_add_rule(Cvc5Grammar grammar, Cvc5Term symbol, Cvc5Term rule)

Add rule to the set of rules corresponding to symbol of a given grammar.

Parameters:

  • grammar – The grammar.

  • symbol – The non-terminal to which the rule is added.

  • rule – The rule to add.

void cvc5_grammar_add_rules(Cvc5Grammar grammar, Cvc5Term symbol, size_t size, const Cvc5Term rules[])

Add rules to the set of rules corresponding to symbol of a given grammar.

Parameters:

  • grammar – The grammar.

  • symbol – The non-terminal to which the rules are added.

  • size – The number of rules to add.

  • rules – The rules to add.

void cvc5_grammar_add_any_constant(Cvc5Grammar grammar, Cvc5Term symbol)

Allow symbol to be an arbitrary constant of a given grammar.

Parameters:

  • grammar – The grammar.

  • symbol – The non-terminal allowed to be any constant.

void cvc5_grammar_add_any_variable(Cvc5Grammar grammar, Cvc5Term symbol)

Allow symbol to be any input variable of a given grammar to corresponding synth-fun/synth-inv with the same sort as symbol.

Parameters:

  • grammar – The grammar.

  • symbol – The non-terminal allowed to be any input variable.

const char *cvc5_grammar_to_string(const Cvc5Grammar grammar)

Get a string representation of a given grammar.

Note

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

Parameters:

grammar – The grammar.

Returns:

A string representation of the grammar.

bool cvc5_grammar_is_equal(Cvc5Grammar a, Cvc5Grammar b)

Compare two grammars for referential equality.

Parameters:

  • a – The first grammar.

  • b – The second grammar.

Returns:

True if both grammar pointers point to the same internal grammar object.

bool cvc5_grammar_is_disequal(Cvc5Grammar a, Cvc5Grammar b)

Compare two grammars for referential disequality.

Parameters:

  • a – The first grammar.

  • b – The second grammar.

Returns:

True if both grammar pointers point to different internal grammar objects.

size_t cvc5_grammar_hash(Cvc5Grammar grammar)

Compute the hash value of a grammar.

Parameters:

grammar – The grammar.

Returns:

The hash value of the grammar.

Cvc5Grammar cvc5_grammar_copy(Cvc5Grammar grammar)

Make copy of grammar, increases reference counter of grammar.

Note

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

Parameters:

grammar – The grammar to copy.

Returns:

The same grammar with its reference count increased by one.

void cvc5_grammar_release(Cvc5Grammar grammar)

Release copy of grammar, decrements reference counter of grammar.

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:

grammar – The grammar to release.