io.github.cvc5.modes

Enum ProofComponent

java.lang.Object

java.lang.Enum<ProofComponent>

io.github.cvc5.modes.ProofComponent

All Implemented Interfaces:

java.io.Serializable, java.lang.Comparable<ProofComponent>

public enum ProofComponent
extends java.lang.Enum<ProofComponent>

Enum Constant Summary

Enum Constants

Enum Constant and Description
FULL A proof of false whose free assumptions are a subset of the input formulas F1), ...
PREPROCESS Proofs of Gu1 ...
RAW_PREPROCESS Proofs of G1 ...
SAT A proof of false whose free assumptions are Gu1, ...
THEORY_LEMMAS Proofs of L1 ...

Method Summary

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

RAW_PREPROCESS

public static final ProofComponent RAW_PREPROCESS

Proofs of G1 ... Gn whose free assumptions are a subset of F1, ... Fm, where:

• G1, ... Gn are the preprocessed input formulas,
• F1, ... Fm are the input formulas.

Note that G1 ... Gn may be arbitrary formulas, not necessarily clauses.

PREPROCESS

public static final ProofComponent PREPROCESS

Proofs of Gu1 ... Gun whose free assumptions are Fu1, ... Fum, where:

• Gu1, ... Gun are clauses corresponding to input formulas used in the SAT

proof,

• Fu1, ... Fum is the subset of the input formulas that are used in the SAT

proof (i.e. the unsat core). Note that Gu1 ... Gun are clauses that are added to the SAT solver before its main search. Only valid immediately after an unsat response.

SAT

public static final ProofComponent SAT

A proof of false whose free assumptions are Gu1, ... Gun, L1 ... Lk, where:

• Gu1, ... Gun, is a set of clauses corresponding to input formulas,
• L1, ..., Lk is a set of clauses corresponding to theory lemmas.

Only valid immediately after an unsat response.

THEORY_LEMMAS

public static final ProofComponent THEORY_LEMMAS

Proofs of L1 ... Lk where:

• L1, ..., Lk are clauses corresponding to theory lemmas used in the SAT

proof. In contrast to proofs given for preprocess, L1 ... Lk are clauses that are added to the SAT solver after its main search. Only valid immediately after an unsat response.

FULL

public static final ProofComponent FULL

A proof of false whose free assumptions are a subset of the input formulas F1), ... Fm. Only valid immediately after an unsat response.

Method Detail

values

public static ProofComponent[] 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 (ProofComponent c : ProofComponent.values())
    System.out.println(c);

Returns:

an array containing the constants of this enum type, in the order they are declared

valueOf

public static ProofComponent 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

fromInt

public static ProofComponent fromInt(int value)
                              throws CVC5ApiException

Throws:

CVC5ApiException

getValue

public int getValue()