+Enum Constants
+
+| Enum Constant |
+Description |
+
+
+ARITH_ABS_ELIM_INT |
+
+ Auto-generated from RARE rule arith-abs-elim-int
+ |
+
+
+ARITH_ABS_ELIM_REAL |
+
+ Auto-generated from RARE rule arith-abs-elim-real
+ |
+
+
+ARITH_ABS_EQ |
+
+ Auto-generated from RARE rule arith-abs-eq
+ |
+
+
+ARITH_ABS_INT_GT |
+
+ Auto-generated from RARE rule arith-abs-int-gt
+ |
+
+
+ARITH_ABS_REAL_GT |
+
+ Auto-generated from RARE rule arith-abs-real-gt
+ |
+
+
+ARITH_COSECENT_ELIM |
+
+ Auto-generated from RARE rule arith-cosecent-elim
+ |
+
+
+ARITH_COSINE_ELIM |
+
+ Auto-generated from RARE rule arith-cosine-elim
+ |
+
+
+ARITH_COTANGENT_ELIM |
+
+ Auto-generated from RARE rule arith-cotangent-elim
+ |
+
+
+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_INT |
+
+ Auto-generated from RARE rule arith-div-total-int
+ |
+
+
+ARITH_DIV_TOTAL_REAL |
+
+ Auto-generated from RARE rule arith-div-total-real
+ |
+
+
+ARITH_DIV_TOTAL_ZERO_INT |
+
+ Auto-generated from RARE rule arith-div-total-zero-int
+ |
+
+
+ARITH_DIV_TOTAL_ZERO_REAL |
+
+ Auto-generated from RARE rule arith-div-total-zero-real
+ |
+
+
+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_EQ_ELIM_INT |
+
+ Auto-generated from RARE rule arith-eq-elim-int
+ |
+
+
+ARITH_EQ_ELIM_REAL |
+
+ Auto-generated from RARE rule arith-eq-elim-real
+ |
+
+
+ARITH_GEQ_NORM1_INT |
+
+ Auto-generated from RARE rule arith-geq-norm1-int
+ |
+
+
+ARITH_GEQ_NORM1_REAL |
+
+ Auto-generated from RARE rule arith-geq-norm1-real
+ |
+
+
+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_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_PI_NOT_INT |
+
+ Auto-generated from RARE rule arith-pi-not-int
+ |
+
+
+ARITH_PLUS_FLATTEN |
+
+ Auto-generated from RARE rule arith-plus-flatten
+ |
+
+
+ARITH_POW_ELIM |
+
+ Arithmetic – power elimination
+
+ \[
+ (x ^ c) = (x \cdot \ldots \cdot x)
+ \]
+ where \(c\) is a non-negative integer.
+ |
+
+
+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_SECENT_ELIM |
+
+ Auto-generated from RARE rule arith-secent-elim
+ |
+
+
+ARITH_SINE_PI2 |
+
+ Auto-generated from RARE rule arith-sine-pi2
+ |
+
+
+ARITH_SINE_ZERO |
+
+ Auto-generated from RARE rule arith-sine-zero
+ |
+
+
+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_TANGENT_ELIM |
+
+ Auto-generated from RARE rule arith-tangent-elim
+ |
+
+
+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_WRITE_SPLIT |
+
+ Auto-generated from RARE rule array-read-over-write-split
+ |
+
+
+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.\> i \leq x \leq j \rightarrow
+ \mathit{select}(a,x)=\mathit{select}(b,x)
+ \]
+ |
+
+
+ARRAYS_SELECT_CONST |
+
+ Arrays – Constant array select
+
+ \[
+ (select A x) = c
+ \]
+ where \(A\) is a constant array storing element \(c\).
+ |
+
+
+BETA_REDUCE |
+
+ Equality – Beta reduction
+
+ \[
+ ((\lambda x_1 \ldots x_n.\> t) \ t_1 \ldots t_n) = t\{x_1 \mapsto t_1,
+ \ldots, x_n \mapsto t_n\}
+ \]
+ The right hand side of the equality in the conclusion is computed using
+ standard substitution via Node.substitute.
+ |
+
+
+BOOL_AND_CONF |
+
+ Auto-generated from RARE rule boolean-and-conf
+ |
+
+
+BOOL_AND_CONF2 |
+
+ Auto-generated from RARE rule boolean-and-conf2
+ |
+
+
+BOOL_AND_DE_MORGAN |
+
+ Auto-generated from RARE rule boolean-and-de-morgan
+ |
+
+
+BOOL_AND_FALSE |
+
+ Auto-generated from RARE rule boolean-and-false
+ |
+
+
+BOOL_AND_FLATTEN |
+
+ Auto-generated from RARE rule boolean-and-flatten
+ |
+
+
+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_ELIM1 |
+
+ Auto-generated from RARE rule boolean-not-eq-elim1
+ |
+
+
+BOOL_NOT_EQ_ELIM2 |
+
+ Auto-generated from RARE rule boolean-not-eq-elim2
+ |
+
+
+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_AND_DISTRIB |
+
+ Auto-generated from RARE rule boolean-or-and-distrib
+ |
+
+
+BOOL_OR_DE_MORGAN |
+
+ Auto-generated from RARE rule boolean-or-de-morgan
+ |
+
+
+BOOL_OR_FLATTEN |
+
+ Auto-generated from RARE rule boolean-or-flatten
+ |
+
+
+BOOL_OR_TAUT |
+
+ Auto-generated from RARE rule boolean-or-taut
+ |
+
+
+BOOL_OR_TAUT2 |
+
+ Auto-generated from RARE rule boolean-or-taut2
+ |
+
+
+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) ...
+ |
+
+
+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_EQ_EXTRACT_ELIM1 |
+
+ Auto-generated from RARE rule bv-eq-extract-elim1
+ |
+
+
+BV_EQ_EXTRACT_ELIM2 |
+
+ Auto-generated from RARE rule bv-eq-extract-elim2
+ |
+
+
+BV_EQ_EXTRACT_ELIM3 |
+
+ Auto-generated from RARE rule bv-eq-extract-elim3
+ |
+
+
+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_ELIM |
+
+ Bitvectors – Extract continuous substrings of bitvectors
+
+ \[
+ repeat(n,\ t) = concat(t ...
+ |
+
+
+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_TO_NAT_ELIM |
+
+ UF – Bitvector to natural elimination
+
+ \[
+ \texttt{bv2nat}(t) = t_1 + \ldots + t_n
+ \]
+ where for \(i=1, \ldots, n\), \(t_i\) is
+ \(\texttt{ite}(x[i-1, i-1] = 1, 2^i, 0)\).
+ |
+
+
+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_ULE |
+
+ Auto-generated from RARE rule bv-zero-ule
+ |
+
+
+DISTINCT_BINARY_ELIM |
+
+ Auto-generated from RARE rule distinct-binary-elim
+ |
+
+
+DISTINCT_CARD_CONFLICT |
+
+ Builtin – Distinct cardinality conflict
+
+ \[
+ \texttt{distinct}(t_1, \ldots, tn) = \bot
+ \]
+ where \(n\) is greater than the cardinality of the type of
+ \(t_1, \ldots, t_n\).
+ |
+
+
+DISTINCT_ELIM |
+
+ Builtin – Distinct elimination
+
+ \[
+ \texttt{distinct}(t_1, t_2) = \neg (t_1 = t2)
+ \]
+ if \(n = 2\), or
+
+ \[
+ \texttt{distinct}(t_1, \ldots, tn) = \bigwedge_{i=1}^n \bigwedge_{j=i+1}^n t_i \neq t_j
+ \]
+ if \(n > 2\)
+ |
+
+
+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_COLLAPSE_UPDATER |
+
+ Datatypes – collapse tester
+
+ \[
+ u_{c,i}(c(t_1, \ldots, t_i, \ldots, t_n), s) = c(t_1, \ldots, s, \ldots, t_n)
+ \]
+ or alternatively
+
+ \[
+ u_{c,i}(d(t_1, \ldots, t_n), s) = d(t_1, \ldots, t_n)
+ \]
+ where \(c\) and \(d\) are distinct constructors.
+ |
+
+
+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_CYCLE |
+
+ Datatypes – cycle
+
+ \[
+ (x = t[x]) = \bot
+ \]
+ where all terms on the path to \(x\) in \(t[x]\) are applications
+ of constructors, and this path is non-empty.
+ |
+
+
+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\).
+ |
+
+
+DT_MATCH_ELIM |
+
+ Datatypes – match elimination
+
+ \[
+ \texttt{match}(t ((p_1 c_1) \ldots (p_n c_n))) = \texttt{ite}(F_1, r_1, \texttt{ite}( \ldots, r_n))
+ \]
+ where for \(i=1, \ldots, n\), \(F_1\) is a formula that holds iff
+ \(t\) matches \(p_i\) and \(r_i\) is the result of a
+ substitution on \(c_i\) based on this match.
+ |
+
+
+DT_UPDATER_ELIM |
+
+ Datatypes - updater elimination
+
+ \[
+ u_{c,i}(t, s) = ite(\mathit{is}_c(t), c(s_0(t), \ldots, s, \ldots s_n(t)), t)
+ \]
+ where \(s_i\) is the \(i^{th}\) selector for constructor \(c\).
+ |
+
+
+EQ_COND_DEQ |
+
+ Auto-generated from RARE rule eq-cond-deq
+ |
+
+
+EQ_ITE_LIFT |
+
+ Auto-generated from RARE rule eq-ite-lift
+ |
+
+
+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.\> F = \neg \forall x_1\dots x_n.\> \neg F
+ \]
+ |
+
+
+INT_TO_BV_ELIM |
+
+ UF – Integer to bitvector elimination
+
+ \[
+ \texttt{int2bv}_n(t) = (bvconcat t_1 \ldots t_n)
+ \]
+ where for \(i=1, \ldots, n\), \(t_i\) is
+ \(\texttt{ite}(\texttt{mod}(t,2^n) \geq 2^{n-1}, 1, 0)\).
+ |
+
+
+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_NOT_SELF |
+
+ Auto-generated from RARE rule ite-else-lookahead-not-self
+ |
+
+
+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_EXPAND |
+
+ Auto-generated from RARE rule ite-expand
+ |
+
+
+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_NOT_SELF |
+
+ Auto-generated from RARE rule ite-then-lookahead-not-self
+ |
+
+
+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
+ |
+
+
+LAMBDA_ELIM |
+
+ Equality – Lambda elimination
+
+ \[
+ (\lambda x_1 \ldots x_n.\> f(x_1 \ldots x_n)) = f
+ \]
+ |
+
+
+MACRO_ARITH_STRING_PRED_ENTAIL |
+
+ Arithmetic – strings predicate entailment
+
+ \[
+ (= s t) = c
+ \]
+ \[
+ (>= s t) = c
+ \]
+ where \(c\) is a Boolean constant.
+ |
+
+
+MACRO_ARRAYS_DISTINCT_ARRAYS |
+
+ Arrays – Macro distinct arrays
+
+ \[
+ (A = B) = \bot
+ \]
+ where \(A\) and \(B\) are distinct array values, that is,
+ the Node.isConst method returns true for both.
+ |
+
+
+MACRO_ARRAYS_NORMALIZE_CONSTANT |
+
+ Arrays – Macro normalize constant
+
+ \[
+ A = B
+ \]
+ where \(B\) is the result of normalizing the array value \(A\)
+ into a canonical form, using the internal method
+ TheoryArraysRewriter.normalizeConstant.
+ |
+
+
+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_MERGE_PRENEX |
+
+ Quantifiers – Macro merge prenex
+
+ \[
+ \forall X_1.\> \ldots \forall X_n.\> F = \forall X.\> F
+ \]
+ where \(X_1 \ldots X_n\) are lists of variables and \(X\) is the
+ result of removing duplicates from \(X_1 \ldots X_n\).
+ |
+
+
+MACRO_QUANT_MINISCOPE |
+
+ Quantifiers – Macro miniscoping
+
+ \[
+ \forall X.\> F_1 \wedge \cdots \wedge F_n =
+ G_1 \wedge \cdots \wedge G_n
+ \]
+ where each \(G_i\) is semantically equivalent to
+ \(\forall X.\> F_i\), or alternatively
+
+ \[
+ \forall X.\> \ite{C}{F_1}{F_2} = \ite{C}{G_1}{G_2}
+ \]
+ where \(C\) does not have any free variable in \(X\).
+ |
+
+
+MACRO_QUANT_PARTITION_CONNECTED_FV |
+
+ Quantifiers – Macro connected free variable partitioning
+
+ \[
+ \forall X.\> F_1 \vee \ldots \vee F_n =
+ (\forall X_1.\> F_{1,1} \vee \ldots \vee F_{1,k_1}) \vee \ldots \vee
+ (\forall X_m.\> F_{m,1} \vee \ldots \vee F_{m,k_m})
+ \]
+ where \(X_1, \ldots, X_m\) is a partition of \(X\).
+ |
+
+
+MACRO_QUANT_PRENEX |
+
+ Quantifiers – Macro prenex
+
+ \[
+ (\forall X.\> F_1 \vee \cdots \vee (\forall Y.\> F_i) \vee \cdots \vee F_n) = (\forall X Z.\> F_1 \vee \cdots \vee F_i\{ Y \mapsto Z \} \vee \cdots \vee F_n)
+ \]
+ |
+
+
+MACRO_QUANT_REWRITE_BODY |
+
+ Quantifiers – Macro quantifiers rewrite body
+
+ \[
+ \forall X.\> F = \forall X.\> G
+ \]
+ where \(G\) is semantically equivalent to \(F\).
+ |
+
+
+MACRO_QUANT_VAR_ELIM_EQ |
+
+ Quantifiers – Macro variable elimination equality
+
+ \[
+ \forall x Y.\> F = \forall Y.\> F \{ x \mapsto t \}
+ \]
+ where \(\neg F\) entails \(x = t\).
+ |
+
+
+MACRO_QUANT_VAR_ELIM_INEQ |
+
+ Quantifiers – Macro variable elimination inequality
+
+ \[
+ \forall x Y.\> F = \forall Y.\> G
+ \]
+ where \(G\) is the result of replacing all literals containing
+ \(x\) with a constant.
+ |
+
+
+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_DT_SPLIT |
+
+ Quantifiers – Datatypes Split
+
+ \[
+ (\forall x Y.\> F) = (\forall X_1 Y.
+ |
+
+
+QUANT_MERGE_PRENEX |
+
+ Quantifiers – Merge prenex
+
+ \[
+ \forall X_1.\> \ldots \forall X_n.\> F = \forall X_1 \ldots X_n.\> F
+ \]
+ where \(X_1 \ldots X_n\) are lists of variables.
+ |
+
+
+QUANT_MINISCOPE_AND |
+
+ Quantifiers – Miniscoping and
+
+ \[
+ \forall X.\> F_1 \wedge \ldots \wedge F_n =
+ (\forall X.\> F_1) \wedge \ldots \wedge (\forall X.\> F_n)
+ \]
+ |
+
+
+QUANT_MINISCOPE_ITE |
+
+ Quantifiers – Miniscoping ite
+
+ \[
+ \forall X.\> \ite{C}{F_1}{F_2} = \ite{C}{\forall X.\> F_1}{\forall X.\> F_2}
+ \]
+ where \(C\) does not have any free variable in \(X\).
+ |
+
+
+QUANT_MINISCOPE_OR |
+
+ Quantifiers – Miniscoping or
+
+ \[
+ \forall X.\> F_1 \vee \ldots \vee F_n = (\forall X_1.\> F_1) \vee \ldots \vee (\forall X_n.\> F_n)
+ \]
+ where \(X = X_1 \ldots X_n\), and the right hand side does not have any
+ free variable in \(X\).
+ |
+
+
+QUANT_UNUSED_VARS |
+
+ Quantifiers – Unused variables
+
+ \[
+ \forall X.\> F = \forall X_1.\> F
+ \]
+ where \(X_1\) is the subset of \(X\) that appear free in \(F\)
+ and \(X_1\) does not contain duplicate variables.
+ |
+
+
+QUANT_VAR_ELIM_EQ |
+
+ Quantifiers – Macro variable elimination equality
+
+ ..
+ |
+
+
+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_REPEAT |
+
+ Auto-generated from RARE rule re-concat-star-repeat
+ |
+
+
+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_STAR_NONE |
+
+ Auto-generated from RARE rule re-star-none
+ |
+
+
+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_EMPTY |
+
+ Auto-generated from RARE rule seq-len-empty
+ |
+
+
+SEQ_LEN_REV |
+
+ Auto-generated from RARE rule seq-len-rev
+ |
+
+
+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_REV |
+
+ Auto-generated from RARE rule seq-rev-rev
+ |
+
+
+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_INSERT_ELIM |
+
+ Sets – sets insert elimination
+
+ \[
+ \mathit{sets.insert}(t_1, \ldots, t_n, S) = \texttt{set.union}(\texttt{sets.singleton}(t_1), \ldots, \texttt{sets.singleton}(t_n), S)
+ \]
+ |
+
+
+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_ELIM |
+
+ Auto-generated from RARE rule sets-is-empty-elim
+ |
+
+
+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_MINUS_SELF |
+
+ Auto-generated from RARE rule sets-minus-self
+ |
+
+
+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_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}.\text{++}(s_1, \ldots, s_n), \mathit{re}.\text{*}(R)) =\\ \mathit{str.in\_re}(s_1, \mathit{re}.\text{*}(R)) \wedge \ldots \wedge \mathit{str.in\_re}(s_n, \mathit{re}.\text{*}(R))
+ \]
+ where all strings in \(R\) have length one.
+ |
+
+
+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}.\text{++}(\mathit{re.allchar}, \ldots, \mathit{re.allchar})) = (\mathit{str.len}(s) = n)
+ \]
+ or alternatively:
+
+ \[
+ \mathit{str.in\_re}(s, \mathit{re}.\text{++}(\mathit{re.allchar}, \ldots, \mathit{re.allchar}, \mathit{re}.\text{*}(\mathit{re.allchar}))) = (\mathit{str.len}(s) \ge n)
+ \]
+ |
+
+
+STR_IN_RE_SIGMA_STAR |
+
+ Strings – string in regular expression sigma star
+
+ \[
+ \mathit{str.in\_re}(s, \mathit{re}.\text{*}(\mathit{re}.\text{++}(\mathit{re.allchar}, \ldots, \mathit{re.allchar}))) = (\mathit{str.len}(s) \ \% \ n = 0)
+ \]
+ where \(n\) is the number of \(\mathit{re.allchar}\) arguments to
+ \(\mathit{re}.\text{++}\).
+ |
+
+
+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_CONTAINS_PRE |
+
+ Auto-generated from RARE rule str-indexof-contains-pre
+ |
+
+
+STR_INDEXOF_NO_CONTAINS |
+
+ Auto-generated from RARE rule str-indexof-no-contains
+ |
+
+
+STR_INDEXOF_RE_NONE |
+
+ Auto-generated from RARE rule str-indexof-re-none
+ |
+
+
+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_LEQ_CONCAT_FALSE |
+
+ Auto-generated from RARE rule str-leq-concat-false
+ |
+
+
+STR_LEQ_CONCAT_TRUE |
+
+ Auto-generated from RARE rule str-leq-concat-true
+ |
+
+
+STR_LEQ_EMPTY |
+
+ Auto-generated from RARE rule str-leq-empty
+ |
+
+
+STR_LEQ_EMPTY_EQ |
+
+ Auto-generated from RARE rule str-leq-empty-eq
+ |
+
+
+STR_LT_ELIM |
+
+ Auto-generated from RARE rule str-lt-elim
+ |
+
+
+STR_PREFIXOF_ELIM |
+
+ Auto-generated from RARE rule str-prefixof-elim
+ |
+
+
+STR_PREFIXOF_ONE |
+
+ Auto-generated from RARE rule str-prefixof-one
+ |
+
+
+STR_REPLACE_ALL_NO_CONTAINS |
+
+ Auto-generated from RARE rule str-replace-all-no-contains
+ |
+
+
+STR_REPLACE_CONTAINS_PRE |
+
+ Auto-generated from RARE rule str-replace-contains-pre
+ |
+
+
+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_PREFIX |
+
+ Auto-generated from RARE rule str-replace-prefix
+ |
+
+
+STR_REPLACE_RE_ALL_NONE |
+
+ Auto-generated from RARE rule str-replace-re-all-none
+ |
+
+
+STR_REPLACE_RE_NONE |
+
+ Auto-generated from RARE rule str-replace-re-none
+ |
+
+
+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_INT_CONCAT_NEG_ONE |
+
+ Auto-generated from RARE rule str-to-int-concat-neg-one
+ |
+
+
+STR_TO_LOWER_CONCAT |
+
+ Auto-generated from RARE rule str-to-lower-concat
+ |
+
+
+STR_TO_LOWER_FROM_INT |
+
+ Auto-generated from RARE rule str-to-lower-from-int
+ |
+
+
+STR_TO_LOWER_LEN |
+
+ Auto-generated from RARE rule str-to-lower-len
+ |
+
+
+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_FROM_INT |
+
+ Auto-generated from RARE rule str-to-upper-from-int
+ |
+
+
+STR_TO_UPPER_LEN |
+
+ Auto-generated from RARE rule str-to-upper-len
+ |
+
+
+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
+ |
+
+
+UF_BV2NAT_INT2BV |
+
+ Auto-generated from RARE rule uf-bv2nat-int2bv
+ |
+
+
+UF_BV2NAT_INT2BV_EXTEND |
+
+ Auto-generated from RARE rule uf-bv2nat-int2bv-extend
+ |
+
+
+UF_BV2NAT_INT2BV_EXTRACT |
+
+ Auto-generated from RARE rule uf-bv2nat-int2bv-extract
+ |
+
+
+UF_INT2BV_BV2NAT |
+
+ Auto-generated from RARE rule uf-int2bv-bv2nat
+ |
+
+
+UF_INT2BV_BVULE_EQUIV |
+
+ Auto-generated from RARE rule uf-int2bv-bvule-equiv
+ |
+
+
+UF_INT2BV_BVULT_EQUIV |
+
+ Auto-generated from RARE rule uf-int2bv-bvult-equiv
+ |
+
+
+