io.github.cvc5

Class Grammar

java.lang.Object

io.github.cvc5.Grammar

public class Grammar
extends java.lang.Object

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.

Field Summary

Fields

Modifier and Type	Field and Description
protected long	pointer

Constructor Summary

Constructors

Constructor and Description
Grammar(Grammar grammar)

Method Summary

Modifier and Type	Method and Description
void	addAnyConstant(Term ntSymbol) Allow ntSymbol to be an arbitrary constant.
void	addAnyVariable(Term ntSymbol) Allow ntSymbol to be any input variable to corresponding synth-fun or synth-inv with the same sort as ntSymbol.
void	addRule(Term ntSymbol, Term rule) Add rule to the set of rules corresponding to ntSymbol.
void	addRules(long pointer, long ntSymbolPointer, long[] rulePointers)
void	addRules(Term ntSymbol, Term[] rules) Add rules to the set of rules corresponding to ntSymbol.
void	deletePointer()
protected void	deletePointer(long pointer)
boolean	equals(java.lang.Object g) Referential equality operator.
long	getPointer()
int	hashCode() Get the hash value of a grammar.
boolean	isNull() Determine if this is the null grammar.
java.lang.String	toString()
protected java.lang.String	toString(long pointer)

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

pointer

protected long pointer

Constructor Detail

Grammar

public Grammar(Grammar grammar)

Method Detail

deletePointer

protected void deletePointer(long pointer)

isNull

public boolean isNull()

Determine if this is the null grammar.

Returns:

True if this Grammar is the null grammar.

equals

public boolean equals(java.lang.Object g)

Referential equality operator.

Overrides:

equals in class java.lang.Object

Parameters:

g - The grammar to compare to for equality.

Returns:

True if the gramamrs point to the same internal grammar object.

addRule

public void addRule(Term ntSymbol,
                    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.

addRules

public void addRules(Term ntSymbol,
                     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.

addRules

public void addRules(long pointer,
                     long ntSymbolPointer,
                     long[] rulePointers)

addAnyConstant

public void addAnyConstant(Term ntSymbol)

Allow ntSymbol to be an arbitrary constant.

Parameters:

ntSymbol - the non-terminal allowed to be any constant.

addAnyVariable

public void addAnyVariable(Term ntSymbol)

Allow ntSymbol to be any input variable to corresponding synth-fun or synth-inv with the same sort as ntSymbol.

Parameters:

ntSymbol - the non-terminal allowed to be any input constant.

toString

protected java.lang.String toString(long pointer)

Returns:

A String representation of this grammar.

hashCode

public int hashCode()

Get the hash value of a grammar.

Overrides:

hashCode in class java.lang.Object

Returns:

The hash value.

getPointer

public long getPointer()

deletePointer

public void deletePointer()

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object