ProofRule and ProofRewriteRule

Enum ProofRule captures the reasoning steps performed by the SAT solver, the theory solvers and the preprocessor. It represents the inference rules used to derive conclusions within a proof.

Enum ProofRewriteRule pertains to rewrites performed on terms. These identifiers are arguments of the proof rules THEORY_REWRITE and DSL_REWRITE.


class cvc5.ProofRule(value)

The ProofRule enum

ACI_NORM

verbatim embed:rst:leading-asterisk Builtin theory – associative/commutative/idempotency/identity normalization

\[\inferrule{- \mid t = s}{t = s}\]

where \(\texttt{expr::isACNorm(t, s)} = \top\). For details, see expr/nary_term_util.h. This method normalizes currently based on two kinds of operators: (1) those that are associative, commutative, idempotent, and have an identity element (examples are or, and, bvand), (2) those that are associative and have an identity element (examples are str.++, re.++). endverbatim

ALETHE_RULE

verbatim embed:rst:leading-asterisk External – Alethe

Place holder for Alethe rules.

\[\inferrule{P_1, \dots, P_n\mid \texttt{id}, Q, Q', A_1,\dots, A_m}{Q}\]

Note that the premises and arguments are arbitrary. It’s expected that \(\texttt{id}\) refer to a proof rule in the external Alethe calculus, and that \(Q'\) be the representation of Q to be printed by the Alethe printer. endverbatim

ALPHA_EQUIV

verbatim embed:rst:leading-asterisk Quantifiers – Alpha equivalence

\[\inferruleSC{-\mid F, (y_1 \ldots y_n), (z_1,\dots, z_n)} {F = F\{y_1\mapsto z_1,\dots,y_n\mapsto z_n\}} {if $y_1,\dots,y_n, z_1,\dots,z_n$ are unique bound variables}\]

Notice that this rule is correct only when \(z_1,\dots,z_n\) are not contained in \(FV(F) \setminus \{ y_1,\dots, y_n \}\), where \(FV(\varphi)\) are the free variables of \(\varphi\). The internal quantifiers proof checker does not currently check that this is the case. endverbatim

AND_ELIM

verbatim embed:rst:leading-asterisk Boolean – And elimination

\[\inferrule{(F_1 \land \dots \land F_n) \mid i}{F_i}\]

endverbatim

AND_INTRO

verbatim embed:rst:leading-asterisk Boolean – And introduction

\[\inferrule{F_1 \dots F_n \mid -}{(F_1 \land \dots \land F_n)}\]

endverbatim

ARITH_MULT_ABS_COMPARISON

verbatim embed:rst:leading-asterisk Arithmetic – Non-linear multiply absolute value comparison

\[\inferrule{F_1 \dots F_n \mid -}{F}\]

where \(F\) is of the form \(\left| t_1 \cdot t_n \right| \diamond \left| s_1 \cdot s_n \right|\). If \(\diamond\) is \(=\), then each \(F_i\) is \(\left| t_i \right| = \left| s_i \right|\).

If \(\diamond\) is \(>\), then each \(F_i\) is either \(\left| t_i \right| > \left| s_i \right|\) or \(\left| t_i \right| = \left| s_i \right| \land \left| t_i \right| \neq 0\), and \(F_1\) is of the former form.

endverbatim

ARITH_MULT_NEG

verbatim embed:rst:leading-asterisk Arithmetic – Multiplication with negative factor

\[\inferrule{- \mid m, l \diamond r}{(m < 0 \land l \diamond r) \rightarrow m \cdot l \diamond_{inv} m \cdot r}\]

where \(\diamond\) is a relation symbol and \(\diamond_{inv}\) the inverted relation symbol. endverbatim

ARITH_MULT_POS

verbatim embed:rst:leading-asterisk Arithmetic – Multiplication with positive factor

\[\inferrule{- \mid m, l \diamond r}{(m > 0 \land l \diamond r) \rightarrow m \cdot l \diamond m \cdot r}\]

where \(\diamond\) is a relation symbol. endverbatim

ARITH_MULT_SIGN

verbatim embed:rst:leading-asterisk Arithmetic – Sign inference

\[\inferrule{- \mid f_1 \dots f_k, m}{(f_1 \land \dots \land f_k) \rightarrow m \diamond 0}\]

where \(f_1 \dots f_k\) are variables compared to zero (less, greater or not equal), \(m\) is a monomial from these variables and \(\diamond\) is the comparison (less or equal) that results from the signs of the variables. All variables with even exponent in \(m\) should be given as not equal to zero while all variables with odd exponent in \(m\) should be given as less or greater than zero. endverbatim

ARITH_MULT_TANGENT

verbatim embed:rst:leading-asterisk Arithmetic – Multiplication tangent plane

\[ \begin{align}\begin{aligned}\inferruleSC{- \mid x, y, a, b, \sigma}{(t \leq tplane) = ((x \leq a \land y \geq b) \lor (x \geq a \land y \leq b))}{if $\sigma = \bot$}\\\inferruleSC{- \mid x, y, a, b, \sigma}{(t \geq tplane) = ((x \leq a \land y \leq b) \lor (x \geq a \land y \geq b))}{if $\sigma = \top$}\end{aligned}\end{align} \]

where \(x,y\) are real terms (variables or extended terms), \(t = x \cdot y\), \(a,b\) are real constants, \(\sigma \in \{ \top, \bot\}\) and \(tplane := b \cdot x + a \cdot y - a \cdot b\) is the tangent plane of \(x \cdot y\) at \((a,b)\). endverbatim

ARITH_POLY_NORM

verbatim embed:rst:leading-asterisk Arithmetic – Polynomial normalization

\[\inferrule{- \mid t = s}{t = s}\]

where \(\texttt{arith::PolyNorm::isArithPolyNorm(t, s)} = \top\). This method normalizes polynomials \(s\) and \(t\) over arithmetic or bitvectors. endverbatim

ARITH_POLY_NORM_REL

verbatim embed:rst:leading-asterisk Arithmetic – Polynomial normalization for relations

\[\inferrule{c_x \cdot (x_1 - x_2) = c_y \cdot (y_1 - y_2) \mid \diamond} {(x_1 \diamond x_2) = (y_1 \diamond y_2)}\]

where \(\diamond \in \{<, \leq, =, \geq, >\}\) for arithmetic and \(\diamond \in \{=\}\) for bitvectors. \(c_x\) and \(c_y\) are scaling factors. For \(<, \leq, \geq, >\), the scaling factors have the same sign. For bitvectors, they are set to \(1\).

If \(c_x\) has type \(Real\) and \(x_1, x_2\) are of type \(Int\), then \((x_1 - x_2)\) is wrapped in an application of to_real, similarly for \((y_1 - y_2)\). endverbatim

ARITH_REDUCTION

verbatim embed:rst:leading-asterisk Arithmetic – Reduction

\[\inferrule{- \mid t}{F}\]

where \(t\) is an application of an extended arithmetic operator (e.g. division, modulus, cosine, sqrt, is_int, to_int) and \(F\) is the reduction predicate for \(t\). In other words, \(F\) is a predicate that is used to reduce reasoning about \(t\) to reasoning about the core operators of arithmetic.

In detail, \(F\) is implemented by \(\texttt{arith::OperatorElim::getAxiomFor(t)}\), see theory/arith/operator_elim.h. endverbatim

ARITH_SUM_UB

verbatim embed:rst:leading-asterisk Arithmetic – Sum upper bounds

\[\inferrule{P_1 \dots P_n \mid -}{L \diamond R}\]

where \(P_i\) has the form \(L_i \diamond_i R_i\) and \(\diamond_i \in \{<, \leq, =\}\). Furthermore \(\diamond = <\) if \(\diamond_i = <\) for any \(i\) and \(\diamond = \leq\) otherwise, \(L = L_1 + \cdots + L_n\) and \(R = R_1 + \cdots + R_n\). endverbatim

ARITH_TRANS_EXP_APPROX_ABOVE_NEG

verbatim embed:rst:leading-asterisk Arithmetic – Transcendentals – Exp is approximated from above for negative values

\[\inferrule{- \mid d,t,l,u}{(t \geq l \land t \leq u) \rightarrow exp(t) \leq \texttt{secant}(\exp, l, u, t)}\]

where \(d\) is an even positive number, \(t\) an arithmetic term and \(l,u\) are lower and upper bounds on \(t\). Let \(p\) be the \(d\)’th taylor polynomial at zero (also called the Maclaurin series) of the exponential function. \(\texttt{secant}(\exp, l, u, t)\) denotes the secant of \(p\) from \((l, \exp(l))\) to \((u, \exp(u))\) evaluated at \(t\), calculated as follows:

\[\frac{p(l) - p(u)}{l - u} \cdot (t - l) + p(l)\]

The lemma states that if \(t\) is between \(l\) and \(u\), then \(\exp(t\) is below the secant of \(p\) from \(l\) to \(u\). endverbatim

ARITH_TRANS_EXP_APPROX_ABOVE_POS

verbatim embed:rst:leading-asterisk Arithmetic – Transcendentals – Exp is approximated from above for positive values

\[\inferrule{- \mid d,t,l,u}{(t \geq l \land t \leq u) \rightarrow exp(t) \leq \texttt{secant-pos}(\exp, l, u, t)}\]

where \(d\) is an even positive number, \(t\) an arithmetic term and \(l,u\) are lower and upper bounds on \(t\). Let \(p^*\) be a modification of the \(d\)’th taylor polynomial at zero (also called the Maclaurin series) of the exponential function as follows where \(p(d-1)\) is the regular Maclaurin series of degree \(d-1\):

\[p^* := p(d-1) \cdot \frac{1 + t^n}{n!}\]

\(\texttt{secant-pos}(\exp, l, u, t)\) denotes the secant of \(p\) from \((l, \exp(l))\) to \((u, \exp(u))\) evaluated at \(t\), calculated as follows:

\[\frac{p(l) - p(u)}{l - u} \cdot (t - l) + p(l)\]

The lemma states that if \(t\) is between \(l\) and \(u\), then \(\exp(t\) is below the secant of \(p\) from \(l\) to \(u\). endverbatim

ARITH_TRANS_EXP_APPROX_BELOW

verbatim embed:rst:leading-asterisk Arithmetic – Transcendentals – Exp is approximated from below

\[\inferrule{- \mid d,c,t}{t \geq c \rightarrow exp(t) \geq \texttt{maclaurin}(\exp, d, c)}\]

where \(d\) is an odd positive number, \(t\) an arithmetic term and \(\texttt{maclaurin}(\exp, d, c)\) is the \(d\)’th taylor polynomial at zero (also called the Maclaurin series) of the exponential function evaluated at \(c\). The Maclaurin series for the exponential function is the following:

\[\exp(x) = \sum_{n=0}^{\infty} \frac{x^n}{n!}\]

endverbatim

ARITH_TRANS_EXP_NEG

verbatim embed:rst:leading-asterisk Arithmetic – Transcendentals – Exp at negative values

\[\inferrule{- \mid t}{(t < 0) \leftrightarrow (\exp(t) < 1)}\]

endverbatim

ARITH_TRANS_EXP_POSITIVITY

verbatim embed:rst:leading-asterisk Arithmetic – Transcendentals – Exp is always positive

\[\inferrule{- \mid t}{\exp(t) > 0}\]

endverbatim

ARITH_TRANS_EXP_SUPER_LIN

verbatim embed:rst:leading-asterisk Arithmetic – Transcendentals – Exp grows super-linearly for positive values

\[\inferrule{- \mid t}{t \leq 0 \lor \exp(t) > t+1}\]

endverbatim

ARITH_TRANS_EXP_ZERO

verbatim embed:rst:leading-asterisk Arithmetic – Transcendentals – Exp at zero

\[\inferrule{- \mid t}{(t=0) \leftrightarrow (\exp(t) = 1)}\]

endverbatim

ARITH_TRANS_PI

verbatim embed:rst:leading-asterisk Arithmetic – Transcendentals – Assert bounds on Pi

\[\inferrule{- \mid l, u}{\texttt{real.pi} \geq l \land \texttt{real.pi} \leq u}\]

where \(l,u\) are valid lower and upper bounds on \(\pi\). endverbatim

ARITH_TRANS_SINE_APPROX_ABOVE_NEG

verbatim embed:rst:leading-asterisk Arithmetic – Transcendentals – Sine is approximated from above for negative values

\[\inferrule{- \mid d,t,lb,ub,l,u}{(t \geq lb land t \leq ub) \rightarrow \sin(t) \leq \texttt{secant}(\sin, l, u, t)}\]

where \(d\) is an even positive number, \(t\) an arithmetic term, \(lb,ub\) are symbolic lower and upper bounds on \(t\) (possibly containing \(\pi\)) and \(l,u\) the evaluated lower and upper bounds on \(t\). Let \(p\) be the \(d\)’th taylor polynomial at zero (also called the Maclaurin series) of the sine function. \(\texttt{secant}(\sin, l, u, t)\) denotes the secant of \(p\) from \((l, \sin(l))\) to \((u, \sin(u))\) evaluated at \(t\), calculated as follows:

\[\frac{p(l) - p(u)}{l - u} \cdot (t - l) + p(l)\]

The lemma states that if \(t\) is between \(l\) and \(u\), then \(\sin(t)\) is below the secant of \(p\) from \(l\) to \(u\). endverbatim

ARITH_TRANS_SINE_APPROX_ABOVE_POS

verbatim embed:rst:leading-asterisk Arithmetic – Transcendentals – Sine is approximated from above for positive values

\[\inferrule{- \mid d,t,c,lb,ub}{(t \geq lb land t \leq ub) \rightarrow \sin(t) \leq \texttt{upper}(\sin, c)}\]

where \(d\) is an even positive number, \(t\) an arithmetic term, \(c\) an arithmetic constant and \(lb,ub\) are symbolic lower and upper bounds on \(t\) (possibly containing \(\pi\)). Let \(p\) be the \(d\)’th taylor polynomial at zero (also called the Maclaurin series) of the sine function. \(\texttt{upper}(\sin, c)\) denotes the upper bound on \(\sin(c)\) given by \(p\) and \(lb,up\) such that \(\sin(t)\) is the maximum of the sine function on \((lb,ub)\). endverbatim

ARITH_TRANS_SINE_APPROX_BELOW_NEG

verbatim embed:rst:leading-asterisk Arithmetic – Transcendentals – Sine is approximated from below for negative values

\[\inferrule{- \mid d,t,c,lb,ub}{(t \geq lb land t \leq ub) \rightarrow \sin(t) \geq \texttt{lower}(\sin, c)}\]

where \(d\) is an even positive number, \(t\) an arithmetic term, \(c\) an arithmetic constant and \(lb,ub\) are symbolic lower and upper bounds on \(t\) (possibly containing \(\pi\)). Let \(p\) be the \(d\)’th taylor polynomial at zero (also called the Maclaurin series) of the sine function. \(\texttt{lower}(\sin, c)\) denotes the lower bound on \(\sin(c)\) given by \(p\) and \(lb,up\) such that \(\sin(t)\) is the minimum of the sine function on \((lb,ub)\). endverbatim

ARITH_TRANS_SINE_APPROX_BELOW_POS

verbatim embed:rst:leading-asterisk Arithmetic – Transcendentals – Sine is approximated from below for positive values

\[\inferrule{- \mid d,t,lb,ub,l,u}{(t \geq lb land t \leq ub) \rightarrow \sin(t) \geq \texttt{secant}(\sin, l, u, t)}\]

where \(d\) is an even positive number, \(t\) an arithmetic term, \(lb,ub\) are symbolic lower and upper bounds on \(t\) (possibly containing \(\pi\)) and \(l,u\) the evaluated lower and upper bounds on \(t\). Let \(p\) be the \(d\)’th taylor polynomial at zero (also called the Maclaurin series) of the sine function. \(\texttt{secant}(\sin, l, u, t)\) denotes the secant of \(p\) from \((l, \sin(l))\) to \((u, \sin(u))\) evaluated at \(t\), calculated as follows:

\[\frac{p(l) - p(u)}{l - u} \cdot (t - l) + p(l)\]

The lemma states that if \(t\) is between \(l\) and \(u\), then \(\sin(t)\) is above the secant of \(p\) from \(l\) to \(u\). endverbatim

ARITH_TRANS_SINE_BOUNDS

verbatim embed:rst:leading-asterisk Arithmetic – Transcendentals – Sine is always between -1 and 1

\[\inferrule{- \mid t}{\sin(t) \leq 1 \land \sin(t) \geq -1}\]

endverbatim

ARITH_TRANS_SINE_SHIFT

verbatim embed:rst:leading-asterisk Arithmetic – Transcendentals – Sine is shifted to -pi…pi

\[\inferrule{- \mid x}{-\pi \leq y \leq \pi \land \sin(y) = \sin(x) \land (\ite{-\pi \leq x \leq \pi}{x = y}{x = y + 2 \pi s})}\]

where \(x\) is the argument to sine, \(y\) is a new real skolem that is \(x\) shifted into \(-\pi \dots \pi\) and \(s\) is a new integer skolem that is the number of phases \(y\) is shifted. In particular, \(y\) is the TRANSCENDENTAL_PURIFY_ARG skolem for \(\sin(x)\) and \(s\) is the TRANSCENDENTAL_SINE_PHASE_SHIFT skolem for \(x\). endverbatim

ARITH_TRANS_SINE_SYMMETRY

verbatim embed:rst:leading-asterisk Arithmetic – Transcendentals – Sine is symmetric with respect to negation of the argument

\[\inferrule{- \mid t}{\sin(t) - \sin(-t) = 0}\]

endverbatim

ARITH_TRANS_SINE_TANGENT_PI

verbatim embed:rst:leading-asterisk Arithmetic – Transcendentals – Sine is bounded by the tangents at -pi and pi

\[\inferrule{- \mid t}{(t > -\pi \rightarrow \sin(t) > -\pi - t) \land (t < \pi \rightarrow \sin(t) < \pi - t)} \endverbatim\]
ARITH_TRANS_SINE_TANGENT_ZERO

verbatim embed:rst:leading-asterisk Arithmetic – Transcendentals – Sine is bounded by the tangent at zero

\[\inferrule{- \mid t}{(t > 0 \rightarrow \sin(t) < t) \land (t < 0 \rightarrow \sin(t) > t)} \endverbatim\]
ARITH_TRICHOTOMY

verbatim embed:rst:leading-asterisk Arithmetic – Trichotomy of the reals

\[\inferrule{A, B \mid -}{C}\]

where \(\neg A, \neg B, C\) are \(x < c, x = c, x > c\) in some order. Note that \(\neg\) here denotes arithmetic negation, i.e., flipping \(\geq\) to \(<\) etc. endverbatim

ARRAYS_EXT

verbatim embed:rst:leading-asterisk Arrays – Arrays extensionality

\[\inferrule{a \neq b\mid -} {\mathit{select}(a,k)\neq\mathit{select}(b,k)}\]

where \(k\) is the \(\texttt{ARRAY_DEQ_DIFF}\) skolem for (a, b). endverbatim

ARRAYS_READ_OVER_WRITE

verbatim embed:rst:leading-asterisk Arrays – Read over write

\[\inferrule{i_1 \neq i_2\mid \mathit{select}(\mathit{store}(a,i_1,e),i_2)} {\mathit{select}(\mathit{store}(a,i_1,e),i_2) = \mathit{select}(a,i_2)}\]

endverbatim

ARRAYS_READ_OVER_WRITE_1

verbatim embed:rst:leading-asterisk Arrays – Read over write 1

\[\inferrule{-\mid \mathit{select}(\mathit{store}(a,i,e),i)} {\mathit{select}(\mathit{store}(a,i,e),i)=e}\]

endverbatim

ARRAYS_READ_OVER_WRITE_CONTRA

verbatim embed:rst:leading-asterisk Arrays – Read over write, contrapositive

\[\inferrule{\mathit{select}(\mathit{store}(a,i_2,e),i_1) \neq \mathit{select}(a,i_1)\mid -}{i_1=i_2}\]

endverbatim

ASSUME

verbatim embed:rst:leading-asterisk Assumption (a leaf)

\[\inferrule{- \mid F}{F}\]

This rule has special status, in that an application of assume is an open leaf in a proof that is not (yet) justified. An assume leaf is analogous to a free variable in a term, where we say “F is a free assumption in proof P” if it contains an application of F that is not bound by SCOPE (see below). endverbatim

BV_BITBLAST_STEP

verbatim embed:rst:leading-asterisk Bit-vectors – Bitblast bit-vector constant, variable, and terms

For constant and variables:

\[\inferrule{-\mid t}{t = \texttt{bitblast}(t)}\]

For terms:

\[\inferrule{-\mid k(\texttt{bitblast}(t_1),\dots,\texttt{bitblast}(t_n))} {k(\texttt{bitblast}(t_1),\dots,\texttt{bitblast}(t_n)) = \texttt{bitblast}(t)}\]

where \(t\) is \(k(t_1,\dots,t_n)\). endverbatim

BV_EAGER_ATOM

verbatim embed:rst:leading-asterisk Bit-vectors – Bit-vector eager atom

\[\inferrule{-\mid F}{F = F[0]}\]

where \(F\) is of kind BITVECTOR_EAGER_ATOM. endverbatim

CHAIN_RESOLUTION

verbatim embed:rst:leading-asterisk Boolean – N-ary Resolution

\[\inferrule{C_1 \dots C_n \mid (pol_1 \dots pol_{n-1}), (L_1 \dots L_{n-1})}{C}\]

where

  • let \(C_1 \dots C_n\) be nodes viewed as clauses, as defined above

  • let \(C_1 \diamond_{L,pol} C_2\) represent the resolution of \(C_1\) with \(C_2\) with pivot \(L\) and polarity \(pol\), as defined above

  • let \(C_1' = C_1\),

  • for each \(i > 1\), let \(C_i' = C_{i-1} \diamond_{L_{i-1}, pol_{i-1}} C_i'\)

Note the list of polarities and pivots are provided as s-expressions.

The result of the chain resolution is \(C = C_n'\) endverbatim

CNF_AND_NEG

verbatim embed:rst:leading-asterisk Boolean – CNF – And Negative

\[\inferrule{- \mid (F_1 \land \dots \land F_n)}{(F_1 \land \dots \land F_n) \lor \neg F_1 \lor \dots \lor \neg F_n}\]

endverbatim

CNF_AND_POS

verbatim embed:rst:leading-asterisk Boolean – CNF – And Positive

\[\inferrule{- \mid (F_1 \land \dots \land F_n), i}{\neg (F_1 \land \dots \land F_n) \lor F_i}\]

endverbatim

CNF_EQUIV_NEG1

verbatim embed:rst:leading-asterisk Boolean – CNF – Equiv Negative 1

\[\inferrule{- \mid F_1 = F_2}{(F_1 = F_2) \lor F_1 \lor F_2}\]

endverbatim

CNF_EQUIV_NEG2

verbatim embed:rst:leading-asterisk Boolean – CNF – Equiv Negative 2

\[\inferrule{- \mid F_1 = F_2}{(F_1 = F_2) \lor \neg F_1 \lor \neg F_2}\]

endverbatim

CNF_EQUIV_POS1

verbatim embed:rst:leading-asterisk Boolean – CNF – Equiv Positive 1

\[\inferrule{- \mid F_1 = F_2}{F_1 \neq F_2 \lor \neg F_1 \lor F_2}\]

endverbatim

CNF_EQUIV_POS2

verbatim embed:rst:leading-asterisk Boolean – CNF – Equiv Positive 2

\[\inferrule{- \mid F_1 = F_2}{F_1 \neq F_2 \lor F_1 \lor \neg F_2}\]

endverbatim

CNF_IMPLIES_NEG1

verbatim embed:rst:leading-asterisk Boolean – CNF – Implies Negative 1

\[\inferrule{- \mid F_1 \rightarrow F_2}{(F_1 \rightarrow F_2) \lor F_1}\]

endverbatim

CNF_IMPLIES_NEG2

verbatim embed:rst:leading-asterisk Boolean – CNF – Implies Negative 2

\[\inferrule{- \mid F_1 \rightarrow F_2}{(F_1 \rightarrow F_2) \lor \neg F_2}\]

endverbatim

CNF_IMPLIES_POS

verbatim embed:rst:leading-asterisk Boolean – CNF – Implies Positive

\[\inferrule{- \mid F_1 \rightarrow F_2}{\neg(F_1 \rightarrow F_2) \lor \neg F_1 \lor F_2}\]

endverbatim

CNF_ITE_NEG1

verbatim embed:rst:leading-asterisk Boolean – CNF – ITE Negative 1

\[\inferrule{- \mid (\ite{C}{F_1}{F_2})}{(\ite{C}{F_1}{F_2}) \lor \neg C \lor \neg F_1}\]

endverbatim

CNF_ITE_NEG2

verbatim embed:rst:leading-asterisk Boolean – CNF – ITE Negative 2

\[\inferrule{- \mid (\ite{C}{F_1}{F_2})}{(\ite{C}{F_1}{F_2}) \lor C \lor \neg F_2}\]

endverbatim

CNF_ITE_NEG3

verbatim embed:rst:leading-asterisk Boolean – CNF – ITE Negative 3

\[\inferrule{- \mid (\ite{C}{F_1}{F_2})}{(\ite{C}{F_1}{F_2}) \lor \neg F_1 \lor \neg F_2}\]

endverbatim

CNF_ITE_POS1

verbatim embed:rst:leading-asterisk Boolean – CNF – ITE Positive 1

\[\inferrule{- \mid (\ite{C}{F_1}{F_2})}{\neg(\ite{C}{F_1}{F_2}) \lor \neg C \lor F_1}\]

endverbatim

CNF_ITE_POS2

verbatim embed:rst:leading-asterisk Boolean – CNF – ITE Positive 2

\[\inferrule{- \mid (\ite{C}{F_1}{F_2})}{\neg(\ite{C}{F_1}{F_2}) \lor C \lor F_2}\]

endverbatim

CNF_ITE_POS3

verbatim embed:rst:leading-asterisk Boolean – CNF – ITE Positive 3

\[\inferrule{- \mid (\ite{C}{F_1}{F_2})}{\neg(\ite{C}{F_1}{F_2}) \lor F_1 \lor F_2}\]

endverbatim

CNF_OR_NEG

verbatim embed:rst:leading-asterisk Boolean – CNF – Or Negative

\[\inferrule{- \mid (F_1 \lor \dots \lor F_n), i}{(F_1 \lor \dots \lor F_n) \lor \neg F_i}\]

endverbatim

CNF_OR_POS

verbatim embed:rst:leading-asterisk Boolean – CNF – Or Positive

\[\inferrule{- \mid (F_1 \lor \dots \lor F_n)}{\neg(F_1 \lor \dots \lor F_n) \lor F_1 \lor \dots \lor F_n}\]

endverbatim

CNF_XOR_NEG1

verbatim embed:rst:leading-asterisk Boolean – CNF – XOR Negative 1

\[\inferrule{- \mid F_1 \xor F_2}{(F_1 \xor F_2) \lor \neg F_1 \lor F_2}\]

endverbatim

CNF_XOR_NEG2

verbatim embed:rst:leading-asterisk Boolean – CNF – XOR Negative 2

\[\inferrule{- \mid F_1 \xor F_2}{(F_1 \xor F_2) \lor F_1 \lor \neg F_2}\]

endverbatim

CNF_XOR_POS1

verbatim embed:rst:leading-asterisk Boolean – CNF – XOR Positive 1

\[\inferrule{- \mid F_1 \xor F_2}{\neg(F_1 \xor F_2) \lor F_1 \lor F_2}\]

endverbatim

CNF_XOR_POS2

verbatim embed:rst:leading-asterisk Boolean – CNF – XOR Positive 2

\[\inferrule{- \mid F_1 \xor F_2}{\neg(F_1 \xor F_2) \lor \neg F_1 \lor \neg F_2}\]

endverbatim

CONCAT_CONFLICT

verbatim embed:rst:leading-asterisk Strings – Core rules – Concatenation conflict

\[\inferrule{(c_1\cdot t) = (c_2 \cdot s)\mid b}{\bot}\]

where \(b\) indicates if the direction is reversed, \(c_1,\,c_2\) are constants such that \(\texttt{Word::splitConstant}(c_1,c_2, \mathit{index},b)\) is null, in other words, neither is a prefix of the other. Note it may be the case that one side of the equality denotes the empty string.

This rule is used exclusively for strings.

endverbatim

CONCAT_CONFLICT_DEQ

verbatim embed:rst:leading-asterisk Strings – Core rules – Concatenation conflict for disequal characters

\[\inferrule{(t_1\cdot t) = (s_1 \cdot s), t_1 \neq s_1 \mid b}{\bot}\]

where \(t_1\) and \(s_1\) are constants of length one, or otherwise one side of the equality is the empty sequence and \(t_1\) or \(s_1\) corresponding to that side is the empty sequence.

This rule is used exclusively for sequences.

endverbatim

CONCAT_CPROP

verbatim embed:rst:leading-asterisk Strings – Core rules – Concatenation constant propagation

\[\inferrule{(t_1\cdot w_1\cdot t_2) = (w_2 \cdot s),\, \mathit{len}(t_1) \neq 0\mid \bot}{(t_1 = t_3\cdot r)}\]

where \(w_1,\,w_2\) are words, \(t_3\) is \(\mathit{pre}(w_2,p)\), \(p\) is \(\texttt{Word::overlap}(\mathit{suf}(w_2,1), w_1)\), and \(r\) is the purification skolem for \(\mathit{suf}(t_1,\mathit{len}(w_3))\). Note that \(\mathit{suf}(w_2,p)\) is the largest suffix of \(\mathit{suf}(w_2,1)\) that can contain a prefix of \(w_1\); since \(t_1\) is non-empty, \(w_3\) must therefore be contained in \(t_1\).

Alternatively for the reverse:

\[\inferrule{(t_1\cdot w_1\cdot t_2) = (s \cdot w_2),\, \mathit{len}(t_2) \neq 0\mid \top}{(t_2 = r\cdot t_3)}\]

where \(w_1,\,w_2\) are words, \(t_3\) is \(\mathit{substr}(w_2, \mathit{len}(w_2) - p, p)\), \(p\) is \(\texttt{Word::roverlap}(\mathit{pre}(w_2, \mathit{len}(w_2) - 1), w_1)\), and \(r\) is the purification skolem for \(\mathit{pre}(t_2,\mathit{len}(t_2) - \mathit{len}(w_3))\). Note that \(\mathit{pre}(w_2, \mathit{len}(w_2) - p)\) is the largest prefix of \(\mathit{pre}(w_2, \mathit{len}(w_2) - 1)\) that can contain a suffix of \(w_1\); since \(t_2\) is non-empty, \(w_3\) must therefore be contained in \(t_2\). endverbatim

CONCAT_CSPLIT

verbatim embed:rst:leading-asterisk Strings – Core rules – Concatenation split for constants

\[\inferrule{(t_1\cdot t_2) = (c \cdot s_2),\, \mathit{len}(t_1) \neq 0\mid \bot}{(t_1 = c\cdot r)}\]

where \(r\) is the purification skolem for \(\mathit{suf}(t_1,1)\).

Alternatively for the reverse:

\[\inferrule{(t_1\cdot t_2) = (s_1 \cdot c),\, \mathit{len}(t_2) \neq 0\mid \top}{(t_2 = r\cdot c)}\]

where \(r\) is the purification skolem for \(\mathit{pre}(t_2,\mathit{len}(t_2) - 1)\). endverbatim

CONCAT_EQ

verbatim embed:rst:leading-asterisk Strings – Core rules – Concatenation equality

\[\inferrule{(t_1\cdot\ldots \cdot t_n \cdot t) = (t_1 \cdot\ldots \cdot t_n\cdot s)\mid b}{t = s}\]

where \(\cdot\) stands for string concatenation and \(b\) indicates if the direction is reversed.

Notice that \(t\) or \(s\) may be empty, in which case they are implicit in the concatenation above. For example, if the premise is \(x\cdot z = x\), then this rule, with argument \(\bot\), concludes \(z = \epsilon\).

Also note that constants are split, such that for \((\mathsf{'abc'} \cdot x) = (\mathsf{'a'} \cdot y)\), this rule, with argument \(\bot\), concludes \((\mathsf{'bc'} \cdot x) = y\). This splitting is done only for constants such that Word::splitConstant returns non-null. endverbatim

CONCAT_LPROP

verbatim embed:rst:leading-asterisk Strings – Core rules – Concatenation length propagation

\[\inferrule{(t_1\cdot t_2) = (s_1 \cdot s_2),\, \mathit{len}(t_1) > \mathit{len}(s_1)\mid \bot}{(t_1 = s_1\cdot r)}\]

where \(r\) is the purification Skolem for \(\mathit{ite}( \mathit{len}(t_1) >= \mathit{len}(s_1), \mathit{suf}(t_1,\mathit{len}(s_1)), \mathit{suf}(s_1,\mathit{len}(t_1)))\).

Alternatively for the reverse:

\[\inferrule{(t_1\cdot t_2) = (s_1 \cdot s_2),\, \mathit{len}(t_2) > \mathit{len}(s_2)\mid \top}{(t_2 = r \cdot s_2)}\]

where \(r\) is the purification Skolem for \(\mathit{ite}( \mathit{len}(t_2) >= \mathit{len}(s_2), \mathit{pre}(t_2,\mathit{len}(t_2) - \mathit{len}(s_2)), \mathit{pre}(s_2,\mathit{len}(s_2) - \mathit{len}(t_2)))\) endverbatim

CONCAT_SPLIT

verbatim embed:rst:leading-asterisk Strings – Core rules – Concatenation split

\[\inferruleSC{(t_1\cdot t_2) = (s_1 \cdot s_2),\, \mathit{len}(t_1) \neq \mathit{len}(s_1)\mid b}{((t_1 = s_1\cdot r) \vee (s_1 = t_1\cdot r)) \wedge r \neq \epsilon \wedge \mathit{len}(r)>0}{if $b=\bot$}\]

where \(r\) is the purification skolem for \(\mathit{ite}( \mathit{len}(t_1) >= \mathit{len}(s_1), \mathit{suf}(t_1,\mathit{len}(s_1)), \mathit{suf}(s_1,\mathit{len}(t_1)))\) and \(\epsilon\) is the empty string (or sequence).

\[\inferruleSC{(t_1\cdot t_2) = (s_1 \cdot s_2),\, \mathit{len}(t_2) \neq \mathit{len}(s_2)\mid b}{((t_2 = r \cdot s_2) \vee (s_2 = r \cdot t_2)) \wedge r \neq \epsilon \wedge \mathit{len}(r)>0}{if $b=\top$}\]

where \(r\) is the purification Skolem for \(\mathit{ite}( \mathit{len}(t_2) >= \mathit{len}(s_2), \mathit{pre}(t_2,\mathit{len}(t_2) - \mathit{len}(s_2)), \mathit{pre}(s_2,\mathit{len}(s_2) - \mathit{len}(t_2)))\) and \(\epsilon\) is the empty string (or sequence).

Above, \(\mathit{suf}(x,n)\) is shorthand for \(\mathit{substr}(x,n, \mathit{len}(x) - n)\) and \(\mathit{pre}(x,n)\) is shorthand for \(\mathit{substr}(x,0,n)\). endverbatim

CONCAT_UNIFY

verbatim embed:rst:leading-asterisk Strings – Core rules – Concatenation unification

\[\inferrule{(t_1\cdot t_2) = (s_1 \cdot s_2),\, \mathit{len}(t_1) = \mathit{len}(s_1)\mid \bot}{t_1 = s_1}\]

Alternatively for the reverse:

\[\inferrule{(t_1\cdot t_2) = (s_1 \cdot s_2),\, \mathit{len}(t_2) = \mathit{len}(s_2)\mid \top}{t_2 = s_2}\]

endverbatim

CONG

verbatim embed:rst:leading-asterisk Equality – Congruence

\[\inferrule{t_1=s_1,\dots,t_n=s_n\mid k, f?}{k(f?, t_1,\dots, t_n) = k(f?, s_1,\dots, s_n)}\]

where \(k\) is the application kind. Notice that \(f\) must be provided iff \(k\) is a parameterized kind, e.g. cvc5::Kind::APPLY_UF. The actual node for \(k\) is constructible via ProofRuleChecker::mkKindNode. If \(k\) is a binder kind (e.g. cvc5::Kind::FORALL) then \(f\) is a term of kind cvc5::Kind::VARIABLE_LIST denoting the variables bound by both sides of the conclusion. This rule is used for kinds that have a fixed arity, such as cvc5::Kind::ITE, cvc5::Kind::EQUAL, and so on. It is also used for cvc5::Kind::APPLY_UF where \(f\) must be provided. It is not used for equality between cvc5::Kind::HO_APPLY terms, which should use the HO_CONG proof rule. endverbatim

CONTRA

verbatim embed:rst:leading-asterisk Boolean – Contradiction

\[\inferrule{F, \neg F \mid -}{\bot}\]

endverbatim

DRAT_REFUTATION

verbatim embed:rst:leading-asterisk DRAT Refutation

\[\inferrule{F_1 \dots F_n \mid D, P}{\bot}\]

where \(F_1 \dots F_n\) correspond to the clauses in the DIMACS file given by filename D and P is a filename of a file storing a DRAT proof. endverbatim

DSL_REWRITE

verbatim embed:rst:leading-asterisk Builtin theory – DSL rewrite

\[\inferrule{F_1 \dots F_n \mid id t_1 \dots t_n}{F}\]

where id is a ProofRewriteRule whose definition in the RARE DSL is \(\forall x_1 \dots x_n. (G_1 \wedge G_n) \Rightarrow G\) where for \(i=1, \dots n\), we have that \(F_i = \sigma(G_i)\) and \(F = \sigma(G)\) where \(\sigma\) is the substitution \(\{x_1\mapsto t_1,\dots,x_n\mapsto t_n\}\).

Notice that the application of the substitution takes into account the possible list semantics of variables \(x_1 \ldots x_n\). If \(x_i\) is a variable with list semantics, then \(t_i\) denotes a list of terms. The substitution implemented by \(\texttt{expr::narySubstitute}\) (for details, see expr/nary_term_util.h) which replaces each \(x_i\) with the list \(t_i\) in its place. endverbatim

DT_CLASH

verbatim embed:rst:leading-asterisk Datatypes – Clash

\[\inferruleSC{\mathit{is}_{C_i}(t), \mathit{is}_{C_j}(t)\mid -}{\bot} {if $i\neq j$}\]

endverbatim

DT_SPLIT

verbatim embed:rst:leading-asterisk Datatypes – Split

\[\inferrule{-\mid t}{\mathit{is}_{C_1}(t)\vee\cdots\vee\mathit{is}_{C_n}(t)}\]

where \(C_1,\dots,C_n\) are all the constructors of the type of \(t\). endverbatim

ENCODE_EQ_INTRO

verbatim embed:rst:leading-asterisk Builtin theory – Encode equality introduction

\[\inferrule{- \mid t}{t=t'}\]

where \(t\) and \(t'\) are equivalent up to their encoding in an external proof format.

More specifically, it is the case that \(\texttt{RewriteDbNodeConverter::postConvert}(t) = t;\). This conversion method for instance may drop user patterns from quantified formulas or change the representation of \(t\) in a way that is a no-op in external proof formats.

Note this rule can be treated as a REFL when appropriate in external proof formats. endverbatim

EQUIV_ELIM1

verbatim embed:rst:leading-asterisk Boolean – Equivalence elimination version 1

\[\inferrule{F_1 = F_2 \mid -}{\neg F_1 \lor F_2}\]

endverbatim

EQUIV_ELIM2

verbatim embed:rst:leading-asterisk Boolean – Equivalence elimination version 2

\[\inferrule{F_1 = F_2 \mid -}{F_1 \lor \neg F_2}\]

endverbatim

EQ_RESOLVE

verbatim embed:rst:leading-asterisk Boolean – Equality resolution

\[\inferrule{F_1, (F_1 = F_2) \mid -}{F_2}\]

Note this can optionally be seen as a macro for EQUIV_ELIM1 + RESOLUTION. endverbatim

EVALUATE

verbatim embed:rst:leading-asterisk Builtin theory – Evaluate

\[\inferrule{- \mid t}{t = \texttt{evaluate}(t)}\]

where \(\texttt{evaluate}\) is implemented by calling the method \(\texttt{Evalutor::evaluate}\) in theory/evaluator.h with an empty substitution. Note this is equivalent to: (REWRITE t MethodId::RW_EVALUATE). endverbatim

FACTORING

verbatim embed:rst:leading-asterisk Boolean – Factoring

\[\inferrule{C_1 \mid -}{C_2}\]

where \(C_2\) is the clause \(C_1\), but every occurrence of a literal after its first occurrence is omitted. endverbatim

FALSE_ELIM

verbatim embed:rst:leading-asterisk Equality – False elim

\[\inferrule{F=\bot\mid -}{\neg F}\]

endverbatim

FALSE_INTRO

verbatim embed:rst:leading-asterisk Equality – False intro

\[\inferrule{\neg F\mid -}{F = \bot}\]

endverbatim

HO_APP_ENCODE

verbatim embed:rst:leading-asterisk Equality – Higher-order application encoding

\[\inferrule{-\mid t}{t=t'}\]

where t’ is the higher-order application that is equivalent to t, as implemented by uf::TheoryUfRewriter::getHoApplyForApplyUf. For details see theory/uf/theory_uf_rewriter.h

For example, this rule concludes \(f(x,y) = @( @(f,x), y)\), where \(@\) is the HO_APPLY kind.

Note this rule can be treated as a REFL when appropriate in external proof formats.

endverbatim

HO_CONG

verbatim embed:rst:leading-asterisk Equality – Higher-order congruence

\[\inferrule{f=g, t_1=s_1,\dots,t_n=s_n\mid k}{k(f, t_1,\dots, t_n) = k(g, s_1,\dots, s_n)}\]

Notice that this rule is only used when the application kind \(k\) is either cvc5::Kind::APPLY_UF or cvc5::Kind::HO_APPLY. endverbatim

IMPLIES_ELIM

verbatim embed:rst:leading-asterisk Boolean – Implication elimination

\[\inferrule{F_1 \rightarrow F_2 \mid -}{\neg F_1 \lor F_2}\]

endverbatim

INSTANTIATE

verbatim embed:rst:leading-asterisk Quantifiers – Instantiation

\[\inferrule{\forall x_1\dots x_n.\> F\mid (t_1 \dots t_n), (id\, (t)?)?} {F\{x_1\mapsto t_1,\dots,x_n\mapsto t_n\}}\]

The list of terms to instantiate \((t_1 \dots t_n)\) is provided as an s-expression as the first argument. The optional argument \(id\) indicates the inference id that caused the instantiation. The term \(t\) indicates an additional term (e.g. the trigger) associated with the instantiation, which depends on the id. If the id has prefix QUANTIFIERS_INST_E_MATCHING, then \(t\) is the trigger that generated the instantiation. endverbatim

INT_TIGHT_LB

verbatim embed:rst:leading-asterisk Arithmetic – Tighten strict integer lower bounds

\[\inferrule{i > c \mid -}{i \geq \lceil c \rceil}\]

where \(i\) has integer type. endverbatim

INT_TIGHT_UB

verbatim embed:rst:leading-asterisk Arithmetic – Tighten strict integer upper bounds

\[\inferrule{i < c \mid -}{i \leq \lfloor c \rfloor}\]

where \(i\) has integer type. endverbatim

ITE_ELIM1

verbatim embed:rst:leading-asterisk Boolean – ITE elimination version 1

\[\inferrule{(\ite{C}{F_1}{F_2}) \mid -}{\neg C \lor F_1}\]

endverbatim

ITE_ELIM2

verbatim embed:rst:leading-asterisk Boolean – ITE elimination version 2

\[\inferrule{(\ite{C}{F_1}{F_2}) \mid -}{C \lor F_2}\]

endverbatim

ITE_EQ

verbatim embed:rst:leading-asterisk Processing rules – If-then-else equivalence

\[\inferrule{- \mid \ite{C}{t_1}{t_2}}{\ite{C}{((\ite{C}{t_1}{t_2}) = t_1)}{((\ite{C}{t_1}{t_2}) = t_2)}}\]

endverbatim

LFSC_RULE

verbatim embed:rst:leading-asterisk External – LFSC

Place holder for LFSC rules.

\[\inferrule{P_1, \dots, P_n\mid \texttt{id}, Q, A_1,\dots, A_m}{Q}\]

Note that the premises and arguments are arbitrary. It’s expected that \(\texttt{id}\) refer to a proof rule in the external LFSC calculus. endverbatim

MACRO_ARITH_SCALE_SUM_UB

verbatim embed:rst:leading-asterisk Arithmetic – Adding inequalities

An arithmetic literal is a term of the form \(p \diamond c\) where \(\diamond \in \{ <, \leq, =, \geq, > \}\), \(p\) a polynomial and \(c\) a rational constant.

\[\inferrule{l_1 \dots l_n \mid k_1 \dots k_n}{t_1 \diamond t_2}\]

where \(k_i \in \mathbb{R}, k_i \neq 0\), \(\diamond\) is the fusion of the \(\diamond_i\) (flipping each if its \(k_i\) is negative) such that \(\diamond_i \in \{ <, \leq \}\) (this implies that lower bounds have negative \(k_i\) and upper bounds have positive \(k_i\)), \(t_1\) is the sum of the scaled polynomials and \(t_2\) is the sum of the scaled constants:

\[ \begin{align}\begin{aligned}t_1 \colon= k_1 \cdot p_1 + \cdots + k_n \cdot p_n\\t_2 \colon= k_1 \cdot c_1 + \cdots + k_n \cdot c_n\end{aligned}\end{align} \]

endverbatim

MACRO_BV_BITBLAST

verbatim embed:rst:leading-asterisk Bit-vectors – (Macro) Bitblast

\[\inferrule{-\mid t}{t = \texttt{bitblast}(t)}\]

where \(\texttt{bitblast}\) represents the result of the bit-blasted term as a bit-vector consisting of the output bits of the bit-blasted circuit representation of the term. Terms are bit-blasted according to the strategies defined in theory/bv/bitblast/bitblast_strategies_template.h. endverbatim

MACRO_RESOLUTION

verbatim embed:rst:leading-asterisk Boolean – N-ary Resolution + Factoring + Reordering

\[\inferrule{C_1 \dots C_n \mid C, pol_1,L_1 \dots pol_{n-1},L_{n-1}}{C}\]

where

  • let \(C_1 \dots C_n\) be nodes viewed as clauses, as defined in RESOLUTION

  • let \(C_1 \diamond_{L,\mathit{pol}} C_2\) represent the resolution of \(C_1\) with \(C_2\) with pivot \(L\) and polarity \(pol\), as defined in RESOLUTION

  • let \(C_1'\) be equal, in its set representation, to \(C_1\),

  • for each \(i > 1\), let \(C_i'\) be equal, in its set representation, to \(C_{i-1} \diamond_{L_{i-1},\mathit{pol}_{i-1}} C_i'\)

The result of the chain resolution is \(C\), which is equal, in its set representation, to \(C_n'\) endverbatim

MACRO_RESOLUTION_TRUST

verbatim embed:rst:leading-asterisk Boolean – N-ary Resolution + Factoring + Reordering unchecked

Same as MACRO_RESOLUTION, but not checked by the internal proof checker. endverbatim

MACRO_REWRITE

verbatim embed:rst:leading-asterisk Builtin theory – Rewrite

\[\inferrule{- \mid t, idr}{t = \texttt{rewrite}_{idr}(t)}\]

where \(idr\) is a MethodId identifier, which determines the kind of rewriter to apply, e.g. Rewriter::rewrite. endverbatim

MACRO_SR_EQ_INTRO

verbatim embed:rst:leading-asterisk Builtin theory – Substitution + Rewriting equality introduction

In this rule, we provide a term \(t\) and conclude that it is equal to its rewritten form under a (proven) substitution.

\[\inferrule{F_1 \dots F_n \mid t, (ids (ida (idr)?)?)?}{t = \texttt{rewrite}_{idr}(t \circ \sigma_{ids, ida}(F_n) \circ \cdots \circ \sigma_{ids, ida}(F_1))}\]

In other words, from the point of view of Skolem forms, this rule transforms \(t\) to \(t'\) by standard substitution + rewriting.

The arguments \(ids\), \(ida\) and \(idr\) are optional and specify the identifier of the substitution, the substitution application and rewriter respectively to be used. For details, see theory/builtin/proof_checker.h. endverbatim

MACRO_SR_PRED_ELIM

verbatim embed:rst:leading-asterisk Builtin theory – Substitution + Rewriting predicate elimination

\[\inferrule{F, F_1 \dots F_n \mid (ids (ida (idr)?)?)?}{\texttt{rewrite}_{idr}(F \circ \sigma_{ids, ida}(F_n) \circ \cdots \circ \sigma_{ids, ida}(F_1))}\]

where \(ids\) and \(idr\) are method identifiers.

We rewrite only on the Skolem form of \(F\), similar to MACRO_SR_EQ_INTRO. endverbatim

MACRO_SR_PRED_INTRO

verbatim embed:rst:leading-asterisk Builtin theory – Substitution + Rewriting predicate introduction

In this rule, we provide a formula \(F\) and conclude it, under the condition that it rewrites to true under a proven substitution.

\[\inferrule{F_1 \dots F_n \mid F, (ids (ida (idr)?)?)?}{F}\]

where \(\texttt{rewrite}_{idr}(F \circ \sigma_{ids, ida}(F_n) \circ \cdots \circ \sigma_{ids, ida}(F_1)) = \top\) and \(ids\) and \(idr\) are method identifiers.

More generally, this rule also holds when \(\texttt{Rewriter::rewrite}(\texttt{toOriginal}(F')) = \top\) where \(F'\) is the result of the left hand side of the equality above. Here, notice that we apply rewriting on the original form of \(F'\), meaning that this rule may conclude an \(F\) whose Skolem form is justified by the definition of its (fresh) Skolem variables. For example, this rule may justify the conclusion \(k = t\) where \(k\) is the purification Skolem for \(t\), e.g. where the original form of \(k\) is \(t\).

Furthermore, notice that the rewriting and substitution is applied only within the side condition, meaning the rewritten form of the original form of \(F\) does not escape this rule. endverbatim

MACRO_SR_PRED_TRANSFORM

verbatim embed:rst:leading-asterisk Builtin theory – Substitution + Rewriting predicate elimination

\[\inferrule{F, F_1 \dots F_n \mid G, (ids (ida (idr)?)?)?}{G}\]

where

\[\begin{split}\texttt{rewrite}_{idr}(F \circ \sigma_{ids, ida}(F_n) \circ\cdots \circ \sigma_{ids, ida}(F_1)) =\\ \texttt{rewrite}_{idr}(G \circ \sigma_{ids, ida}(F_n) \circ \cdots \circ \sigma_{ids, ida}(F_1))\end{split}\]

More generally, this rule also holds when: \(\texttt{Rewriter::rewrite}(\texttt{toOriginal}(F')) = \texttt{Rewriter::rewrite}(\texttt{toOriginal}(G'))\) where \(F'\) and \(G'\) are the result of each side of the equation above. Here, original forms are used in a similar manner to MACRO_SR_PRED_INTRO above. endverbatim

MACRO_STRING_INFERENCE

verbatim embed:rst:leading-asterisk Strings – (Macro) String inference

\[\inferrule{?\mid F,\mathit{id},\mathit{isRev},\mathit{exp}}{F}\]

used to bookkeep an inference that has not yet been converted via \(\texttt{strings::InferProofCons::convert}\). endverbatim

MODUS_PONENS

verbatim embed:rst:leading-asterisk Boolean – Modus Ponens

\[\inferrule{F_1, (F_1 \rightarrow F_2) \mid -}{F_2}\]

Note this can optionally be seen as a macro for IMPLIES_ELIM + RESOLUTION. endverbatim

NARY_CONG

verbatim embed:rst:leading-asterisk Equality – N-ary Congruence

\[\inferrule{t_1=s_1,\dots,t_n=s_n\mid k}{k(t_1,\dots, t_n) = k(s_1,\dots, s_n)}\]

where \(k\) is the application kind. The actual node for \(k\) is constructible via ProofRuleChecker::mkKindNode. This rule is used for kinds that have variadic arity, such as cvc5::Kind::AND, cvc5::Kind::PLUS and so on. endverbatim

NOT_AND

verbatim embed:rst:leading-asterisk Boolean – De Morgan – Not And

\[\inferrule{\neg(F_1 \land \dots \land F_n) \mid -}{\neg F_1 \lor \dots \lor \neg F_n}\]

endverbatim

NOT_EQUIV_ELIM1

verbatim embed:rst:leading-asterisk Boolean – Not Equivalence elimination version 1

\[\inferrule{F_1 \neq F_2 \mid -}{F_1 \lor F_2}\]

endverbatim

NOT_EQUIV_ELIM2

verbatim embed:rst:leading-asterisk Boolean – Not Equivalence elimination version 2

\[\inferrule{F_1 \neq F_2 \mid -}{\neg F_1 \lor \neg F_2}\]

endverbatim

NOT_IMPLIES_ELIM1

verbatim embed:rst:leading-asterisk Boolean – Not Implication elimination version 1

\[\inferrule{\neg(F_1 \rightarrow F_2) \mid -}{F_1}\]

endverbatim

NOT_IMPLIES_ELIM2

verbatim embed:rst:leading-asterisk Boolean – Not Implication elimination version 2

\[\inferrule{\neg(F_1 \rightarrow F_2) \mid -}{\neg F_2}\]

endverbatim

NOT_ITE_ELIM1

verbatim embed:rst:leading-asterisk Boolean – Not ITE elimination version 1

\[\inferrule{\neg(\ite{C}{F_1}{F_2}) \mid -}{\neg C \lor \neg F_1}\]

endverbatim

NOT_ITE_ELIM2

verbatim embed:rst:leading-asterisk Boolean – Not ITE elimination version 2

\[\inferrule{\neg(\ite{C}{F_1}{F_2}) \mid -}{C \lor \neg F_2}\]

endverbatim

NOT_NOT_ELIM

verbatim embed:rst:leading-asterisk Boolean – Double negation elimination

\[\inferrule{\neg (\neg F) \mid -}{F}\]

endverbatim

NOT_OR_ELIM

verbatim embed:rst:leading-asterisk Boolean – Not Or elimination

\[\inferrule{\neg(F_1 \lor \dots \lor F_n) \mid i}{\neg F_i}\]

endverbatim

NOT_XOR_ELIM1

verbatim embed:rst:leading-asterisk Boolean – Not XOR elimination version 1

\[\inferrule{\neg(F_1 \xor F_2) \mid -}{F_1 \lor \neg F_2}\]

endverbatim

NOT_XOR_ELIM2

verbatim embed:rst:leading-asterisk Boolean – Not XOR elimination version 2

\[\inferrule{\neg(F_1 \xor F_2) \mid -}{\neg F_1 \lor F_2}\]

endverbatim

QUANT_VAR_REORDERING

verbatim embed:rst:leading-asterisk Quantifiers – Variable reordering

\[\inferrule{-\mid (\forall X.\> F) = (\forall Y.\> F)} {(\forall X.\> F) = (\forall Y.\> F)}\]

where \(Y\) is a reordering of \(X\).

endverbatim

REFL

verbatim embed:rst:leading-asterisk Equality – Reflexivity

\[\inferrule{-\mid t}{t = t}\]

endverbatim

REORDERING

verbatim embed:rst:leading-asterisk Boolean – Reordering

\[\inferrule{C_1 \mid C_2}{C_2}\]

where the multiset representations of \(C_1\) and \(C_2\) are the same. endverbatim

RESOLUTION

verbatim embed:rst:leading-asterisk Boolean – Resolution

\[\inferrule{C_1, C_2 \mid pol, L}{C}\]

where

  • \(C_1\) and \(C_2\) are nodes viewed as clauses, i.e., either an OR node with each children viewed as a literal or a node viewed as a literal. Note that an OR node could also be a literal.

  • \(pol\) is either true or false, representing the polarity of the pivot on the first clause

  • \(L\) is the pivot of the resolution, which occurs as is (resp. under a NOT) in \(C_1\) and negatively (as is) in \(C_2\) if \(pol = \top\) (\(pol = \bot\)).

\(C\) is a clause resulting from collecting all the literals in \(C_1\), minus the first occurrence of the pivot or its negation, and \(C_2\), minus the first occurrence of the pivot or its negation, according to the policy above. If the resulting clause has a single literal, that literal itself is the result; if it has no literals, then the result is false; otherwise it’s an OR node of the resulting literals.

Note that it may be the case that the pivot does not occur in the clauses. In this case the rule is not unsound, but it does not correspond to resolution but rather to a weakening of the clause that did not have a literal eliminated. endverbatim

RE_INTER

verbatim embed:rst:leading-asterisk Strings – Regular expressions – Intersection

\[\inferrule{t\in R_1,\,t\in R_2\mid -}{t\in \mathit{re.inter}(R_1,R_2)}\]

endverbatim

RE_UNFOLD_NEG

verbatim embed:rst:leading-asterisk Strings – Regular expressions – Negative Unfold

\[\inferrule{t \not \in \mathit{re}.\text{*}(R) \mid -}{t \neq \ \epsilon \ \wedge \forall L. L \leq 0 \vee \mathit{str.len}(t) < L \vee \mathit{pre}(t, L) \not \in R \vee \mathit{suf}(t, L) \not \in \mathit{re}.\text{*}(R)}\]

Or alternatively for regular expression concatenation:

\[\inferrule{t \not \in \mathit{re}.\text{++}(R_1, \ldots, R_n)\mid -}{\forall L. L < 0 \vee \mathit{str.len}(t) < L \vee \mathit{pre}(t, L) \not \in R_1 \vee \mathit{suf}(t, L) \not \in \mathit{re}.\text{++}(R_2, \ldots, R_n)}\]

Note that in either case the varaible \(L\) has type \(Int\) and name “@var.str_index”.

endverbatim

RE_UNFOLD_NEG_CONCAT_FIXED

verbatim embed:rst:leading-asterisk Strings – Regular expressions – Unfold negative concatenation, fixed

\[ \inferrule{t\not\in \mathit{re}.\text{re.++}(r_1, \ldots, r_n) \mid \bot}{ \mathit{pre}(t, L) \not \in r_1 \vee \mathit{suf}(t, L) \not \in \mathit{re}.\text{re.++}(r_2, \ldots, r_n)}\]

where \(r_1\) has fixed length \(L\).

or alternatively for the reverse:

\[\inferrule{t \not \in \mathit{re}.\text{re.++}(r_1, \ldots, r_n) \mid \top}{ \mathit{suf}(t, str.len(t) - L) \not \in r_n \vee \mathit{pre}(t, str.len(t) - L) \not \in \mathit{re}.\text{re.++}(r_1, \ldots, r_{n-1})}\]

where \(r_n\) has fixed length \(L\).

endverbatim

RE_UNFOLD_POS

verbatim embed:rst:leading-asterisk Strings – Regular expressions – Positive Unfold

\[\inferrule{t\in R\mid -}{F}\]

where \(F\) corresponds to the one-step unfolding of the premise. This is implemented by \(\texttt{RegExpOpr::reduceRegExpPos}(t\in R)\). endverbatim

SAT_EXTERNAL_PROVE

verbatim embed:rst:leading-asterisk SAT external prove Refutation

\[\inferrule{F_1 \dots F_n \mid D}{\bot}\]

where \(F_1 \dots F_n\) correspond to the input clauses in the DIMACS file D. endverbatim

SAT_REFUTATION

verbatim embed:rst:leading-asterisk SAT Refutation for assumption-based unsat cores

\[\inferrule{F_1 \dots F_n \mid -}{\bot}\]

where \(F_1 \dots F_n\) correspond to the unsat core determined by the SAT solver. endverbatim

SCOPE

verbatim embed:rst:leading-asterisk Scope (a binder for assumptions)

\[\inferruleSC{F \mid F_1 \dots F_n}{(F_1 \land \dots \land F_n) \Rightarrow F}{if $F\neq\bot$} \textrm{ or } \inferruleSC{F \mid F_1 \dots F_n}{\neg (F_1 \land \dots \land F_n)}{if $F=\bot$}\]

This rule has a dual purpose with ASSUME. It is a way to close assumptions in a proof. We require that \(F_1 \dots F_n\) are free assumptions in P and say that \(F_1 \dots F_n\) are not free in (SCOPE P). In other words, they are bound by this application. For example, the proof node: (SCOPE (ASSUME F) :args F) has the conclusion \(F \Rightarrow F\) and has no free assumptions. More generally, a proof with no free assumptions always concludes a valid formula. endverbatim

SETS_EXT

verbatim embed:rst:leading-asterisk Sets – Sets extensionality

\[\inferrule{a \neq b\mid -} {\mathit{set.member}(k,a)\neq\mathit{set.member}(k,b)}\]

where \(k\) is the \(\texttt{SETS_DEQ_DIFF}\) skolem for (a, b). endverbatim

SETS_FILTER_DOWN

verbatim embed:rst:leading-asterisk Sets – Sets filter down

\[\inferrule{\mathit{set.member}(x,\mathit{set.filter}(P, a))\mid -} {\mathit{set.member}(x,a) \wedge P(x)}\]

endverbatim

SETS_FILTER_UP

verbatim embed:rst:leading-asterisk Sets – Sets filter up

\[\inferrule{\mathit{set.member}(x,a)\mid P} {\mathit{set.member}(x, \mathit{set.filter}(P, a)) = P(x)}\]

endverbatim

SETS_SINGLETON_INJ

verbatim embed:rst:leading-asterisk Sets – Singleton injectivity

\[\inferrule{\mathit{set.singleton}(t) = \mathit{set.singleton}(s)\mid -}{t=s}\]

endverbatim

SKOLEMIZE

verbatim embed:rst:leading-asterisk Quantifiers – Skolemization

\[\inferrule{\neg (\forall x_1\dots x_n.\> F)\mid -}{\neg F\sigma}\]

where \(\sigma\) maps \(x_1,\dots,x_n\) to their representative skolems, which are skolems \(k_1,\dots,k_n\). For each \(k_i\), its skolem identifier is QUANTIFIERS_SKOLEMIZE, and its indices are \((\forall x_1\dots x_n.\> F)\) and \(x_i\). endverbatim

SKOLEM_INTRO

verbatim embed:rst:leading-asterisk Quantifiers – Skolem introduction

\[\inferrule{-\mid k}{k = t}\]

where \(t\) is the unpurified form of skolem \(k\). endverbatim

SPLIT

verbatim embed:rst:leading-asterisk Boolean – Split

\[\inferrule{- \mid F}{F \lor \neg F}\]

endverbatim

STRING_CODE_INJ

verbatim embed:rst:leading-asterisk Strings – Code points

\[\inferrule{-\mid t,s}{\mathit{to\_code}(t) = -1 \vee \mathit{to\_code}(t) \neq \mathit{to\_code}(s) \vee t = s}\]

endverbatim

STRING_DECOMPOSE

verbatim embed:rst:leading-asterisk Strings – Core rules – String decomposition

\[\inferrule{\mathit{len}(t) \geq n\mid \bot}{t = w_1\cdot w_2 \wedge \mathit{len}(w_1) = n}\]

where \(w_1\) is the purification skolem for \(\mathit{pre}(t,n)\) and \(w_2\) is the purification skolem for \(\mathit{suf}(t,n)\). Or alternatively for the reverse:

\[\inferrule{\mathit{len}(t) \geq n\mid \top}{t = w_1\cdot w_2 \wedge \mathit{len}(w_2) = n}\]

where \(w_1\) is the purification skolem for \(\mathit{pre}(t,n)\) and \(w_2\) is the purification skolem for \(\mathit{suf}(t,n)\). endverbatim

STRING_EAGER_REDUCTION

verbatim embed:rst:leading-asterisk Strings – Extended functions – Eager reduction

\[\inferrule{-\mid t}{R}\]

where \(R\) is \(\texttt{TermRegistry::eagerReduce}(t)\). For details, see theory/strings/term_registry.h. endverbatim

STRING_EXT

verbatim embed:rst:leading-asterisk Strings – Extensionality

\[\inferrule{s \neq t\mid -} {\mathit{seq.len}(s) \neq \mathit{seq.len}(t) \vee (\mathit{seq.nth}(s,k)\neq\mathit{set.nth}(t,k) \wedge 0 \leq k \wedge k < \mathit{seq.len}(s))}\]

where \(s,t\) are terms of sequence type, \(k\) is the \(\texttt{STRINGS_DEQ_DIFF}\) skolem for \(s,t\). Alternatively, if \(s,t\) are terms of string type, we use \(\mathit{seq.substr}(s,k,1)\) instead of \(\mathit{seq.nth}(s,k)\) and similarly for \(t\).

endverbatim

STRING_LENGTH_NON_EMPTY

verbatim embed:rst:leading-asterisk Strings – Core rules – Length non-empty

\[\inferrule{t\neq \epsilon\mid -}{\mathit{len}(t) \neq 0}\]

endverbatim

STRING_LENGTH_POS

verbatim embed:rst:leading-asterisk Strings – Core rules – Length positive

\[\inferrule{-\mid t}{(\mathit{len}(t) = 0\wedge t= \epsilon)\vee \mathit{len}(t) > 0}\]

endverbatim

STRING_REDUCTION

verbatim embed:rst:leading-asterisk Strings – Extended functions – Reduction

\[\inferrule{-\mid t}{R\wedge t = w}\]

where \(w\) is \(\texttt{StringsPreprocess::reduce}(t, R, \dots)\). For details, see theory/strings/theory_strings_preprocess.h. In other words, \(R\) is the reduction predicate for extended term \(t\), and \(w\) is the purification skolem for \(t\).

Notice that the free variables of \(R\) are \(w\) and the free variables of \(t\). endverbatim

STRING_SEQ_UNIT_INJ

verbatim embed:rst:leading-asterisk Strings – Sequence unit

\[\inferrule{\mathit{unit}(x) = \mathit{unit}(y)\mid -}{x = y}\]

Also applies to the case where \(\mathit{unit}(y)\) is a constant sequence of length one. endverbatim

SUBS

verbatim embed:rst:leading-asterisk Builtin theory – Substitution

\[\inferrule{F_1 \dots F_n \mid t, ids?}{t = t \circ \sigma_{ids}(F_n) \circ \cdots \circ \sigma_{ids}(F_1)}\]

where \(\sigma_{ids}(F_i)\) are substitutions, which notice are applied in reverse order. Notice that \(ids\) is a MethodId identifier, which determines how to convert the formulas \(F_1 \dots F_n\) into substitutions. It is an optional argument, where by default the premises are equalities of the form (= x y) and converted into substitutions \(x\mapsto y\). endverbatim

SYMM

verbatim embed:rst:leading-asterisk Equality – Symmetry

\[\inferrule{t_1 = t_2\mid -}{t_2 = t_1}\]

or

\[\inferrule{t_1 \neq t_2\mid -}{t_2 \neq t_1}\]

endverbatim

THEORY_REWRITE

verbatim embed:rst:leading-asterisk Other theory rewrite rules

\[\inferrule{- \mid id, t = t'}{t = t'}\]

where id is the ProofRewriteRule of the theory rewrite rule which transforms \(t\) to \(t'\).

In contrast to DSL_REWRITE, theory rewrite rules used by this proof rule are not necessarily expressible in RARE. Each rule that can be used in this proof rule are documented explicitly in cases within the ProofRewriteRule enum. endverbatim

TRANS

verbatim embed:rst:leading-asterisk Equality – Transitivity

\[\inferrule{t_1=t_2,\dots,t_{n-1}=t_n\mid -}{t_1 = t_n}\]

endverbatim

TRUE_ELIM

verbatim embed:rst:leading-asterisk Equality – True elim

\[\inferrule{F=\top\mid -}{F}\]

endverbatim

TRUE_INTRO

verbatim embed:rst:leading-asterisk Equality – True intro

\[\inferrule{F\mid -}{F = \top}\]

endverbatim

TRUST

verbatim embed:rst:leading-asterisk Trusted rule

\[\inferrule{F_1 \dots F_n \mid tid, F, ...}{F}\]

where \(tid\) is an identifier and \(F\) is a formula. This rule is used when a formal justification of an inference step cannot be provided. The formulas \(F_1 \dots F_n\) refer to a set of formulas that entail \(F\), which may or may not be provided. endverbatim

TRUST_THEORY_REWRITE

verbatim embed:rst:leading-asterisk Trusted rules – Theory rewrite

\[\inferrule{- \mid F, tid, rid}{F}\]

where \(F\) is an equality of the form \(t = t'\) where \(t'\) is obtained by applying the kind of rewriting given by the method identifier \(rid\), which is one of: RW_REWRITE_THEORY_PRE, RW_REWRITE_THEORY_POST, RW_REWRITE_EQ_EXT. Notice that the checker for this rule does not replay the rewrite to ensure correctness, since theory rewriter methods are not static. For example, the quantifiers rewriter involves constructing new bound variables that are not guaranteed to be consistent on each call. endverbatim

UNKNOWN

verbatim embed:rst:leading-asterisk External – Alethe

Place holder for Alethe rules.

\[\inferrule{P_1, \dots, P_n\mid \texttt{id}, Q, Q', A_1,\dots, A_m}{Q}\]

Note that the premises and arguments are arbitrary. It’s expected that \(\texttt{id}\) refer to a proof rule in the external Alethe calculus, and that \(Q'\) be the representation of Q to be printed by the Alethe printer. endverbatim

XOR_ELIM1

verbatim embed:rst:leading-asterisk Boolean – XOR elimination version 1

\[\inferrule{F_1 \xor F_2 \mid -}{F_1 \lor F_2}\]

endverbatim

XOR_ELIM2

verbatim embed:rst:leading-asterisk Boolean – XOR elimination version 2

\[\inferrule{F_1 \xor F_2 \mid -}{\neg F_1 \lor \neg F_2}\]

endverbatim


class cvc5.ProofRewriteRule(value)

The ProofRewriteRule enum

ARITH_ABS_ELIM_INT

Auto-generated from RARE rule arith-abs-elim-int

ARITH_ABS_ELIM_REAL

Auto-generated from RARE rule arith-abs-elim-real

ARITH_ABS_EQ

Auto-generated from RARE rule arith-abs-eq

ARITH_ABS_INT_GT

Auto-generated from RARE rule arith-abs-int-gt

ARITH_ABS_REAL_GT

Auto-generated from RARE rule arith-abs-real-gt

ARITH_COSECENT_ELIM

Auto-generated from RARE rule arith-cosecent-elim

ARITH_COSINE_ELIM

Auto-generated from RARE rule arith-cosine-elim

ARITH_COTANGENT_ELIM

Auto-generated from RARE rule arith-cotangent-elim

ARITH_DIV_ELIM_TO_REAL1

Auto-generated from RARE rule arith-div-elim-to-real1

ARITH_DIV_ELIM_TO_REAL2

Auto-generated from RARE rule arith-div-elim-to-real2

ARITH_DIV_TOTAL_INT

Auto-generated from RARE rule arith-div-total-int

ARITH_DIV_TOTAL_REAL

Auto-generated from RARE rule arith-div-total-real

ARITH_DIV_TOTAL_ZERO_INT

Auto-generated from RARE rule arith-div-total-zero-int

ARITH_DIV_TOTAL_ZERO_REAL

Auto-generated from RARE rule arith-div-total-zero-real

ARITH_ELIM_GT

Auto-generated from RARE rule arith-elim-gt

ARITH_ELIM_INT_GT

Auto-generated from RARE rule arith-elim-int-gt

ARITH_ELIM_INT_LT

Auto-generated from RARE rule arith-elim-int-lt

ARITH_ELIM_LEQ

Auto-generated from RARE rule arith-elim-leq

ARITH_ELIM_LT

Auto-generated from RARE rule arith-elim-lt

ARITH_EQ_ELIM_INT

Auto-generated from RARE rule arith-eq-elim-int

ARITH_EQ_ELIM_REAL

Auto-generated from RARE rule arith-eq-elim-real

ARITH_GEQ_NORM1_INT

Auto-generated from RARE rule arith-geq-norm1-int

ARITH_GEQ_NORM1_REAL

Auto-generated from RARE rule arith-geq-norm1-real

ARITH_GEQ_NORM2

Auto-generated from RARE rule arith-geq-norm2

ARITH_GEQ_TIGHTEN

Auto-generated from RARE rule arith-geq-tighten

ARITH_INT_DIV_TOTAL

Auto-generated from RARE rule arith-int-div-total

ARITH_INT_DIV_TOTAL_ONE

Auto-generated from RARE rule arith-int-div-total-one

ARITH_INT_DIV_TOTAL_ZERO

Auto-generated from RARE rule arith-int-div-total-zero

ARITH_INT_MOD_TOTAL

Auto-generated from RARE rule arith-int-mod-total

ARITH_INT_MOD_TOTAL_ONE

Auto-generated from RARE rule arith-int-mod-total-one

ARITH_INT_MOD_TOTAL_ZERO

Auto-generated from RARE rule arith-int-mod-total-zero

ARITH_LEQ_NORM

Auto-generated from RARE rule arith-leq-norm

ARITH_MULT_DIST

Auto-generated from RARE rule arith-mult-dist

ARITH_MULT_FLATTEN

Auto-generated from RARE rule arith-mult-flatten

ARITH_MUL_ONE

Auto-generated from RARE rule arith-mul-one

ARITH_MUL_ZERO

Auto-generated from RARE rule arith-mul-zero

ARITH_PI_NOT_INT

Auto-generated from RARE rule arith-pi-not-int

ARITH_PLUS_FLATTEN

Auto-generated from RARE rule arith-plus-flatten

ARITH_POW_ELIM

verbatim embed:rst:leading-asterisk Arithmetic – power elimination

\[(x ^ c) = (x \cdot \ldots \cdot x)\]

where \(c\) is a non-negative integer.

endverbatim

ARITH_REFL_GEQ

Auto-generated from RARE rule arith-refl-geq

ARITH_REFL_GT

Auto-generated from RARE rule arith-refl-gt

ARITH_REFL_LEQ

Auto-generated from RARE rule arith-refl-leq

ARITH_REFL_LT

Auto-generated from RARE rule arith-refl-lt

ARITH_SECENT_ELIM

Auto-generated from RARE rule arith-secent-elim

ARITH_SINE_PI2

Auto-generated from RARE rule arith-sine-pi2

ARITH_SINE_ZERO

Auto-generated from RARE rule arith-sine-zero

ARITH_STRING_PRED_ENTAIL

verbatim embed:rst:leading-asterisk 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.

endverbatim

ARITH_STRING_PRED_SAFE_APPROX

verbatim embed:rst:leading-asterisk 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”.

endverbatim

ARITH_TANGENT_ELIM

Auto-generated from RARE rule arith-tangent-elim

ARITH_TO_INT_ELIM_TO_REAL

Auto-generated from RARE rule arith-to-int-elim-to-real

ARITH_TO_REAL_ELIM

Auto-generated from RARE rule arith-to-real-elim

ARRAYS_EQ_RANGE_EXPAND

verbatim embed:rst:leading-asterisk 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)\]

endverbatim

ARRAYS_SELECT_CONST

verbatim embed:rst:leading-asterisk Arrays – Constant array select

\[(select A x) = c\]

where \(A\) is a constant array storing element \(c\).

endverbatim

ARRAY_READ_OVER_WRITE

Auto-generated from RARE rule array-read-over-write

ARRAY_READ_OVER_WRITE2

Auto-generated from RARE rule array-read-over-write2

ARRAY_READ_OVER_WRITE_SPLIT

Auto-generated from RARE rule array-read-over-write-split

ARRAY_STORE_OVERWRITE

Auto-generated from RARE rule array-store-overwrite

ARRAY_STORE_SELF

Auto-generated from RARE rule array-store-self

BETA_REDUCE

verbatim embed:rst:leading-asterisk Equality – Beta reduction

\[((\lambda x_1 \ldots x_n.\> t) \ t_1 \ldots t_n) = t\{x_1 \mapsto t_1, \ldots, x_n \mapsto t_n\}\]

The right hand side of the equality in the conclusion is computed using standard substitution via Node::substitute. endverbatim

BOOL_AND_CONF

Auto-generated from RARE rule bool-and-conf

BOOL_AND_CONF2

Auto-generated from RARE rule bool-and-conf2

BOOL_AND_DE_MORGAN

Auto-generated from RARE rule bool-and-de-morgan

BOOL_AND_FALSE

Auto-generated from RARE rule bool-and-false

BOOL_AND_FLATTEN

Auto-generated from RARE rule bool-and-flatten

BOOL_DOUBLE_NOT_ELIM

Auto-generated from RARE rule bool-double-not-elim

BOOL_EQ_FALSE

Auto-generated from RARE rule bool-eq-false

BOOL_EQ_NREFL

Auto-generated from RARE rule bool-eq-nrefl

BOOL_EQ_TRUE

Auto-generated from RARE rule bool-eq-true

BOOL_IMPLIES_DE_MORGAN

Auto-generated from RARE rule bool-implies-de-morgan

BOOL_IMPL_ELIM

Auto-generated from RARE rule bool-impl-elim

BOOL_IMPL_FALSE1

Auto-generated from RARE rule bool-impl-false1

BOOL_IMPL_FALSE2

Auto-generated from RARE rule bool-impl-false2

BOOL_IMPL_TRUE1

Auto-generated from RARE rule bool-impl-true1

BOOL_IMPL_TRUE2

Auto-generated from RARE rule bool-impl-true2

BOOL_NOT_EQ_ELIM1

Auto-generated from RARE rule bool-not-eq-elim1

BOOL_NOT_EQ_ELIM2

Auto-generated from RARE rule bool-not-eq-elim2

BOOL_NOT_FALSE

Auto-generated from RARE rule bool-not-false

BOOL_NOT_ITE_ELIM

Auto-generated from RARE rule bool-not-ite-elim

BOOL_NOT_TRUE

Auto-generated from RARE rule bool-not-true

BOOL_NOT_XOR_ELIM

Auto-generated from RARE rule bool-not-xor-elim

BOOL_OR_AND_DISTRIB

Auto-generated from RARE rule bool-or-and-distrib

BOOL_OR_DE_MORGAN

Auto-generated from RARE rule bool-or-de-morgan

BOOL_OR_FLATTEN

Auto-generated from RARE rule bool-or-flatten

BOOL_OR_TAUT

Auto-generated from RARE rule bool-or-taut

BOOL_OR_TAUT2

Auto-generated from RARE rule bool-or-taut2

BOOL_OR_TRUE

Auto-generated from RARE rule bool-or-true

BOOL_XOR_COMM

Auto-generated from RARE rule bool-xor-comm

BOOL_XOR_ELIM

Auto-generated from RARE rule bool-xor-elim

BOOL_XOR_FALSE

Auto-generated from RARE rule bool-xor-false

BOOL_XOR_NREFL

Auto-generated from RARE rule bool-xor-nrefl

BOOL_XOR_REFL

Auto-generated from RARE rule bool-xor-refl

BOOL_XOR_TRUE

Auto-generated from RARE rule bool-xor-true

BV_ADD_COMBINE_LIKE_TERMS

verbatim embed:rst:leading-asterisk Bitvectors – Combine like terms during addition by counting terms endverbatim

BV_ADD_TWO

Auto-generated from RARE rule bv-add-two

BV_ADD_ZERO

Auto-generated from RARE rule bv-add-zero

BV_AND_CONCAT_PULLUP

Auto-generated from RARE rule bv-and-concat-pullup

BV_AND_FLATTEN

Auto-generated from RARE rule bv-and-flatten

BV_AND_ONE

Auto-generated from RARE rule bv-and-one

BV_AND_SIMPLIFY_1

Auto-generated from RARE rule bv-and-simplify-1

BV_AND_SIMPLIFY_2

Auto-generated from RARE rule bv-and-simplify-2

BV_AND_ZERO

Auto-generated from RARE rule bv-and-zero

BV_ASHR_BY_CONST_0

Auto-generated from RARE rule bv-ashr-by-const-0

BV_ASHR_BY_CONST_1

Auto-generated from RARE rule bv-ashr-by-const-1

BV_ASHR_BY_CONST_2

Auto-generated from RARE rule bv-ashr-by-const-2

BV_ASHR_ZERO

Auto-generated from RARE rule bv-ashr-zero

BV_BITWISE_IDEMP_1

Auto-generated from RARE rule bv-bitwise-idemp-1

BV_BITWISE_IDEMP_2

Auto-generated from RARE rule bv-bitwise-idemp-2

BV_BITWISE_NOT_AND

Auto-generated from RARE rule bv-bitwise-not-and

BV_BITWISE_NOT_OR

Auto-generated from RARE rule bv-bitwise-not-or

BV_BITWISE_SLICING

verbatim embed:rst:leading-asterisk 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 endverbatim

BV_COMMUTATIVE_ADD

Auto-generated from RARE rule bv-commutative-add

BV_COMMUTATIVE_AND

Auto-generated from RARE rule bv-commutative-and

BV_COMMUTATIVE_MUL

Auto-generated from RARE rule bv-commutative-mul

BV_COMMUTATIVE_OR

Auto-generated from RARE rule bv-commutative-or

BV_COMMUTATIVE_XOR

Auto-generated from RARE rule bv-commutative-xor

BV_COMP_ELIMINATE

Auto-generated from RARE rule bv-comp-eliminate

BV_CONCAT_EXTRACT_MERGE

Auto-generated from RARE rule bv-concat-extract-merge

BV_CONCAT_FLATTEN

Auto-generated from RARE rule bv-concat-flatten

BV_CONCAT_MERGE_CONST

Auto-generated from RARE rule bv-concat-merge-const

BV_CONCAT_TO_MULT

Auto-generated from RARE rule bv-concat-to-mult

BV_EQ_EXTRACT_ELIM1

Auto-generated from RARE rule bv-eq-extract-elim1

BV_EQ_EXTRACT_ELIM2

Auto-generated from RARE rule bv-eq-extract-elim2

BV_EQ_EXTRACT_ELIM3

Auto-generated from RARE rule bv-eq-extract-elim3

BV_EXTRACT_BITWISE_AND

Auto-generated from RARE rule bv-extract-bitwise-and

BV_EXTRACT_BITWISE_OR

Auto-generated from RARE rule bv-extract-bitwise-or

BV_EXTRACT_BITWISE_XOR

Auto-generated from RARE rule bv-extract-bitwise-xor

BV_EXTRACT_CONCAT_1

Auto-generated from RARE rule bv-extract-concat-1

BV_EXTRACT_CONCAT_2

Auto-generated from RARE rule bv-extract-concat-2

BV_EXTRACT_CONCAT_3

Auto-generated from RARE rule bv-extract-concat-3

BV_EXTRACT_CONCAT_4

Auto-generated from RARE rule bv-extract-concat-4

BV_EXTRACT_EXTRACT

Auto-generated from RARE rule bv-extract-extract

BV_EXTRACT_MULT_LEADING_BIT

Auto-generated from RARE rule bv-extract-mult-leading-bit

BV_EXTRACT_NOT

Auto-generated from RARE rule bv-extract-not

BV_EXTRACT_SIGN_EXTEND_1

Auto-generated from RARE rule bv-extract-sign-extend-1

BV_EXTRACT_SIGN_EXTEND_2

Auto-generated from RARE rule bv-extract-sign-extend-2

BV_EXTRACT_SIGN_EXTEND_3

Auto-generated from RARE rule bv-extract-sign-extend-3

BV_EXTRACT_WHOLE

Auto-generated from RARE rule bv-extract-whole

BV_ITE_CONST_CHILDREN_1

Auto-generated from RARE rule bv-ite-const-children-1

BV_ITE_CONST_CHILDREN_2

Auto-generated from RARE rule bv-ite-const-children-2

BV_ITE_EQUAL_CHILDREN

Auto-generated from RARE rule bv-ite-equal-children

BV_ITE_EQUAL_COND_1

Auto-generated from RARE rule bv-ite-equal-cond-1

BV_ITE_EQUAL_COND_2

Auto-generated from RARE rule bv-ite-equal-cond-2

BV_ITE_EQUAL_COND_3

Auto-generated from RARE rule bv-ite-equal-cond-3

BV_ITE_MERGE_ELSE_ELSE

Auto-generated from RARE rule bv-ite-merge-else-else

BV_ITE_MERGE_ELSE_IF

Auto-generated from RARE rule bv-ite-merge-else-if

BV_ITE_MERGE_THEN_ELSE

Auto-generated from RARE rule bv-ite-merge-then-else

BV_ITE_MERGE_THEN_IF

Auto-generated from RARE rule bv-ite-merge-then-if

BV_LSHR_BY_CONST_0

Auto-generated from RARE rule bv-lshr-by-const-0

BV_LSHR_BY_CONST_1

Auto-generated from RARE rule bv-lshr-by-const-1

BV_LSHR_BY_CONST_2

Auto-generated from RARE rule bv-lshr-by-const-2

BV_LSHR_ZERO

Auto-generated from RARE rule bv-lshr-zero

BV_LT_SELF

Auto-generated from RARE rule bv-lt-self

BV_MERGE_SIGN_EXTEND_1

Auto-generated from RARE rule bv-merge-sign-extend-1

BV_MERGE_SIGN_EXTEND_2

Auto-generated from RARE rule bv-merge-sign-extend-2

BV_MERGE_SIGN_EXTEND_3

Auto-generated from RARE rule bv-merge-sign-extend-3

BV_MULT_DISTRIB_1

Auto-generated from RARE rule bv-mult-distrib-1

BV_MULT_DISTRIB_2

Auto-generated from RARE rule bv-mult-distrib-2

BV_MULT_DISTRIB_CONST_ADD

Auto-generated from RARE rule bv-mult-distrib-const-add

BV_MULT_DISTRIB_CONST_NEG

Auto-generated from RARE rule bv-mult-distrib-const-neg

BV_MULT_DISTRIB_CONST_SUB

Auto-generated from RARE rule bv-mult-distrib-const-sub

BV_MULT_POW2_1

Auto-generated from RARE rule bv-mult-pow2-1

BV_MULT_POW2_2

Auto-generated from RARE rule bv-mult-pow2-2

BV_MULT_POW2_2B

Auto-generated from RARE rule bv-mult-pow2-2b

BV_MULT_SIMPLIFY

verbatim embed:rst:leading-asterisk Bitvectors – Extract negations from multiplicands

\[bvmul(bvneg(a),\ b,\ c) = bvneg(bvmul(a,\ b,\ c))\]

endverbatim

BV_MULT_SLT_MULT_1

Auto-generated from RARE rule bv-mult-slt-mult-1

BV_MULT_SLT_MULT_2

Auto-generated from RARE rule bv-mult-slt-mult-2

BV_MUL_FLATTEN

Auto-generated from RARE rule bv-mul-flatten

BV_MUL_ONE

Auto-generated from RARE rule bv-mul-one

BV_MUL_ZERO

Auto-generated from RARE rule bv-mul-zero

BV_NAND_ELIMINATE

Auto-generated from RARE rule bv-nand-eliminate

BV_NEG_ADD

Auto-generated from RARE rule bv-neg-add

BV_NEG_IDEMP

Auto-generated from RARE rule bv-neg-idemp

BV_NEG_MULT

Auto-generated from RARE rule bv-neg-mult

BV_NEG_SUB

Auto-generated from RARE rule bv-neg-sub

BV_NOR_ELIMINATE

Auto-generated from RARE rule bv-nor-eliminate

BV_NOT_IDEMP

Auto-generated from RARE rule bv-not-idemp

BV_NOT_NEQ

Auto-generated from RARE rule bv-not-neq

BV_NOT_SLE

Auto-generated from RARE rule bv-not-sle

BV_NOT_ULE

Auto-generated from RARE rule bv-not-ule

BV_NOT_ULT

Auto-generated from RARE rule bv-not-ult

BV_NOT_XOR

Auto-generated from RARE rule bv-not-xor

BV_OR_CONCAT_PULLUP

Auto-generated from RARE rule bv-or-concat-pullup

BV_OR_FLATTEN

Auto-generated from RARE rule bv-or-flatten

BV_OR_ONE

Auto-generated from RARE rule bv-or-one

BV_OR_SIMPLIFY_1

Auto-generated from RARE rule bv-or-simplify-1

BV_OR_SIMPLIFY_2

Auto-generated from RARE rule bv-or-simplify-2

BV_OR_ZERO

Auto-generated from RARE rule bv-or-zero

BV_REDAND_ELIMINATE

Auto-generated from RARE rule bv-redand-eliminate

BV_REDOR_ELIMINATE

Auto-generated from RARE rule bv-redor-eliminate

BV_REPEAT_ELIM

verbatim embed:rst:leading-asterisk Bitvectors – Extract continuous substrings of bitvectors

\[repeat(n,\ t) = concat(t ... t)\]

where \(t\) is repeated \(n\) times. endverbatim

BV_ROTATE_LEFT_ELIMINATE_1

Auto-generated from RARE rule bv-rotate-left-eliminate-1

BV_ROTATE_LEFT_ELIMINATE_2

Auto-generated from RARE rule bv-rotate-left-eliminate-2

BV_ROTATE_RIGHT_ELIMINATE_1

Auto-generated from RARE rule bv-rotate-right-eliminate-1

BV_ROTATE_RIGHT_ELIMINATE_2

Auto-generated from RARE rule bv-rotate-right-eliminate-2

BV_SADDO_ELIMINATE

Auto-generated from RARE rule bv-saddo-eliminate

BV_SDIVO_ELIMINATE

Auto-generated from RARE rule bv-sdivo-eliminate

BV_SDIV_ELIMINATE

Auto-generated from RARE rule bv-sdiv-eliminate

BV_SDIV_ELIMINATE_FEWER_BITWISE_OPS

Auto-generated from RARE rule bv-sdiv-eliminate-fewer-bitwise-ops

BV_SGE_ELIMINATE

Auto-generated from RARE rule bv-sge-eliminate

BV_SGT_ELIMINATE

Auto-generated from RARE rule bv-sgt-eliminate

BV_SHL_BY_CONST_0

Auto-generated from RARE rule bv-shl-by-const-0

BV_SHL_BY_CONST_1

Auto-generated from RARE rule bv-shl-by-const-1

BV_SHL_BY_CONST_2

Auto-generated from RARE rule bv-shl-by-const-2

BV_SHL_ZERO

Auto-generated from RARE rule bv-shl-zero

BV_SIGN_EXTEND_ELIMINATE

Auto-generated from RARE rule bv-sign-extend-eliminate

BV_SIGN_EXTEND_ELIMINATE_0

Auto-generated from RARE rule bv-sign-extend-eliminate-0

BV_SIGN_EXTEND_EQ_CONST_1

Auto-generated from RARE rule bv-sign-extend-eq-const-1

BV_SIGN_EXTEND_EQ_CONST_2

Auto-generated from RARE rule bv-sign-extend-eq-const-2

BV_SIGN_EXTEND_ULT_CONST_1

Auto-generated from RARE rule bv-sign-extend-ult-const-1

BV_SIGN_EXTEND_ULT_CONST_2

Auto-generated from RARE rule bv-sign-extend-ult-const-2

BV_SIGN_EXTEND_ULT_CONST_3

Auto-generated from RARE rule bv-sign-extend-ult-const-3

BV_SIGN_EXTEND_ULT_CONST_4

Auto-generated from RARE rule bv-sign-extend-ult-const-4

BV_SLE_ELIMINATE

Auto-generated from RARE rule bv-sle-eliminate

BV_SLE_SELF

Auto-generated from RARE rule bv-sle-self

BV_SLT_ELIMINATE

Auto-generated from RARE rule bv-slt-eliminate

BV_SLT_ZERO

Auto-generated from RARE rule bv-slt-zero

BV_SMOD_ELIMINATE

Auto-generated from RARE rule bv-smod-eliminate

BV_SMOD_ELIMINATE_FEWER_BITWISE_OPS

Auto-generated from RARE rule bv-smod-eliminate-fewer-bitwise-ops

BV_SMULO_ELIMINATE

verbatim embed:rst:leading-asterisk Bitvectors – Unsigned multiplication overflow detection elimination

See M.Gok, M.J. Schulte, P.I. Balzola, “Efficient integer multiplication overflow detection circuits”, 2001. http: endverbatim

BV_SREM_ELIMINATE

Auto-generated from RARE rule bv-srem-eliminate

BV_SREM_ELIMINATE_FEWER_BITWISE_OPS

Auto-generated from RARE rule bv-srem-eliminate-fewer-bitwise-ops

BV_SSUBO_ELIMINATE

Auto-generated from RARE rule bv-ssubo-eliminate

BV_SUB_ELIMINATE

Auto-generated from RARE rule bv-sub-eliminate

BV_TO_NAT_ELIM

verbatim embed:rst:leading-asterisk 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)\).

endverbatim

BV_UADDO_ELIMINATE

Auto-generated from RARE rule bv-uaddo-eliminate

BV_UDIV_ONE

Auto-generated from RARE rule bv-udiv-one

BV_UDIV_POW2_NOT_ONE

Auto-generated from RARE rule bv-udiv-pow2-not-one

BV_UDIV_ZERO

Auto-generated from RARE rule bv-udiv-zero

BV_UGE_ELIMINATE

Auto-generated from RARE rule bv-uge-eliminate

BV_UGT_ELIMINATE

Auto-generated from RARE rule bv-ugt-eliminate

BV_UGT_UREM

Auto-generated from RARE rule bv-ugt-urem

BV_ULE_ELIMINATE

Auto-generated from RARE rule bv-ule-eliminate

BV_ULE_MAX

Auto-generated from RARE rule bv-ule-max

BV_ULE_SELF

Auto-generated from RARE rule bv-ule-self

BV_ULE_ZERO

Auto-generated from RARE rule bv-ule-zero

BV_ULT_ADD_ONE

Auto-generated from RARE rule bv-ult-add-one

BV_ULT_ONE

Auto-generated from RARE rule bv-ult-one

BV_ULT_ONES

Auto-generated from RARE rule bv-ult-ones

BV_ULT_SELF

Auto-generated from RARE rule bv-ult-self

BV_ULT_ZERO_1

Auto-generated from RARE rule bv-ult-zero-1

BV_ULT_ZERO_2

Auto-generated from RARE rule bv-ult-zero-2

BV_UMULO_ELIMINATE

verbatim embed:rst:leading-asterisk Bitvectors – Unsigned multiplication overflow detection elimination

See M.Gok, M.J. Schulte, P.I. Balzola, “Efficient integer multiplication overflow detection circuits”, 2001. http: endverbatim

BV_UREM_ONE

Auto-generated from RARE rule bv-urem-one

BV_UREM_POW2_NOT_ONE

Auto-generated from RARE rule bv-urem-pow2-not-one

BV_UREM_SELF

Auto-generated from RARE rule bv-urem-self

BV_USUBO_ELIMINATE

Auto-generated from RARE rule bv-usubo-eliminate

BV_XNOR_ELIMINATE

Auto-generated from RARE rule bv-xnor-eliminate

BV_XOR_CONCAT_PULLUP

Auto-generated from RARE rule bv-xor-concat-pullup

BV_XOR_DUPLICATE

Auto-generated from RARE rule bv-xor-duplicate

BV_XOR_FLATTEN

Auto-generated from RARE rule bv-xor-flatten

BV_XOR_NOT

Auto-generated from RARE rule bv-xor-not

BV_XOR_ONES

Auto-generated from RARE rule bv-xor-ones

BV_XOR_SIMPLIFY_1

Auto-generated from RARE rule bv-xor-simplify-1

BV_XOR_SIMPLIFY_2

Auto-generated from RARE rule bv-xor-simplify-2

BV_XOR_SIMPLIFY_3

Auto-generated from RARE rule bv-xor-simplify-3

BV_XOR_ZERO

Auto-generated from RARE rule bv-xor-zero

BV_ZERO_EXTEND_ELIMINATE

Auto-generated from RARE rule bv-zero-extend-eliminate

BV_ZERO_EXTEND_ELIMINATE_0

Auto-generated from RARE rule bv-zero-extend-eliminate-0

BV_ZERO_EXTEND_EQ_CONST_1

Auto-generated from RARE rule bv-zero-extend-eq-const-1

BV_ZERO_EXTEND_EQ_CONST_2

Auto-generated from RARE rule bv-zero-extend-eq-const-2

BV_ZERO_ULE

Auto-generated from RARE rule bv-zero-ule

DISTINCT_BINARY_ELIM

Auto-generated from RARE rule distinct-binary-elim

DISTINCT_CARD_CONFLICT

verbatim embed:rst:leading-asterisk 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\).

endverbatim

DISTINCT_ELIM

verbatim embed:rst:leading-asterisk 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\)

endverbatim

DT_COLLAPSE_SELECTOR

verbatim embed:rst:leading-asterisk Datatypes – collapse selector

\[s_i(c(t_1, \ldots, t_n)) = t_i\]

where \(s_i\) is the \(i^{th}\) selector for constructor \(c\).

endverbatim

DT_COLLAPSE_TESTER

verbatim embed:rst:leading-asterisk 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.

endverbatim

DT_COLLAPSE_TESTER_SINGLETON

verbatim embed:rst:leading-asterisk Datatypes – collapse tester

\[\mathit{is}_c(t) = true\]

where \(c\) is the only constructor of its associated datatype.

endverbatim

DT_COLLAPSE_UPDATER

verbatim embed:rst:leading-asterisk 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.

endverbatim

DT_CONS_EQ

verbatim embed:rst:leading-asterisk Datatypes – constructor equality

\[(c(t_1, \ldots, t_n) = c(s_1, \ldots, s_n)) = (t_1 = s_1 \wedge \ldots \wedge t_n = s_n)\]

or alternatively

\[(c(t_1, \ldots, t_n) = d(s_1, \ldots, s_m)) = false\]

where \(c\) and \(d\) are distinct constructors.

endverbatim

DT_CYCLE

verbatim embed:rst:leading-asterisk 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.

endverbatim

DT_INST

verbatim embed:rst:leading-asterisk 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\). endverbatim

DT_MATCH_ELIM

verbatim embed:rst:leading-asterisk 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.

endverbatim

DT_UPDATER_ELIM

verbatim embed:rst:leading-asterisk 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\).

endverbatim

EQ_COND_DEQ

Auto-generated from RARE rule eq-cond-deq

EQ_ITE_LIFT

Auto-generated from RARE rule eq-ite-lift

EQ_REFL

Auto-generated from RARE rule eq-refl

EQ_SYMM

Auto-generated from RARE rule eq-symm

EXISTS_ELIM

verbatim embed:rst:leading-asterisk Quantifiers – Exists elimination

\[\exists x_1\dots x_n.\> F = \neg \forall x_1\dots x_n.\> \neg F\]

endverbatim

INT_TO_BV_ELIM

verbatim embed:rst:leading-asterisk 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)\).

endverbatim

ITE_ELSE_FALSE

Auto-generated from RARE rule ite-else-false

ITE_ELSE_LOOKAHEAD

Auto-generated from RARE rule ite-else-lookahead

ITE_ELSE_LOOKAHEAD_NOT_SELF

Auto-generated from RARE rule ite-else-lookahead-not-self

ITE_ELSE_LOOKAHEAD_SELF

Auto-generated from RARE rule ite-else-lookahead-self

ITE_ELSE_NEG_LOOKAHEAD

Auto-generated from RARE rule ite-else-neg-lookahead

ITE_ELSE_TRUE

Auto-generated from RARE rule ite-else-true

ITE_EQ_BRANCH

Auto-generated from RARE rule ite-eq-branch

ITE_EXPAND

Auto-generated from RARE rule ite-expand

ITE_FALSE_COND

Auto-generated from RARE rule ite-false-cond

ITE_NEG_BRANCH

Auto-generated from RARE rule ite-neg-branch

ITE_NOT_COND

Auto-generated from RARE rule ite-not-cond

ITE_THEN_FALSE

Auto-generated from RARE rule ite-then-false

ITE_THEN_LOOKAHEAD

Auto-generated from RARE rule ite-then-lookahead

ITE_THEN_LOOKAHEAD_NOT_SELF

Auto-generated from RARE rule ite-then-lookahead-not-self

ITE_THEN_LOOKAHEAD_SELF

Auto-generated from RARE rule ite-then-lookahead-self

ITE_THEN_NEG_LOOKAHEAD

Auto-generated from RARE rule ite-then-neg-lookahead

ITE_THEN_TRUE

Auto-generated from RARE rule ite-then-true

ITE_TRUE_COND

Auto-generated from RARE rule ite-true-cond

LAMBDA_ELIM

verbatim embed:rst:leading-asterisk Equality – Lambda elimination

\[(\lambda x_1 \ldots x_n.\> f(x_1 \ldots x_n)) = f\]

endverbatim

MACRO_ARITH_STRING_PRED_ENTAIL

verbatim embed:rst:leading-asterisk Arithmetic – strings predicate entailment

\[(= s t) = c\]
\[(>= s t) = c\]

where \(c\) is a Boolean constant. This macro is elaborated by applications of EVALUATE, ARITH_POLY_NORM, ARITH_STRING_PRED_ENTAIL, ARITH_STRING_PRED_SAFE_APPROX, as well as other rewrites for normalizing arithmetic predicates.

endverbatim

MACRO_BOOL_NNF_NORM

verbatim embed:rst:leading-asterisk 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.

endverbatim

MACRO_QUANT_MERGE_PRENEX

verbatim embed:rst:leading-asterisk 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\).

endverbatim

MACRO_QUANT_MINISCOPE

verbatim embed:rst:leading-asterisk 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\).

endverbatim

MACRO_QUANT_PARTITION_CONNECTED_FV

verbatim embed:rst:leading-asterisk 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\). endverbatim

MACRO_QUANT_PRENEX

verbatim embed:rst:leading-asterisk 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)\]

endverbatim

MACRO_QUANT_REWRITE_BODY

verbatim embed:rst:leading-asterisk Quantifiers – Macro quantifiers rewrite body

\[\forall X.\> F = \forall X.\> G\]

where \(G\) is semantically equivalent to \(F\).

endverbatim

MACRO_QUANT_VAR_ELIM_EQ

verbatim embed:rst:leading-asterisk Quantifiers – Macro variable elimination equality

\[\forall x Y.\> F = \forall Y.\> F \{ x \mapsto t \}\]

where \(\neg F\) entails \(x = t\).

endverbatim

MACRO_QUANT_VAR_ELIM_INEQ

verbatim embed:rst:leading-asterisk 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\).

endverbatim

MACRO_SUBSTR_STRIP_SYM_LENGTH

verbatim embed:rst:leading-asterisk 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\).

endverbatim

NONE

verbatim embed:rst:leading-asterisk 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 proof rule and the THEORY_REWRITE proof rule. endverbatim

QUANT_DT_SPLIT

verbatim embed:rst:leading-asterisk 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) \}\).

endverbatim

QUANT_MERGE_PRENEX

verbatim embed:rst:leading-asterisk 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.

endverbatim

QUANT_MINISCOPE

verbatim embed:rst:leading-asterisk Quantifiers – Miniscoping

\[\forall X.\> F_1 \wedge \ldots \wedge F_n = (\forall X.\> F_1) \wedge \ldots \wedge (\forall X.\> F_n)\]

endverbatim

QUANT_MINISCOPE_FV

verbatim embed:rst:leading-asterisk Quantifiers – Miniscoping free variables

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

endverbatim

QUANT_UNUSED_VARS

verbatim embed:rst:leading-asterisk 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.

endverbatim

QUANT_VAR_ELIM_EQ

verbatim embed:rst:leading-asterisk Quantifiers – Macro variable elimination equality

\[(\forall x.\> x \neq t \vee F) = F \{ x \mapsto t \}\]

or alternatively

\[(\forall x.\> x \neq t) = \bot\]

endverbatim

RE_ALL_ELIM

Auto-generated from RARE rule re-all-elim

RE_CONCAT_EMP

Auto-generated from RARE rule re-concat-emp

RE_CONCAT_FLATTEN

Auto-generated from RARE rule re-concat-flatten

RE_CONCAT_MERGE

Auto-generated from RARE rule re-concat-merge

RE_CONCAT_NONE

Auto-generated from RARE rule re-concat-none

RE_CONCAT_STAR_REPEAT

Auto-generated from RARE rule re-concat-star-repeat

RE_CONCAT_STAR_SWAP

Auto-generated from RARE rule re-concat-star-swap

RE_DIFF_ELIM

Auto-generated from RARE rule re-diff-elim

RE_INTER_ALL

Auto-generated from RARE rule re-inter-all

RE_INTER_CSTRING

Auto-generated from RARE rule re-inter-cstring

RE_INTER_CSTRING_NEG

Auto-generated from RARE rule re-inter-cstring-neg

RE_INTER_DUP

Auto-generated from RARE rule re-inter-dup

RE_INTER_FLATTEN

Auto-generated from RARE rule re-inter-flatten

RE_INTER_NONE

Auto-generated from RARE rule re-inter-none

RE_INTER_UNION_INCLUSION

verbatim embed:rst:leading-asterisk 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.

endverbatim

RE_IN_COMP

Auto-generated from RARE rule re-in-comp

RE_IN_CSTRING

Auto-generated from RARE rule re-in-cstring

RE_IN_EMPTY

Auto-generated from RARE rule re-in-empty

RE_IN_SIGMA

Auto-generated from RARE rule re-in-sigma

RE_IN_SIGMA_STAR

Auto-generated from RARE rule re-in-sigma-star

RE_LOOP_ELIM

verbatim embed:rst:leading-asterisk Strings – regular expression loop elimination

\[re.loop_{l,u}(R) = re.union(R^l, \ldots, R^u)\]

where \(u \geq l\).

endverbatim

RE_LOOP_NEG

Auto-generated from RARE rule re-loop-neg

RE_OPT_ELIM

Auto-generated from RARE rule re-opt-elim

RE_STAR_NONE

Auto-generated from RARE rule re-star-none

RE_UNION_ALL

Auto-generated from RARE rule re-union-all

RE_UNION_DUP

Auto-generated from RARE rule re-union-dup

RE_UNION_FLATTEN

Auto-generated from RARE rule re-union-flatten

RE_UNION_NONE

Auto-generated from RARE rule re-union-none

SEQ_LEN_REV

Auto-generated from RARE rule seq-len-rev

SEQ_LEN_UNIT

Auto-generated from RARE rule seq-len-unit

SEQ_NTH_UNIT

Auto-generated from RARE rule seq-nth-unit

SEQ_REV_CONCAT

Auto-generated from RARE rule seq-rev-concat

SEQ_REV_REV

Auto-generated from RARE rule seq-rev-rev

SEQ_REV_UNIT

Auto-generated from RARE rule seq-rev-unit

SETS_CARD_EMP

Auto-generated from RARE rule sets-card-emp

SETS_CARD_MINUS

Auto-generated from RARE rule sets-card-minus

SETS_CARD_SINGLETON

Auto-generated from RARE rule sets-card-singleton

SETS_CARD_UNION

Auto-generated from RARE rule sets-card-union

SETS_CHOOSE_SINGLETON

Auto-generated from RARE rule sets-choose-singleton

SETS_EQ_SINGLETON_EMP

Auto-generated from RARE rule sets-eq-singleton-emp

SETS_INSERT_ELIM

verbatim embed:rst:leading-asterisk 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)\]

endverbatim

SETS_INTER_COMM

Auto-generated from RARE rule sets-inter-comm

SETS_INTER_EMP1

Auto-generated from RARE rule sets-inter-emp1

SETS_INTER_EMP2

Auto-generated from RARE rule sets-inter-emp2

SETS_INTER_MEMBER

Auto-generated from RARE rule sets-inter-member

SETS_IS_EMPTY_EVAL

verbatim embed:rst:leading-asterisk 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.

endverbatim

SETS_MEMBER_EMP

Auto-generated from RARE rule sets-member-emp

SETS_MEMBER_SINGLETON

Auto-generated from RARE rule sets-member-singleton

SETS_MINUS_EMP1

Auto-generated from RARE rule sets-minus-emp1

SETS_MINUS_EMP2

Auto-generated from RARE rule sets-minus-emp2

SETS_MINUS_MEMBER

Auto-generated from RARE rule sets-minus-member

SETS_SUBSET_ELIM

Auto-generated from RARE rule sets-subset-elim

SETS_UNION_COMM

Auto-generated from RARE rule sets-union-comm

SETS_UNION_EMP1

Auto-generated from RARE rule sets-union-emp1

SETS_UNION_EMP2

Auto-generated from RARE rule sets-union-emp2

SETS_UNION_MEMBER

Auto-generated from RARE rule sets-union-member

STR_AT_ELIM

Auto-generated from RARE rule str-at-elim

STR_CONCAT_CLASH

Auto-generated from RARE rule str-concat-clash

STR_CONCAT_CLASH2

Auto-generated from RARE rule str-concat-clash2

STR_CONCAT_CLASH2_REV

Auto-generated from RARE rule str-concat-clash2-rev

STR_CONCAT_CLASH_CHAR

Auto-generated from RARE rule str-concat-clash-char

STR_CONCAT_CLASH_CHAR_REV

Auto-generated from RARE rule str-concat-clash-char-rev

STR_CONCAT_CLASH_REV

Auto-generated from RARE rule str-concat-clash-rev

STR_CONCAT_EMP

Auto-generated from RARE rule str-concat-emp

STR_CONCAT_FLATTEN

Auto-generated from RARE rule str-concat-flatten

STR_CONCAT_FLATTEN_EQ

Auto-generated from RARE rule str-concat-flatten-eq

STR_CONCAT_FLATTEN_EQ_REV

Auto-generated from RARE rule str-concat-flatten-eq-rev

STR_CONCAT_UNIFY

Auto-generated from RARE rule str-concat-unify

STR_CONCAT_UNIFY_BASE

Auto-generated from RARE rule str-concat-unify-base

STR_CONCAT_UNIFY_BASE_REV

Auto-generated from RARE rule str-concat-unify-base-rev

STR_CONCAT_UNIFY_REV

Auto-generated from RARE rule str-concat-unify-rev

STR_CONTAINS_CONCAT_FIND

Auto-generated from RARE rule str-contains-concat-find

STR_CONTAINS_EMP

Auto-generated from RARE rule str-contains-emp

STR_CONTAINS_IS_EMP

Auto-generated from RARE rule str-contains-is-emp

STR_CONTAINS_LEQ_LEN_EQ

Auto-generated from RARE rule str-contains-leq-len-eq

STR_CONTAINS_LT_LEN

Auto-generated from RARE rule str-contains-lt-len

STR_CONTAINS_REFL

Auto-generated from RARE rule str-contains-refl

STR_CONTAINS_SPLIT_CHAR

Auto-generated from RARE rule str-contains-split-char

STR_EQ_CTN_FALSE

Auto-generated from RARE rule str-eq-ctn-false

STR_EQ_CTN_FULL_FALSE1

Auto-generated from RARE rule str-eq-ctn-full-false1

STR_EQ_CTN_FULL_FALSE2

Auto-generated from RARE rule str-eq-ctn-full-false2

STR_INDEXOF_CONTAINS_PRE

Auto-generated from RARE rule str-indexof-contains-pre

STR_INDEXOF_NO_CONTAINS

Auto-generated from RARE rule str-indexof-no-contains

STR_INDEXOF_RE_NONE

Auto-generated from RARE rule str-indexof-re-none

STR_INDEXOF_SELF

Auto-generated from RARE rule str-indexof-self

STR_IN_RE_CONCAT_STAR_CHAR

verbatim embed:rst:leading-asterisk Strings – string in regular expression concatenation star character

\[\begin{split}\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))\end{split}\]

where all strings in \(R\) have length one.

endverbatim

STR_IN_RE_CONSUME

verbatim embed:rst:leading-asterisk 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\).

endverbatim

STR_IN_RE_CONTAINS

Auto-generated from RARE rule str-in-re-contains

STR_IN_RE_EVAL

verbatim embed:rst:leading-asterisk 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.

endverbatim

STR_IN_RE_INTER_ELIM

Auto-generated from RARE rule str-in-re-inter-elim

STR_IN_RE_RANGE_ELIM

Auto-generated from RARE rule str-in-re-range-elim

STR_IN_RE_REQ_UNFOLD

Auto-generated from RARE rule str-in-re-req-unfold

STR_IN_RE_REQ_UNFOLD_REV

Auto-generated from RARE rule str-in-re-req-unfold-rev

STR_IN_RE_SIGMA

verbatim embed:rst:leading-asterisk 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)\]

endverbatim

STR_IN_RE_SIGMA_STAR

verbatim embed:rst:leading-asterisk 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{++}\).

endverbatim

STR_IN_RE_SKIP_UNFOLD

Auto-generated from RARE rule str-in-re-skip-unfold

STR_IN_RE_SKIP_UNFOLD_REV

Auto-generated from RARE rule str-in-re-skip-unfold-rev

STR_IN_RE_STRIP_CHAR

Auto-generated from RARE rule str-in-re-strip-char

STR_IN_RE_STRIP_CHAR_REV

Auto-generated from RARE rule str-in-re-strip-char-rev

STR_IN_RE_STRIP_CHAR_S_SINGLE

Auto-generated from RARE rule str-in-re-strip-char-s-single

STR_IN_RE_STRIP_CHAR_S_SINGLE_REV

Auto-generated from RARE rule str-in-re-strip-char-s-single-rev

STR_IN_RE_STRIP_PREFIX

Auto-generated from RARE rule str-in-re-strip-prefix

STR_IN_RE_STRIP_PREFIX_BASE

Auto-generated from RARE rule str-in-re-strip-prefix-base

STR_IN_RE_STRIP_PREFIX_BASE_NEG

Auto-generated from RARE rule str-in-re-strip-prefix-base-neg

STR_IN_RE_STRIP_PREFIX_BASE_NEG_REV

Auto-generated from RARE rule str-in-re-strip-prefix-base-neg-rev

STR_IN_RE_STRIP_PREFIX_BASE_REV

Auto-generated from RARE rule str-in-re-strip-prefix-base-rev

STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE

Auto-generated from RARE rule str-in-re-strip-prefix-base-s-single

STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE_NEG

Auto-generated from RARE rule str-in-re-strip-prefix-base-s-single-neg

STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE_NEG_REV

Auto-generated from RARE rule str-in-re-strip-prefix-base-s-single-neg-rev

STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE_REV

Auto-generated from RARE rule str-in-re-strip-prefix-base-s-single-rev

STR_IN_RE_STRIP_PREFIX_NEG

Auto-generated from RARE rule str-in-re-strip-prefix-neg

STR_IN_RE_STRIP_PREFIX_NEG_REV

Auto-generated from RARE rule str-in-re-strip-prefix-neg-rev

STR_IN_RE_STRIP_PREFIX_REV

Auto-generated from RARE rule str-in-re-strip-prefix-rev

STR_IN_RE_STRIP_PREFIX_SRS_SINGLE

Auto-generated from RARE rule str-in-re-strip-prefix-srs-single

STR_IN_RE_STRIP_PREFIX_SRS_SINGLE_NEG

Auto-generated from RARE rule str-in-re-strip-prefix-srs-single-neg

STR_IN_RE_STRIP_PREFIX_SRS_SINGLE_NEG_REV

Auto-generated from RARE rule str-in-re-strip-prefix-srs-single-neg-rev

STR_IN_RE_STRIP_PREFIX_SRS_SINGLE_REV

Auto-generated from RARE rule str-in-re-strip-prefix-srs-single-rev

STR_IN_RE_STRIP_PREFIX_SR_SINGLE

Auto-generated from RARE rule str-in-re-strip-prefix-sr-single

STR_IN_RE_STRIP_PREFIX_SR_SINGLE_NEG

Auto-generated from RARE rule str-in-re-strip-prefix-sr-single-neg

STR_IN_RE_STRIP_PREFIX_SR_SINGLE_NEG_REV

Auto-generated from RARE rule str-in-re-strip-prefix-sr-single-neg-rev

STR_IN_RE_STRIP_PREFIX_SR_SINGLE_REV

Auto-generated from RARE rule str-in-re-strip-prefix-sr-single-rev

STR_IN_RE_STRIP_PREFIX_S_SINGLE

Auto-generated from RARE rule str-in-re-strip-prefix-s-single

STR_IN_RE_STRIP_PREFIX_S_SINGLE_NEG

Auto-generated from RARE rule str-in-re-strip-prefix-s-single-neg

STR_IN_RE_STRIP_PREFIX_S_SINGLE_NEG_REV

Auto-generated from RARE rule str-in-re-strip-prefix-s-single-neg-rev

STR_IN_RE_STRIP_PREFIX_S_SINGLE_REV

Auto-generated from RARE rule str-in-re-strip-prefix-s-single-rev

STR_IN_RE_TEST_UNFOLD

Auto-generated from RARE rule str-in-re-test-unfold

STR_IN_RE_TEST_UNFOLD_REV

Auto-generated from RARE rule str-in-re-test-unfold-rev

STR_IN_RE_UNION_ELIM

Auto-generated from RARE rule str-in-re-union-elim

STR_LEN_CONCAT_REC

Auto-generated from RARE rule str-len-concat-rec

STR_LEN_REPLACE_INV

Auto-generated from RARE rule str-len-replace-inv

STR_LEN_SUBSTR_IN_RANGE

Auto-generated from RARE rule str-len-substr-in-range

STR_LEN_SUBSTR_UB1

Auto-generated from RARE rule str-len-substr-ub1

STR_LEN_SUBSTR_UB2

Auto-generated from RARE rule str-len-substr-ub2

STR_LEN_UPDATE_INV

Auto-generated from RARE rule str-len-update-inv

STR_LEQ_CONCAT_FALSE

Auto-generated from RARE rule str-leq-concat-false

STR_LEQ_CONCAT_TRUE

Auto-generated from RARE rule str-leq-concat-true

STR_LEQ_EMPTY

Auto-generated from RARE rule str-leq-empty

STR_LEQ_EMPTY_EQ

Auto-generated from RARE rule str-leq-empty-eq

STR_LT_ELIM

Auto-generated from RARE rule str-lt-elim

STR_PREFIXOF_ELIM

Auto-generated from RARE rule str-prefixof-elim

STR_PREFIXOF_ONE

Auto-generated from RARE rule str-prefixof-one

STR_REPLACE_ALL_NO_CONTAINS

Auto-generated from RARE rule str-replace-all-no-contains

STR_REPLACE_CONTAINS_PRE

Auto-generated from RARE rule str-replace-contains-pre

STR_REPLACE_EMPTY

Auto-generated from RARE rule str-replace-empty

STR_REPLACE_NO_CONTAINS

Auto-generated from RARE rule str-replace-no-contains

STR_REPLACE_PREFIX

Auto-generated from RARE rule str-replace-prefix

STR_REPLACE_RE_ALL_NONE

Auto-generated from RARE rule str-replace-re-all-none

STR_REPLACE_RE_NONE

Auto-generated from RARE rule str-replace-re-none

STR_REPLACE_SELF

Auto-generated from RARE rule str-replace-self

STR_SUBSTR_COMBINE1

Auto-generated from RARE rule str-substr-combine1

STR_SUBSTR_COMBINE2

Auto-generated from RARE rule str-substr-combine2

STR_SUBSTR_COMBINE3

Auto-generated from RARE rule str-substr-combine3

STR_SUBSTR_COMBINE4

Auto-generated from RARE rule str-substr-combine4

STR_SUBSTR_CONCAT1

Auto-generated from RARE rule str-substr-concat1

STR_SUBSTR_CONCAT2

Auto-generated from RARE rule str-substr-concat2

STR_SUBSTR_EMPTY_RANGE

Auto-generated from RARE rule str-substr-empty-range

STR_SUBSTR_EMPTY_START

Auto-generated from RARE rule str-substr-empty-start

STR_SUBSTR_EMPTY_START_NEG

Auto-generated from RARE rule str-substr-empty-start-neg

STR_SUBSTR_EMPTY_STR

Auto-generated from RARE rule str-substr-empty-str

STR_SUBSTR_EQ_EMPTY

Auto-generated from RARE rule str-substr-eq-empty

STR_SUBSTR_FULL

Auto-generated from RARE rule str-substr-full

STR_SUBSTR_FULL_EQ

Auto-generated from RARE rule str-substr-full-eq

STR_SUBSTR_LEN_INCLUDE

Auto-generated from RARE rule str-substr-len-include

STR_SUBSTR_LEN_INCLUDE_PRE

Auto-generated from RARE rule str-substr-len-include-pre

STR_SUBSTR_LEN_SKIP

Auto-generated from RARE rule str-substr-len-skip

STR_SUFFIXOF_ELIM

Auto-generated from RARE rule str-suffixof-elim

STR_SUFFIXOF_ONE

Auto-generated from RARE rule str-suffixof-one

STR_TO_INT_CONCAT_NEG_ONE

Auto-generated from RARE rule str-to-int-concat-neg-one

STR_TO_LOWER_CONCAT

Auto-generated from RARE rule str-to-lower-concat

STR_TO_LOWER_FROM_INT

Auto-generated from RARE rule str-to-lower-from-int

STR_TO_LOWER_LEN

Auto-generated from RARE rule str-to-lower-len

STR_TO_LOWER_UPPER

Auto-generated from RARE rule str-to-lower-upper

STR_TO_UPPER_CONCAT

Auto-generated from RARE rule str-to-upper-concat

STR_TO_UPPER_FROM_INT

Auto-generated from RARE rule str-to-upper-from-int

STR_TO_UPPER_LEN

Auto-generated from RARE rule str-to-upper-len

STR_TO_UPPER_LOWER

Auto-generated from RARE rule str-to-upper-lower

UF_BV2NAT_GEQ_ELIM

Auto-generated from RARE rule uf-bv2nat-geq-elim

UF_BV2NAT_INT2BV

Auto-generated from RARE rule uf-bv2nat-int2bv

UF_BV2NAT_INT2BV_EXTEND

Auto-generated from RARE rule uf-bv2nat-int2bv-extend

UF_BV2NAT_INT2BV_EXTRACT

Auto-generated from RARE rule uf-bv2nat-int2bv-extract

UF_INT2BV_BV2NAT

Auto-generated from RARE rule uf-int2bv-bv2nat

UF_INT2BV_BVULE_EQUIV

Auto-generated from RARE rule uf-int2bv-bvule-equiv

UF_INT2BV_BVULT_EQUIV

Auto-generated from RARE rule uf-int2bv-bvult-equiv