Enum Class ProofRewriteRule

Enum Constant Details

• 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 via Node.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_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_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_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_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_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_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_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_ZERO_EXTEND_ELIMINATE

  public static final ProofRewriteRule BV_ZERO_EXTEND_ELIMINATE

  Auto-generated from RARE rule bv-zero-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_SREM_ELIMINATE

  public static final ProofRewriteRule BV_SREM_ELIMINATE

  Auto-generated from RARE rule bv-srem-eliminate

• 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_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