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

• std::ostream& cvc5::operator<< (std::ostream& out, const Grammar& g)

class 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

Grammar ( ) 

Nullary constructor. Needed for the Cython API.

~Grammar ( ) 

Destructor for bookeeping.

bool isNull ( ) const 

Determine if this is the null grammar ( Grammar::Grammar() ).

Returns :

True if this grammar is the null grammar.

bool operator == ( const Grammar & grammar ) const 

Operator overloading for referential equality of two grammars.

Parameters :

grammar – The grammarto compare to for equality.

Returns :

True if both grammars point to the same internal grammar object.

bool operator != ( const Grammar & grammar ) const 

Referential disequality operator.

Parameters :

grammar – The grammar to compare to for disequality.

Returns :

True if both grammars point to different internal grammar objects.

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.

Friends

friend class parser::Cmd

friend struct std::hash< Grammar >

std :: ostream & cvc5 :: operator << ( std :: ostream & out , const Grammar & grammar ) 

Serialize a grammar to given stream.

Parameters :

• out – The output stream.

• grammar – The grammar to be serialized to the given output stream.

Returns :

The output stream.