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

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.

~Grammar()

Destructor for bookeeping.

Friends

friend class parser::Cmd

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

Serialize a grammar to given stream.

Parameters:

• out – The output stream.

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

Returns:

The output stream.