Package io.github.cvc5.modes

Enum Class FindSynthTarget

java.lang.Object
java.lang.Enum<FindSynthTarget>
io.github.cvc5.modes.FindSynthTarget
All Implemented Interfaces:
Serializable, Comparable<FindSynthTarget>, Constable
public enum FindSynthTarget extends Enum<FindSynthTarget>
Enum representing the set of possible values for FindSynthTarget.

  • Nested Class Summary

    Nested classes/interfaces inherited from class java.lang.Enum

    Enum.EnumDesc<E extends Enum<E>>

  • 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

    Modifier and Type
    Method
    Description
    static FindSynthTarget
    fromInt(int value)
    Converts an integer value to the corresponding enum constant.
    int
    getValue()
    Get the integer value associated with this enum constant.
    static FindSynthTarget
    valueOf(String name)
    Returns the enum constant of this class with the specified name.
    static FindSynthTarget[]
    values()
    Returns an array containing the constants of this enum class, in the order they are declared.

    Methods inherited from class java.lang.Enum

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

    Methods inherited from class java.lang.Object

    getClass, notify, notifyAll, wait, wait, wait

  • Enum Constant Details

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

    • values

      public static FindSynthTarget[] values()
      Returns an array containing the constants of this enum class, in the order they are declared.
      Returns:
      an array containing the constants of this enum class, in the order they are declared

    • valueOf

      public static FindSynthTarget valueOf(String name)
      Returns the enum constant of this class with the specified name. The string must match exactly an identifier used to declare an enum constant in this class. (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:
      IllegalArgumentException - if this enum class has no constant with the specified name
      NullPointerException - if the argument is null

    • fromInt

      public static FindSynthTarget fromInt(int value) throws CVC5ApiException
      Converts an integer value to the corresponding enum constant.
      Parameters:
      value - the integer representation of the enum constant.
      Returns:
      the corresponding enum constant for the given integer value.
      Throws:
      CVC5ApiException - if the value is outside the valid range, or if no corresponding enum constant exists.

    • getValue

      public int getValue()
      Get the integer value associated with this enum constant.
      Returns:
      the integer representation of the enum constant.