Enum ProofRule

  • All Implemented Interfaces:
    java.io.Serializable, java.lang.Comparable<ProofRule>

    public enum ProofRule
    extends java.lang.Enum<ProofRule>
    • Enum Constant Summary

      Enum Constants 
      Enum Constant Description
      ALETHE_RULE
      External – Alethe Place holder for Alethe rules.
      ALPHA_EQUIV
      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\).
      AND_ELIM
      Boolean – And elimination \[ \inferrule{(F_1 \land \dots \land F_n) \mid i}{F_i} \]
      AND_INTRO
      Boolean – And introduction \[ \inferrule{F_1 \dots F_n \mid -}{(F_1 \land \dots \land F_n)} \]
      ANNOTATION
      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.
      ARITH_MULT_NEG
      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.
      ARITH_MULT_POS
      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.
      ARITH_MULT_SIGN
      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.
      ARITH_MULT_TANGENT
      Arithmetic – Multiplication tangent plane \[ \inferruleSC{- \mid t, 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 t, 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$} \] where \(x,y\) are real terms (variables or extended terms), \(t = x \cdot y\) (possibly under rewriting), \(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)\).
      ARITH_NL_COVERING_DIRECT
      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\).
      ARITH_NL_COVERING_RECURSIVE
      Arithmetic – Coverings – Recursive interval See ARITH_NL_COVERING_DIRECT <cvc5.ARITH_NL_COVERING_DIRECT> for the necessary definitions.
      ARITH_OP_ELIM_AXIOM
      Arithmetic – Operator elimination \[ \inferrule{- \mid t}{\texttt{arith::OperatorElim::getAxiomFor(t)}} \]
      ARITH_POLY_NORM
      Arithmetic – Polynomial normalization \[ \inferrule{- \mid t = s}{t = s} \] where \(\texttt{arith::PolyNorm::isArithPolyNorm(t, s)} = \top\).
      ARITH_SUM_UB
      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, =\}\).
      ARITH_TRANS_EXP_APPROX_ABOVE_NEG
      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\).
      ARITH_TRANS_EXP_APPROX_ABOVE_POS
      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\).
      ARITH_TRANS_EXP_APPROX_BELOW
      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\).
      ARITH_TRANS_EXP_NEG
      Arithmetic – Transcendentals – Exp at negative values \[ \inferrule{- \mid t}{(t < 0) \leftrightarrow (\exp(t) < 1)} \]
      ARITH_TRANS_EXP_POSITIVITY
      Arithmetic – Transcendentals – Exp is always positive \[ \inferrule{- \mid t}{\exp(t) > 0} \]
      ARITH_TRANS_EXP_SUPER_LIN
      Arithmetic – Transcendentals – Exp grows super-linearly for positive values \[ \inferrule{- \mid t}{t \leq 0 \lor \exp(t) > t+1} \]
      ARITH_TRANS_EXP_ZERO
      Arithmetic – Transcendentals – Exp at zero \[ \inferrule{- \mid t}{(t=0) \leftrightarrow (\exp(t) = 1)} \]
      ARITH_TRANS_PI
      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\).
      ARITH_TRANS_SINE_APPROX_ABOVE_NEG
      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\).
      ARITH_TRANS_SINE_APPROX_ABOVE_POS
      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\)).
      ARITH_TRANS_SINE_APPROX_BELOW_NEG
      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\)).
      ARITH_TRANS_SINE_APPROX_BELOW_POS
      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\).
      ARITH_TRANS_SINE_BOUNDS
      Arithmetic – Transcendentals – Sine is always between -1 and 1 \[ \inferrule{- \mid t}{\sin(t) \leq 1 \land \sin(t) \geq -1} \]
      ARITH_TRANS_SINE_SHIFT
      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.
      ARITH_TRANS_SINE_SYMMETRY
      Arithmetic – Transcendentals – Sine is symmetric with respect to negation of the argument \[ \inferrule{- \mid t}{\sin(t) - \sin(-t) = 0} \]
      ARITH_TRANS_SINE_TANGENT_PI
      Arithmetic – Transcendentals – Sine is bounded by the tangents at -pi and pi ..
      ARITH_TRANS_SINE_TANGENT_ZERO
      Arithmetic – Transcendentals – Sine is bounded by the tangent at zero ..
      ARITH_TRICHOTOMY
      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.
      ARRAYS_EQ_RANGE_EXPAND
      Arrays – Expansion of array range equality \[ \inferrule{-\mid \mathit{eqrange}(a,b,i,j)} {\mathit{eqrange}(a,b,i,j)= \forall x.\> i \leq x \leq j \rightarrow \mathit{select}(a,x)=\mathit{select}(b,x)} \]
      ARRAYS_EXT
      Arrays – Arrays extensionality \[ \inferrule{a \neq b\mid -} {\mathit{select}(a,k)\neq\mathit{select}(b,k)} \] where \(k\) is \(\texttt{arrays::SkolemCache::getExtIndexSkolem}(a\neq b)\).
      ARRAYS_READ_OVER_WRITE
      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)} \]
      ARRAYS_READ_OVER_WRITE_1
      Arrays – Read over write 1 \[ \inferrule{-\mid \mathit{select}(\mathit{store}(a,i,e),i)} {\mathit{select}(\mathit{store}(a,i,e),i)=e} \]
      ARRAYS_READ_OVER_WRITE_CONTRA
      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} \]
      ASSUME
      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.
      BETA_REDUCE
      Equality – Beta reduction \[ \inferrule{\mid \lambda x_1\dots x_n.\> t, t_1,\dots,t_n} {((\lambda x_1\dots x_n.\> t) t_1 \ldots t_n)=t\{x_1\mapsto t_1,\dots,x_n\mapsto t_n\}} \] The right hand side of the equality in the conclusion is computed using standard substitution via Node.substitute.
      BV_BITBLAST_STEP
      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)\).
      BV_EAGER_ATOM
      Bit-vectors – Bit-vector eager atom \[ \inferrule{-\mid F}{F = F[0]} \] where \(F\) is of kind BITVECTOR_EAGER_ATOM.
      CHAIN_RESOLUTION
      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.
      CNF_AND_NEG
      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} \]
      CNF_AND_POS
      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} \]
      CNF_EQUIV_NEG1
      Boolean – CNF – Equiv Negative 1 \[ \inferrule{- \mid F_1 = F_2}{(F_1 = F_2) \lor F_1 \lor F_2} \]
      CNF_EQUIV_NEG2
      Boolean – CNF – Equiv Negative 2 \[ \inferrule{- \mid F_1 = F_2}{(F_1 = F_2) \lor \neg F_1 \lor \neg F_2} \]
      CNF_EQUIV_POS1
      Boolean – CNF – Equiv Positive 1 \[ \inferrule{- \mid F_1 = F_2}{F_1 \neq F_2 \lor \neg F_1 \lor F_2} \]
      CNF_EQUIV_POS2
      Boolean – CNF – Equiv Positive 2 \[ \inferrule{- \mid F_1 = F_2}{F_1 \neq F_2 \lor F_1 \lor \neg F_2} \]
      CNF_IMPLIES_NEG1
      Boolean – CNF – Implies Negative 1 \[ \inferrule{- \mid F_1 \rightarrow F_2}{(F_1 \rightarrow F_2) \lor F_1} \]
      CNF_IMPLIES_NEG2
      Boolean – CNF – Implies Negative 2 \[ \inferrule{- \mid F_1 \rightarrow F_2}{(F_1 \rightarrow F_2) \lor \neg F_2} \]
      CNF_IMPLIES_POS
      Boolean – CNF – Implies Positive \[ \inferrule{- \mid F_1 \rightarrow F_2}{\neg(F_1 \rightarrow F_2) \lor \neg F_1 \lor F_2} \]
      CNF_ITE_NEG1
      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} \]
      CNF_ITE_NEG2
      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} \]
      CNF_ITE_NEG3
      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} \]
      CNF_ITE_POS1
      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} \]
      CNF_ITE_POS2
      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} \]
      CNF_ITE_POS3
      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} \]
      CNF_OR_NEG
      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} \]
      CNF_OR_POS
      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} \]
      CNF_XOR_NEG1
      Boolean – CNF – XOR Negative 1 \[ \inferrule{- \mid F_1 \xor F_2}{(F_1 \xor F_2) \lor \neg F_1 \lor F_2} \]
      CNF_XOR_NEG2
      Boolean – CNF – XOR Negative 2 \[ \inferrule{- \mid F_1 \xor F_2}{(F_1 \xor F_2) \lor F_1 \lor \neg F_2} \]
      CNF_XOR_POS1
      Boolean – CNF – XOR Positive 1 \[ \inferrule{- \mid F_1 \xor F_2}{\neg(F_1 \xor F_2) \lor F_1 \lor F_2} \]
      CNF_XOR_POS2
      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} \]
      CONCAT_CONFLICT
      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.
      CONCAT_CONFLICT_DEQ
      Strings – Core rules – Concatenation conflict for disequal characters \[ \inferrule{(t_1\cdot t) = (s_1 \cdot s), t_1 \deq 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.
      CONCAT_CPROP
      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 = w_3\cdot r)} \] where \(w_1,\,w_2,\,w_3\) are words, \(w_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)))\).
      CONCAT_CSPLIT
      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))\).
      CONCAT_EQ
      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.
      CONCAT_LPROP
      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_t)} \] where \(r_t\) is \(\mathit{skolem}(\mathit{suf}(t_1,\mathit{len}(s_1)))\).
      CONCAT_SPLIT
      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_t) \vee (s_1 = t_1\cdot r_s)}{if $b=\bot$} \] where \(r_t\) is \(\mathit{skolem}(\mathit{suf}(t_1,\mathit{len}(s_1)))\) and \(r_s\) is \(\mathit{skolem}(\mathit{suf}(s_1,\mathit{len}(t_1)))\).
      CONCAT_UNIFY
      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.
      CONG
      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.
      CONTRA
      Boolean – Contradiction \[ \inferrule{F, \neg F \mid -}{\bot} \]
      DSL_REWRITE
      Builtin theory – DSL rewrite \[ \inferrule{F_1 \dots F_n \mid id t_1 \dots t_n}{F} \] where the DSL rewrite rule with the given identifier is \(\forall x_1 \dots x_n.
      DT_CLASH
      Datatypes – Clash \[ \inferruleSC{\mathit{is}_{C_i}(t), \mathit{is}_{C_j}(t)\mid -}{\bot} {if $i\neq j$} \]
      DT_COLLAPSE
      Datatypes – Collapse \[ \inferrule{-\mid \mathit{sel}_i(C_j(t_1,\dots,t_n))}{ \mathit{sel}_i(C_j(t_1,\dots,t_n)) = r} \] where \(C_j\) is a constructor, \(r\) is \(t_i\) if \(\mathit{sel}_i\) is a correctly applied selector, or {@link TypeNode#mkGroundTerm()} of the proper type otherwise.
      DT_INST
      Datatypes – Instantiation \[ \inferrule{-\mid t,n}{\mathit{is}_C(t) = (t = C(\mathit{sel}_1(t),\dots,\mathit{sel}_n(t)))} \] where \(C\) is the \(n^{\mathit{th}}\) constructor of the type of t, and \(\mathit{is}_C\) is the discriminator (tester) for \(C\).
      DT_SPLIT
      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\).
      DT_UNIF
      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.
      ENCODE_PRED_TRANSFORM
      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.
      EQ_RESOLVE
      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 <cvc5.EQUIV_ELIM1> + RESOLUTION <cvc5.RESOLUTION>.
      EQUIV_ELIM1
      Boolean – Equivalence elimination version 1 \[ \inferrule{F_1 = F_2 \mid -}{\neg F_1 \lor F_2} \]
      EQUIV_ELIM2
      Boolean – Equivalence elimination version 2 \[ \inferrule{F_1 = F_2 \mid -}{F_1 \lor \neg F_2} \]
      EVALUATE
      Builtin theory – Evaluate \[ \inferrule{- \mid t}{t = \texttt{Evaluator::evaluate}(t)} \] Note this is equivalent to: (REWRITE t {@link MethodId#RW_EVALUATE)}.
      FACTORING
      Boolean – Factoring \[ \inferrule{C_1 \mid -}{C_2} \] where \(C_2\) is the clause \(C_1\), but every occurence of a literal after its first occurence is omitted.
      FALSE_ELIM
      Equality – False elim \[ \inferrule{F=\bot\mid -}{\neg F} \]
      FALSE_INTRO
      Equality – False intro \[ \inferrule{\neg F\mid -}{F = \bot} \]
      HO_APP_ENCODE
      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.
      HO_CONG
      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`.
      IMPLIES_ELIM
      Boolean – Implication elimination \[ \inferrule{F_1 \rightarrow F_2 \mid -}{\neg F_1 \lor F_2} \]
      INSTANTIATE
      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.
      INT_TIGHT_LB
      Arithmetic – Tighten strict integer lower bounds \[ \inferrule{i > c \mid -}{i \geq \lceil c \rceil} \] where \(i\) has integer type.
      INT_TIGHT_UB
      Arithmetic – Tighten strict integer upper bounds \[ \inferrule{i < c \mid -}{i \leq \lfloor c \rfloor} \] where \(i\) has integer type.
      ITE_ELIM1
      Boolean – ITE elimination version 1 \[ \inferrule{(\ite{C}{F_1}{F_2}) \mid -}{\neg C \lor F_1} \]
      ITE_ELIM2
      Boolean – ITE elimination version 2 \[ \inferrule{(\ite{C}{F_1}{F_2}) \mid -}{C \lor F_2} \]
      LFSC_RULE
      External – LFSC Place holder for LFSC rules.
      MACRO_ARITH_SCALE_SUM_UB
      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.
      MACRO_BV_BITBLAST
      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.
      MACRO_RESOLUTION
      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 <cvc5.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 <cvc5.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'\)
      MACRO_RESOLUTION_TRUST
      Boolean – N-ary Resolution + Factoring + Reordering unchecked Same as :cpp:enumerator:`MACRO_RESOLUTION <cvc5.MACRO_RESOLUTION>`, but not checked by the internal proof checker.
      MACRO_REWRITE
      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.
      MACRO_SR_EQ_INTRO
      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.
      MACRO_SR_PRED_ELIM
      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.
      MACRO_SR_PRED_INTRO
      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.
      MACRO_SR_PRED_TRANSFORM
      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))\).
      MACRO_STRING_INFERENCE
      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}\).
      MODUS_PONENS
      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 <cvc5.IMPLIES_ELIM> + RESOLUTION <cvc5.RESOLUTION>.
      NARY_CONG
      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.
      NOT_AND
      Boolean – De Morgan – Not And \[ \inferrule{\neg(F_1 \land \dots \land F_n) \mid -}{\neg F_1 \lor \dots \lor \neg F_n} \]
      NOT_EQUIV_ELIM1
      Boolean – Not Equivalence elimination version 1 \[ \inferrule{F_1 \neq F_2 \mid -}{F_1 \lor F_2} \]
      NOT_EQUIV_ELIM2
      Boolean – Not Equivalence elimination version 2 \[ \inferrule{F_1 \neq F_2 \mid -}{\neg F_1 \lor \neg F_2} \]
      NOT_IMPLIES_ELIM1
      Boolean – Not Implication elimination version 1 \[ \inferrule{\neg(F_1 \rightarrow F_2) \mid -}{F_1} \]
      NOT_IMPLIES_ELIM2
      Boolean – Not Implication elimination version 2 \[ \inferrule{\neg(F_1 \rightarrow F_2) \mid -}{\neg F_2} \]
      NOT_ITE_ELIM1
      Boolean – Not ITE elimination version 1 \[ \inferrule{\neg(\ite{C}{F_1}{F_2}) \mid -}{\neg C \lor \neg F_1} \]
      NOT_ITE_ELIM2
      Boolean – Not ITE elimination version 2 \[ \inferrule{\neg(\ite{C}{F_1}{F_2}) \mid -}{C \lor \neg F_2} \]
      NOT_NOT_ELIM
      Boolean – Double negation elimination \[ \inferrule{\neg (\neg F) \mid -}{F} \]
      NOT_OR_ELIM
      Boolean – Not Or elimination \[ \inferrule{\neg(F_1 \lor \dots \lor F_n) \mid i}{\neg F_i} \]
      NOT_XOR_ELIM1
      Boolean – Not XOR elimination version 1 \[ \inferrule{\neg(F_1 \xor F_2) \mid -}{F_1 \lor \neg F_2} \]
      NOT_XOR_ELIM2
      Boolean – Not XOR elimination version 2 \[ \inferrule{\neg(F_1 \xor F_2) \mid -}{\neg F_1 \lor F_2} \]
      RE_ELIM
      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.
      RE_INTER
      Strings – Regular expressions – Intersection \[ \inferrule{t\in R_1,\,t\in R_2\mid -}{t\in \mathit{inter}(R_1,R_2)} \]
      RE_UNFOLD_NEG
      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.
      RE_UNFOLD_NEG_CONCAT_FIXED
      Strings – Regular expressions – Unfold negative concatenation, fixed \[ \inferrule{t\not\in R\mid -}{\texttt{RegExpOpr::reduceRegExpNegConcatFixed}(t\not\in R,L,i)} \] where \(\texttt{RegExpOpr::getRegExpConcatFixed}(t\not\in R, i) = L\), corresponding to the one-step unfolding of the premise, optimized for fixed length of component \(i\) of the regular expression concatenation \(R\).
      RE_UNFOLD_POS
      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.
      REFL
      Equality – Reflexivity \[ \inferrule{-\mid t}{t = t} \]
      REMOVE_TERM_FORMULA_AXIOM
      Processing rules – Remove Term Formulas Axiom \[ \inferrule{- \mid t}{\texttt{RemoveTermFormulas::getAxiomFor}(t)} \]
      REORDERING
      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\).
      RESOLUTION
      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.
      SAT_REFUTATION
      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.
      SCOPE
      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 :cpp:enumerator:`ASSUME <cvc5.ASSUME>`.
      SKOLEM_INTRO
      Quantifiers – Skolem introduction \[ \inferrule{-\mid k}{k = t} \] where \(t\) is the unpurified form of skolem \(k\).
      SKOLEMIZE
      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.
      SPLIT
      Boolean – Split \[ \inferrule{- \mid F}{F \lor \neg F} \]
      STRING_CODE_INJ
      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} \]
      STRING_DECOMPOSE
      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)\).
      STRING_EAGER_REDUCTION
      Strings – Extended functions – Eager reduction \[ \inferrule{-\mid t}{R} \] where \(R\) is \(\texttt{strings::TermRegistry::eagerReduce}(t)\).
      STRING_LENGTH_NON_EMPTY
      Strings – Core rules – Length non-empty \[ \inferrule{t\neq ''\mid -}{\mathit{len}(t) \neq 0} \]
      STRING_LENGTH_POS
      Strings – Core rules – Length positive \[ \inferrule{-\mid t}{(\mathit{len}(t) = 0\wedge t= '')\vee \mathit{len}(t) > 0} \]
      STRING_REDUCTION
      Strings – Extended functions – Reduction \[ \inferrule{-\mid t}{R\wedge t = w} \] where \(w\) is \(\texttt{strings::StringsPreprocess::reduce}(t, R, \dots)\).
      STRING_SEQ_UNIT_INJ
      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.
      SUBS
      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.
      SYMM
      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} \]
      TRANS
      Equality – Transitivity \[ \inferrule{t_1=t_2,\dots,t_{n-1}=t_n\mid -}{t_1 = t_n} \]
      TRUE_ELIM
      Equality – True elim \[ \inferrule{F=\top\mid -}{F} \]
      TRUE_INTRO
      Equality – True intro \[ \inferrule{F\mid -}{F = \top} \]
      TRUST
      Trusted rule \[ \inferrule{F_1 \dots F_n \mid tid, F, ...}{F} \] where \(tid\) is an identifier and \(F\) is a formula.
      TRUST_THEORY_REWRITE
      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.
      UNKNOWN
      External – Alethe Place holder for Alethe rules.
      XOR_ELIM1
      Boolean – XOR elimination version 1 \[ \inferrule{F_1 \xor F_2 \mid -}{F_1 \lor F_2} \]
      XOR_ELIM2
      Boolean – XOR elimination version 2 \[ \inferrule{F_1 \xor F_2 \mid -}{\neg F_1 \lor \neg F_2} \]
    • Method Summary

      All Methods Static Methods Instance Methods Concrete Methods 
      Modifier and Type Method Description
      static ProofRule fromInt​(int value)  
      int getValue()  
      static ProofRule valueOf​(java.lang.String name)
      Returns the enum constant of this type with the specified name.
      static ProofRule[] values()
      Returns an array containing the constants of this enum type, in the order they are declared.
      • Methods inherited from class java.lang.Enum

        clone, compareTo, equals, finalize, getDeclaringClass, hashCode, name, ordinal, toString, valueOf
      • Methods inherited from class java.lang.Object

        getClass, notify, notifyAll, wait, wait, wait
    • Enum Constant Detail

      • ASSUME

        public static final ProofRule ASSUME
        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 <cvc5.SCOPE> (see below).
      • SCOPE

        public static final ProofRule SCOPE
        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 :cpp:enumerator:`ASSUME <cvc5.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.
      • SUBS

        public static final ProofRule SUBS
        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\).
      • MACRO_REWRITE

        public static final ProofRule MACRO_REWRITE
        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.
      • EVALUATE

        public static final ProofRule EVALUATE
        Builtin theory – Evaluate \[ \inferrule{- \mid t}{t = \texttt{Evaluator::evaluate}(t)} \] Note this is equivalent to: (REWRITE t {@link MethodId#RW_EVALUATE)}.
      • MACRO_SR_EQ_INTRO

        public static final ProofRule MACRO_SR_EQ_INTRO
        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 :cvc5src:`theory/builtin/proof_checker.h`.
      • MACRO_SR_PRED_INTRO

        public static final ProofRule MACRO_SR_PRED_INTRO
        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.
      • MACRO_SR_PRED_ELIM

        public static final ProofRule MACRO_SR_PRED_ELIM
        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 <cvc5.MACRO_SR_EQ_INTRO>.
      • MACRO_SR_PRED_TRANSFORM

        public static final ProofRule MACRO_SR_PRED_TRANSFORM
        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 <cvc5.MACRO_SR_PRED_INTRO> above.
      • ENCODE_PRED_TRANSFORM

        public static final ProofRule ENCODE_PRED_TRANSFORM
        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.
      • DSL_REWRITE

        public static final ProofRule DSL_REWRITE
        Builtin theory – DSL rewrite \[ \inferrule{F_1 \dots F_n \mid id t_1 \dots t_n}{F} \] where the DSL rewrite rule with the given identifier 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.
      • ANNOTATION

        public static final ProofRule ANNOTATION
        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.
      • REMOVE_TERM_FORMULA_AXIOM

        public static final ProofRule REMOVE_TERM_FORMULA_AXIOM
        Processing rules – Remove Term Formulas Axiom \[ \inferrule{- \mid t}{\texttt{RemoveTermFormulas::getAxiomFor}(t)} \]
      • TRUST

        public static final ProofRule TRUST
        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.
      • TRUST_THEORY_REWRITE

        public static final ProofRule TRUST_THEORY_REWRITE
        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.
      • SAT_REFUTATION

        public static final ProofRule SAT_REFUTATION
        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.
      • RESOLUTION

        public static final ProofRule RESOLUTION
        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.
      • CHAIN_RESOLUTION

        public static final ProofRule CHAIN_RESOLUTION
        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'\)
      • FACTORING

        public static final ProofRule FACTORING
        Boolean – Factoring \[ \inferrule{C_1 \mid -}{C_2} \] where \(C_2\) is the clause \(C_1\), but every occurence of a literal after its first occurence is omitted.
      • REORDERING

        public static final ProofRule REORDERING
        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\).
      • MACRO_RESOLUTION

        public static final ProofRule MACRO_RESOLUTION
        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 <cvc5.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 <cvc5.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'\)
      • MACRO_RESOLUTION_TRUST

        public static final ProofRule MACRO_RESOLUTION_TRUST
        Boolean – N-ary Resolution + Factoring + Reordering unchecked Same as :cpp:enumerator:`MACRO_RESOLUTION <cvc5.MACRO_RESOLUTION>`, but not checked by the internal proof checker.
      • SPLIT

        public static final ProofRule SPLIT
        Boolean – Split \[ \inferrule{- \mid F}{F \lor \neg F} \]
      • EQ_RESOLVE

        public static final ProofRule EQ_RESOLVE
        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 <cvc5.EQUIV_ELIM1> + RESOLUTION <cvc5.RESOLUTION>.
      • MODUS_PONENS

        public static final ProofRule MODUS_PONENS
        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 <cvc5.IMPLIES_ELIM> + RESOLUTION <cvc5.RESOLUTION>.
      • NOT_NOT_ELIM

        public static final ProofRule NOT_NOT_ELIM
        Boolean – Double negation elimination \[ \inferrule{\neg (\neg F) \mid -}{F} \]
      • CONTRA

        public static final ProofRule CONTRA
        Boolean – Contradiction \[ \inferrule{F, \neg F \mid -}{\bot} \]
      • AND_ELIM

        public static final ProofRule AND_ELIM
        Boolean – And elimination \[ \inferrule{(F_1 \land \dots \land F_n) \mid i}{F_i} \]
      • AND_INTRO

        public static final ProofRule AND_INTRO
        Boolean – And introduction \[ \inferrule{F_1 \dots F_n \mid -}{(F_1 \land \dots \land F_n)} \]
      • NOT_OR_ELIM

        public static final ProofRule NOT_OR_ELIM
        Boolean – Not Or elimination \[ \inferrule{\neg(F_1 \lor \dots \lor F_n) \mid i}{\neg F_i} \]
      • IMPLIES_ELIM

        public static final ProofRule IMPLIES_ELIM
        Boolean – Implication elimination \[ \inferrule{F_1 \rightarrow F_2 \mid -}{\neg F_1 \lor F_2} \]
      • NOT_IMPLIES_ELIM1

        public static final ProofRule NOT_IMPLIES_ELIM1
        Boolean – Not Implication elimination version 1 \[ \inferrule{\neg(F_1 \rightarrow F_2) \mid -}{F_1} \]
      • NOT_IMPLIES_ELIM2

        public static final ProofRule NOT_IMPLIES_ELIM2
        Boolean – Not Implication elimination version 2 \[ \inferrule{\neg(F_1 \rightarrow F_2) \mid -}{\neg F_2} \]
      • EQUIV_ELIM1

        public static final ProofRule EQUIV_ELIM1
        Boolean – Equivalence elimination version 1 \[ \inferrule{F_1 = F_2 \mid -}{\neg F_1 \lor F_2} \]
      • EQUIV_ELIM2

        public static final ProofRule EQUIV_ELIM2
        Boolean – Equivalence elimination version 2 \[ \inferrule{F_1 = F_2 \mid -}{F_1 \lor \neg F_2} \]
      • NOT_EQUIV_ELIM1

        public static final ProofRule NOT_EQUIV_ELIM1
        Boolean – Not Equivalence elimination version 1 \[ \inferrule{F_1 \neq F_2 \mid -}{F_1 \lor F_2} \]
      • NOT_EQUIV_ELIM2

        public static final ProofRule NOT_EQUIV_ELIM2
        Boolean – Not Equivalence elimination version 2 \[ \inferrule{F_1 \neq F_2 \mid -}{\neg F_1 \lor \neg F_2} \]
      • XOR_ELIM1

        public static final ProofRule XOR_ELIM1
        Boolean – XOR elimination version 1 \[ \inferrule{F_1 \xor F_2 \mid -}{F_1 \lor F_2} \]
      • XOR_ELIM2

        public static final ProofRule XOR_ELIM2
        Boolean – XOR elimination version 2 \[ \inferrule{F_1 \xor F_2 \mid -}{\neg F_1 \lor \neg F_2} \]
      • NOT_XOR_ELIM1

        public static final ProofRule NOT_XOR_ELIM1
        Boolean – Not XOR elimination version 1 \[ \inferrule{\neg(F_1 \xor F_2) \mid -}{F_1 \lor \neg F_2} \]
      • NOT_XOR_ELIM2

        public static final ProofRule NOT_XOR_ELIM2
        Boolean – Not XOR elimination version 2 \[ \inferrule{\neg(F_1 \xor F_2) \mid -}{\neg F_1 \lor F_2} \]
      • ITE_ELIM1

        public static final ProofRule ITE_ELIM1
        Boolean – ITE elimination version 1 \[ \inferrule{(\ite{C}{F_1}{F_2}) \mid -}{\neg C \lor F_1} \]
      • ITE_ELIM2

        public static final ProofRule ITE_ELIM2
        Boolean – ITE elimination version 2 \[ \inferrule{(\ite{C}{F_1}{F_2}) \mid -}{C \lor F_2} \]
      • NOT_ITE_ELIM1

        public static final ProofRule NOT_ITE_ELIM1
        Boolean – Not ITE elimination version 1 \[ \inferrule{\neg(\ite{C}{F_1}{F_2}) \mid -}{\neg C \lor \neg F_1} \]
      • NOT_ITE_ELIM2

        public static final ProofRule NOT_ITE_ELIM2
        Boolean – Not ITE elimination version 2 \[ \inferrule{\neg(\ite{C}{F_1}{F_2}) \mid -}{C \lor \neg F_2} \]
      • NOT_AND

        public static final ProofRule NOT_AND
        Boolean – De Morgan – Not And \[ \inferrule{\neg(F_1 \land \dots \land F_n) \mid -}{\neg F_1 \lor \dots \lor \neg F_n} \]
      • CNF_AND_POS

        public static final ProofRule CNF_AND_POS
        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} \]
      • CNF_AND_NEG

        public static final ProofRule CNF_AND_NEG
        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} \]
      • CNF_OR_POS

        public static final ProofRule CNF_OR_POS
        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} \]
      • CNF_OR_NEG

        public static final ProofRule CNF_OR_NEG
        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} \]
      • CNF_IMPLIES_POS

        public static final ProofRule CNF_IMPLIES_POS
        Boolean – CNF – Implies Positive \[ \inferrule{- \mid F_1 \rightarrow F_2}{\neg(F_1 \rightarrow F_2) \lor \neg F_1 \lor F_2} \]
      • CNF_IMPLIES_NEG1

        public static final ProofRule CNF_IMPLIES_NEG1
        Boolean – CNF – Implies Negative 1 \[ \inferrule{- \mid F_1 \rightarrow F_2}{(F_1 \rightarrow F_2) \lor F_1} \]
      • CNF_IMPLIES_NEG2

        public static final ProofRule CNF_IMPLIES_NEG2
        Boolean – CNF – Implies Negative 2 \[ \inferrule{- \mid F_1 \rightarrow F_2}{(F_1 \rightarrow F_2) \lor \neg F_2} \]
      • CNF_EQUIV_POS1

        public static final ProofRule CNF_EQUIV_POS1
        Boolean – CNF – Equiv Positive 1 \[ \inferrule{- \mid F_1 = F_2}{F_1 \neq F_2 \lor \neg F_1 \lor F_2} \]
      • CNF_EQUIV_POS2

        public static final ProofRule CNF_EQUIV_POS2
        Boolean – CNF – Equiv Positive 2 \[ \inferrule{- \mid F_1 = F_2}{F_1 \neq F_2 \lor F_1 \lor \neg F_2} \]
      • CNF_EQUIV_NEG1

        public static final ProofRule CNF_EQUIV_NEG1
        Boolean – CNF – Equiv Negative 1 \[ \inferrule{- \mid F_1 = F_2}{(F_1 = F_2) \lor F_1 \lor F_2} \]
      • CNF_EQUIV_NEG2

        public static final ProofRule CNF_EQUIV_NEG2
        Boolean – CNF – Equiv Negative 2 \[ \inferrule{- \mid F_1 = F_2}{(F_1 = F_2) \lor \neg F_1 \lor \neg F_2} \]
      • CNF_XOR_POS1

        public static final ProofRule CNF_XOR_POS1
        Boolean – CNF – XOR Positive 1 \[ \inferrule{- \mid F_1 \xor F_2}{\neg(F_1 \xor F_2) \lor F_1 \lor F_2} \]
      • CNF_XOR_POS2

        public static final ProofRule CNF_XOR_POS2
        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} \]
      • CNF_XOR_NEG1

        public static final ProofRule CNF_XOR_NEG1
        Boolean – CNF – XOR Negative 1 \[ \inferrule{- \mid F_1 \xor F_2}{(F_1 \xor F_2) \lor \neg F_1 \lor F_2} \]
      • CNF_XOR_NEG2

        public static final ProofRule CNF_XOR_NEG2
        Boolean – CNF – XOR Negative 2 \[ \inferrule{- \mid F_1 \xor F_2}{(F_1 \xor F_2) \lor F_1 \lor \neg F_2} \]
      • CNF_ITE_POS1

        public static final ProofRule CNF_ITE_POS1
        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} \]
      • CNF_ITE_POS2

        public static final ProofRule CNF_ITE_POS2
        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} \]
      • CNF_ITE_POS3

        public static final ProofRule CNF_ITE_POS3
        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} \]
      • CNF_ITE_NEG1

        public static final ProofRule CNF_ITE_NEG1
        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} \]
      • CNF_ITE_NEG2

        public static final ProofRule CNF_ITE_NEG2
        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} \]
      • CNF_ITE_NEG3

        public static final ProofRule CNF_ITE_NEG3
        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} \]
      • REFL

        public static final ProofRule REFL
        Equality – Reflexivity \[ \inferrule{-\mid t}{t = t} \]
      • SYMM

        public static final ProofRule SYMM
        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} \]
      • TRANS

        public static final ProofRule TRANS
        Equality – Transitivity \[ \inferrule{t_1=t_2,\dots,t_{n-1}=t_n\mid -}{t_1 = t_n} \]
      • CONG

        public static final ProofRule CONG
        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.{@link 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 <cvc5.HO_CONG> proof rule.
      • NARY_CONG

        public static final ProofRule NARY_CONG
        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.
      • TRUE_INTRO

        public static final ProofRule TRUE_INTRO
        Equality – True intro \[ \inferrule{F\mid -}{F = \top} \]
      • TRUE_ELIM

        public static final ProofRule TRUE_ELIM
        Equality – True elim \[ \inferrule{F=\top\mid -}{F} \]
      • FALSE_INTRO

        public static final ProofRule FALSE_INTRO
        Equality – False intro \[ \inferrule{\neg F\mid -}{F = \bot} \]
      • FALSE_ELIM

        public static final ProofRule FALSE_ELIM
        Equality – False elim \[ \inferrule{F=\bot\mid -}{\neg F} \]
      • HO_APP_ENCODE

        public static final ProofRule HO_APP_ENCODE
        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.
      • HO_CONG

        public static final ProofRule HO_CONG
        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`.
      • BETA_REDUCE

        public static final ProofRule BETA_REDUCE
        Equality – Beta reduction \[ \inferrule{\mid \lambda x_1\dots x_n.\> t, t_1,\dots,t_n} {((\lambda x_1\dots x_n.\> t) t_1 \ldots t_n)=t\{x_1\mapsto t_1,\dots,x_n\mapsto t_n\}} \] The right hand side of the equality in the conclusion is computed using standard substitution via Node.substitute.
      • ARRAYS_READ_OVER_WRITE

        public static final ProofRule ARRAYS_READ_OVER_WRITE
        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)} \]
      • ARRAYS_READ_OVER_WRITE_CONTRA

        public static final ProofRule ARRAYS_READ_OVER_WRITE_CONTRA
        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} \]
      • ARRAYS_READ_OVER_WRITE_1

        public static final ProofRule ARRAYS_READ_OVER_WRITE_1
        Arrays – Read over write 1 \[ \inferrule{-\mid \mathit{select}(\mathit{store}(a,i,e),i)} {\mathit{select}(\mathit{store}(a,i,e),i)=e} \]
      • ARRAYS_EXT

        public static final ProofRule ARRAYS_EXT
        Arrays – Arrays extensionality \[ \inferrule{a \neq b\mid -} {\mathit{select}(a,k)\neq\mathit{select}(b,k)} \] where \(k\) is \(\texttt{arrays::SkolemCache::getExtIndexSkolem}(a\neq b)\).
      • ARRAYS_EQ_RANGE_EXPAND

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

        public static final ProofRule MACRO_BV_BITBLAST
        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.
      • BV_BITBLAST_STEP

        public static final ProofRule BV_BITBLAST_STEP
        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)\).
      • BV_EAGER_ATOM

        public static final ProofRule BV_EAGER_ATOM
        Bit-vectors – Bit-vector eager atom \[ \inferrule{-\mid F}{F = F[0]} \] where \(F\) is of kind BITVECTOR_EAGER_ATOM.
      • DT_UNIF

        public static final ProofRule DT_UNIF
        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.
      • DT_INST

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

        public static final ProofRule DT_COLLAPSE
        Datatypes – Collapse \[ \inferrule{-\mid \mathit{sel}_i(C_j(t_1,\dots,t_n))}{ \mathit{sel}_i(C_j(t_1,\dots,t_n)) = r} \] where \(C_j\) is a constructor, \(r\) is \(t_i\) if \(\mathit{sel}_i\) is a correctly applied selector, or {@link TypeNode#mkGroundTerm()} of the proper type otherwise. Notice that the use of mkGroundTerm differs from the rewriter which uses mkGroundValue in this case.
      • DT_SPLIT

        public static final ProofRule DT_SPLIT
        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\).
      • DT_CLASH

        public static final ProofRule DT_CLASH
        Datatypes – Clash \[ \inferruleSC{\mathit{is}_{C_i}(t), \mathit{is}_{C_j}(t)\mid -}{\bot} {if $i\neq j$} \]
      • SKOLEM_INTRO

        public static final ProofRule SKOLEM_INTRO
        Quantifiers – Skolem introduction \[ \inferrule{-\mid k}{k = t} \] where \(t\) is the unpurified form of skolem \(k\).
      • SKOLEMIZE

        public static final ProofRule SKOLEMIZE
        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.
      • INSTANTIATE

        public static final ProofRule INSTANTIATE
        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.
      • ALPHA_EQUIV

        public static final ProofRule ALPHA_EQUIV
        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.
      • CONCAT_EQ

        public static final ProofRule CONCAT_EQ
        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.
      • CONCAT_UNIFY

        public static final ProofRule CONCAT_UNIFY
        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.
      • CONCAT_CONFLICT

        public static final ProofRule CONCAT_CONFLICT
        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.
      • CONCAT_CONFLICT_DEQ

        public static final ProofRule CONCAT_CONFLICT_DEQ
        Strings – Core rules – Concatenation conflict for disequal characters \[ \inferrule{(t_1\cdot t) = (s_1 \cdot s), t_1 \deq 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.
      • CONCAT_SPLIT

        public static final ProofRule CONCAT_SPLIT
        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_t) \vee (s_1 = t_1\cdot r_s)}{if $b=\bot$} \] where \(r_t\) is \(\mathit{skolem}(\mathit{suf}(t_1,\mathit{len}(s_1)))\) and \(r_s\) is \(\mathit{skolem}(\mathit{suf}(s_1,\mathit{len}(t_1)))\). \[ \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_t) \vee (s_1 = t_1\cdot r_s)}{if $b=\top$} \] where \(r_t\) is \(\mathit{skolem}(\mathit{pre}(t_2,\mathit{len}(t_2) - \mathit{len}(s_2)))\) and \(r_s\) is \(\mathit{skolem}(\mathit{pre}(s_2,\mathit{len}(s_2) - \mathit{len}(t_2)))\). 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)\).
      • CONCAT_CSPLIT

        public static final ProofRule CONCAT_CSPLIT
        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))\).
      • CONCAT_LPROP

        public static final ProofRule CONCAT_LPROP
        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_t)} \] where \(r_t\) is \(\mathit{skolem}(\mathit{suf}(t_1,\mathit{len}(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 = r_t\cdot s_2)} \] where \(r_t\) is \(\mathit{skolem}(\mathit{pre}(t_2,\mathit{len}(t_2) - \mathit{len}(s_2)))\).
      • CONCAT_CPROP

        public static final ProofRule CONCAT_CPROP
        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 = w_3\cdot r)} \] where \(w_1,\,w_2,\,w_3\) are words, \(w_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 w_3)} \] where \(w_1,\,w_2,\,w_3\) are words, \(w_3\) is \(\mathit{suf}(w_2, \mathit{len}(w_2) - 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\).
      • STRING_DECOMPOSE

        public static final ProofRule STRING_DECOMPOSE
        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)\).
      • STRING_LENGTH_POS

        public static final ProofRule STRING_LENGTH_POS
        Strings – Core rules – Length positive \[ \inferrule{-\mid t}{(\mathit{len}(t) = 0\wedge t= '')\vee \mathit{len}(t) > 0} \]
      • STRING_LENGTH_NON_EMPTY

        public static final ProofRule STRING_LENGTH_NON_EMPTY
        Strings – Core rules – Length non-empty \[ \inferrule{t\neq ''\mid -}{\mathit{len}(t) \neq 0} \]
      • STRING_REDUCTION

        public static final ProofRule STRING_REDUCTION
        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\).
      • STRING_EAGER_REDUCTION

        public static final ProofRule STRING_EAGER_REDUCTION
        Strings – Extended functions – Eager reduction \[ \inferrule{-\mid t}{R} \] where \(R\) is \(\texttt{strings::TermRegistry::eagerReduce}(t)\).
      • RE_INTER

        public static final ProofRule RE_INTER
        Strings – Regular expressions – Intersection \[ \inferrule{t\in R_1,\,t\in R_2\mid -}{t\in \mathit{inter}(R_1,R_2)} \]
      • RE_UNFOLD_POS

        public static final ProofRule RE_UNFOLD_POS
        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.
      • RE_UNFOLD_NEG

        public static final ProofRule RE_UNFOLD_NEG
        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.
      • RE_UNFOLD_NEG_CONCAT_FIXED

        public static final ProofRule RE_UNFOLD_NEG_CONCAT_FIXED
        Strings – Regular expressions – Unfold negative concatenation, fixed \[ \inferrule{t\not\in R\mid -}{\texttt{RegExpOpr::reduceRegExpNegConcatFixed}(t\not\in R,L,i)} \] where \(\texttt{RegExpOpr::getRegExpConcatFixed}(t\not\in R, i) = L\), corresponding to the one-step unfolding of the premise, optimized for fixed length of component \(i\) of the regular expression concatenation \(R\).
      • RE_ELIM

        public static final ProofRule RE_ELIM
        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\).
      • STRING_CODE_INJ

        public static final ProofRule STRING_CODE_INJ
        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} \]
      • STRING_SEQ_UNIT_INJ

        public static final ProofRule STRING_SEQ_UNIT_INJ
        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.
      • MACRO_STRING_INFERENCE

        public static final ProofRule MACRO_STRING_INFERENCE
        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}\).
      • MACRO_ARITH_SCALE_SUM_UB

        public static final ProofRule MACRO_ARITH_SCALE_SUM_UB
        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: \[ 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 \]
      • ARITH_SUM_UB

        public static final ProofRule ARITH_SUM_UB
        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\).
      • INT_TIGHT_UB

        public static final ProofRule INT_TIGHT_UB
        Arithmetic – Tighten strict integer upper bounds \[ \inferrule{i < c \mid -}{i \leq \lfloor c \rfloor} \] where \(i\) has integer type.
      • INT_TIGHT_LB

        public static final ProofRule INT_TIGHT_LB
        Arithmetic – Tighten strict integer lower bounds \[ \inferrule{i > c \mid -}{i \geq \lceil c \rceil} \] where \(i\) has integer type.
      • ARITH_TRICHOTOMY

        public static final ProofRule ARITH_TRICHOTOMY
        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.
      • ARITH_OP_ELIM_AXIOM

        public static final ProofRule ARITH_OP_ELIM_AXIOM
        Arithmetic – Operator elimination \[ \inferrule{- \mid t}{\texttt{arith::OperatorElim::getAxiomFor(t)}} \]
      • ARITH_POLY_NORM

        public static final ProofRule ARITH_POLY_NORM
        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.
      • ARITH_MULT_SIGN

        public static final ProofRule ARITH_MULT_SIGN
        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.
      • ARITH_MULT_POS

        public static final ProofRule ARITH_MULT_POS
        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.
      • ARITH_MULT_NEG

        public static final ProofRule ARITH_MULT_NEG
        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.
      • ARITH_MULT_TANGENT

        public static final ProofRule ARITH_MULT_TANGENT
        Arithmetic – Multiplication tangent plane \[ \inferruleSC{- \mid t, 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 t, 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$} \] where \(x,y\) are real terms (variables or extended terms), \(t = x \cdot y\) (possibly under rewriting), \(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)\).
      • ARITH_TRANS_PI

        public static final ProofRule ARITH_TRANS_PI
        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\).
      • ARITH_TRANS_EXP_NEG

        public static final ProofRule ARITH_TRANS_EXP_NEG
        Arithmetic – Transcendentals – Exp at negative values \[ \inferrule{- \mid t}{(t < 0) \leftrightarrow (\exp(t) < 1)} \]
      • ARITH_TRANS_EXP_POSITIVITY

        public static final ProofRule ARITH_TRANS_EXP_POSITIVITY
        Arithmetic – Transcendentals – Exp is always positive \[ \inferrule{- \mid t}{\exp(t) > 0} \]
      • ARITH_TRANS_EXP_SUPER_LIN

        public static final ProofRule ARITH_TRANS_EXP_SUPER_LIN
        Arithmetic – Transcendentals – Exp grows super-linearly for positive values \[ \inferrule{- \mid t}{t \leq 0 \lor \exp(t) > t+1} \]
      • ARITH_TRANS_EXP_ZERO

        public static final ProofRule ARITH_TRANS_EXP_ZERO
        Arithmetic – Transcendentals – Exp at zero \[ \inferrule{- \mid t}{(t=0) \leftrightarrow (\exp(t) = 1)} \]
      • ARITH_TRANS_EXP_APPROX_ABOVE_NEG

        public static final ProofRule ARITH_TRANS_EXP_APPROX_ABOVE_NEG
        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\).
      • ARITH_TRANS_EXP_APPROX_ABOVE_POS

        public static final ProofRule ARITH_TRANS_EXP_APPROX_ABOVE_POS
        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\).
      • ARITH_TRANS_EXP_APPROX_BELOW

        public static final ProofRule ARITH_TRANS_EXP_APPROX_BELOW
        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!} \]
      • ARITH_TRANS_SINE_BOUNDS

        public static final ProofRule ARITH_TRANS_SINE_BOUNDS
        Arithmetic – Transcendentals – Sine is always between -1 and 1 \[ \inferrule{- \mid t}{\sin(t) \leq 1 \land \sin(t) \geq -1} \]
      • ARITH_TRANS_SINE_SHIFT

        public static final ProofRule ARITH_TRANS_SINE_SHIFT
        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.
      • ARITH_TRANS_SINE_SYMMETRY

        public static final ProofRule ARITH_TRANS_SINE_SYMMETRY
        Arithmetic – Transcendentals – Sine is symmetric with respect to negation of the argument \[ \inferrule{- \mid t}{\sin(t) - \sin(-t) = 0} \]
      • ARITH_TRANS_SINE_TANGENT_ZERO

        public static final ProofRule ARITH_TRANS_SINE_TANGENT_ZERO
        Arithmetic – Transcendentals – Sine is bounded by the tangent at zero .. math. \inferrule{- \mid t}{(t > 0 \rightarrow \sin(t) < t) \land (t < 0 \rightarrow \sin(t) > t)}
      • ARITH_TRANS_SINE_TANGENT_PI

        public static final ProofRule ARITH_TRANS_SINE_TANGENT_PI
        Arithmetic – Transcendentals – Sine is bounded by the tangents at -pi and pi .. math. \inferrule{- \mid t}{(t > -\pi \rightarrow \sin(t) > -\pi - t) \land (t < \pi \rightarrow \sin(t) < \pi - t)}
      • ARITH_TRANS_SINE_APPROX_ABOVE_NEG

        public static final ProofRule ARITH_TRANS_SINE_APPROX_ABOVE_NEG
        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\).
      • ARITH_TRANS_SINE_APPROX_ABOVE_POS

        public static final ProofRule ARITH_TRANS_SINE_APPROX_ABOVE_POS
        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)\).
      • ARITH_TRANS_SINE_APPROX_BELOW_NEG

        public static final ProofRule ARITH_TRANS_SINE_APPROX_BELOW_NEG
        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)\).
      • ARITH_TRANS_SINE_APPROX_BELOW_POS

        public static final ProofRule ARITH_TRANS_SINE_APPROX_BELOW_POS
        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\).
      • ARITH_NL_COVERING_DIRECT

        public static final ProofRule ARITH_NL_COVERING_DIRECT
        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: \[ \texttt{IRP}_k(poly) < x_i < \texttt{IRP}_k(poly) x_i = \texttt{IRP}_k(poly) \] 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.
      • ARITH_NL_COVERING_RECURSIVE

        public static final ProofRule ARITH_NL_COVERING_RECURSIVE
        Arithmetic – Coverings – Recursive interval See ARITH_NL_COVERING_DIRECT <cvc5.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.
      • LFSC_RULE

        public static final ProofRule LFSC_RULE
        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.
      • ALETHE_RULE

        public static final ProofRule ALETHE_RULE
        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.
      • UNKNOWN

        public static final ProofRule UNKNOWN
        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.
    • Method Detail

      • values

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

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

        public int getValue()