Package io.github.cvc5

Enum ProofRewriteRule

  • All Implemented Interfaces:
    java.io.Serializable, java.lang.Comparable<ProofRewriteRule>
    public enum ProofRewriteRule
extends java.lang.Enum<ProofRewriteRule>

    • Enum Constant Detail

      • NONE

        public static final ProofRewriteRule NONE
        This enumeration represents the rewrite rules used in a rewrite proof. Some of the rules are internal ad-hoc rewrites, while others are rewrites specified by the RARE DSL. This enumeration is used as the first argument to the DSL_REWRITE <cvc5.ProofRule.DSL_REWRITE> proof rule and the THEORY_REWRITE <cvc5.ProofRule.THEORY_REWRITE> proof rule.

      • DISTINCT_ELIM

        public static final ProofRewriteRule DISTINCT_ELIM
        Builtin – Distinct elimination \[ \texttt{distinct}(t_1, t_2) = \neg (t_1 = t2) \] if \(n = 2\), or \[ \texttt{distinct}(t_1, \ldots, tn) = \bigwedge_{i=1}^n \bigwedge_{j=i+1}^n t_i \neq t_j \] if \(n > 2\)

      • DISTINCT_CARD_CONFLICT

        public static final ProofRewriteRule DISTINCT_CARD_CONFLICT
        Builtin – Distinct cardinality conflict \[ \texttt{distinct}(t_1, \ldots, tn) = \bot \] where \(n\) is greater than the cardinality of the type of \(t_1, \ldots, t_n\).

      • BV_TO_NAT_ELIM

        public static final ProofRewriteRule BV_TO_NAT_ELIM
        UF – Bitvector to natural elimination \[ \texttt{bv2nat}(t) = t_1 + \ldots + t_n \] where for \(i=1, \ldots, n\), \(t_i\) is \(\texttt{ite}(x[i-1, i-1] = 1, 2^i, 0)\).

      • INT_TO_BV_ELIM

        public static final ProofRewriteRule INT_TO_BV_ELIM
        UF – Integer to bitvector elimination \[ \texttt{int2bv}_n(t) = (bvconcat t_1 \ldots t_n) \] where for \(i=1, \ldots, n\), \(t_i\) is \(\texttt{ite}(\texttt{mod}(t,2^n) \geq 2^{n-1}, 1, 0)\).

      • MACRO_BOOL_NNF_NORM

        public static final ProofRewriteRule MACRO_BOOL_NNF_NORM
        Booleans – Negation Normal Form with normalization \[ F = G \] where \(G\) is the result of applying negation normal form to \(F\) with additional normalizations, see TheoryBoolRewriter.computeNnfNorm.

      • MACRO_ARITH_STRING_PRED_ENTAIL

        public static final ProofRewriteRule MACRO_ARITH_STRING_PRED_ENTAIL
        Arithmetic – strings predicate entailment \[ (= s t) = c \] \[ (>= s t) = c \] where \(c\) is a Boolean constant. This macro is elaborated by applications of EVALUATE <cvc5.ProofRule.EVALUATE>, ARITH_POLY_NORM <cvc5.ProofRule.ARITH_POLY_NORM>, ARITH_STRING_PRED_ENTAIL <cvc5.ProofRewriteRule.ARITH_STRING_PRED_ENTAIL>, ARITH_STRING_PRED_SAFE_APPROX <cvc5.ProofRewriteRule.ARITH_STRING_PRED_SAFE_APPROX>, as well as other rewrites for normalizing arithmetic predicates.

      • ARITH_STRING_PRED_ENTAIL

        public static final ProofRewriteRule ARITH_STRING_PRED_ENTAIL
        Arithmetic – strings predicate entailment \[ (>= n 0) = true \] Where \(n\) can be shown to be greater than or equal to \(0\) by reasoning about string length being positive and basic properties of addition and multiplication.

      • ARITH_STRING_PRED_SAFE_APPROX

        public static final ProofRewriteRule ARITH_STRING_PRED_SAFE_APPROX
        Arithmetic – strings predicate entailment \[ (>= n 0) = (>= m 0) \] Where \(m\) is a safe under-approximation of \(n\), namely we have that \((>= n m)\) and \((>= m 0)\). In detail, subterms of \(n\) may be replaced with other terms to obtain \(m\) based on the reasoning described in the paper Reynolds et al, CAV 2019, "High-Level Abstractions for Simplifying Extended String Constraints in SMT".

      • ARITH_POW_ELIM

        public static final ProofRewriteRule ARITH_POW_ELIM
        Arithmetic – power elimination \[ (x ^ c) = (x \cdot \ldots \cdot x) \] where \(c\) is a non-negative integer.

      • BETA_REDUCE

        public static final ProofRewriteRule BETA_REDUCE
        Equality – Beta reduction \[ ((\lambda x_1 \ldots x_n.\> t) \ t_1 \ldots t_n) = t\{x_1 \mapsto t_1, \ldots, x_n \mapsto t_n\} \] 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_DISTINCT_ARRAYS

        public static final ProofRewriteRule MACRO_ARRAYS_DISTINCT_ARRAYS
        Arrays – Macro distinct arrays \[ (A = B) = \bot \] where \(A\) and \(B\) are distinct array values, that is, the Node.isConst method returns true for both.

      • MACRO_ARRAYS_NORMALIZE_CONSTANT

        public static final ProofRewriteRule MACRO_ARRAYS_NORMALIZE_CONSTANT
        Arrays – Macro normalize constant \[ A = B \] where \(B\) is the result of normalizing the array value \(A\) into a canonical form, using the internal method TheoryArraysRewriter.normalizeConstant.

      • ARRAYS_EQ_RANGE_EXPAND

        public static final ProofRewriteRule ARRAYS_EQ_RANGE_EXPAND
        Arrays – Expansion of array range equality \[ \mathit{eqrange}(a,b,i,j)= \forall x.\> i \leq x \leq j \rightarrow \mathit{select}(a,x)=\mathit{select}(b,x) \]

      • EXISTS_ELIM

        public static final ProofRewriteRule EXISTS_ELIM
        Quantifiers – Exists elimination \[ \exists x_1\dots x_n.\> F = \neg \forall x_1\dots x_n.\> \neg F \]

      • QUANT_UNUSED_VARS

        public static final ProofRewriteRule QUANT_UNUSED_VARS
        Quantifiers – Unused variables \[ \forall X.\> F = \forall X_1.\> F \] where \(X_1\) is the subset of \(X\) that appear free in \(F\) and \(X_1\) does not contain duplicate variables.

      • MACRO_QUANT_MERGE_PRENEX

        public static final ProofRewriteRule MACRO_QUANT_MERGE_PRENEX
        Quantifiers – Macro merge prenex \[ \forall X_1.\> \ldots \forall X_n.\> F = \forall X.\> F \] where \(X_1 \ldots X_n\) are lists of variables and \(X\) is the result of removing duplicates from \(X_1 \ldots X_n\).

      • QUANT_MERGE_PRENEX

        public static final ProofRewriteRule QUANT_MERGE_PRENEX
        Quantifiers – Merge prenex \[ \forall X_1.\> \ldots \forall X_n.\> F = \forall X_1 \ldots X_n.\> F \] where \(X_1 \ldots X_n\) are lists of variables.

      • MACRO_QUANT_PRENEX

        public static final ProofRewriteRule MACRO_QUANT_PRENEX
        Quantifiers – Macro prenex \[ (\forall X.\> F_1 \vee \cdots \vee (\forall Y.\> F_i) \vee \cdots \vee F_n) = (\forall X Z.\> F_1 \vee \cdots \vee F_i\{ Y \mapsto Z \} \vee \cdots \vee F_n) \]

      • MACRO_QUANT_MINISCOPE

        public static final ProofRewriteRule MACRO_QUANT_MINISCOPE
        Quantifiers – Macro miniscoping \[ \forall X.\> F_1 \wedge \cdots \wedge F_n = G_1 \wedge \cdots \wedge G_n \] where each \(G_i\) is semantically equivalent to \(\forall X.\> F_i\), or alternatively \[ \forall X.\> \ite{C}{F_1}{F_2} = \ite{C}{G_1}{G_2} \] where \(C\) does not have any free variable in \(X\).

      • QUANT_MINISCOPE_AND

        public static final ProofRewriteRule QUANT_MINISCOPE_AND
        Quantifiers – Miniscoping and \[ \forall X.\> F_1 \wedge \ldots \wedge F_n = (\forall X.\> F_1) \wedge \ldots \wedge (\forall X.\> F_n) \]

      • QUANT_MINISCOPE_OR

        public static final ProofRewriteRule QUANT_MINISCOPE_OR
        Quantifiers – Miniscoping or \[ \forall X.\> F_1 \vee \ldots \vee F_n = (\forall X_1.\> F_1) \vee \ldots \vee (\forall X_n.\> F_n) \] where \(X = X_1 \ldots X_n\), and the right hand side does not have any free variable in \(X\).

      • QUANT_MINISCOPE_ITE

        public static final ProofRewriteRule QUANT_MINISCOPE_ITE
        Quantifiers – Miniscoping ite \[ \forall X.\> \ite{C}{F_1}{F_2} = \ite{C}{\forall X.\> F_1}{\forall X.\> F_2} \] where \(C\) does not have any free variable in \(X\).

      • QUANT_DT_SPLIT

        public static final ProofRewriteRule QUANT_DT_SPLIT
        Quantifiers – Datatypes Split \[ (\forall x Y.\> F) = (\forall X_1 Y. F_1) \vee \cdots \vee (\forall X_n Y. F_n) \] where \(x\) is of a datatype type with constructors \(C_1, \ldots, C_n\), where for each \(i = 1, \ldots, n\), \(F_i\) is \(F \{ x \mapsto C_i(X_i) \}\).

      • MACRO_QUANT_PARTITION_CONNECTED_FV

        public static final ProofRewriteRule MACRO_QUANT_PARTITION_CONNECTED_FV
        Quantifiers – Macro connected free variable partitioning \[ \forall X.\> F_1 \vee \ldots \vee F_n = (\forall X_1.\> F_{1,1} \vee \ldots \vee F_{1,k_1}) \vee \ldots \vee (\forall X_m.\> F_{m,1} \vee \ldots \vee F_{m,k_m}) \] where \(X_1, \ldots, X_m\) is a partition of \(X\). This is determined by computing the connected components when considering two variables in \(X\) to be connected if they occur in the same \(F_i\).

      • MACRO_QUANT_VAR_ELIM_EQ

        public static final ProofRewriteRule MACRO_QUANT_VAR_ELIM_EQ
        Quantifiers – Macro variable elimination equality \[ \forall x Y.\> F = \forall Y.\> F \{ x \mapsto t \} \] where \(\neg F\) entails \(x = t\).

      • QUANT_VAR_ELIM_EQ

        public static final ProofRewriteRule QUANT_VAR_ELIM_EQ
        Quantifiers – Macro variable elimination equality .. math. (\forall x.\> x \neq t \vee F) = F \{ x \mapsto t \} or alternatively .. math. (\forall x.\> x \neq t) = \bot

      • MACRO_QUANT_VAR_ELIM_INEQ

        public static final ProofRewriteRule MACRO_QUANT_VAR_ELIM_INEQ
        Quantifiers – Macro variable elimination inequality \[ \forall x Y.\> F = \forall Y.\> G \] where \(G\) is the result of replacing all literals containing \(x\) with a constant. This is applied only when all such literals are lower (resp. upper) bounds for \(x\).

      • MACRO_QUANT_REWRITE_BODY

        public static final ProofRewriteRule MACRO_QUANT_REWRITE_BODY
        Quantifiers – Macro quantifiers rewrite body \[ \forall X.\> F = \forall X.\> G \] where \(G\) is semantically equivalent to \(F\).

      • DT_INST

        public static final ProofRewriteRule DT_INST
        Datatypes – Instantiation \[ \mathit{is}_C(t) = (t = C(\mathit{sel}_1(t),\dots,\mathit{sel}_n(t))) \] where \(C\) is the \(n^{\mathit{th}}\) constructor of the type of \(t\), and \(\mathit{is}_C\) is the discriminator (tester) for \(C\).

      • DT_COLLAPSE_SELECTOR

        public static final ProofRewriteRule DT_COLLAPSE_SELECTOR
        Datatypes – collapse selector \[ s_i(c(t_1, \ldots, t_n)) = t_i \] where \(s_i\) is the \(i^{th}\) selector for constructor \(c\).

      • DT_COLLAPSE_TESTER

        public static final ProofRewriteRule DT_COLLAPSE_TESTER
        Datatypes – collapse tester \[ \mathit{is}_c(c(t_1, \ldots, t_n)) = true \] or alternatively \[ \mathit{is}_c(d(t_1, \ldots, t_n)) = false \] where \(c\) and \(d\) are distinct constructors.

      • DT_COLLAPSE_TESTER_SINGLETON

        public static final ProofRewriteRule DT_COLLAPSE_TESTER_SINGLETON
        Datatypes – collapse tester \[ \mathit{is}_c(t) = true \] where \(c\) is the only constructor of its associated datatype.

      • MACRO_DT_CONS_EQ

        public static final ProofRewriteRule MACRO_DT_CONS_EQ
        Datatypes – Macro constructor equality \[ (t = s) = (t_1 = s_1 \wedge \ldots \wedge t_n = s_n) \] where \(t_1, \ldots, t_n\) and \(s_1, \ldots, s_n\) are subterms of \(t\) and \(s\) that occur at the same position respectively (beneath constructor applications), or alternatively \[ (t = s) = false \] where \(t\) and \(s\) have subterms that occur in the same position (beneath constructor applications) that are distinct.

      • DT_CONS_EQ

        public static final ProofRewriteRule DT_CONS_EQ
        Datatypes – constructor equality \[ (c(t_1, \ldots, t_n) = c(s_1, \ldots, s_n)) = (t_1 = s_1 \wedge \ldots \wedge t_n = s_n) \] where \(c\) is a constructor.

      • DT_CONS_EQ_CLASH

        public static final ProofRewriteRule DT_CONS_EQ_CLASH
        Datatypes – constructor equality clash \[ (t = s) = false \] where \(t\) and \(s\) have subterms that occur in the same position (beneath constructor applications) that are distinct constructor applications.

      • DT_CYCLE

        public static final ProofRewriteRule DT_CYCLE
        Datatypes – cycle \[ (x = t[x]) = \bot \] where all terms on the path to \(x\) in \(t[x]\) are applications of constructors, and this path is non-empty.

      • DT_COLLAPSE_UPDATER

        public static final ProofRewriteRule DT_COLLAPSE_UPDATER
        Datatypes – collapse tester \[ u_{c,i}(c(t_1, \ldots, t_i, \ldots, t_n), s) = c(t_1, \ldots, s, \ldots, t_n) \] or alternatively \[ u_{c,i}(d(t_1, \ldots, t_n), s) = d(t_1, \ldots, t_n) \] where \(c\) and \(d\) are distinct constructors.

      • DT_UPDATER_ELIM

        public static final ProofRewriteRule DT_UPDATER_ELIM
        Datatypes - updater elimination \[ u_{c,i}(t, s) = ite(\mathit{is}_c(t), c(s_0(t), \ldots, s, \ldots s_n(t)), t) \] where \(s_i\) is the \(i^{th}\) selector for constructor \(c\).

      • DT_MATCH_ELIM

        public static final ProofRewriteRule DT_MATCH_ELIM
        Datatypes – match elimination \[ \texttt{match}(t ((p_1 c_1) \ldots (p_n c_n))) = \texttt{ite}(F_1, r_1, \texttt{ite}( \ldots, r_n)) \] where for \(i=1, \ldots, n\), \(F_1\) is a formula that holds iff \(t\) matches \(p_i\) and \(r_i\) is the result of a substitution on \(c_i\) based on this match.

      • BV_UMULO_ELIMINATE

        public static final ProofRewriteRule BV_UMULO_ELIMINATE
        Bitvectors – Unsigned multiplication overflow detection elimination See M.Gok, M.J. Schulte, P.I. Balzola, "Efficient integer multiplication overflow detection circuits", 2001. http:

      • BV_SMULO_ELIMINATE

        public static final ProofRewriteRule BV_SMULO_ELIMINATE
        Bitvectors – Unsigned multiplication overflow detection elimination See M.Gok, M.J. Schulte, P.I. Balzola, "Efficient integer multiplication overflow detection circuits", 2001. http:

      • BV_ADD_COMBINE_LIKE_TERMS

        public static final ProofRewriteRule BV_ADD_COMBINE_LIKE_TERMS
        Bitvectors – Combine like terms during addition by counting terms

      • BV_MULT_SIMPLIFY

        public static final ProofRewriteRule BV_MULT_SIMPLIFY
        Bitvectors – Extract negations from multiplicands \[ bvmul(bvneg(a),\ b,\ c) = bvneg(bvmul(a,\ b,\ c)) \]

      • BV_BITWISE_SLICING

        public static final ProofRewriteRule BV_BITWISE_SLICING
        Bitvectors – Extract continuous substrings of bitvectors \[ bvand(a,\ c) = concat(bvand(a[i_0:j_0],\ c_0) ... bvand(a[i_n:j_n],\ c_n)) \] where c0,..., cn are maximally continuous substrings of 0 or 1 in the constant c

      • BV_REPEAT_ELIM

        public static final ProofRewriteRule BV_REPEAT_ELIM
        Bitvectors – Extract continuous substrings of bitvectors \[ repeat(n,\ t) = concat(t ... t) \] where \(t\) is repeated \(n\) times.

      • STR_CTN_MULTISET_SUBSET

        public static final ProofRewriteRule STR_CTN_MULTISET_SUBSET
        Strings – String contains multiset subset \[ 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\).

      • 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\).

      • RE_INTER_UNION_INCLUSION

        public static final ProofRewriteRule RE_INTER_UNION_INCLUSION
        Strings – regular expression intersection/union inclusion \[ (re.inter\ R) = \mathit{re.inter}(\mathit{re.none}, R_0) \] where \(R\) is a list of regular expressions containing `r_1`, `re.comp(r_2)` and the list \(R_0\) where `r_2` is a superset of `r_1`. or alternatively: \[ \mathit{re.union}(R) = \mathit{re.union}(\mathit{re}.\text{*}(\mathit{re.allchar}),\ R_0) \] where \(R\) is a list of regular expressions containing `r_1`, `re.comp(r_2)` and the list \(R_0\), where `r_1` is a superset of `r_2`.

      • STR_IN_RE_EVAL

        public static final ProofRewriteRule STR_IN_RE_EVAL
        Strings – regular expression membership evaluation \[ \mathit{str.in\_re}(s, R) = c \] where \(s\) is a constant string, \(R\) is a constant regular expression and \(c\) is true or false.

      • STR_IN_RE_CONSUME

        public static final ProofRewriteRule STR_IN_RE_CONSUME
        Strings – regular expression membership consume \[ \mathit{str.in_re}(s, R) = b \] where \(b\) is either \(false\) or the result of stripping entailed prefixes and suffixes off of \(s\) and \(R\).

      • STR_IN_RE_CONCAT_STAR_CHAR

        public static final ProofRewriteRule STR_IN_RE_CONCAT_STAR_CHAR
        Strings – string in regular expression concatenation star character \[ \mathit{str.in\_re}(\mathit{str}.\text{++}(s_1, \ldots, s_n), \mathit{re}.\text{*}(R)) =\\ \mathit{str.in\_re}(s_1, \mathit{re}.\text{*}(R)) \wedge \ldots \wedge \mathit{str.in\_re}(s_n, \mathit{re}.\text{*}(R)) \] where all strings in \(R\) have length one.

      • STR_IN_RE_SIGMA

        public static final ProofRewriteRule STR_IN_RE_SIGMA
        Strings – string in regular expression sigma \[ \mathit{str.in\_re}(s, \mathit{re}.\text{++}(\mathit{re.allchar}, \ldots, \mathit{re.allchar})) = (\mathit{str.len}(s) = n) \] or alternatively: \[ \mathit{str.in\_re}(s, \mathit{re}.\text{++}(\mathit{re.allchar}, \ldots, \mathit{re.allchar}, \mathit{re}.\text{*}(\mathit{re.allchar}))) = (\mathit{str.len}(s) \ge n) \]

      • STR_IN_RE_SIGMA_STAR

        public static final ProofRewriteRule STR_IN_RE_SIGMA_STAR
        Strings – string in regular expression sigma star \[ \mathit{str.in\_re}(s, \mathit{re}.\text{*}(\mathit{re}.\text{++}(\mathit{re.allchar}, \ldots, \mathit{re.allchar}))) = (\mathit{str.len}(s) \ \% \ n = 0) \] where \(n\) is the number of \(\mathit{re.allchar}\) arguments to \(\mathit{re}.\text{++}\).

      • MACRO_SUBSTR_STRIP_SYM_LENGTH

        public static final ProofRewriteRule MACRO_SUBSTR_STRIP_SYM_LENGTH
        Strings – strings substring strip symbolic length \[ str.substr(s, n, m) = t \] where \(t\) is obtained by fully or partially stripping components of \(s\) based on \(n\) and \(m\).

      • MACRO_SETS_DISTINCT_SETS

        public static final ProofRewriteRule MACRO_SETS_DISTINCT_SETS
        Sets – distinct sets \[ (A = B) = \bot \] where \(A\) and \(B\) are distinct set values, that is, the Node.isConst method returns true for both. This rule verifies that this returns true for both terms and that these terms are distinct.

      • MACRO_SETS_INTER_EVAL

        public static final ProofRewriteRule MACRO_SETS_INTER_EVAL
        Sets – sets intersection evaluate \[ \mathit{set.inter}(t_1, t_2) = t \] where \(t_1\) and \(t_2\) are set values, that is, the Node.isConst method returns true for both, and where \(t\) is an intersection of the component elements of \(t_1\) and \(t_2\).

      • MACRO_SETS_MINUS_EVAL

        public static final ProofRewriteRule MACRO_SETS_MINUS_EVAL
        Sets – sets minus evaluate \[ \mathit{set.minus}(t_1, t_2) = t \] where \(t_1\) and \(t_2\) are set values, that is, the Node.isConst method returns true for both, and where \(t\) is the difference of the component elements of \(t_1\) and \(t_2\).

      • SETS_UNION_NORM

        public static final ProofRewriteRule SETS_UNION_NORM
        Sets – sets union normalize \[ \mathit{set.union}(t_1, t_2) = t \] where \(t\) is a union of the component elements of \(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_IS_EMPTY_EVAL

        public static final ProofRewriteRule SETS_IS_EMPTY_EVAL
        Sets – empty tester evaluation \[ \mathit{sets.is\_empty}(\epsilon) = \top \] where \(\epsilon\) is the empty set, or alternatively: \[ \mathit{sets.is\_empty}(c) = \bot \] where \(c\) is a constant set that is not the empty set.

      • SETS_INSERT_ELIM

        public static final ProofRewriteRule SETS_INSERT_ELIM
        Sets – sets insert elimination \[ \mathit{sets.insert}(t_1, \ldots, t_n, S) = \texttt{set.union}(\texttt{sets.singleton}(t_1), \ldots, \texttt{sets.singleton}(t_n), S) \]

      • ARITH_MUL_ONE

        public static final ProofRewriteRule ARITH_MUL_ONE
        Auto-generated from RARE rule arith-mul-one

      • ARITH_MUL_ZERO

        public static final ProofRewriteRule ARITH_MUL_ZERO
        Auto-generated from RARE rule arith-mul-zero

      • ARITH_DIV_TOTAL_REAL

        public static final ProofRewriteRule ARITH_DIV_TOTAL_REAL
        Auto-generated from RARE rule arith-div-total-real

      • ARITH_DIV_TOTAL_INT

        public static final ProofRewriteRule ARITH_DIV_TOTAL_INT
        Auto-generated from RARE rule arith-div-total-int

      • ARITH_DIV_TOTAL_ZERO_REAL

        public static final ProofRewriteRule ARITH_DIV_TOTAL_ZERO_REAL
        Auto-generated from RARE rule arith-div-total-zero-real

      • ARITH_DIV_TOTAL_ZERO_INT

        public static final ProofRewriteRule ARITH_DIV_TOTAL_ZERO_INT
        Auto-generated from RARE rule arith-div-total-zero-int

      • ARITH_INT_DIV_TOTAL

        public static final ProofRewriteRule ARITH_INT_DIV_TOTAL
        Auto-generated from RARE rule arith-int-div-total

      • ARITH_INT_DIV_TOTAL_ONE

        public static final ProofRewriteRule ARITH_INT_DIV_TOTAL_ONE
        Auto-generated from RARE rule arith-int-div-total-one

      • ARITH_INT_DIV_TOTAL_ZERO

        public static final ProofRewriteRule ARITH_INT_DIV_TOTAL_ZERO
        Auto-generated from RARE rule arith-int-div-total-zero

      • ARITH_INT_MOD_TOTAL

        public static final ProofRewriteRule ARITH_INT_MOD_TOTAL
        Auto-generated from RARE rule arith-int-mod-total

      • ARITH_INT_MOD_TOTAL_ONE

        public static final ProofRewriteRule ARITH_INT_MOD_TOTAL_ONE
        Auto-generated from RARE rule arith-int-mod-total-one

      • ARITH_INT_MOD_TOTAL_ZERO

        public static final ProofRewriteRule ARITH_INT_MOD_TOTAL_ZERO
        Auto-generated from RARE rule arith-int-mod-total-zero

      • ARITH_ELIM_GT

        public static final ProofRewriteRule ARITH_ELIM_GT
        Auto-generated from RARE rule arith-elim-gt

      • ARITH_ELIM_LT

        public static final ProofRewriteRule ARITH_ELIM_LT
        Auto-generated from RARE rule arith-elim-lt

      • ARITH_ELIM_INT_GT

        public static final ProofRewriteRule ARITH_ELIM_INT_GT
        Auto-generated from RARE rule arith-elim-int-gt

      • ARITH_ELIM_INT_LT

        public static final ProofRewriteRule ARITH_ELIM_INT_LT
        Auto-generated from RARE rule arith-elim-int-lt

      • ARITH_ELIM_LEQ

        public static final ProofRewriteRule ARITH_ELIM_LEQ
        Auto-generated from RARE rule arith-elim-leq

      • ARITH_LEQ_NORM

        public static final ProofRewriteRule ARITH_LEQ_NORM
        Auto-generated from RARE rule arith-leq-norm

      • ARITH_GEQ_TIGHTEN

        public static final ProofRewriteRule ARITH_GEQ_TIGHTEN
        Auto-generated from RARE rule arith-geq-tighten

      • ARITH_GEQ_NORM1_INT

        public static final ProofRewriteRule ARITH_GEQ_NORM1_INT
        Auto-generated from RARE rule arith-geq-norm1-int

      • ARITH_GEQ_NORM1_REAL

        public static final ProofRewriteRule ARITH_GEQ_NORM1_REAL
        Auto-generated from RARE rule arith-geq-norm1-real

      • ARITH_GEQ_NORM2

        public static final ProofRewriteRule ARITH_GEQ_NORM2
        Auto-generated from RARE rule arith-geq-norm2

      • ARITH_REFL_LEQ

        public static final ProofRewriteRule ARITH_REFL_LEQ
        Auto-generated from RARE rule arith-refl-leq

      • ARITH_REFL_LT

        public static final ProofRewriteRule ARITH_REFL_LT
        Auto-generated from RARE rule arith-refl-lt

      • ARITH_REFL_GEQ

        public static final ProofRewriteRule ARITH_REFL_GEQ
        Auto-generated from RARE rule arith-refl-geq

      • ARITH_REFL_GT

        public static final ProofRewriteRule ARITH_REFL_GT
        Auto-generated from RARE rule arith-refl-gt

      • ARITH_EQ_ELIM_REAL

        public static final ProofRewriteRule ARITH_EQ_ELIM_REAL
        Auto-generated from RARE rule arith-eq-elim-real

      • ARITH_EQ_ELIM_INT

        public static final ProofRewriteRule ARITH_EQ_ELIM_INT
        Auto-generated from RARE rule arith-eq-elim-int

      • ARITH_PLUS_FLATTEN

        public static final ProofRewriteRule ARITH_PLUS_FLATTEN
        Auto-generated from RARE rule arith-plus-flatten

      • ARITH_MULT_FLATTEN

        public static final ProofRewriteRule ARITH_MULT_FLATTEN
        Auto-generated from RARE rule arith-mult-flatten

      • ARITH_MULT_DIST

        public static final ProofRewriteRule ARITH_MULT_DIST
        Auto-generated from RARE rule arith-mult-dist

      • ARITH_ABS_ELIM_INT

        public static final ProofRewriteRule ARITH_ABS_ELIM_INT
        Auto-generated from RARE rule arith-abs-elim-int

      • ARITH_ABS_ELIM_REAL

        public static final ProofRewriteRule ARITH_ABS_ELIM_REAL
        Auto-generated from RARE rule arith-abs-elim-real

      • ARITH_TO_REAL_ELIM

        public static final ProofRewriteRule ARITH_TO_REAL_ELIM
        Auto-generated from RARE rule arith-to-real-elim

      • ARITH_TO_INT_ELIM_TO_REAL

        public static final ProofRewriteRule ARITH_TO_INT_ELIM_TO_REAL
        Auto-generated from RARE rule arith-to-int-elim-to-real

      • ARITH_DIV_ELIM_TO_REAL1

        public static final ProofRewriteRule ARITH_DIV_ELIM_TO_REAL1
        Auto-generated from RARE rule arith-div-elim-to-real1

      • ARITH_DIV_ELIM_TO_REAL2

        public static final ProofRewriteRule ARITH_DIV_ELIM_TO_REAL2
        Auto-generated from RARE rule arith-div-elim-to-real2

      • ARITH_SINE_ZERO

        public static final ProofRewriteRule ARITH_SINE_ZERO
        Auto-generated from RARE rule arith-sine-zero

      • ARITH_SINE_PI2

        public static final ProofRewriteRule ARITH_SINE_PI2
        Auto-generated from RARE rule arith-sine-pi2

      • ARITH_COSINE_ELIM

        public static final ProofRewriteRule ARITH_COSINE_ELIM
        Auto-generated from RARE rule arith-cosine-elim

      • ARITH_TANGENT_ELIM

        public static final ProofRewriteRule ARITH_TANGENT_ELIM
        Auto-generated from RARE rule arith-tangent-elim

      • ARITH_SECENT_ELIM

        public static final ProofRewriteRule ARITH_SECENT_ELIM
        Auto-generated from RARE rule arith-secent-elim

      • ARITH_COSECENT_ELIM

        public static final ProofRewriteRule ARITH_COSECENT_ELIM
        Auto-generated from RARE rule arith-cosecent-elim

      • ARITH_COTANGENT_ELIM

        public static final ProofRewriteRule ARITH_COTANGENT_ELIM
        Auto-generated from RARE rule arith-cotangent-elim

      • ARITH_PI_NOT_INT

        public static final ProofRewriteRule ARITH_PI_NOT_INT
        Auto-generated from RARE rule arith-pi-not-int

      • ARITH_ABS_EQ

        public static final ProofRewriteRule ARITH_ABS_EQ
        Auto-generated from RARE rule arith-abs-eq

      • ARITH_ABS_INT_GT

        public static final ProofRewriteRule ARITH_ABS_INT_GT
        Auto-generated from RARE rule arith-abs-int-gt

      • ARITH_ABS_REAL_GT

        public static final ProofRewriteRule ARITH_ABS_REAL_GT
        Auto-generated from RARE rule arith-abs-real-gt

      • ARRAY_READ_OVER_WRITE

        public static final ProofRewriteRule ARRAY_READ_OVER_WRITE
        Auto-generated from RARE rule array-read-over-write

      • ARRAY_READ_OVER_WRITE2

        public static final ProofRewriteRule ARRAY_READ_OVER_WRITE2
        Auto-generated from RARE rule array-read-over-write2

      • ARRAY_STORE_OVERWRITE

        public static final ProofRewriteRule ARRAY_STORE_OVERWRITE
        Auto-generated from RARE rule array-store-overwrite

      • ARRAY_STORE_SELF

        public static final ProofRewriteRule ARRAY_STORE_SELF
        Auto-generated from RARE rule array-store-self

      • ARRAY_READ_OVER_WRITE_SPLIT

        public static final ProofRewriteRule ARRAY_READ_OVER_WRITE_SPLIT
        Auto-generated from RARE rule array-read-over-write-split

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

        public static final ProofRewriteRule BOOL_OR_TRUE
        Auto-generated from RARE rule boolean-or-true

      • BOOL_OR_FLATTEN

        public static final ProofRewriteRule BOOL_OR_FLATTEN
        Auto-generated from RARE rule boolean-or-flatten

      • BOOL_AND_FALSE

        public static final ProofRewriteRule BOOL_AND_FALSE
        Auto-generated from RARE rule boolean-and-false

      • BOOL_AND_FLATTEN

        public static final ProofRewriteRule BOOL_AND_FLATTEN
        Auto-generated from RARE rule boolean-and-flatten

      • BOOL_AND_CONF

        public static final ProofRewriteRule BOOL_AND_CONF
        Auto-generated from RARE rule boolean-and-conf

      • BOOL_AND_CONF2

        public static final ProofRewriteRule BOOL_AND_CONF2
        Auto-generated from RARE rule boolean-and-conf2

      • BOOL_OR_TAUT

        public static final ProofRewriteRule BOOL_OR_TAUT
        Auto-generated from RARE rule boolean-or-taut

      • BOOL_OR_TAUT2

        public static final ProofRewriteRule BOOL_OR_TAUT2
        Auto-generated from RARE rule boolean-or-taut2

      • BOOL_OR_DE_MORGAN

        public static final ProofRewriteRule BOOL_OR_DE_MORGAN
        Auto-generated from RARE rule boolean-or-de-morgan

      • BOOL_IMPLIES_DE_MORGAN

        public static final ProofRewriteRule BOOL_IMPLIES_DE_MORGAN
        Auto-generated from RARE rule boolean-implies-de-morgan

      • BOOL_AND_DE_MORGAN

        public static final ProofRewriteRule BOOL_AND_DE_MORGAN
        Auto-generated from RARE rule boolean-and-de-morgan

      • BOOL_OR_AND_DISTRIB

        public static final ProofRewriteRule BOOL_OR_AND_DISTRIB
        Auto-generated from RARE rule boolean-or-and-distrib

      • BOOL_XOR_REFL

        public static final ProofRewriteRule BOOL_XOR_REFL
        Auto-generated from RARE rule boolean-xor-refl

      • BOOL_XOR_NREFL

        public static final ProofRewriteRule BOOL_XOR_NREFL
        Auto-generated from RARE rule boolean-xor-nrefl

      • BOOL_XOR_FALSE

        public static final ProofRewriteRule BOOL_XOR_FALSE
        Auto-generated from RARE rule boolean-xor-false

      • BOOL_XOR_TRUE

        public static final ProofRewriteRule BOOL_XOR_TRUE
        Auto-generated from RARE rule boolean-xor-true

      • BOOL_XOR_COMM

        public static final ProofRewriteRule BOOL_XOR_COMM
        Auto-generated from RARE rule boolean-xor-comm

      • BOOL_XOR_ELIM

        public static final ProofRewriteRule BOOL_XOR_ELIM
        Auto-generated from RARE rule boolean-xor-elim

      • BOOL_NOT_XOR_ELIM

        public static final ProofRewriteRule BOOL_NOT_XOR_ELIM
        Auto-generated from RARE rule boolean-not-xor-elim

      • BOOL_NOT_EQ_ELIM1

        public static final ProofRewriteRule BOOL_NOT_EQ_ELIM1
        Auto-generated from RARE rule boolean-not-eq-elim1

      • BOOL_NOT_EQ_ELIM2

        public static final ProofRewriteRule BOOL_NOT_EQ_ELIM2
        Auto-generated from RARE rule boolean-not-eq-elim2

      • ITE_NEG_BRANCH

        public static final ProofRewriteRule ITE_NEG_BRANCH
        Auto-generated from RARE rule ite-neg-branch

      • ITE_THEN_TRUE

        public static final ProofRewriteRule ITE_THEN_TRUE
        Auto-generated from RARE rule ite-then-true

      • ITE_ELSE_FALSE

        public static final ProofRewriteRule ITE_ELSE_FALSE
        Auto-generated from RARE rule ite-else-false

      • ITE_THEN_FALSE

        public static final ProofRewriteRule ITE_THEN_FALSE
        Auto-generated from RARE rule ite-then-false

      • ITE_ELSE_TRUE

        public static final ProofRewriteRule ITE_ELSE_TRUE
        Auto-generated from RARE rule ite-else-true

      • ITE_THEN_LOOKAHEAD_SELF

        public static final ProofRewriteRule ITE_THEN_LOOKAHEAD_SELF
        Auto-generated from RARE rule ite-then-lookahead-self

      • ITE_ELSE_LOOKAHEAD_SELF

        public static final ProofRewriteRule ITE_ELSE_LOOKAHEAD_SELF
        Auto-generated from RARE rule ite-else-lookahead-self

      • ITE_THEN_LOOKAHEAD_NOT_SELF

        public static final ProofRewriteRule ITE_THEN_LOOKAHEAD_NOT_SELF
        Auto-generated from RARE rule ite-then-lookahead-not-self

      • ITE_ELSE_LOOKAHEAD_NOT_SELF

        public static final ProofRewriteRule ITE_ELSE_LOOKAHEAD_NOT_SELF
        Auto-generated from RARE rule ite-else-lookahead-not-self

      • ITE_EXPAND

        public static final ProofRewriteRule ITE_EXPAND
        Auto-generated from RARE rule ite-expand

      • BOOL_NOT_ITE_ELIM

        public static final ProofRewriteRule BOOL_NOT_ITE_ELIM
        Auto-generated from RARE rule boolean-not-ite-elim

      • ITE_TRUE_COND

        public static final ProofRewriteRule ITE_TRUE_COND
        Auto-generated from RARE rule ite-true-cond

      • ITE_FALSE_COND

        public static final ProofRewriteRule ITE_FALSE_COND
        Auto-generated from RARE rule ite-false-cond

      • ITE_NOT_COND

        public static final ProofRewriteRule ITE_NOT_COND
        Auto-generated from RARE rule ite-not-cond

      • ITE_EQ_BRANCH

        public static final ProofRewriteRule ITE_EQ_BRANCH
        Auto-generated from RARE rule ite-eq-branch

      • ITE_THEN_LOOKAHEAD

        public static final ProofRewriteRule ITE_THEN_LOOKAHEAD
        Auto-generated from RARE rule ite-then-lookahead

      • ITE_ELSE_LOOKAHEAD

        public static final ProofRewriteRule ITE_ELSE_LOOKAHEAD
        Auto-generated from RARE rule ite-else-lookahead

      • ITE_THEN_NEG_LOOKAHEAD

        public static final ProofRewriteRule ITE_THEN_NEG_LOOKAHEAD
        Auto-generated from RARE rule ite-then-neg-lookahead

      • ITE_ELSE_NEG_LOOKAHEAD

        public static final ProofRewriteRule ITE_ELSE_NEG_LOOKAHEAD
        Auto-generated from RARE rule ite-else-neg-lookahead

      • BV_CONCAT_FLATTEN

        public static final ProofRewriteRule BV_CONCAT_FLATTEN
        Auto-generated from RARE rule bv-concat-flatten

      • BV_CONCAT_EXTRACT_MERGE

        public static final ProofRewriteRule BV_CONCAT_EXTRACT_MERGE
        Auto-generated from RARE rule bv-concat-extract-merge

      • BV_EXTRACT_EXTRACT

        public static final ProofRewriteRule BV_EXTRACT_EXTRACT
        Auto-generated from RARE rule bv-extract-extract

      • BV_EXTRACT_WHOLE

        public static final ProofRewriteRule BV_EXTRACT_WHOLE
        Auto-generated from RARE rule bv-extract-whole

      • BV_EXTRACT_CONCAT_1

        public static final ProofRewriteRule BV_EXTRACT_CONCAT_1
        Auto-generated from RARE rule bv-extract-concat-1

      • BV_EXTRACT_CONCAT_2

        public static final ProofRewriteRule BV_EXTRACT_CONCAT_2
        Auto-generated from RARE rule bv-extract-concat-2

      • BV_EXTRACT_CONCAT_3

        public static final ProofRewriteRule BV_EXTRACT_CONCAT_3
        Auto-generated from RARE rule bv-extract-concat-3

      • BV_EXTRACT_CONCAT_4

        public static final ProofRewriteRule BV_EXTRACT_CONCAT_4
        Auto-generated from RARE rule bv-extract-concat-4

      • BV_EQ_EXTRACT_ELIM1

        public static final ProofRewriteRule BV_EQ_EXTRACT_ELIM1
        Auto-generated from RARE rule bv-eq-extract-elim1

      • BV_EQ_EXTRACT_ELIM2

        public static final ProofRewriteRule BV_EQ_EXTRACT_ELIM2
        Auto-generated from RARE rule bv-eq-extract-elim2

      • BV_EQ_EXTRACT_ELIM3

        public static final ProofRewriteRule BV_EQ_EXTRACT_ELIM3
        Auto-generated from RARE rule bv-eq-extract-elim3

      • BV_EXTRACT_BITWISE_AND

        public static final ProofRewriteRule BV_EXTRACT_BITWISE_AND
        Auto-generated from RARE rule bv-extract-bitwise-and

      • BV_EXTRACT_BITWISE_OR

        public static final ProofRewriteRule BV_EXTRACT_BITWISE_OR
        Auto-generated from RARE rule bv-extract-bitwise-or

      • BV_EXTRACT_BITWISE_XOR

        public static final ProofRewriteRule BV_EXTRACT_BITWISE_XOR
        Auto-generated from RARE rule bv-extract-bitwise-xor

      • BV_EXTRACT_NOT

        public static final ProofRewriteRule BV_EXTRACT_NOT
        Auto-generated from RARE rule bv-extract-not

      • BV_EXTRACT_SIGN_EXTEND_1

        public static final ProofRewriteRule BV_EXTRACT_SIGN_EXTEND_1
        Auto-generated from RARE rule bv-extract-sign-extend-1

      • BV_EXTRACT_SIGN_EXTEND_2

        public static final ProofRewriteRule BV_EXTRACT_SIGN_EXTEND_2
        Auto-generated from RARE rule bv-extract-sign-extend-2

      • BV_EXTRACT_SIGN_EXTEND_3

        public static final ProofRewriteRule BV_EXTRACT_SIGN_EXTEND_3
        Auto-generated from RARE rule bv-extract-sign-extend-3

      • BV_NEG_MULT

        public static final ProofRewriteRule BV_NEG_MULT
        Auto-generated from RARE rule bv-neg-mult

      • BV_NEG_ADD

        public static final ProofRewriteRule BV_NEG_ADD
        Auto-generated from RARE rule bv-neg-add

      • BV_MULT_DISTRIB_CONST_NEG

        public static final ProofRewriteRule BV_MULT_DISTRIB_CONST_NEG
        Auto-generated from RARE rule bv-mult-distrib--neg

      • BV_MULT_DISTRIB_CONST_ADD

        public static final ProofRewriteRule BV_MULT_DISTRIB_CONST_ADD
        Auto-generated from RARE rule bv-mult-distrib--add

      • BV_MULT_DISTRIB_CONST_SUB

        public static final ProofRewriteRule BV_MULT_DISTRIB_CONST_SUB
        Auto-generated from RARE rule bv-mult-distrib--sub

      • BV_MULT_DISTRIB_1

        public static final ProofRewriteRule BV_MULT_DISTRIB_1
        Auto-generated from RARE rule bv-mult-distrib-1

      • BV_MULT_DISTRIB_2

        public static final ProofRewriteRule BV_MULT_DISTRIB_2
        Auto-generated from RARE rule bv-mult-distrib-2

      • BV_NOT_XOR

        public static final ProofRewriteRule BV_NOT_XOR
        Auto-generated from RARE rule bv-not-xor

      • BV_AND_SIMPLIFY_1

        public static final ProofRewriteRule BV_AND_SIMPLIFY_1
        Auto-generated from RARE rule bv-and-simplify-1

      • BV_AND_SIMPLIFY_2

        public static final ProofRewriteRule BV_AND_SIMPLIFY_2
        Auto-generated from RARE rule bv-and-simplify-2

      • BV_OR_SIMPLIFY_1

        public static final ProofRewriteRule BV_OR_SIMPLIFY_1
        Auto-generated from RARE rule bv-or-simplify-1

      • BV_OR_SIMPLIFY_2

        public static final ProofRewriteRule BV_OR_SIMPLIFY_2
        Auto-generated from RARE rule bv-or-simplify-2

      • BV_XOR_SIMPLIFY_1

        public static final ProofRewriteRule BV_XOR_SIMPLIFY_1
        Auto-generated from RARE rule bv-xor-simplify-1

      • BV_XOR_SIMPLIFY_2

        public static final ProofRewriteRule BV_XOR_SIMPLIFY_2
        Auto-generated from RARE rule bv-xor-simplify-2

      • BV_XOR_SIMPLIFY_3

        public static final ProofRewriteRule BV_XOR_SIMPLIFY_3
        Auto-generated from RARE rule bv-xor-simplify-3

      • BV_ULT_ADD_ONE

        public static final ProofRewriteRule BV_ULT_ADD_ONE
        Auto-generated from RARE rule bv-ult-add-one

      • BV_CONCAT_TO_MULT

        public static final ProofRewriteRule BV_CONCAT_TO_MULT
        Auto-generated from RARE rule bv-concat-to-mult

      • BV_MULT_SLT_MULT_1

        public static final ProofRewriteRule BV_MULT_SLT_MULT_1
        Auto-generated from RARE rule bv-mult-slt-mult-1

      • BV_MULT_SLT_MULT_2

        public static final ProofRewriteRule BV_MULT_SLT_MULT_2
        Auto-generated from RARE rule bv-mult-slt-mult-2

      • BV_COMMUTATIVE_AND

        public static final ProofRewriteRule BV_COMMUTATIVE_AND
        Auto-generated from RARE rule bv-commutative-and

      • BV_COMMUTATIVE_OR

        public static final ProofRewriteRule BV_COMMUTATIVE_OR
        Auto-generated from RARE rule bv-commutative-or

      • BV_COMMUTATIVE_XOR

        public static final ProofRewriteRule BV_COMMUTATIVE_XOR
        Auto-generated from RARE rule bv-commutative-xor

      • BV_COMMUTATIVE_MUL

        public static final ProofRewriteRule BV_COMMUTATIVE_MUL
        Auto-generated from RARE rule bv-commutative-mul

      • BV_OR_ZERO

        public static final ProofRewriteRule BV_OR_ZERO
        Auto-generated from RARE rule bv-or-zero

      • BV_MUL_ONE

        public static final ProofRewriteRule BV_MUL_ONE
        Auto-generated from RARE rule bv-mul-one

      • BV_MUL_ZERO

        public static final ProofRewriteRule BV_MUL_ZERO
        Auto-generated from RARE rule bv-mul-zero

      • BV_ADD_ZERO

        public static final ProofRewriteRule BV_ADD_ZERO
        Auto-generated from RARE rule bv-add-zero

      • BV_ADD_TWO

        public static final ProofRewriteRule BV_ADD_TWO
        Auto-generated from RARE rule bv-add-two

      • BV_ZERO_EXTEND_ELIMINATE_0

        public static final ProofRewriteRule BV_ZERO_EXTEND_ELIMINATE_0
        Auto-generated from RARE rule bv-zero-extend-eliminate-0

      • BV_SIGN_EXTEND_ELIMINATE_0

        public static final ProofRewriteRule BV_SIGN_EXTEND_ELIMINATE_0
        Auto-generated from RARE rule bv-sign-extend-eliminate-0

      • BV_NOT_NEQ

        public static final ProofRewriteRule BV_NOT_NEQ
        Auto-generated from RARE rule bv-not-neq

      • BV_ULT_ONES

        public static final ProofRewriteRule BV_ULT_ONES
        Auto-generated from RARE rule bv-ult-ones

      • BV_OR_FLATTEN

        public static final ProofRewriteRule BV_OR_FLATTEN
        Auto-generated from RARE rule bv-or-flatten

      • BV_XOR_FLATTEN

        public static final ProofRewriteRule BV_XOR_FLATTEN
        Auto-generated from RARE rule bv-xor-flatten

      • BV_AND_FLATTEN

        public static final ProofRewriteRule BV_AND_FLATTEN
        Auto-generated from RARE rule bv-and-flatten

      • BV_MUL_FLATTEN

        public static final ProofRewriteRule BV_MUL_FLATTEN
        Auto-generated from RARE rule bv-mul-flatten

      • BV_CONCAT_MERGE_CONST

        public static final ProofRewriteRule BV_CONCAT_MERGE_CONST
        Auto-generated from RARE rule bv-concat-merge-

      • BV_COMMUTATIVE_ADD

        public static final ProofRewriteRule BV_COMMUTATIVE_ADD
        Auto-generated from RARE rule bv-commutative-add

      • BV_NEG_SUB

        public static final ProofRewriteRule BV_NEG_SUB
        Auto-generated from RARE rule bv-neg-sub

      • BV_NEG_IDEMP

        public static final ProofRewriteRule BV_NEG_IDEMP
        Auto-generated from RARE rule bv-neg-idemp

      • BV_SUB_ELIMINATE

        public static final ProofRewriteRule BV_SUB_ELIMINATE
        Auto-generated from RARE rule bv-sub-eliminate

      • BV_UGT_ELIMINATE

        public static final ProofRewriteRule BV_UGT_ELIMINATE
        Auto-generated from RARE rule bv-ugt-eliminate

      • BV_UGE_ELIMINATE

        public static final ProofRewriteRule BV_UGE_ELIMINATE
        Auto-generated from RARE rule bv-uge-eliminate

      • BV_SGT_ELIMINATE

        public static final ProofRewriteRule BV_SGT_ELIMINATE
        Auto-generated from RARE rule bv-sgt-eliminate

      • BV_SGE_ELIMINATE

        public static final ProofRewriteRule BV_SGE_ELIMINATE
        Auto-generated from RARE rule bv-sge-eliminate

      • BV_SLT_ELIMINATE

        public static final ProofRewriteRule BV_SLT_ELIMINATE
        Auto-generated from RARE rule bv-slt-eliminate

      • BV_SLE_ELIMINATE

        public static final ProofRewriteRule BV_SLE_ELIMINATE
        Auto-generated from RARE rule bv-sle-eliminate

      • BV_REDOR_ELIMINATE

        public static final ProofRewriteRule BV_REDOR_ELIMINATE
        Auto-generated from RARE rule bv-redor-eliminate

      • BV_REDAND_ELIMINATE

        public static final ProofRewriteRule BV_REDAND_ELIMINATE
        Auto-generated from RARE rule bv-redand-eliminate

      • BV_ULE_ELIMINATE

        public static final ProofRewriteRule BV_ULE_ELIMINATE
        Auto-generated from RARE rule bv-ule-eliminate

      • BV_COMP_ELIMINATE

        public static final ProofRewriteRule BV_COMP_ELIMINATE
        Auto-generated from RARE rule bv-comp-eliminate

      • BV_ROTATE_LEFT_ELIMINATE_1

        public static final ProofRewriteRule BV_ROTATE_LEFT_ELIMINATE_1
        Auto-generated from RARE rule bv-rotate-left-eliminate-1

      • BV_ROTATE_LEFT_ELIMINATE_2

        public static final ProofRewriteRule BV_ROTATE_LEFT_ELIMINATE_2
        Auto-generated from RARE rule bv-rotate-left-eliminate-2

      • BV_ROTATE_RIGHT_ELIMINATE_1

        public static final ProofRewriteRule BV_ROTATE_RIGHT_ELIMINATE_1
        Auto-generated from RARE rule bv-rotate-right-eliminate-1

      • BV_ROTATE_RIGHT_ELIMINATE_2

        public static final ProofRewriteRule BV_ROTATE_RIGHT_ELIMINATE_2
        Auto-generated from RARE rule bv-rotate-right-eliminate-2

      • BV_NAND_ELIMINATE

        public static final ProofRewriteRule BV_NAND_ELIMINATE
        Auto-generated from RARE rule bv-nand-eliminate

      • BV_NOR_ELIMINATE

        public static final ProofRewriteRule BV_NOR_ELIMINATE
        Auto-generated from RARE rule bv-nor-eliminate

      • BV_XNOR_ELIMINATE

        public static final ProofRewriteRule BV_XNOR_ELIMINATE
        Auto-generated from RARE rule bv-xnor-eliminate

      • BV_SDIV_ELIMINATE

        public static final ProofRewriteRule BV_SDIV_ELIMINATE
        Auto-generated from RARE rule bv-sdiv-eliminate

      • BV_SDIV_ELIMINATE_FEWER_BITWISE_OPS

        public static final ProofRewriteRule BV_SDIV_ELIMINATE_FEWER_BITWISE_OPS
        Auto-generated from RARE rule bv-sdiv-eliminate-fewer-bitwise-ops

      • BV_ZERO_EXTEND_ELIMINATE

        public static final ProofRewriteRule BV_ZERO_EXTEND_ELIMINATE
        Auto-generated from RARE rule bv-zero-extend-eliminate

      • BV_SIGN_EXTEND_ELIMINATE

        public static final ProofRewriteRule BV_SIGN_EXTEND_ELIMINATE
        Auto-generated from RARE rule bv-sign-extend-eliminate

      • BV_UADDO_ELIMINATE

        public static final ProofRewriteRule BV_UADDO_ELIMINATE
        Auto-generated from RARE rule bv-uaddo-eliminate

      • BV_SADDO_ELIMINATE

        public static final ProofRewriteRule BV_SADDO_ELIMINATE
        Auto-generated from RARE rule bv-saddo-eliminate

      • BV_SDIVO_ELIMINATE

        public static final ProofRewriteRule BV_SDIVO_ELIMINATE
        Auto-generated from RARE rule bv-sdivo-eliminate

      • BV_SMOD_ELIMINATE

        public static final ProofRewriteRule BV_SMOD_ELIMINATE
        Auto-generated from RARE rule bv-smod-eliminate

      • BV_SMOD_ELIMINATE_FEWER_BITWISE_OPS

        public static final ProofRewriteRule BV_SMOD_ELIMINATE_FEWER_BITWISE_OPS
        Auto-generated from RARE rule bv-smod-eliminate-fewer-bitwise-ops

      • BV_SREM_ELIMINATE

        public static final ProofRewriteRule BV_SREM_ELIMINATE
        Auto-generated from RARE rule bv-srem-eliminate

      • BV_SREM_ELIMINATE_FEWER_BITWISE_OPS

        public static final ProofRewriteRule BV_SREM_ELIMINATE_FEWER_BITWISE_OPS
        Auto-generated from RARE rule bv-srem-eliminate-fewer-bitwise-ops

      • BV_USUBO_ELIMINATE

        public static final ProofRewriteRule BV_USUBO_ELIMINATE
        Auto-generated from RARE rule bv-usubo-eliminate

      • BV_SSUBO_ELIMINATE

        public static final ProofRewriteRule BV_SSUBO_ELIMINATE
        Auto-generated from RARE rule bv-ssubo-eliminate

      • BV_ITE_EQUAL_CHILDREN

        public static final ProofRewriteRule BV_ITE_EQUAL_CHILDREN
        Auto-generated from RARE rule bv-ite-equal-children

      • BV_ITE_CONST_CHILDREN_1

        public static final ProofRewriteRule BV_ITE_CONST_CHILDREN_1
        Auto-generated from RARE rule bv-ite--children-1

      • BV_ITE_CONST_CHILDREN_2

        public static final ProofRewriteRule BV_ITE_CONST_CHILDREN_2
        Auto-generated from RARE rule bv-ite--children-2

      • BV_ITE_EQUAL_COND_1

        public static final ProofRewriteRule BV_ITE_EQUAL_COND_1
        Auto-generated from RARE rule bv-ite-equal-cond-1

      • BV_ITE_EQUAL_COND_2

        public static final ProofRewriteRule BV_ITE_EQUAL_COND_2
        Auto-generated from RARE rule bv-ite-equal-cond-2

      • BV_ITE_EQUAL_COND_3

        public static final ProofRewriteRule BV_ITE_EQUAL_COND_3
        Auto-generated from RARE rule bv-ite-equal-cond-3

      • BV_ITE_MERGE_THEN_IF

        public static final ProofRewriteRule BV_ITE_MERGE_THEN_IF
        Auto-generated from RARE rule bv-ite-merge-then-if

      • BV_ITE_MERGE_ELSE_IF

        public static final ProofRewriteRule BV_ITE_MERGE_ELSE_IF
        Auto-generated from RARE rule bv-ite-merge-else-if

      • BV_ITE_MERGE_THEN_ELSE

        public static final ProofRewriteRule BV_ITE_MERGE_THEN_ELSE
        Auto-generated from RARE rule bv-ite-merge-then-else

      • BV_ITE_MERGE_ELSE_ELSE

        public static final ProofRewriteRule BV_ITE_MERGE_ELSE_ELSE
        Auto-generated from RARE rule bv-ite-merge-else-else

      • BV_SHL_BY_CONST_0

        public static final ProofRewriteRule BV_SHL_BY_CONST_0
        Auto-generated from RARE rule bv-shl-by--0

      • BV_SHL_BY_CONST_1

        public static final ProofRewriteRule BV_SHL_BY_CONST_1
        Auto-generated from RARE rule bv-shl-by--1

      • BV_SHL_BY_CONST_2

        public static final ProofRewriteRule BV_SHL_BY_CONST_2
        Auto-generated from RARE rule bv-shl-by--2

      • BV_LSHR_BY_CONST_0

        public static final ProofRewriteRule BV_LSHR_BY_CONST_0
        Auto-generated from RARE rule bv-lshr-by--0

      • BV_LSHR_BY_CONST_1

        public static final ProofRewriteRule BV_LSHR_BY_CONST_1
        Auto-generated from RARE rule bv-lshr-by--1

      • BV_LSHR_BY_CONST_2

        public static final ProofRewriteRule BV_LSHR_BY_CONST_2
        Auto-generated from RARE rule bv-lshr-by--2

      • BV_ASHR_BY_CONST_0

        public static final ProofRewriteRule BV_ASHR_BY_CONST_0
        Auto-generated from RARE rule bv-ashr-by--0

      • BV_ASHR_BY_CONST_1

        public static final ProofRewriteRule BV_ASHR_BY_CONST_1
        Auto-generated from RARE rule bv-ashr-by--1

      • BV_ASHR_BY_CONST_2

        public static final ProofRewriteRule BV_ASHR_BY_CONST_2
        Auto-generated from RARE rule bv-ashr-by--2

      • BV_AND_CONCAT_PULLUP

        public static final ProofRewriteRule BV_AND_CONCAT_PULLUP
        Auto-generated from RARE rule bv-and-concat-pullup

      • BV_OR_CONCAT_PULLUP

        public static final ProofRewriteRule BV_OR_CONCAT_PULLUP
        Auto-generated from RARE rule bv-or-concat-pullup

      • BV_XOR_CONCAT_PULLUP

        public static final ProofRewriteRule BV_XOR_CONCAT_PULLUP
        Auto-generated from RARE rule bv-xor-concat-pullup

      • BV_BITWISE_IDEMP_1

        public static final ProofRewriteRule BV_BITWISE_IDEMP_1
        Auto-generated from RARE rule bv-bitwise-idemp-1

      • BV_BITWISE_IDEMP_2

        public static final ProofRewriteRule BV_BITWISE_IDEMP_2
        Auto-generated from RARE rule bv-bitwise-idemp-2

      • BV_AND_ZERO

        public static final ProofRewriteRule BV_AND_ZERO
        Auto-generated from RARE rule bv-and-zero

      • BV_AND_ONE

        public static final ProofRewriteRule BV_AND_ONE
        Auto-generated from RARE rule bv-and-one

      • BV_OR_ONE

        public static final ProofRewriteRule BV_OR_ONE
        Auto-generated from RARE rule bv-or-one

      • BV_XOR_DUPLICATE

        public static final ProofRewriteRule BV_XOR_DUPLICATE
        Auto-generated from RARE rule bv-xor-duplicate

      • BV_XOR_ONES

        public static final ProofRewriteRule BV_XOR_ONES
        Auto-generated from RARE rule bv-xor-ones

      • BV_XOR_ZERO

        public static final ProofRewriteRule BV_XOR_ZERO
        Auto-generated from RARE rule bv-xor-zero

      • BV_BITWISE_NOT_AND

        public static final ProofRewriteRule BV_BITWISE_NOT_AND
        Auto-generated from RARE rule bv-bitwise-not-and

      • BV_BITWISE_NOT_OR

        public static final ProofRewriteRule BV_BITWISE_NOT_OR
        Auto-generated from RARE rule bv-bitwise-not-or

      • BV_XOR_NOT

        public static final ProofRewriteRule BV_XOR_NOT
        Auto-generated from RARE rule bv-xor-not

      • BV_NOT_IDEMP

        public static final ProofRewriteRule BV_NOT_IDEMP
        Auto-generated from RARE rule bv-not-idemp

      • BV_ULT_ZERO_1

        public static final ProofRewriteRule BV_ULT_ZERO_1
        Auto-generated from RARE rule bv-ult-zero-1

      • BV_ULT_ZERO_2

        public static final ProofRewriteRule BV_ULT_ZERO_2
        Auto-generated from RARE rule bv-ult-zero-2

      • BV_ULT_SELF

        public static final ProofRewriteRule BV_ULT_SELF
        Auto-generated from RARE rule bv-ult-self

      • BV_LT_SELF

        public static final ProofRewriteRule BV_LT_SELF
        Auto-generated from RARE rule bv-lt-self

      • BV_ULE_SELF

        public static final ProofRewriteRule BV_ULE_SELF
        Auto-generated from RARE rule bv-ule-self

      • BV_ULE_ZERO

        public static final ProofRewriteRule BV_ULE_ZERO
        Auto-generated from RARE rule bv-ule-zero

      • BV_ZERO_ULE

        public static final ProofRewriteRule BV_ZERO_ULE
        Auto-generated from RARE rule bv-zero-ule

      • BV_SLE_SELF

        public static final ProofRewriteRule BV_SLE_SELF
        Auto-generated from RARE rule bv-sle-self

      • BV_ULE_MAX

        public static final ProofRewriteRule BV_ULE_MAX
        Auto-generated from RARE rule bv-ule-max

      • BV_NOT_ULT

        public static final ProofRewriteRule BV_NOT_ULT
        Auto-generated from RARE rule bv-not-ult

      • BV_NOT_ULE

        public static final ProofRewriteRule BV_NOT_ULE
        Auto-generated from RARE rule bv-not-ule

      • BV_NOT_SLE

        public static final ProofRewriteRule BV_NOT_SLE
        Auto-generated from RARE rule bv-not-sle

      • BV_MULT_POW2_1

        public static final ProofRewriteRule BV_MULT_POW2_1
        Auto-generated from RARE rule bv-mult-pow2-1

      • BV_MULT_POW2_2

        public static final ProofRewriteRule BV_MULT_POW2_2
        Auto-generated from RARE rule bv-mult-pow2-2

      • BV_MULT_POW2_2B

        public static final ProofRewriteRule BV_MULT_POW2_2B
        Auto-generated from RARE rule bv-mult-pow2-2b

      • BV_EXTRACT_MULT_LEADING_BIT

        public static final ProofRewriteRule BV_EXTRACT_MULT_LEADING_BIT
        Auto-generated from RARE rule bv-extract-mult-leading-bit

      • BV_UDIV_POW2_NOT_ONE

        public static final ProofRewriteRule BV_UDIV_POW2_NOT_ONE
        Auto-generated from RARE rule bv-udiv-pow2-not-one

      • BV_UDIV_ZERO

        public static final ProofRewriteRule BV_UDIV_ZERO
        Auto-generated from RARE rule bv-udiv-zero

      • BV_UDIV_ONE

        public static final ProofRewriteRule BV_UDIV_ONE
        Auto-generated from RARE rule bv-udiv-one

      • BV_UREM_POW2_NOT_ONE

        public static final ProofRewriteRule BV_UREM_POW2_NOT_ONE
        Auto-generated from RARE rule bv-urem-pow2-not-one

      • BV_UREM_ONE

        public static final ProofRewriteRule BV_UREM_ONE
        Auto-generated from RARE rule bv-urem-one

      • BV_UREM_SELF

        public static final ProofRewriteRule BV_UREM_SELF
        Auto-generated from RARE rule bv-urem-self

      • BV_SHL_ZERO

        public static final ProofRewriteRule BV_SHL_ZERO
        Auto-generated from RARE rule bv-shl-zero

      • BV_LSHR_ZERO

        public static final ProofRewriteRule BV_LSHR_ZERO
        Auto-generated from RARE rule bv-lshr-zero

      • BV_ASHR_ZERO

        public static final ProofRewriteRule BV_ASHR_ZERO
        Auto-generated from RARE rule bv-ashr-zero

      • BV_UGT_UREM

        public static final ProofRewriteRule BV_UGT_UREM
        Auto-generated from RARE rule bv-ugt-urem

      • BV_ULT_ONE

        public static final ProofRewriteRule BV_ULT_ONE
        Auto-generated from RARE rule bv-ult-one

      • BV_SLT_ZERO

        public static final ProofRewriteRule BV_SLT_ZERO
        Auto-generated from RARE rule bv-slt-zero

      • BV_MERGE_SIGN_EXTEND_1

        public static final ProofRewriteRule BV_MERGE_SIGN_EXTEND_1
        Auto-generated from RARE rule bv-merge-sign-extend-1

      • BV_MERGE_SIGN_EXTEND_2

        public static final ProofRewriteRule BV_MERGE_SIGN_EXTEND_2
        Auto-generated from RARE rule bv-merge-sign-extend-2

      • BV_MERGE_SIGN_EXTEND_3

        public static final ProofRewriteRule BV_MERGE_SIGN_EXTEND_3
        Auto-generated from RARE rule bv-merge-sign-extend-3

      • BV_SIGN_EXTEND_EQ_CONST_1

        public static final ProofRewriteRule BV_SIGN_EXTEND_EQ_CONST_1
        Auto-generated from RARE rule bv-sign-extend-eq--1

      • BV_SIGN_EXTEND_EQ_CONST_2

        public static final ProofRewriteRule BV_SIGN_EXTEND_EQ_CONST_2
        Auto-generated from RARE rule bv-sign-extend-eq--2

      • BV_ZERO_EXTEND_EQ_CONST_1

        public static final ProofRewriteRule BV_ZERO_EXTEND_EQ_CONST_1
        Auto-generated from RARE rule bv-zero-extend-eq--1

      • BV_ZERO_EXTEND_EQ_CONST_2

        public static final ProofRewriteRule BV_ZERO_EXTEND_EQ_CONST_2
        Auto-generated from RARE rule bv-zero-extend-eq--2

      • BV_SIGN_EXTEND_ULT_CONST_1

        public static final ProofRewriteRule BV_SIGN_EXTEND_ULT_CONST_1
        Auto-generated from RARE rule bv-sign-extend-ult--1

      • BV_SIGN_EXTEND_ULT_CONST_2

        public static final ProofRewriteRule BV_SIGN_EXTEND_ULT_CONST_2
        Auto-generated from RARE rule bv-sign-extend-ult--2

      • BV_SIGN_EXTEND_ULT_CONST_3

        public static final ProofRewriteRule BV_SIGN_EXTEND_ULT_CONST_3
        Auto-generated from RARE rule bv-sign-extend-ult--3

      • BV_SIGN_EXTEND_ULT_CONST_4

        public static final ProofRewriteRule BV_SIGN_EXTEND_ULT_CONST_4
        Auto-generated from RARE rule bv-sign-extend-ult--4

      • SETS_EQ_SINGLETON_EMP

        public static final ProofRewriteRule SETS_EQ_SINGLETON_EMP
        Auto-generated from RARE rule sets-eq-singleton-emp

      • SETS_MEMBER_SINGLETON

        public static final ProofRewriteRule SETS_MEMBER_SINGLETON
        Auto-generated from RARE rule sets-member-singleton

      • SETS_MEMBER_EMP

        public static final ProofRewriteRule SETS_MEMBER_EMP
        Auto-generated from RARE rule sets-member-emp

      • SETS_SUBSET_ELIM

        public static final ProofRewriteRule SETS_SUBSET_ELIM
        Auto-generated from RARE rule sets-subset-elim

      • SETS_UNION_COMM

        public static final ProofRewriteRule SETS_UNION_COMM
        Auto-generated from RARE rule sets-union-comm

      • SETS_INTER_COMM

        public static final ProofRewriteRule SETS_INTER_COMM
        Auto-generated from RARE rule sets-inter-comm

      • SETS_INTER_EMP1

        public static final ProofRewriteRule SETS_INTER_EMP1
        Auto-generated from RARE rule sets-inter-emp1

      • SETS_INTER_EMP2

        public static final ProofRewriteRule SETS_INTER_EMP2
        Auto-generated from RARE rule sets-inter-emp2

      • SETS_MINUS_EMP1

        public static final ProofRewriteRule SETS_MINUS_EMP1
        Auto-generated from RARE rule sets-minus-emp1

      • SETS_MINUS_EMP2

        public static final ProofRewriteRule SETS_MINUS_EMP2
        Auto-generated from RARE rule sets-minus-emp2

      • SETS_UNION_EMP1

        public static final ProofRewriteRule SETS_UNION_EMP1
        Auto-generated from RARE rule sets-union-emp1

      • SETS_UNION_EMP2

        public static final ProofRewriteRule SETS_UNION_EMP2
        Auto-generated from RARE rule sets-union-emp2

      • SETS_INTER_MEMBER

        public static final ProofRewriteRule SETS_INTER_MEMBER
        Auto-generated from RARE rule sets-inter-member

      • SETS_MINUS_MEMBER

        public static final ProofRewriteRule SETS_MINUS_MEMBER
        Auto-generated from RARE rule sets-minus-member

      • SETS_UNION_MEMBER

        public static final ProofRewriteRule SETS_UNION_MEMBER
        Auto-generated from RARE rule sets-union-member

      • SETS_CHOOSE_SINGLETON

        public static final ProofRewriteRule SETS_CHOOSE_SINGLETON
        Auto-generated from RARE rule sets-choose-singleton

      • SETS_CARD_SINGLETON

        public static final ProofRewriteRule SETS_CARD_SINGLETON
        Auto-generated from RARE rule sets-card-singleton

      • SETS_CARD_UNION

        public static final ProofRewriteRule SETS_CARD_UNION
        Auto-generated from RARE rule sets-card-union

      • SETS_CARD_MINUS

        public static final ProofRewriteRule SETS_CARD_MINUS
        Auto-generated from RARE rule sets-card-minus

      • SETS_CARD_EMP

        public static final ProofRewriteRule SETS_CARD_EMP
        Auto-generated from RARE rule sets-card-emp

      • SETS_MINUS_SELF

        public static final ProofRewriteRule SETS_MINUS_SELF
        Auto-generated from RARE rule sets-minus-self

      • SETS_IS_EMPTY_ELIM

        public static final ProofRewriteRule SETS_IS_EMPTY_ELIM
        Auto-generated from RARE rule sets-is-empty-elim

      • STR_EQ_CTN_FALSE

        public static final ProofRewriteRule STR_EQ_CTN_FALSE
        Auto-generated from RARE rule str-eq-ctn-false

      • STR_EQ_CTN_FULL_FALSE1

        public static final ProofRewriteRule STR_EQ_CTN_FULL_FALSE1
        Auto-generated from RARE rule str-eq-ctn-full-false1

      • STR_EQ_CTN_FULL_FALSE2

        public static final ProofRewriteRule STR_EQ_CTN_FULL_FALSE2
        Auto-generated from RARE rule str-eq-ctn-full-false2

      • STR_CONCAT_FLATTEN

        public static final ProofRewriteRule STR_CONCAT_FLATTEN
        Auto-generated from RARE rule str-concat-flatten

      • STR_CONCAT_FLATTEN_EQ

        public static final ProofRewriteRule STR_CONCAT_FLATTEN_EQ
        Auto-generated from RARE rule str-concat-flatten-eq

      • STR_CONCAT_FLATTEN_EQ_REV

        public static final ProofRewriteRule STR_CONCAT_FLATTEN_EQ_REV
        Auto-generated from RARE rule str-concat-flatten-eq-rev

      • STR_SUBSTR_EMPTY_STR

        public static final ProofRewriteRule STR_SUBSTR_EMPTY_STR
        Auto-generated from RARE rule str-substr-empty-str

      • STR_SUBSTR_EMPTY_RANGE

        public static final ProofRewriteRule STR_SUBSTR_EMPTY_RANGE
        Auto-generated from RARE rule str-substr-empty-range

      • STR_SUBSTR_EMPTY_START

        public static final ProofRewriteRule STR_SUBSTR_EMPTY_START
        Auto-generated from RARE rule str-substr-empty-start

      • STR_SUBSTR_EMPTY_START_NEG

        public static final ProofRewriteRule STR_SUBSTR_EMPTY_START_NEG
        Auto-generated from RARE rule str-substr-empty-start-neg

      • STR_SUBSTR_EQ_EMPTY

        public static final ProofRewriteRule STR_SUBSTR_EQ_EMPTY
        Auto-generated from RARE rule str-substr-eq-empty

      • STR_LEN_REPLACE_INV

        public static final ProofRewriteRule STR_LEN_REPLACE_INV
        Auto-generated from RARE rule str-len-replace-inv

      • STR_LEN_UPDATE_INV

        public static final ProofRewriteRule STR_LEN_UPDATE_INV
        Auto-generated from RARE rule str-len-update-inv

      • STR_LEN_SUBSTR_IN_RANGE

        public static final ProofRewriteRule STR_LEN_SUBSTR_IN_RANGE
        Auto-generated from RARE rule str-len-substr-in-range

      • STR_LEN_SUBSTR_UB1

        public static final ProofRewriteRule STR_LEN_SUBSTR_UB1
        Auto-generated from RARE rule str-len-substr-ub1

      • STR_LEN_SUBSTR_UB2

        public static final ProofRewriteRule STR_LEN_SUBSTR_UB2
        Auto-generated from RARE rule str-len-substr-ub2

      • STR_CONCAT_CLASH

        public static final ProofRewriteRule STR_CONCAT_CLASH
        Auto-generated from RARE rule str-concat-clash

      • STR_CONCAT_CLASH_REV

        public static final ProofRewriteRule STR_CONCAT_CLASH_REV
        Auto-generated from RARE rule str-concat-clash-rev

      • STR_CONCAT_CLASH2

        public static final ProofRewriteRule STR_CONCAT_CLASH2
        Auto-generated from RARE rule str-concat-clash2

      • STR_CONCAT_CLASH2_REV

        public static final ProofRewriteRule STR_CONCAT_CLASH2_REV
        Auto-generated from RARE rule str-concat-clash2-rev

      • STR_CONCAT_UNIFY

        public static final ProofRewriteRule STR_CONCAT_UNIFY
        Auto-generated from RARE rule str-concat-unify

      • STR_CONCAT_UNIFY_REV

        public static final ProofRewriteRule STR_CONCAT_UNIFY_REV
        Auto-generated from RARE rule str-concat-unify-rev

      • STR_CONCAT_UNIFY_BASE

        public static final ProofRewriteRule STR_CONCAT_UNIFY_BASE
        Auto-generated from RARE rule str-concat-unify-base

      • STR_CONCAT_UNIFY_BASE_REV

        public static final ProofRewriteRule STR_CONCAT_UNIFY_BASE_REV
        Auto-generated from RARE rule str-concat-unify-base-rev

      • STR_CONCAT_CLASH_CHAR

        public static final ProofRewriteRule STR_CONCAT_CLASH_CHAR
        Auto-generated from RARE rule str-concat-clash-char

      • STR_CONCAT_CLASH_CHAR_REV

        public static final ProofRewriteRule STR_CONCAT_CLASH_CHAR_REV
        Auto-generated from RARE rule str-concat-clash-char-rev

      • STR_PREFIXOF_ELIM

        public static final ProofRewriteRule STR_PREFIXOF_ELIM
        Auto-generated from RARE rule str-prefixof-elim

      • STR_SUFFIXOF_ELIM

        public static final ProofRewriteRule STR_SUFFIXOF_ELIM
        Auto-generated from RARE rule str-suffixof-elim

      • STR_PREFIXOF_ONE

        public static final ProofRewriteRule STR_PREFIXOF_ONE
        Auto-generated from RARE rule str-prefixof-one

      • STR_SUFFIXOF_ONE

        public static final ProofRewriteRule STR_SUFFIXOF_ONE
        Auto-generated from RARE rule str-suffixof-one

      • STR_SUBSTR_COMBINE1

        public static final ProofRewriteRule STR_SUBSTR_COMBINE1
        Auto-generated from RARE rule str-substr-combine1

      • STR_SUBSTR_COMBINE2

        public static final ProofRewriteRule STR_SUBSTR_COMBINE2
        Auto-generated from RARE rule str-substr-combine2

      • STR_SUBSTR_COMBINE3

        public static final ProofRewriteRule STR_SUBSTR_COMBINE3
        Auto-generated from RARE rule str-substr-combine3

      • STR_SUBSTR_COMBINE4

        public static final ProofRewriteRule STR_SUBSTR_COMBINE4
        Auto-generated from RARE rule str-substr-combine4

      • STR_SUBSTR_CONCAT1

        public static final ProofRewriteRule STR_SUBSTR_CONCAT1
        Auto-generated from RARE rule str-substr-concat1

      • STR_SUBSTR_CONCAT2

        public static final ProofRewriteRule STR_SUBSTR_CONCAT2
        Auto-generated from RARE rule str-substr-concat2

      • STR_SUBSTR_FULL

        public static final ProofRewriteRule STR_SUBSTR_FULL
        Auto-generated from RARE rule str-substr-full

      • STR_SUBSTR_FULL_EQ

        public static final ProofRewriteRule STR_SUBSTR_FULL_EQ
        Auto-generated from RARE rule str-substr-full-eq

      • STR_CONTAINS_REFL

        public static final ProofRewriteRule STR_CONTAINS_REFL
        Auto-generated from RARE rule str-contains-refl

      • STR_CONTAINS_CONCAT_FIND

        public static final ProofRewriteRule STR_CONTAINS_CONCAT_FIND
        Auto-generated from RARE rule str-contains-concat-find

      • STR_CONTAINS_SPLIT_CHAR

        public static final ProofRewriteRule STR_CONTAINS_SPLIT_CHAR
        Auto-generated from RARE rule str-contains-split-char

      • STR_CONTAINS_LT_LEN

        public static final ProofRewriteRule STR_CONTAINS_LT_LEN
        Auto-generated from RARE rule str-contains-lt-len

      • STR_CONTAINS_LEQ_LEN_EQ

        public static final ProofRewriteRule STR_CONTAINS_LEQ_LEN_EQ
        Auto-generated from RARE rule str-contains-leq-len-eq

      • STR_CONTAINS_EMP

        public static final ProofRewriteRule STR_CONTAINS_EMP
        Auto-generated from RARE rule str-contains-emp

      • STR_CONTAINS_IS_EMP

        public static final ProofRewriteRule STR_CONTAINS_IS_EMP
        Auto-generated from RARE rule str-contains-is-emp

      • STR_AT_ELIM

        public static final ProofRewriteRule STR_AT_ELIM
        Auto-generated from RARE rule str-at-elim

      • STR_REPLACE_SELF

        public static final ProofRewriteRule STR_REPLACE_SELF
        Auto-generated from RARE rule str-replace-self

      • STR_REPLACE_PREFIX

        public static final ProofRewriteRule STR_REPLACE_PREFIX
        Auto-generated from RARE rule str-replace-prefix

      • STR_REPLACE_NO_CONTAINS

        public static final ProofRewriteRule STR_REPLACE_NO_CONTAINS
        Auto-generated from RARE rule str-replace-no-contains

      • STR_REPLACE_EMPTY

        public static final ProofRewriteRule STR_REPLACE_EMPTY
        Auto-generated from RARE rule str-replace-empty

      • STR_REPLACE_CONTAINS_PRE

        public static final ProofRewriteRule STR_REPLACE_CONTAINS_PRE
        Auto-generated from RARE rule str-replace-contains-pre

      • STR_REPLACE_ALL_NO_CONTAINS

        public static final ProofRewriteRule STR_REPLACE_ALL_NO_CONTAINS
        Auto-generated from RARE rule str-replace-all-no-contains

      • STR_REPLACE_RE_NONE

        public static final ProofRewriteRule STR_REPLACE_RE_NONE
        Auto-generated from RARE rule str-replace-re-none

      • STR_REPLACE_RE_ALL_NONE

        public static final ProofRewriteRule STR_REPLACE_RE_ALL_NONE
        Auto-generated from RARE rule str-replace-re-all-none

      • STR_LEN_CONCAT_REC

        public static final ProofRewriteRule STR_LEN_CONCAT_REC
        Auto-generated from RARE rule str-len-concat-rec

      • STR_INDEXOF_SELF

        public static final ProofRewriteRule STR_INDEXOF_SELF
        Auto-generated from RARE rule str-indexof-self

      • STR_INDEXOF_NO_CONTAINS

        public static final ProofRewriteRule STR_INDEXOF_NO_CONTAINS
        Auto-generated from RARE rule str-indexof-no-contains

      • STR_INDEXOF_CONTAINS_PRE

        public static final ProofRewriteRule STR_INDEXOF_CONTAINS_PRE
        Auto-generated from RARE rule str-indexof-contains-pre

      • STR_INDEXOF_RE_NONE

        public static final ProofRewriteRule STR_INDEXOF_RE_NONE
        Auto-generated from RARE rule str-indexof-re-none

      • STR_TO_LOWER_CONCAT

        public static final ProofRewriteRule STR_TO_LOWER_CONCAT
        Auto-generated from RARE rule str-to-lower-concat

      • STR_TO_UPPER_CONCAT

        public static final ProofRewriteRule STR_TO_UPPER_CONCAT
        Auto-generated from RARE rule str-to-upper-concat

      • STR_TO_LOWER_UPPER

        public static final ProofRewriteRule STR_TO_LOWER_UPPER
        Auto-generated from RARE rule str-to-lower-upper

      • STR_TO_UPPER_LOWER

        public static final ProofRewriteRule STR_TO_UPPER_LOWER
        Auto-generated from RARE rule str-to-upper-lower

      • STR_TO_LOWER_LEN

        public static final ProofRewriteRule STR_TO_LOWER_LEN
        Auto-generated from RARE rule str-to-lower-len

      • STR_TO_UPPER_LEN

        public static final ProofRewriteRule STR_TO_UPPER_LEN
        Auto-generated from RARE rule str-to-upper-len

      • STR_TO_LOWER_FROM_INT

        public static final ProofRewriteRule STR_TO_LOWER_FROM_INT
        Auto-generated from RARE rule str-to-lower-from-int

      • STR_TO_UPPER_FROM_INT

        public static final ProofRewriteRule STR_TO_UPPER_FROM_INT
        Auto-generated from RARE rule str-to-upper-from-int

      • STR_TO_INT_CONCAT_NEG_ONE

        public static final ProofRewriteRule STR_TO_INT_CONCAT_NEG_ONE
        Auto-generated from RARE rule str-to-int-concat-neg-one

      • STR_LEQ_EMPTY

        public static final ProofRewriteRule STR_LEQ_EMPTY
        Auto-generated from RARE rule str-leq-empty

      • STR_LEQ_EMPTY_EQ

        public static final ProofRewriteRule STR_LEQ_EMPTY_EQ
        Auto-generated from RARE rule str-leq-empty-eq

      • STR_LEQ_CONCAT_FALSE

        public static final ProofRewriteRule STR_LEQ_CONCAT_FALSE
        Auto-generated from RARE rule str-leq-concat-false

      • STR_LEQ_CONCAT_TRUE

        public static final ProofRewriteRule STR_LEQ_CONCAT_TRUE
        Auto-generated from RARE rule str-leq-concat-true

      • STR_LT_ELIM

        public static final ProofRewriteRule STR_LT_ELIM
        Auto-generated from RARE rule str-lt-elim

      • RE_ALL_ELIM

        public static final ProofRewriteRule RE_ALL_ELIM
        Auto-generated from RARE rule re-all-elim

      • RE_OPT_ELIM

        public static final ProofRewriteRule RE_OPT_ELIM
        Auto-generated from RARE rule re-opt-elim

      • RE_DIFF_ELIM

        public static final ProofRewriteRule RE_DIFF_ELIM
        Auto-generated from RARE rule re-diff-elim

      • RE_CONCAT_EMP

        public static final ProofRewriteRule RE_CONCAT_EMP
        Auto-generated from RARE rule re-concat-emp

      • RE_CONCAT_NONE

        public static final ProofRewriteRule RE_CONCAT_NONE
        Auto-generated from RARE rule re-concat-none

      • RE_CONCAT_FLATTEN

        public static final ProofRewriteRule RE_CONCAT_FLATTEN
        Auto-generated from RARE rule re-concat-flatten

      • RE_CONCAT_STAR_SWAP

        public static final ProofRewriteRule RE_CONCAT_STAR_SWAP
        Auto-generated from RARE rule re-concat-star-swap

      • RE_CONCAT_STAR_REPEAT

        public static final ProofRewriteRule RE_CONCAT_STAR_REPEAT
        Auto-generated from RARE rule re-concat-star-repeat

      • RE_CONCAT_MERGE

        public static final ProofRewriteRule RE_CONCAT_MERGE
        Auto-generated from RARE rule re-concat-merge

      • RE_UNION_ALL

        public static final ProofRewriteRule RE_UNION_ALL
        Auto-generated from RARE rule re-union-all

      • RE_UNION_NONE

        public static final ProofRewriteRule RE_UNION_NONE
        Auto-generated from RARE rule re-union-none

      • RE_UNION_FLATTEN

        public static final ProofRewriteRule RE_UNION_FLATTEN
        Auto-generated from RARE rule re-union-flatten

      • RE_UNION_DUP

        public static final ProofRewriteRule RE_UNION_DUP
        Auto-generated from RARE rule re-union-dup

      • RE_INTER_ALL

        public static final ProofRewriteRule RE_INTER_ALL
        Auto-generated from RARE rule re-inter-all

      • RE_INTER_NONE

        public static final ProofRewriteRule RE_INTER_NONE
        Auto-generated from RARE rule re-inter-none

      • RE_INTER_FLATTEN

        public static final ProofRewriteRule RE_INTER_FLATTEN
        Auto-generated from RARE rule re-inter-flatten

      • RE_INTER_DUP

        public static final ProofRewriteRule RE_INTER_DUP
        Auto-generated from RARE rule re-inter-dup

      • RE_STAR_NONE

        public static final ProofRewriteRule RE_STAR_NONE
        Auto-generated from RARE rule re-star-none

      • RE_LOOP_NEG

        public static final ProofRewriteRule RE_LOOP_NEG
        Auto-generated from RARE rule re-loop-neg

      • RE_INTER_CSTRING

        public static final ProofRewriteRule RE_INTER_CSTRING
        Auto-generated from RARE rule re-inter-cstring

      • RE_INTER_CSTRING_NEG

        public static final ProofRewriteRule RE_INTER_CSTRING_NEG
        Auto-generated from RARE rule re-inter-cstring-neg

      • STR_SUBSTR_LEN_INCLUDE

        public static final ProofRewriteRule STR_SUBSTR_LEN_INCLUDE
        Auto-generated from RARE rule str-substr-len-include

      • STR_SUBSTR_LEN_INCLUDE_PRE

        public static final ProofRewriteRule STR_SUBSTR_LEN_INCLUDE_PRE
        Auto-generated from RARE rule str-substr-len-include-pre

      • STR_SUBSTR_LEN_SKIP

        public static final ProofRewriteRule STR_SUBSTR_LEN_SKIP
        Auto-generated from RARE rule str-substr-len-skip

      • SEQ_LEN_REV

        public static final ProofRewriteRule SEQ_LEN_REV
        Auto-generated from RARE rule seq-len-rev

      • SEQ_REV_REV

        public static final ProofRewriteRule SEQ_REV_REV
        Auto-generated from RARE rule seq-rev-rev

      • SEQ_REV_CONCAT

        public static final ProofRewriteRule SEQ_REV_CONCAT
        Auto-generated from RARE rule seq-rev-concat

      • SEQ_LEN_UNIT

        public static final ProofRewriteRule SEQ_LEN_UNIT
        Auto-generated from RARE rule seq-len-unit

      • SEQ_NTH_UNIT

        public static final ProofRewriteRule SEQ_NTH_UNIT
        Auto-generated from RARE rule seq-nth-unit

      • SEQ_REV_UNIT

        public static final ProofRewriteRule SEQ_REV_UNIT
        Auto-generated from RARE rule seq-rev-unit

      • SEQ_LEN_EMPTY

        public static final ProofRewriteRule SEQ_LEN_EMPTY
        Auto-generated from RARE rule seq-len-empty

      • RE_IN_EMPTY

        public static final ProofRewriteRule RE_IN_EMPTY
        Auto-generated from RARE rule re-in-empty

      • RE_IN_SIGMA

        public static final ProofRewriteRule RE_IN_SIGMA
        Auto-generated from RARE rule re-in-sigma

      • RE_IN_SIGMA_STAR

        public static final ProofRewriteRule RE_IN_SIGMA_STAR
        Auto-generated from RARE rule re-in-sigma-star

      • RE_IN_CSTRING

        public static final ProofRewriteRule RE_IN_CSTRING
        Auto-generated from RARE rule re-in-cstring

      • RE_IN_COMP

        public static final ProofRewriteRule RE_IN_COMP
        Auto-generated from RARE rule re-in-comp

      • STR_IN_RE_UNION_ELIM

        public static final ProofRewriteRule STR_IN_RE_UNION_ELIM
        Auto-generated from RARE rule str-in-re-union-elim

      • STR_IN_RE_INTER_ELIM

        public static final ProofRewriteRule STR_IN_RE_INTER_ELIM
        Auto-generated from RARE rule str-in-re-inter-elim

      • STR_IN_RE_RANGE_ELIM

        public static final ProofRewriteRule STR_IN_RE_RANGE_ELIM
        Auto-generated from RARE rule str-in-re-range-elim

      • STR_IN_RE_CONTAINS

        public static final ProofRewriteRule STR_IN_RE_CONTAINS
        Auto-generated from RARE rule str-in-re-contains

      • STR_IN_RE_STRIP_PREFIX

        public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX
        Auto-generated from RARE rule str-in-re-strip-prefix

      • STR_IN_RE_STRIP_PREFIX_NEG

        public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_NEG
        Auto-generated from RARE rule str-in-re-strip-prefix-neg

      • STR_IN_RE_STRIP_PREFIX_SR_SINGLE

        public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_SR_SINGLE
        Auto-generated from RARE rule str-in-re-strip-prefix-sr-single

      • STR_IN_RE_STRIP_PREFIX_SR_SINGLE_NEG

        public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_SR_SINGLE_NEG
        Auto-generated from RARE rule str-in-re-strip-prefix-sr-single-neg

      • STR_IN_RE_STRIP_PREFIX_SRS_SINGLE

        public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_SRS_SINGLE
        Auto-generated from RARE rule str-in-re-strip-prefix-srs-single

      • STR_IN_RE_STRIP_PREFIX_SRS_SINGLE_NEG

        public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_SRS_SINGLE_NEG
        Auto-generated from RARE rule str-in-re-strip-prefix-srs-single-neg

      • STR_IN_RE_STRIP_PREFIX_S_SINGLE

        public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_S_SINGLE
        Auto-generated from RARE rule str-in-re-strip-prefix-s-single

      • STR_IN_RE_STRIP_PREFIX_S_SINGLE_NEG

        public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_S_SINGLE_NEG
        Auto-generated from RARE rule str-in-re-strip-prefix-s-single-neg

      • STR_IN_RE_STRIP_PREFIX_BASE

        public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_BASE
        Auto-generated from RARE rule str-in-re-strip-prefix-base

      • STR_IN_RE_STRIP_PREFIX_BASE_NEG

        public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_BASE_NEG
        Auto-generated from RARE rule str-in-re-strip-prefix-base-neg

      • STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE

        public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE
        Auto-generated from RARE rule str-in-re-strip-prefix-base-s-single

      • STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE_NEG

        public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE_NEG
        Auto-generated from RARE rule str-in-re-strip-prefix-base-s-single-neg

      • STR_IN_RE_STRIP_CHAR

        public static final ProofRewriteRule STR_IN_RE_STRIP_CHAR
        Auto-generated from RARE rule str-in-re-strip-char

      • STR_IN_RE_STRIP_CHAR_S_SINGLE

        public static final ProofRewriteRule STR_IN_RE_STRIP_CHAR_S_SINGLE
        Auto-generated from RARE rule str-in-re-strip-char-s-single

      • STR_IN_RE_STRIP_PREFIX_REV

        public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_REV
        Auto-generated from RARE rule str-in-re-strip-prefix-rev

      • STR_IN_RE_STRIP_PREFIX_NEG_REV

        public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_NEG_REV
        Auto-generated from RARE rule str-in-re-strip-prefix-neg-rev

      • STR_IN_RE_STRIP_PREFIX_SR_SINGLE_REV

        public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_SR_SINGLE_REV
        Auto-generated from RARE rule str-in-re-strip-prefix-sr-single-rev

      • STR_IN_RE_STRIP_PREFIX_SR_SINGLE_NEG_REV

        public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_SR_SINGLE_NEG_REV
        Auto-generated from RARE rule str-in-re-strip-prefix-sr-single-neg-rev

      • STR_IN_RE_STRIP_PREFIX_SRS_SINGLE_REV

        public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_SRS_SINGLE_REV
        Auto-generated from RARE rule str-in-re-strip-prefix-srs-single-rev

      • STR_IN_RE_STRIP_PREFIX_SRS_SINGLE_NEG_REV

        public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_SRS_SINGLE_NEG_REV
        Auto-generated from RARE rule str-in-re-strip-prefix-srs-single-neg-rev

      • STR_IN_RE_STRIP_PREFIX_S_SINGLE_REV

        public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_S_SINGLE_REV
        Auto-generated from RARE rule str-in-re-strip-prefix-s-single-rev

      • STR_IN_RE_STRIP_PREFIX_S_SINGLE_NEG_REV

        public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_S_SINGLE_NEG_REV
        Auto-generated from RARE rule str-in-re-strip-prefix-s-single-neg-rev

      • STR_IN_RE_STRIP_PREFIX_BASE_REV

        public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_BASE_REV
        Auto-generated from RARE rule str-in-re-strip-prefix-base-rev

      • STR_IN_RE_STRIP_PREFIX_BASE_NEG_REV

        public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_BASE_NEG_REV
        Auto-generated from RARE rule str-in-re-strip-prefix-base-neg-rev

      • STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE_REV

        public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE_REV
        Auto-generated from RARE rule str-in-re-strip-prefix-base-s-single-rev

      • STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE_NEG_REV

        public static final ProofRewriteRule STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE_NEG_REV
        Auto-generated from RARE rule str-in-re-strip-prefix-base-s-single-neg-rev

      • STR_IN_RE_STRIP_CHAR_REV

        public static final ProofRewriteRule STR_IN_RE_STRIP_CHAR_REV
        Auto-generated from RARE rule str-in-re-strip-char-rev

      • STR_IN_RE_STRIP_CHAR_S_SINGLE_REV

        public static final ProofRewriteRule STR_IN_RE_STRIP_CHAR_S_SINGLE_REV
        Auto-generated from RARE rule str-in-re-strip-char-s-single-rev

      • STR_IN_RE_REQ_UNFOLD

        public static final ProofRewriteRule STR_IN_RE_REQ_UNFOLD
        Auto-generated from RARE rule str-in-re-req-unfold

      • STR_IN_RE_REQ_UNFOLD_REV

        public static final ProofRewriteRule STR_IN_RE_REQ_UNFOLD_REV
        Auto-generated from RARE rule str-in-re-req-unfold-rev

      • STR_IN_RE_SKIP_UNFOLD

        public static final ProofRewriteRule STR_IN_RE_SKIP_UNFOLD
        Auto-generated from RARE rule str-in-re-skip-unfold

      • STR_IN_RE_SKIP_UNFOLD_REV

        public static final ProofRewriteRule STR_IN_RE_SKIP_UNFOLD_REV
        Auto-generated from RARE rule str-in-re-skip-unfold-rev

      • STR_IN_RE_TEST_UNFOLD

        public static final ProofRewriteRule STR_IN_RE_TEST_UNFOLD
        Auto-generated from RARE rule str-in-re-test-unfold

      • STR_IN_RE_TEST_UNFOLD_REV

        public static final ProofRewriteRule STR_IN_RE_TEST_UNFOLD_REV
        Auto-generated from RARE rule str-in-re-test-unfold-rev

      • EQ_REFL

        public static final ProofRewriteRule EQ_REFL
        Auto-generated from RARE rule eq-refl

      • EQ_SYMM

        public static final ProofRewriteRule EQ_SYMM
        Auto-generated from RARE rule eq-symm

      • EQ_COND_DEQ

        public static final ProofRewriteRule EQ_COND_DEQ
        Auto-generated from RARE rule eq-cond-deq

      • EQ_ITE_LIFT

        public static final ProofRewriteRule EQ_ITE_LIFT
        Auto-generated from RARE rule eq-ite-lift

      • DISTINCT_BINARY_ELIM

        public static final ProofRewriteRule DISTINCT_BINARY_ELIM
        Auto-generated from RARE rule distinct-binary-elim

      • UF_BV2NAT_INT2BV

        public static final ProofRewriteRule UF_BV2NAT_INT2BV
        Auto-generated from RARE rule uf-bv2nat-int2bv

      • UF_BV2NAT_INT2BV_EXTEND

        public static final ProofRewriteRule UF_BV2NAT_INT2BV_EXTEND
        Auto-generated from RARE rule uf-bv2nat-int2bv-extend

      • UF_BV2NAT_INT2BV_EXTRACT

        public static final ProofRewriteRule UF_BV2NAT_INT2BV_EXTRACT
        Auto-generated from RARE rule uf-bv2nat-int2bv-extract

      • UF_INT2BV_BV2NAT

        public static final ProofRewriteRule UF_INT2BV_BV2NAT
        Auto-generated from RARE rule uf-int2bv-bv2nat

      • UF_BV2NAT_GEQ_ELIM

        public static final ProofRewriteRule UF_BV2NAT_GEQ_ELIM
        Auto-generated from RARE rule uf-bv2nat-geq-elim

      • UF_INT2BV_BVULT_EQUIV

        public static final ProofRewriteRule UF_INT2BV_BVULT_EQUIV
        Auto-generated from RARE rule uf-int2bv-bvult-equiv

      • UF_INT2BV_BVULE_EQUIV

        public static final ProofRewriteRule UF_INT2BV_BVULE_EQUIV
        Auto-generated from RARE rule uf-int2bv-bvule-equiv

    • Method Detail

      • values

        public static ProofRewriteRule[] values()
        Returns an array containing the constants of this enum type, in the order they are declared. This method may be used to iterate over the constants as follows: 
        for (ProofRewriteRule c : ProofRewriteRule.values())
    System.out.println(c);
        Returns:
        an array containing the constants of this enum type, in the order they are declared

      • valueOf

        public static ProofRewriteRule valueOf​(java.lang.String name)
        Returns the enum constant of this type with the specified name. The string must match exactly an identifier used to declare an enum constant in this type. (Extraneous whitespace characters are not permitted.)
        Parameters:
        name - the name of the enum constant to be returned.
        Returns:
        the enum constant with the specified name
        Throws:
        java.lang.IllegalArgumentException - if this enum type has no constant with the specified name
        java.lang.NullPointerException - if the argument is null

      • getValue

        public int getValue()