Package io.github.cvc5.modes

Enum LearnedLitType

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

    • Enum Constant Summary

      Enum Constants 
      Enum Constant Description
      CONSTANT_PROP
      An internal literal that can be made into a constant propagation for an input term.
      INPUT
      A literal from the preprocessed set of input formulas that does not occur at top-level after preprocessing.
      INTERNAL
      Any internal literal that does not fall into the above categories.
      PREPROCESS
      A top-level literal (unit clause) from the preprocessed set of input formulas.
      PREPROCESS_SOLVED
      An equality that was turned into a substitution during preprocessing.
      SOLVABLE
      An internal literal that is solvable for an input variable.
      UNKNOWN
      Special case for when produce-learned-literals is not set.

    • Method Summary

      All Methods Static Methods Instance Methods Concrete Methods 
      Modifier and Type Method Description
      static LearnedLitType fromInt​(int value)  
      int getValue()  
      static LearnedLitType valueOf​(java.lang.String name)
      Returns the enum constant of this type with the specified name.
      static LearnedLitType[] 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

      • PREPROCESS_SOLVED

        public static final LearnedLitType PREPROCESS_SOLVED
        An equality that was turned into a substitution during preprocessing. In particular, literals in this category are of the form (= x t) where x does not occur in t.

      • PREPROCESS

        public static final LearnedLitType PREPROCESS
        A top-level literal (unit clause) from the preprocessed set of input formulas.

      • INPUT

        public static final LearnedLitType INPUT
        A literal from the preprocessed set of input formulas that does not occur at top-level after preprocessing. Typically), this is the most interesting category of literals to learn.

      • SOLVABLE

        public static final LearnedLitType SOLVABLE
        An internal literal that is solvable for an input variable. In particular, literals in this category are of the form (= x t) where x does not occur in t, the preprocessed set of input formulas contains the term x, but not the literal (= x t). Note that solvable literals can be turned into substitutions during preprocessing.

      • CONSTANT_PROP

        public static final LearnedLitType CONSTANT_PROP
        An internal literal that can be made into a constant propagation for an input term. In particular, literals in this category are of the form (= t c) where c is a constant, the preprocessed set of input formulas contains the term t, but not the literal (= t c).

      • INTERNAL

        public static final LearnedLitType INTERNAL
        Any internal literal that does not fall into the above categories.

      • UNKNOWN

        public static final LearnedLitType UNKNOWN
        Special case for when produce-learned-literals is not set.

    • Method Detail

      • values

        public static LearnedLitType[] 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 (LearnedLitType c : LearnedLitType.values())
    System.out.println(c);
        Returns:
        an array containing the constants of this enum type, in the order they are declared

      • valueOf

        public static LearnedLitType 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()