ProofRule

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$. 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

ANNOTATION

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

\[\inferrule{F \mid a_1 \dots a_n}{F}\]

The terms $a_1 \dots a_n$ can be anything used to annotate the proof node, one example is where $a_1$ is a theory::InferenceId. 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) \leftrightarrow ((x \leq a \land y \geq b) \lor (x \geq a \land y \leq b))}{if $\sigma = -1$}\\\inferruleSC{- \mid x, y, a, b, \sigma}{(t \geq tplane) \leftrightarrow ((x \leq a \land y \leq b) \lor (x \geq a \land y \geq b))}{if $\sigma = 1$}\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 \{ 1, -1\}$ and $tplane := b \cdot x + a \cdot y - a \cdot b$ is the tangent plane of $x \cdot y$ at $(a,b)$. endverbatim

ARITH_NL_COVERING_DIRECT

verbatim embed:rst:leading-asterisk Arithmetic – Coverings – Direct conflict

We use $\texttt{IRP}_k(poly)$ for an IndexedRootPredicate that is defined as the $k$’th root of the polynomial $poly$. Note that $poly$ may not be univariate; in this case, the value of $\texttt{IRP}_k(poly)$ can only be calculated with respect to a (partial) model for all but one variable of $poly$.

A formula $\texttt{Interval}(x_i)$ describes that a variable $x_i$ is within a particular interval whose bounds are given as IRPs. It is either an open interval or a point interval:

\[ \begin{align}\begin{aligned}\texttt{IRP}_k(poly) < x_i < \texttt{IRP}_k(poly)\\x_i = \texttt{IRP}_k(poly)\end{aligned}\end{align} \]

A formula $\texttt{Cell}(x_1 \dots x_i)$ describes a portion of the real space in the following form:

\[\texttt{Interval}(x_1) \land \dots \land \texttt{Interval}(x_i)\]

A cell can also be empty (for $i = 0$).

A formula $\texttt{Covering}(x_i)$ is a set of intervals, implying that $x_i$ can be in neither of these intervals. To be a covering (of the real line), the union of these intervals should be the real numbers.

\[\inferrule{\texttt{Cell}, A \mid -}{\bot}\]

A direct interval is generated from an assumption $A$ (in variables $x_1 \dots x_i$) over a $\texttt{Cell}(x_1 \dots x_i)$. It derives that $A$ evaluates to false over the cell. In the actual algorithm, it means that $x_i$ can not be in the topmost interval of the cell. endverbatim

ARITH_NL_COVERING_RECURSIVE

verbatim embed:rst:leading-asterisk Arithmetic – Coverings – Recursive interval

See ARITH_NL_COVERING_DIRECT for the necessary definitions.

\[\inferrule{\texttt{Cell}, \texttt{Covering} \mid -}{\bot}\]

A recursive interval is generated from $\texttt{Covering}(x_i)$ over $\texttt{Cell}(x_1 \dots x_{i-1})$. It generates the conclusion that no $x_i$ exists that extends the cell and satisfies all assumptions. endverbatim

ARITH_OP_ELIM_AXIOM

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

\[\inferrule{- \mid t}{\texttt{arith::OperatorElim::getAxiomFor(t)}}\]

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 over arithmetic or bitvectors. 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, y, s}{-\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 slolem that is the number of phases $y$ is shifted. 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,\mathit{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}, \mathit{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 $\mathit{skolem}(\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 $\mathit{skolem}(\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 $\mathit{skolem}(\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 $\mathit{skolem}(\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 = ''$.

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{skolem}(\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 $\mathit{skolem}(\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 b}{t_1 = s_1}\]

where $b$ indicates if the direction is reversed. endverbatim

CONG

verbatim embed:rst:leading-asterisk Equality – Congruence

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

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

CONTRA

verbatim embed:rst:leading-asterisk Boolean – Contradiction

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

endverbatim

DRAT_REFUTATION

verbatim embed:rst:leading-asterisk DRAT Refutation

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

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

DSL_REWRITE

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

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

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

Notice that the application of the substitution takes into account the possible list semantics of variables $x_1 \ldots x_n$. If $x_i$ is a variable with list semantics, then $t_i$ denotes a list of terms. The substitution implemented by expr::narySubstitute 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

DT_UNIF

verbatim embed:rst:leading-asterisk Datatypes – Unification

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

where $C$ is a constructor. endverbatim

ENCODE_PRED_TRANSFORM

verbatim embed:rst:leading-asterisk Builtin theory – Encode predicate transformation

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

where $F$ and $G$ are equivalent up to their encoding in an external proof format. This is currently verified by $\texttt{RewriteDbNodeConverter::convert}(F) = \texttt{RewriteDbNodeConverter::convert}(G)$. This rule can be treated as a no-op 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{Evaluator::evaluate}(t)}\]

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= \texttt{TheoryUfRewriter::getHoApplyForApplyUf}(t)}\]

For example, this rule concludes $f(x,y) = @(@(f,x),y)$, where $@$ isthe HO_APPLY kind.

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 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{Rewriter}_{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{Rewriter}_{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{Rewriter}_{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{Rewriter}_{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 $\texttt{Rewriter}_{idr}(F \circ \sigma_{ids, ida}(F_n) \circ \cdots \circ \sigma_{ids, ida}(F_1)) = \texttt{Rewriter}_{idr}(G \circ \sigma_{ids, ida}(F_n) \circ \cdots \circ \sigma_{ids, ida}(F_1))$.

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

MACRO_STRING_INFERENCE

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

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

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

MODUS_PONENS

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

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

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

NARY_CONG

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

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

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

NOT_AND

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

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

endverbatim

NOT_EQUIV_ELIM1

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

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

endverbatim

NOT_EQUIV_ELIM2

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

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

endverbatim

NOT_IMPLIES_ELIM1

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

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

endverbatim

NOT_IMPLIES_ELIM2

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

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

endverbatim

NOT_ITE_ELIM1

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

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

endverbatim

NOT_ITE_ELIM2

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

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

endverbatim

NOT_NOT_ELIM

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

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

endverbatim

NOT_OR_ELIM

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

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

endverbatim

NOT_XOR_ELIM1

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

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

endverbatim

NOT_XOR_ELIM2

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

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

endverbatim

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 set representations of $C_1$ and $C_2$ are the same and the number of literals in $C_2$ is the same of that of $C_1$. endverbatim

RESOLUTION

verbatim embed:rst:leading-asterisk Boolean – Resolution

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

where

$C_1$ and $C_2$ are nodes viewed as clauses, i.e., either an OR node with each children viewed as a literal or a node viewed as a literal. Note that an OR node could also be a literal.
$pol$ is either true or false, representing the polarity of the pivot on the first clause
$L$ is the pivot of the resolution, which occurs as is (resp. under a NOT) in $C_1$ and negatively (as is) in $C_2$ if $pol = \top$ ($pol = \bot$).

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

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

RE_ELIM

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

\[\inferrule{-\mid F,b}{F = \texttt{strings::RegExpElimination::eliminate}(F, b)}\]

where $b$ is a Boolean indicating whether we are using aggressive eliminations. Notice this rule concludes $F = F$ if no eliminations are performed for $F$. 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{inter}(R_1,R_2)}\]

endverbatim

RE_UNFOLD_NEG

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

\[\inferrule{t\not\in R\mid -}{\texttt{RegExpOpr::reduceRegExpNeg}(t\not\in R)}\]

corresponding to the one-step unfolding of the premise. 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{++}(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{++}(r_2, \ldots, r_n)}\]

where $r_1$ has fixed length $L$.

or alternatively for the reverse:

\[\inferrule{t \not \in \mathit{re}.\text{++}(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{++}(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 -}{\texttt{RegExpOpr::reduceRegExpPos}(t\in R)}\]

corresponding to the one-step unfolding of the premise. 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_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{\exists x_1\dots x_n.\> F\mid -}{F\sigma}\]

or

\[\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 obtained by SkolemManager::mkSkolemize, returned in the skolems argument of that method. The witness terms for the returned skolems can be obtained by SkolemManager::getWitnessForm. 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\neq 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}\]

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 $\mathit{skolem}(\mathit{pre}(t,n)$ and $w_2$ is $\mathit{skolem}(\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{strings::TermRegistry::eagerReduce}(t)$. endverbatim

STRING_LENGTH_NON_EMPTY

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

\[\inferrule{t\neq ''\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= '')\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{strings::StringsPreprocess::reduce}(t, R, \dots)$. In other words, $R$ is the reduction predicate for extended term $t$, and $w$ is $skolem(t)$.

Notice that the free variables of $R$ are $w$ and the free variables of $t$. endverbatim

STRING_SEQ_UNIT_INJ

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

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

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

SUBS

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

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

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

SYMM

verbatim embed:rst:leading-asterisk Equality – Symmetry

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

or

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

endverbatim

THEORY_REWRITE

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

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

where id is the ProofRewriteRule of the theory rewrite rule which transforms $t$ to $t'$.

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

TRANS

verbatim embed:rst:leading-asterisk Equality – Transitivity

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

endverbatim

TRUE_ELIM

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

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

endverbatim

TRUE_INTRO

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

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

endverbatim

TRUST

verbatim embed:rst:leading-asterisk Trusted rule

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

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

TRUST_THEORY_REWRITE

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

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

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

UNKNOWN

verbatim embed:rst:leading-asterisk External – Alethe

Place holder for Alethe rules.

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

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

XOR_ELIM1

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

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

endverbatim

XOR_ELIM2

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

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

endverbatim