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.

Wrapper class for cvc5::Grammar.

addAnyConstant()

Allow ntSymbol to be an arbitrary constant.

Parameters:

ntSymbol – The non-terminal allowed to be constant.

addAnyVariable()

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.

addRule()

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.

addRules()

Add ntSymbol to the set of rules corresponding to ntSymbol.

Parameters:

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

• rules – The rules to add.