Grammar 

class cvc5 :: Grammar 

A Sygus Grammar . This class 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.

Public Functions

void addRule ( const Term & ntSymbol , const Term & rule ) 

Add rule to the set of rules corresponding to ntSymbol .

Parameters

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

• rule – The rule to add.

void addRules ( const Term & ntSymbol , const std :: vector < Term > & rules ) 

Add rules to the set of rules corresponding to ntSymbol .

Parameters

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

• rules – The rules to add.

void addAnyConstant ( const Term & ntSymbol ) 

Allow ntSymbol to be an arbitrary constant.

Parameters

ntSymbol – The non-terminal allowed to be any constant.

void addAnyVariable ( const Term & ntSymbol ) 

Allow ntSymbol to be any input variable to corresponding synth-fun/synth-inv with the same sort as ntSymbol .

Parameters

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

std :: string toString ( ) const 

Returns

A string representation of this grammar.

Grammar ( ) 

Nullary constructor. Needed for the Cython API.

Friends

friend class cvc5::Command