Package io.github.cvc5

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  
      protected Solver solver  

    • 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.
      protected void deletePointer​(long pointer)  
      long getPointer()  
      Solver getSolver()  
      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

      • solver

        protected final Solver solver

      • pointer

        protected long pointer

    • Constructor Detail

      • Grammar

        public Grammar​(Grammar grammar)

    • Method Detail

      • deletePointer

        protected void deletePointer​(long pointer)

      • getPointer

        public long getPointer()

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

      • getSolver

        public Solver getSolver()

      • toString

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