Package io.github.cvc5.modes

Enum FindSynthTarget

  • All Implemented Interfaces:
    java.io.Serializable, java.lang.Comparable<FindSynthTarget>
    public enum FindSynthTarget
extends java.lang.Enum<FindSynthTarget>

    • Enum Constant Summary

      Enum Constants 
      Enum Constant Description
      ENUM
      Find the next term in the enumeration of the target grammar.
      QUERY
      Find a query over the given grammar.
      REWRITE
      Find a pair of terms (t,s) in the target grammar which are equivalent but do not rewrite to the same term in the given rewriter (--sygus-rewrite=MODE).
      REWRITE_INPUT
      Find a rewrite between pairs of terms (t,s) that are matchable with terms in the input assertions where t and s are equivalent but do not rewrite to the same term in the given rewriter (--sygus-rewrite=MODE).
      REWRITE_UNSOUND
      Find a term t in the target grammar which rewrites to a term s that is not equivalent to it.

    • Method Summary

      All Methods Static Methods Instance Methods Concrete Methods 
      Modifier and Type Method Description
      static FindSynthTarget fromInt​(int value)  
      int getValue()  
      static FindSynthTarget valueOf​(java.lang.String name)
      Returns the enum constant of this type with the specified name.
      static FindSynthTarget[] values()
      Returns an array containing the constants of this enum type, in the order they are declared.

      • Methods inherited from class java.lang.Enum

        clone, compareTo, equals, finalize, getDeclaringClass, hashCode, name, ordinal, toString, valueOf

      • Methods inherited from class java.lang.Object

        getClass, notify, notifyAll, wait, wait, wait

    • Enum Constant Detail

      • ENUM

        public static final FindSynthTarget ENUM
        Find the next term in the enumeration of the target grammar.

      • REWRITE

        public static final FindSynthTarget REWRITE
        Find a pair of terms (t,s) in the target grammar which are equivalent but do not rewrite to the same term in the given rewriter (--sygus-rewrite=MODE). If so, the equality (= t s) is returned by findSynth. This can be used to synthesize rewrite rules. Note if the rewriter is set to none (--sygus-rewrite=none), this indicates a possible rewrite when implementing a rewriter from scratch.

      • REWRITE_UNSOUND

        public static final FindSynthTarget REWRITE_UNSOUND
        Find a term t in the target grammar which rewrites to a term s that is not equivalent to it. If so, the equality (= t s) is returned by findSynth. This can be used to test the correctness of the given rewriter. Any returned rewrite indicates an unsoundness in the given rewriter.

      • REWRITE_INPUT

        public static final FindSynthTarget REWRITE_INPUT
        Find a rewrite between pairs of terms (t,s) that are matchable with terms in the input assertions where t and s are equivalent but do not rewrite to the same term in the given rewriter (--sygus-rewrite=MODE). This can be used to synthesize rewrite rules that apply to the current problem.

      • QUERY

        public static final FindSynthTarget QUERY
        Find a query over the given grammar. If the given grammar generates terms that are not Boolean, we consider equalities over terms from the given grammar. The algorithm for determining which queries to generate is configured by --sygus-query-gen=MODE. Queries that are internally solved can be filtered by the option --sygus-query-gen-filter-solved.

    • Method Detail

      • values

        public static FindSynthTarget[] values()
        Returns an array containing the constants of this enum type, in the order they are declared. This method may be used to iterate over the constants as follows: 
        for (FindSynthTarget c : FindSynthTarget.values())
    System.out.println(c);
        Returns:
        an array containing the constants of this enum type, in the order they are declared

      • valueOf

        public static FindSynthTarget valueOf​(java.lang.String name)
        Returns the enum constant of this type with the specified name. The string must match exactly an identifier used to declare an enum constant in this type. (Extraneous whitespace characters are not permitted.)
        Parameters:
        name - the name of the enum constant to be returned.
        Returns:
        the enum constant with the specified name
        Throws:
        java.lang.IllegalArgumentException - if this enum type has no constant with the specified name
        java.lang.NullPointerException - if the argument is null

      • getValue

        public int getValue()