Package io.github.cvc5

Class Grammar

java.lang.Object
io.github.cvc5.Grammar
public class Grammar extends 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
    Description
    protected long
    pointer
    The raw native pointer value.

  • Constructor Summary

    Constructors
    Constructor
    Description
    Grammar(Grammar grammar)
    Constructs a new Grammar instance by creating a deep copy of the specified Grammar.

  • Method Summary

    Modifier and Type
    Method
    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(Term ntSymbol, Term[] rules)
    Add rules to the set of rules corresponding to ntSymbol.
    void
    deletePointer()
    Free the native resource associated with this pointer.
    boolean
    equals(Object g)
    Referential equality operator.
    long
    getPointer()
    Return the raw native pointer.
    int
    hashCode()
    Get the hash value of a grammar.
    boolean
    isNull()
    Determine if this is the null grammar.
    String
    toString()
    Return a string representation of the pointer.
    protected String
    toString(long pointer)
    Return a string representation of the specified native pointer.

    Methods inherited from class java.lang.Object

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

  • Field Details

    • pointer

      protected long pointer
      The raw native pointer value.

  • Constructor Details

    • Grammar

      public Grammar(Grammar grammar)
      Constructs a new Grammar instance by creating a deep copy of the specified Grammar.
      Parameters:
      grammar - The Grammar instance to copy.

  • Method Details

    • isNull

      public boolean isNull()
      Determine if this is the null grammar.
      Returns:
      True if this Grammar is the null grammar.

    • equals

      public boolean equals(Object g)
      Referential equality operator.
      Overrides:
      equals in class 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.

    • 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 String toString(long pointer)
      Return a string representation of the specified native pointer.

      Subclasses must implement this method to convert the native pointer into a meaningful string.

      Parameters:
      pointer - the native pointer
      Returns:
      A String representation of this grammar.

    • hashCode

      public int hashCode()
      Get the hash value of a grammar.
      Overrides:
      hashCode in class Object
      Returns:
      The hash value.

    • getPointer

      public long getPointer()
      Return the raw native pointer.

      Every native call obtains the pointers of the objects it uses through this method, so that using an object after its native resource has been released raises an exception instead of crashing the JVM.

      Returns:
      the pointer value
      Throws:
      IllegalStateException - if the native resource of this object has been released, e.g., via deletePointer()

    • deletePointer

      public void deletePointer()
      Free the native resource associated with this pointer.

      Native resources are freed automatically once the Java object is no longer reachable. This method frees the native resource immediately instead; afterwards, using the object raises an IllegalStateException. It must be called from the thread that is using the associated term manager. Calling it more than once has no further effect.

    • toString

      public String toString()
      Return a string representation of the pointer.
      Overrides:
      toString in class Object
      Returns:
      a string representation of the pointer