Grammar

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


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.

isNull ( )