Package io.github.cvc5.modes

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

      All Methods Static Methods Instance Methods Concrete Methods 
      Modifier and Type Method 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

      • getValue

        public int getValue()