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 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.