public enum ProofRewriteRule extends Enum<ProofRewriteRule>
| Enum Constant and Description |
|---|
ARITH_ABS_ELIM
Auto-generated from RARE rule arith-abs-elim
|
ARITH_DIV_BY_CONST_ELIM
Arith – Division by constant elimination
\[
t / c = t * 1/c
\]
where \(c\) is a constant.
|
ARITH_DIV_ELIM_TO_REAL1
Auto-generated from RARE rule arith-div-elim-to-real1
|
ARITH_DIV_ELIM_TO_REAL2
Auto-generated from RARE rule arith-div-elim-to-real2
|
ARITH_DIV_TOTAL
Auto-generated from RARE rule arith-div-total
|
ARITH_ELIM_GT
Auto-generated from RARE rule arith-elim-gt
|
ARITH_ELIM_INT_GT
Auto-generated from RARE rule arith-elim-int-gt
|
ARITH_ELIM_INT_LT
Auto-generated from RARE rule arith-elim-int-lt
|
ARITH_ELIM_LEQ
Auto-generated from RARE rule arith-elim-leq
|
ARITH_ELIM_LT
Auto-generated from RARE rule arith-elim-lt
|
ARITH_ELIM_MINUS
Auto-generated from RARE rule arith-elim-minus
|
ARITH_ELIM_UMINUS
Auto-generated from RARE rule arith-elim-uminus
|
ARITH_GEQ_NORM1
Auto-generated from RARE rule arith-geq-norm1
|
ARITH_GEQ_NORM2
Auto-generated from RARE rule arith-geq-norm2
|
ARITH_GEQ_TIGHTEN
Auto-generated from RARE rule arith-geq-tighten
|
ARITH_INT_DIV_TOTAL
Auto-generated from RARE rule arith-int-div-total
|
ARITH_INT_DIV_TOTAL_ONE
Auto-generated from RARE rule arith-int-div-total-one
|
ARITH_INT_DIV_TOTAL_ZERO
Auto-generated from RARE rule arith-int-div-total-zero
|
ARITH_INT_EQ_ELIM
Auto-generated from RARE rule arith-int-eq-elim
|
ARITH_INT_MOD_TOTAL
Auto-generated from RARE rule arith-int-mod-total
|
ARITH_INT_MOD_TOTAL_ONE
Auto-generated from RARE rule arith-int-mod-total-one
|
ARITH_INT_MOD_TOTAL_ZERO
Auto-generated from RARE rule arith-int-mod-total-zero
|
ARITH_LEQ_NORM
Auto-generated from RARE rule arith-leq-norm
|
ARITH_MUL_ONE
Auto-generated from RARE rule arith-mul-one
|
ARITH_MUL_ZERO
Auto-generated from RARE rule arith-mul-zero
|
ARITH_MULT_DIST
Auto-generated from RARE rule arith-mult-dist
|
ARITH_MULT_FLATTEN
Auto-generated from RARE rule arith-mult-flatten
|
ARITH_NEG_NEG_ONE
Auto-generated from RARE rule arith-neg-neg-one
|
ARITH_PLUS_CANCEL1
Auto-generated from RARE rule arith-plus-cancel1
|
ARITH_PLUS_CANCEL2
Auto-generated from RARE rule arith-plus-cancel2
|
ARITH_PLUS_FLATTEN
Auto-generated from RARE rule arith-plus-flatten
|
ARITH_PLUS_ZERO
Auto-generated from RARE rule arith-plus-zero
|
ARITH_REAL_EQ_ELIM
Auto-generated from RARE rule arith-real-eq-elim
|
ARITH_REFL_GEQ
Auto-generated from RARE rule arith-refl-geq
|
ARITH_REFL_GT
Auto-generated from RARE rule arith-refl-gt
|
ARITH_REFL_LEQ
Auto-generated from RARE rule arith-refl-leq
|
ARITH_REFL_LT
Auto-generated from RARE rule arith-refl-lt
|
ARITH_STRING_PRED_ENTAIL
Arithmetic - strings predicate entailment
\[
(>= n 0) = true
\]
Where \(n\) can be shown to be greater than or equal to \(0\) by
reasoning about string length being positive and basic properties of
addition and multiplication.
|
ARITH_STRING_PRED_SAFE_APPROX
Arithmetic - strings predicate entailment
\[
(>= n 0) = (>= m 0)
\]
Where \(m\) is a safe under-approximation of \(n\), namely
we have that \((>= n m)\) and \((>= m 0)\).
|
ARITH_TO_INT_ELIM_TO_REAL
Auto-generated from RARE rule arith-to-int-elim-to-real
|
ARITH_TO_REAL_ELIM
Auto-generated from RARE rule arith-to-real-elim
|
ARRAY_READ_OVER_WRITE
Auto-generated from RARE rule array-read-over-write
|
ARRAY_READ_OVER_WRITE2
Auto-generated from RARE rule array-read-over-write2
|
ARRAY_STORE_OVERWRITE
Auto-generated from RARE rule array-store-overwrite
|
ARRAY_STORE_SELF
Auto-generated from RARE rule array-store-self
|
ARRAYS_EQ_RANGE_EXPAND
Arrays – Expansion of array range equality
\[
\mathit{eqrange}(a,b,i,j)=
\forall x.
|
BETA_REDUCE
Equality – Beta reduction
\[
((\lambda x_1 \ldots x_n.
|
BOOL_AND_CONF
Auto-generated from RARE rule boolean-and-conf
|
BOOL_AND_DE_MORGAN
Auto-generated from RARE rule boolean-and-de-morgan
|
BOOL_AND_DUP
Auto-generated from RARE rule boolean-and-dup
|
BOOL_AND_FALSE
Auto-generated from RARE rule boolean-and-false
|
BOOL_AND_FLATTEN
Auto-generated from RARE rule boolean-and-flatten
|
BOOL_AND_TRUE
Auto-generated from RARE rule boolean-and-true
|
BOOL_DOUBLE_NOT_ELIM
Auto-generated from RARE rule boolean-double-not-elim
|
BOOL_EQ_FALSE
Auto-generated from RARE rule boolean-eq-false
|
BOOL_EQ_NREFL
Auto-generated from RARE rule boolean-eq-nrefl
|
BOOL_EQ_TRUE
Auto-generated from RARE rule boolean-eq-true
|
BOOL_IMPL_ELIM
Auto-generated from RARE rule boolean-impl-elim
|
BOOL_IMPL_FALSE1
Auto-generated from RARE rule boolean-impl-false1
|
BOOL_IMPL_FALSE2
Auto-generated from RARE rule boolean-impl-false2
|
BOOL_IMPL_TRUE1
Auto-generated from RARE rule boolean-impl-true1
|
BOOL_IMPL_TRUE2
Auto-generated from RARE rule boolean-impl-true2
|
BOOL_IMPLIES_DE_MORGAN
Auto-generated from RARE rule boolean-implies-de-morgan
|
BOOL_NOT_EQ_ELIM
Auto-generated from RARE rule boolean-not-eq-elim
|
BOOL_NOT_FALSE
Auto-generated from RARE rule boolean-not-false
|
BOOL_NOT_ITE_ELIM
Auto-generated from RARE rule boolean-not-ite-elim
|
BOOL_NOT_TRUE
Auto-generated from RARE rule boolean-not-true
|
BOOL_NOT_XOR_ELIM
Auto-generated from RARE rule boolean-not-xor-elim
|
BOOL_OR_DE_MORGAN
Auto-generated from RARE rule boolean-or-de-morgan
|
BOOL_OR_DUP
Auto-generated from RARE rule boolean-or-dup
|
BOOL_OR_FALSE
Auto-generated from RARE rule boolean-or-false
|
BOOL_OR_FLATTEN
Auto-generated from RARE rule boolean-or-flatten
|
BOOL_OR_TAUT
Auto-generated from RARE rule boolean-or-taut
|
BOOL_OR_TRUE
Auto-generated from RARE rule boolean-or-true
|
BOOL_XOR_COMM
Auto-generated from RARE rule boolean-xor-comm
|
BOOL_XOR_ELIM
Auto-generated from RARE rule boolean-xor-elim
|
BOOL_XOR_FALSE
Auto-generated from RARE rule boolean-xor-false
|
BOOL_XOR_NREFL
Auto-generated from RARE rule boolean-xor-nrefl
|
BOOL_XOR_REFL
Auto-generated from RARE rule boolean-xor-refl
|
BOOL_XOR_TRUE
Auto-generated from RARE rule boolean-xor-true
|
BV_ADD_COMBINE_LIKE_TERMS
Bitvectors - Combine like terms during addition by counting terms
|
BV_ADD_TWO
Auto-generated from RARE rule bv-add-two
|
BV_ADD_ZERO
Auto-generated from RARE rule bv-add-zero
|
BV_AND_CONCAT_PULLUP
Auto-generated from RARE rule bv-and-concat-pullup
|
BV_AND_FLATTEN
Auto-generated from RARE rule bv-and-flatten
|
BV_AND_ONE
Auto-generated from RARE rule bv-and-one
|
BV_AND_SIMPLIFY_1
Auto-generated from RARE rule bv-and-simplify-1
|
BV_AND_SIMPLIFY_2
Auto-generated from RARE rule bv-and-simplify-2
|
BV_AND_ZERO
Auto-generated from RARE rule bv-and-zero
|
BV_ASHR_BY_CONST_0
Auto-generated from RARE rule bv-ashr-by--0
|
BV_ASHR_BY_CONST_1
Auto-generated from RARE rule bv-ashr-by--1
|
BV_ASHR_BY_CONST_2
Auto-generated from RARE rule bv-ashr-by--2
|
BV_ASHR_ZERO
Auto-generated from RARE rule bv-ashr-zero
|
BV_BITWISE_IDEMP_1
Auto-generated from RARE rule bv-bitwise-idemp-1
|
BV_BITWISE_IDEMP_2
Auto-generated from RARE rule bv-bitwise-idemp-2
|
BV_BITWISE_NOT_AND
Auto-generated from RARE rule bv-bitwise-not-and
|
BV_BITWISE_NOT_OR
Auto-generated from RARE rule bv-bitwise-not-or
|
BV_BITWISE_SLICING
Bitvectors - Extract continuous substrings of bitvectors
\[
bvand(a,\ c) = concat(bvand(a[i_0:j_0],\ c_0) ... bvand(a[i_n:j_n],\ c_n))
\]
where c0,..., cn are maximally continuous substrings of 0 or 1 in the
constant c
|
BV_COMMUTATIVE_ADD
Auto-generated from RARE rule bv-commutative-add
|
BV_COMMUTATIVE_AND
Auto-generated from RARE rule bv-commutative-and
|
BV_COMMUTATIVE_MUL
Auto-generated from RARE rule bv-commutative-mul
|
BV_COMMUTATIVE_OR
Auto-generated from RARE rule bv-commutative-or
|
BV_COMMUTATIVE_XOR
Auto-generated from RARE rule bv-commutative-xor
|
BV_COMP_ELIMINATE
Auto-generated from RARE rule bv-comp-eliminate
|
BV_CONCAT_EXTRACT_MERGE
Auto-generated from RARE rule bv-concat-extract-merge
|
BV_CONCAT_FLATTEN
Auto-generated from RARE rule bv-concat-flatten
|
BV_CONCAT_MERGE_CONST
Auto-generated from RARE rule bv-concat-merge-
|
BV_CONCAT_TO_MULT
Auto-generated from RARE rule bv-concat-to-mult
|
BV_EXTRACT_BITWISE_AND
Auto-generated from RARE rule bv-extract-bitwise-and
|
BV_EXTRACT_BITWISE_OR
Auto-generated from RARE rule bv-extract-bitwise-or
|
BV_EXTRACT_BITWISE_XOR
Auto-generated from RARE rule bv-extract-bitwise-xor
|
BV_EXTRACT_CONCAT_1
Auto-generated from RARE rule bv-extract-concat-1
|
BV_EXTRACT_CONCAT_2
Auto-generated from RARE rule bv-extract-concat-2
|
BV_EXTRACT_CONCAT_3
Auto-generated from RARE rule bv-extract-concat-3
|
BV_EXTRACT_CONCAT_4
Auto-generated from RARE rule bv-extract-concat-4
|
BV_EXTRACT_EXTRACT
Auto-generated from RARE rule bv-extract-extract
|
BV_EXTRACT_MULT_LEADING_BIT
Auto-generated from RARE rule bv-extract-mult-leading-bit
|
BV_EXTRACT_NOT
Auto-generated from RARE rule bv-extract-not
|
BV_EXTRACT_SIGN_EXTEND_1
Auto-generated from RARE rule bv-extract-sign-extend-1
|
BV_EXTRACT_SIGN_EXTEND_2
Auto-generated from RARE rule bv-extract-sign-extend-2
|
BV_EXTRACT_SIGN_EXTEND_3
Auto-generated from RARE rule bv-extract-sign-extend-3
|
BV_EXTRACT_WHOLE
Auto-generated from RARE rule bv-extract-whole
|
BV_ITE_CONST_CHILDREN_1
Auto-generated from RARE rule bv-ite--children-1
|
BV_ITE_CONST_CHILDREN_2
Auto-generated from RARE rule bv-ite--children-2
|
BV_ITE_EQUAL_CHILDREN
Auto-generated from RARE rule bv-ite-equal-children
|
BV_ITE_EQUAL_COND_1
Auto-generated from RARE rule bv-ite-equal-cond-1
|
BV_ITE_EQUAL_COND_2
Auto-generated from RARE rule bv-ite-equal-cond-2
|
BV_ITE_EQUAL_COND_3
Auto-generated from RARE rule bv-ite-equal-cond-3
|
BV_ITE_MERGE_ELSE_ELSE
Auto-generated from RARE rule bv-ite-merge-else-else
|
BV_ITE_MERGE_ELSE_IF
Auto-generated from RARE rule bv-ite-merge-else-if
|
BV_ITE_MERGE_THEN_ELSE
Auto-generated from RARE rule bv-ite-merge-then-else
|
BV_ITE_MERGE_THEN_IF
Auto-generated from RARE rule bv-ite-merge-then-if
|
BV_LSHR_BY_CONST_0
Auto-generated from RARE rule bv-lshr-by--0
|
BV_LSHR_BY_CONST_1
Auto-generated from RARE rule bv-lshr-by--1
|
BV_LSHR_BY_CONST_2
Auto-generated from RARE rule bv-lshr-by--2
|
BV_LSHR_ZERO
Auto-generated from RARE rule bv-lshr-zero
|
BV_LT_SELF
Auto-generated from RARE rule bv-lt-self
|
BV_MERGE_SIGN_EXTEND_1
Auto-generated from RARE rule bv-merge-sign-extend-1
|
BV_MERGE_SIGN_EXTEND_2
Auto-generated from RARE rule bv-merge-sign-extend-2
|
BV_MERGE_SIGN_EXTEND_3
Auto-generated from RARE rule bv-merge-sign-extend-3
|
BV_MUL_FLATTEN
Auto-generated from RARE rule bv-mul-flatten
|
BV_MUL_ONE
Auto-generated from RARE rule bv-mul-one
|
BV_MUL_ZERO
Auto-generated from RARE rule bv-mul-zero
|
BV_MULT_DISTRIB_1
Auto-generated from RARE rule bv-mult-distrib-1
|
BV_MULT_DISTRIB_2
Auto-generated from RARE rule bv-mult-distrib-2
|
BV_MULT_DISTRIB_CONST_ADD
Auto-generated from RARE rule bv-mult-distrib--add
|
BV_MULT_DISTRIB_CONST_NEG
Auto-generated from RARE rule bv-mult-distrib--neg
|
BV_MULT_DISTRIB_CONST_SUB
Auto-generated from RARE rule bv-mult-distrib--sub
|
BV_MULT_POW2_1
Auto-generated from RARE rule bv-mult-pow2-1
|
BV_MULT_POW2_2
Auto-generated from RARE rule bv-mult-pow2-2
|
BV_MULT_POW2_2B
Auto-generated from RARE rule bv-mult-pow2-2b
|
BV_MULT_SIMPLIFY
Bitvectors - Extract negations from multiplicands
\[
bvmul(bvneg(a),\ b,\ c) = bvneg(bvmul(a,\ b,\ c))
\]
|
BV_MULT_SLT_MULT_1
Auto-generated from RARE rule bv-mult-slt-mult-1
|
BV_MULT_SLT_MULT_2
Auto-generated from RARE rule bv-mult-slt-mult-2
|
BV_NAND_ELIMINATE
Auto-generated from RARE rule bv-nand-eliminate
|
BV_NEG_ADD
Auto-generated from RARE rule bv-neg-add
|
BV_NEG_IDEMP
Auto-generated from RARE rule bv-neg-idemp
|
BV_NEG_MULT
Auto-generated from RARE rule bv-neg-mult
|
BV_NEG_SUB
Auto-generated from RARE rule bv-neg-sub
|
BV_NOR_ELIMINATE
Auto-generated from RARE rule bv-nor-eliminate
|
BV_NOT_IDEMP
Auto-generated from RARE rule bv-not-idemp
|
BV_NOT_NEQ
Auto-generated from RARE rule bv-not-neq
|
BV_NOT_SLE
Auto-generated from RARE rule bv-not-sle
|
BV_NOT_ULE
Auto-generated from RARE rule bv-not-ule
|
BV_NOT_ULT
Auto-generated from RARE rule bv-not-ult
|
BV_NOT_XOR
Auto-generated from RARE rule bv-not-xor
|
BV_OR_CONCAT_PULLUP
Auto-generated from RARE rule bv-or-concat-pullup
|
BV_OR_FLATTEN
Auto-generated from RARE rule bv-or-flatten
|
BV_OR_ONE
Auto-generated from RARE rule bv-or-one
|
BV_OR_SIMPLIFY_1
Auto-generated from RARE rule bv-or-simplify-1
|
BV_OR_SIMPLIFY_2
Auto-generated from RARE rule bv-or-simplify-2
|
BV_OR_ZERO
Auto-generated from RARE rule bv-or-zero
|
BV_REDAND_ELIMINATE
Auto-generated from RARE rule bv-redand-eliminate
|
BV_REDOR_ELIMINATE
Auto-generated from RARE rule bv-redor-eliminate
|
BV_REPEAT_ELIMINATE_1
Auto-generated from RARE rule bv-repeat-eliminate-1
|
BV_REPEAT_ELIMINATE_2
Auto-generated from RARE rule bv-repeat-eliminate-2
|
BV_ROTATE_LEFT_ELIMINATE_1
Auto-generated from RARE rule bv-rotate-left-eliminate-1
|
BV_ROTATE_LEFT_ELIMINATE_2
Auto-generated from RARE rule bv-rotate-left-eliminate-2
|
BV_ROTATE_RIGHT_ELIMINATE_1
Auto-generated from RARE rule bv-rotate-right-eliminate-1
|
BV_ROTATE_RIGHT_ELIMINATE_2
Auto-generated from RARE rule bv-rotate-right-eliminate-2
|
BV_SADDO_ELIMINATE
Auto-generated from RARE rule bv-saddo-eliminate
|
BV_SDIV_ELIMINATE
Auto-generated from RARE rule bv-sdiv-eliminate
|
BV_SDIV_ELIMINATE_FEWER_BITWISE_OPS
Auto-generated from RARE rule bv-sdiv-eliminate-fewer-bitwise-ops
|
BV_SDIVO_ELIMINATE
Auto-generated from RARE rule bv-sdivo-eliminate
|
BV_SGE_ELIMINATE
Auto-generated from RARE rule bv-sge-eliminate
|
BV_SGT_ELIMINATE
Auto-generated from RARE rule bv-sgt-eliminate
|
BV_SHL_BY_CONST_0
Auto-generated from RARE rule bv-shl-by--0
|
BV_SHL_BY_CONST_1
Auto-generated from RARE rule bv-shl-by--1
|
BV_SHL_BY_CONST_2
Auto-generated from RARE rule bv-shl-by--2
|
BV_SHL_ZERO
Auto-generated from RARE rule bv-shl-zero
|
BV_SIGN_EXTEND_ELIMINATE
Auto-generated from RARE rule bv-sign-extend-eliminate
|
BV_SIGN_EXTEND_ELIMINATE_0
Auto-generated from RARE rule bv-sign-extend-eliminate-0
|
BV_SIGN_EXTEND_EQ_CONST_1
Auto-generated from RARE rule bv-sign-extend-eq--1
|
BV_SIGN_EXTEND_EQ_CONST_2
Auto-generated from RARE rule bv-sign-extend-eq--2
|
BV_SIGN_EXTEND_ULT_CONST_1
Auto-generated from RARE rule bv-sign-extend-ult--1
|
BV_SIGN_EXTEND_ULT_CONST_2
Auto-generated from RARE rule bv-sign-extend-ult--2
|
BV_SIGN_EXTEND_ULT_CONST_3
Auto-generated from RARE rule bv-sign-extend-ult--3
|
BV_SIGN_EXTEND_ULT_CONST_4
Auto-generated from RARE rule bv-sign-extend-ult--4
|
BV_SLE_ELIMINATE
Auto-generated from RARE rule bv-sle-eliminate
|
BV_SLE_SELF
Auto-generated from RARE rule bv-sle-self
|
BV_SLT_ELIMINATE
Auto-generated from RARE rule bv-slt-eliminate
|
BV_SLT_ZERO
Auto-generated from RARE rule bv-slt-zero
|
BV_SMOD_ELIMINATE
Auto-generated from RARE rule bv-smod-eliminate
|
BV_SMOD_ELIMINATE_FEWER_BITWISE_OPS
Auto-generated from RARE rule bv-smod-eliminate-fewer-bitwise-ops
|
BV_SMULO_ELIMINATE
Bitvectors - Unsigned multiplication overflow detection elimination
See M.Gok, M.J.
|
BV_SREM_ELIMINATE
Auto-generated from RARE rule bv-srem-eliminate
|
BV_SREM_ELIMINATE_FEWER_BITWISE_OPS
Auto-generated from RARE rule bv-srem-eliminate-fewer-bitwise-ops
|
BV_SSUBO_ELIMINATE
Auto-generated from RARE rule bv-ssubo-eliminate
|
BV_SUB_ELIMINATE
Auto-generated from RARE rule bv-sub-eliminate
|
BV_UADDO_ELIMINATE
Auto-generated from RARE rule bv-uaddo-eliminate
|
BV_UDIV_ONE
Auto-generated from RARE rule bv-udiv-one
|
BV_UDIV_POW2_NOT_ONE
Auto-generated from RARE rule bv-udiv-pow2-not-one
|
BV_UDIV_ZERO
Auto-generated from RARE rule bv-udiv-zero
|
BV_UGE_ELIMINATE
Auto-generated from RARE rule bv-uge-eliminate
|
BV_UGT_ELIMINATE
Auto-generated from RARE rule bv-ugt-eliminate
|
BV_UGT_UREM
Auto-generated from RARE rule bv-ugt-urem
|
BV_ULE_ELIMINATE
Auto-generated from RARE rule bv-ule-eliminate
|
BV_ULE_MAX
Auto-generated from RARE rule bv-ule-max
|
BV_ULE_SELF
Auto-generated from RARE rule bv-ule-self
|
BV_ULE_ZERO
Auto-generated from RARE rule bv-ule-zero
|
BV_ULT_ADD_ONE
Auto-generated from RARE rule bv-ult-add-one
|
BV_ULT_ONE
Auto-generated from RARE rule bv-ult-one
|
BV_ULT_ONES
Auto-generated from RARE rule bv-ult-ones
|
BV_ULT_SELF
Auto-generated from RARE rule bv-ult-self
|
BV_ULT_ZERO_1
Auto-generated from RARE rule bv-ult-zero-1
|
BV_ULT_ZERO_2
Auto-generated from RARE rule bv-ult-zero-2
|
BV_UMULO_ELIMINATE
Bitvectors - Unsigned multiplication overflow detection elimination
See M.Gok, M.J.
|
BV_UREM_ONE
Auto-generated from RARE rule bv-urem-one
|
BV_UREM_POW2_NOT_ONE
Auto-generated from RARE rule bv-urem-pow2-not-one
|
BV_UREM_SELF
Auto-generated from RARE rule bv-urem-self
|
BV_USUBO_ELIMINATE
Auto-generated from RARE rule bv-usubo-eliminate
|
BV_XNOR_ELIMINATE
Auto-generated from RARE rule bv-xnor-eliminate
|
BV_XOR_CONCAT_PULLUP
Auto-generated from RARE rule bv-xor-concat-pullup
|
BV_XOR_DUPLICATE
Auto-generated from RARE rule bv-xor-duplicate
|
BV_XOR_FLATTEN
Auto-generated from RARE rule bv-xor-flatten
|
BV_XOR_NOT
Auto-generated from RARE rule bv-xor-not
|
BV_XOR_ONES
Auto-generated from RARE rule bv-xor-ones
|
BV_XOR_SIMPLIFY_1
Auto-generated from RARE rule bv-xor-simplify-1
|
BV_XOR_SIMPLIFY_2
Auto-generated from RARE rule bv-xor-simplify-2
|
BV_XOR_SIMPLIFY_3
Auto-generated from RARE rule bv-xor-simplify-3
|
BV_XOR_ZERO
Auto-generated from RARE rule bv-xor-zero
|
BV_ZERO_EXTEND_ELIMINATE
Auto-generated from RARE rule bv-zero-extend-eliminate
|
BV_ZERO_EXTEND_ELIMINATE_0
Auto-generated from RARE rule bv-zero-extend-eliminate-0
|
BV_ZERO_EXTEND_EQ_CONST_1
Auto-generated from RARE rule bv-zero-extend-eq--1
|
BV_ZERO_EXTEND_EQ_CONST_2
Auto-generated from RARE rule bv-zero-extend-eq--2
|
BV_ZERO_EXTEND_ULT_CONST_1
Auto-generated from RARE rule bv-zero-extend-ult--1
|
BV_ZERO_EXTEND_ULT_CONST_2
Auto-generated from RARE rule bv-zero-extend-ult--2
|
BV_ZERO_ULE
Auto-generated from RARE rule bv-zero-ule
|
DISTINCT_BINARY_ELIM
Auto-generated from RARE rule distinct-binary-elim
|
DISTINCT_ELIM
Builtin – Distinct elimination
\[
\texttt{distinct}(t_1, \ldots, tn) = \bigwedge_{i \neq j} t_i \neq t_j
\]
|
DT_COLLAPSE_SELECTOR
Datatypes - collapse selector
\[
s_i(c(t_1, \ldots, t_n)) = t_i
\]
where \(s_i\) is the \(i^{th}\) selector for constructor \(c\).
|
DT_COLLAPSE_TESTER
Datatypes - collapse tester
\[
\mathit{is}_c(c(t_1, \ldots, t_n)) = true
\]
or alternatively
\[
\mathit{is}_c(d(t_1, \ldots, t_n)) = false
\]
where \(c\) and \(d\) are distinct constructors.
|
DT_COLLAPSE_TESTER_SINGLETON
Datatypes - collapse tester
\[
\mathit{is}_c(t) = true
\]
where \(c\) is the only constructor of its associated datatype.
|
DT_CONS_EQ
Datatypes - constructor equality
\[
(c(t_1, \ldots, t_n) = c(s_1, \ldots, s_n)) =
(t_1 = s_1 \wedge \ldots \wedge t_n = s_n)
\]
or alternatively
\[
(c(t_1, \ldots, t_n) = d(s_1, \ldots, s_m)) = false
\]
where \(c\) and \(d\) are distinct constructors.
|
DT_INST
Datatypes – Instantiation
\[
\mathit{is}_C(t) = (t = C(\mathit{sel}_1(t),\dots,\mathit{sel}_n(t)))
\]
where \(C\) is the \(n^{\mathit{th}}\) constructor of the type of
\(t\), and \(\mathit{is}_C\) is the discriminator (tester) for
\(C\).
|
EQ_REFL
Auto-generated from RARE rule eq-refl
|
EQ_SYMM
Auto-generated from RARE rule eq-symm
|
EXISTS_ELIM
Quantifiers – Exists elimination
\[
\exists x_1\dots x_n.
|
ITE_ELSE_FALSE
Auto-generated from RARE rule ite-else-false
|
ITE_ELSE_LOOKAHEAD
Auto-generated from RARE rule ite-else-lookahead
|
ITE_ELSE_LOOKAHEAD_SELF
Auto-generated from RARE rule ite-else-lookahead-self
|
ITE_ELSE_NEG_LOOKAHEAD
Auto-generated from RARE rule ite-else-neg-lookahead
|
ITE_ELSE_TRUE
Auto-generated from RARE rule ite-else-true
|
ITE_EQ_BRANCH
Auto-generated from RARE rule ite-eq-branch
|
ITE_FALSE_COND
Auto-generated from RARE rule ite-false-cond
|
ITE_NEG_BRANCH
Auto-generated from RARE rule ite-neg-branch
|
ITE_NOT_COND
Auto-generated from RARE rule ite-not-cond
|
ITE_THEN_FALSE
Auto-generated from RARE rule ite-then-false
|
ITE_THEN_LOOKAHEAD
Auto-generated from RARE rule ite-then-lookahead
|
ITE_THEN_LOOKAHEAD_SELF
Auto-generated from RARE rule ite-then-lookahead-self
|
ITE_THEN_NEG_LOOKAHEAD
Auto-generated from RARE rule ite-then-neg-lookahead
|
ITE_THEN_TRUE
Auto-generated from RARE rule ite-then-true
|
ITE_TRUE_COND
Auto-generated from RARE rule ite-true-cond
|
MACRO_ARITH_STRING_PRED_ENTAIL
Arithmetic - strings predicate entailment
\[
(= s t) = c
\]
\[
(>= s t) = c
\]
where \(c\) is a Boolean constant.
|
MACRO_BOOL_NNF_NORM
Booleans – Negation Normal Form with normalization
\[
F = G
\]
where \(G\) is the result of applying negation normal form to
\(F\) with additional normalizations, see
TheoryBoolRewriter.computeNnfNorm.
|
MACRO_QUANT_PARTITION_CONNECTED_FV
Quantifiers – Macro connected free variable partitioning
\[
\forall X.
|
MACRO_SUBSTR_STRIP_SYM_LENGTH
Strings - strings substring strip symbolic length
\[
str.substr(s, n, m) = t
\]
where \(t\) is obtained by fully or partially stripping components of
\(s\) based on \(n\) and \(m\).
|
NONE
This enumeration represents the rewrite rules used in a rewrite proof.
|
QUANT_MERGE_PRENEX
Quantifiers – Merge prenex
\[
\forall X_1.
|
QUANT_MINISCOPE
Quantifiers – Miniscoping
\[
\forall X.
|
QUANT_UNUSED_VARS
Quantifiers – Unused variables
\[
\forall X.
|
RE_ALL_ELIM
Auto-generated from RARE rule re-all-elim
|
RE_CONCAT_EMP
Auto-generated from RARE rule re-concat-emp
|
RE_CONCAT_FLATTEN
Auto-generated from RARE rule re-concat-flatten
|
RE_CONCAT_MERGE
Auto-generated from RARE rule re-concat-merge
|
RE_CONCAT_NONE
Auto-generated from RARE rule re-concat-none
|
RE_CONCAT_STAR_SWAP
Auto-generated from RARE rule re-concat-star-swap
|
RE_DIFF_ELIM
Auto-generated from RARE rule re-diff-elim
|
RE_IN_COMP
Auto-generated from RARE rule re-in-comp
|
RE_IN_CSTRING
Auto-generated from RARE rule re-in-cstring
|
RE_IN_EMPTY
Auto-generated from RARE rule re-in-empty
|
RE_IN_SIGMA
Auto-generated from RARE rule re-in-sigma
|
RE_IN_SIGMA_STAR
Auto-generated from RARE rule re-in-sigma-star
|
RE_INTER_ALL
Auto-generated from RARE rule re-inter-all
|
RE_INTER_CSTRING
Auto-generated from RARE rule re-inter-cstring
|
RE_INTER_CSTRING_NEG
Auto-generated from RARE rule re-inter-cstring-neg
|
RE_INTER_DUP
Auto-generated from RARE rule re-inter-dup
|
RE_INTER_FLATTEN
Auto-generated from RARE rule re-inter-flatten
|
RE_INTER_NONE
Auto-generated from RARE rule re-inter-none
|
RE_INTER_UNION_INCLUSION
Strings - regular expression intersection/union inclusion
\[
(re.inter\ R) = \mathit{re.inter}(\mathit{re.none}, R_0)
\]
where \(R\) is a list of regular expressions containing `r_1`,
`re.comp(r_2)` and the list \(R_0\) where `r_2` is a superset of
`r_1`.
|
RE_LOOP_ELIM
Strings - regular expression loop elimination
\[
re.loop_{l,u}(R) = re.union(R^l, \ldots, R^u)
\]
where \(u \geq l\).
|
RE_LOOP_NEG
Auto-generated from RARE rule re-loop-neg
|
RE_OPT_ELIM
Auto-generated from RARE rule re-opt-elim
|
RE_UNION_ALL
Auto-generated from RARE rule re-union-all
|
RE_UNION_DUP
Auto-generated from RARE rule re-union-dup
|
RE_UNION_FLATTEN
Auto-generated from RARE rule re-union-flatten
|
RE_UNION_NONE
Auto-generated from RARE rule re-union-none
|
SEQ_LEN_UNIT
Auto-generated from RARE rule seq-len-unit
|
SEQ_NTH_UNIT
Auto-generated from RARE rule seq-nth-unit
|
SEQ_REV_CONCAT
Auto-generated from RARE rule seq-rev-concat
|
SEQ_REV_UNIT
Auto-generated from RARE rule seq-rev-unit
|
SETS_CARD_EMP
Auto-generated from RARE rule sets-card-emp
|
SETS_CARD_MINUS
Auto-generated from RARE rule sets-card-minus
|
SETS_CARD_SINGLETON
Auto-generated from RARE rule sets-card-singleton
|
SETS_CARD_UNION
Auto-generated from RARE rule sets-card-union
|
SETS_CHOOSE_SINGLETON
Auto-generated from RARE rule sets-choose-singleton
|
SETS_EQ_SINGLETON_EMP
Auto-generated from RARE rule sets-eq-singleton-emp
|
SETS_INTER_COMM
Auto-generated from RARE rule sets-inter-comm
|
SETS_INTER_EMP1
Auto-generated from RARE rule sets-inter-emp1
|
SETS_INTER_EMP2
Auto-generated from RARE rule sets-inter-emp2
|
SETS_INTER_MEMBER
Auto-generated from RARE rule sets-inter-member
|
SETS_IS_EMPTY_EVAL
Sets - empty tester evaluation
\[
\mathit{sets.is\_empty}(\epsilon) = \top
\]
where \(\epsilon\) is the empty set, or alternatively:
\[
\mathit{sets.is\_empty}(c) = \bot
\]
where \(c\) is a constant set that is not the empty set.
|
SETS_MEMBER_EMP
Auto-generated from RARE rule sets-member-emp
|
SETS_MEMBER_SINGLETON
Auto-generated from RARE rule sets-member-singleton
|
SETS_MINUS_EMP1
Auto-generated from RARE rule sets-minus-emp1
|
SETS_MINUS_EMP2
Auto-generated from RARE rule sets-minus-emp2
|
SETS_MINUS_MEMBER
Auto-generated from RARE rule sets-minus-member
|
SETS_SUBSET_ELIM
Auto-generated from RARE rule sets-subset-elim
|
SETS_UNION_COMM
Auto-generated from RARE rule sets-union-comm
|
SETS_UNION_EMP1
Auto-generated from RARE rule sets-union-emp1
|
SETS_UNION_EMP2
Auto-generated from RARE rule sets-union-emp2
|
SETS_UNION_MEMBER
Auto-generated from RARE rule sets-union-member
|
STR_AT_ELIM
Auto-generated from RARE rule str-at-elim
|
STR_CONCAT_CLASH
Auto-generated from RARE rule str-concat-clash
|
STR_CONCAT_CLASH_CHAR
Auto-generated from RARE rule str-concat-clash-char
|
STR_CONCAT_CLASH_CHAR_REV
Auto-generated from RARE rule str-concat-clash-char-rev
|
STR_CONCAT_CLASH_REV
Auto-generated from RARE rule str-concat-clash-rev
|
STR_CONCAT_CLASH2
Auto-generated from RARE rule str-concat-clash2
|
STR_CONCAT_CLASH2_REV
Auto-generated from RARE rule str-concat-clash2-rev
|
STR_CONCAT_EMP
Auto-generated from RARE rule str-concat-emp
|
STR_CONCAT_FLATTEN
Auto-generated from RARE rule str-concat-flatten
|
STR_CONCAT_FLATTEN_EQ
Auto-generated from RARE rule str-concat-flatten-eq
|
STR_CONCAT_FLATTEN_EQ_REV
Auto-generated from RARE rule str-concat-flatten-eq-rev
|
STR_CONCAT_UNIFY
Auto-generated from RARE rule str-concat-unify
|
STR_CONCAT_UNIFY_BASE
Auto-generated from RARE rule str-concat-unify-base
|
STR_CONCAT_UNIFY_BASE_REV
Auto-generated from RARE rule str-concat-unify-base-rev
|
STR_CONCAT_UNIFY_REV
Auto-generated from RARE rule str-concat-unify-rev
|
STR_CONTAINS_CONCAT_FIND
Auto-generated from RARE rule str-contains-concat-find
|
STR_CONTAINS_EMP
Auto-generated from RARE rule str-contains-emp
|
STR_CONTAINS_IS_EMP
Auto-generated from RARE rule str-contains-is-emp
|
STR_CONTAINS_LEQ_LEN_EQ
Auto-generated from RARE rule str-contains-leq-len-eq
|
STR_CONTAINS_LT_LEN
Auto-generated from RARE rule str-contains-lt-len
|
STR_CONTAINS_REFL
Auto-generated from RARE rule str-contains-refl
|
STR_CONTAINS_SPLIT_CHAR
Auto-generated from RARE rule str-contains-split-char
|
STR_EQ_CTN_FALSE
Auto-generated from RARE rule str-eq-ctn-false
|
STR_EQ_CTN_FULL_FALSE1
Auto-generated from RARE rule str-eq-ctn-full-false1
|
STR_EQ_CTN_FULL_FALSE2
Auto-generated from RARE rule str-eq-ctn-full-false2
|
STR_IN_RE_CONCAT_STAR_CHAR
Strings - string in regular expression concatenation star character
\[
\mathit{str.in\_re}(\mathit{str}.
|
STR_IN_RE_CONSUME
Strings - regular expression membership consume
\[
\mathit{str.in_re}(s, R) = b
\]
where \(b\) is either \(false\) or the result of stripping
entailed prefixes and suffixes off of \(s\) and \(R\).
|
STR_IN_RE_CONTAINS
Auto-generated from RARE rule str-in-re-contains
|
STR_IN_RE_EVAL
Strings - regular expression membership evaluation
\[
\mathit{str.in\_re}(s, R) = c
\]
where \(s\) is a constant string, \(R\) is a constant regular
expression and \(c\) is true or false.
|
STR_IN_RE_INTER_ELIM
Auto-generated from RARE rule str-in-re-inter-elim
|
STR_IN_RE_RANGE_ELIM
Auto-generated from RARE rule str-in-re-range-elim
|
STR_IN_RE_REQ_UNFOLD
Auto-generated from RARE rule str-in-re-req-unfold
|
STR_IN_RE_REQ_UNFOLD_REV
Auto-generated from RARE rule str-in-re-req-unfold-rev
|
STR_IN_RE_SIGMA
Strings - string in regular expression sigma
\[
\mathit{str.in\_re}(s, \mathit{re}.
|
STR_IN_RE_SIGMA_STAR
Strings - string in regular expression sigma star
\[
\mathit{str.in\_re}(s, \mathit{re}.
|
STR_IN_RE_SKIP_UNFOLD
Auto-generated from RARE rule str-in-re-skip-unfold
|
STR_IN_RE_SKIP_UNFOLD_REV
Auto-generated from RARE rule str-in-re-skip-unfold-rev
|
STR_IN_RE_STRIP_CHAR
Auto-generated from RARE rule str-in-re-strip-char
|
STR_IN_RE_STRIP_CHAR_REV
Auto-generated from RARE rule str-in-re-strip-char-rev
|
STR_IN_RE_STRIP_CHAR_S_SINGLE
Auto-generated from RARE rule str-in-re-strip-char-s-single
|
STR_IN_RE_STRIP_CHAR_S_SINGLE_REV
Auto-generated from RARE rule str-in-re-strip-char-s-single-rev
|
STR_IN_RE_STRIP_PREFIX
Auto-generated from RARE rule str-in-re-strip-prefix
|
STR_IN_RE_STRIP_PREFIX_BASE
Auto-generated from RARE rule str-in-re-strip-prefix-base
|
STR_IN_RE_STRIP_PREFIX_BASE_NEG
Auto-generated from RARE rule str-in-re-strip-prefix-base-neg
|
STR_IN_RE_STRIP_PREFIX_BASE_NEG_REV
Auto-generated from RARE rule str-in-re-strip-prefix-base-neg-rev
|
STR_IN_RE_STRIP_PREFIX_BASE_REV
Auto-generated from RARE rule str-in-re-strip-prefix-base-rev
|
STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE
Auto-generated from RARE rule str-in-re-strip-prefix-base-s-single
|
STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE_NEG
Auto-generated from RARE rule str-in-re-strip-prefix-base-s-single-neg
|
STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE_NEG_REV
Auto-generated from RARE rule str-in-re-strip-prefix-base-s-single-neg-rev
|
STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE_REV
Auto-generated from RARE rule str-in-re-strip-prefix-base-s-single-rev
|
STR_IN_RE_STRIP_PREFIX_NEG
Auto-generated from RARE rule str-in-re-strip-prefix-neg
|
STR_IN_RE_STRIP_PREFIX_NEG_REV
Auto-generated from RARE rule str-in-re-strip-prefix-neg-rev
|
STR_IN_RE_STRIP_PREFIX_REV
Auto-generated from RARE rule str-in-re-strip-prefix-rev
|
STR_IN_RE_STRIP_PREFIX_S_SINGLE
Auto-generated from RARE rule str-in-re-strip-prefix-s-single
|
STR_IN_RE_STRIP_PREFIX_S_SINGLE_NEG
Auto-generated from RARE rule str-in-re-strip-prefix-s-single-neg
|
STR_IN_RE_STRIP_PREFIX_S_SINGLE_NEG_REV
Auto-generated from RARE rule str-in-re-strip-prefix-s-single-neg-rev
|
STR_IN_RE_STRIP_PREFIX_S_SINGLE_REV
Auto-generated from RARE rule str-in-re-strip-prefix-s-single-rev
|
STR_IN_RE_STRIP_PREFIX_SR_SINGLE
Auto-generated from RARE rule str-in-re-strip-prefix-sr-single
|
STR_IN_RE_STRIP_PREFIX_SR_SINGLE_NEG
Auto-generated from RARE rule str-in-re-strip-prefix-sr-single-neg
|
STR_IN_RE_STRIP_PREFIX_SR_SINGLE_NEG_REV
Auto-generated from RARE rule str-in-re-strip-prefix-sr-single-neg-rev
|
STR_IN_RE_STRIP_PREFIX_SR_SINGLE_REV
Auto-generated from RARE rule str-in-re-strip-prefix-sr-single-rev
|
STR_IN_RE_STRIP_PREFIX_SRS_SINGLE
Auto-generated from RARE rule str-in-re-strip-prefix-srs-single
|
STR_IN_RE_STRIP_PREFIX_SRS_SINGLE_NEG
Auto-generated from RARE rule str-in-re-strip-prefix-srs-single-neg
|
STR_IN_RE_STRIP_PREFIX_SRS_SINGLE_NEG_REV
Auto-generated from RARE rule str-in-re-strip-prefix-srs-single-neg-rev
|
STR_IN_RE_STRIP_PREFIX_SRS_SINGLE_REV
Auto-generated from RARE rule str-in-re-strip-prefix-srs-single-rev
|
STR_IN_RE_TEST_UNFOLD
Auto-generated from RARE rule str-in-re-test-unfold
|
STR_IN_RE_TEST_UNFOLD_REV
Auto-generated from RARE rule str-in-re-test-unfold-rev
|
STR_IN_RE_UNION_ELIM
Auto-generated from RARE rule str-in-re-union-elim
|
STR_INDEXOF_NO_CONTAINS
Auto-generated from RARE rule str-indexof-no-contains
|
STR_INDEXOF_SELF
Auto-generated from RARE rule str-indexof-self
|
STR_LEN_CONCAT_REC
Auto-generated from RARE rule str-len-concat-rec
|
STR_LEN_REPLACE_INV
Auto-generated from RARE rule str-len-replace-inv
|
STR_LEN_SUBSTR_IN_RANGE
Auto-generated from RARE rule str-len-substr-in-range
|
STR_LEN_SUBSTR_UB1
Auto-generated from RARE rule str-len-substr-ub1
|
STR_LEN_SUBSTR_UB2
Auto-generated from RARE rule str-len-substr-ub2
|
STR_LEN_UPDATE_INV
Auto-generated from RARE rule str-len-update-inv
|
STR_NTH_ELIM_CODE
Auto-generated from RARE rule str-nth-elim-code
|
STR_PREFIXOF_ELIM
Auto-generated from RARE rule str-prefixof-elim
|
STR_PREFIXOF_ONE
Auto-generated from RARE rule str-prefixof-one
|
STR_REPLACE_EMPTY
Auto-generated from RARE rule str-replace-empty
|
STR_REPLACE_NO_CONTAINS
Auto-generated from RARE rule str-replace-no-contains
|
STR_REPLACE_SELF
Auto-generated from RARE rule str-replace-self
|
STR_SUBSTR_COMBINE1
Auto-generated from RARE rule str-substr-combine1
|
STR_SUBSTR_COMBINE2
Auto-generated from RARE rule str-substr-combine2
|
STR_SUBSTR_COMBINE3
Auto-generated from RARE rule str-substr-combine3
|
STR_SUBSTR_COMBINE4
Auto-generated from RARE rule str-substr-combine4
|
STR_SUBSTR_CONCAT1
Auto-generated from RARE rule str-substr-concat1
|
STR_SUBSTR_CONCAT2
Auto-generated from RARE rule str-substr-concat2
|
STR_SUBSTR_EMPTY_RANGE
Auto-generated from RARE rule str-substr-empty-range
|
STR_SUBSTR_EMPTY_START
Auto-generated from RARE rule str-substr-empty-start
|
STR_SUBSTR_EMPTY_START_NEG
Auto-generated from RARE rule str-substr-empty-start-neg
|
STR_SUBSTR_EMPTY_STR
Auto-generated from RARE rule str-substr-empty-str
|
STR_SUBSTR_EQ_EMPTY
Auto-generated from RARE rule str-substr-eq-empty
|
STR_SUBSTR_FULL
Auto-generated from RARE rule str-substr-full
|
STR_SUBSTR_FULL_EQ
Auto-generated from RARE rule str-substr-full-eq
|
STR_SUBSTR_LEN_INCLUDE
Auto-generated from RARE rule str-substr-len-include
|
STR_SUBSTR_LEN_INCLUDE_PRE
Auto-generated from RARE rule str-substr-len-include-pre
|
STR_SUBSTR_LEN_SKIP
Auto-generated from RARE rule str-substr-len-skip
|
STR_SUFFIXOF_ELIM
Auto-generated from RARE rule str-suffixof-elim
|
STR_SUFFIXOF_ONE
Auto-generated from RARE rule str-suffixof-one
|
STR_TO_LOWER_CONCAT
Auto-generated from RARE rule str-to-lower-concat
|
STR_TO_LOWER_UPPER
Auto-generated from RARE rule str-to-lower-upper
|
STR_TO_UPPER_CONCAT
Auto-generated from RARE rule str-to-upper-concat
|
STR_TO_UPPER_LOWER
Auto-generated from RARE rule str-to-upper-lower
|
UF_BV2NAT_GEQ_ELIM
Auto-generated from RARE rule uf-bv2nat-geq-elim
|
| Modifier and Type | Method and Description |
|---|---|
static ProofRewriteRule |
fromInt(int value) |
int |
getValue() |
static ProofRewriteRule |
valueOf(String name)
Returns the enum constant of this type with the specified name.
|
static ProofRewriteRule[] |
values()
Returns an array containing the constants of this enum type, in
the order they are declared.
|
public static final ProofRewriteRule NONE
ProofRule.DSL_REWRITE> proof rule
and the THEORY_REWRITE <cvc5.ProofRule.THEORY_REWRITE>
proof rule.public static final ProofRewriteRule DISTINCT_ELIM
public static final ProofRewriteRule MACRO_BOOL_NNF_NORM
public static final ProofRewriteRule ARITH_DIV_BY_CONST_ELIM
public static final ProofRewriteRule MACRO_ARITH_STRING_PRED_ENTAIL
ProofRule.EVALUATE>,
ARITH_POLY_NORM <cvc5.ProofRule.ARITH_POLY_NORM>,
ARITH_STRING_PRED_ENTAIL <cvc5.ProofRewriteRule.ARITH_STRING_PRED_ENTAIL>,
ARITH_STRING_PRED_SAFE_APPROX <cvc5.ProofRewriteRule.ARITH_STRING_PRED_SAFE_APPROX>,
as well as other rewrites for normalizing arithmetic predicates.public static final ProofRewriteRule ARITH_STRING_PRED_ENTAIL
public static final ProofRewriteRule ARITH_STRING_PRED_SAFE_APPROX
public static final ProofRewriteRule BETA_REDUCE
Node.substitute.public static final ProofRewriteRule ARRAYS_EQ_RANGE_EXPAND
public static final ProofRewriteRule EXISTS_ELIM
public static final ProofRewriteRule QUANT_UNUSED_VARS
public static final ProofRewriteRule QUANT_MERGE_PRENEX
public static final ProofRewriteRule QUANT_MINISCOPE
public static final ProofRewriteRule MACRO_QUANT_PARTITION_CONNECTED_FV
public static final ProofRewriteRule DT_INST
public static final ProofRewriteRule DT_COLLAPSE_SELECTOR
public static final ProofRewriteRule DT_COLLAPSE_TESTER
public static final ProofRewriteRule DT_COLLAPSE_TESTER_SINGLETON
public static final ProofRewriteRule DT_CONS_EQ
public static final ProofRewriteRule BV_UMULO_ELIMINATE
public static final ProofRewriteRule BV_SMULO_ELIMINATE
public static final ProofRewriteRule BV_ADD_COMBINE_LIKE_TERMS
public static final ProofRewriteRule BV_MULT_SIMPLIFY
public static final ProofRewriteRule BV_BITWISE_SLICING
public static final ProofRewriteRule RE_LOOP_ELIM
public static final ProofRewriteRule RE_INTER_UNION_INCLUSION
public static final ProofRewriteRule STR_IN_RE_EVAL
public static final ProofRewriteRule STR_IN_RE_CONSUME
public static final ProofRewriteRule STR_IN_RE_CONCAT_STAR_CHAR
public static final ProofRewriteRule STR_IN_RE_SIGMA
public static final ProofRewriteRule STR_IN_RE_SIGMA_STAR
public static final ProofRewriteRule MACRO_SUBSTR_STRIP_SYM_LENGTH
public static final ProofRewriteRule SETS_IS_EMPTY_EVAL
public static final ProofRewriteRule ARITH_PLUS_ZERO
public static final ProofRewriteRule ARITH_MUL_ONE
public static final ProofRewriteRule ARITH_MUL_ZERO
public static final ProofRewriteRule ARITH_DIV_TOTAL
public static final ProofRewriteRule ARITH_INT_DIV_TOTAL
public static final ProofRewriteRule ARITH_INT_DIV_TOTAL_ONE
public static final ProofRewriteRule ARITH_INT_DIV_TOTAL_ZERO
public static final ProofRewriteRule ARITH_INT_MOD_TOTAL
public static final ProofRewriteRule ARITH_INT_MOD_TOTAL_ONE
public static final ProofRewriteRule ARITH_INT_MOD_TOTAL_ZERO
public static final ProofRewriteRule ARITH_NEG_NEG_ONE
public static final ProofRewriteRule ARITH_ELIM_UMINUS
public static final ProofRewriteRule ARITH_ELIM_MINUS
public static final ProofRewriteRule ARITH_ELIM_GT
public static final ProofRewriteRule ARITH_ELIM_LT
public static final ProofRewriteRule ARITH_ELIM_INT_GT
public static final ProofRewriteRule ARITH_ELIM_INT_LT
public static final ProofRewriteRule ARITH_ELIM_LEQ
public static final ProofRewriteRule ARITH_LEQ_NORM
public static final ProofRewriteRule ARITH_GEQ_TIGHTEN
public static final ProofRewriteRule ARITH_GEQ_NORM1
public static final ProofRewriteRule ARITH_GEQ_NORM2
public static final ProofRewriteRule ARITH_REFL_LEQ
public static final ProofRewriteRule ARITH_REFL_LT
public static final ProofRewriteRule ARITH_REFL_GEQ
public static final ProofRewriteRule ARITH_REFL_GT
public static final ProofRewriteRule ARITH_REAL_EQ_ELIM
public static final ProofRewriteRule ARITH_INT_EQ_ELIM
public static final ProofRewriteRule ARITH_PLUS_FLATTEN
public static final ProofRewriteRule ARITH_MULT_FLATTEN
public static final ProofRewriteRule ARITH_MULT_DIST
public static final ProofRewriteRule ARITH_PLUS_CANCEL1
public static final ProofRewriteRule ARITH_PLUS_CANCEL2
public static final ProofRewriteRule ARITH_ABS_ELIM
public static final ProofRewriteRule ARITH_TO_REAL_ELIM
public static final ProofRewriteRule ARITH_TO_INT_ELIM_TO_REAL
public static final ProofRewriteRule ARITH_DIV_ELIM_TO_REAL1
public static final ProofRewriteRule ARITH_DIV_ELIM_TO_REAL2
public static final ProofRewriteRule ARRAY_READ_OVER_WRITE
public static final ProofRewriteRule ARRAY_READ_OVER_WRITE2
public static final ProofRewriteRule ARRAY_STORE_OVERWRITE
public static final ProofRewriteRule ARRAY_STORE_SELF
public static final ProofRewriteRule BOOL_DOUBLE_NOT_ELIM
public static final ProofRewriteRule BOOL_NOT_TRUE
public static final ProofRewriteRule BOOL_NOT_FALSE
public static final ProofRewriteRule BOOL_EQ_TRUE
public static final ProofRewriteRule BOOL_EQ_FALSE
public static final ProofRewriteRule BOOL_EQ_NREFL
public static final ProofRewriteRule BOOL_IMPL_FALSE1
public static final ProofRewriteRule BOOL_IMPL_FALSE2
public static final ProofRewriteRule BOOL_IMPL_TRUE1
public static final ProofRewriteRule BOOL_IMPL_TRUE2
public static final ProofRewriteRule BOOL_IMPL_ELIM
public static final ProofRewriteRule BOOL_OR_TRUE
public static final ProofRewriteRule BOOL_OR_FALSE
public static final ProofRewriteRule BOOL_OR_FLATTEN
public static final ProofRewriteRule BOOL_OR_DUP
public static final ProofRewriteRule BOOL_AND_TRUE
public static final ProofRewriteRule BOOL_AND_FALSE
public static final ProofRewriteRule BOOL_AND_FLATTEN
public static final ProofRewriteRule BOOL_AND_DUP
public static final ProofRewriteRule BOOL_AND_CONF
public static final ProofRewriteRule BOOL_OR_TAUT
public static final ProofRewriteRule BOOL_OR_DE_MORGAN
public static final ProofRewriteRule BOOL_IMPLIES_DE_MORGAN
public static final ProofRewriteRule BOOL_AND_DE_MORGAN
public static final ProofRewriteRule BOOL_XOR_REFL
public static final ProofRewriteRule BOOL_XOR_NREFL
public static final ProofRewriteRule BOOL_XOR_FALSE
public static final ProofRewriteRule BOOL_XOR_TRUE
public static final ProofRewriteRule BOOL_XOR_COMM
public static final ProofRewriteRule BOOL_XOR_ELIM
public static final ProofRewriteRule BOOL_NOT_XOR_ELIM
public static final ProofRewriteRule BOOL_NOT_EQ_ELIM
public static final ProofRewriteRule ITE_NEG_BRANCH
public static final ProofRewriteRule ITE_THEN_TRUE
public static final ProofRewriteRule ITE_ELSE_FALSE
public static final ProofRewriteRule ITE_THEN_FALSE
public static final ProofRewriteRule ITE_ELSE_TRUE
public static final ProofRewriteRule ITE_THEN_LOOKAHEAD_SELF
public static final ProofRewriteRule ITE_ELSE_LOOKAHEAD_SELF
public static final ProofRewriteRule BOOL_NOT_ITE_ELIM
public static final ProofRewriteRule ITE_TRUE_COND
public static final ProofRewriteRule ITE_FALSE_COND
public static final ProofRewriteRule ITE_NOT_COND
public static final ProofRewriteRule ITE_EQ_BRANCH
public static final ProofRewriteRule ITE_THEN_LOOKAHEAD
public static final ProofRewriteRule ITE_ELSE_LOOKAHEAD
public static final ProofRewriteRule ITE_THEN_NEG_LOOKAHEAD
public static final ProofRewriteRule ITE_ELSE_NEG_LOOKAHEAD
public static final ProofRewriteRule BV_CONCAT_FLATTEN
public static final ProofRewriteRule BV_CONCAT_EXTRACT_MERGE
public static final ProofRewriteRule BV_EXTRACT_EXTRACT
public static final ProofRewriteRule BV_EXTRACT_WHOLE
public static final ProofRewriteRule BV_EXTRACT_CONCAT_1
public static final ProofRewriteRule BV_EXTRACT_CONCAT_2
public static final ProofRewriteRule BV_EXTRACT_CONCAT_3
public static final ProofRewriteRule BV_EXTRACT_CONCAT_4
public static final ProofRewriteRule BV_EXTRACT_BITWISE_AND
public static final ProofRewriteRule BV_EXTRACT_BITWISE_OR
public static final ProofRewriteRule BV_EXTRACT_BITWISE_XOR
public static final ProofRewriteRule BV_EXTRACT_NOT
public static final ProofRewriteRule BV_EXTRACT_SIGN_EXTEND_1
public static final ProofRewriteRule BV_EXTRACT_SIGN_EXTEND_2
public static final ProofRewriteRule BV_EXTRACT_SIGN_EXTEND_3
public static final ProofRewriteRule BV_NEG_MULT
public static final ProofRewriteRule BV_NEG_ADD
public static final ProofRewriteRule BV_MULT_DISTRIB_CONST_NEG
public static final ProofRewriteRule BV_MULT_DISTRIB_CONST_ADD
public static final ProofRewriteRule BV_MULT_DISTRIB_CONST_SUB
public static final ProofRewriteRule BV_MULT_DISTRIB_1
public static final ProofRewriteRule BV_MULT_DISTRIB_2
public static final ProofRewriteRule BV_NOT_XOR
public static final ProofRewriteRule BV_AND_SIMPLIFY_1
public static final ProofRewriteRule BV_AND_SIMPLIFY_2
public static final ProofRewriteRule BV_OR_SIMPLIFY_1
public static final ProofRewriteRule BV_OR_SIMPLIFY_2
public static final ProofRewriteRule BV_XOR_SIMPLIFY_1
public static final ProofRewriteRule BV_XOR_SIMPLIFY_2
public static final ProofRewriteRule BV_XOR_SIMPLIFY_3
public static final ProofRewriteRule BV_ULT_ADD_ONE
public static final ProofRewriteRule BV_CONCAT_TO_MULT
public static final ProofRewriteRule BV_MULT_SLT_MULT_1
public static final ProofRewriteRule BV_MULT_SLT_MULT_2
public static final ProofRewriteRule BV_COMMUTATIVE_AND
public static final ProofRewriteRule BV_COMMUTATIVE_OR
public static final ProofRewriteRule BV_COMMUTATIVE_XOR
public static final ProofRewriteRule BV_COMMUTATIVE_MUL
public static final ProofRewriteRule BV_OR_ZERO
public static final ProofRewriteRule BV_MUL_ONE
public static final ProofRewriteRule BV_MUL_ZERO
public static final ProofRewriteRule BV_ADD_ZERO
public static final ProofRewriteRule BV_ADD_TWO
public static final ProofRewriteRule BV_ZERO_EXTEND_ELIMINATE_0
public static final ProofRewriteRule BV_SIGN_EXTEND_ELIMINATE_0
public static final ProofRewriteRule BV_NOT_NEQ
public static final ProofRewriteRule BV_ULT_ONES
public static final ProofRewriteRule BV_OR_FLATTEN
public static final ProofRewriteRule BV_XOR_FLATTEN
public static final ProofRewriteRule BV_AND_FLATTEN
public static final ProofRewriteRule BV_MUL_FLATTEN
public static final ProofRewriteRule BV_CONCAT_MERGE_CONST
public static final ProofRewriteRule BV_COMMUTATIVE_ADD
public static final ProofRewriteRule BV_NEG_SUB
public static final ProofRewriteRule BV_NEG_IDEMP
public static final ProofRewriteRule BV_SUB_ELIMINATE
public static final ProofRewriteRule BV_UGT_ELIMINATE
public static final ProofRewriteRule BV_UGE_ELIMINATE
public static final ProofRewriteRule BV_SGT_ELIMINATE
public static final ProofRewriteRule BV_SGE_ELIMINATE
public static final ProofRewriteRule BV_SLT_ELIMINATE
public static final ProofRewriteRule BV_SLE_ELIMINATE
public static final ProofRewriteRule BV_REDOR_ELIMINATE
public static final ProofRewriteRule BV_REDAND_ELIMINATE
public static final ProofRewriteRule BV_ULE_ELIMINATE
public static final ProofRewriteRule BV_COMP_ELIMINATE
public static final ProofRewriteRule BV_REPEAT_ELIMINATE_1
public static final ProofRewriteRule BV_REPEAT_ELIMINATE_2
public static final ProofRewriteRule BV_ROTATE_LEFT_ELIMINATE_1
public static final ProofRewriteRule BV_ROTATE_LEFT_ELIMINATE_2
public static final ProofRewriteRule BV_ROTATE_RIGHT_ELIMINATE_1
public static final ProofRewriteRule BV_ROTATE_RIGHT_ELIMINATE_2
public static final ProofRewriteRule BV_NAND_ELIMINATE
public static final ProofRewriteRule BV_NOR_ELIMINATE
public static final ProofRewriteRule BV_XNOR_ELIMINATE
public static final ProofRewriteRule BV_SDIV_ELIMINATE
public static final ProofRewriteRule BV_SDIV_ELIMINATE_FEWER_BITWISE_OPS
public static final ProofRewriteRule BV_ZERO_EXTEND_ELIMINATE
public static final ProofRewriteRule BV_SIGN_EXTEND_ELIMINATE
public static final ProofRewriteRule BV_UADDO_ELIMINATE
public static final ProofRewriteRule BV_SADDO_ELIMINATE
public static final ProofRewriteRule BV_SDIVO_ELIMINATE
public static final ProofRewriteRule BV_SMOD_ELIMINATE
public static final ProofRewriteRule BV_SMOD_ELIMINATE_FEWER_BITWISE_OPS
public static final ProofRewriteRule BV_SREM_ELIMINATE
public static final ProofRewriteRule BV_SREM_ELIMINATE_FEWER_BITWISE_OPS
public static final ProofRewriteRule BV_USUBO_ELIMINATE
public static final ProofRewriteRule BV_SSUBO_ELIMINATE
public static final ProofRewriteRule BV_ITE_EQUAL_CHILDREN
public static final ProofRewriteRule BV_ITE_CONST_CHILDREN_1
public static final ProofRewriteRule BV_ITE_CONST_CHILDREN_2
public static final ProofRewriteRule BV_ITE_EQUAL_COND_1
public static final ProofRewriteRule BV_ITE_EQUAL_COND_2
public static final ProofRewriteRule BV_ITE_EQUAL_COND_3
public static final ProofRewriteRule BV_ITE_MERGE_THEN_IF
public static final ProofRewriteRule BV_ITE_MERGE_ELSE_IF
public static final ProofRewriteRule BV_ITE_MERGE_THEN_ELSE
public static final ProofRewriteRule BV_ITE_MERGE_ELSE_ELSE
public static final ProofRewriteRule BV_SHL_BY_CONST_0
public static final ProofRewriteRule BV_SHL_BY_CONST_1
public static final ProofRewriteRule BV_SHL_BY_CONST_2
public static final ProofRewriteRule BV_LSHR_BY_CONST_0
public static final ProofRewriteRule BV_LSHR_BY_CONST_1
public static final ProofRewriteRule BV_LSHR_BY_CONST_2
public static final ProofRewriteRule BV_ASHR_BY_CONST_0
public static final ProofRewriteRule BV_ASHR_BY_CONST_1
public static final ProofRewriteRule BV_ASHR_BY_CONST_2
public static final ProofRewriteRule BV_AND_CONCAT_PULLUP
public static final ProofRewriteRule BV_OR_CONCAT_PULLUP
public static final ProofRewriteRule BV_XOR_CONCAT_PULLUP
public static final ProofRewriteRule BV_BITWISE_IDEMP_1
public static final ProofRewriteRule BV_BITWISE_IDEMP_2
public static final ProofRewriteRule BV_AND_ZERO
public static final ProofRewriteRule BV_AND_ONE
public static final ProofRewriteRule BV_OR_ONE
public static final ProofRewriteRule BV_XOR_DUPLICATE
public static final ProofRewriteRule BV_XOR_ONES
public static final ProofRewriteRule BV_XOR_ZERO
public static final ProofRewriteRule BV_BITWISE_NOT_AND
public static final ProofRewriteRule BV_BITWISE_NOT_OR
public static final ProofRewriteRule BV_XOR_NOT
public static final ProofRewriteRule BV_NOT_IDEMP
public static final ProofRewriteRule BV_ULT_ZERO_1
public static final ProofRewriteRule BV_ULT_ZERO_2
public static final ProofRewriteRule BV_ULT_SELF
public static final ProofRewriteRule BV_LT_SELF
public static final ProofRewriteRule BV_ULE_SELF
public static final ProofRewriteRule BV_ULE_ZERO
public static final ProofRewriteRule BV_ZERO_ULE
public static final ProofRewriteRule BV_SLE_SELF
public static final ProofRewriteRule BV_ULE_MAX
public static final ProofRewriteRule BV_NOT_ULT
public static final ProofRewriteRule BV_NOT_ULE
public static final ProofRewriteRule BV_NOT_SLE
public static final ProofRewriteRule BV_MULT_POW2_1
public static final ProofRewriteRule BV_MULT_POW2_2
public static final ProofRewriteRule BV_MULT_POW2_2B
public static final ProofRewriteRule BV_EXTRACT_MULT_LEADING_BIT
public static final ProofRewriteRule BV_UDIV_POW2_NOT_ONE
public static final ProofRewriteRule BV_UDIV_ZERO
public static final ProofRewriteRule BV_UDIV_ONE
public static final ProofRewriteRule BV_UREM_POW2_NOT_ONE
public static final ProofRewriteRule BV_UREM_ONE
public static final ProofRewriteRule BV_UREM_SELF
public static final ProofRewriteRule BV_SHL_ZERO
public static final ProofRewriteRule BV_LSHR_ZERO
public static final ProofRewriteRule BV_ASHR_ZERO
public static final ProofRewriteRule BV_UGT_UREM
public static final ProofRewriteRule BV_ULT_ONE
public static final ProofRewriteRule BV_SLT_ZERO
public static final ProofRewriteRule BV_MERGE_SIGN_EXTEND_1
public static final ProofRewriteRule BV_MERGE_SIGN_EXTEND_2
public static final ProofRewriteRule BV_MERGE_SIGN_EXTEND_3
public static final ProofRewriteRule BV_SIGN_EXTEND_EQ_CONST_1
public static final ProofRewriteRule BV_SIGN_EXTEND_EQ_CONST_2
public static final ProofRewriteRule BV_ZERO_EXTEND_EQ_CONST_1
public static final ProofRewriteRule BV_ZERO_EXTEND_EQ_CONST_2
public static final ProofRewriteRule BV_ZERO_EXTEND_ULT_CONST_1
public static final ProofRewriteRule BV_ZERO_EXTEND_ULT_CONST_2
public static final ProofRewriteRule BV_SIGN_EXTEND_ULT_CONST_1
public static final ProofRewriteRule BV_SIGN_EXTEND_ULT_CONST_2
public static final ProofRewriteRule BV_SIGN_EXTEND_ULT_CONST_3
public static final ProofRewriteRule BV_SIGN_EXTEND_ULT_CONST_4
public static final ProofRewriteRule SETS_EQ_SINGLETON_EMP
public static final ProofRewriteRule SETS_MEMBER_SINGLETON
public static final ProofRewriteRule SETS_MEMBER_EMP
public static final ProofRewriteRule SETS_SUBSET_ELIM
public static final ProofRewriteRule SETS_UNION_COMM
public static final ProofRewriteRule SETS_INTER_COMM
public static final ProofRewriteRule SETS_INTER_EMP1
public static final ProofRewriteRule SETS_INTER_EMP2
public static final ProofRewriteRule SETS_MINUS_EMP1
public static final ProofRewriteRule SETS_MINUS_EMP2
public static final ProofRewriteRule SETS_UNION_EMP1
public static final ProofRewriteRule SETS_UNION_EMP2
public static final ProofRewriteRule SETS_INTER_MEMBER
public static final ProofRewriteRule SETS_MINUS_MEMBER
public static final ProofRewriteRule SETS_UNION_MEMBER
public static final ProofRewriteRule SETS_CHOOSE_SINGLETON
public static final ProofRewriteRule SETS_CARD_SINGLETON
public static final ProofRewriteRule SETS_CARD_UNION
public static final ProofRewriteRule SETS_CARD_MINUS
public static final ProofRewriteRule SETS_CARD_EMP
public static final ProofRewriteRule STR_EQ_CTN_FALSE
public static final ProofRewriteRule STR_EQ_CTN_FULL_FALSE1
public static final ProofRewriteRule STR_EQ_CTN_FULL_FALSE2
public static final ProofRewriteRule STR_CONCAT_FLATTEN
public static final ProofRewriteRule STR_CONCAT_FLATTEN_EQ
public static final ProofRewriteRule STR_CONCAT_FLATTEN_EQ_REV
public static final ProofRewriteRule STR_SUBSTR_EMPTY_STR
public static final ProofRewriteRule STR_SUBSTR_EMPTY_RANGE
public static final ProofRewriteRule STR_SUBSTR_EMPTY_START
public static final ProofRewriteRule STR_SUBSTR_EMPTY_START_NEG
public static final ProofRewriteRule STR_SUBSTR_EQ_EMPTY
public static final ProofRewriteRule STR_LEN_REPLACE_INV
public static final ProofRewriteRule STR_LEN_UPDATE_INV
public static final ProofRewriteRule STR_LEN_SUBSTR_IN_RANGE
public static final ProofRewriteRule STR_LEN_SUBSTR_UB1
public static final ProofRewriteRule STR_LEN_SUBSTR_UB2
public static final ProofRewriteRule STR_CONCAT_CLASH
public static final ProofRewriteRule STR_CONCAT_CLASH_REV
public static final ProofRewriteRule STR_CONCAT_CLASH2
public static final ProofRewriteRule STR_CONCAT_CLASH2_REV
public static final ProofRewriteRule STR_CONCAT_UNIFY
public static final ProofRewriteRule STR_CONCAT_UNIFY_REV
public static final ProofRewriteRule STR_CONCAT_UNIFY_BASE
public static final ProofRewriteRule STR_CONCAT_UNIFY_BASE_REV
public static final ProofRewriteRule STR_CONCAT_CLASH_CHAR
public static final ProofRewriteRule STR_CONCAT_CLASH_CHAR_REV
public static final ProofRewriteRule STR_PREFIXOF_ELIM
public static final ProofRewriteRule STR_SUFFIXOF_ELIM
public static final ProofRewriteRule STR_PREFIXOF_ONE
public static final ProofRewriteRule STR_SUFFIXOF_ONE
public static final ProofRewriteRule STR_SUBSTR_COMBINE1
public static final ProofRewriteRule STR_SUBSTR_COMBINE2
public static final ProofRewriteRule STR_SUBSTR_COMBINE3
public static final ProofRewriteRule STR_SUBSTR_COMBINE4
public static final ProofRewriteRule STR_SUBSTR_CONCAT1
public static final ProofRewriteRule STR_SUBSTR_CONCAT2
public static final ProofRewriteRule STR_SUBSTR_FULL
public static final ProofRewriteRule STR_SUBSTR_FULL_EQ
public static final ProofRewriteRule STR_CONTAINS_REFL
public static final ProofRewriteRule STR_CONTAINS_CONCAT_FIND
public static final ProofRewriteRule STR_CONTAINS_SPLIT_CHAR
public static final ProofRewriteRule STR_CONTAINS_LT_LEN
public static final ProofRewriteRule STR_CONTAINS_LEQ_LEN_EQ
public static final ProofRewriteRule STR_CONTAINS_EMP
public static final ProofRewriteRule STR_CONTAINS_IS_EMP
public static final ProofRewriteRule STR_CONCAT_EMP
public static final ProofRewriteRule STR_AT_ELIM
public static final ProofRewriteRule STR_REPLACE_SELF
public static final ProofRewriteRule STR_REPLACE_NO_CONTAINS
public static final ProofRewriteRule STR_REPLACE_EMPTY
public static final ProofRewriteRule STR_LEN_CONCAT_REC
public static final ProofRewriteRule STR_INDEXOF_SELF
public static final ProofRewriteRule STR_INDEXOF_NO_CONTAINS
public static final ProofRewriteRule STR_TO_LOWER_CONCAT
public static final ProofRewriteRule STR_TO_UPPER_CONCAT
public static final ProofRewriteRule STR_TO_LOWER_UPPER
public static final ProofRewriteRule STR_TO_UPPER_LOWER
public static final ProofRewriteRule RE_ALL_ELIM
public static final ProofRewriteRule RE_OPT_ELIM
public static final ProofRewriteRule RE_DIFF_ELIM
public static final ProofRewriteRule RE_CONCAT_EMP
public static final ProofRewriteRule RE_CONCAT_NONE
public static final ProofRewriteRule RE_CONCAT_FLATTEN
public static final ProofRewriteRule RE_CONCAT_STAR_SWAP
public static final ProofRewriteRule RE_CONCAT_MERGE
public static final ProofRewriteRule RE_UNION_ALL
public static final ProofRewriteRule RE_UNION_NONE
public static final ProofRewriteRule RE_UNION_FLATTEN
public static final ProofRewriteRule RE_UNION_DUP
public static final ProofRewriteRule RE_INTER_ALL
public static final ProofRewriteRule RE_INTER_NONE
public static final ProofRewriteRule RE_INTER_FLATTEN
public static final ProofRewriteRule RE_INTER_DUP
public static final ProofRewriteRule RE_LOOP_NEG
public static final ProofRewriteRule RE_INTER_CSTRING
public static final ProofRewriteRule RE_INTER_CSTRING_NEG
public static final ProofRewriteRule STR_NTH_ELIM_CODE
public static final ProofRewriteRule STR_SUBSTR_LEN_INCLUDE
public static final ProofRewriteRule STR_SUBSTR_LEN_INCLUDE_PRE
public static final ProofRewriteRule STR_SUBSTR_LEN_SKIP
public static final ProofRewriteRule SEQ_REV_CONCAT
public static final ProofRewriteRule SEQ_LEN_UNIT
public static final ProofRewriteRule SEQ_NTH_UNIT
public static final ProofRewriteRule SEQ_REV_UNIT
public static final ProofRewriteRule RE_IN_EMPTY
public static final ProofRewriteRule RE_IN_SIGMA
public static final ProofRewriteRule RE_IN_SIGMA_STAR
public static final ProofRewriteRule RE_IN_CSTRING
public static final ProofRewriteRule RE_IN_COMP
public static final ProofRewriteRule STR_IN_RE_UNION_ELIM
public static final ProofRewriteRule STR_IN_RE_INTER_ELIM
public static final ProofRewriteRule STR_IN_RE_RANGE_ELIM
public static final ProofRewriteRule STR_IN_RE_CONTAINS
public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX
public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_NEG
public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_SR_SINGLE
public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_SR_SINGLE_NEG
public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_SRS_SINGLE
public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_SRS_SINGLE_NEG
public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_S_SINGLE
public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_S_SINGLE_NEG
public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_BASE
public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_BASE_NEG
public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE
public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE_NEG
public static final ProofRewriteRule STR_IN_RE_STRIP_CHAR
public static final ProofRewriteRule STR_IN_RE_STRIP_CHAR_S_SINGLE
public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_REV
public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_NEG_REV
public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_SR_SINGLE_REV
public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_SR_SINGLE_NEG_REV
public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_SRS_SINGLE_REV
public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_SRS_SINGLE_NEG_REV
public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_S_SINGLE_REV
public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_S_SINGLE_NEG_REV
public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_BASE_REV
public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_BASE_NEG_REV
public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE_REV
public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE_NEG_REV
public static final ProofRewriteRule STR_IN_RE_STRIP_CHAR_REV
public static final ProofRewriteRule STR_IN_RE_STRIP_CHAR_S_SINGLE_REV
public static final ProofRewriteRule STR_IN_RE_REQ_UNFOLD
public static final ProofRewriteRule STR_IN_RE_REQ_UNFOLD_REV
public static final ProofRewriteRule STR_IN_RE_SKIP_UNFOLD
public static final ProofRewriteRule STR_IN_RE_SKIP_UNFOLD_REV
public static final ProofRewriteRule STR_IN_RE_TEST_UNFOLD
public static final ProofRewriteRule STR_IN_RE_TEST_UNFOLD_REV
public static final ProofRewriteRule EQ_REFL
public static final ProofRewriteRule EQ_SYMM
public static final ProofRewriteRule DISTINCT_BINARY_ELIM
public static final ProofRewriteRule UF_BV2NAT_GEQ_ELIM
public static ProofRewriteRule[] values()
for (ProofRewriteRule c : ProofRewriteRule.values()) System.out.println(c);
public static ProofRewriteRule valueOf(String name)
name - the name of the enum constant to be returned.IllegalArgumentException - if this enum type has no constant with the specified nameNullPointerException - if the argument is nullpublic static ProofRewriteRule fromInt(int value) throws CVC5ApiException
CVC5ApiExceptionpublic int getValue()