Proof Rules

This section introduces two enumerations: ProofRule and ProofRewriteRule.

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

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

enum class cvc5::ProofRule : uint32_t

An enumeration for proof rules. This enumeration is analogous to Kind for Node objects.

All proof rules are given as inference rules, presented in the following form:

\[\texttt{RULENAME}: \inferruleSC{\varphi_1 \dots \varphi_n \mid t_1 \dots t_m}{\psi}{if $C$}\]

where we call \(\varphi_i\) its premises or children, \(t_i\) its arguments, \(\psi\) its conclusion, and \(C\) its side condition. Alternatively, we can write the application of a proof rule as (RULENAME F1 ... Fn :args t1 ... tm), omitting the conclusion (since it can be uniquely determined from premises and arguments). Note that premises are sometimes given as proofs, i.e., application of proof rules, instead of formulas. This abuses the notation to see proof rule applications and their conclusions interchangeably.

Conceptually, the following proof rules form a calculus whose target user is the Node-level theory solvers. This means that the rules below are designed to reason about, among other things, common operations on Node objects like Rewriter::rewrite or Node::substitute. It is intended to be translated or printed in other formats.

The following ProofRule values include core rules and those categorized by theory, including the theory of equality.

The “core rules” include two distinguished rules which have special status: (1) ASSUME, which represents an open leaf in a proof; and (2) SCOPE, which encloses a scope (a subproof) with a set of scoped assumptions. The core rules additionally correspond to generic operations that are done internally on nodes, e.g., calling Rewriter::rewrite.

Rules with prefix MACRO_ are those that can be defined in terms of other rules. These exist for convenience and can be replaced by their definition in post-processing.

Values:

enumerator 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 (see below).

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

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

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

enumerator EVALUATE

Builtin theory – Evaluate

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

Note this is equivalent to: (REWRITE t MethodId::RW_EVALUATE).

enumerator ACI_NORM

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.++).

enumerator 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 theory/builtin/proof_checker.h.

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

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

enumerator 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 above.

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

enumerator DSL_REWRITE

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.

enumerator THEORY_REWRITE

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.

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

enumerator ITE_EQ

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)}}\]

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

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

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

enumerator DRAT_REFUTATION

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.

enumerator SAT_EXTERNAL_PROVE

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.

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

enumerator 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'\)

enumerator FACTORING

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.

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

enumerator 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

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

enumerator MACRO_RESOLUTION_TRUST

Boolean – N-ary Resolution + Factoring + Reordering unchecked

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

enumerator SPLIT

Boolean – Split

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

enumerator 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 + RESOLUTION.

enumerator 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 + RESOLUTION.

enumerator NOT_NOT_ELIM

Boolean – Double negation elimination

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

enumerator CONTRA

Boolean – Contradiction

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

enumerator AND_ELIM

Boolean – And elimination

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

enumerator AND_INTRO

Boolean – And introduction

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

enumerator NOT_OR_ELIM

Boolean – Not Or elimination

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

enumerator IMPLIES_ELIM

Boolean – Implication elimination

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

enumerator NOT_IMPLIES_ELIM1

Boolean – Not Implication elimination version 1

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

enumerator NOT_IMPLIES_ELIM2

Boolean – Not Implication elimination version 2

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

enumerator EQUIV_ELIM1

Boolean – Equivalence elimination version 1

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

enumerator EQUIV_ELIM2

Boolean – Equivalence elimination version 2

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

enumerator NOT_EQUIV_ELIM1

Boolean – Not Equivalence elimination version 1

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

enumerator NOT_EQUIV_ELIM2

Boolean – Not Equivalence elimination version 2

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

enumerator XOR_ELIM1

Boolean – XOR elimination version 1

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

enumerator XOR_ELIM2

Boolean – XOR elimination version 2

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

enumerator NOT_XOR_ELIM1

Boolean – Not XOR elimination version 1

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

enumerator NOT_XOR_ELIM2

Boolean – Not XOR elimination version 2

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

enumerator ITE_ELIM1

Boolean – ITE elimination version 1

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

enumerator ITE_ELIM2

Boolean – ITE elimination version 2

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

enumerator NOT_ITE_ELIM1

Boolean – Not ITE elimination version 1

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

enumerator NOT_ITE_ELIM2

Boolean – Not ITE elimination version 2

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

enumerator 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}\]

enumerator 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}\]

enumerator 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}\]

enumerator 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}\]

enumerator 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}\]

enumerator 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}\]

enumerator CNF_IMPLIES_NEG1

Boolean – CNF – Implies Negative 1

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

enumerator CNF_IMPLIES_NEG2

Boolean – CNF – Implies Negative 2

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

enumerator 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}\]

enumerator 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}\]

enumerator CNF_EQUIV_NEG1

Boolean – CNF – Equiv Negative 1

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

enumerator 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}\]

enumerator 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}\]

enumerator 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}\]

enumerator 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}\]

enumerator 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}\]

enumerator 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}\]

enumerator 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}\]

enumerator 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}\]

enumerator 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}\]

enumerator 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}\]

enumerator 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}\]

enumerator REFL

Equality – Reflexivity

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

enumerator 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}\]

enumerator TRANS

Equality – Transitivity

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

enumerator 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::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.

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

enumerator TRUE_INTRO

Equality – True intro

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

enumerator TRUE_ELIM

Equality – True elim

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

enumerator FALSE_INTRO

Equality – False intro

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

enumerator FALSE_ELIM

Equality – False elim

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

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

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

enumerator 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)}\]

enumerator 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}\]

enumerator 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}\]

enumerator ARRAYS_EXT

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

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

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

enumerator BV_EAGER_ATOM

Bit-vectors – Bit-vector eager atom

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

where \(F\) is of kind BITVECTOR_EAGER_ATOM.

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

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

enumerator DT_CLASH

Datatypes – Clash

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

enumerator SKOLEM_INTRO

Quantifiers – Skolem introduction

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

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

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

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

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

enumerator SETS_SINGLETON_INJ

Sets – Singleton injectivity

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

enumerator SETS_EXT

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

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

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

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

enumerator CONCAT_CONFLICT_DEQ

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.

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

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

enumerator 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)}\]

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

enumerator 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 = 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\).

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

enumerator STRING_LENGTH_POS

Strings – Core rules – Length positive

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

enumerator STRING_LENGTH_NON_EMPTY

Strings – Core rules – Length non-empty

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

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

enumerator STRING_EAGER_REDUCTION

Strings – Extended functions – Eager reduction

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

where \(R\) is \(\texttt{strings::TermRegistry::eagerReduce}(t)\).

enumerator RE_INTER

Strings – Regular expressions – Intersection

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

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

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

enumerator RE_UNFOLD_NEG_CONCAT_FIXED

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

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

enumerator 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}\]

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

enumerator 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}\).

enumerator 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:

\[ \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} \]

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

enumerator INT_TIGHT_UB

Arithmetic – Tighten strict integer upper bounds

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

where \(i\) has integer type.

enumerator INT_TIGHT_LB

Arithmetic – Tighten strict integer lower bounds

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

where \(i\) has integer type.

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

enumerator ARITH_OP_ELIM_AXIOM

Arithmetic – Operator elimination

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

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

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

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

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

enumerator ARITH_MULT_TANGENT

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

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

enumerator ARITH_TRANS_EXP_NEG

Arithmetic – Transcendentals – Exp at negative values

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

enumerator ARITH_TRANS_EXP_POSITIVITY

Arithmetic – Transcendentals – Exp is always positive

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

enumerator 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}\]

enumerator ARITH_TRANS_EXP_ZERO

Arithmetic – Transcendentals – Exp at zero

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

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

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

enumerator 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!}\]

enumerator 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}\]

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

enumerator ARITH_TRANS_SINE_SYMMETRY

Arithmetic – Transcendentals – Sine is symmetric with respect to negation of the argument

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

enumerator ARITH_TRANS_SINE_TANGENT_ZERO

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)} \]

enumerator ARITH_TRANS_SINE_TANGENT_PI

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)} \]

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

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

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

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

enumerator 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:

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

enumerator ARITH_NL_COVERING_RECURSIVE

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.

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

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

enumerator UNKNOWN

enum class cvc5::ProofRewriteRule : uint32_t

This enumeration represents the rewrite rules used in a rewrite proof. Some of the rules are internal ad-hoc rewrites, while others are rewrites specified by the RARE DSL. This enumeration is used as the first argument to the DSL_REWRITE proof rule and the THEORY_REWRITE proof rule.

Values:

enumerator NONE

enumerator DISTINCT_ELIM

Builtin – Distinct elimination

\[\texttt{distinct}(t_1, \ldots, tn) = \bigwedge_{i \neq j} t_i \neq t_j\]

enumerator BETA_REDUCE

Equality – Beta reduction

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

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

enumerator ARRAYS_EQ_RANGE_EXPAND

Arrays – Expansion of array range equality

\[\mathit{eqrange}(a,b,i,j)= \forall x.\> i \leq x \leq j \rightarrow \mathit{select}(a,x)=\mathit{select}(b,x)\]

enumerator EXISTS_ELIM

Quantifiers – Exists elimination

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

enumerator DT_INST

Datatypes – Instantiation

\[\mathit{is}_C(t) = (t = C(\mathit{sel}_1(t),\dots,\mathit{sel}_n(t)))\]

where \(C\) is the \(n^{\mathit{th}}\) constructor of the type of \(t\), and \(\mathit{is}_C\) is the discriminator (tester) for \(C\).

enumerator DT_COLLAPSE_SELECTOR

Datatypes - collapse selector

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

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

enumerator DT_COLLAPSE_TESTER

Datatypes - collapse tester

\[\mathit{is}_c(c(t_1, \ldots, t_n)) = true\]

or alternatively

\[\mathit{is}_c(d(t_1, \ldots, t_n)) = false\]

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

enumerator DT_COLLAPSE_TESTER_SINGLETON

Datatypes - collapse tester

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

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

enumerator DT_CONS_EQ

Datatypes - constructor equality

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

or alternatively

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

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

enumerator RE_LOOP_ELIM

Strings - regular expression loop elimination

\[((\_\ re.loop\ l\ u)\ R) = (re.union\ R^l \ldots R^u)\]

where \(u \geq l\).

enumerator SETS_IS_EMPTY_EVAL

Sets - empty tester evaluation

\[\mathit{sets.is\_empty}(as \ \mathit{set.empty} \ (\mathit{Set} \ T)) = \top\]

or alternatively:

\[\mathit{sets.is\_empty}(c) = \bot\]

where \(c\) is a constant set that is not the empty set.

enumerator ARITH_PLUS_ZERO

Auto-generated from RARE rule arith-plus-zero

enumerator ARITH_MUL_ONE

Auto-generated from RARE rule arith-mul-one

enumerator ARITH_MUL_ZERO

Auto-generated from RARE rule arith-mul-zero

enumerator ARITH_INT_DIV_ONE

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

enumerator ARITH_NEG_NEG_ONE

Auto-generated from RARE rule arith-neg-neg-one

enumerator ARITH_ELIM_UMINUS

Auto-generated from RARE rule arith-elim-uminus

enumerator ARITH_ELIM_MINUS

Auto-generated from RARE rule arith-elim-minus

enumerator ARITH_ELIM_GT

Auto-generated from RARE rule arith-elim-gt

enumerator ARITH_ELIM_LT

Auto-generated from RARE rule arith-elim-lt

enumerator ARITH_ELIM_LEQ

Auto-generated from RARE rule arith-elim-leq

enumerator ARITH_LEQ_NORM

Auto-generated from RARE rule arith-leq-norm

enumerator ARITH_GEQ_TIGHTEN

Auto-generated from RARE rule arith-geq-tighten

enumerator ARITH_GEQ_NORM

Auto-generated from RARE rule arith-geq-norm

enumerator ARITH_REFL_LEQ

Auto-generated from RARE rule arith-refl-leq

enumerator ARITH_REFL_LT

Auto-generated from RARE rule arith-refl-lt

enumerator ARITH_REFL_GEQ

Auto-generated from RARE rule arith-refl-geq

enumerator ARITH_REFL_GT

Auto-generated from RARE rule arith-refl-gt

enumerator ARITH_PLUS_FLATTEN

Auto-generated from RARE rule arith-plus-flatten

enumerator ARITH_MULT_FLATTEN

Auto-generated from RARE rule arith-mult-flatten

enumerator ARITH_MULT_DIST

Auto-generated from RARE rule arith-mult-dist

enumerator ARITH_PLUS_CANCEL1

Auto-generated from RARE rule arith-plus-cancel1

enumerator ARITH_PLUS_CANCEL2

Auto-generated from RARE rule arith-plus-cancel2

enumerator ARRAY_READ_OVER_WRITE

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

enumerator ARRAY_READ_OVER_WRITE2

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

enumerator ARRAY_STORE_OVERWRITE

Auto-generated from RARE rule array-store-overwrite

enumerator ARRAY_STORE_SELF

Auto-generated from RARE rule array-store-self

enumerator BOOL_DOUBLE_NOT_ELIM

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

enumerator BOOL_EQ_TRUE

Auto-generated from RARE rule bool-eq-true

enumerator BOOL_EQ_FALSE

Auto-generated from RARE rule bool-eq-false

enumerator BOOL_EQ_NREFL

Auto-generated from RARE rule bool-eq-nrefl

enumerator BOOL_IMPL_FALSE1

Auto-generated from RARE rule bool-impl-false1

enumerator BOOL_IMPL_FALSE2

Auto-generated from RARE rule bool-impl-false2

enumerator BOOL_IMPL_TRUE1

Auto-generated from RARE rule bool-impl-true1

enumerator BOOL_IMPL_TRUE2

Auto-generated from RARE rule bool-impl-true2

enumerator BOOL_IMPL_ELIM

Auto-generated from RARE rule bool-impl-elim

enumerator BOOL_OR_TRUE

Auto-generated from RARE rule bool-or-true

enumerator BOOL_OR_FALSE

Auto-generated from RARE rule bool-or-false

enumerator BOOL_OR_FLATTEN

Auto-generated from RARE rule bool-or-flatten

enumerator BOOL_OR_DUP

Auto-generated from RARE rule bool-or-dup

enumerator BOOL_AND_TRUE

Auto-generated from RARE rule bool-and-true

enumerator BOOL_AND_FALSE

Auto-generated from RARE rule bool-and-false

enumerator BOOL_AND_FLATTEN

Auto-generated from RARE rule bool-and-flatten

enumerator BOOL_AND_DUP

Auto-generated from RARE rule bool-and-dup

enumerator BOOL_AND_CONF

Auto-generated from RARE rule bool-and-conf

enumerator BOOL_OR_TAUT

Auto-generated from RARE rule bool-or-taut

enumerator BOOL_XOR_REFL

Auto-generated from RARE rule bool-xor-refl

enumerator BOOL_XOR_NREFL

Auto-generated from RARE rule bool-xor-nrefl

enumerator BOOL_XOR_FALSE

Auto-generated from RARE rule bool-xor-false

enumerator BOOL_XOR_TRUE

Auto-generated from RARE rule bool-xor-true

enumerator BOOL_XOR_COMM

Auto-generated from RARE rule bool-xor-comm

enumerator BOOL_XOR_ELIM

Auto-generated from RARE rule bool-xor-elim

enumerator ITE_NEG_BRANCH

Auto-generated from RARE rule ite-neg-branch

enumerator ITE_THEN_TRUE

Auto-generated from RARE rule ite-then-true

enumerator ITE_ELSE_FALSE

Auto-generated from RARE rule ite-else-false

enumerator ITE_THEN_FALSE

Auto-generated from RARE rule ite-then-false

enumerator ITE_ELSE_TRUE

Auto-generated from RARE rule ite-else-true

enumerator ITE_THEN_LOOKAHEAD_SELF

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

enumerator ITE_ELSE_LOOKAHEAD_SELF

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

enumerator ITE_TRUE_COND

Auto-generated from RARE rule ite-true-cond

enumerator ITE_FALSE_COND

Auto-generated from RARE rule ite-false-cond

enumerator ITE_NOT_COND

Auto-generated from RARE rule ite-not-cond

enumerator ITE_EQ_BRANCH

Auto-generated from RARE rule ite-eq-branch

enumerator ITE_THEN_LOOKAHEAD

Auto-generated from RARE rule ite-then-lookahead

enumerator ITE_ELSE_LOOKAHEAD

Auto-generated from RARE rule ite-else-lookahead

enumerator ITE_THEN_NEG_LOOKAHEAD

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

enumerator ITE_ELSE_NEG_LOOKAHEAD

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

enumerator BV_CONCAT_FLATTEN

Auto-generated from RARE rule bv-concat-flatten

enumerator BV_CONCAT_EXTRACT_MERGE

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

enumerator BV_EXTRACT_EXTRACT

Auto-generated from RARE rule bv-extract-extract

enumerator BV_EXTRACT_WHOLE

Auto-generated from RARE rule bv-extract-whole

enumerator BV_EXTRACT_CONCAT_1

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

enumerator BV_EXTRACT_CONCAT_2

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

enumerator BV_EXTRACT_CONCAT_3

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

enumerator BV_EXTRACT_CONCAT_4

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

enumerator BV_EXTRACT_BITWISE_AND

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

enumerator BV_EXTRACT_BITWISE_OR

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

enumerator BV_EXTRACT_BITWISE_XOR

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

enumerator BV_EXTRACT_NOT

Auto-generated from RARE rule bv-extract-not

enumerator BV_EXTRACT_SIGN_EXTEND_1

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

enumerator BV_EXTRACT_SIGN_EXTEND_2

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

enumerator BV_EXTRACT_SIGN_EXTEND_3

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

enumerator BV_NEG_MULT

Auto-generated from RARE rule bv-neg-mult

enumerator BV_NEG_ADD

Auto-generated from RARE rule bv-neg-add

enumerator BV_MULT_DISTRIB_CONST_NEG

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

enumerator BV_MULT_DISTRIB_CONST_ADD

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

enumerator BV_MULT_DISTRIB_CONST_SUB

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

enumerator BV_MULT_DISTRIB_1

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

enumerator BV_MULT_DISTRIB_2

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

enumerator BV_NOT_XOR

Auto-generated from RARE rule bv-not-xor

enumerator BV_AND_SIMPLIFY_1

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

enumerator BV_AND_SIMPLIFY_2

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

enumerator BV_OR_SIMPLIFY_1

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

enumerator BV_OR_SIMPLIFY_2

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

enumerator BV_XOR_SIMPLIFY_1

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

enumerator BV_XOR_SIMPLIFY_2

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

enumerator BV_XOR_SIMPLIFY_3

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

enumerator BV_ULT_ADD_ONE

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

enumerator BV_CONCAT_TO_MULT

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

enumerator BV_MULT_SLT_MULT_1

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

enumerator BV_MULT_SLT_MULT_2

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

enumerator BV_COMMUTATIVE_AND

Auto-generated from RARE rule bv-commutative-and

enumerator BV_COMMUTATIVE_OR

Auto-generated from RARE rule bv-commutative-or

enumerator BV_COMMUTATIVE_XOR

Auto-generated from RARE rule bv-commutative-xor

enumerator BV_COMMUTATIVE_MUL

Auto-generated from RARE rule bv-commutative-mul

enumerator BV_OR_ZERO

Auto-generated from RARE rule bv-or-zero

enumerator BV_MUL_ONE

Auto-generated from RARE rule bv-mul-one

enumerator BV_MUL_ZERO

Auto-generated from RARE rule bv-mul-zero

enumerator BV_ADD_ZERO

Auto-generated from RARE rule bv-add-zero

enumerator BV_ADD_TWO

Auto-generated from RARE rule bv-add-two

enumerator BV_ZERO_EXTEND_ELIMINATE_0

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

enumerator BV_SIGN_EXTEND_ELIMINATE_0

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

enumerator BV_NOT_NEQ

Auto-generated from RARE rule bv-not-neq

enumerator BV_ULT_ONES

Auto-generated from RARE rule bv-ult-ones

enumerator BV_OR_FLATTEN

Auto-generated from RARE rule bv-or-flatten

enumerator BV_XOR_FLATTEN

Auto-generated from RARE rule bv-xor-flatten

enumerator BV_AND_FLATTEN

Auto-generated from RARE rule bv-and-flatten

enumerator BV_MUL_FLATTEN

Auto-generated from RARE rule bv-mul-flatten

enumerator BV_CONCAT_MERGE_CONST

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

enumerator BV_COMMUTATIVE_ADD

Auto-generated from RARE rule bv-commutative-add

enumerator BV_NEG_SUB

Auto-generated from RARE rule bv-neg-sub

enumerator BV_NEG_IDEMP

Auto-generated from RARE rule bv-neg-idemp

enumerator BV_SUB_ELIMINATE

Auto-generated from RARE rule bv-sub-eliminate

enumerator BV_UGT_ELIMINATE

Auto-generated from RARE rule bv-ugt-eliminate

enumerator BV_UGE_ELIMINATE

Auto-generated from RARE rule bv-uge-eliminate

enumerator BV_SGT_ELIMINATE

Auto-generated from RARE rule bv-sgt-eliminate

enumerator BV_SGE_ELIMINATE

Auto-generated from RARE rule bv-sge-eliminate

enumerator BV_SLT_ELIMINATE

Auto-generated from RARE rule bv-slt-eliminate

enumerator BV_SLE_ELIMINATE

Auto-generated from RARE rule bv-sle-eliminate

enumerator BV_REDOR_ELIMINATE

Auto-generated from RARE rule bv-redor-eliminate

enumerator BV_REDAND_ELIMINATE

Auto-generated from RARE rule bv-redand-eliminate

enumerator BV_ULE_ELIMINATE

Auto-generated from RARE rule bv-ule-eliminate

enumerator BV_COMP_ELIMINATE

Auto-generated from RARE rule bv-comp-eliminate

enumerator BV_REPEAT_ELIMINATE_1

Auto-generated from RARE rule bv-repeat-eliminate-1

enumerator BV_REPEAT_ELIMINATE_2

Auto-generated from RARE rule bv-repeat-eliminate-2

enumerator BV_ROTATE_LEFT_ELIMINATE_1

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

enumerator BV_ROTATE_LEFT_ELIMINATE_2

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

enumerator BV_ROTATE_RIGHT_ELIMINATE_1

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

enumerator BV_ROTATE_RIGHT_ELIMINATE_2

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

enumerator BV_NAND_ELIMINATE

Auto-generated from RARE rule bv-nand-eliminate

enumerator BV_NOR_ELIMINATE

Auto-generated from RARE rule bv-nor-eliminate

enumerator BV_XNOR_ELIMINATE

Auto-generated from RARE rule bv-xnor-eliminate

enumerator BV_SDIV_ELIMINATE

Auto-generated from RARE rule bv-sdiv-eliminate

enumerator BV_SDIV_ELIMINATE_FEWER_BITWISE_OPS

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

enumerator BV_ZERO_EXTEND_ELIMINATE

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

enumerator BV_SIGN_EXTEND_ELIMINATE

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

enumerator BV_UADDO_ELIMINATE

Auto-generated from RARE rule bv-uaddo-eliminate

enumerator BV_SADDO_ELIMINATE

Auto-generated from RARE rule bv-saddo-eliminate

enumerator BV_SDIVO_ELIMINATE

Auto-generated from RARE rule bv-sdivo-eliminate

enumerator BV_SMOD_ELIMINATE

Auto-generated from RARE rule bv-smod-eliminate

enumerator BV_SMOD_ELIMINATE_FEWER_BITWISE_OPS

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

enumerator BV_SREM_ELIMINATE

Auto-generated from RARE rule bv-srem-eliminate

enumerator BV_SREM_ELIMINATE_FEWER_BITWISE_OPS

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

enumerator BV_USUBO_ELIMINATE

Auto-generated from RARE rule bv-usubo-eliminate

enumerator BV_SSUBO_ELIMINATE

Auto-generated from RARE rule bv-ssubo-eliminate

enumerator BV_ITE_EQUAL_CHILDREN

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

enumerator BV_ITE_CONST_CHILDREN_1

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

enumerator BV_ITE_CONST_CHILDREN_2

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

enumerator BV_ITE_EQUAL_COND_1

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

enumerator BV_ITE_EQUAL_COND_2

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

enumerator BV_ITE_EQUAL_COND_3

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

enumerator BV_ITE_MERGE_THEN_IF

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

enumerator BV_ITE_MERGE_ELSE_IF

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

enumerator BV_ITE_MERGE_THEN_ELSE

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

enumerator BV_ITE_MERGE_ELSE_ELSE

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

enumerator BV_SHL_BY_CONST_0

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

enumerator BV_SHL_BY_CONST_1

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

enumerator BV_SHL_BY_CONST_2

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

enumerator BV_LSHR_BY_CONST_0

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

enumerator BV_LSHR_BY_CONST_1

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

enumerator BV_LSHR_BY_CONST_2

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

enumerator BV_ASHR_BY_CONST_0

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

enumerator BV_ASHR_BY_CONST_1

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

enumerator BV_ASHR_BY_CONST_2

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

enumerator BV_AND_CONCAT_PULLUP

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

enumerator BV_OR_CONCAT_PULLUP

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

enumerator BV_XOR_CONCAT_PULLUP

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

enumerator BV_BITWISE_IDEMP_1

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

enumerator BV_BITWISE_IDEMP_2

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

enumerator BV_AND_ZERO

Auto-generated from RARE rule bv-and-zero

enumerator BV_AND_ONE

Auto-generated from RARE rule bv-and-one

enumerator BV_OR_ONE

Auto-generated from RARE rule bv-or-one

enumerator BV_XOR_DUPLICATE

Auto-generated from RARE rule bv-xor-duplicate

enumerator BV_XOR_ONES

Auto-generated from RARE rule bv-xor-ones

enumerator BV_XOR_ZERO

Auto-generated from RARE rule bv-xor-zero

enumerator BV_BITWISE_NOT_AND

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

enumerator BV_BITWISE_NOT_OR

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

enumerator BV_XOR_NOT

Auto-generated from RARE rule bv-xor-not

enumerator BV_NOT_IDEMP

Auto-generated from RARE rule bv-not-idemp

enumerator BV_ULT_ZERO_1

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

enumerator BV_ULT_ZERO_2

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

enumerator BV_ULT_SELF

Auto-generated from RARE rule bv-ult-self

enumerator BV_LT_SELF

Auto-generated from RARE rule bv-lt-self

enumerator BV_ULE_SELF

Auto-generated from RARE rule bv-ule-self

enumerator BV_ULE_ZERO

Auto-generated from RARE rule bv-ule-zero

enumerator BV_ZERO_ULE

Auto-generated from RARE rule bv-zero-ule

enumerator BV_SLE_SELF

Auto-generated from RARE rule bv-sle-self

enumerator BV_ULE_MAX

Auto-generated from RARE rule bv-ule-max

enumerator BV_NOT_ULT

Auto-generated from RARE rule bv-not-ult

enumerator BV_NOT_ULE

Auto-generated from RARE rule bv-not-ule

enumerator BV_NOT_SLE

Auto-generated from RARE rule bv-not-sle

enumerator BV_MULT_POW2_1

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

enumerator BV_MULT_POW2_2

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

enumerator BV_MULT_POW2_2B

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

enumerator BV_EXTRACT_MULT_LEADING_BIT

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

enumerator BV_UDIV_POW2_NOT_ONE

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

enumerator BV_UDIV_ZERO

Auto-generated from RARE rule bv-udiv-zero

enumerator BV_UDIV_ONE

Auto-generated from RARE rule bv-udiv-one

enumerator BV_UREM_POW2_NOT_ONE

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

enumerator BV_UREM_ONE

Auto-generated from RARE rule bv-urem-one

enumerator BV_UREM_SELF

Auto-generated from RARE rule bv-urem-self

enumerator BV_SHL_ZERO

Auto-generated from RARE rule bv-shl-zero

enumerator BV_LSHR_ZERO

Auto-generated from RARE rule bv-lshr-zero

enumerator BV_ASHR_ZERO

Auto-generated from RARE rule bv-ashr-zero

enumerator BV_UGT_UREM

Auto-generated from RARE rule bv-ugt-urem

enumerator BV_ULT_ONE

Auto-generated from RARE rule bv-ult-one

enumerator BV_SLT_ZERO

Auto-generated from RARE rule bv-slt-zero

enumerator BV_MERGE_SIGN_EXTEND_1

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

enumerator BV_MERGE_SIGN_EXTEND_2

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

enumerator BV_MERGE_SIGN_EXTEND_3

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

enumerator BV_SIGN_EXTEND_EQ_CONST_1

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

enumerator BV_SIGN_EXTEND_EQ_CONST_2

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

enumerator BV_ZERO_EXTEND_EQ_CONST_1

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

enumerator BV_ZERO_EXTEND_EQ_CONST_2

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

enumerator BV_ZERO_EXTEND_ULT_CONST_1

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

enumerator BV_ZERO_EXTEND_ULT_CONST_2

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

enumerator BV_SIGN_EXTEND_ULT_CONST_1

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

enumerator BV_SIGN_EXTEND_ULT_CONST_2

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

enumerator BV_SIGN_EXTEND_ULT_CONST_3

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

enumerator BV_SIGN_EXTEND_ULT_CONST_4

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

enumerator SETS_EQ_SINGLETON_EMP

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

enumerator SETS_MEMBER_SINGLETON

Auto-generated from RARE rule sets-member-singleton

enumerator SETS_MEMBER_EMP

Auto-generated from RARE rule sets-member-emp

enumerator SETS_SUBSET_ELIM

Auto-generated from RARE rule sets-subset-elim

enumerator SETS_UNION_COMM

Auto-generated from RARE rule sets-union-comm

enumerator SETS_INTER_COMM

Auto-generated from RARE rule sets-inter-comm

enumerator SETS_INTER_EMP1

Auto-generated from RARE rule sets-inter-emp1

enumerator SETS_INTER_EMP2

Auto-generated from RARE rule sets-inter-emp2

enumerator SETS_MINUS_EMP1

Auto-generated from RARE rule sets-minus-emp1

enumerator SETS_MINUS_EMP2

Auto-generated from RARE rule sets-minus-emp2

enumerator SETS_UNION_EMP1

Auto-generated from RARE rule sets-union-emp1

enumerator SETS_UNION_EMP2

Auto-generated from RARE rule sets-union-emp2

enumerator SETS_INTER_MEMBER

Auto-generated from RARE rule sets-inter-member

enumerator SETS_MINUS_MEMBER

Auto-generated from RARE rule sets-minus-member

enumerator SETS_UNION_MEMBER

Auto-generated from RARE rule sets-union-member

enumerator SETS_CHOOSE_SINGLETON

Auto-generated from RARE rule sets-choose-singleton

enumerator SETS_CARD_SINGLETON

Auto-generated from RARE rule sets-card-singleton

enumerator SETS_CARD_UNION

Auto-generated from RARE rule sets-card-union

enumerator SETS_CARD_MINUS

Auto-generated from RARE rule sets-card-minus

enumerator SETS_CARD_EMP

Auto-generated from RARE rule sets-card-emp

enumerator STR_EQ_CTN_FALSE

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

enumerator STR_CONCAT_FLATTEN

Auto-generated from RARE rule str-concat-flatten

enumerator STR_CONCAT_FLATTEN_EQ

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

enumerator STR_CONCAT_FLATTEN_EQ_REV

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

enumerator STR_SUBSTR_EMPTY_STR

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

enumerator STR_SUBSTR_EMPTY_RANGE

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

enumerator STR_SUBSTR_EMPTY_START

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

enumerator STR_SUBSTR_EMPTY_START_NEG

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

enumerator STR_SUBSTR_EQ_EMPTY

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

enumerator STR_LEN_REPLACE_INV

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

enumerator STR_LEN_UPDATE_INV

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

enumerator STR_LEN_SUBSTR_IN_RANGE

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

enumerator STR_LEN_SUBSTR_UB1

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

enumerator STR_LEN_SUBSTR_UB2

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

enumerator RE_IN_EMPTY

Auto-generated from RARE rule re-in-empty

enumerator RE_IN_SIGMA

Auto-generated from RARE rule re-in-sigma

enumerator RE_IN_SIGMA_STAR

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

enumerator RE_IN_CSTRING

Auto-generated from RARE rule re-in-cstring

enumerator RE_IN_COMP

Auto-generated from RARE rule re-in-comp

enumerator STR_CONCAT_CLASH

Auto-generated from RARE rule str-concat-clash

enumerator STR_CONCAT_CLASH_REV

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

enumerator STR_CONCAT_CLASH2

Auto-generated from RARE rule str-concat-clash2

enumerator STR_CONCAT_CLASH2_REV

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

enumerator STR_CONCAT_UNIFY

Auto-generated from RARE rule str-concat-unify

enumerator STR_CONCAT_UNIFY_REV

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

enumerator STR_CONCAT_CLASH_CHAR

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

enumerator STR_CONCAT_CLASH_CHAR_REV

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

enumerator STR_PREFIXOF_ELIM

Auto-generated from RARE rule str-prefixof-elim

enumerator STR_SUFFIXOF_ELIM

Auto-generated from RARE rule str-suffixof-elim

enumerator STR_PREFIXOF_ONE

Auto-generated from RARE rule str-prefixof-one

enumerator STR_SUFFIXOF_ONE

Auto-generated from RARE rule str-suffixof-one

enumerator STR_SUBSTR_COMBINE1

Auto-generated from RARE rule str-substr-combine1

enumerator STR_SUBSTR_COMBINE2

Auto-generated from RARE rule str-substr-combine2

enumerator STR_SUBSTR_CONCAT1

Auto-generated from RARE rule str-substr-concat1

enumerator STR_SUBSTR_FULL

Auto-generated from RARE rule str-substr-full

enumerator STR_CONTAINS_REFL

Auto-generated from RARE rule str-contains-refl

enumerator STR_CONTAINS_CONCAT_FIND

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

enumerator STR_CONTAINS_SPLIT_CHAR

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

enumerator STR_CONTAINS_LEQ_LEN_EQ

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

enumerator STR_CONCAT_EMP

Auto-generated from RARE rule str-concat-emp

enumerator STR_AT_ELIM

Auto-generated from RARE rule str-at-elim

enumerator RE_ALL_ELIM

Auto-generated from RARE rule re-all-elim

enumerator RE_OPT_ELIM

Auto-generated from RARE rule re-opt-elim

enumerator RE_CONCAT_EMP

Auto-generated from RARE rule re-concat-emp

enumerator RE_CONCAT_NONE

Auto-generated from RARE rule re-concat-none

enumerator RE_CONCAT_FLATTEN

Auto-generated from RARE rule re-concat-flatten

enumerator RE_CONCAT_STAR_SWAP

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

enumerator RE_UNION_ALL

Auto-generated from RARE rule re-union-all

enumerator RE_UNION_NONE

Auto-generated from RARE rule re-union-none

enumerator RE_UNION_FLATTEN

Auto-generated from RARE rule re-union-flatten

enumerator RE_UNION_DUP

Auto-generated from RARE rule re-union-dup

enumerator RE_INTER_ALL

Auto-generated from RARE rule re-inter-all

enumerator RE_INTER_NONE

Auto-generated from RARE rule re-inter-none

enumerator RE_INTER_FLATTEN

Auto-generated from RARE rule re-inter-flatten

enumerator RE_INTER_DUP

Auto-generated from RARE rule re-inter-dup

enumerator STR_LEN_CONCAT_REC

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

enumerator STR_IN_RE_RANGE_ELIM

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

enumerator SEQ_LEN_UNIT

Auto-generated from RARE rule seq-len-unit

enumerator SEQ_NTH_UNIT

Auto-generated from RARE rule seq-nth-unit

enumerator SEQ_REV_UNIT

Auto-generated from RARE rule seq-rev-unit

enumerator EQ_REFL

Auto-generated from RARE rule eq-refl

enumerator EQ_SYMM

Auto-generated from RARE rule eq-symm

enumerator DISTINCT_BINARY_ELIM

Auto-generated from RARE rule distinct-binary-elim