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_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_ZERO_INTAuto-generated from RARE rule arith-div-total-zero-intARITH_DIV_TOTAL_ZERO_REALAuto-generated from RARE rule arith-div-total-zero-realARITH_DIVISIBLE_ELIMAuto-generated from RARE rule arith-divisible-elimARITH_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_ITE_LIFTAuto-generated from RARE rule arith-geq-ite-liftARITH_GEQ_NORM1_INTAuto-generated from RARE rule arith-geq-norm1-intARITH_GEQ_NORM1_REALAuto-generated from RARE rule arith-geq-norm1-realARITH_GEQ_TIGHTENAuto-generated from RARE rule arith-geq-tightenARITH_INT_DIV_TOTALAuto-generated from RARE rule arith-int-div-totalARITH_INT_DIV_TOTAL_NEGAuto-generated from RARE rule arith-int-div-total-negARITH_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_EQ_CONFLICTAuto-generated from RARE rule arith-int-eq-conflictARITH_INT_GEQ_TIGHTENAuto-generated from RARE rule arith-int-geq-tightenARITH_INT_MOD_TOTALAuto-generated from RARE rule arith-int-mod-totalARITH_INT_MOD_TOTAL_NEGAuto-generated from RARE rule arith-int-mod-total-negARITH_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_ITE_LIFTAuto-generated from RARE rule arith-leq-ite-liftARITH_LEQ_NORMAuto-generated from RARE rule arith-leq-normARITH_MAX_GEQ1Auto-generated from RARE rule arith-max-geq1ARITH_MAX_GEQ2Auto-generated from RARE rule arith-max-geq2ARITH_MIN_LT1Auto-generated from RARE rule arith-min-lt1ARITH_MIN_LT2Auto-generated from RARE rule arith-min-lt2ARITH_MOD_OVER_MODAuto-generated from RARE rule arith-mod-over-modARITH_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_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_ELIMAuto-generated from RARE rule arith-to-int-elimARITH_TO_INT_ELIM_TO_REALAuto-generated from RARE rule arith-to-int-elim-to-realARRAY_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-selfARRAY_STORE_SWAPAuto-generated from RARE rule array-store-swapARRAYS_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\} \] or alternatively \[ ((\lambda x_1 \ldots x_n.\> t) \ t_1) = (\lambda x_2 \ldots x_n.\> t)\{x_1 \mapsto t_1\} \] In the former case, the left hand side may either be a term of kind `cvc5.Kind.APPLY_UF` or `cvc5.Kind.HO_APPLY`.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_FLATTENAuto-generated from RARE rule boolean-and-flattenBOOL_DOUBLE_NOT_ELIMAuto-generated from RARE rule boolean-double-not-elimBOOL_DUAL_IMPL_EQAuto-generated from RARE rule boolean-dual-impl-eqBOOL_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_IMPLIES_OR_DISTRIBAuto-generated from RARE rule boolean-implies-or-distribBOOL_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_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_AND_CONCAT_PULLUPAuto-generated from RARE rule bv-and-concat-pullupBV_AND_CONCAT_PULLUP2Auto-generated from RARE rule bv-and-concat-pullup2BV_AND_CONCAT_PULLUP3Auto-generated from RARE rule bv-and-concat-pullup3BV_AND_SIMPLIFY_1Auto-generated from RARE rule bv-and-simplify-1BV_AND_SIMPLIFY_2Auto-generated from RARE rule bv-and-simplify-2BV_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_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_COMPAuto-generated from RARE rule bv-commutative-compBV_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_EQ_NOT_SOLVEAuto-generated from RARE rule bv-eq-not-solveBV_EQ_XOR_SOLVEAuto-generated from RARE rule bv-eq-xor-solveBV_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_ITE_WIDTH_ONEAuto-generated from RARE rule bv-ite-width-oneBV_ITE_WIDTH_ONE_NOTAuto-generated from RARE rule bv-ite-width-one-notBV_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_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_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_NEGO_ELIMINATEAuto-generated from RARE rule bv-nego-eliminateBV_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_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_CONCAT_PULLUP2Auto-generated from RARE rule bv-or-concat-pullup2BV_OR_CONCAT_PULLUP3Auto-generated from RARE rule bv-or-concat-pullup3BV_OR_SIMPLIFY_1Auto-generated from RARE rule bv-or-simplify-1BV_OR_SIMPLIFY_2Auto-generated from RARE rule bv-or-simplify-2BV_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_ELIMBitvectors – Unsigned multiplication overflow detection elimination \[ \texttt{bvsmulo}(x,y) = t \] where \(t\) is the result of eliminating the application of \(\texttt{bvsmulo}\).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_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_ELIMBitvectors – Unsigned multiplication overflow detection elimination \[ \texttt{bvumulo}(x,y) = t \] where \(t\) is the result of eliminating the application of \(\texttt{bvumulo}\).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_CONCAT_PULLUP2Auto-generated from RARE rule bv-xor-concat-pullup2BV_XOR_CONCAT_PULLUP3Auto-generated from RARE rule bv-xor-concat-pullup3BV_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_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_EXTEND_ULT_CONST_1Auto-generated from RARE rule bv-zero-extend-ult--1BV_ZERO_EXTEND_ULT_CONST_2Auto-generated from RARE rule bv-zero-extend-ult--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_INT_EQ_CONFLICTArithmetic – Integer equality conflict \[ (t=s) = \bot \] where \(t=s\) is equivalent (via ARITH_POLY_NORM <cvc5.ProofRule.ARITH_POLY_NORM>) to \((r = c)\) where \(r\) is an integral term and \(c\) is a non-integral constant.MACRO_ARITH_INT_GEQ_TIGHTENArithmetic – Integer inequality tightening \[ (t \geq s) = ( r \geq \lceil c \rceil) \] or \[ (t \geq s) = \neg( r \geq \lceil c \rceil) \] where \(t \geq s\) is equivalent (via ARITH_POLY_NORM <cvc5.ProofRule.ARITH_POLY_NORM>) to the right hand side where \(r\) is an integral term and \(c\) is a non-integral constant.MACRO_ARITH_STRING_PRED_ENTAILArithmetic – strings predicate entailment \[ (= s t) = c \] \[ (>= s t) = c \] where \(c\) is a Boolean constant.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_ARRAYS_NORMALIZE_OPArrays – Macro normalize operation \[ A = B \] where \(B\) is the result of normalizing the array operation \(A\) into a canonical form, based on commutativity of disjoint indices.MACRO_BOOL_BV_INVERT_SOLVEBooleans – Bitvector invert solve \[ ((t_1 = t_2) = (x = r)) = \top \] where \(x\) occurs on an invertible path in \(t_1 = t_2\) and has solved form \(r\).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_BV_AND_OR_XOR_CONCAT_PULLUPBitvectors – Macro and/or/xor concat pullup \[ a = b \] where \(a\) is rewritten to \(b\) by the internal rewrite rule AndOrXorConcatPullup.MACRO_BV_AND_SIMPLIFYBitvectors – Macro and simplify \[ a = b \] where \(a\) is rewritten to \(b\) by the internal rewrite rule AndSimplify.MACRO_BV_CONCAT_CONSTANT_MERGEBitvectors – Macro concat constant merge \[ a = b \] where \(a\) is rewritten to \(b\) by the internal rewrite rule ConcatConstantMerge.MACRO_BV_CONCAT_EXTRACT_MERGEBitvectors – Macro concat extract merge \[ a = b \] where \(a\) is rewritten to \(b\) by the internal rewrite rule ConcatExtractMerge.MACRO_BV_EQ_SOLVEBitvectors – Macro equality solve \[ (a = b) = \bot \] where \(bvsub(a,b)\) normalizes to a non-zero constant, or alternatively \[ (a = b) = \top \] where \(bvsub(a,b)\) normalizes to zero.MACRO_BV_EXTRACT_CONCATBitvectors – Macro extract and concat \[ a = b \] where \(a\) is rewritten to \(b\) by the internal rewrite rule ExtractConcat.MACRO_BV_MULT_SLT_MULTBitvectors – Macro multiply signed less than multiply \[ a = b \] where \(a\) is rewritten to \(b\) by the internal rewrite rule MultSltMult.MACRO_BV_OR_SIMPLIFYBitvectors – Macro or simplify \[ a = b \] where \(a\) is rewritten to \(b\) by the internal rewrite rule OrSimplify.MACRO_BV_XOR_SIMPLIFYBitvectors – Macro xor simplify \[ a = b \] where \(a\) is rewritten to \(b\) by the internal rewrite rule XorSimplify.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_LAMBDA_CAPTURE_AVOIDEquality – Macro lambda application capture avoid \[ ((\lambda x_1 \ldots x_n.\> t) \ t_1 \ldots t_n) = ((\lambda y_1 \ldots y_n.\> t') \ t_1 \ldots t_n) \] The terms may either be of kind `cvc5.Kind.APPLY_UF` or `cvc5.Kind.HO_APPLY`.MACRO_QUANT_DT_VAR_EXPANDQuantifiers – Macro datatype variable expand \[ (\forall Y x Z.\> F) = (\forall Y X_1 Z.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 \(F\) is a disjunction and where \(G\) is the result of dropping all literals containing \(x\).MACRO_RE_INTER_UNION_CONST_ELIMStrings – Macro regular expression intersection/union constant elimination One of the following forms: \[ \mathit{re.union}(R) = \mathit{re.union}(R') \] where \(R\) is a list of regular expressions containing \(R_i\) and \(\mathit{str.to_re(c)}\) where \(c\) is a string in \(R_i\) and \(R'\) is the result of removing \(\mathit{str.to_re(c)}\) from \(R\).MACRO_RE_INTER_UNION_INCLUSIONStrings – regular expression intersection/union inclusion \[ \mathit{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`.MACRO_STR_COMPONENT_CTNStrings – Macro string component contains \[ \mathit{str.contains}(t, s) = \top \] where a substring of \(t\) can be inferred to be a superstring of \(s\) based on iterating on components of string concatenation terms as well as prefix and suffix reasoning.MACRO_STR_CONST_NCTN_CONCATStrings – Macro string constant no contains concatenation \[ \mathit{str.contains}(c, \mathit{str.++}(t_1, \ldots, t_n)) = \bot \] where \(c\) is not contained in \(R_t\), where the regular expression \(R_t\) overapproximates the possible values of \(\mathit{str.++}(t_1, \ldots, t_n)\).MACRO_STR_EQ_LEN_UNIFYStrings – String equality length unify \[ (\mathit{str}.\text{++}(s_1, \ldots, s_n) = \mathit{str}.\text{++}(t_1, \ldots, t_m)) = (r_1 = u_1 \wedge \ldots r_k = u_k) \] where for each \(i = 1, \ldots, k\), we can show the length of \(r_i\) and \(u_i\) are equal, \(s_1, \ldots, s_n\) is \(r_1, \ldots, r_k\), and \(t_1, \ldots, t_m\) is \(u_1, \ldots, u_k\).MACRO_STR_EQ_LEN_UNIFY_PREFIXStrings – String equality length unify prefix \[ (s = \mathit{str}.\text{++}(t_1, \ldots, t_n)) = (s = \mathit{str}.\text{++}(t_1, \ldots t_i)) \wedge t_{i+1} = \epsilon \wedge \ldots \wedge t_n = \epsilon \] where we can show \(s\) has a length that is at least the length of \(\text{++}(t_1, \ldots t_i)\).MACRO_STR_IN_RE_INCLUSIONStrings – Macro string in regular expression inclusion \[ \mathit{str.in_re}(s, R) = \top \] where \(R\) includes the regular expression \(R_s\) which overapproximates the possible values of string \(s\).MACRO_STR_SPLIT_CTNStrings – Macro string split contains \[ \mathit{str.contains}(t, s) = \mathit{str.contains}(t_1, s) \vee \mathit{str.contains}(t_2, s) \] where \(t_1\) and \(t_2\) are substrings of \(t\).MACRO_STR_STRIP_ENDPOINTSStrings – Macro string strip endpoints One of the following forms: \[ \mathit{str.contains}(t, s) = \mathit{str.contains}(t_2, s) \] \[ \mathit{str.indexof}(t, s, n) = \mathit{str.indexof}(t_2, s, n) \] \[ \mathit{str.replace}(t, s, r) = \mathit{str.++}(t_1, \mathit{str.replace}(t_2, s, r) t_3) \] where in each case we reason about removing portions of \(t\) that are irrelevant to the evaluation of the term.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_MERGEAuto-generated from RARE rule re-concat-mergeRE_CONCAT_STAR_REPEATAuto-generated from RARE rule re-concat-star-repeatRE_CONCAT_STAR_SUBSUME1Auto-generated from RARE rule re-concat-star-subsume1RE_CONCAT_STAR_SUBSUME2Auto-generated from RARE rule re-concat-star-subsume2RE_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_INCLUSIONStrings – regular expression intersection inclusion \[ \mathit{re.inter}(r_1, re.comp(r_2)) = \mathit{re.none} \] 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_PLUS_ELIMAuto-generated from RARE rule re-plus-elimRE_STAR_EMPAuto-generated from RARE rule re-star-empRE_STAR_NONEAuto-generated from RARE rule re-star-noneRE_STAR_STARAuto-generated from RARE rule re-star-starRE_STAR_UNION_DROP_EMPAuto-generated from RARE rule re-star-union-drop-empRE_UNION_ALLAuto-generated from RARE rule re-union-allRE_UNION_CONST_ELIMAuto-generated from RARE rule re-union--elimRE_UNION_INCLUSIONStrings – regular expression union inclusion \[ \mathit{re.union}(r_1, re.comp(r_2)) = \mathit{re}.\text{*}(\mathit{re.allchar}) \] where \(r_1\) is a superset of \(r_2\).SEQ_EVAL_OPStrings – Sequence evaluate operator \[ f(s_1, \ldots, s_n) = t \] where \(f\) is an operator over sequences and \(s_1, \ldots, s_n\) are values, that is, the Node.isConst method returns true for each, and \(t\) is the result of evaluating \(f\) on them.SEQ_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_EVAL_OPSets – sets evaluate operator \[ \mathit{f}(t_1, t_2) = t \] where \(f\) is one of \(\mathit{set.inter}, \mathit{set.minus}, \mathit{set.union}\), and \(t\) is the result of evaluating \(f\) on \(t_1\) and \(t_2\).SETS_INSERT_ELIMSets – sets insert elimination \[ \mathit{set.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_SINGLETON_ELIMAuto-generated from RARE rule sets-is-singleton-elimSETS_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_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_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_CHARAuto-generated from RARE rule str-contains-charSTR_CONTAINS_CONCAT_FINDAuto-generated from RARE rule str-contains-concat-findSTR_CONTAINS_CONCAT_FIND_CONTRAAuto-generated from RARE rule str-contains-concat-find-contraSTR_CONTAINS_EMPAuto-generated from RARE rule str-contains-empSTR_CONTAINS_LEQ_LEN_EQAuto-generated from RARE rule str-contains-leq-len-eqSTR_CONTAINS_REFLAuto-generated from RARE rule str-contains-reflSTR_CONTAINS_REPL_CHARAuto-generated from RARE rule str-contains-repl-charSTR_CONTAINS_REPL_SELFAuto-generated from RARE rule str-contains-repl-selfSTR_CONTAINS_REPL_SELF_TGT_CHARAuto-generated from RARE rule str-contains-repl-self-tgt-charSTR_CONTAINS_REPL_TGTAuto-generated from RARE rule str-contains-repl-tgtSTR_CONTAINS_SPLIT_CHARAuto-generated from RARE rule str-contains-split-charSTR_CTN_MULTISET_SUBSETStrings – String contains multiset subset \[ \mathit{str}.contains(s,t) = \bot \] where the multiset overapproximation of \(s\) can be shown to not contain the multiset abstraction of \(t\) based on the reasoning described in the paper Reynolds et al, CAV 2019, "High-Level Abstractions for Simplifying Extended String Constraints in SMT".STR_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_EQ_LEN_FALSEAuto-generated from RARE rule str-eq-len-falseSTR_EQ_REPL_EMP_TGT_NEMPAuto-generated from RARE rule str-eq-repl-emp-tgt-nempSTR_EQ_REPL_LEN_ONE_EMP_PREFIXAuto-generated from RARE rule str-eq-repl-len-one-emp-prefixSTR_EQ_REPL_NEMP_SRC_EMPAuto-generated from RARE rule str-eq-repl-nemp-src-empSTR_EQ_REPL_NO_CHANGEAuto-generated from RARE rule str-eq-repl-no-changeSTR_EQ_REPL_SELF_EMPAuto-generated from RARE rule str-eq-repl-self-empSTR_EQ_REPL_SELF_SRCAuto-generated from RARE rule str-eq-repl-self-srcSTR_EQ_REPL_TGT_EQ_LENAuto-generated from RARE rule str-eq-repl-tgt-eq-lenSTR_FROM_INT_NO_CTN_NONDIGITAuto-generated from RARE rule str-from-int-no-ctn-nondigitSTR_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_FROM_INT_DIG_RANGEAuto-generated from RARE rule str-in-re-from-int-dig-rangeSTR_IN_RE_FROM_INT_NEMP_DIG_RANGEAuto-generated from RARE rule str-in-re-from-int-nemp-dig-rangeSTR_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_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_UNION_ELIMAuto-generated from RARE rule str-in-re-union-elimSTR_INDEXOF_CONTAINS_PREAuto-generated from RARE rule str-indexof-contains-preSTR_INDEXOF_EQ_IRRAuto-generated from RARE rule str-indexof-eq-irrSTR_INDEXOF_FIND_EMPAuto-generated from RARE rule str-indexof-find-empSTR_INDEXOF_NO_CONTAINSAuto-generated from RARE rule str-indexof-no-containsSTR_INDEXOF_OOBAuto-generated from RARE rule str-indexof-oobSTR_INDEXOF_OOB2Auto-generated from RARE rule str-indexof-oob2STR_INDEXOF_RE_EMP_REAuto-generated from RARE rule str-indexof-re-emp-reSTR_INDEXOF_RE_EVALStrings – string indexof regex evaluation \[ str.indexof\_re(s,r,n) = m \] where \(s\) is a string values, \(n\) is an integer value, \(r\) is a ground regular expression and \(m\) is the result of evaluating the left hand side.STR_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_EQ_ZERO_BASEAuto-generated from RARE rule str-len-eq-zero-baseSTR_LEN_EQ_ZERO_CONCAT_RECAuto-generated from RARE rule str-len-eq-zero-concat-recSTR_LEN_REPLACE_ALL_INVAuto-generated from RARE rule str-len-replace-all-invSTR_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_UPDATE_INVAuto-generated from RARE rule str-len-update-invSTR_LEQ_CONCAT_BASE_1Auto-generated from RARE rule str-leq-concat-base-1STR_LEQ_CONCAT_BASE_2Auto-generated from RARE rule str-leq-concat-base-2STR_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_OVERLAP_ENDPOINTS_CTNStrings – Strings overlap endpoints contains \[ \mathit{str.contains}(\mathit{str.++}(t_1, t_2, t_3), s) = \mathit{str.contains}(t_2, s) \] where \(s\) is `:math:\mathit{str.++}(s_1, s_2, s_3)`, \(t_1\) has no forward overlap with \(s_1\) and \(t_3\) has no reverse overlap with \(s_3\).STR_OVERLAP_ENDPOINTS_INDEXOFStrings – Strings overlap endpoints indexof \[ \mathit{str.indexof}(\mathit{str.++}(t_1, t_2), s, n) = \mathit{str.indexof}(t_1, s, n) \] where \(s\) is `:math:\mathit{str.++}(s_1, s_2)` and \(t_2\) has no reverse overlap with \(s_2\).STR_OVERLAP_ENDPOINTS_REPLACEStrings – Strings overlap endpoints replace \[ \mathit{str.replace}(\mathit{str.++}(t_1, t_2, t_3), s, r) = \mathit{str.++}(t_1, \mathit{str.replace}(t_2, s, r) t_3) \] where \(s\) is `:math:\mathit{str.++}(s_1, s_2, s_3)`, \(t_1\) has no forward overlap with \(s_1\) and \(t_3\) has no reverse overlap with \(s_3\).STR_OVERLAP_SPLIT_CTNStrings – Strings overlap split contains \[ \mathit{str.contains}(\mathit{str.++}(t_1, t_2, t_3), s) = \mathit{str.contains}(t_1, s) \vee \mathit{str.contains}(t_3, s) \] \(t_2\) has no forward overlap with \(s\) and \(s\) has no forward overlap with \(t_2\).STR_PREFIXOF_ELIMAuto-generated from RARE rule str-prefixof-elimSTR_PREFIXOF_EQAuto-generated from RARE rule str-prefixof-eqSTR_PREFIXOF_ONEAuto-generated from RARE rule str-prefixof-oneSTR_REPL_REPL_DUAL_ITE1Auto-generated from RARE rule str-repl-repl-dual-ite1STR_REPL_REPL_DUAL_ITE2Auto-generated from RARE rule str-repl-repl-dual-ite2STR_REPL_REPL_DUAL_SELFAuto-generated from RARE rule str-repl-repl-dual-selfSTR_REPL_REPL_LEN_IDAuto-generated from RARE rule str-repl-repl-len-idSTR_REPL_REPL_LOOKAHEAD_ID_SIMPAuto-generated from RARE rule str-repl-repl-lookahead-id-simpSTR_REPL_REPL_SRC_INV_NO_CTN1Auto-generated from RARE rule str-repl-repl-src-inv-no-ctn1STR_REPL_REPL_SRC_INV_NO_CTN2Auto-generated from RARE rule str-repl-repl-src-inv-no-ctn2STR_REPL_REPL_SRC_INV_NO_CTN3Auto-generated from RARE rule str-repl-repl-src-inv-no-ctn3STR_REPL_REPL_SRC_SELFAuto-generated from RARE rule str-repl-repl-src-selfSTR_REPL_REPL_SRC_TGT_NO_CTNAuto-generated from RARE rule str-repl-repl-src-tgt-no-ctnSTR_REPL_REPL_TGT_NO_CTNAuto-generated from RARE rule str-repl-repl-tgt-no-ctnSTR_REPL_REPL_TGT_SELFAuto-generated from RARE rule str-repl-repl-tgt-selfSTR_REPLACE_ALL_NO_CONTAINSAuto-generated from RARE rule str-replace-all-no-containsSTR_REPLACE_DUAL_CTNAuto-generated from RARE rule str-replace-dual-ctnSTR_REPLACE_DUAL_CTN_FALSEAuto-generated from RARE rule str-replace-dual-ctn-falseSTR_REPLACE_EMP_CTN_SRCAuto-generated from RARE rule str-replace-emp-ctn-srcSTR_REPLACE_EMPTYAuto-generated from RARE rule str-replace-emptySTR_REPLACE_FIND_BASEAuto-generated from RARE rule str-replace-find-baseSTR_REPLACE_FIND_FIRST_CONCATAuto-generated from RARE rule str-replace-find-first-concatSTR_REPLACE_FIND_PREAuto-generated from RARE rule str-replace-find-preSTR_REPLACE_IDAuto-generated from RARE rule str-replace-idSTR_REPLACE_NO_CONTAINSAuto-generated from RARE rule str-replace-no-containsSTR_REPLACE_ONE_PREAuto-generated from RARE rule str-replace-one-preSTR_REPLACE_PREFIXAuto-generated from RARE rule str-replace-prefixSTR_REPLACE_RE_ALL_EVALStrings – string replace regex all evaluation \[ str.replace\_re\_all(s,r,t) = u \] where \(s,t\) are string values, \(r\) is a ground regular expression and \(u\) is the result of evaluating the left hand side.STR_REPLACE_RE_ALL_NONEAuto-generated from RARE rule str-replace-re-all-noneSTR_REPLACE_RE_EVALStrings – string replace regex evaluation \[ str.replace\_re(s,r,t) = u \] where \(s,t\) are string values, \(r\) is a ground regular expression and \(u\) is the result of evaluating the left hand side.STR_REPLACE_RE_NONEAuto-generated from RARE rule str-replace-re-noneSTR_REPLACE_SELFAuto-generated from RARE rule str-replace-selfSTR_REPLACE_SELF_CTN_SIMPAuto-generated from RARE rule str-replace-self-ctn-simpSTR_SUBSTR_CHAR_START_EQ_LENAuto-generated from RARE rule str-substr-char-start-eq-lenSTR_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_CTNAuto-generated from RARE rule str-substr-ctnSTR_SUBSTR_CTN_CONTRAAuto-generated from RARE rule str-substr-ctn-contraSTR_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_EQ_EMPTY_LEQ_LENAuto-generated from RARE rule str-substr-eq-empty-leq-lenSTR_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_NORMAuto-generated from RARE rule str-substr-len-normSTR_SUBSTR_REPLACEAuto-generated from RARE rule str-substr-replaceSTR_SUBSTR_SUBSTR_START_GEQ_LENAuto-generated from RARE rule str-substr-substr-start-geq-lenSTR_SUBSTR_Z_EQ_EMPTY_LEQAuto-generated from RARE rule str-substr-z-eq-empty-leqSTR_SUFFIXOF_ELIMAuto-generated from RARE rule str-suffixof-elimSTR_SUFFIXOF_EQAuto-generated from RARE rule str-suffixof-eqSTR_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-lowerSTR_UPDATE_IN_FIRST_CONCATAuto-generated from RARE rule str-update-in-first-concatUBV_TO_INT_ELIMUF – Bitvector to natural elimination \[ \texttt{ubv_to_int}(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)\).UF_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-equivUF_SBV_TO_INT_ELIMAuto-generated from RARE rule uf-sbv-to-int-elim
-
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\).
-
UBV_TO_INT_ELIM
public static final ProofRewriteRule UBV_TO_INT_ELIM
UF – Bitvector to natural elimination \[ \texttt{ubv_to_int}(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_BOOL_BV_INVERT_SOLVE
public static final ProofRewriteRule MACRO_BOOL_BV_INVERT_SOLVE
Booleans – Bitvector invert solve \[ ((t_1 = t_2) = (x = r)) = \top \] where \(x\) occurs on an invertible path in \(t_1 = t_2\) and has solved form \(r\).
-
MACRO_ARITH_INT_EQ_CONFLICT
public static final ProofRewriteRule MACRO_ARITH_INT_EQ_CONFLICT
Arithmetic – Integer equality conflict \[ (t=s) = \bot \] where \(t=s\) is equivalent (via ARITH_POLY_NORM <cvc5.ProofRule.ARITH_POLY_NORM>) to \((r = c)\) where \(r\) is an integral term and \(c\) is a non-integral constant.
-
MACRO_ARITH_INT_GEQ_TIGHTEN
public static final ProofRewriteRule MACRO_ARITH_INT_GEQ_TIGHTEN
Arithmetic – Integer inequality tightening \[ (t \geq s) = ( r \geq \lceil c \rceil) \] or \[ (t \geq s) = \neg( r \geq \lceil c \rceil) \] where \(t \geq s\) is equivalent (via ARITH_POLY_NORM <cvc5.ProofRule.ARITH_POLY_NORM>) to the right hand side where \(r\) is an integral term and \(c\) is a non-integral constant. Note that we end up with a negation if the leading coefficient in \(t\) is negative.
-
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\} \] or alternatively \[ ((\lambda x_1 \ldots x_n.\> t) \ t_1) = (\lambda x_2 \ldots x_n.\> t)\{x_1 \mapsto t_1\} \] In the former case, the left hand side may either be a term of kind `cvc5.Kind.APPLY_UF` or `cvc5.Kind.HO_APPLY`. The latter case is used only if the term has kind `cvc5.Kind.HO_APPLY`. In either case, 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 \]
-
MACRO_LAMBDA_CAPTURE_AVOID
public static final ProofRewriteRule MACRO_LAMBDA_CAPTURE_AVOID
Equality – Macro lambda application capture avoid \[ ((\lambda x_1 \ldots x_n.\> t) \ t_1 \ldots t_n) = ((\lambda y_1 \ldots y_n.\> t') \ t_1 \ldots t_n) \] The terms may either be of kind `cvc5.Kind.APPLY_UF` or `cvc5.Kind.HO_APPLY`. This rule ensures that the free variables of \(y_1, \ldots, y_n, t_1 \ldots t_n\) do not occur in binders within \(t'\), and \((\lambda x_1 \ldots x_n.\> t)\) is alpha-equivalent to \((\lambda y_1 \ldots y_n.\> t')\). This rule is applied prior to beta reduction to ensure there is no variable capturing.
-
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_NORMALIZE_OP
public static final ProofRewriteRule MACRO_ARRAYS_NORMALIZE_OP
Arrays – Macro normalize operation \[ A = B \] where \(B\) is the result of normalizing the array operation \(A\) into a canonical form, based on commutativity of disjoint indices.
-
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_DT_VAR_EXPAND
public static final ProofRewriteRule MACRO_QUANT_DT_VAR_EXPAND
Quantifiers – Macro datatype variable expand \[ (\forall Y x Z.\> F) = (\forall Y X_1 Z. F_1) \vee \cdots \vee (\forall Y X_n Z. 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) \}\), and \(F\) entails \(\mathit{is}_c(x)\) for some \(c\).
-
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 \(F\) is a disjunction and where \(G\) is the result of dropping all literals containing \(x\). This is applied only when all such literals are lower (resp. upper) bounds for integer or real variable \(x\). Note that \(G\) may be false, and \(Y\) may be empty in which case it is omitted.
-
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.
-
MACRO_BV_EXTRACT_CONCAT
public static final ProofRewriteRule MACRO_BV_EXTRACT_CONCAT
Bitvectors – Macro extract and concat \[ a = b \] where \(a\) is rewritten to \(b\) by the internal rewrite rule ExtractConcat.
-
MACRO_BV_OR_SIMPLIFY
public static final ProofRewriteRule MACRO_BV_OR_SIMPLIFY
Bitvectors – Macro or simplify \[ a = b \] where \(a\) is rewritten to \(b\) by the internal rewrite rule OrSimplify.
-
MACRO_BV_AND_SIMPLIFY
public static final ProofRewriteRule MACRO_BV_AND_SIMPLIFY
Bitvectors – Macro and simplify \[ a = b \] where \(a\) is rewritten to \(b\) by the internal rewrite rule AndSimplify.
-
MACRO_BV_XOR_SIMPLIFY
public static final ProofRewriteRule MACRO_BV_XOR_SIMPLIFY
Bitvectors – Macro xor simplify \[ a = b \] where \(a\) is rewritten to \(b\) by the internal rewrite rule XorSimplify.
-
MACRO_BV_AND_OR_XOR_CONCAT_PULLUP
public static final ProofRewriteRule MACRO_BV_AND_OR_XOR_CONCAT_PULLUP
Bitvectors – Macro and/or/xor concat pullup \[ a = b \] where \(a\) is rewritten to \(b\) by the internal rewrite rule AndOrXorConcatPullup.
-
MACRO_BV_MULT_SLT_MULT
public static final ProofRewriteRule MACRO_BV_MULT_SLT_MULT
Bitvectors – Macro multiply signed less than multiply \[ a = b \] where \(a\) is rewritten to \(b\) by the internal rewrite rule MultSltMult.
-
MACRO_BV_CONCAT_EXTRACT_MERGE
public static final ProofRewriteRule MACRO_BV_CONCAT_EXTRACT_MERGE
Bitvectors – Macro concat extract merge \[ a = b \] where \(a\) is rewritten to \(b\) by the internal rewrite rule ConcatExtractMerge.
-
MACRO_BV_CONCAT_CONSTANT_MERGE
public static final ProofRewriteRule MACRO_BV_CONCAT_CONSTANT_MERGE
Bitvectors – Macro concat constant merge \[ a = b \] where \(a\) is rewritten to \(b\) by the internal rewrite rule ConcatConstantMerge.
-
MACRO_BV_EQ_SOLVE
public static final ProofRewriteRule MACRO_BV_EQ_SOLVE
Bitvectors – Macro equality solve \[ (a = b) = \bot \] where \(bvsub(a,b)\) normalizes to a non-zero constant, or alternatively \[ (a = b) = \top \] where \(bvsub(a,b)\) normalizes to zero.
-
BV_UMULO_ELIM
public static final ProofRewriteRule BV_UMULO_ELIM
Bitvectors – Unsigned multiplication overflow detection elimination \[ \texttt{bvumulo}(x,y) = t \] where \(t\) is the result of eliminating the application of \(\texttt{bvumulo}\). See M.Gok, M.J. Schulte, P.I. Balzola, "Efficient integer multiplication overflow detection circuits", 2001. http:
-
BV_SMULO_ELIM
public static final ProofRewriteRule BV_SMULO_ELIM
Bitvectors – Unsigned multiplication overflow detection elimination \[ \texttt{bvsmulo}(x,y) = t \] where \(t\) is the result of eliminating the application of \(\texttt{bvsmulo}\). See M.Gok, M.J. Schulte, P.I. Balzola, "Efficient integer multiplication overflow detection circuits", 2001. http:
-
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.
-
STR_CTN_MULTISET_SUBSET
public static final ProofRewriteRule STR_CTN_MULTISET_SUBSET
Strings – String contains multiset subset \[ \mathit{str}.contains(s,t) = \bot \] where the multiset overapproximation of \(s\) can be shown to not contain the multiset abstraction of \(t\) based on the reasoning described in the paper Reynolds et al, CAV 2019, "High-Level Abstractions for Simplifying Extended String Constraints in SMT".
-
MACRO_STR_EQ_LEN_UNIFY_PREFIX
public static final ProofRewriteRule MACRO_STR_EQ_LEN_UNIFY_PREFIX
Strings – String equality length unify prefix \[ (s = \mathit{str}.\text{++}(t_1, \ldots, t_n)) = (s = \mathit{str}.\text{++}(t_1, \ldots t_i)) \wedge t_{i+1} = \epsilon \wedge \ldots \wedge t_n = \epsilon \] where we can show \(s\) has a length that is at least the length of \(\text{++}(t_1, \ldots t_i)\).
-
MACRO_STR_EQ_LEN_UNIFY
public static final ProofRewriteRule MACRO_STR_EQ_LEN_UNIFY
Strings – String equality length unify \[ (\mathit{str}.\text{++}(s_1, \ldots, s_n) = \mathit{str}.\text{++}(t_1, \ldots, t_m)) = (r_1 = u_1 \wedge \ldots r_k = u_k) \] where for each \(i = 1, \ldots, k\), we can show the length of \(r_i\) and \(u_i\) are equal, \(s_1, \ldots, s_n\) is \(r_1, \ldots, r_k\), and \(t_1, \ldots, t_m\) is \(u_1, \ldots, u_k\).
-
MACRO_STR_SPLIT_CTN
public static final ProofRewriteRule MACRO_STR_SPLIT_CTN
Strings – Macro string split contains \[ \mathit{str.contains}(t, s) = \mathit{str.contains}(t_1, s) \vee \mathit{str.contains}(t_2, s) \] where \(t_1\) and \(t_2\) are substrings of \(t\). This rule is elaborated using STR_OVERLAP_SPLIT_CTN <cvc5.ProofRewriteRule.STR_OVERLAP_SPLIT_CTN>.
-
MACRO_STR_STRIP_ENDPOINTS
public static final ProofRewriteRule MACRO_STR_STRIP_ENDPOINTS
Strings – Macro string strip endpoints One of the following forms: \[ \mathit{str.contains}(t, s) = \mathit{str.contains}(t_2, s) \] \[ \mathit{str.indexof}(t, s, n) = \mathit{str.indexof}(t_2, s, n) \] \[ \mathit{str.replace}(t, s, r) = \mathit{str.++}(t_1, \mathit{str.replace}(t_2, s, r) t_3) \] where in each case we reason about removing portions of \(t\) that are irrelevant to the evaluation of the term. This rule is elaborated using STR_OVERLAP_ENDPOINTS_CTN <cvc5.ProofRewriteRule.STR_OVERLAP_ENDPOINTS_CTN>, STR_OVERLAP_ENDPOINTS_INDEXOF <cvc5.ProofRewriteRule.STR_OVERLAP_ENDPOINTS_INDEXOF> and STR_OVERLAP_ENDPOINTS_REPLACE <cvc5.ProofRewriteRule.STR_OVERLAP_ENDPOINTS_REPLACE>.
-
STR_OVERLAP_SPLIT_CTN
public static final ProofRewriteRule STR_OVERLAP_SPLIT_CTN
Strings – Strings overlap split contains \[ \mathit{str.contains}(\mathit{str.++}(t_1, t_2, t_3), s) = \mathit{str.contains}(t_1, s) \vee \mathit{str.contains}(t_3, s) \] \(t_2\) has no forward overlap with \(s\) and \(s\) has no forward overlap with \(t_2\). For details see \(\texttt{Word::hasOverlap}\) in :cvc5src:`theory/strings/word.h`.
-
STR_OVERLAP_ENDPOINTS_CTN
public static final ProofRewriteRule STR_OVERLAP_ENDPOINTS_CTN
Strings – Strings overlap endpoints contains \[ \mathit{str.contains}(\mathit{str.++}(t_1, t_2, t_3), s) = \mathit{str.contains}(t_2, s) \] where \(s\) is `:math:\mathit{str.++}(s_1, s_2, s_3)`, \(t_1\) has no forward overlap with \(s_1\) and \(t_3\) has no reverse overlap with \(s_3\). For details see \(\texttt{Word::hasOverlap}\) in :cvc5src:`theory/strings/word.h`.
-
STR_OVERLAP_ENDPOINTS_INDEXOF
public static final ProofRewriteRule STR_OVERLAP_ENDPOINTS_INDEXOF
Strings – Strings overlap endpoints indexof \[ \mathit{str.indexof}(\mathit{str.++}(t_1, t_2), s, n) = \mathit{str.indexof}(t_1, s, n) \] where \(s\) is `:math:\mathit{str.++}(s_1, s_2)` and \(t_2\) has no reverse overlap with \(s_2\). For details see \(\texttt{Word::hasOverlap}\) in :cvc5src:`theory/strings/word.h`.
-
STR_OVERLAP_ENDPOINTS_REPLACE
public static final ProofRewriteRule STR_OVERLAP_ENDPOINTS_REPLACE
Strings – Strings overlap endpoints replace \[ \mathit{str.replace}(\mathit{str.++}(t_1, t_2, t_3), s, r) = \mathit{str.++}(t_1, \mathit{str.replace}(t_2, s, r) t_3) \] where \(s\) is `:math:\mathit{str.++}(s_1, s_2, s_3)`, \(t_1\) has no forward overlap with \(s_1\) and \(t_3\) has no reverse overlap with \(s_3\). For details see \(\texttt{Word::hasOverlap}\) in :cvc5src:`theory/strings/word.h`.
-
MACRO_STR_COMPONENT_CTN
public static final ProofRewriteRule MACRO_STR_COMPONENT_CTN
Strings – Macro string component contains \[ \mathit{str.contains}(t, s) = \top \] where a substring of \(t\) can be inferred to be a superstring of \(s\) based on iterating on components of string concatenation terms as well as prefix and suffix reasoning.
-
MACRO_STR_CONST_NCTN_CONCAT
public static final ProofRewriteRule MACRO_STR_CONST_NCTN_CONCAT
Strings – Macro string constant no contains concatenation \[ \mathit{str.contains}(c, \mathit{str.++}(t_1, \ldots, t_n)) = \bot \] where \(c\) is not contained in \(R_t\), where the regular expression \(R_t\) overapproximates the possible values of \(\mathit{str.++}(t_1, \ldots, t_n)\).
-
MACRO_STR_IN_RE_INCLUSION
public static final ProofRewriteRule MACRO_STR_IN_RE_INCLUSION
Strings – Macro string in regular expression inclusion \[ \mathit{str.in_re}(s, R) = \top \] where \(R\) includes the regular expression \(R_s\) which overapproximates the possible values of string \(s\).
-
MACRO_RE_INTER_UNION_CONST_ELIM
public static final ProofRewriteRule MACRO_RE_INTER_UNION_CONST_ELIM
Strings – Macro regular expression intersection/union constant elimination One of the following forms: \[ \mathit{re.union}(R) = \mathit{re.union}(R') \] where \(R\) is a list of regular expressions containing \(R_i\) and \(\mathit{str.to_re(c)}\) where \(c\) is a string in \(R_i\) and \(R'\) is the result of removing \(\mathit{str.to_re(c)}\) from \(R\). \[ \mathit{re.inter}(R) = \mathit{re.inter}(R') \] where \(R\) is a list of regular expressions containing \(R_i\) and \(\mathit{str.to_re(c)}\) where \(c\) is a string in \(R_i\) and \(R'\) is the result of removing \(R_i\) from \(R\). \[ \mathit{re.inter}(R) = \mathit{re.none} \] where \(R\) is a list of regular expressions containing \(R_i\) and \(\mathit{str.to_re(c)}\) where \(c\) is a string not in \(R_i\).
-
SEQ_EVAL_OP
public static final ProofRewriteRule SEQ_EVAL_OP
Strings – Sequence evaluate operator \[ f(s_1, \ldots, s_n) = t \] where \(f\) is an operator over sequences and \(s_1, \ldots, s_n\) are values, that is, the Node.isConst method returns true for each, and \(t\) is the result of evaluating \(f\) on them.
-
STR_INDEXOF_RE_EVAL
public static final ProofRewriteRule STR_INDEXOF_RE_EVAL
Strings – string indexof regex evaluation \[ str.indexof\_re(s,r,n) = m \] where \(s\) is a string values, \(n\) is an integer value, \(r\) is a ground regular expression and \(m\) is the result of evaluating the left hand side.
-
STR_REPLACE_RE_EVAL
public static final ProofRewriteRule STR_REPLACE_RE_EVAL
Strings – string replace regex evaluation \[ str.replace\_re(s,r,t) = u \] where \(s,t\) are string values, \(r\) is a ground regular expression and \(u\) is the result of evaluating the left hand side.
-
STR_REPLACE_RE_ALL_EVAL
public static final ProofRewriteRule STR_REPLACE_RE_ALL_EVAL
Strings – string replace regex all evaluation \[ str.replace\_re\_all(s,r,t) = u \] where \(s,t\) are string values, \(r\) is a ground regular expression and \(u\) is the result of evaluating the left hand side.
-
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\).
-
MACRO_RE_INTER_UNION_INCLUSION
public static final ProofRewriteRule MACRO_RE_INTER_UNION_INCLUSION
Strings – regular expression intersection/union inclusion \[ \mathit{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`.
-
RE_INTER_INCLUSION
public static final ProofRewriteRule RE_INTER_INCLUSION
Strings – regular expression intersection inclusion \[ \mathit{re.inter}(r_1, re.comp(r_2)) = \mathit{re.none} \] where \(r_2\) is a superset of \(r_1\).
-
RE_UNION_INCLUSION
public static final ProofRewriteRule RE_UNION_INCLUSION
Strings – regular expression union inclusion \[ \mathit{re.union}(r_1, re.comp(r_2)) = \mathit{re}.\text{*}(\mathit{re.allchar}) \] 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_EVAL_OP
public static final ProofRewriteRule SETS_EVAL_OP
Sets – sets evaluate operator \[ \mathit{f}(t_1, t_2) = t \] where \(f\) is one of \(\mathit{set.inter}, \mathit{set.minus}, \mathit{set.union}\), and \(t\) is the result of evaluating \(f\) on \(t_1\) and \(t_2\). Note we use this rule only when \(t_1\) and \(t_2\) are set values, that is, the Node.isConst method returns true for both.
-
SETS_INSERT_ELIM
public static final ProofRewriteRule SETS_INSERT_ELIM
Sets – sets insert elimination \[ \mathit{set.insert}(t_1, \ldots, t_n, S) = \texttt{set.union}(\texttt{sets.singleton}(t_1), \ldots, \texttt{sets.singleton}(t_n), S) \]
-
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_DIV_TOTAL_NEG
public static final ProofRewriteRule ARITH_INT_DIV_TOTAL_NEG
Auto-generated from RARE rule arith-int-div-total-neg
-
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_INT_MOD_TOTAL_NEG
public static final ProofRewriteRule ARITH_INT_MOD_TOTAL_NEG
Auto-generated from RARE rule arith-int-mod-total-neg
-
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_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_TO_INT_ELIM
public static final ProofRewriteRule ARITH_TO_INT_ELIM
Auto-generated from RARE rule arith-to-int-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_MOD_OVER_MOD
public static final ProofRewriteRule ARITH_MOD_OVER_MOD
Auto-generated from RARE rule arith-mod-over-mod
-
ARITH_INT_EQ_CONFLICT
public static final ProofRewriteRule ARITH_INT_EQ_CONFLICT
Auto-generated from RARE rule arith-int-eq-conflict
-
ARITH_INT_GEQ_TIGHTEN
public static final ProofRewriteRule ARITH_INT_GEQ_TIGHTEN
Auto-generated from RARE rule arith-int-geq-tighten
-
ARITH_DIVISIBLE_ELIM
public static final ProofRewriteRule ARITH_DIVISIBLE_ELIM
Auto-generated from RARE rule arith-divisible-elim
-
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
-
ARITH_GEQ_ITE_LIFT
public static final ProofRewriteRule ARITH_GEQ_ITE_LIFT
Auto-generated from RARE rule arith-geq-ite-lift
-
ARITH_LEQ_ITE_LIFT
public static final ProofRewriteRule ARITH_LEQ_ITE_LIFT
Auto-generated from RARE rule arith-leq-ite-lift
-
ARITH_MIN_LT1
public static final ProofRewriteRule ARITH_MIN_LT1
Auto-generated from RARE rule arith-min-lt1
-
ARITH_MIN_LT2
public static final ProofRewriteRule ARITH_MIN_LT2
Auto-generated from RARE rule arith-min-lt2
-
ARITH_MAX_GEQ1
public static final ProofRewriteRule ARITH_MAX_GEQ1
Auto-generated from RARE rule arith-max-geq1
-
ARITH_MAX_GEQ2
public static final ProofRewriteRule ARITH_MAX_GEQ2
Auto-generated from RARE rule arith-max-geq2
-
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
-
ARRAY_STORE_SWAP
public static final ProofRewriteRule ARRAY_STORE_SWAP
Auto-generated from RARE rule array-store-swap
-
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_DUAL_IMPL_EQ
public static final ProofRewriteRule BOOL_DUAL_IMPL_EQ
Auto-generated from RARE rule boolean-dual-impl-eq
-
BOOL_OR_FLATTEN
public static final ProofRewriteRule BOOL_OR_FLATTEN
Auto-generated from RARE rule boolean-or-flatten
-
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_IMPLIES_OR_DISTRIB
public static final ProofRewriteRule BOOL_IMPLIES_OR_DISTRIB
Auto-generated from RARE rule boolean-implies-or-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_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_XOR
public static final ProofRewriteRule BV_COMMUTATIVE_XOR
Auto-generated from RARE rule bv-commutative-xor
-
BV_COMMUTATIVE_COMP
public static final ProofRewriteRule BV_COMMUTATIVE_COMP
Auto-generated from RARE rule bv-commutative-comp
-
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_XOR_FLATTEN
public static final ProofRewriteRule BV_XOR_FLATTEN
Auto-generated from RARE rule bv-xor-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_SUB_ELIMINATE
public static final ProofRewriteRule BV_SUB_ELIMINATE
Auto-generated from RARE rule bv-sub-eliminate
-
BV_ITE_WIDTH_ONE
public static final ProofRewriteRule BV_ITE_WIDTH_ONE
Auto-generated from RARE rule bv-ite-width-one
-
BV_ITE_WIDTH_ONE_NOT
public static final ProofRewriteRule BV_ITE_WIDTH_ONE_NOT
Auto-generated from RARE rule bv-ite-width-one-not
-
BV_EQ_XOR_SOLVE
public static final ProofRewriteRule BV_EQ_XOR_SOLVE
Auto-generated from RARE rule bv-eq-xor-solve
-
BV_EQ_NOT_SOLVE
public static final ProofRewriteRule BV_EQ_NOT_SOLVE
Auto-generated from RARE rule bv-eq-not-solve
-
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_NEGO_ELIMINATE
public static final ProofRewriteRule BV_NEGO_ELIMINATE
Auto-generated from RARE rule bv-nego-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_AND_CONCAT_PULLUP2
public static final ProofRewriteRule BV_AND_CONCAT_PULLUP2
Auto-generated from RARE rule bv-and-concat-pullup2
-
BV_OR_CONCAT_PULLUP2
public static final ProofRewriteRule BV_OR_CONCAT_PULLUP2
Auto-generated from RARE rule bv-or-concat-pullup2
-
BV_XOR_CONCAT_PULLUP2
public static final ProofRewriteRule BV_XOR_CONCAT_PULLUP2
Auto-generated from RARE rule bv-xor-concat-pullup2
-
BV_AND_CONCAT_PULLUP3
public static final ProofRewriteRule BV_AND_CONCAT_PULLUP3
Auto-generated from RARE rule bv-and-concat-pullup3
-
BV_OR_CONCAT_PULLUP3
public static final ProofRewriteRule BV_OR_CONCAT_PULLUP3
Auto-generated from RARE rule bv-or-concat-pullup3
-
BV_XOR_CONCAT_PULLUP3
public static final ProofRewriteRule BV_XOR_CONCAT_PULLUP3
Auto-generated from RARE rule bv-xor-concat-pullup3
-
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_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_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_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_ZERO_EXTEND_ULT_CONST_1
public static final ProofRewriteRule BV_ZERO_EXTEND_ULT_CONST_1
Auto-generated from RARE rule bv-zero-extend-ult--1
-
BV_ZERO_EXTEND_ULT_CONST_2
public static final ProofRewriteRule BV_ZERO_EXTEND_ULT_CONST_2
Auto-generated from RARE rule bv-zero-extend-ult--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_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
-
SETS_IS_SINGLETON_ELIM
public static final ProofRewriteRule SETS_IS_SINGLETON_ELIM
Auto-generated from RARE rule sets-is-singleton-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_EQ_LEN_FALSE
public static final ProofRewriteRule STR_EQ_LEN_FALSE
Auto-generated from RARE rule str-eq-len-false
-
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_SUBSTR_START_GEQ_LEN
public static final ProofRewriteRule STR_SUBSTR_SUBSTR_START_GEQ_LEN
Auto-generated from RARE rule str-substr-substr-start-geq-len
-
STR_SUBSTR_EQ_EMPTY
public static final ProofRewriteRule STR_SUBSTR_EQ_EMPTY
Auto-generated from RARE rule str-substr-eq-empty
-
STR_SUBSTR_Z_EQ_EMPTY_LEQ
public static final ProofRewriteRule STR_SUBSTR_Z_EQ_EMPTY_LEQ
Auto-generated from RARE rule str-substr-z-eq-empty-leq
-
STR_SUBSTR_EQ_EMPTY_LEQ_LEN
public static final ProofRewriteRule STR_SUBSTR_EQ_EMPTY_LEQ_LEN
Auto-generated from RARE rule str-substr-eq-empty-leq-len
-
STR_LEN_REPLACE_INV
public static final ProofRewriteRule STR_LEN_REPLACE_INV
Auto-generated from RARE rule str-len-replace-inv
-
STR_LEN_REPLACE_ALL_INV
public static final ProofRewriteRule STR_LEN_REPLACE_ALL_INV
Auto-generated from RARE rule str-len-replace-all-inv
-
STR_LEN_UPDATE_INV
public static final ProofRewriteRule STR_LEN_UPDATE_INV
Auto-generated from RARE rule str-len-update-inv
-
STR_UPDATE_IN_FIRST_CONCAT
public static final ProofRewriteRule STR_UPDATE_IN_FIRST_CONCAT
Auto-generated from RARE rule str-update-in-first-concat
-
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_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_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_EQ
public static final ProofRewriteRule STR_PREFIXOF_EQ
Auto-generated from RARE rule str-prefixof-eq
-
STR_SUFFIXOF_EQ
public static final ProofRewriteRule STR_SUFFIXOF_EQ
Auto-generated from RARE rule str-suffixof-eq
-
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_REPLACE
public static final ProofRewriteRule STR_SUBSTR_REPLACE
Auto-generated from RARE rule str-substr-replace
-
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_CONCAT_FIND_CONTRA
public static final ProofRewriteRule STR_CONTAINS_CONCAT_FIND_CONTRA
Auto-generated from RARE rule str-contains-concat-find-contra
-
STR_CONTAINS_SPLIT_CHAR
public static final ProofRewriteRule STR_CONTAINS_SPLIT_CHAR
Auto-generated from RARE rule str-contains-split-char
-
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_CHAR
public static final ProofRewriteRule STR_CONTAINS_CHAR
Auto-generated from RARE rule str-contains-char
-
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_ID
public static final ProofRewriteRule STR_REPLACE_ID
Auto-generated from RARE rule str-replace-id
-
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_FIND_BASE
public static final ProofRewriteRule STR_REPLACE_FIND_BASE
Auto-generated from RARE rule str-replace-find-base
-
STR_REPLACE_FIND_FIRST_CONCAT
public static final ProofRewriteRule STR_REPLACE_FIND_FIRST_CONCAT
Auto-generated from RARE rule str-replace-find-first-concat
-
STR_REPLACE_EMPTY
public static final ProofRewriteRule STR_REPLACE_EMPTY
Auto-generated from RARE rule str-replace-empty
-
STR_REPLACE_ONE_PRE
public static final ProofRewriteRule STR_REPLACE_ONE_PRE
Auto-generated from RARE rule str-replace-one-pre
-
STR_REPLACE_FIND_PRE
public static final ProofRewriteRule STR_REPLACE_FIND_PRE
Auto-generated from RARE rule str-replace-find-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_LEN_EQ_ZERO_CONCAT_REC
public static final ProofRewriteRule STR_LEN_EQ_ZERO_CONCAT_REC
Auto-generated from RARE rule str-len-eq-zero-concat-rec
-
STR_LEN_EQ_ZERO_BASE
public static final ProofRewriteRule STR_LEN_EQ_ZERO_BASE
Auto-generated from RARE rule str-len-eq-zero-base
-
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_OOB
public static final ProofRewriteRule STR_INDEXOF_OOB
Auto-generated from RARE rule str-indexof-oob
-
STR_INDEXOF_OOB2
public static final ProofRewriteRule STR_INDEXOF_OOB2
Auto-generated from RARE rule str-indexof-oob2
-
STR_INDEXOF_CONTAINS_PRE
public static final ProofRewriteRule STR_INDEXOF_CONTAINS_PRE
Auto-generated from RARE rule str-indexof-contains-pre
-
STR_INDEXOF_FIND_EMP
public static final ProofRewriteRule STR_INDEXOF_FIND_EMP
Auto-generated from RARE rule str-indexof-find-emp
-
STR_INDEXOF_EQ_IRR
public static final ProofRewriteRule STR_INDEXOF_EQ_IRR
Auto-generated from RARE rule str-indexof-eq-irr
-
STR_INDEXOF_RE_NONE
public static final ProofRewriteRule STR_INDEXOF_RE_NONE
Auto-generated from RARE rule str-indexof-re-none
-
STR_INDEXOF_RE_EMP_RE
public static final ProofRewriteRule STR_INDEXOF_RE_EMP_RE
Auto-generated from RARE rule str-indexof-re-emp-re
-
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_LEQ_CONCAT_BASE_1
public static final ProofRewriteRule STR_LEQ_CONCAT_BASE_1
Auto-generated from RARE rule str-leq-concat-base-1
-
STR_LEQ_CONCAT_BASE_2
public static final ProofRewriteRule STR_LEQ_CONCAT_BASE_2
Auto-generated from RARE rule str-leq-concat-base-2
-
STR_LT_ELIM
public static final ProofRewriteRule STR_LT_ELIM
Auto-generated from RARE rule str-lt-elim
-
STR_FROM_INT_NO_CTN_NONDIGIT
public static final ProofRewriteRule STR_FROM_INT_NO_CTN_NONDIGIT
Auto-generated from RARE rule str-from-int-no-ctn-nondigit
-
STR_SUBSTR_CTN_CONTRA
public static final ProofRewriteRule STR_SUBSTR_CTN_CONTRA
Auto-generated from RARE rule str-substr-ctn-contra
-
STR_SUBSTR_CTN
public static final ProofRewriteRule STR_SUBSTR_CTN
Auto-generated from RARE rule str-substr-ctn
-
STR_REPLACE_DUAL_CTN
public static final ProofRewriteRule STR_REPLACE_DUAL_CTN
Auto-generated from RARE rule str-replace-dual-ctn
-
STR_REPLACE_DUAL_CTN_FALSE
public static final ProofRewriteRule STR_REPLACE_DUAL_CTN_FALSE
Auto-generated from RARE rule str-replace-dual-ctn-false
-
STR_REPLACE_SELF_CTN_SIMP
public static final ProofRewriteRule STR_REPLACE_SELF_CTN_SIMP
Auto-generated from RARE rule str-replace-self-ctn-simp
-
STR_REPLACE_EMP_CTN_SRC
public static final ProofRewriteRule STR_REPLACE_EMP_CTN_SRC
Auto-generated from RARE rule str-replace-emp-ctn-src
-
STR_SUBSTR_CHAR_START_EQ_LEN
public static final ProofRewriteRule STR_SUBSTR_CHAR_START_EQ_LEN
Auto-generated from RARE rule str-substr-char-start-eq-len
-
STR_CONTAINS_REPL_CHAR
public static final ProofRewriteRule STR_CONTAINS_REPL_CHAR
Auto-generated from RARE rule str-contains-repl-char
-
STR_CONTAINS_REPL_SELF_TGT_CHAR
public static final ProofRewriteRule STR_CONTAINS_REPL_SELF_TGT_CHAR
Auto-generated from RARE rule str-contains-repl-self-tgt-char
-
STR_CONTAINS_REPL_SELF
public static final ProofRewriteRule STR_CONTAINS_REPL_SELF
Auto-generated from RARE rule str-contains-repl-self
-
STR_CONTAINS_REPL_TGT
public static final ProofRewriteRule STR_CONTAINS_REPL_TGT
Auto-generated from RARE rule str-contains-repl-tgt
-
STR_REPL_REPL_LEN_ID
public static final ProofRewriteRule STR_REPL_REPL_LEN_ID
Auto-generated from RARE rule str-repl-repl-len-id
-
STR_REPL_REPL_SRC_TGT_NO_CTN
public static final ProofRewriteRule STR_REPL_REPL_SRC_TGT_NO_CTN
Auto-generated from RARE rule str-repl-repl-src-tgt-no-ctn
-
STR_REPL_REPL_TGT_SELF
public static final ProofRewriteRule STR_REPL_REPL_TGT_SELF
Auto-generated from RARE rule str-repl-repl-tgt-self
-
STR_REPL_REPL_TGT_NO_CTN
public static final ProofRewriteRule STR_REPL_REPL_TGT_NO_CTN
Auto-generated from RARE rule str-repl-repl-tgt-no-ctn
-
STR_REPL_REPL_SRC_SELF
public static final ProofRewriteRule STR_REPL_REPL_SRC_SELF
Auto-generated from RARE rule str-repl-repl-src-self
-
STR_REPL_REPL_SRC_INV_NO_CTN1
public static final ProofRewriteRule STR_REPL_REPL_SRC_INV_NO_CTN1
Auto-generated from RARE rule str-repl-repl-src-inv-no-ctn1
-
STR_REPL_REPL_SRC_INV_NO_CTN2
public static final ProofRewriteRule STR_REPL_REPL_SRC_INV_NO_CTN2
Auto-generated from RARE rule str-repl-repl-src-inv-no-ctn2
-
STR_REPL_REPL_SRC_INV_NO_CTN3
public static final ProofRewriteRule STR_REPL_REPL_SRC_INV_NO_CTN3
Auto-generated from RARE rule str-repl-repl-src-inv-no-ctn3
-
STR_REPL_REPL_DUAL_SELF
public static final ProofRewriteRule STR_REPL_REPL_DUAL_SELF
Auto-generated from RARE rule str-repl-repl-dual-self
-
STR_REPL_REPL_DUAL_ITE1
public static final ProofRewriteRule STR_REPL_REPL_DUAL_ITE1
Auto-generated from RARE rule str-repl-repl-dual-ite1
-
STR_REPL_REPL_DUAL_ITE2
public static final ProofRewriteRule STR_REPL_REPL_DUAL_ITE2
Auto-generated from RARE rule str-repl-repl-dual-ite2
-
STR_REPL_REPL_LOOKAHEAD_ID_SIMP
public static final ProofRewriteRule STR_REPL_REPL_LOOKAHEAD_ID_SIMP
Auto-generated from RARE rule str-repl-repl-lookahead-id-simp
-
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_PLUS_ELIM
public static final ProofRewriteRule RE_PLUS_ELIM
Auto-generated from RARE rule re-plus-elim
-
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_STAR_SUBSUME1
public static final ProofRewriteRule RE_CONCAT_STAR_SUBSUME1
Auto-generated from RARE rule re-concat-star-subsume1
-
RE_CONCAT_STAR_SUBSUME2
public static final ProofRewriteRule RE_CONCAT_STAR_SUBSUME2
Auto-generated from RARE rule re-concat-star-subsume2
-
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_CONST_ELIM
public static final ProofRewriteRule RE_UNION_CONST_ELIM
Auto-generated from RARE rule re-union--elim
-
RE_INTER_ALL
public static final ProofRewriteRule RE_INTER_ALL
Auto-generated from RARE rule re-inter-all
-
RE_STAR_NONE
public static final ProofRewriteRule RE_STAR_NONE
Auto-generated from RARE rule re-star-none
-
RE_STAR_EMP
public static final ProofRewriteRule RE_STAR_EMP
Auto-generated from RARE rule re-star-emp
-
RE_STAR_STAR
public static final ProofRewriteRule RE_STAR_STAR
Auto-generated from RARE rule re-star-star
-
RE_STAR_UNION_DROP_EMP
public static final ProofRewriteRule RE_STAR_UNION_DROP_EMP
Auto-generated from RARE rule re-star-union-drop-emp
-
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_NORM
public static final ProofRewriteRule STR_SUBSTR_LEN_NORM
Auto-generated from RARE rule str-substr-len-norm
-
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
-
STR_EQ_REPL_SELF_EMP
public static final ProofRewriteRule STR_EQ_REPL_SELF_EMP
Auto-generated from RARE rule str-eq-repl-self-emp
-
STR_EQ_REPL_NO_CHANGE
public static final ProofRewriteRule STR_EQ_REPL_NO_CHANGE
Auto-generated from RARE rule str-eq-repl-no-change
-
STR_EQ_REPL_TGT_EQ_LEN
public static final ProofRewriteRule STR_EQ_REPL_TGT_EQ_LEN
Auto-generated from RARE rule str-eq-repl-tgt-eq-len
-
STR_EQ_REPL_LEN_ONE_EMP_PREFIX
public static final ProofRewriteRule STR_EQ_REPL_LEN_ONE_EMP_PREFIX
Auto-generated from RARE rule str-eq-repl-len-one-emp-prefix
-
STR_EQ_REPL_EMP_TGT_NEMP
public static final ProofRewriteRule STR_EQ_REPL_EMP_TGT_NEMP
Auto-generated from RARE rule str-eq-repl-emp-tgt-nemp
-
STR_EQ_REPL_NEMP_SRC_EMP
public static final ProofRewriteRule STR_EQ_REPL_NEMP_SRC_EMP
Auto-generated from RARE rule str-eq-repl-nemp-src-emp
-
STR_EQ_REPL_SELF_SRC
public static final ProofRewriteRule STR_EQ_REPL_SELF_SRC
Auto-generated from RARE rule str-eq-repl-self-src
-
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_FROM_INT_NEMP_DIG_RANGE
public static final ProofRewriteRule STR_IN_RE_FROM_INT_NEMP_DIG_RANGE
Auto-generated from RARE rule str-in-re-from-int-nemp-dig-range
-
STR_IN_RE_FROM_INT_DIG_RANGE
public static final ProofRewriteRule STR_IN_RE_FROM_INT_DIG_RANGE
Auto-generated from RARE rule str-in-re-from-int-dig-range
-
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
-
UF_SBV_TO_INT_ELIM
public static final ProofRewriteRule UF_SBV_TO_INT_ELIM
Auto-generated from RARE rule uf-sbv-to-int-elim
-
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
-
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
-
-
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()
-
-