Package io.github.cvc5
Enum ProofRewriteRule
- java.lang.Object
-
- java.lang.Enum<ProofRewriteRule>
-
- io.github.cvc5.ProofRewriteRule
-
- All Implemented Interfaces:
java.io.Serializable,java.lang.Comparable<ProofRewriteRule>
public enum ProofRewriteRule extends java.lang.Enum<ProofRewriteRule>
-
-
Enum Constant Summary
Enum Constants Enum Constant Description ARITH_ABS_ELIM_INTAuto-generated from RARE rule arith-abs-elim-intARITH_ABS_ELIM_REALAuto-generated from RARE rule arith-abs-elim-realARITH_ABS_EQAuto-generated from RARE rule arith-abs-eqARITH_ABS_INT_GTAuto-generated from RARE rule arith-abs-int-gtARITH_ABS_REAL_GTAuto-generated from RARE rule arith-abs-real-gtARITH_COSECENT_ELIMAuto-generated from RARE rule arith-cosecent-elimARITH_COSINE_ELIMAuto-generated from RARE rule arith-cosine-elimARITH_COTANGENT_ELIMAuto-generated from RARE rule arith-cotangent-elimARITH_DIV_ELIM_TO_REAL1Auto-generated from RARE rule arith-div-elim-to-real1ARITH_DIV_ELIM_TO_REAL2Auto-generated from RARE rule arith-div-elim-to-real2ARITH_DIV_TOTAL_INTAuto-generated from RARE rule arith-div-total-intARITH_DIV_TOTAL_REALAuto-generated from RARE rule arith-div-total-realARITH_DIV_TOTAL_ZERO_INTAuto-generated from RARE rule arith-div-total-zero-intARITH_DIV_TOTAL_ZERO_REALAuto-generated from RARE rule arith-div-total-zero-realARITH_ELIM_GTAuto-generated from RARE rule arith-elim-gtARITH_ELIM_INT_GTAuto-generated from RARE rule arith-elim-int-gtARITH_ELIM_INT_LTAuto-generated from RARE rule arith-elim-int-ltARITH_ELIM_LEQAuto-generated from RARE rule arith-elim-leqARITH_ELIM_LTAuto-generated from RARE rule arith-elim-ltARITH_EQ_ELIM_INTAuto-generated from RARE rule arith-eq-elim-intARITH_EQ_ELIM_REALAuto-generated from RARE rule arith-eq-elim-realARITH_GEQ_NORM1_INTAuto-generated from RARE rule arith-geq-norm1-intARITH_GEQ_NORM1_REALAuto-generated from RARE rule arith-geq-norm1-realARITH_GEQ_NORM2Auto-generated from RARE rule arith-geq-norm2ARITH_GEQ_TIGHTENAuto-generated from RARE rule arith-geq-tightenARITH_INT_DIV_TOTALAuto-generated from RARE rule arith-int-div-totalARITH_INT_DIV_TOTAL_ONEAuto-generated from RARE rule arith-int-div-total-oneARITH_INT_DIV_TOTAL_ZEROAuto-generated from RARE rule arith-int-div-total-zeroARITH_INT_MOD_TOTALAuto-generated from RARE rule arith-int-mod-totalARITH_INT_MOD_TOTAL_ONEAuto-generated from RARE rule arith-int-mod-total-oneARITH_INT_MOD_TOTAL_ZEROAuto-generated from RARE rule arith-int-mod-total-zeroARITH_LEQ_NORMAuto-generated from RARE rule arith-leq-normARITH_MUL_ONEAuto-generated from RARE rule arith-mul-oneARITH_MUL_ZEROAuto-generated from RARE rule arith-mul-zeroARITH_MULT_DISTAuto-generated from RARE rule arith-mult-distARITH_MULT_FLATTENAuto-generated from RARE rule arith-mult-flattenARITH_PI_NOT_INTAuto-generated from RARE rule arith-pi-not-intARITH_PLUS_FLATTENAuto-generated from RARE rule arith-plus-flattenARITH_POW_ELIMArithmetic – power elimination \[ (x ^ c) = (x \cdot \ldots \cdot x) \] where \(c\) is a non-negative integer.ARITH_REFL_GEQAuto-generated from RARE rule arith-refl-geqARITH_REFL_GTAuto-generated from RARE rule arith-refl-gtARITH_REFL_LEQAuto-generated from RARE rule arith-refl-leqARITH_REFL_LTAuto-generated from RARE rule arith-refl-ltARITH_SECENT_ELIMAuto-generated from RARE rule arith-secent-elimARITH_SINE_PI2Auto-generated from RARE rule arith-sine-pi2ARITH_SINE_ZEROAuto-generated from RARE rule arith-sine-zeroARITH_STRING_PRED_ENTAILArithmetic – 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_APPROXArithmetic – 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_ELIMAuto-generated from RARE rule arith-tangent-elimARITH_TO_INT_ELIM_TO_REALAuto-generated from RARE rule arith-to-int-elim-to-realARITH_TO_REAL_ELIMAuto-generated from RARE rule arith-to-real-elimARRAY_READ_OVER_WRITEAuto-generated from RARE rule array-read-over-writeARRAY_READ_OVER_WRITE_SPLITAuto-generated from RARE rule array-read-over-write-splitARRAY_READ_OVER_WRITE2Auto-generated from RARE rule array-read-over-write2ARRAY_STORE_OVERWRITEAuto-generated from RARE rule array-store-overwriteARRAY_STORE_SELFAuto-generated from RARE rule array-store-selfARRAYS_EQ_RANGE_EXPANDArrays – 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_CONSTArrays – Constant array select \[ (select A x) = c \] where \(A\) is a constant array storing element \(c\).BETA_REDUCEEquality – 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 viaNode.substitute.BOOL_AND_CONFAuto-generated from RARE rule boolean-and-confBOOL_AND_CONF2Auto-generated from RARE rule boolean-and-conf2BOOL_AND_DE_MORGANAuto-generated from RARE rule boolean-and-de-morganBOOL_AND_FALSEAuto-generated from RARE rule boolean-and-falseBOOL_AND_FLATTENAuto-generated from RARE rule boolean-and-flattenBOOL_DOUBLE_NOT_ELIMAuto-generated from RARE rule boolean-double-not-elimBOOL_EQ_FALSEAuto-generated from RARE rule boolean-eq-falseBOOL_EQ_NREFLAuto-generated from RARE rule boolean-eq-nreflBOOL_EQ_TRUEAuto-generated from RARE rule boolean-eq-trueBOOL_IMPL_ELIMAuto-generated from RARE rule boolean-impl-elimBOOL_IMPL_FALSE1Auto-generated from RARE rule boolean-impl-false1BOOL_IMPL_FALSE2Auto-generated from RARE rule boolean-impl-false2BOOL_IMPL_TRUE1Auto-generated from RARE rule boolean-impl-true1BOOL_IMPL_TRUE2Auto-generated from RARE rule boolean-impl-true2BOOL_IMPLIES_DE_MORGANAuto-generated from RARE rule boolean-implies-de-morganBOOL_NOT_EQ_ELIM1Auto-generated from RARE rule boolean-not-eq-elim1BOOL_NOT_EQ_ELIM2Auto-generated from RARE rule boolean-not-eq-elim2BOOL_NOT_FALSEAuto-generated from RARE rule boolean-not-falseBOOL_NOT_ITE_ELIMAuto-generated from RARE rule boolean-not-ite-elimBOOL_NOT_TRUEAuto-generated from RARE rule boolean-not-trueBOOL_NOT_XOR_ELIMAuto-generated from RARE rule boolean-not-xor-elimBOOL_OR_AND_DISTRIBAuto-generated from RARE rule boolean-or-and-distribBOOL_OR_DE_MORGANAuto-generated from RARE rule boolean-or-de-morganBOOL_OR_FLATTENAuto-generated from RARE rule boolean-or-flattenBOOL_OR_TAUTAuto-generated from RARE rule boolean-or-tautBOOL_OR_TAUT2Auto-generated from RARE rule boolean-or-taut2BOOL_OR_TRUEAuto-generated from RARE rule boolean-or-trueBOOL_XOR_COMMAuto-generated from RARE rule boolean-xor-commBOOL_XOR_ELIMAuto-generated from RARE rule boolean-xor-elimBOOL_XOR_FALSEAuto-generated from RARE rule boolean-xor-falseBOOL_XOR_NREFLAuto-generated from RARE rule boolean-xor-nreflBOOL_XOR_REFLAuto-generated from RARE rule boolean-xor-reflBOOL_XOR_TRUEAuto-generated from RARE rule boolean-xor-trueBV_ADD_COMBINE_LIKE_TERMSBitvectors – Combine like terms during addition by counting termsBV_ADD_TWOAuto-generated from RARE rule bv-add-twoBV_ADD_ZEROAuto-generated from RARE rule bv-add-zeroBV_AND_CONCAT_PULLUPAuto-generated from RARE rule bv-and-concat-pullupBV_AND_FLATTENAuto-generated from RARE rule bv-and-flattenBV_AND_ONEAuto-generated from RARE rule bv-and-oneBV_AND_SIMPLIFY_1Auto-generated from RARE rule bv-and-simplify-1BV_AND_SIMPLIFY_2Auto-generated from RARE rule bv-and-simplify-2BV_AND_ZEROAuto-generated from RARE rule bv-and-zeroBV_ASHR_BY_CONST_0Auto-generated from RARE rule bv-ashr-by--0BV_ASHR_BY_CONST_1Auto-generated from RARE rule bv-ashr-by--1BV_ASHR_BY_CONST_2Auto-generated from RARE rule bv-ashr-by--2BV_ASHR_ZEROAuto-generated from RARE rule bv-ashr-zeroBV_BITWISE_IDEMP_1Auto-generated from RARE rule bv-bitwise-idemp-1BV_BITWISE_IDEMP_2Auto-generated from RARE rule bv-bitwise-idemp-2BV_BITWISE_NOT_ANDAuto-generated from RARE rule bv-bitwise-not-andBV_BITWISE_NOT_ORAuto-generated from RARE rule bv-bitwise-not-orBV_BITWISE_SLICINGBitvectors – Extract continuous substrings of bitvectors \[ bvand(a,\ c) = concat(bvand(a[i_0:j_0],\ c_0) ...BV_COMMUTATIVE_ADDAuto-generated from RARE rule bv-commutative-addBV_COMMUTATIVE_ANDAuto-generated from RARE rule bv-commutative-andBV_COMMUTATIVE_MULAuto-generated from RARE rule bv-commutative-mulBV_COMMUTATIVE_ORAuto-generated from RARE rule bv-commutative-orBV_COMMUTATIVE_XORAuto-generated from RARE rule bv-commutative-xorBV_COMP_ELIMINATEAuto-generated from RARE rule bv-comp-eliminateBV_CONCAT_EXTRACT_MERGEAuto-generated from RARE rule bv-concat-extract-mergeBV_CONCAT_FLATTENAuto-generated from RARE rule bv-concat-flattenBV_CONCAT_MERGE_CONSTAuto-generated from RARE rule bv-concat-merge-BV_CONCAT_TO_MULTAuto-generated from RARE rule bv-concat-to-multBV_EQ_EXTRACT_ELIM1Auto-generated from RARE rule bv-eq-extract-elim1BV_EQ_EXTRACT_ELIM2Auto-generated from RARE rule bv-eq-extract-elim2BV_EQ_EXTRACT_ELIM3Auto-generated from RARE rule bv-eq-extract-elim3BV_EXTRACT_BITWISE_ANDAuto-generated from RARE rule bv-extract-bitwise-andBV_EXTRACT_BITWISE_ORAuto-generated from RARE rule bv-extract-bitwise-orBV_EXTRACT_BITWISE_XORAuto-generated from RARE rule bv-extract-bitwise-xorBV_EXTRACT_CONCAT_1Auto-generated from RARE rule bv-extract-concat-1BV_EXTRACT_CONCAT_2Auto-generated from RARE rule bv-extract-concat-2BV_EXTRACT_CONCAT_3Auto-generated from RARE rule bv-extract-concat-3BV_EXTRACT_CONCAT_4Auto-generated from RARE rule bv-extract-concat-4BV_EXTRACT_EXTRACTAuto-generated from RARE rule bv-extract-extractBV_EXTRACT_MULT_LEADING_BITAuto-generated from RARE rule bv-extract-mult-leading-bitBV_EXTRACT_NOTAuto-generated from RARE rule bv-extract-notBV_EXTRACT_SIGN_EXTEND_1Auto-generated from RARE rule bv-extract-sign-extend-1BV_EXTRACT_SIGN_EXTEND_2Auto-generated from RARE rule bv-extract-sign-extend-2BV_EXTRACT_SIGN_EXTEND_3Auto-generated from RARE rule bv-extract-sign-extend-3BV_EXTRACT_WHOLEAuto-generated from RARE rule bv-extract-wholeBV_ITE_CONST_CHILDREN_1Auto-generated from RARE rule bv-ite--children-1BV_ITE_CONST_CHILDREN_2Auto-generated from RARE rule bv-ite--children-2BV_ITE_EQUAL_CHILDRENAuto-generated from RARE rule bv-ite-equal-childrenBV_ITE_EQUAL_COND_1Auto-generated from RARE rule bv-ite-equal-cond-1BV_ITE_EQUAL_COND_2Auto-generated from RARE rule bv-ite-equal-cond-2BV_ITE_EQUAL_COND_3Auto-generated from RARE rule bv-ite-equal-cond-3BV_ITE_MERGE_ELSE_ELSEAuto-generated from RARE rule bv-ite-merge-else-elseBV_ITE_MERGE_ELSE_IFAuto-generated from RARE rule bv-ite-merge-else-ifBV_ITE_MERGE_THEN_ELSEAuto-generated from RARE rule bv-ite-merge-then-elseBV_ITE_MERGE_THEN_IFAuto-generated from RARE rule bv-ite-merge-then-ifBV_LSHR_BY_CONST_0Auto-generated from RARE rule bv-lshr-by--0BV_LSHR_BY_CONST_1Auto-generated from RARE rule bv-lshr-by--1BV_LSHR_BY_CONST_2Auto-generated from RARE rule bv-lshr-by--2BV_LSHR_ZEROAuto-generated from RARE rule bv-lshr-zeroBV_LT_SELFAuto-generated from RARE rule bv-lt-selfBV_MERGE_SIGN_EXTEND_1Auto-generated from RARE rule bv-merge-sign-extend-1BV_MERGE_SIGN_EXTEND_2Auto-generated from RARE rule bv-merge-sign-extend-2BV_MERGE_SIGN_EXTEND_3Auto-generated from RARE rule bv-merge-sign-extend-3BV_MUL_FLATTENAuto-generated from RARE rule bv-mul-flattenBV_MUL_ONEAuto-generated from RARE rule bv-mul-oneBV_MUL_ZEROAuto-generated from RARE rule bv-mul-zeroBV_MULT_DISTRIB_1Auto-generated from RARE rule bv-mult-distrib-1BV_MULT_DISTRIB_2Auto-generated from RARE rule bv-mult-distrib-2BV_MULT_DISTRIB_CONST_ADDAuto-generated from RARE rule bv-mult-distrib--addBV_MULT_DISTRIB_CONST_NEGAuto-generated from RARE rule bv-mult-distrib--negBV_MULT_DISTRIB_CONST_SUBAuto-generated from RARE rule bv-mult-distrib--subBV_MULT_POW2_1Auto-generated from RARE rule bv-mult-pow2-1BV_MULT_POW2_2Auto-generated from RARE rule bv-mult-pow2-2BV_MULT_POW2_2BAuto-generated from RARE rule bv-mult-pow2-2bBV_MULT_SIMPLIFYBitvectors – Extract negations from multiplicands \[ bvmul(bvneg(a),\ b,\ c) = bvneg(bvmul(a,\ b,\ c)) \]BV_MULT_SLT_MULT_1Auto-generated from RARE rule bv-mult-slt-mult-1BV_MULT_SLT_MULT_2Auto-generated from RARE rule bv-mult-slt-mult-2BV_NAND_ELIMINATEAuto-generated from RARE rule bv-nand-eliminateBV_NEG_ADDAuto-generated from RARE rule bv-neg-addBV_NEG_IDEMPAuto-generated from RARE rule bv-neg-idempBV_NEG_MULTAuto-generated from RARE rule bv-neg-multBV_NEG_SUBAuto-generated from RARE rule bv-neg-subBV_NOR_ELIMINATEAuto-generated from RARE rule bv-nor-eliminateBV_NOT_IDEMPAuto-generated from RARE rule bv-not-idempBV_NOT_NEQAuto-generated from RARE rule bv-not-neqBV_NOT_SLEAuto-generated from RARE rule bv-not-sleBV_NOT_ULEAuto-generated from RARE rule bv-not-uleBV_NOT_ULTAuto-generated from RARE rule bv-not-ultBV_NOT_XORAuto-generated from RARE rule bv-not-xorBV_OR_CONCAT_PULLUPAuto-generated from RARE rule bv-or-concat-pullupBV_OR_FLATTENAuto-generated from RARE rule bv-or-flattenBV_OR_ONEAuto-generated from RARE rule bv-or-oneBV_OR_SIMPLIFY_1Auto-generated from RARE rule bv-or-simplify-1BV_OR_SIMPLIFY_2Auto-generated from RARE rule bv-or-simplify-2BV_OR_ZEROAuto-generated from RARE rule bv-or-zeroBV_REDAND_ELIMINATEAuto-generated from RARE rule bv-redand-eliminateBV_REDOR_ELIMINATEAuto-generated from RARE rule bv-redor-eliminateBV_REPEAT_ELIMBitvectors – Extract continuous substrings of bitvectors \[ repeat(n,\ t) = concat(t ...BV_ROTATE_LEFT_ELIMINATE_1Auto-generated from RARE rule bv-rotate-left-eliminate-1BV_ROTATE_LEFT_ELIMINATE_2Auto-generated from RARE rule bv-rotate-left-eliminate-2BV_ROTATE_RIGHT_ELIMINATE_1Auto-generated from RARE rule bv-rotate-right-eliminate-1BV_ROTATE_RIGHT_ELIMINATE_2Auto-generated from RARE rule bv-rotate-right-eliminate-2BV_SADDO_ELIMINATEAuto-generated from RARE rule bv-saddo-eliminateBV_SDIV_ELIMINATEAuto-generated from RARE rule bv-sdiv-eliminateBV_SDIV_ELIMINATE_FEWER_BITWISE_OPSAuto-generated from RARE rule bv-sdiv-eliminate-fewer-bitwise-opsBV_SDIVO_ELIMINATEAuto-generated from RARE rule bv-sdivo-eliminateBV_SGE_ELIMINATEAuto-generated from RARE rule bv-sge-eliminateBV_SGT_ELIMINATEAuto-generated from RARE rule bv-sgt-eliminateBV_SHL_BY_CONST_0Auto-generated from RARE rule bv-shl-by--0BV_SHL_BY_CONST_1Auto-generated from RARE rule bv-shl-by--1BV_SHL_BY_CONST_2Auto-generated from RARE rule bv-shl-by--2BV_SHL_ZEROAuto-generated from RARE rule bv-shl-zeroBV_SIGN_EXTEND_ELIMINATEAuto-generated from RARE rule bv-sign-extend-eliminateBV_SIGN_EXTEND_ELIMINATE_0Auto-generated from RARE rule bv-sign-extend-eliminate-0BV_SIGN_EXTEND_EQ_CONST_1Auto-generated from RARE rule bv-sign-extend-eq--1BV_SIGN_EXTEND_EQ_CONST_2Auto-generated from RARE rule bv-sign-extend-eq--2BV_SIGN_EXTEND_ULT_CONST_1Auto-generated from RARE rule bv-sign-extend-ult--1BV_SIGN_EXTEND_ULT_CONST_2Auto-generated from RARE rule bv-sign-extend-ult--2BV_SIGN_EXTEND_ULT_CONST_3Auto-generated from RARE rule bv-sign-extend-ult--3BV_SIGN_EXTEND_ULT_CONST_4Auto-generated from RARE rule bv-sign-extend-ult--4BV_SLE_ELIMINATEAuto-generated from RARE rule bv-sle-eliminateBV_SLE_SELFAuto-generated from RARE rule bv-sle-selfBV_SLT_ELIMINATEAuto-generated from RARE rule bv-slt-eliminateBV_SLT_ZEROAuto-generated from RARE rule bv-slt-zeroBV_SMOD_ELIMINATEAuto-generated from RARE rule bv-smod-eliminateBV_SMOD_ELIMINATE_FEWER_BITWISE_OPSAuto-generated from RARE rule bv-smod-eliminate-fewer-bitwise-opsBV_SMULO_ELIMINATEBitvectors – Unsigned multiplication overflow detection elimination See M.Gok, M.J.BV_SREM_ELIMINATEAuto-generated from RARE rule bv-srem-eliminateBV_SREM_ELIMINATE_FEWER_BITWISE_OPSAuto-generated from RARE rule bv-srem-eliminate-fewer-bitwise-opsBV_SSUBO_ELIMINATEAuto-generated from RARE rule bv-ssubo-eliminateBV_SUB_ELIMINATEAuto-generated from RARE rule bv-sub-eliminateBV_TO_NAT_ELIMUF – 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_ELIMINATEAuto-generated from RARE rule bv-uaddo-eliminateBV_UDIV_ONEAuto-generated from RARE rule bv-udiv-oneBV_UDIV_POW2_NOT_ONEAuto-generated from RARE rule bv-udiv-pow2-not-oneBV_UDIV_ZEROAuto-generated from RARE rule bv-udiv-zeroBV_UGE_ELIMINATEAuto-generated from RARE rule bv-uge-eliminateBV_UGT_ELIMINATEAuto-generated from RARE rule bv-ugt-eliminateBV_UGT_UREMAuto-generated from RARE rule bv-ugt-uremBV_ULE_ELIMINATEAuto-generated from RARE rule bv-ule-eliminateBV_ULE_MAXAuto-generated from RARE rule bv-ule-maxBV_ULE_SELFAuto-generated from RARE rule bv-ule-selfBV_ULE_ZEROAuto-generated from RARE rule bv-ule-zeroBV_ULT_ADD_ONEAuto-generated from RARE rule bv-ult-add-oneBV_ULT_ONEAuto-generated from RARE rule bv-ult-oneBV_ULT_ONESAuto-generated from RARE rule bv-ult-onesBV_ULT_SELFAuto-generated from RARE rule bv-ult-selfBV_ULT_ZERO_1Auto-generated from RARE rule bv-ult-zero-1BV_ULT_ZERO_2Auto-generated from RARE rule bv-ult-zero-2BV_UMULO_ELIMINATEBitvectors – Unsigned multiplication overflow detection elimination See M.Gok, M.J.BV_UREM_ONEAuto-generated from RARE rule bv-urem-oneBV_UREM_POW2_NOT_ONEAuto-generated from RARE rule bv-urem-pow2-not-oneBV_UREM_SELFAuto-generated from RARE rule bv-urem-selfBV_USUBO_ELIMINATEAuto-generated from RARE rule bv-usubo-eliminateBV_XNOR_ELIMINATEAuto-generated from RARE rule bv-xnor-eliminateBV_XOR_CONCAT_PULLUPAuto-generated from RARE rule bv-xor-concat-pullupBV_XOR_DUPLICATEAuto-generated from RARE rule bv-xor-duplicateBV_XOR_FLATTENAuto-generated from RARE rule bv-xor-flattenBV_XOR_NOTAuto-generated from RARE rule bv-xor-notBV_XOR_ONESAuto-generated from RARE rule bv-xor-onesBV_XOR_SIMPLIFY_1Auto-generated from RARE rule bv-xor-simplify-1BV_XOR_SIMPLIFY_2Auto-generated from RARE rule bv-xor-simplify-2BV_XOR_SIMPLIFY_3Auto-generated from RARE rule bv-xor-simplify-3BV_XOR_ZEROAuto-generated from RARE rule bv-xor-zeroBV_ZERO_EXTEND_ELIMINATEAuto-generated from RARE rule bv-zero-extend-eliminateBV_ZERO_EXTEND_ELIMINATE_0Auto-generated from RARE rule bv-zero-extend-eliminate-0BV_ZERO_EXTEND_EQ_CONST_1Auto-generated from RARE rule bv-zero-extend-eq--1BV_ZERO_EXTEND_EQ_CONST_2Auto-generated from RARE rule bv-zero-extend-eq--2BV_ZERO_ULEAuto-generated from RARE rule bv-zero-uleDISTINCT_BINARY_ELIMAuto-generated from RARE rule distinct-binary-elimDISTINCT_CARD_CONFLICTBuiltin – 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_ELIMBuiltin – 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_SELECTORDatatypes – 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_TESTERDatatypes – 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_SINGLETONDatatypes – collapse tester \[ \mathit{is}_c(t) = true \] where \(c\) is the only constructor of its associated datatype.DT_COLLAPSE_UPDATERDatatypes – 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_EQDatatypes – 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) \] where \(c\) is a constructor.DT_CONS_EQ_CLASHDatatypes – constructor equality clash \[ (t = s) = false \] where \(t\) and \(s\) have subterms that occur in the same position (beneath constructor applications) that are distinct constructor applications.DT_CYCLEDatatypes – 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_INSTDatatypes – 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_ELIMDatatypes – 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_ELIMDatatypes - 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_DEQAuto-generated from RARE rule eq-cond-deqEQ_ITE_LIFTAuto-generated from RARE rule eq-ite-liftEQ_REFLAuto-generated from RARE rule eq-reflEQ_SYMMAuto-generated from RARE rule eq-symmEXISTS_ELIMQuantifiers – Exists elimination \[ \exists x_1\dots x_n.\> F = \neg \forall x_1\dots x_n.\> \neg F \]INT_TO_BV_ELIMUF – 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_FALSEAuto-generated from RARE rule ite-else-falseITE_ELSE_LOOKAHEADAuto-generated from RARE rule ite-else-lookaheadITE_ELSE_LOOKAHEAD_NOT_SELFAuto-generated from RARE rule ite-else-lookahead-not-selfITE_ELSE_LOOKAHEAD_SELFAuto-generated from RARE rule ite-else-lookahead-selfITE_ELSE_NEG_LOOKAHEADAuto-generated from RARE rule ite-else-neg-lookaheadITE_ELSE_TRUEAuto-generated from RARE rule ite-else-trueITE_EQ_BRANCHAuto-generated from RARE rule ite-eq-branchITE_EXPANDAuto-generated from RARE rule ite-expandITE_FALSE_CONDAuto-generated from RARE rule ite-false-condITE_NEG_BRANCHAuto-generated from RARE rule ite-neg-branchITE_NOT_CONDAuto-generated from RARE rule ite-not-condITE_THEN_FALSEAuto-generated from RARE rule ite-then-falseITE_THEN_LOOKAHEADAuto-generated from RARE rule ite-then-lookaheadITE_THEN_LOOKAHEAD_NOT_SELFAuto-generated from RARE rule ite-then-lookahead-not-selfITE_THEN_LOOKAHEAD_SELFAuto-generated from RARE rule ite-then-lookahead-selfITE_THEN_NEG_LOOKAHEADAuto-generated from RARE rule ite-then-neg-lookaheadITE_THEN_TRUEAuto-generated from RARE rule ite-then-trueITE_TRUE_CONDAuto-generated from RARE rule ite-true-condLAMBDA_ELIMEquality – Lambda elimination \[ (\lambda x_1 \ldots x_n.\> f(x_1 \ldots x_n)) = f \]MACRO_ARITH_STRING_PRED_ENTAILArithmetic – strings predicate entailment \[ (= s t) = c \] \[ (>= s t) = c \] where \(c\) is a Boolean constant.MACRO_ARRAYS_DISTINCT_ARRAYSArrays – 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_CONSTANTArrays – 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_NORMBooleans – 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_DT_CONS_EQDatatypes – Macro constructor equality \[ (t = s) = (t_1 = s_1 \wedge \ldots \wedge t_n = s_n) \] where \(t_1, \ldots, t_n\) and \(s_1, \ldots, s_n\) are subterms of \(t\) and \(s\) that occur at the same position respectively (beneath constructor applications), or alternatively \[ (t = s) = false \] where \(t\) and \(s\) have subterms that occur in the same position (beneath constructor applications) that are distinct.MACRO_QUANT_MERGE_PRENEXQuantifiers – 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_MINISCOPEQuantifiers – 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_FVQuantifiers – 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_PRENEXQuantifiers – 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_BODYQuantifiers – Macro quantifiers rewrite body \[ \forall X.\> F = \forall X.\> G \] where \(G\) is semantically equivalent to \(F\).MACRO_QUANT_VAR_ELIM_EQQuantifiers – Macro variable elimination equality \[ \forall x Y.\> F = \forall Y.\> F \{ x \mapsto t \} \] where \(\neg F\) entails \(x = t\).MACRO_QUANT_VAR_ELIM_INEQQuantifiers – 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_LENGTHStrings – 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\).NONEThis enumeration represents the rewrite rules used in a rewrite proof.QUANT_DT_SPLITQuantifiers – Datatypes Split \[ (\forall x Y.\> F) = (\forall X_1 Y.QUANT_MERGE_PRENEXQuantifiers – 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_ANDQuantifiers – Miniscoping and \[ \forall X.\> F_1 \wedge \ldots \wedge F_n = (\forall X.\> F_1) \wedge \ldots \wedge (\forall X.\> F_n) \]QUANT_MINISCOPE_ITEQuantifiers – 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_ORQuantifiers – 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_VARSQuantifiers – 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_EQQuantifiers – Macro variable elimination equality ..RE_ALL_ELIMAuto-generated from RARE rule re-all-elimRE_CONCAT_EMPAuto-generated from RARE rule re-concat-empRE_CONCAT_FLATTENAuto-generated from RARE rule re-concat-flattenRE_CONCAT_MERGEAuto-generated from RARE rule re-concat-mergeRE_CONCAT_NONEAuto-generated from RARE rule re-concat-noneRE_CONCAT_STAR_REPEATAuto-generated from RARE rule re-concat-star-repeatRE_CONCAT_STAR_SWAPAuto-generated from RARE rule re-concat-star-swapRE_DIFF_ELIMAuto-generated from RARE rule re-diff-elimRE_IN_COMPAuto-generated from RARE rule re-in-compRE_IN_CSTRINGAuto-generated from RARE rule re-in-cstringRE_IN_EMPTYAuto-generated from RARE rule re-in-emptyRE_IN_SIGMAAuto-generated from RARE rule re-in-sigmaRE_IN_SIGMA_STARAuto-generated from RARE rule re-in-sigma-starRE_INTER_ALLAuto-generated from RARE rule re-inter-allRE_INTER_CSTRINGAuto-generated from RARE rule re-inter-cstringRE_INTER_CSTRING_NEGAuto-generated from RARE rule re-inter-cstring-negRE_INTER_DUPAuto-generated from RARE rule re-inter-dupRE_INTER_FLATTENAuto-generated from RARE rule re-inter-flattenRE_INTER_NONEAuto-generated from RARE rule re-inter-noneRE_INTER_UNION_INCLUSIONStrings – 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_ELIMStrings – regular expression loop elimination \[ re.loop_{l,u}(R) = re.union(R^l, \ldots, R^u) \] where \(u \geq l\).RE_LOOP_NEGAuto-generated from RARE rule re-loop-negRE_OPT_ELIMAuto-generated from RARE rule re-opt-elimRE_STAR_NONEAuto-generated from RARE rule re-star-noneRE_UNION_ALLAuto-generated from RARE rule re-union-allRE_UNION_DUPAuto-generated from RARE rule re-union-dupRE_UNION_FLATTENAuto-generated from RARE rule re-union-flattenRE_UNION_NONEAuto-generated from RARE rule re-union-noneSEQ_LEN_EMPTYAuto-generated from RARE rule seq-len-emptySEQ_LEN_REVAuto-generated from RARE rule seq-len-revSEQ_LEN_UNITAuto-generated from RARE rule seq-len-unitSEQ_NTH_UNITAuto-generated from RARE rule seq-nth-unitSEQ_REV_CONCATAuto-generated from RARE rule seq-rev-concatSEQ_REV_REVAuto-generated from RARE rule seq-rev-revSEQ_REV_UNITAuto-generated from RARE rule seq-rev-unitSETS_CARD_EMPAuto-generated from RARE rule sets-card-empSETS_CARD_MINUSAuto-generated from RARE rule sets-card-minusSETS_CARD_SINGLETONAuto-generated from RARE rule sets-card-singletonSETS_CARD_UNIONAuto-generated from RARE rule sets-card-unionSETS_CHOOSE_SINGLETONAuto-generated from RARE rule sets-choose-singletonSETS_EQ_SINGLETON_EMPAuto-generated from RARE rule sets-eq-singleton-empSETS_INSERT_ELIMSets – 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_COMMAuto-generated from RARE rule sets-inter-commSETS_INTER_EMP1Auto-generated from RARE rule sets-inter-emp1SETS_INTER_EMP2Auto-generated from RARE rule sets-inter-emp2SETS_INTER_MEMBERAuto-generated from RARE rule sets-inter-memberSETS_IS_EMPTY_ELIMAuto-generated from RARE rule sets-is-empty-elimSETS_IS_EMPTY_EVALSets – 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_EMPAuto-generated from RARE rule sets-member-empSETS_MEMBER_SINGLETONAuto-generated from RARE rule sets-member-singletonSETS_MINUS_EMP1Auto-generated from RARE rule sets-minus-emp1SETS_MINUS_EMP2Auto-generated from RARE rule sets-minus-emp2SETS_MINUS_MEMBERAuto-generated from RARE rule sets-minus-memberSETS_MINUS_SELFAuto-generated from RARE rule sets-minus-selfSETS_SUBSET_ELIMAuto-generated from RARE rule sets-subset-elimSETS_UNION_COMMAuto-generated from RARE rule sets-union-commSETS_UNION_EMP1Auto-generated from RARE rule sets-union-emp1SETS_UNION_EMP2Auto-generated from RARE rule sets-union-emp2SETS_UNION_MEMBERAuto-generated from RARE rule sets-union-memberSTR_AT_ELIMAuto-generated from RARE rule str-at-elimSTR_CONCAT_CLASHAuto-generated from RARE rule str-concat-clashSTR_CONCAT_CLASH_CHARAuto-generated from RARE rule str-concat-clash-charSTR_CONCAT_CLASH_CHAR_REVAuto-generated from RARE rule str-concat-clash-char-revSTR_CONCAT_CLASH_REVAuto-generated from RARE rule str-concat-clash-revSTR_CONCAT_CLASH2Auto-generated from RARE rule str-concat-clash2STR_CONCAT_CLASH2_REVAuto-generated from RARE rule str-concat-clash2-revSTR_CONCAT_FLATTENAuto-generated from RARE rule str-concat-flattenSTR_CONCAT_FLATTEN_EQAuto-generated from RARE rule str-concat-flatten-eqSTR_CONCAT_FLATTEN_EQ_REVAuto-generated from RARE rule str-concat-flatten-eq-revSTR_CONCAT_UNIFYAuto-generated from RARE rule str-concat-unifySTR_CONCAT_UNIFY_BASEAuto-generated from RARE rule str-concat-unify-baseSTR_CONCAT_UNIFY_BASE_REVAuto-generated from RARE rule str-concat-unify-base-revSTR_CONCAT_UNIFY_REVAuto-generated from RARE rule str-concat-unify-revSTR_CONTAINS_CONCAT_FINDAuto-generated from RARE rule str-contains-concat-findSTR_CONTAINS_EMPAuto-generated from RARE rule str-contains-empSTR_CONTAINS_IS_EMPAuto-generated from RARE rule str-contains-is-empSTR_CONTAINS_LEQ_LEN_EQAuto-generated from RARE rule str-contains-leq-len-eqSTR_CONTAINS_LT_LENAuto-generated from RARE rule str-contains-lt-lenSTR_CONTAINS_REFLAuto-generated from RARE rule str-contains-reflSTR_CONTAINS_SPLIT_CHARAuto-generated from RARE rule str-contains-split-charSTR_EQ_CTN_FALSEAuto-generated from RARE rule str-eq-ctn-falseSTR_EQ_CTN_FULL_FALSE1Auto-generated from RARE rule str-eq-ctn-full-false1STR_EQ_CTN_FULL_FALSE2Auto-generated from RARE rule str-eq-ctn-full-false2STR_IN_RE_CONCAT_STAR_CHARStrings – 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_CONSUMEStrings – 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_CONTAINSAuto-generated from RARE rule str-in-re-containsSTR_IN_RE_EVALStrings – 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_ELIMAuto-generated from RARE rule str-in-re-inter-elimSTR_IN_RE_RANGE_ELIMAuto-generated from RARE rule str-in-re-range-elimSTR_IN_RE_REQ_UNFOLDAuto-generated from RARE rule str-in-re-req-unfoldSTR_IN_RE_REQ_UNFOLD_REVAuto-generated from RARE rule str-in-re-req-unfold-revSTR_IN_RE_SIGMAStrings – 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_STARStrings – 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_UNFOLDAuto-generated from RARE rule str-in-re-skip-unfoldSTR_IN_RE_SKIP_UNFOLD_REVAuto-generated from RARE rule str-in-re-skip-unfold-revSTR_IN_RE_STRIP_CHARAuto-generated from RARE rule str-in-re-strip-charSTR_IN_RE_STRIP_CHAR_REVAuto-generated from RARE rule str-in-re-strip-char-revSTR_IN_RE_STRIP_CHAR_S_SINGLEAuto-generated from RARE rule str-in-re-strip-char-s-singleSTR_IN_RE_STRIP_CHAR_S_SINGLE_REVAuto-generated from RARE rule str-in-re-strip-char-s-single-revSTR_IN_RE_STRIP_PREFIXAuto-generated from RARE rule str-in-re-strip-prefixSTR_IN_RE_STRIP_PREFIX_BASEAuto-generated from RARE rule str-in-re-strip-prefix-baseSTR_IN_RE_STRIP_PREFIX_BASE_NEGAuto-generated from RARE rule str-in-re-strip-prefix-base-negSTR_IN_RE_STRIP_PREFIX_BASE_NEG_REVAuto-generated from RARE rule str-in-re-strip-prefix-base-neg-revSTR_IN_RE_STRIP_PREFIX_BASE_REVAuto-generated from RARE rule str-in-re-strip-prefix-base-revSTR_IN_RE_STRIP_PREFIX_BASE_S_SINGLEAuto-generated from RARE rule str-in-re-strip-prefix-base-s-singleSTR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE_NEGAuto-generated from RARE rule str-in-re-strip-prefix-base-s-single-negSTR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE_NEG_REVAuto-generated from RARE rule str-in-re-strip-prefix-base-s-single-neg-revSTR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE_REVAuto-generated from RARE rule str-in-re-strip-prefix-base-s-single-revSTR_IN_RE_STRIP_PREFIX_NEGAuto-generated from RARE rule str-in-re-strip-prefix-negSTR_IN_RE_STRIP_PREFIX_NEG_REVAuto-generated from RARE rule str-in-re-strip-prefix-neg-revSTR_IN_RE_STRIP_PREFIX_REVAuto-generated from RARE rule str-in-re-strip-prefix-revSTR_IN_RE_STRIP_PREFIX_S_SINGLEAuto-generated from RARE rule str-in-re-strip-prefix-s-singleSTR_IN_RE_STRIP_PREFIX_S_SINGLE_NEGAuto-generated from RARE rule str-in-re-strip-prefix-s-single-negSTR_IN_RE_STRIP_PREFIX_S_SINGLE_NEG_REVAuto-generated from RARE rule str-in-re-strip-prefix-s-single-neg-revSTR_IN_RE_STRIP_PREFIX_S_SINGLE_REVAuto-generated from RARE rule str-in-re-strip-prefix-s-single-revSTR_IN_RE_STRIP_PREFIX_SR_SINGLEAuto-generated from RARE rule str-in-re-strip-prefix-sr-singleSTR_IN_RE_STRIP_PREFIX_SR_SINGLE_NEGAuto-generated from RARE rule str-in-re-strip-prefix-sr-single-negSTR_IN_RE_STRIP_PREFIX_SR_SINGLE_NEG_REVAuto-generated from RARE rule str-in-re-strip-prefix-sr-single-neg-revSTR_IN_RE_STRIP_PREFIX_SR_SINGLE_REVAuto-generated from RARE rule str-in-re-strip-prefix-sr-single-revSTR_IN_RE_STRIP_PREFIX_SRS_SINGLEAuto-generated from RARE rule str-in-re-strip-prefix-srs-singleSTR_IN_RE_STRIP_PREFIX_SRS_SINGLE_NEGAuto-generated from RARE rule str-in-re-strip-prefix-srs-single-negSTR_IN_RE_STRIP_PREFIX_SRS_SINGLE_NEG_REVAuto-generated from RARE rule str-in-re-strip-prefix-srs-single-neg-revSTR_IN_RE_STRIP_PREFIX_SRS_SINGLE_REVAuto-generated from RARE rule str-in-re-strip-prefix-srs-single-revSTR_IN_RE_TEST_UNFOLDAuto-generated from RARE rule str-in-re-test-unfoldSTR_IN_RE_TEST_UNFOLD_REVAuto-generated from RARE rule str-in-re-test-unfold-revSTR_IN_RE_UNION_ELIMAuto-generated from RARE rule str-in-re-union-elimSTR_INDEXOF_CONTAINS_PREAuto-generated from RARE rule str-indexof-contains-preSTR_INDEXOF_NO_CONTAINSAuto-generated from RARE rule str-indexof-no-containsSTR_INDEXOF_RE_NONEAuto-generated from RARE rule str-indexof-re-noneSTR_INDEXOF_SELFAuto-generated from RARE rule str-indexof-selfSTR_LEN_CONCAT_RECAuto-generated from RARE rule str-len-concat-recSTR_LEN_REPLACE_INVAuto-generated from RARE rule str-len-replace-invSTR_LEN_SUBSTR_IN_RANGEAuto-generated from RARE rule str-len-substr-in-rangeSTR_LEN_SUBSTR_UB1Auto-generated from RARE rule str-len-substr-ub1STR_LEN_SUBSTR_UB2Auto-generated from RARE rule str-len-substr-ub2STR_LEN_UPDATE_INVAuto-generated from RARE rule str-len-update-invSTR_LEQ_CONCAT_FALSEAuto-generated from RARE rule str-leq-concat-falseSTR_LEQ_CONCAT_TRUEAuto-generated from RARE rule str-leq-concat-trueSTR_LEQ_EMPTYAuto-generated from RARE rule str-leq-emptySTR_LEQ_EMPTY_EQAuto-generated from RARE rule str-leq-empty-eqSTR_LT_ELIMAuto-generated from RARE rule str-lt-elimSTR_PREFIXOF_ELIMAuto-generated from RARE rule str-prefixof-elimSTR_PREFIXOF_ONEAuto-generated from RARE rule str-prefixof-oneSTR_REPLACE_ALL_NO_CONTAINSAuto-generated from RARE rule str-replace-all-no-containsSTR_REPLACE_CONTAINS_PREAuto-generated from RARE rule str-replace-contains-preSTR_REPLACE_EMPTYAuto-generated from RARE rule str-replace-emptySTR_REPLACE_NO_CONTAINSAuto-generated from RARE rule str-replace-no-containsSTR_REPLACE_PREFIXAuto-generated from RARE rule str-replace-prefixSTR_REPLACE_RE_ALL_NONEAuto-generated from RARE rule str-replace-re-all-noneSTR_REPLACE_RE_NONEAuto-generated from RARE rule str-replace-re-noneSTR_REPLACE_SELFAuto-generated from RARE rule str-replace-selfSTR_SUBSTR_COMBINE1Auto-generated from RARE rule str-substr-combine1STR_SUBSTR_COMBINE2Auto-generated from RARE rule str-substr-combine2STR_SUBSTR_COMBINE3Auto-generated from RARE rule str-substr-combine3STR_SUBSTR_COMBINE4Auto-generated from RARE rule str-substr-combine4STR_SUBSTR_CONCAT1Auto-generated from RARE rule str-substr-concat1STR_SUBSTR_CONCAT2Auto-generated from RARE rule str-substr-concat2STR_SUBSTR_EMPTY_RANGEAuto-generated from RARE rule str-substr-empty-rangeSTR_SUBSTR_EMPTY_STARTAuto-generated from RARE rule str-substr-empty-startSTR_SUBSTR_EMPTY_START_NEGAuto-generated from RARE rule str-substr-empty-start-negSTR_SUBSTR_EMPTY_STRAuto-generated from RARE rule str-substr-empty-strSTR_SUBSTR_EQ_EMPTYAuto-generated from RARE rule str-substr-eq-emptySTR_SUBSTR_FULLAuto-generated from RARE rule str-substr-fullSTR_SUBSTR_FULL_EQAuto-generated from RARE rule str-substr-full-eqSTR_SUBSTR_LEN_INCLUDEAuto-generated from RARE rule str-substr-len-includeSTR_SUBSTR_LEN_INCLUDE_PREAuto-generated from RARE rule str-substr-len-include-preSTR_SUBSTR_LEN_SKIPAuto-generated from RARE rule str-substr-len-skipSTR_SUFFIXOF_ELIMAuto-generated from RARE rule str-suffixof-elimSTR_SUFFIXOF_ONEAuto-generated from RARE rule str-suffixof-oneSTR_TO_INT_CONCAT_NEG_ONEAuto-generated from RARE rule str-to-int-concat-neg-oneSTR_TO_LOWER_CONCATAuto-generated from RARE rule str-to-lower-concatSTR_TO_LOWER_FROM_INTAuto-generated from RARE rule str-to-lower-from-intSTR_TO_LOWER_LENAuto-generated from RARE rule str-to-lower-lenSTR_TO_LOWER_UPPERAuto-generated from RARE rule str-to-lower-upperSTR_TO_UPPER_CONCATAuto-generated from RARE rule str-to-upper-concatSTR_TO_UPPER_FROM_INTAuto-generated from RARE rule str-to-upper-from-intSTR_TO_UPPER_LENAuto-generated from RARE rule str-to-upper-lenSTR_TO_UPPER_LOWERAuto-generated from RARE rule str-to-upper-lowerUF_BV2NAT_GEQ_ELIMAuto-generated from RARE rule uf-bv2nat-geq-elimUF_BV2NAT_INT2BVAuto-generated from RARE rule uf-bv2nat-int2bvUF_BV2NAT_INT2BV_EXTENDAuto-generated from RARE rule uf-bv2nat-int2bv-extendUF_BV2NAT_INT2BV_EXTRACTAuto-generated from RARE rule uf-bv2nat-int2bv-extractUF_INT2BV_BV2NATAuto-generated from RARE rule uf-int2bv-bv2natUF_INT2BV_BVULE_EQUIVAuto-generated from RARE rule uf-int2bv-bvule-equivUF_INT2BV_BVULT_EQUIVAuto-generated from RARE rule uf-int2bv-bvult-equiv
-
Method Summary
All Methods Static Methods Instance Methods Concrete Methods Modifier and Type Method Description static ProofRewriteRulefromInt(int value)intgetValue()static ProofRewriteRulevalueOf(java.lang.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.
-
-
-
Enum Constant Detail
-
NONE
public static final ProofRewriteRule NONE
This enumeration represents the rewrite rules used in a rewrite proof. Some of the rules are internal ad-hoc rewrites, while others are rewrites specified by the RARE DSL. This enumeration is used as the first argument to the DSL_REWRITE <cvc5.ProofRule.DSL_REWRITE> proof rule and the THEORY_REWRITE <cvc5.ProofRule.THEORY_REWRITE> proof rule.
-
DISTINCT_ELIM
public static final ProofRewriteRule 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\)
-
DISTINCT_CARD_CONFLICT
public static final ProofRewriteRule 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\).
-
BV_TO_NAT_ELIM
public static final ProofRewriteRule 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)\).
-
INT_TO_BV_ELIM
public static final ProofRewriteRule 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)\).
-
MACRO_BOOL_NNF_NORM
public static final ProofRewriteRule 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_ARITH_STRING_PRED_ENTAIL
public static final ProofRewriteRule MACRO_ARITH_STRING_PRED_ENTAIL
Arithmetic – strings predicate entailment \[ (= s t) = c \] \[ (>= s t) = c \] where \(c\) is a Boolean constant. This macro is elaborated by applications of EVALUATE <cvc5.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.
-
ARITH_STRING_PRED_ENTAIL
public static final ProofRewriteRule 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
public static final ProofRewriteRule 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)\). In detail, subterms of \(n\) may be replaced with other terms to obtain \(m\) based on the reasoning described in the paper Reynolds et al, CAV 2019, "High-Level Abstractions for Simplifying Extended String Constraints in SMT".
-
ARITH_POW_ELIM
public static final ProofRewriteRule ARITH_POW_ELIM
Arithmetic – power elimination \[ (x ^ c) = (x \cdot \ldots \cdot x) \] where \(c\) is a non-negative integer.
-
BETA_REDUCE
public static final ProofRewriteRule 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 viaNode.substitute.
-
LAMBDA_ELIM
public static final ProofRewriteRule LAMBDA_ELIM
Equality – Lambda elimination \[ (\lambda x_1 \ldots x_n.\> f(x_1 \ldots x_n)) = f \]
-
ARRAYS_SELECT_CONST
public static final ProofRewriteRule ARRAYS_SELECT_CONST
Arrays – Constant array select \[ (select A x) = c \] where \(A\) is a constant array storing element \(c\).
-
MACRO_ARRAYS_DISTINCT_ARRAYS
public static final ProofRewriteRule 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
public static final ProofRewriteRule 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.
-
ARRAYS_EQ_RANGE_EXPAND
public static final ProofRewriteRule 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) \]
-
EXISTS_ELIM
public static final ProofRewriteRule EXISTS_ELIM
Quantifiers – Exists elimination \[ \exists x_1\dots x_n.\> F = \neg \forall x_1\dots x_n.\> \neg F \]
-
QUANT_UNUSED_VARS
public static final ProofRewriteRule 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.
-
MACRO_QUANT_MERGE_PRENEX
public static final ProofRewriteRule 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\).
-
QUANT_MERGE_PRENEX
public static final ProofRewriteRule 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.
-
MACRO_QUANT_PRENEX
public static final ProofRewriteRule 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_MINISCOPE
public static final ProofRewriteRule 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\).
-
QUANT_MINISCOPE_AND
public static final ProofRewriteRule 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_OR
public static final ProofRewriteRule 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_MINISCOPE_ITE
public static final ProofRewriteRule 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_DT_SPLIT
public static final ProofRewriteRule QUANT_DT_SPLIT
Quantifiers – Datatypes Split \[ (\forall x Y.\> F) = (\forall X_1 Y. F_1) \vee \cdots \vee (\forall X_n Y. F_n) \] where \(x\) is of a datatype type with constructors \(C_1, \ldots, C_n\), where for each \(i = 1, \ldots, n\), \(F_i\) is \(F \{ x \mapsto C_i(X_i) \}\).
-
MACRO_QUANT_PARTITION_CONNECTED_FV
public static final ProofRewriteRule 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\). This is determined by computing the connected components when considering two variables in \(X\) to be connected if they occur in the same \(F_i\).
-
MACRO_QUANT_VAR_ELIM_EQ
public static final ProofRewriteRule 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\).
-
QUANT_VAR_ELIM_EQ
public static final ProofRewriteRule QUANT_VAR_ELIM_EQ
Quantifiers – Macro variable elimination equality .. math. (\forall x.\> x \neq t \vee F) = F \{ x \mapsto t \} or alternatively .. math. (\forall x.\> x \neq t) = \bot
-
MACRO_QUANT_VAR_ELIM_INEQ
public static final ProofRewriteRule 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. This is applied only when all such literals are lower (resp. upper) bounds for \(x\).
-
MACRO_QUANT_REWRITE_BODY
public static final ProofRewriteRule MACRO_QUANT_REWRITE_BODY
Quantifiers – Macro quantifiers rewrite body \[ \forall X.\> F = \forall X.\> G \] where \(G\) is semantically equivalent to \(F\).
-
DT_INST
public static final ProofRewriteRule 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_COLLAPSE_SELECTOR
public static final ProofRewriteRule 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
public static final ProofRewriteRule 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
public static final ProofRewriteRule DT_COLLAPSE_TESTER_SINGLETON
Datatypes – collapse tester \[ \mathit{is}_c(t) = true \] where \(c\) is the only constructor of its associated datatype.
-
MACRO_DT_CONS_EQ
public static final ProofRewriteRule MACRO_DT_CONS_EQ
Datatypes – Macro constructor equality \[ (t = s) = (t_1 = s_1 \wedge \ldots \wedge t_n = s_n) \] where \(t_1, \ldots, t_n\) and \(s_1, \ldots, s_n\) are subterms of \(t\) and \(s\) that occur at the same position respectively (beneath constructor applications), or alternatively \[ (t = s) = false \] where \(t\) and \(s\) have subterms that occur in the same position (beneath constructor applications) that are distinct.
-
DT_CONS_EQ
public static final ProofRewriteRule 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) \] where \(c\) is a constructor.
-
DT_CONS_EQ_CLASH
public static final ProofRewriteRule DT_CONS_EQ_CLASH
Datatypes – constructor equality clash \[ (t = s) = false \] where \(t\) and \(s\) have subterms that occur in the same position (beneath constructor applications) that are distinct constructor applications.
-
DT_CYCLE
public static final ProofRewriteRule 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_COLLAPSE_UPDATER
public static final ProofRewriteRule 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_UPDATER_ELIM
public static final ProofRewriteRule 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\).
-
DT_MATCH_ELIM
public static final ProofRewriteRule 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.
-
BV_UMULO_ELIMINATE
public static final ProofRewriteRule BV_UMULO_ELIMINATE
Bitvectors – Unsigned multiplication overflow detection elimination See M.Gok, M.J. Schulte, P.I. Balzola, "Efficient integer multiplication overflow detection circuits", 2001. http:
-
BV_SMULO_ELIMINATE
public static final ProofRewriteRule BV_SMULO_ELIMINATE
Bitvectors – Unsigned multiplication overflow detection elimination See M.Gok, M.J. Schulte, P.I. Balzola, "Efficient integer multiplication overflow detection circuits", 2001. http:
-
BV_ADD_COMBINE_LIKE_TERMS
public static final ProofRewriteRule BV_ADD_COMBINE_LIKE_TERMS
Bitvectors – Combine like terms during addition by counting terms
-
BV_MULT_SIMPLIFY
public static final ProofRewriteRule BV_MULT_SIMPLIFY
Bitvectors – Extract negations from multiplicands \[ bvmul(bvneg(a),\ b,\ c) = bvneg(bvmul(a,\ b,\ c)) \]
-
BV_BITWISE_SLICING
public static final ProofRewriteRule 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_REPEAT_ELIM
public static final ProofRewriteRule BV_REPEAT_ELIM
Bitvectors – Extract continuous substrings of bitvectors \[ repeat(n,\ t) = concat(t ... t) \] where \(t\) is repeated \(n\) times.
-
RE_LOOP_ELIM
public static final ProofRewriteRule 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_INTER_UNION_INCLUSION
public static final ProofRewriteRule 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`. or alternatively: \[ \mathit{re.union}(R) = \mathit{re.union}(\mathit{re}.\text{*}(\mathit{re.allchar}),\ R_0) \] where \(R\) is a list of regular expressions containing `r_1`, `re.comp(r_2)` and the list \(R_0\), where `r_1` is a superset of `r_2`.
-
STR_IN_RE_EVAL
public static final ProofRewriteRule 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_CONSUME
public static final ProofRewriteRule 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_CONCAT_STAR_CHAR
public static final ProofRewriteRule 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_SIGMA
public static final ProofRewriteRule 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
public static final ProofRewriteRule 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{++}\).
-
MACRO_SUBSTR_STRIP_SYM_LENGTH
public static final ProofRewriteRule 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\).
-
SETS_IS_EMPTY_EVAL
public static final ProofRewriteRule 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_INSERT_ELIM
public static final ProofRewriteRule 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) \]
-
ARITH_MUL_ONE
public static final ProofRewriteRule ARITH_MUL_ONE
Auto-generated from RARE rule arith-mul-one
-
ARITH_MUL_ZERO
public static final ProofRewriteRule ARITH_MUL_ZERO
Auto-generated from RARE rule arith-mul-zero
-
ARITH_DIV_TOTAL_REAL
public static final ProofRewriteRule ARITH_DIV_TOTAL_REAL
Auto-generated from RARE rule arith-div-total-real
-
ARITH_DIV_TOTAL_INT
public static final ProofRewriteRule ARITH_DIV_TOTAL_INT
Auto-generated from RARE rule arith-div-total-int
-
ARITH_DIV_TOTAL_ZERO_REAL
public static final ProofRewriteRule ARITH_DIV_TOTAL_ZERO_REAL
Auto-generated from RARE rule arith-div-total-zero-real
-
ARITH_DIV_TOTAL_ZERO_INT
public static final ProofRewriteRule ARITH_DIV_TOTAL_ZERO_INT
Auto-generated from RARE rule arith-div-total-zero-int
-
ARITH_INT_DIV_TOTAL
public static final ProofRewriteRule ARITH_INT_DIV_TOTAL
Auto-generated from RARE rule arith-int-div-total
-
ARITH_INT_DIV_TOTAL_ONE
public static final ProofRewriteRule ARITH_INT_DIV_TOTAL_ONE
Auto-generated from RARE rule arith-int-div-total-one
-
ARITH_INT_DIV_TOTAL_ZERO
public static final ProofRewriteRule ARITH_INT_DIV_TOTAL_ZERO
Auto-generated from RARE rule arith-int-div-total-zero
-
ARITH_INT_MOD_TOTAL
public static final ProofRewriteRule ARITH_INT_MOD_TOTAL
Auto-generated from RARE rule arith-int-mod-total
-
ARITH_INT_MOD_TOTAL_ONE
public static final ProofRewriteRule ARITH_INT_MOD_TOTAL_ONE
Auto-generated from RARE rule arith-int-mod-total-one
-
ARITH_INT_MOD_TOTAL_ZERO
public static final ProofRewriteRule ARITH_INT_MOD_TOTAL_ZERO
Auto-generated from RARE rule arith-int-mod-total-zero
-
ARITH_ELIM_GT
public static final ProofRewriteRule ARITH_ELIM_GT
Auto-generated from RARE rule arith-elim-gt
-
ARITH_ELIM_LT
public static final ProofRewriteRule ARITH_ELIM_LT
Auto-generated from RARE rule arith-elim-lt
-
ARITH_ELIM_INT_GT
public static final ProofRewriteRule ARITH_ELIM_INT_GT
Auto-generated from RARE rule arith-elim-int-gt
-
ARITH_ELIM_INT_LT
public static final ProofRewriteRule ARITH_ELIM_INT_LT
Auto-generated from RARE rule arith-elim-int-lt
-
ARITH_ELIM_LEQ
public static final ProofRewriteRule ARITH_ELIM_LEQ
Auto-generated from RARE rule arith-elim-leq
-
ARITH_LEQ_NORM
public static final ProofRewriteRule ARITH_LEQ_NORM
Auto-generated from RARE rule arith-leq-norm
-
ARITH_GEQ_TIGHTEN
public static final ProofRewriteRule ARITH_GEQ_TIGHTEN
Auto-generated from RARE rule arith-geq-tighten
-
ARITH_GEQ_NORM1_INT
public static final ProofRewriteRule ARITH_GEQ_NORM1_INT
Auto-generated from RARE rule arith-geq-norm1-int
-
ARITH_GEQ_NORM1_REAL
public static final ProofRewriteRule ARITH_GEQ_NORM1_REAL
Auto-generated from RARE rule arith-geq-norm1-real
-
ARITH_GEQ_NORM2
public static final ProofRewriteRule ARITH_GEQ_NORM2
Auto-generated from RARE rule arith-geq-norm2
-
ARITH_REFL_LEQ
public static final ProofRewriteRule ARITH_REFL_LEQ
Auto-generated from RARE rule arith-refl-leq
-
ARITH_REFL_LT
public static final ProofRewriteRule ARITH_REFL_LT
Auto-generated from RARE rule arith-refl-lt
-
ARITH_REFL_GEQ
public static final ProofRewriteRule ARITH_REFL_GEQ
Auto-generated from RARE rule arith-refl-geq
-
ARITH_REFL_GT
public static final ProofRewriteRule ARITH_REFL_GT
Auto-generated from RARE rule arith-refl-gt
-
ARITH_EQ_ELIM_REAL
public static final ProofRewriteRule ARITH_EQ_ELIM_REAL
Auto-generated from RARE rule arith-eq-elim-real
-
ARITH_EQ_ELIM_INT
public static final ProofRewriteRule ARITH_EQ_ELIM_INT
Auto-generated from RARE rule arith-eq-elim-int
-
ARITH_PLUS_FLATTEN
public static final ProofRewriteRule ARITH_PLUS_FLATTEN
Auto-generated from RARE rule arith-plus-flatten
-
ARITH_MULT_FLATTEN
public static final ProofRewriteRule ARITH_MULT_FLATTEN
Auto-generated from RARE rule arith-mult-flatten
-
ARITH_MULT_DIST
public static final ProofRewriteRule ARITH_MULT_DIST
Auto-generated from RARE rule arith-mult-dist
-
ARITH_ABS_ELIM_INT
public static final ProofRewriteRule ARITH_ABS_ELIM_INT
Auto-generated from RARE rule arith-abs-elim-int
-
ARITH_ABS_ELIM_REAL
public static final ProofRewriteRule ARITH_ABS_ELIM_REAL
Auto-generated from RARE rule arith-abs-elim-real
-
ARITH_TO_REAL_ELIM
public static final ProofRewriteRule ARITH_TO_REAL_ELIM
Auto-generated from RARE rule arith-to-real-elim
-
ARITH_TO_INT_ELIM_TO_REAL
public static final ProofRewriteRule ARITH_TO_INT_ELIM_TO_REAL
Auto-generated from RARE rule arith-to-int-elim-to-real
-
ARITH_DIV_ELIM_TO_REAL1
public static final ProofRewriteRule ARITH_DIV_ELIM_TO_REAL1
Auto-generated from RARE rule arith-div-elim-to-real1
-
ARITH_DIV_ELIM_TO_REAL2
public static final ProofRewriteRule ARITH_DIV_ELIM_TO_REAL2
Auto-generated from RARE rule arith-div-elim-to-real2
-
ARITH_SINE_ZERO
public static final ProofRewriteRule ARITH_SINE_ZERO
Auto-generated from RARE rule arith-sine-zero
-
ARITH_SINE_PI2
public static final ProofRewriteRule ARITH_SINE_PI2
Auto-generated from RARE rule arith-sine-pi2
-
ARITH_COSINE_ELIM
public static final ProofRewriteRule ARITH_COSINE_ELIM
Auto-generated from RARE rule arith-cosine-elim
-
ARITH_TANGENT_ELIM
public static final ProofRewriteRule ARITH_TANGENT_ELIM
Auto-generated from RARE rule arith-tangent-elim
-
ARITH_SECENT_ELIM
public static final ProofRewriteRule ARITH_SECENT_ELIM
Auto-generated from RARE rule arith-secent-elim
-
ARITH_COSECENT_ELIM
public static final ProofRewriteRule ARITH_COSECENT_ELIM
Auto-generated from RARE rule arith-cosecent-elim
-
ARITH_COTANGENT_ELIM
public static final ProofRewriteRule ARITH_COTANGENT_ELIM
Auto-generated from RARE rule arith-cotangent-elim
-
ARITH_PI_NOT_INT
public static final ProofRewriteRule ARITH_PI_NOT_INT
Auto-generated from RARE rule arith-pi-not-int
-
ARITH_ABS_EQ
public static final ProofRewriteRule ARITH_ABS_EQ
Auto-generated from RARE rule arith-abs-eq
-
ARITH_ABS_INT_GT
public static final ProofRewriteRule ARITH_ABS_INT_GT
Auto-generated from RARE rule arith-abs-int-gt
-
ARITH_ABS_REAL_GT
public static final ProofRewriteRule ARITH_ABS_REAL_GT
Auto-generated from RARE rule arith-abs-real-gt
-
ARRAY_READ_OVER_WRITE
public static final ProofRewriteRule ARRAY_READ_OVER_WRITE
Auto-generated from RARE rule array-read-over-write
-
ARRAY_READ_OVER_WRITE2
public static final ProofRewriteRule ARRAY_READ_OVER_WRITE2
Auto-generated from RARE rule array-read-over-write2
-
ARRAY_STORE_OVERWRITE
public static final ProofRewriteRule ARRAY_STORE_OVERWRITE
Auto-generated from RARE rule array-store-overwrite
-
ARRAY_STORE_SELF
public static final ProofRewriteRule ARRAY_STORE_SELF
Auto-generated from RARE rule array-store-self
-
ARRAY_READ_OVER_WRITE_SPLIT
public static final ProofRewriteRule ARRAY_READ_OVER_WRITE_SPLIT
Auto-generated from RARE rule array-read-over-write-split
-
BOOL_DOUBLE_NOT_ELIM
public static final ProofRewriteRule BOOL_DOUBLE_NOT_ELIM
Auto-generated from RARE rule boolean-double-not-elim
-
BOOL_NOT_TRUE
public static final ProofRewriteRule BOOL_NOT_TRUE
Auto-generated from RARE rule boolean-not-true
-
BOOL_NOT_FALSE
public static final ProofRewriteRule BOOL_NOT_FALSE
Auto-generated from RARE rule boolean-not-false
-
BOOL_EQ_TRUE
public static final ProofRewriteRule BOOL_EQ_TRUE
Auto-generated from RARE rule boolean-eq-true
-
BOOL_EQ_FALSE
public static final ProofRewriteRule BOOL_EQ_FALSE
Auto-generated from RARE rule boolean-eq-false
-
BOOL_EQ_NREFL
public static final ProofRewriteRule BOOL_EQ_NREFL
Auto-generated from RARE rule boolean-eq-nrefl
-
BOOL_IMPL_FALSE1
public static final ProofRewriteRule BOOL_IMPL_FALSE1
Auto-generated from RARE rule boolean-impl-false1
-
BOOL_IMPL_FALSE2
public static final ProofRewriteRule BOOL_IMPL_FALSE2
Auto-generated from RARE rule boolean-impl-false2
-
BOOL_IMPL_TRUE1
public static final ProofRewriteRule BOOL_IMPL_TRUE1
Auto-generated from RARE rule boolean-impl-true1
-
BOOL_IMPL_TRUE2
public static final ProofRewriteRule BOOL_IMPL_TRUE2
Auto-generated from RARE rule boolean-impl-true2
-
BOOL_IMPL_ELIM
public static final ProofRewriteRule BOOL_IMPL_ELIM
Auto-generated from RARE rule boolean-impl-elim
-
BOOL_OR_TRUE
public static final ProofRewriteRule BOOL_OR_TRUE
Auto-generated from RARE rule boolean-or-true
-
BOOL_OR_FLATTEN
public static final ProofRewriteRule BOOL_OR_FLATTEN
Auto-generated from RARE rule boolean-or-flatten
-
BOOL_AND_FALSE
public static final ProofRewriteRule BOOL_AND_FALSE
Auto-generated from RARE rule boolean-and-false
-
BOOL_AND_FLATTEN
public static final ProofRewriteRule BOOL_AND_FLATTEN
Auto-generated from RARE rule boolean-and-flatten
-
BOOL_AND_CONF
public static final ProofRewriteRule BOOL_AND_CONF
Auto-generated from RARE rule boolean-and-conf
-
BOOL_AND_CONF2
public static final ProofRewriteRule BOOL_AND_CONF2
Auto-generated from RARE rule boolean-and-conf2
-
BOOL_OR_TAUT
public static final ProofRewriteRule BOOL_OR_TAUT
Auto-generated from RARE rule boolean-or-taut
-
BOOL_OR_TAUT2
public static final ProofRewriteRule BOOL_OR_TAUT2
Auto-generated from RARE rule boolean-or-taut2
-
BOOL_OR_DE_MORGAN
public static final ProofRewriteRule BOOL_OR_DE_MORGAN
Auto-generated from RARE rule boolean-or-de-morgan
-
BOOL_IMPLIES_DE_MORGAN
public static final ProofRewriteRule BOOL_IMPLIES_DE_MORGAN
Auto-generated from RARE rule boolean-implies-de-morgan
-
BOOL_AND_DE_MORGAN
public static final ProofRewriteRule BOOL_AND_DE_MORGAN
Auto-generated from RARE rule boolean-and-de-morgan
-
BOOL_OR_AND_DISTRIB
public static final ProofRewriteRule BOOL_OR_AND_DISTRIB
Auto-generated from RARE rule boolean-or-and-distrib
-
BOOL_XOR_REFL
public static final ProofRewriteRule BOOL_XOR_REFL
Auto-generated from RARE rule boolean-xor-refl
-
BOOL_XOR_NREFL
public static final ProofRewriteRule BOOL_XOR_NREFL
Auto-generated from RARE rule boolean-xor-nrefl
-
BOOL_XOR_FALSE
public static final ProofRewriteRule BOOL_XOR_FALSE
Auto-generated from RARE rule boolean-xor-false
-
BOOL_XOR_TRUE
public static final ProofRewriteRule BOOL_XOR_TRUE
Auto-generated from RARE rule boolean-xor-true
-
BOOL_XOR_COMM
public static final ProofRewriteRule BOOL_XOR_COMM
Auto-generated from RARE rule boolean-xor-comm
-
BOOL_XOR_ELIM
public static final ProofRewriteRule BOOL_XOR_ELIM
Auto-generated from RARE rule boolean-xor-elim
-
BOOL_NOT_XOR_ELIM
public static final ProofRewriteRule BOOL_NOT_XOR_ELIM
Auto-generated from RARE rule boolean-not-xor-elim
-
BOOL_NOT_EQ_ELIM1
public static final ProofRewriteRule BOOL_NOT_EQ_ELIM1
Auto-generated from RARE rule boolean-not-eq-elim1
-
BOOL_NOT_EQ_ELIM2
public static final ProofRewriteRule BOOL_NOT_EQ_ELIM2
Auto-generated from RARE rule boolean-not-eq-elim2
-
ITE_NEG_BRANCH
public static final ProofRewriteRule ITE_NEG_BRANCH
Auto-generated from RARE rule ite-neg-branch
-
ITE_THEN_TRUE
public static final ProofRewriteRule ITE_THEN_TRUE
Auto-generated from RARE rule ite-then-true
-
ITE_ELSE_FALSE
public static final ProofRewriteRule ITE_ELSE_FALSE
Auto-generated from RARE rule ite-else-false
-
ITE_THEN_FALSE
public static final ProofRewriteRule ITE_THEN_FALSE
Auto-generated from RARE rule ite-then-false
-
ITE_ELSE_TRUE
public static final ProofRewriteRule ITE_ELSE_TRUE
Auto-generated from RARE rule ite-else-true
-
ITE_THEN_LOOKAHEAD_SELF
public static final ProofRewriteRule ITE_THEN_LOOKAHEAD_SELF
Auto-generated from RARE rule ite-then-lookahead-self
-
ITE_ELSE_LOOKAHEAD_SELF
public static final ProofRewriteRule ITE_ELSE_LOOKAHEAD_SELF
Auto-generated from RARE rule ite-else-lookahead-self
-
ITE_THEN_LOOKAHEAD_NOT_SELF
public static final ProofRewriteRule ITE_THEN_LOOKAHEAD_NOT_SELF
Auto-generated from RARE rule ite-then-lookahead-not-self
-
ITE_ELSE_LOOKAHEAD_NOT_SELF
public static final ProofRewriteRule ITE_ELSE_LOOKAHEAD_NOT_SELF
Auto-generated from RARE rule ite-else-lookahead-not-self
-
ITE_EXPAND
public static final ProofRewriteRule ITE_EXPAND
Auto-generated from RARE rule ite-expand
-
BOOL_NOT_ITE_ELIM
public static final ProofRewriteRule BOOL_NOT_ITE_ELIM
Auto-generated from RARE rule boolean-not-ite-elim
-
ITE_TRUE_COND
public static final ProofRewriteRule ITE_TRUE_COND
Auto-generated from RARE rule ite-true-cond
-
ITE_FALSE_COND
public static final ProofRewriteRule ITE_FALSE_COND
Auto-generated from RARE rule ite-false-cond
-
ITE_NOT_COND
public static final ProofRewriteRule ITE_NOT_COND
Auto-generated from RARE rule ite-not-cond
-
ITE_EQ_BRANCH
public static final ProofRewriteRule ITE_EQ_BRANCH
Auto-generated from RARE rule ite-eq-branch
-
ITE_THEN_LOOKAHEAD
public static final ProofRewriteRule ITE_THEN_LOOKAHEAD
Auto-generated from RARE rule ite-then-lookahead
-
ITE_ELSE_LOOKAHEAD
public static final ProofRewriteRule ITE_ELSE_LOOKAHEAD
Auto-generated from RARE rule ite-else-lookahead
-
ITE_THEN_NEG_LOOKAHEAD
public static final ProofRewriteRule ITE_THEN_NEG_LOOKAHEAD
Auto-generated from RARE rule ite-then-neg-lookahead
-
ITE_ELSE_NEG_LOOKAHEAD
public static final ProofRewriteRule ITE_ELSE_NEG_LOOKAHEAD
Auto-generated from RARE rule ite-else-neg-lookahead
-
BV_CONCAT_FLATTEN
public static final ProofRewriteRule BV_CONCAT_FLATTEN
Auto-generated from RARE rule bv-concat-flatten
-
BV_CONCAT_EXTRACT_MERGE
public static final ProofRewriteRule BV_CONCAT_EXTRACT_MERGE
Auto-generated from RARE rule bv-concat-extract-merge
-
BV_EXTRACT_EXTRACT
public static final ProofRewriteRule BV_EXTRACT_EXTRACT
Auto-generated from RARE rule bv-extract-extract
-
BV_EXTRACT_WHOLE
public static final ProofRewriteRule BV_EXTRACT_WHOLE
Auto-generated from RARE rule bv-extract-whole
-
BV_EXTRACT_CONCAT_1
public static final ProofRewriteRule BV_EXTRACT_CONCAT_1
Auto-generated from RARE rule bv-extract-concat-1
-
BV_EXTRACT_CONCAT_2
public static final ProofRewriteRule BV_EXTRACT_CONCAT_2
Auto-generated from RARE rule bv-extract-concat-2
-
BV_EXTRACT_CONCAT_3
public static final ProofRewriteRule BV_EXTRACT_CONCAT_3
Auto-generated from RARE rule bv-extract-concat-3
-
BV_EXTRACT_CONCAT_4
public static final ProofRewriteRule BV_EXTRACT_CONCAT_4
Auto-generated from RARE rule bv-extract-concat-4
-
BV_EQ_EXTRACT_ELIM1
public static final ProofRewriteRule BV_EQ_EXTRACT_ELIM1
Auto-generated from RARE rule bv-eq-extract-elim1
-
BV_EQ_EXTRACT_ELIM2
public static final ProofRewriteRule BV_EQ_EXTRACT_ELIM2
Auto-generated from RARE rule bv-eq-extract-elim2
-
BV_EQ_EXTRACT_ELIM3
public static final ProofRewriteRule BV_EQ_EXTRACT_ELIM3
Auto-generated from RARE rule bv-eq-extract-elim3
-
BV_EXTRACT_BITWISE_AND
public static final ProofRewriteRule BV_EXTRACT_BITWISE_AND
Auto-generated from RARE rule bv-extract-bitwise-and
-
BV_EXTRACT_BITWISE_OR
public static final ProofRewriteRule BV_EXTRACT_BITWISE_OR
Auto-generated from RARE rule bv-extract-bitwise-or
-
BV_EXTRACT_BITWISE_XOR
public static final ProofRewriteRule BV_EXTRACT_BITWISE_XOR
Auto-generated from RARE rule bv-extract-bitwise-xor
-
BV_EXTRACT_NOT
public static final ProofRewriteRule BV_EXTRACT_NOT
Auto-generated from RARE rule bv-extract-not
-
BV_EXTRACT_SIGN_EXTEND_1
public static final ProofRewriteRule BV_EXTRACT_SIGN_EXTEND_1
Auto-generated from RARE rule bv-extract-sign-extend-1
-
BV_EXTRACT_SIGN_EXTEND_2
public static final ProofRewriteRule BV_EXTRACT_SIGN_EXTEND_2
Auto-generated from RARE rule bv-extract-sign-extend-2
-
BV_EXTRACT_SIGN_EXTEND_3
public static final ProofRewriteRule BV_EXTRACT_SIGN_EXTEND_3
Auto-generated from RARE rule bv-extract-sign-extend-3
-
BV_NEG_MULT
public static final ProofRewriteRule BV_NEG_MULT
Auto-generated from RARE rule bv-neg-mult
-
BV_NEG_ADD
public static final ProofRewriteRule BV_NEG_ADD
Auto-generated from RARE rule bv-neg-add
-
BV_MULT_DISTRIB_CONST_NEG
public static final ProofRewriteRule BV_MULT_DISTRIB_CONST_NEG
Auto-generated from RARE rule bv-mult-distrib--neg
-
BV_MULT_DISTRIB_CONST_ADD
public static final ProofRewriteRule BV_MULT_DISTRIB_CONST_ADD
Auto-generated from RARE rule bv-mult-distrib--add
-
BV_MULT_DISTRIB_CONST_SUB
public static final ProofRewriteRule BV_MULT_DISTRIB_CONST_SUB
Auto-generated from RARE rule bv-mult-distrib--sub
-
BV_MULT_DISTRIB_1
public static final ProofRewriteRule BV_MULT_DISTRIB_1
Auto-generated from RARE rule bv-mult-distrib-1
-
BV_MULT_DISTRIB_2
public static final ProofRewriteRule BV_MULT_DISTRIB_2
Auto-generated from RARE rule bv-mult-distrib-2
-
BV_NOT_XOR
public static final ProofRewriteRule BV_NOT_XOR
Auto-generated from RARE rule bv-not-xor
-
BV_AND_SIMPLIFY_1
public static final ProofRewriteRule BV_AND_SIMPLIFY_1
Auto-generated from RARE rule bv-and-simplify-1
-
BV_AND_SIMPLIFY_2
public static final ProofRewriteRule BV_AND_SIMPLIFY_2
Auto-generated from RARE rule bv-and-simplify-2
-
BV_OR_SIMPLIFY_1
public static final ProofRewriteRule BV_OR_SIMPLIFY_1
Auto-generated from RARE rule bv-or-simplify-1
-
BV_OR_SIMPLIFY_2
public static final ProofRewriteRule BV_OR_SIMPLIFY_2
Auto-generated from RARE rule bv-or-simplify-2
-
BV_XOR_SIMPLIFY_1
public static final ProofRewriteRule BV_XOR_SIMPLIFY_1
Auto-generated from RARE rule bv-xor-simplify-1
-
BV_XOR_SIMPLIFY_2
public static final ProofRewriteRule BV_XOR_SIMPLIFY_2
Auto-generated from RARE rule bv-xor-simplify-2
-
BV_XOR_SIMPLIFY_3
public static final ProofRewriteRule BV_XOR_SIMPLIFY_3
Auto-generated from RARE rule bv-xor-simplify-3
-
BV_ULT_ADD_ONE
public static final ProofRewriteRule BV_ULT_ADD_ONE
Auto-generated from RARE rule bv-ult-add-one
-
BV_CONCAT_TO_MULT
public static final ProofRewriteRule BV_CONCAT_TO_MULT
Auto-generated from RARE rule bv-concat-to-mult
-
BV_MULT_SLT_MULT_1
public static final ProofRewriteRule BV_MULT_SLT_MULT_1
Auto-generated from RARE rule bv-mult-slt-mult-1
-
BV_MULT_SLT_MULT_2
public static final ProofRewriteRule BV_MULT_SLT_MULT_2
Auto-generated from RARE rule bv-mult-slt-mult-2
-
BV_COMMUTATIVE_AND
public static final ProofRewriteRule BV_COMMUTATIVE_AND
Auto-generated from RARE rule bv-commutative-and
-
BV_COMMUTATIVE_OR
public static final ProofRewriteRule BV_COMMUTATIVE_OR
Auto-generated from RARE rule bv-commutative-or
-
BV_COMMUTATIVE_XOR
public static final ProofRewriteRule BV_COMMUTATIVE_XOR
Auto-generated from RARE rule bv-commutative-xor
-
BV_COMMUTATIVE_MUL
public static final ProofRewriteRule BV_COMMUTATIVE_MUL
Auto-generated from RARE rule bv-commutative-mul
-
BV_OR_ZERO
public static final ProofRewriteRule BV_OR_ZERO
Auto-generated from RARE rule bv-or-zero
-
BV_MUL_ONE
public static final ProofRewriteRule BV_MUL_ONE
Auto-generated from RARE rule bv-mul-one
-
BV_MUL_ZERO
public static final ProofRewriteRule BV_MUL_ZERO
Auto-generated from RARE rule bv-mul-zero
-
BV_ADD_ZERO
public static final ProofRewriteRule BV_ADD_ZERO
Auto-generated from RARE rule bv-add-zero
-
BV_ADD_TWO
public static final ProofRewriteRule BV_ADD_TWO
Auto-generated from RARE rule bv-add-two
-
BV_ZERO_EXTEND_ELIMINATE_0
public static final ProofRewriteRule BV_ZERO_EXTEND_ELIMINATE_0
Auto-generated from RARE rule bv-zero-extend-eliminate-0
-
BV_SIGN_EXTEND_ELIMINATE_0
public static final ProofRewriteRule BV_SIGN_EXTEND_ELIMINATE_0
Auto-generated from RARE rule bv-sign-extend-eliminate-0
-
BV_NOT_NEQ
public static final ProofRewriteRule BV_NOT_NEQ
Auto-generated from RARE rule bv-not-neq
-
BV_ULT_ONES
public static final ProofRewriteRule BV_ULT_ONES
Auto-generated from RARE rule bv-ult-ones
-
BV_OR_FLATTEN
public static final ProofRewriteRule BV_OR_FLATTEN
Auto-generated from RARE rule bv-or-flatten
-
BV_XOR_FLATTEN
public static final ProofRewriteRule BV_XOR_FLATTEN
Auto-generated from RARE rule bv-xor-flatten
-
BV_AND_FLATTEN
public static final ProofRewriteRule BV_AND_FLATTEN
Auto-generated from RARE rule bv-and-flatten
-
BV_MUL_FLATTEN
public static final ProofRewriteRule BV_MUL_FLATTEN
Auto-generated from RARE rule bv-mul-flatten
-
BV_CONCAT_MERGE_CONST
public static final ProofRewriteRule BV_CONCAT_MERGE_CONST
Auto-generated from RARE rule bv-concat-merge-
-
BV_COMMUTATIVE_ADD
public static final ProofRewriteRule BV_COMMUTATIVE_ADD
Auto-generated from RARE rule bv-commutative-add
-
BV_NEG_SUB
public static final ProofRewriteRule BV_NEG_SUB
Auto-generated from RARE rule bv-neg-sub
-
BV_NEG_IDEMP
public static final ProofRewriteRule BV_NEG_IDEMP
Auto-generated from RARE rule bv-neg-idemp
-
BV_SUB_ELIMINATE
public static final ProofRewriteRule BV_SUB_ELIMINATE
Auto-generated from RARE rule bv-sub-eliminate
-
BV_UGT_ELIMINATE
public static final ProofRewriteRule BV_UGT_ELIMINATE
Auto-generated from RARE rule bv-ugt-eliminate
-
BV_UGE_ELIMINATE
public static final ProofRewriteRule BV_UGE_ELIMINATE
Auto-generated from RARE rule bv-uge-eliminate
-
BV_SGT_ELIMINATE
public static final ProofRewriteRule BV_SGT_ELIMINATE
Auto-generated from RARE rule bv-sgt-eliminate
-
BV_SGE_ELIMINATE
public static final ProofRewriteRule BV_SGE_ELIMINATE
Auto-generated from RARE rule bv-sge-eliminate
-
BV_SLT_ELIMINATE
public static final ProofRewriteRule BV_SLT_ELIMINATE
Auto-generated from RARE rule bv-slt-eliminate
-
BV_SLE_ELIMINATE
public static final ProofRewriteRule BV_SLE_ELIMINATE
Auto-generated from RARE rule bv-sle-eliminate
-
BV_REDOR_ELIMINATE
public static final ProofRewriteRule BV_REDOR_ELIMINATE
Auto-generated from RARE rule bv-redor-eliminate
-
BV_REDAND_ELIMINATE
public static final ProofRewriteRule BV_REDAND_ELIMINATE
Auto-generated from RARE rule bv-redand-eliminate
-
BV_ULE_ELIMINATE
public static final ProofRewriteRule BV_ULE_ELIMINATE
Auto-generated from RARE rule bv-ule-eliminate
-
BV_COMP_ELIMINATE
public static final ProofRewriteRule BV_COMP_ELIMINATE
Auto-generated from RARE rule bv-comp-eliminate
-
BV_ROTATE_LEFT_ELIMINATE_1
public static final ProofRewriteRule BV_ROTATE_LEFT_ELIMINATE_1
Auto-generated from RARE rule bv-rotate-left-eliminate-1
-
BV_ROTATE_LEFT_ELIMINATE_2
public static final ProofRewriteRule BV_ROTATE_LEFT_ELIMINATE_2
Auto-generated from RARE rule bv-rotate-left-eliminate-2
-
BV_ROTATE_RIGHT_ELIMINATE_1
public static final ProofRewriteRule BV_ROTATE_RIGHT_ELIMINATE_1
Auto-generated from RARE rule bv-rotate-right-eliminate-1
-
BV_ROTATE_RIGHT_ELIMINATE_2
public static final ProofRewriteRule BV_ROTATE_RIGHT_ELIMINATE_2
Auto-generated from RARE rule bv-rotate-right-eliminate-2
-
BV_NAND_ELIMINATE
public static final ProofRewriteRule BV_NAND_ELIMINATE
Auto-generated from RARE rule bv-nand-eliminate
-
BV_NOR_ELIMINATE
public static final ProofRewriteRule BV_NOR_ELIMINATE
Auto-generated from RARE rule bv-nor-eliminate
-
BV_XNOR_ELIMINATE
public static final ProofRewriteRule BV_XNOR_ELIMINATE
Auto-generated from RARE rule bv-xnor-eliminate
-
BV_SDIV_ELIMINATE
public static final ProofRewriteRule BV_SDIV_ELIMINATE
Auto-generated from RARE rule bv-sdiv-eliminate
-
BV_SDIV_ELIMINATE_FEWER_BITWISE_OPS
public static final ProofRewriteRule BV_SDIV_ELIMINATE_FEWER_BITWISE_OPS
Auto-generated from RARE rule bv-sdiv-eliminate-fewer-bitwise-ops
-
BV_ZERO_EXTEND_ELIMINATE
public static final ProofRewriteRule BV_ZERO_EXTEND_ELIMINATE
Auto-generated from RARE rule bv-zero-extend-eliminate
-
BV_SIGN_EXTEND_ELIMINATE
public static final ProofRewriteRule BV_SIGN_EXTEND_ELIMINATE
Auto-generated from RARE rule bv-sign-extend-eliminate
-
BV_UADDO_ELIMINATE
public static final ProofRewriteRule BV_UADDO_ELIMINATE
Auto-generated from RARE rule bv-uaddo-eliminate
-
BV_SADDO_ELIMINATE
public static final ProofRewriteRule BV_SADDO_ELIMINATE
Auto-generated from RARE rule bv-saddo-eliminate
-
BV_SDIVO_ELIMINATE
public static final ProofRewriteRule BV_SDIVO_ELIMINATE
Auto-generated from RARE rule bv-sdivo-eliminate
-
BV_SMOD_ELIMINATE
public static final ProofRewriteRule BV_SMOD_ELIMINATE
Auto-generated from RARE rule bv-smod-eliminate
-
BV_SMOD_ELIMINATE_FEWER_BITWISE_OPS
public static final ProofRewriteRule BV_SMOD_ELIMINATE_FEWER_BITWISE_OPS
Auto-generated from RARE rule bv-smod-eliminate-fewer-bitwise-ops
-
BV_SREM_ELIMINATE
public static final ProofRewriteRule BV_SREM_ELIMINATE
Auto-generated from RARE rule bv-srem-eliminate
-
BV_SREM_ELIMINATE_FEWER_BITWISE_OPS
public static final ProofRewriteRule BV_SREM_ELIMINATE_FEWER_BITWISE_OPS
Auto-generated from RARE rule bv-srem-eliminate-fewer-bitwise-ops
-
BV_USUBO_ELIMINATE
public static final ProofRewriteRule BV_USUBO_ELIMINATE
Auto-generated from RARE rule bv-usubo-eliminate
-
BV_SSUBO_ELIMINATE
public static final ProofRewriteRule BV_SSUBO_ELIMINATE
Auto-generated from RARE rule bv-ssubo-eliminate
-
BV_ITE_EQUAL_CHILDREN
public static final ProofRewriteRule BV_ITE_EQUAL_CHILDREN
Auto-generated from RARE rule bv-ite-equal-children
-
BV_ITE_CONST_CHILDREN_1
public static final ProofRewriteRule BV_ITE_CONST_CHILDREN_1
Auto-generated from RARE rule bv-ite--children-1
-
BV_ITE_CONST_CHILDREN_2
public static final ProofRewriteRule BV_ITE_CONST_CHILDREN_2
Auto-generated from RARE rule bv-ite--children-2
-
BV_ITE_EQUAL_COND_1
public static final ProofRewriteRule BV_ITE_EQUAL_COND_1
Auto-generated from RARE rule bv-ite-equal-cond-1
-
BV_ITE_EQUAL_COND_2
public static final ProofRewriteRule BV_ITE_EQUAL_COND_2
Auto-generated from RARE rule bv-ite-equal-cond-2
-
BV_ITE_EQUAL_COND_3
public static final ProofRewriteRule BV_ITE_EQUAL_COND_3
Auto-generated from RARE rule bv-ite-equal-cond-3
-
BV_ITE_MERGE_THEN_IF
public static final ProofRewriteRule BV_ITE_MERGE_THEN_IF
Auto-generated from RARE rule bv-ite-merge-then-if
-
BV_ITE_MERGE_ELSE_IF
public static final ProofRewriteRule BV_ITE_MERGE_ELSE_IF
Auto-generated from RARE rule bv-ite-merge-else-if
-
BV_ITE_MERGE_THEN_ELSE
public static final ProofRewriteRule BV_ITE_MERGE_THEN_ELSE
Auto-generated from RARE rule bv-ite-merge-then-else
-
BV_ITE_MERGE_ELSE_ELSE
public static final ProofRewriteRule BV_ITE_MERGE_ELSE_ELSE
Auto-generated from RARE rule bv-ite-merge-else-else
-
BV_SHL_BY_CONST_0
public static final ProofRewriteRule BV_SHL_BY_CONST_0
Auto-generated from RARE rule bv-shl-by--0
-
BV_SHL_BY_CONST_1
public static final ProofRewriteRule BV_SHL_BY_CONST_1
Auto-generated from RARE rule bv-shl-by--1
-
BV_SHL_BY_CONST_2
public static final ProofRewriteRule BV_SHL_BY_CONST_2
Auto-generated from RARE rule bv-shl-by--2
-
BV_LSHR_BY_CONST_0
public static final ProofRewriteRule BV_LSHR_BY_CONST_0
Auto-generated from RARE rule bv-lshr-by--0
-
BV_LSHR_BY_CONST_1
public static final ProofRewriteRule BV_LSHR_BY_CONST_1
Auto-generated from RARE rule bv-lshr-by--1
-
BV_LSHR_BY_CONST_2
public static final ProofRewriteRule BV_LSHR_BY_CONST_2
Auto-generated from RARE rule bv-lshr-by--2
-
BV_ASHR_BY_CONST_0
public static final ProofRewriteRule BV_ASHR_BY_CONST_0
Auto-generated from RARE rule bv-ashr-by--0
-
BV_ASHR_BY_CONST_1
public static final ProofRewriteRule BV_ASHR_BY_CONST_1
Auto-generated from RARE rule bv-ashr-by--1
-
BV_ASHR_BY_CONST_2
public static final ProofRewriteRule BV_ASHR_BY_CONST_2
Auto-generated from RARE rule bv-ashr-by--2
-
BV_AND_CONCAT_PULLUP
public static final ProofRewriteRule BV_AND_CONCAT_PULLUP
Auto-generated from RARE rule bv-and-concat-pullup
-
BV_OR_CONCAT_PULLUP
public static final ProofRewriteRule BV_OR_CONCAT_PULLUP
Auto-generated from RARE rule bv-or-concat-pullup
-
BV_XOR_CONCAT_PULLUP
public static final ProofRewriteRule BV_XOR_CONCAT_PULLUP
Auto-generated from RARE rule bv-xor-concat-pullup
-
BV_BITWISE_IDEMP_1
public static final ProofRewriteRule BV_BITWISE_IDEMP_1
Auto-generated from RARE rule bv-bitwise-idemp-1
-
BV_BITWISE_IDEMP_2
public static final ProofRewriteRule BV_BITWISE_IDEMP_2
Auto-generated from RARE rule bv-bitwise-idemp-2
-
BV_AND_ZERO
public static final ProofRewriteRule BV_AND_ZERO
Auto-generated from RARE rule bv-and-zero
-
BV_AND_ONE
public static final ProofRewriteRule BV_AND_ONE
Auto-generated from RARE rule bv-and-one
-
BV_OR_ONE
public static final ProofRewriteRule BV_OR_ONE
Auto-generated from RARE rule bv-or-one
-
BV_XOR_DUPLICATE
public static final ProofRewriteRule BV_XOR_DUPLICATE
Auto-generated from RARE rule bv-xor-duplicate
-
BV_XOR_ONES
public static final ProofRewriteRule BV_XOR_ONES
Auto-generated from RARE rule bv-xor-ones
-
BV_XOR_ZERO
public static final ProofRewriteRule BV_XOR_ZERO
Auto-generated from RARE rule bv-xor-zero
-
BV_BITWISE_NOT_AND
public static final ProofRewriteRule BV_BITWISE_NOT_AND
Auto-generated from RARE rule bv-bitwise-not-and
-
BV_BITWISE_NOT_OR
public static final ProofRewriteRule BV_BITWISE_NOT_OR
Auto-generated from RARE rule bv-bitwise-not-or
-
BV_XOR_NOT
public static final ProofRewriteRule BV_XOR_NOT
Auto-generated from RARE rule bv-xor-not
-
BV_NOT_IDEMP
public static final ProofRewriteRule BV_NOT_IDEMP
Auto-generated from RARE rule bv-not-idemp
-
BV_ULT_ZERO_1
public static final ProofRewriteRule BV_ULT_ZERO_1
Auto-generated from RARE rule bv-ult-zero-1
-
BV_ULT_ZERO_2
public static final ProofRewriteRule BV_ULT_ZERO_2
Auto-generated from RARE rule bv-ult-zero-2
-
BV_ULT_SELF
public static final ProofRewriteRule BV_ULT_SELF
Auto-generated from RARE rule bv-ult-self
-
BV_LT_SELF
public static final ProofRewriteRule BV_LT_SELF
Auto-generated from RARE rule bv-lt-self
-
BV_ULE_SELF
public static final ProofRewriteRule BV_ULE_SELF
Auto-generated from RARE rule bv-ule-self
-
BV_ULE_ZERO
public static final ProofRewriteRule BV_ULE_ZERO
Auto-generated from RARE rule bv-ule-zero
-
BV_ZERO_ULE
public static final ProofRewriteRule BV_ZERO_ULE
Auto-generated from RARE rule bv-zero-ule
-
BV_SLE_SELF
public static final ProofRewriteRule BV_SLE_SELF
Auto-generated from RARE rule bv-sle-self
-
BV_ULE_MAX
public static final ProofRewriteRule BV_ULE_MAX
Auto-generated from RARE rule bv-ule-max
-
BV_NOT_ULT
public static final ProofRewriteRule BV_NOT_ULT
Auto-generated from RARE rule bv-not-ult
-
BV_NOT_ULE
public static final ProofRewriteRule BV_NOT_ULE
Auto-generated from RARE rule bv-not-ule
-
BV_NOT_SLE
public static final ProofRewriteRule BV_NOT_SLE
Auto-generated from RARE rule bv-not-sle
-
BV_MULT_POW2_1
public static final ProofRewriteRule BV_MULT_POW2_1
Auto-generated from RARE rule bv-mult-pow2-1
-
BV_MULT_POW2_2
public static final ProofRewriteRule BV_MULT_POW2_2
Auto-generated from RARE rule bv-mult-pow2-2
-
BV_MULT_POW2_2B
public static final ProofRewriteRule BV_MULT_POW2_2B
Auto-generated from RARE rule bv-mult-pow2-2b
-
BV_EXTRACT_MULT_LEADING_BIT
public static final ProofRewriteRule BV_EXTRACT_MULT_LEADING_BIT
Auto-generated from RARE rule bv-extract-mult-leading-bit
-
BV_UDIV_POW2_NOT_ONE
public static final ProofRewriteRule BV_UDIV_POW2_NOT_ONE
Auto-generated from RARE rule bv-udiv-pow2-not-one
-
BV_UDIV_ZERO
public static final ProofRewriteRule BV_UDIV_ZERO
Auto-generated from RARE rule bv-udiv-zero
-
BV_UDIV_ONE
public static final ProofRewriteRule BV_UDIV_ONE
Auto-generated from RARE rule bv-udiv-one
-
BV_UREM_POW2_NOT_ONE
public static final ProofRewriteRule BV_UREM_POW2_NOT_ONE
Auto-generated from RARE rule bv-urem-pow2-not-one
-
BV_UREM_ONE
public static final ProofRewriteRule BV_UREM_ONE
Auto-generated from RARE rule bv-urem-one
-
BV_UREM_SELF
public static final ProofRewriteRule BV_UREM_SELF
Auto-generated from RARE rule bv-urem-self
-
BV_SHL_ZERO
public static final ProofRewriteRule BV_SHL_ZERO
Auto-generated from RARE rule bv-shl-zero
-
BV_LSHR_ZERO
public static final ProofRewriteRule BV_LSHR_ZERO
Auto-generated from RARE rule bv-lshr-zero
-
BV_ASHR_ZERO
public static final ProofRewriteRule BV_ASHR_ZERO
Auto-generated from RARE rule bv-ashr-zero
-
BV_UGT_UREM
public static final ProofRewriteRule BV_UGT_UREM
Auto-generated from RARE rule bv-ugt-urem
-
BV_ULT_ONE
public static final ProofRewriteRule BV_ULT_ONE
Auto-generated from RARE rule bv-ult-one
-
BV_SLT_ZERO
public static final ProofRewriteRule BV_SLT_ZERO
Auto-generated from RARE rule bv-slt-zero
-
BV_MERGE_SIGN_EXTEND_1
public static final ProofRewriteRule BV_MERGE_SIGN_EXTEND_1
Auto-generated from RARE rule bv-merge-sign-extend-1
-
BV_MERGE_SIGN_EXTEND_2
public static final ProofRewriteRule BV_MERGE_SIGN_EXTEND_2
Auto-generated from RARE rule bv-merge-sign-extend-2
-
BV_MERGE_SIGN_EXTEND_3
public static final ProofRewriteRule BV_MERGE_SIGN_EXTEND_3
Auto-generated from RARE rule bv-merge-sign-extend-3
-
BV_SIGN_EXTEND_EQ_CONST_1
public static final ProofRewriteRule BV_SIGN_EXTEND_EQ_CONST_1
Auto-generated from RARE rule bv-sign-extend-eq--1
-
BV_SIGN_EXTEND_EQ_CONST_2
public static final ProofRewriteRule BV_SIGN_EXTEND_EQ_CONST_2
Auto-generated from RARE rule bv-sign-extend-eq--2
-
BV_ZERO_EXTEND_EQ_CONST_1
public static final ProofRewriteRule BV_ZERO_EXTEND_EQ_CONST_1
Auto-generated from RARE rule bv-zero-extend-eq--1
-
BV_ZERO_EXTEND_EQ_CONST_2
public static final ProofRewriteRule BV_ZERO_EXTEND_EQ_CONST_2
Auto-generated from RARE rule bv-zero-extend-eq--2
-
BV_SIGN_EXTEND_ULT_CONST_1
public static final ProofRewriteRule BV_SIGN_EXTEND_ULT_CONST_1
Auto-generated from RARE rule bv-sign-extend-ult--1
-
BV_SIGN_EXTEND_ULT_CONST_2
public static final ProofRewriteRule BV_SIGN_EXTEND_ULT_CONST_2
Auto-generated from RARE rule bv-sign-extend-ult--2
-
BV_SIGN_EXTEND_ULT_CONST_3
public static final ProofRewriteRule BV_SIGN_EXTEND_ULT_CONST_3
Auto-generated from RARE rule bv-sign-extend-ult--3
-
BV_SIGN_EXTEND_ULT_CONST_4
public static final ProofRewriteRule BV_SIGN_EXTEND_ULT_CONST_4
Auto-generated from RARE rule bv-sign-extend-ult--4
-
SETS_EQ_SINGLETON_EMP
public static final ProofRewriteRule SETS_EQ_SINGLETON_EMP
Auto-generated from RARE rule sets-eq-singleton-emp
-
SETS_MEMBER_SINGLETON
public static final ProofRewriteRule SETS_MEMBER_SINGLETON
Auto-generated from RARE rule sets-member-singleton
-
SETS_MEMBER_EMP
public static final ProofRewriteRule SETS_MEMBER_EMP
Auto-generated from RARE rule sets-member-emp
-
SETS_SUBSET_ELIM
public static final ProofRewriteRule SETS_SUBSET_ELIM
Auto-generated from RARE rule sets-subset-elim
-
SETS_UNION_COMM
public static final ProofRewriteRule SETS_UNION_COMM
Auto-generated from RARE rule sets-union-comm
-
SETS_INTER_COMM
public static final ProofRewriteRule SETS_INTER_COMM
Auto-generated from RARE rule sets-inter-comm
-
SETS_INTER_EMP1
public static final ProofRewriteRule SETS_INTER_EMP1
Auto-generated from RARE rule sets-inter-emp1
-
SETS_INTER_EMP2
public static final ProofRewriteRule SETS_INTER_EMP2
Auto-generated from RARE rule sets-inter-emp2
-
SETS_MINUS_EMP1
public static final ProofRewriteRule SETS_MINUS_EMP1
Auto-generated from RARE rule sets-minus-emp1
-
SETS_MINUS_EMP2
public static final ProofRewriteRule SETS_MINUS_EMP2
Auto-generated from RARE rule sets-minus-emp2
-
SETS_UNION_EMP1
public static final ProofRewriteRule SETS_UNION_EMP1
Auto-generated from RARE rule sets-union-emp1
-
SETS_UNION_EMP2
public static final ProofRewriteRule SETS_UNION_EMP2
Auto-generated from RARE rule sets-union-emp2
-
SETS_INTER_MEMBER
public static final ProofRewriteRule SETS_INTER_MEMBER
Auto-generated from RARE rule sets-inter-member
-
SETS_MINUS_MEMBER
public static final ProofRewriteRule SETS_MINUS_MEMBER
Auto-generated from RARE rule sets-minus-member
-
SETS_UNION_MEMBER
public static final ProofRewriteRule SETS_UNION_MEMBER
Auto-generated from RARE rule sets-union-member
-
SETS_CHOOSE_SINGLETON
public static final ProofRewriteRule SETS_CHOOSE_SINGLETON
Auto-generated from RARE rule sets-choose-singleton
-
SETS_CARD_SINGLETON
public static final ProofRewriteRule SETS_CARD_SINGLETON
Auto-generated from RARE rule sets-card-singleton
-
SETS_CARD_UNION
public static final ProofRewriteRule SETS_CARD_UNION
Auto-generated from RARE rule sets-card-union
-
SETS_CARD_MINUS
public static final ProofRewriteRule SETS_CARD_MINUS
Auto-generated from RARE rule sets-card-minus
-
SETS_CARD_EMP
public static final ProofRewriteRule SETS_CARD_EMP
Auto-generated from RARE rule sets-card-emp
-
SETS_MINUS_SELF
public static final ProofRewriteRule SETS_MINUS_SELF
Auto-generated from RARE rule sets-minus-self
-
SETS_IS_EMPTY_ELIM
public static final ProofRewriteRule SETS_IS_EMPTY_ELIM
Auto-generated from RARE rule sets-is-empty-elim
-
STR_EQ_CTN_FALSE
public static final ProofRewriteRule STR_EQ_CTN_FALSE
Auto-generated from RARE rule str-eq-ctn-false
-
STR_EQ_CTN_FULL_FALSE1
public static final ProofRewriteRule STR_EQ_CTN_FULL_FALSE1
Auto-generated from RARE rule str-eq-ctn-full-false1
-
STR_EQ_CTN_FULL_FALSE2
public static final ProofRewriteRule STR_EQ_CTN_FULL_FALSE2
Auto-generated from RARE rule str-eq-ctn-full-false2
-
STR_CONCAT_FLATTEN
public static final ProofRewriteRule STR_CONCAT_FLATTEN
Auto-generated from RARE rule str-concat-flatten
-
STR_CONCAT_FLATTEN_EQ
public static final ProofRewriteRule STR_CONCAT_FLATTEN_EQ
Auto-generated from RARE rule str-concat-flatten-eq
-
STR_CONCAT_FLATTEN_EQ_REV
public static final ProofRewriteRule STR_CONCAT_FLATTEN_EQ_REV
Auto-generated from RARE rule str-concat-flatten-eq-rev
-
STR_SUBSTR_EMPTY_STR
public static final ProofRewriteRule STR_SUBSTR_EMPTY_STR
Auto-generated from RARE rule str-substr-empty-str
-
STR_SUBSTR_EMPTY_RANGE
public static final ProofRewriteRule STR_SUBSTR_EMPTY_RANGE
Auto-generated from RARE rule str-substr-empty-range
-
STR_SUBSTR_EMPTY_START
public static final ProofRewriteRule STR_SUBSTR_EMPTY_START
Auto-generated from RARE rule str-substr-empty-start
-
STR_SUBSTR_EMPTY_START_NEG
public static final ProofRewriteRule STR_SUBSTR_EMPTY_START_NEG
Auto-generated from RARE rule str-substr-empty-start-neg
-
STR_SUBSTR_EQ_EMPTY
public static final ProofRewriteRule STR_SUBSTR_EQ_EMPTY
Auto-generated from RARE rule str-substr-eq-empty
-
STR_LEN_REPLACE_INV
public static final ProofRewriteRule STR_LEN_REPLACE_INV
Auto-generated from RARE rule str-len-replace-inv
-
STR_LEN_UPDATE_INV
public static final ProofRewriteRule STR_LEN_UPDATE_INV
Auto-generated from RARE rule str-len-update-inv
-
STR_LEN_SUBSTR_IN_RANGE
public static final ProofRewriteRule STR_LEN_SUBSTR_IN_RANGE
Auto-generated from RARE rule str-len-substr-in-range
-
STR_LEN_SUBSTR_UB1
public static final ProofRewriteRule STR_LEN_SUBSTR_UB1
Auto-generated from RARE rule str-len-substr-ub1
-
STR_LEN_SUBSTR_UB2
public static final ProofRewriteRule STR_LEN_SUBSTR_UB2
Auto-generated from RARE rule str-len-substr-ub2
-
STR_CONCAT_CLASH
public static final ProofRewriteRule STR_CONCAT_CLASH
Auto-generated from RARE rule str-concat-clash
-
STR_CONCAT_CLASH_REV
public static final ProofRewriteRule STR_CONCAT_CLASH_REV
Auto-generated from RARE rule str-concat-clash-rev
-
STR_CONCAT_CLASH2
public static final ProofRewriteRule STR_CONCAT_CLASH2
Auto-generated from RARE rule str-concat-clash2
-
STR_CONCAT_CLASH2_REV
public static final ProofRewriteRule STR_CONCAT_CLASH2_REV
Auto-generated from RARE rule str-concat-clash2-rev
-
STR_CONCAT_UNIFY
public static final ProofRewriteRule STR_CONCAT_UNIFY
Auto-generated from RARE rule str-concat-unify
-
STR_CONCAT_UNIFY_REV
public static final ProofRewriteRule STR_CONCAT_UNIFY_REV
Auto-generated from RARE rule str-concat-unify-rev
-
STR_CONCAT_UNIFY_BASE
public static final ProofRewriteRule STR_CONCAT_UNIFY_BASE
Auto-generated from RARE rule str-concat-unify-base
-
STR_CONCAT_UNIFY_BASE_REV
public static final ProofRewriteRule STR_CONCAT_UNIFY_BASE_REV
Auto-generated from RARE rule str-concat-unify-base-rev
-
STR_CONCAT_CLASH_CHAR
public static final ProofRewriteRule STR_CONCAT_CLASH_CHAR
Auto-generated from RARE rule str-concat-clash-char
-
STR_CONCAT_CLASH_CHAR_REV
public static final ProofRewriteRule STR_CONCAT_CLASH_CHAR_REV
Auto-generated from RARE rule str-concat-clash-char-rev
-
STR_PREFIXOF_ELIM
public static final ProofRewriteRule STR_PREFIXOF_ELIM
Auto-generated from RARE rule str-prefixof-elim
-
STR_SUFFIXOF_ELIM
public static final ProofRewriteRule STR_SUFFIXOF_ELIM
Auto-generated from RARE rule str-suffixof-elim
-
STR_PREFIXOF_ONE
public static final ProofRewriteRule STR_PREFIXOF_ONE
Auto-generated from RARE rule str-prefixof-one
-
STR_SUFFIXOF_ONE
public static final ProofRewriteRule STR_SUFFIXOF_ONE
Auto-generated from RARE rule str-suffixof-one
-
STR_SUBSTR_COMBINE1
public static final ProofRewriteRule STR_SUBSTR_COMBINE1
Auto-generated from RARE rule str-substr-combine1
-
STR_SUBSTR_COMBINE2
public static final ProofRewriteRule STR_SUBSTR_COMBINE2
Auto-generated from RARE rule str-substr-combine2
-
STR_SUBSTR_COMBINE3
public static final ProofRewriteRule STR_SUBSTR_COMBINE3
Auto-generated from RARE rule str-substr-combine3
-
STR_SUBSTR_COMBINE4
public static final ProofRewriteRule STR_SUBSTR_COMBINE4
Auto-generated from RARE rule str-substr-combine4
-
STR_SUBSTR_CONCAT1
public static final ProofRewriteRule STR_SUBSTR_CONCAT1
Auto-generated from RARE rule str-substr-concat1
-
STR_SUBSTR_CONCAT2
public static final ProofRewriteRule STR_SUBSTR_CONCAT2
Auto-generated from RARE rule str-substr-concat2
-
STR_SUBSTR_FULL
public static final ProofRewriteRule STR_SUBSTR_FULL
Auto-generated from RARE rule str-substr-full
-
STR_SUBSTR_FULL_EQ
public static final ProofRewriteRule STR_SUBSTR_FULL_EQ
Auto-generated from RARE rule str-substr-full-eq
-
STR_CONTAINS_REFL
public static final ProofRewriteRule STR_CONTAINS_REFL
Auto-generated from RARE rule str-contains-refl
-
STR_CONTAINS_CONCAT_FIND
public static final ProofRewriteRule STR_CONTAINS_CONCAT_FIND
Auto-generated from RARE rule str-contains-concat-find
-
STR_CONTAINS_SPLIT_CHAR
public static final ProofRewriteRule STR_CONTAINS_SPLIT_CHAR
Auto-generated from RARE rule str-contains-split-char
-
STR_CONTAINS_LT_LEN
public static final ProofRewriteRule STR_CONTAINS_LT_LEN
Auto-generated from RARE rule str-contains-lt-len
-
STR_CONTAINS_LEQ_LEN_EQ
public static final ProofRewriteRule STR_CONTAINS_LEQ_LEN_EQ
Auto-generated from RARE rule str-contains-leq-len-eq
-
STR_CONTAINS_EMP
public static final ProofRewriteRule STR_CONTAINS_EMP
Auto-generated from RARE rule str-contains-emp
-
STR_CONTAINS_IS_EMP
public static final ProofRewriteRule STR_CONTAINS_IS_EMP
Auto-generated from RARE rule str-contains-is-emp
-
STR_AT_ELIM
public static final ProofRewriteRule STR_AT_ELIM
Auto-generated from RARE rule str-at-elim
-
STR_REPLACE_SELF
public static final ProofRewriteRule STR_REPLACE_SELF
Auto-generated from RARE rule str-replace-self
-
STR_REPLACE_PREFIX
public static final ProofRewriteRule STR_REPLACE_PREFIX
Auto-generated from RARE rule str-replace-prefix
-
STR_REPLACE_NO_CONTAINS
public static final ProofRewriteRule STR_REPLACE_NO_CONTAINS
Auto-generated from RARE rule str-replace-no-contains
-
STR_REPLACE_EMPTY
public static final ProofRewriteRule STR_REPLACE_EMPTY
Auto-generated from RARE rule str-replace-empty
-
STR_REPLACE_CONTAINS_PRE
public static final ProofRewriteRule STR_REPLACE_CONTAINS_PRE
Auto-generated from RARE rule str-replace-contains-pre
-
STR_REPLACE_ALL_NO_CONTAINS
public static final ProofRewriteRule STR_REPLACE_ALL_NO_CONTAINS
Auto-generated from RARE rule str-replace-all-no-contains
-
STR_REPLACE_RE_NONE
public static final ProofRewriteRule STR_REPLACE_RE_NONE
Auto-generated from RARE rule str-replace-re-none
-
STR_REPLACE_RE_ALL_NONE
public static final ProofRewriteRule STR_REPLACE_RE_ALL_NONE
Auto-generated from RARE rule str-replace-re-all-none
-
STR_LEN_CONCAT_REC
public static final ProofRewriteRule STR_LEN_CONCAT_REC
Auto-generated from RARE rule str-len-concat-rec
-
STR_INDEXOF_SELF
public static final ProofRewriteRule STR_INDEXOF_SELF
Auto-generated from RARE rule str-indexof-self
-
STR_INDEXOF_NO_CONTAINS
public static final ProofRewriteRule STR_INDEXOF_NO_CONTAINS
Auto-generated from RARE rule str-indexof-no-contains
-
STR_INDEXOF_CONTAINS_PRE
public static final ProofRewriteRule STR_INDEXOF_CONTAINS_PRE
Auto-generated from RARE rule str-indexof-contains-pre
-
STR_INDEXOF_RE_NONE
public static final ProofRewriteRule STR_INDEXOF_RE_NONE
Auto-generated from RARE rule str-indexof-re-none
-
STR_TO_LOWER_CONCAT
public static final ProofRewriteRule STR_TO_LOWER_CONCAT
Auto-generated from RARE rule str-to-lower-concat
-
STR_TO_UPPER_CONCAT
public static final ProofRewriteRule STR_TO_UPPER_CONCAT
Auto-generated from RARE rule str-to-upper-concat
-
STR_TO_LOWER_UPPER
public static final ProofRewriteRule STR_TO_LOWER_UPPER
Auto-generated from RARE rule str-to-lower-upper
-
STR_TO_UPPER_LOWER
public static final ProofRewriteRule STR_TO_UPPER_LOWER
Auto-generated from RARE rule str-to-upper-lower
-
STR_TO_LOWER_LEN
public static final ProofRewriteRule STR_TO_LOWER_LEN
Auto-generated from RARE rule str-to-lower-len
-
STR_TO_UPPER_LEN
public static final ProofRewriteRule STR_TO_UPPER_LEN
Auto-generated from RARE rule str-to-upper-len
-
STR_TO_LOWER_FROM_INT
public static final ProofRewriteRule STR_TO_LOWER_FROM_INT
Auto-generated from RARE rule str-to-lower-from-int
-
STR_TO_UPPER_FROM_INT
public static final ProofRewriteRule STR_TO_UPPER_FROM_INT
Auto-generated from RARE rule str-to-upper-from-int
-
STR_TO_INT_CONCAT_NEG_ONE
public static final ProofRewriteRule STR_TO_INT_CONCAT_NEG_ONE
Auto-generated from RARE rule str-to-int-concat-neg-one
-
STR_LEQ_EMPTY
public static final ProofRewriteRule STR_LEQ_EMPTY
Auto-generated from RARE rule str-leq-empty
-
STR_LEQ_EMPTY_EQ
public static final ProofRewriteRule STR_LEQ_EMPTY_EQ
Auto-generated from RARE rule str-leq-empty-eq
-
STR_LEQ_CONCAT_FALSE
public static final ProofRewriteRule STR_LEQ_CONCAT_FALSE
Auto-generated from RARE rule str-leq-concat-false
-
STR_LEQ_CONCAT_TRUE
public static final ProofRewriteRule STR_LEQ_CONCAT_TRUE
Auto-generated from RARE rule str-leq-concat-true
-
STR_LT_ELIM
public static final ProofRewriteRule STR_LT_ELIM
Auto-generated from RARE rule str-lt-elim
-
RE_ALL_ELIM
public static final ProofRewriteRule RE_ALL_ELIM
Auto-generated from RARE rule re-all-elim
-
RE_OPT_ELIM
public static final ProofRewriteRule RE_OPT_ELIM
Auto-generated from RARE rule re-opt-elim
-
RE_DIFF_ELIM
public static final ProofRewriteRule RE_DIFF_ELIM
Auto-generated from RARE rule re-diff-elim
-
RE_CONCAT_EMP
public static final ProofRewriteRule RE_CONCAT_EMP
Auto-generated from RARE rule re-concat-emp
-
RE_CONCAT_NONE
public static final ProofRewriteRule RE_CONCAT_NONE
Auto-generated from RARE rule re-concat-none
-
RE_CONCAT_FLATTEN
public static final ProofRewriteRule RE_CONCAT_FLATTEN
Auto-generated from RARE rule re-concat-flatten
-
RE_CONCAT_STAR_SWAP
public static final ProofRewriteRule RE_CONCAT_STAR_SWAP
Auto-generated from RARE rule re-concat-star-swap
-
RE_CONCAT_STAR_REPEAT
public static final ProofRewriteRule RE_CONCAT_STAR_REPEAT
Auto-generated from RARE rule re-concat-star-repeat
-
RE_CONCAT_MERGE
public static final ProofRewriteRule RE_CONCAT_MERGE
Auto-generated from RARE rule re-concat-merge
-
RE_UNION_ALL
public static final ProofRewriteRule RE_UNION_ALL
Auto-generated from RARE rule re-union-all
-
RE_UNION_NONE
public static final ProofRewriteRule RE_UNION_NONE
Auto-generated from RARE rule re-union-none
-
RE_UNION_FLATTEN
public static final ProofRewriteRule RE_UNION_FLATTEN
Auto-generated from RARE rule re-union-flatten
-
RE_UNION_DUP
public static final ProofRewriteRule RE_UNION_DUP
Auto-generated from RARE rule re-union-dup
-
RE_INTER_ALL
public static final ProofRewriteRule RE_INTER_ALL
Auto-generated from RARE rule re-inter-all
-
RE_INTER_NONE
public static final ProofRewriteRule RE_INTER_NONE
Auto-generated from RARE rule re-inter-none
-
RE_INTER_FLATTEN
public static final ProofRewriteRule RE_INTER_FLATTEN
Auto-generated from RARE rule re-inter-flatten
-
RE_INTER_DUP
public static final ProofRewriteRule RE_INTER_DUP
Auto-generated from RARE rule re-inter-dup
-
RE_STAR_NONE
public static final ProofRewriteRule RE_STAR_NONE
Auto-generated from RARE rule re-star-none
-
RE_LOOP_NEG
public static final ProofRewriteRule RE_LOOP_NEG
Auto-generated from RARE rule re-loop-neg
-
RE_INTER_CSTRING
public static final ProofRewriteRule RE_INTER_CSTRING
Auto-generated from RARE rule re-inter-cstring
-
RE_INTER_CSTRING_NEG
public static final ProofRewriteRule RE_INTER_CSTRING_NEG
Auto-generated from RARE rule re-inter-cstring-neg
-
STR_SUBSTR_LEN_INCLUDE
public static final ProofRewriteRule STR_SUBSTR_LEN_INCLUDE
Auto-generated from RARE rule str-substr-len-include
-
STR_SUBSTR_LEN_INCLUDE_PRE
public static final ProofRewriteRule STR_SUBSTR_LEN_INCLUDE_PRE
Auto-generated from RARE rule str-substr-len-include-pre
-
STR_SUBSTR_LEN_SKIP
public static final ProofRewriteRule STR_SUBSTR_LEN_SKIP
Auto-generated from RARE rule str-substr-len-skip
-
SEQ_LEN_REV
public static final ProofRewriteRule SEQ_LEN_REV
Auto-generated from RARE rule seq-len-rev
-
SEQ_REV_REV
public static final ProofRewriteRule SEQ_REV_REV
Auto-generated from RARE rule seq-rev-rev
-
SEQ_REV_CONCAT
public static final ProofRewriteRule SEQ_REV_CONCAT
Auto-generated from RARE rule seq-rev-concat
-
SEQ_LEN_UNIT
public static final ProofRewriteRule SEQ_LEN_UNIT
Auto-generated from RARE rule seq-len-unit
-
SEQ_NTH_UNIT
public static final ProofRewriteRule SEQ_NTH_UNIT
Auto-generated from RARE rule seq-nth-unit
-
SEQ_REV_UNIT
public static final ProofRewriteRule SEQ_REV_UNIT
Auto-generated from RARE rule seq-rev-unit
-
SEQ_LEN_EMPTY
public static final ProofRewriteRule SEQ_LEN_EMPTY
Auto-generated from RARE rule seq-len-empty
-
RE_IN_EMPTY
public static final ProofRewriteRule RE_IN_EMPTY
Auto-generated from RARE rule re-in-empty
-
RE_IN_SIGMA
public static final ProofRewriteRule RE_IN_SIGMA
Auto-generated from RARE rule re-in-sigma
-
RE_IN_SIGMA_STAR
public static final ProofRewriteRule RE_IN_SIGMA_STAR
Auto-generated from RARE rule re-in-sigma-star
-
RE_IN_CSTRING
public static final ProofRewriteRule RE_IN_CSTRING
Auto-generated from RARE rule re-in-cstring
-
RE_IN_COMP
public static final ProofRewriteRule RE_IN_COMP
Auto-generated from RARE rule re-in-comp
-
STR_IN_RE_UNION_ELIM
public static final ProofRewriteRule STR_IN_RE_UNION_ELIM
Auto-generated from RARE rule str-in-re-union-elim
-
STR_IN_RE_INTER_ELIM
public static final ProofRewriteRule STR_IN_RE_INTER_ELIM
Auto-generated from RARE rule str-in-re-inter-elim
-
STR_IN_RE_RANGE_ELIM
public static final ProofRewriteRule STR_IN_RE_RANGE_ELIM
Auto-generated from RARE rule str-in-re-range-elim
-
STR_IN_RE_CONTAINS
public static final ProofRewriteRule STR_IN_RE_CONTAINS
Auto-generated from RARE rule str-in-re-contains
-
STR_IN_RE_STRIP_PREFIX
public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX
Auto-generated from RARE rule str-in-re-strip-prefix
-
STR_IN_RE_STRIP_PREFIX_NEG
public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_NEG
Auto-generated from RARE rule str-in-re-strip-prefix-neg
-
STR_IN_RE_STRIP_PREFIX_SR_SINGLE
public static final ProofRewriteRule 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
public static final ProofRewriteRule 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_SRS_SINGLE
public static final ProofRewriteRule 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
public static final ProofRewriteRule 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_S_SINGLE
public static final ProofRewriteRule 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
public static final ProofRewriteRule 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_BASE
public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_BASE
Auto-generated from RARE rule str-in-re-strip-prefix-base
-
STR_IN_RE_STRIP_PREFIX_BASE_NEG
public static final ProofRewriteRule 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_S_SINGLE
public static final ProofRewriteRule 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
public static final ProofRewriteRule 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_CHAR
public static final ProofRewriteRule STR_IN_RE_STRIP_CHAR
Auto-generated from RARE rule str-in-re-strip-char
-
STR_IN_RE_STRIP_CHAR_S_SINGLE
public static final ProofRewriteRule STR_IN_RE_STRIP_CHAR_S_SINGLE
Auto-generated from RARE rule str-in-re-strip-char-s-single
-
STR_IN_RE_STRIP_PREFIX_REV
public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_REV
Auto-generated from RARE rule str-in-re-strip-prefix-rev
-
STR_IN_RE_STRIP_PREFIX_NEG_REV
public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_NEG_REV
Auto-generated from RARE rule str-in-re-strip-prefix-neg-rev
-
STR_IN_RE_STRIP_PREFIX_SR_SINGLE_REV
public static final ProofRewriteRule 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_SR_SINGLE_NEG_REV
public static final ProofRewriteRule 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_SRS_SINGLE_REV
public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_SRS_SINGLE_REV
Auto-generated from RARE rule str-in-re-strip-prefix-srs-single-rev
-
STR_IN_RE_STRIP_PREFIX_SRS_SINGLE_NEG_REV
public static final ProofRewriteRule 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_S_SINGLE_REV
public static final ProofRewriteRule 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_S_SINGLE_NEG_REV
public static final ProofRewriteRule 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_BASE_REV
public static final ProofRewriteRule 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_NEG_REV
public static final ProofRewriteRule 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_S_SINGLE_REV
public static final ProofRewriteRule 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_BASE_S_SINGLE_NEG_REV
public static final ProofRewriteRule 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_CHAR_REV
public static final ProofRewriteRule STR_IN_RE_STRIP_CHAR_REV
Auto-generated from RARE rule str-in-re-strip-char-rev
-
STR_IN_RE_STRIP_CHAR_S_SINGLE_REV
public static final ProofRewriteRule STR_IN_RE_STRIP_CHAR_S_SINGLE_REV
Auto-generated from RARE rule str-in-re-strip-char-s-single-rev
-
STR_IN_RE_REQ_UNFOLD
public static final ProofRewriteRule STR_IN_RE_REQ_UNFOLD
Auto-generated from RARE rule str-in-re-req-unfold
-
STR_IN_RE_REQ_UNFOLD_REV
public static final ProofRewriteRule STR_IN_RE_REQ_UNFOLD_REV
Auto-generated from RARE rule str-in-re-req-unfold-rev
-
STR_IN_RE_SKIP_UNFOLD
public static final ProofRewriteRule STR_IN_RE_SKIP_UNFOLD
Auto-generated from RARE rule str-in-re-skip-unfold
-
STR_IN_RE_SKIP_UNFOLD_REV
public static final ProofRewriteRule STR_IN_RE_SKIP_UNFOLD_REV
Auto-generated from RARE rule str-in-re-skip-unfold-rev
-
STR_IN_RE_TEST_UNFOLD
public static final ProofRewriteRule STR_IN_RE_TEST_UNFOLD
Auto-generated from RARE rule str-in-re-test-unfold
-
STR_IN_RE_TEST_UNFOLD_REV
public static final ProofRewriteRule STR_IN_RE_TEST_UNFOLD_REV
Auto-generated from RARE rule str-in-re-test-unfold-rev
-
EQ_REFL
public static final ProofRewriteRule EQ_REFL
Auto-generated from RARE rule eq-refl
-
EQ_SYMM
public static final ProofRewriteRule EQ_SYMM
Auto-generated from RARE rule eq-symm
-
EQ_COND_DEQ
public static final ProofRewriteRule EQ_COND_DEQ
Auto-generated from RARE rule eq-cond-deq
-
EQ_ITE_LIFT
public static final ProofRewriteRule EQ_ITE_LIFT
Auto-generated from RARE rule eq-ite-lift
-
DISTINCT_BINARY_ELIM
public static final ProofRewriteRule DISTINCT_BINARY_ELIM
Auto-generated from RARE rule distinct-binary-elim
-
UF_BV2NAT_INT2BV
public static final ProofRewriteRule UF_BV2NAT_INT2BV
Auto-generated from RARE rule uf-bv2nat-int2bv
-
UF_BV2NAT_INT2BV_EXTEND
public static final ProofRewriteRule UF_BV2NAT_INT2BV_EXTEND
Auto-generated from RARE rule uf-bv2nat-int2bv-extend
-
UF_BV2NAT_INT2BV_EXTRACT
public static final ProofRewriteRule UF_BV2NAT_INT2BV_EXTRACT
Auto-generated from RARE rule uf-bv2nat-int2bv-extract
-
UF_INT2BV_BV2NAT
public static final ProofRewriteRule UF_INT2BV_BV2NAT
Auto-generated from RARE rule uf-int2bv-bv2nat
-
UF_BV2NAT_GEQ_ELIM
public static final ProofRewriteRule UF_BV2NAT_GEQ_ELIM
Auto-generated from RARE rule uf-bv2nat-geq-elim
-
UF_INT2BV_BVULT_EQUIV
public static final ProofRewriteRule UF_INT2BV_BVULT_EQUIV
Auto-generated from RARE rule uf-int2bv-bvult-equiv
-
UF_INT2BV_BVULE_EQUIV
public static final ProofRewriteRule UF_INT2BV_BVULE_EQUIV
Auto-generated from RARE rule uf-int2bv-bvule-equiv
-
-
Method Detail
-
values
public static ProofRewriteRule[] values()
Returns an array containing the constants of this enum type, in the order they are declared. This method may be used to iterate over the constants as follows:for (ProofRewriteRule c : ProofRewriteRule.values()) System.out.println(c);
- Returns:
- an array containing the constants of this enum type, in the order they are declared
-
valueOf
public static ProofRewriteRule valueOf(java.lang.String name)
Returns the enum constant of this type with the specified name. The string must match exactly an identifier used to declare an enum constant in this type. (Extraneous whitespace characters are not permitted.)- Parameters:
name- the name of the enum constant to be returned.- Returns:
- the enum constant with the specified name
- Throws:
java.lang.IllegalArgumentException- if this enum type has no constant with the specified namejava.lang.NullPointerException- if the argument is null
-
fromInt
public static ProofRewriteRule fromInt(int value) throws CVC5ApiException
- Throws:
CVC5ApiException
-
getValue
public int getValue()
-
-