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 theTRANSCENDENTAL_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 kindcvc5::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 ascvc5::Kind::ITE
,cvc5::Kind::EQUAL
, and so on. It is also used forcvc5::Kind::APPLY_UF
where \(f\) must be provided. It is not used for equality betweencvc5::Kind::HO_APPLY
terms, which should use theHO_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.hFor 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 ascvc5::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 anOR
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 theProofRewriteRule
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 theTHEORY_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