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.