Package io.github.cvc5.modes

Enum Class ProofComponent

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

  • Enum Constant Details

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

    • values

      public static ProofComponent[] 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 ProofComponent 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 ProofComponent 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.