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 asntSymbol
.- Parameters :
-
ntSymbol – The non-terminal allowed to be any input variable.
- addRule ( )
-
Add
rule
to the set of rules corresponding tontSymbol
.- 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 tontSymbol
.- Parameters :
-
-
ntSymbol – The non-terminal to which the rules are added.
-
rules – The rules to add.
-
- isNull ( )