io.github.cvc5.modes

Enum LearnedLitType

java.lang.Object

java.lang.Enum<LearnedLitType>

io.github.cvc5.modes.LearnedLitType

All Implemented Interfaces:

Serializable, Comparable<LearnedLitType>

public enum LearnedLitType
extends Enum<LearnedLitType>

Enum Constant Summary

Enum Constants

Enum Constant and 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

Modifier and Type	Method and Description
static LearnedLitType	fromInt(int value)
int	getValue()
static LearnedLitType	valueOf(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(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:

IllegalArgumentException - if this enum type has no constant with the specified name

NullPointerException - if the argument is null

fromInt

public static LearnedLitType fromInt(int value)
                              throws CVC5ApiException

Throws:

CVC5ApiException

getValue

public int getValue()