Enum Cvc5ProofRule

Source

#[repr(u32)]pub enum Cvc5ProofRule {
Show 158 variants    CVC5_PROOF_RULE_ASSUME = 0,
    CVC5_PROOF_RULE_SCOPE = 1,
    CVC5_PROOF_RULE_SUBS = 2,
    CVC5_PROOF_RULE_MACRO_REWRITE = 3,
    CVC5_PROOF_RULE_EVALUATE = 4,
    CVC5_PROOF_RULE_DISTINCT_VALUES = 5,
    CVC5_PROOF_RULE_ACI_NORM = 6,
    CVC5_PROOF_RULE_ABSORB = 7,
    CVC5_PROOF_RULE_MACRO_SR_EQ_INTRO = 8,
    CVC5_PROOF_RULE_MACRO_SR_PRED_INTRO = 9,
    CVC5_PROOF_RULE_MACRO_SR_PRED_ELIM = 10,
    CVC5_PROOF_RULE_MACRO_SR_PRED_TRANSFORM = 11,
    CVC5_PROOF_RULE_ENCODE_EQ_INTRO = 12,
    CVC5_PROOF_RULE_DSL_REWRITE = 13,
    CVC5_PROOF_RULE_THEORY_REWRITE = 14,
    CVC5_PROOF_RULE_ITE_EQ = 15,
    CVC5_PROOF_RULE_TRUST = 16,
    CVC5_PROOF_RULE_TRUST_THEORY_REWRITE = 17,
    CVC5_PROOF_RULE_SAT_REFUTATION = 18,
    CVC5_PROOF_RULE_DRAT_REFUTATION = 19,
    CVC5_PROOF_RULE_SAT_EXTERNAL_PROVE = 20,
    CVC5_PROOF_RULE_RESOLUTION = 21,
    CVC5_PROOF_RULE_CHAIN_RESOLUTION = 22,
    CVC5_PROOF_RULE_FACTORING = 23,
    CVC5_PROOF_RULE_REORDERING = 24,
    CVC5_PROOF_RULE_MACRO_RESOLUTION = 25,
    CVC5_PROOF_RULE_MACRO_RESOLUTION_TRUST = 26,
    CVC5_PROOF_RULE_CHAIN_M_RESOLUTION = 27,
    CVC5_PROOF_RULE_SPLIT = 28,
    CVC5_PROOF_RULE_EQ_RESOLVE = 29,
    CVC5_PROOF_RULE_MODUS_PONENS = 30,
    CVC5_PROOF_RULE_NOT_NOT_ELIM = 31,
    CVC5_PROOF_RULE_CONTRA = 32,
    CVC5_PROOF_RULE_AND_ELIM = 33,
    CVC5_PROOF_RULE_AND_INTRO = 34,
    CVC5_PROOF_RULE_NOT_OR_ELIM = 35,
    CVC5_PROOF_RULE_IMPLIES_ELIM = 36,
    CVC5_PROOF_RULE_NOT_IMPLIES_ELIM1 = 37,
    CVC5_PROOF_RULE_NOT_IMPLIES_ELIM2 = 38,
    CVC5_PROOF_RULE_EQUIV_ELIM1 = 39,
    CVC5_PROOF_RULE_EQUIV_ELIM2 = 40,
    CVC5_PROOF_RULE_NOT_EQUIV_ELIM1 = 41,
    CVC5_PROOF_RULE_NOT_EQUIV_ELIM2 = 42,
    CVC5_PROOF_RULE_XOR_ELIM1 = 43,
    CVC5_PROOF_RULE_XOR_ELIM2 = 44,
    CVC5_PROOF_RULE_NOT_XOR_ELIM1 = 45,
    CVC5_PROOF_RULE_NOT_XOR_ELIM2 = 46,
    CVC5_PROOF_RULE_ITE_ELIM1 = 47,
    CVC5_PROOF_RULE_ITE_ELIM2 = 48,
    CVC5_PROOF_RULE_NOT_ITE_ELIM1 = 49,
    CVC5_PROOF_RULE_NOT_ITE_ELIM2 = 50,
    CVC5_PROOF_RULE_NOT_AND = 51,
    CVC5_PROOF_RULE_CNF_AND_POS = 52,
    CVC5_PROOF_RULE_CNF_AND_NEG = 53,
    CVC5_PROOF_RULE_CNF_OR_POS = 54,
    CVC5_PROOF_RULE_CNF_OR_NEG = 55,
    CVC5_PROOF_RULE_CNF_IMPLIES_POS = 56,
    CVC5_PROOF_RULE_CNF_IMPLIES_NEG1 = 57,
    CVC5_PROOF_RULE_CNF_IMPLIES_NEG2 = 58,
    CVC5_PROOF_RULE_CNF_EQUIV_POS1 = 59,
    CVC5_PROOF_RULE_CNF_EQUIV_POS2 = 60,
    CVC5_PROOF_RULE_CNF_EQUIV_NEG1 = 61,
    CVC5_PROOF_RULE_CNF_EQUIV_NEG2 = 62,
    CVC5_PROOF_RULE_CNF_XOR_POS1 = 63,
    CVC5_PROOF_RULE_CNF_XOR_POS2 = 64,
    CVC5_PROOF_RULE_CNF_XOR_NEG1 = 65,
    CVC5_PROOF_RULE_CNF_XOR_NEG2 = 66,
    CVC5_PROOF_RULE_CNF_ITE_POS1 = 67,
    CVC5_PROOF_RULE_CNF_ITE_POS2 = 68,
    CVC5_PROOF_RULE_CNF_ITE_POS3 = 69,
    CVC5_PROOF_RULE_CNF_ITE_NEG1 = 70,
    CVC5_PROOF_RULE_CNF_ITE_NEG2 = 71,
    CVC5_PROOF_RULE_CNF_ITE_NEG3 = 72,
    CVC5_PROOF_RULE_REFL = 73,
    CVC5_PROOF_RULE_SYMM = 74,
    CVC5_PROOF_RULE_TRANS = 75,
    CVC5_PROOF_RULE_CONG = 76,
    CVC5_PROOF_RULE_NARY_CONG = 77,
    CVC5_PROOF_RULE_TRUE_INTRO = 78,
    CVC5_PROOF_RULE_TRUE_ELIM = 79,
    CVC5_PROOF_RULE_FALSE_INTRO = 80,
    CVC5_PROOF_RULE_FALSE_ELIM = 81,
    CVC5_PROOF_RULE_HO_APP_ENCODE = 82,
    CVC5_PROOF_RULE_HO_CONG = 83,
    CVC5_PROOF_RULE_ARRAYS_READ_OVER_WRITE = 84,
    CVC5_PROOF_RULE_ARRAYS_READ_OVER_WRITE_CONTRA = 85,
    CVC5_PROOF_RULE_ARRAYS_READ_OVER_WRITE_1 = 86,
    CVC5_PROOF_RULE_ARRAYS_EXT = 87,
    CVC5_PROOF_RULE_MACRO_BV_BITBLAST = 88,
    CVC5_PROOF_RULE_BV_BITBLAST_STEP = 89,
    CVC5_PROOF_RULE_BV_EAGER_ATOM = 90,
    CVC5_PROOF_RULE_BV_POLY_NORM = 91,
    CVC5_PROOF_RULE_BV_POLY_NORM_EQ = 92,
    CVC5_PROOF_RULE_DT_SPLIT = 93,
    CVC5_PROOF_RULE_SKOLEM_INTRO = 94,
    CVC5_PROOF_RULE_SKOLEMIZE = 95,
    CVC5_PROOF_RULE_INSTANTIATE = 96,
    CVC5_PROOF_RULE_ALPHA_EQUIV = 97,
    CVC5_PROOF_RULE_QUANT_VAR_REORDERING = 98,
    CVC5_PROOF_RULE_EXISTS_STRING_LENGTH = 99,
    CVC5_PROOF_RULE_SETS_SINGLETON_INJ = 100,
    CVC5_PROOF_RULE_SETS_EXT = 101,
    CVC5_PROOF_RULE_SETS_FILTER_UP = 102,
    CVC5_PROOF_RULE_SETS_FILTER_DOWN = 103,
    CVC5_PROOF_RULE_CONCAT_EQ = 104,
    CVC5_PROOF_RULE_CONCAT_UNIFY = 105,
    CVC5_PROOF_RULE_CONCAT_SPLIT = 106,
    CVC5_PROOF_RULE_CONCAT_CSPLIT = 107,
    CVC5_PROOF_RULE_CONCAT_LPROP = 108,
    CVC5_PROOF_RULE_CONCAT_CPROP = 109,
    CVC5_PROOF_RULE_STRING_DECOMPOSE = 110,
    CVC5_PROOF_RULE_STRING_LENGTH_POS = 111,
    CVC5_PROOF_RULE_STRING_LENGTH_NON_EMPTY = 112,
    CVC5_PROOF_RULE_STRING_REDUCTION = 113,
    CVC5_PROOF_RULE_STRING_EAGER_REDUCTION = 114,
    CVC5_PROOF_RULE_RE_INTER = 115,
    CVC5_PROOF_RULE_RE_CONCAT = 116,
    CVC5_PROOF_RULE_RE_UNFOLD_POS = 117,
    CVC5_PROOF_RULE_RE_UNFOLD_NEG = 118,
    CVC5_PROOF_RULE_RE_UNFOLD_NEG_CONCAT_FIXED = 119,
    CVC5_PROOF_RULE_STRING_CODE_INJ = 120,
    CVC5_PROOF_RULE_STRING_SEQ_UNIT_INJ = 121,
    CVC5_PROOF_RULE_STRING_EXT = 122,
    CVC5_PROOF_RULE_MACRO_STRING_INFERENCE = 123,
    CVC5_PROOF_RULE_MACRO_ARITH_SCALE_SUM_UB = 124,
    CVC5_PROOF_RULE_ARITH_MULT_ABS_COMPARISON = 125,
    CVC5_PROOF_RULE_ARITH_SUM_UB = 126,
    CVC5_PROOF_RULE_INT_TIGHT_UB = 127,
    CVC5_PROOF_RULE_INT_TIGHT_LB = 128,
    CVC5_PROOF_RULE_ARITH_TRICHOTOMY = 129,
    CVC5_PROOF_RULE_ARITH_REDUCTION = 130,
    CVC5_PROOF_RULE_ARITH_POLY_NORM = 131,
    CVC5_PROOF_RULE_ARITH_POLY_NORM_REL = 132,
    CVC5_PROOF_RULE_ARITH_MULT_SIGN = 133,
    CVC5_PROOF_RULE_ARITH_MULT_POS = 134,
    CVC5_PROOF_RULE_ARITH_MULT_NEG = 135,
    CVC5_PROOF_RULE_ARITH_MULT_TANGENT = 136,
    CVC5_PROOF_RULE_ARITH_TRANS_PI = 137,
    CVC5_PROOF_RULE_ARITH_TRANS_EXP_NEG = 138,
    CVC5_PROOF_RULE_ARITH_TRANS_EXP_POSITIVITY = 139,
    CVC5_PROOF_RULE_ARITH_TRANS_EXP_SUPER_LIN = 140,
    CVC5_PROOF_RULE_ARITH_TRANS_EXP_ZERO = 141,
    CVC5_PROOF_RULE_ARITH_TRANS_EXP_APPROX_ABOVE_NEG = 142,
    CVC5_PROOF_RULE_ARITH_TRANS_EXP_APPROX_ABOVE_POS = 143,
    CVC5_PROOF_RULE_ARITH_TRANS_EXP_APPROX_BELOW = 144,
    CVC5_PROOF_RULE_ARITH_TRANS_SINE_BOUNDS = 145,
    CVC5_PROOF_RULE_ARITH_TRANS_SINE_SHIFT = 146,
    CVC5_PROOF_RULE_ARITH_TRANS_SINE_SYMMETRY = 147,
    CVC5_PROOF_RULE_ARITH_TRANS_SINE_TANGENT_ZERO = 148,
    CVC5_PROOF_RULE_ARITH_TRANS_SINE_TANGENT_PI = 149,
    CVC5_PROOF_RULE_ARITH_TRANS_SINE_APPROX_ABOVE_NEG = 150,
    CVC5_PROOF_RULE_ARITH_TRANS_SINE_APPROX_ABOVE_POS = 151,
    CVC5_PROOF_RULE_ARITH_TRANS_SINE_APPROX_BELOW_NEG = 152,
    CVC5_PROOF_RULE_ARITH_TRANS_SINE_APPROX_BELOW_POS = 153,
    CVC5_PROOF_RULE_LFSC_RULE = 154,
    CVC5_PROOF_RULE_ALETHE_RULE = 155,
    CVC5_PROOF_RULE_UNKNOWN = 156,
    CVC5_PROOF_RULE_LAST = 157,
}