Class 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 Description
      protected long pointer  
    • Constructor Summary

      Constructors 
      Constructor Description
      Grammar​(Grammar grammar)  
    • Method Summary

      All Methods Instance Methods Concrete Methods 
      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​(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)  
      long getPointer()  
      java.lang.String toString()  
      protected java.lang.String toString​(long pointer)  
      • Methods inherited from class java.lang.Object

        clone, equals, finalize, getClass, hashCode, 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)
      • 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.
      • getPointer

        public long getPointer()
      • deletePointer

        public void deletePointer()
      • toString

        public java.lang.String toString()
        Overrides:
        toString in class java.lang.Object