Cvc5ProofRule and Cvc5ProofRewriteRule

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

Enum Cvc5ProofRewriteRule pertains to rewrites performed on terms. These identifiers are arguments of the proof rules CVC5_PROOF_RULE_THEORY_REWRITE and CVC5_PROOF_RULE_DSL_REWRITE.

enum Cvc5ProofRule

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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_MACRO_REWRITE

Builtin theory – Rewrite

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

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

enumerator CVC5_PROOF_RULE_EVALUATE

Builtin theory – Evaluate

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

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

Note this proof rule only applies to atomic sorts, that is, operators on Int, Real, String, Bool or BitVector.

enumerator CVC5_PROOF_RULE_DISTINCT_VALUES

Builtin theory – Distinct values

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

where $t$ and $s$ are distinct values.

Note that cvc5 internally has a notion of which terms denote “values”. This property is implemented for any sort that can appear in equalities. A term denotes a value if and only if it is the canonical representation of a value of that sort. For example, set values are a chain of unions of singleton sets whose elements are also values, where this chain is sorted. Any two distinct values are semantically disequal in all models.

In practice, we use this rule only to show the distinctness of non-atomic sort, e.g. Sets, Sequences, Datatypes, Arrays, etc.

Note that internally, the notion of value is implemented by the Node::isConst method.

enumerator CVC5_PROOF_RULE_ACI_NORM

Builtin theory – associative/commutative/idempotency/identity normalization

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

where $t$ and $s$ are equivalent modulo associativity and identity elements, and (optionally) commutativity and idempotency.

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, commutative and have an identity element (bvxor), (3) those that are associative and have an identity element (examples are concat, str.++, re.++).

This is implemented internally by checking that $\texttt{expr::isACINorm(t, s)} = \top$. For details, see expr/aci_norm.h.

enumerator CVC5_PROOF_RULE_ABSORB

Builtin theory – absorb

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

where $t$ contains $z$ as a subterm, where $z$ is a zero element.

In particular, $t$ is expected to be an application of a function with a zero element $z$, and $z$ is contained as a subterm of $t$ beneath applications of that function. For example, this may show that $(A \wedge ( B \wedge \bot)) = \bot$.

This is implemented internally by checking that $\texttt{expr::isAbsorb(t, z)} = \top$. For details, see expr/aci_norm.h.

enumerator CVC5_PROOF_RULE_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{rewrite}_{idr}(t \circ \sigma_{ids, ida}(F_n) \circ \cdots \circ \sigma_{ids, ida}(F_1))}\]

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

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

enumerator CVC5_PROOF_RULE_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{rewrite}_{idr}(F \circ \sigma_{ids, ida}(F_n) \circ \cdots \circ \sigma_{ids, ida}(F_1)) = \top$ and $ids$ and $idr$ are method identifiers.

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

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

enumerator CVC5_PROOF_RULE_MACRO_SR_PRED_ELIM

Builtin theory – Substitution + Rewriting predicate elimination

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

where $ids$ and $idr$ are method identifiers.

We rewrite only on the Skolem form of $F$, similar to MACRO_SR_EQ_INTRO.

enumerator CVC5_PROOF_RULE_MACRO_SR_PRED_TRANSFORM

Builtin theory – Substitution + Rewriting predicate elimination

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

where

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

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

enumerator CVC5_PROOF_RULE_ENCODE_EQ_INTRO

Builtin theory – Encode equality introduction

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

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

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

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

enumerator CVC5_PROOF_RULE_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 $\texttt{expr::narySubstitute}$ (for details, see expr/nary_term_util.h) which replaces each $x_i$ with the list $t_i$ in its place.

enumerator CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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,pol} C_2$ represent the resolution of $C_1$ with $C_2$ with pivot $L$ and polarity $pol$, as defined above
let $C_1' = C_1$,
for each $i > 1$, let $C_i' = C_{i-1} \diamond_{L_{i-1}, pol_{i-1}} C_i'$

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

The result of the chain resolution is $C = C_n'$

enumerator CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_REORDERING

Boolean – Reordering

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

where the multiset representations of $C_1$ and $C_2$ are the same.

enumerator CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_MACRO_RESOLUTION_TRUST

Boolean – N-ary Resolution + Factoring + Reordering unchecked

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

enumerator CVC5_PROOF_RULE_CHAIN_M_RESOLUTION

Boolean – Chain multiset resolution

This rule combines Resolution + Factoring + Reordering.

\[\inferrule{C_1 \dots C_n \mid C, (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 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 CVC5_PROOF_RULE_SPLIT

Boolean – Split

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

enumerator CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_NOT_NOT_ELIM

Boolean – Double negation elimination

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

enumerator CVC5_PROOF_RULE_CONTRA

Boolean – Contradiction

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

enumerator CVC5_PROOF_RULE_AND_ELIM

Boolean – And elimination

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

enumerator CVC5_PROOF_RULE_AND_INTRO

Boolean – And introduction

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

enumerator CVC5_PROOF_RULE_NOT_OR_ELIM

Boolean – Not Or elimination

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

enumerator CVC5_PROOF_RULE_IMPLIES_ELIM

Boolean – Implication elimination

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

enumerator CVC5_PROOF_RULE_NOT_IMPLIES_ELIM1

Boolean – Not Implication elimination version 1

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

enumerator CVC5_PROOF_RULE_NOT_IMPLIES_ELIM2

Boolean – Not Implication elimination version 2

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

enumerator CVC5_PROOF_RULE_EQUIV_ELIM1

Boolean – Equivalence elimination version 1

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

enumerator CVC5_PROOF_RULE_EQUIV_ELIM2

Boolean – Equivalence elimination version 2

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

enumerator CVC5_PROOF_RULE_NOT_EQUIV_ELIM1

Boolean – Not Equivalence elimination version 1

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

enumerator CVC5_PROOF_RULE_NOT_EQUIV_ELIM2

Boolean – Not Equivalence elimination version 2

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

enumerator CVC5_PROOF_RULE_XOR_ELIM1

Boolean – XOR elimination version 1

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

enumerator CVC5_PROOF_RULE_XOR_ELIM2

Boolean – XOR elimination version 2

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

enumerator CVC5_PROOF_RULE_NOT_XOR_ELIM1

Boolean – Not XOR elimination version 1

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

enumerator CVC5_PROOF_RULE_NOT_XOR_ELIM2

Boolean – Not XOR elimination version 2

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

enumerator CVC5_PROOF_RULE_ITE_ELIM1

Boolean – ITE elimination version 1

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

enumerator CVC5_PROOF_RULE_ITE_ELIM2

Boolean – ITE elimination version 2

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

enumerator CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_NOT_ITE_ELIM2

Boolean – Not ITE elimination version 2

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

enumerator CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_CNF_IMPLIES_NEG1

Boolean – CNF – Implies Negative 1

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

enumerator CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_REFL

Equality – Reflexivity

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

enumerator CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_TRANS

Equality – Transitivity

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

enumerator CVC5_PROOF_RULE_CONG

Equality – Congruence

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

This rule is used when the kind of $f(t_1,\dots, t_n)$ has a fixed arity. This includes kinds such as cvc5::Kind::ITE, cvc5::Kind::EQUAL, as well as indexed functions such as cvc5::Kind::BITVECTOR_EXTRACT.

It is also used for cvc5::Kind::APPLY_UF, where $f$ is an uninterpreted function.

It is not used for kinds with variadic arity, or for kind cvc5::Kind::HO_APPLY, which respectively use the rules NARY_CONG and HO_CONG below.

enumerator CVC5_PROOF_RULE_NARY_CONG

Equality – N-ary Congruence

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

This rule is used for terms $f(t_1,\dots, t_n)$ whose kinds $k$ have variadic arity, such as cvc5::Kind::AND, cvc5::Kind::PLUS and so on.

enumerator CVC5_PROOF_RULE_TRUE_INTRO

Equality – True intro

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

enumerator CVC5_PROOF_RULE_TRUE_ELIM

Equality – True elim

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

enumerator CVC5_PROOF_RULE_FALSE_INTRO

Equality – False intro

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

enumerator CVC5_PROOF_RULE_FALSE_ELIM

Equality – False elim

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

enumerator CVC5_PROOF_RULE_HO_APP_ENCODE

Equality – Higher-order application encoding

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

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

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

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

enumerator CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_MACRO_BV_BITBLAST

Bit-vectors – (Macro) Bitblast

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

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

enumerator CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_BV_EAGER_ATOM

Bit-vectors – Bit-vector eager atom

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

where $F$ is of kind BITVECTOR_EAGER_ATOM.

enumerator CVC5_PROOF_RULE_BV_POLY_NORM

Bit-vectors – Polynomial normalization

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

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

enumerator CVC5_PROOF_RULE_BV_POLY_NORM_EQ

Bit-vectors – Polynomial normalization for relations

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

$c_x$ and $c_y$ are scaling factors, currently required to be one.

enumerator CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_SKOLEM_INTRO

Quantifiers – Skolem introduction

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

where $t$ is the unpurified form of skolem $k$.

enumerator CVC5_PROOF_RULE_SKOLEMIZE

Quantifiers – Skolemization

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

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

enumerator CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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(F)$ are the free variables of $F$. The internal quantifiers proof checker does not currently check that this is the case.

enumerator CVC5_PROOF_RULE_QUANT_VAR_REORDERING

Quantifiers – Variable reordering

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

where $Y$ is a reordering of $X$.

enumerator CVC5_PROOF_RULE_EXISTS_STRING_LENGTH

Quantifiers – Exists string length

\[\inferrule{-\mid T n i} {\mathit{len}(k) = n}\]

where $k$ is a skolem of string or sequence type $T$ and $n$ is a non-negative integer. The argument $i$ is an identifier for $k$. These three arguments are the indices of $k$, whose skolem identifier is WITNESS_STRING_LENGTH.

enumerator CVC5_PROOF_RULE_SETS_SINGLETON_INJ

Sets – Singleton injectivity

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

enumerator CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_SETS_FILTER_UP

Sets – Sets filter up

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

enumerator CVC5_PROOF_RULE_SETS_FILTER_DOWN

Sets – Sets filter down

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

enumerator CVC5_PROOF_RULE_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 \bot}{t = s}\]

Alternatively for the reverse:

inferrule{(t cdot t_1 cdot ldots cdot t_n) = (s cdot t_1 cdot ldots cdot t_n)mid top}{t = s}

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

enumerator CVC5_PROOF_RULE_CONCAT_UNIFY

Strings – Core rules – Concatenation unification

\[\inferrule{(t_1 \cdot \ldots \cdot t_n) = (s_1 \cdot \ldots \cdot s_m),\, \mathit{len}(t_1) = \mathit{len}(s_1)\mid \bot}{t_1 = s_1}\]

Alternatively for the reverse:

\[\inferrule{(t_1 \cdot \ldots \cdot t_n) = (s_1 \cdot \ldots \cdot s_m),\, \mathit{len}(t_n) = \mathit{len}(s_m)\mid \top}{t_n = s_m}\]

enumerator CVC5_PROOF_RULE_CONCAT_SPLIT

Strings – Core rules – Concatenation split

\[\inferruleSC{(t_1 \cdot \ldots \cdot t_n) = (s_1 \cdot \ldots \cdot s_m),\, \mathit{len}(t_1) \neq \mathit{len}(s_1)\mid \bot}{((t_1 = s_1\cdot r) \vee (s_1 = t_1\cdot r)) \wedge r \neq \epsilon \wedge \mathit{len}(r)>0}\]

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

\[\inferruleSC{(t_1 \cdot \ldots \cdot t_n) = (s_1 \cdot \ldots \cdot s_m),\, \mathit{len}(t_n) \neq \mathit{len}(s_m)\mid \top}{((t_n = r \cdot s_m) \vee (s_m = r \cdot t_n)) \wedge r \neq \epsilon \wedge \mathit{len}(r)>0}\]

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

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

enumerator CVC5_PROOF_RULE_CONCAT_CSPLIT

Strings – Core rules – Concatenation split for constants

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

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

Alternatively for the reverse:

\[\inferrule{(t_1\cdot \ldots \cdot t_n) = (s_1 \cdot \ldots s_{m-1} \cdot c),\,\mathit{len}(t_n) \neq 0\mid \top}{(t_n = r\cdot c)}\]

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

enumerator CVC5_PROOF_RULE_CONCAT_LPROP

Strings – Core rules – Concatenation length propagation

\[\inferrule{(t_1\cdot \ldots \cdot t_n) = (s_1 \cdot \ldots \cdot s_m),\, \mathit{len}(t_1) > \mathit{len}(s_1)\mid \bot}{(t_1 = s_1\cdot r)}\]

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

Alternatively for the reverse:

\[\inferrule{(t_1\cdot \ldots \cdot t_n) = (s_1 \cdot \ldots \cdot s_m)),\, \mathit{len}(t_n) > \mathit{len}(s_m)\mid \top}{(t_n = r \cdot s_m)}\]

where $r$ is the purification Skolem for $\mathit{ite}( \mathit{len}(t_n) >= \mathit{len}(s_m), \mathit{pre}(t_n,\mathit{len}(t_n) - \mathit{len}(s_m)), \mathit{pre}(s_m,\mathit{len}(s_m) - \mathit{len}(t_n)))$

enumerator CVC5_PROOF_RULE_CONCAT_CPROP

Strings – Core rules – Concatenation constant propagation

\[\inferrule{(t_1 \cdot w_1 \cdot \ldots \cdot t_n) = (w_2 \cdot s_2 \cdot \ldots \cdot s_m),\, \mathit{len}(t_1) \neq 0\mid \bot}{(t_1 = t_3\cdot r)}\]

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

Alternatively for the reverse:

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

where $w_1,\,w_2$ are words, $t_3$ is $\mathit{substr}(w_2, \mathit{len}(w_2) - p, p)$, $p$ is $\texttt{Word::roverlap}(\mathit{pre}(w_2, \mathit{len}(w_2) - 1), w_1)$, and $r$ is the purification skolem for $\mathit{pre}(t_n,\mathit{len}(t_n) - \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_n$ is non-empty, $w_3$ must therefore be contained in $t_n$.

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

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

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

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

enumerator CVC5_PROOF_RULE_STRING_LENGTH_POS

Strings – Core rules – Length positive

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

enumerator CVC5_PROOF_RULE_STRING_LENGTH_NON_EMPTY

Strings – Core rules – Length non-empty

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

enumerator CVC5_PROOF_RULE_STRING_REDUCTION

Strings – Extended functions – Reduction

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

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

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

enumerator CVC5_PROOF_RULE_STRING_EAGER_REDUCTION

Strings – Extended functions – Eager reduction

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

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

enumerator CVC5_PROOF_RULE_RE_INTER

Strings – Regular expressions – Intersection

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

enumerator CVC5_PROOF_RULE_RE_CONCAT

Strings – Regular expressions – Concatenation

\[\inferrule{t_1\in R_1,\,\ldots,\,t_n\in R_n\mid -}{\text{str.++}(t_1, \ldots, t_n)\in \text{re.++}(R_1, \ldots, R_n)}\]

enumerator CVC5_PROOF_RULE_RE_UNFOLD_POS

Strings – Regular expressions – Positive Unfold

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

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

enumerator CVC5_PROOF_RULE_RE_UNFOLD_NEG

Strings – Regular expressions – Negative Unfold

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

Or alternatively for regular expression concatenation:

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

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

enumerator CVC5_PROOF_RULE_RE_UNFOLD_NEG_CONCAT_FIXED

Strings – Regular expressions – Unfold negative concatenation, fixed

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

where $r_1$ has fixed length $L$.

or alternatively for the reverse:

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

where $r_n$ has fixed length $L$.

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

enumerator CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_STRING_EXT

Strings – Extensionality

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

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

enumerator CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_ARITH_MULT_ABS_COMPARISON

Arithmetic – Non-linear multiply absolute value comparison

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

enumerator CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_INT_TIGHT_UB

Arithmetic – Tighten strict integer upper bounds

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

where $i$ has integer type.

enumerator CVC5_PROOF_RULE_INT_TIGHT_LB

Arithmetic – Tighten strict integer lower bounds

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

where $i$ has integer type.

enumerator CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_ARITH_REDUCTION

Arithmetic – Reduction

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

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

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

enumerator CVC5_PROOF_RULE_ARITH_POLY_NORM

Arithmetic – Polynomial normalization

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

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

enumerator CVC5_PROOF_RULE_ARITH_POLY_NORM_REL

Arithmetic – Polynomial normalization for relations

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

where $\diamond \in \{<, \leq, =, \geq, >\}$. $c_x$ and $c_y$ are scaling factors. For $<, \leq, \geq, >$, the scaling factors have the same sign.

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

enumerator CVC5_PROOF_RULE_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 greater) that results from the signs of the variables. In particular, $\diamond$ is :math`<` if $f_1 \dots f_k$ contains an odd number of :math`<. Otherwise :math:diamond` is :math`>`. All variables with even exponent in $m$ are given as not equal to zero while all variables with odd exponent in $m$ should be given as less or greater than zero.

enumerator CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_ARITH_MULT_TANGENT

Arithmetic – Multiplication tangent plane

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

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

enumerator CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_ARITH_TRANS_EXP_NEG

Arithmetic – Transcendentals – Exp at negative values

\[\inferrule{- \mid t}{(t < 0.0) \leftrightarrow (\exp(t) < 1.0)}\]

enumerator CVC5_PROOF_RULE_ARITH_TRANS_EXP_POSITIVITY

Arithmetic – Transcendentals – Exp is always positive

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

enumerator CVC5_PROOF_RULE_ARITH_TRANS_EXP_SUPER_LIN

Arithmetic – Transcendentals – Exp grows super-linearly for positive values

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

enumerator CVC5_PROOF_RULE_ARITH_TRANS_EXP_ZERO

Arithmetic – Transcendentals – Exp at zero

\[\inferrule{- \mid t}{(t=0.0) \leftrightarrow (\exp(t) = 1.0)}\]

enumerator CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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!})^{-1}\]

$\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 CVC5_PROOF_RULE_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 a non-negative number, $t$ an arithmetic term and $\texttt{maclaurin}(\exp, n+1, c)$ is the $(n+1)$’th taylor polynomial at zero (also called the Maclaurin series) of the exponential function evaluated at $c$ where $n$ is $2 \cdot d$. The Maclaurin series for the exponential function is the following:

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

This rule furthermore requires that $1 > c^{n+1}/(n+1)!$

enumerator CVC5_PROOF_RULE_ARITH_TRANS_SINE_BOUNDS

Arithmetic – Transcendentals – Sine is always between -1 and 1

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

enumerator CVC5_PROOF_RULE_ARITH_TRANS_SINE_SHIFT

Arithmetic – Transcendentals – Sine is shifted to -pi…pi

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

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

enumerator CVC5_PROOF_RULE_ARITH_TRANS_SINE_SYMMETRY

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

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

enumerator CVC5_PROOF_RULE_ARITH_TRANS_SINE_TANGENT_ZERO

Arithmetic – Transcendentals – Sine is bounded by the tangent at zero

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

enumerator CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_ARITH_TRANS_SINE_APPROX_ABOVE_NEG

Arithmetic – Transcendentals – Sine is approximated from above fornegative 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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_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 CVC5_PROOF_RULE_UNKNOWN

enumerator CVC5_PROOF_RULE_LAST

const char *cvc5_proof_rule_to_string(Cvc5ProofRule rule)

Get a string representation of a Cvc5ProofRule.

Parameters:: rule – The proof rule.
Returns:: The string representation.

size_t cvc5_proof_rule_hash(Cvc5ProofRule rule)

Hash function for Cvc5ProofRule.

Parameters:: rule – The proof rule.
Returns:: The hash value.

enum Cvc5ProofRewriteRule

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 CVC5_PROOF_REWRITE_RULE_NONE

enumerator CVC5_PROOF_REWRITE_RULE_DISTINCT_ELIM

Builtin – Distinct elimination

\[\texttt{distinct}(t_1, t_2) = \neg (t_1 = t2)\]

if $n = 2$, or

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

if $n > 2$

enumerator CVC5_PROOF_REWRITE_RULE_DISTINCT_CARD_CONFLICT

Builtin – Distinct cardinality conflict

\[\texttt{distinct}(t_1, \ldots, tn) = \bot\]

where $n$ is greater than the cardinality of the type of $t_1, \ldots, t_n$.

enumerator CVC5_PROOF_REWRITE_RULE_UBV_TO_INT_ELIM

UF – Bitvector to natural elimination

\[\texttt{ubv_to_int}(t) = t_1 + \ldots + t_n\]

where for $i=1, \ldots, n$, $t_i$ is $\texttt{ite}(x[i-1, i-1] = 1, 2^i, 0)$.

enumerator CVC5_PROOF_REWRITE_RULE_INT_TO_BV_ELIM

UF – Integer to bitvector elimination

\[\texttt{int2bv}_n(t) = (bvconcat t_1 \ldots t_n)\]

where for $i=1, \ldots, n$, $t_i$ is $\texttt{ite}(\texttt{mod}(t,2^n) \geq 2^{n-1}, 1, 0)$.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_BOOL_NNF_NORM

Booleans – Negation Normal Form with normalization

\[F = G\]

where $G$ is the result of applying negation normal form to $F$ with additional normalizations, see TheoryBoolRewriter::computeNnfNorm.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_BOOL_BV_INVERT_SOLVE

Booleans – Bitvector invert solve

\[((t_1 = t_2) = (x = r)) = \top\]

where $x$ occurs on an invertible path in $t_1 = t_2$ and has solved form $r$.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_ARITH_INT_EQ_CONFLICT

Arithmetic – Integer equality conflict

\[(t=s) = \bot\]

where $t=s$ is equivalent (via ARITH_POLY_NORM) to $(r = c)$ where $r$ is an integral term and $c$ is a non-integral constant.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_ARITH_INT_GEQ_TIGHTEN

Arithmetic – Integer inequality tightening

\[(t \geq s) = ( r \geq \lceil c \rceil)\]

or

\[(t \geq s) = \neg( r \geq \lceil c \rceil)\]

where $t \geq s$ is equivalent (via ARITH_POLY_NORM) to the right hand side where $r$ is an integral term and $c$ is a non-integral constant. Note that we end up with a negation if the leading coefficient in $t$ is negative.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_ARITH_STRING_PRED_ENTAIL

Arithmetic – strings predicate entailment

\[(= s t) = c\]

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

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

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_STRING_PRED_ENTAIL

Arithmetic – strings predicate entailment

\[(>= n 0) = true\]

Where $n$ can be shown to be greater than or equal to $0$ by reasoning about string length being positive and basic properties of addition and multiplication.

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_STRING_PRED_SAFE_APPROX

Arithmetic – strings predicate entailment

\[(>= n 0) = (>= m 0)\]

Where $m$ is a safe under-approximation of $n$, namely we have that $(>= n m)$ and $(>= m 0)$.

In detail, subterms of $n$ may be replaced with other terms to obtain $m$ based on the reasoning described in the paper Reynolds et al, CAV 2019, “High-Level Abstractions for Simplifying Extended String Constraints in SMT”.

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_POW_ELIM

Arithmetic – power elimination

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

where $c$ is a non-negative integer.

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

or alternatively

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

In the former case, the left hand side may either be a term of kind cvc5::Kind::APPLY_UF or cvc5::Kind::HO_APPLY. The latter case is used only if the term has kind cvc5::Kind::HO_APPLY.

In either case, the right hand side of the equality in the conclusion is computed using standard substitution via Node::substitute.

enumerator CVC5_PROOF_REWRITE_RULE_LAMBDA_ELIM

Equality – Lambda elimination

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

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_LAMBDA_CAPTURE_AVOID

Equality – Macro lambda application capture avoid

\[((\lambda x_1 \ldots x_n.\> t) \ t_1 \ldots t_n) = ((\lambda y_1 \ldots y_n.\> t') \ t_1 \ldots t_n)\]

The terms may either be of kind cvc5::Kind::APPLY_UF or cvc5::Kind::HO_APPLY. This rule ensures that the free variables of $y_1, \ldots, y_n, t_1 \ldots t_n$ do not occur in binders within $t'$, and $(\lambda x_1 \ldots x_n.\> t)$ is alpha-equivalent to $(\lambda y_1 \ldots y_n.\> t')$. This rule is applied prior to beta reduction to ensure there is no variable capturing.

enumerator CVC5_PROOF_REWRITE_RULE_ARRAYS_SELECT_CONST

Arrays – Constant array select

\[(select A x) = c\]

where $A$ is a constant array storing element $c$.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_ARRAYS_NORMALIZE_OP

Arrays – Macro normalize operation

\[A = B\]

where $B$ is the result of normalizing the array operation $A$ into a canonical form, based on commutativity of disjoint indices.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_ARRAYS_NORMALIZE_CONSTANT

Arrays – Macro normalize constant

\[A = B\]

where $B$ is the result of normalizing the array value $A$ into a canonical form, using the internal method TheoryArraysRewriter::normalizeConstant.

enumerator CVC5_PROOF_REWRITE_RULE_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 CVC5_PROOF_REWRITE_RULE_EXISTS_ELIM

Quantifiers – Exists elimination

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

enumerator CVC5_PROOF_REWRITE_RULE_QUANT_UNUSED_VARS

Quantifiers – Unused variables

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

where $X_1$ is the subset of $X$ that appear free in $F$ and $X_1$ does not contain duplicate variables.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_QUANT_MERGE_PRENEX

Quantifiers – Macro merge prenex

\[\forall X_1.\> \ldots \forall X_n.\> F = \forall X.\> F\]

where $X_1 \ldots X_n$ are lists of variables and $X$ is the result of removing duplicates from $X_1 \ldots X_n$.

enumerator CVC5_PROOF_REWRITE_RULE_QUANT_MERGE_PRENEX

Quantifiers – Merge prenex

\[\forall X_1.\> \ldots \forall X_n.\> F = \forall X_1 \ldots X_n.\> F\]

where $X_1 \ldots X_n$ are lists of variables.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_QUANT_PRENEX

Quantifiers – Macro prenex

\[(\forall X.\> F_1 \vee \cdots \vee (\forall Y.\> F_i) \vee \cdots \vee F_n) = (\forall X Z.\> F_1 \vee \cdots \vee F_i\{ Y \mapsto Z \} \vee \cdots \vee F_n)\]

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_QUANT_MINISCOPE

Quantifiers – Macro miniscoping

\[\forall X.\> F_1 \wedge \cdots \wedge F_n = G_1 \wedge \cdots \wedge G_n\]

where each $G_i$ is semantically equivalent to $\forall X.\> F_i$, or alternatively

\[\forall X.\> \ite{C}{F_1}{F_2} = \ite{C}{G_1}{G_2}\]

where $C$ does not have any free variable in $X$.

enumerator CVC5_PROOF_REWRITE_RULE_QUANT_MINISCOPE_AND

Quantifiers – Miniscoping and

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

enumerator CVC5_PROOF_REWRITE_RULE_QUANT_MINISCOPE_OR

Quantifiers – Miniscoping or

\[\forall X.\> F_1 \vee \ldots \vee F_n = (\forall X_1.\> F_1) \vee \ldots \vee (\forall X_n.\> F_n)\]

where $X = X_1 \ldots X_n$, and the right hand side does not have any free variable in $X$.

enumerator CVC5_PROOF_REWRITE_RULE_QUANT_MINISCOPE_ITE

Quantifiers – Miniscoping ite

\[\forall X.\> \ite{C}{F_1}{F_2} = \ite{C}{\forall X.\> F_1}{\forall X.\> F_2}\]

where $C$ does not have any free variable in $X$.

enumerator CVC5_PROOF_REWRITE_RULE_QUANT_DT_SPLIT

Quantifiers – Datatypes Split

\[(\forall x Y.\> F) = (\forall X_1 Y. F_1) \vee \cdots \vee (\forall X_n Y. F_n)\]

where $x$ is of a datatype type with constructors $C_1, \ldots, C_n$, where for each $i = 1, \ldots, n$, $F_i$ is $F \{ x \mapsto C_i(X_i) \}$.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_QUANT_DT_VAR_EXPAND

Quantifiers – Macro datatype variable expand

\[(\forall Y x Z.\> F) = (\forall Y X_1 Z. F_1) \vee \cdots \vee (\forall Y X_n Z. F_n)\]

where $x$ is of a datatype type with constructors $C_1, \ldots, C_n$, where for each $i = 1, \ldots, n$, $F_i$ is $F \{ x \mapsto C_i(X_i) \}$, and $F$ entails $\mathit{is}_c(x)$ for some $c$.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_QUANT_PARTITION_CONNECTED_FV

Quantifiers – Macro connected free variable partitioning

\[\forall X.\> F_1 \vee \ldots \vee F_n = (\forall X_1.\> F_{1,1} \vee \ldots \vee F_{1,k_1}) \vee \ldots \vee (\forall X_m.\> F_{m,1} \vee \ldots \vee F_{m,k_m})\]

where $X_1, \ldots, X_m$ is a partition of $X$. This is determined by computing the connected components when considering two variables in $X$ to be connected if they occur in the same $F_i$.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_QUANT_VAR_ELIM_EQ

Quantifiers – Macro variable elimination equality

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

where $\neg F$ entails $x = t$.

enumerator CVC5_PROOF_REWRITE_RULE_QUANT_VAR_ELIM_EQ

Quantifiers – Macro variable elimination equality

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

or alternatively

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

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_QUANT_VAR_ELIM_INEQ

Quantifiers – Macro variable elimination inequality

\[\forall x Y.\> F = \forall Y.\> G\]

where $F$ is a disjunction and where $G$ is the result of dropping all literals containing $x$. This is applied only when all such literals are lower (resp. upper) bounds for integer or real variable $x$. Note that $G$ may be false, and $Y$ may be empty in which case it is omitted.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_QUANT_REWRITE_BODY

Quantifiers – Macro quantifiers rewrite body

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

where $G$ is semantically equivalent to $F$.

enumerator CVC5_PROOF_REWRITE_RULE_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 CVC5_PROOF_REWRITE_RULE_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 CVC5_PROOF_REWRITE_RULE_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 CVC5_PROOF_REWRITE_RULE_DT_COLLAPSE_TESTER_SINGLETON

Datatypes – collapse tester

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

where $c$ is the only constructor of its associated datatype.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_DT_CONS_EQ

Datatypes – Macro constructor equality

\[(t = s) = (t_1 = s_1 \wedge \ldots \wedge t_n = s_n)\]

where $t_1, \ldots, t_n$ and $s_1, \ldots, s_n$ are subterms of $t$ and $s$ that occur at the same position respectively (beneath constructor applications), or alternatively

\[(t = s) = false\]

where $t$ and $s$ have subterms that occur in the same position (beneath constructor applications) that are distinct.

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

where $c$ is a constructor.

enumerator CVC5_PROOF_REWRITE_RULE_DT_CONS_EQ_CLASH

Datatypes – constructor equality clash

\[(t = s) = false\]

where $t$ and $s$ have subterms that occur in the same position (beneath constructor applications) that are distinct constructor applications.

enumerator CVC5_PROOF_REWRITE_RULE_DT_CYCLE

Datatypes – cycle

\[(x = t[x]) = \bot\]

where all terms on the path to $x$ in $t[x]$ are applications of constructors, and this path is non-empty.

enumerator CVC5_PROOF_REWRITE_RULE_DT_COLLAPSE_UPDATER

Datatypes – collapse tester

\[u_{c,i}(c(t_1, \ldots, t_i, \ldots, t_n), s) = c(t_1, \ldots, s, \ldots, t_n)\]

or alternatively

\[u_{c,i}(d(t_1, \ldots, t_n), s) = d(t_1, \ldots, t_n)\]

where $c$ and $d$ are distinct constructors.

enumerator CVC5_PROOF_REWRITE_RULE_DT_UPDATER_ELIM

Datatypes - updater elimination

\[u_{c,i}(t, s) = ite(\mathit{is}_c(t), c(s_0(t), \ldots, s, \ldots s_n(t)), t)\]

where $s_i$ is the $i^{th}$ selector for constructor $c$.

enumerator CVC5_PROOF_REWRITE_RULE_DT_MATCH_ELIM

Datatypes – match elimination

\[\texttt{match}(t ((p_1 c_1) \ldots (p_n c_n))) = \texttt{ite}(F_1, r_1, \texttt{ite}( \ldots, r_n))\]

where for $i=1, \ldots, n$, $F_1$ is a formula that holds iff $t$ matches $p_i$ and $r_i$ is the result of a substitution on $c_i$ based on this match.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_BV_EXTRACT_CONCAT

Bitvectors – Macro extract and concat

\[a = b\]

where $a$ is rewritten to $b$ by the internal rewrite rule ExtractConcat.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_BV_OR_SIMPLIFY

Bitvectors – Macro or simplify

\[a = b\]

where $a$ is rewritten to $b$ by the internal rewrite rule OrSimplify.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_BV_AND_SIMPLIFY

Bitvectors – Macro and simplify

\[a = b\]

where $a$ is rewritten to $b$ by the internal rewrite rule AndSimplify.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_BV_XOR_SIMPLIFY

Bitvectors – Macro xor simplify

\[a = b\]

where $a$ is rewritten to $b$ by the internal rewrite rule XorSimplify.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_BV_AND_OR_XOR_CONCAT_PULLUP

Bitvectors – Macro and/or/xor concat pullup

\[a = b\]

where $a$ is rewritten to $b$ by the internal rewrite rule AndOrXorConcatPullup.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_BV_MULT_SLT_MULT

Bitvectors – Macro multiply signed less than multiply

\[a = b\]

where $a$ is rewritten to $b$ by the internal rewrite rule MultSltMult.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_BV_CONCAT_EXTRACT_MERGE

Bitvectors – Macro concat extract merge

\[a = b\]

where $a$ is rewritten to $b$ by the internal rewrite rule ConcatExtractMerge.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_BV_CONCAT_CONSTANT_MERGE

Bitvectors – Macro concat constant merge

\[a = b\]

where $a$ is rewritten to $b$ by the internal rewrite rule ConcatConstantMerge.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_BV_EQ_SOLVE

Bitvectors – Macro equality solve

\[(a = b) = \bot\]

where $bvsub(a,b)$ normalizes to a non-zero constant, or alternatively

\[(a = b) = \top\]

where $bvsub(a,b)$ normalizes to zero.

enumerator CVC5_PROOF_REWRITE_RULE_BV_UMULO_ELIM

Bitvectors – Unsigned multiplication overflow detection elimination

\[\texttt{bvumulo}(x,y) = t\]

where $t$ is the result of eliminating the application of $\texttt{bvumulo}$.

See M.Gok, M.J. Schulte, P.I. Balzola, “Efficient integer multiplication overflow detection circuits”, 2001. http://ieeexplore.ieee.org/document/987767

enumerator CVC5_PROOF_REWRITE_RULE_BV_SMULO_ELIM

Bitvectors – Unsigned multiplication overflow detection elimination

\[\texttt{bvsmulo}(x,y) = t\]

where $t$ is the result of eliminating the application of $\texttt{bvsmulo}$.

See M.Gok, M.J. Schulte, P.I. Balzola, “Efficient integer multiplication overflow detection circuits”, 2001. http://ieeexplore.ieee.org/document/987767

enumerator CVC5_PROOF_REWRITE_RULE_BV_BITWISE_SLICING

Bitvectors – Extract continuous substrings of bitvectors

\[bvand(a,\ c) = concat(bvand(a[i_0:j_0],\ c_0) ... bvand(a[i_n:j_n],\ c_n))\]

where c0,…, cn are maximally continuous substrings of 0 or 1 in the constant c

enumerator CVC5_PROOF_REWRITE_RULE_BV_REPEAT_ELIM

Bitvectors – Extract continuous substrings of bitvectors

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

where $t$ is repeated $n$ times.

enumerator CVC5_PROOF_REWRITE_RULE_STR_CTN_MULTISET_SUBSET

Strings – String contains multiset subset

\[\mathit{str}.contains(s,t) = \bot\]

where the multiset overapproximation of $s$ can be shown to not contain the multiset abstraction of $t$ based on the reasoning described in the paper Reynolds et al, CAV 2019, “High-Level Abstractions for Simplifying Extended String Constraints in SMT”.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_STR_EQ_LEN_UNIFY_PREFIX

Strings – String equality length unify prefix

\[(s = \mathit{str}.\text{++}(t_1, \ldots, t_n)) = (s = \mathit{str}.\text{++}(t_1, \ldots t_i)) \wedge t_{i+1} = \epsilon \wedge \ldots \wedge t_n = \epsilon\]

where we can show $s$ has a length that is at least the length of $\text{++}(t_1, \ldots t_i)$.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_STR_EQ_LEN_UNIFY

Strings – String equality length unify

\[(\mathit{str}.\text{++}(s_1, \ldots, s_n) = \mathit{str}.\text{++}(t_1, \ldots, t_m)) = (r_1 = u_1 \wedge \ldots r_k = u_k)\]

where for each $i = 1, \ldots, k$, we can show the length of $r_i$ and $u_i$ are equal, $s_1, \ldots, s_n$ is $r_1, \ldots, r_k$, and $t_1, \ldots, t_m$ is $u_1, \ldots, u_k$.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_STR_SPLIT_CTN

Strings – Macro string split contains

\[\mathit{str.contains}(t, s) = \mathit{str.contains}(t_1, s) \vee \mathit{str.contains}(t_2, s)\]

where $t_1$ and $t_2$ are substrings of $t$. This rule is elaborated using STR_OVERLAP_SPLIT_CTN.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_STR_STRIP_ENDPOINTS

Strings – Macro string strip endpoints

One of the following forms:

\[\mathit{str.contains}(t, s) = \mathit{str.contains}(t_2, s)\]

\[\mathit{str.indexof}(t, s, n) = \mathit{str.indexof}(t_2, s, n)\]

\[\mathit{str.replace}(t, s, r) = \mathit{str.++}(t_1, \mathit{str.replace}(t_2, s, r) t_3)\]

where in each case we reason about removing portions of $t$ that are irrelevant to the evaluation of the term. This rule is elaborated using STR_OVERLAP_ENDPOINTS_CTN, STR_OVERLAP_ENDPOINTS_INDEXOF and STR_OVERLAP_ENDPOINTS_REPLACE.

enumerator CVC5_PROOF_REWRITE_RULE_STR_OVERLAP_SPLIT_CTN

Strings – Strings overlap split contains

\[\mathit{str.contains}(\mathit{str.++}(t_1, t_2, t_3), s) = \mathit{str.contains}(t_1, s) \vee \mathit{str.contains}(t_3, s)\]

$t_2$ has no forward overlap with $s$ and $s$ has no forward overlap with $t_2$. For details see $\texttt{Word::hasOverlap}$ in theory/strings/word.h.

enumerator CVC5_PROOF_REWRITE_RULE_STR_OVERLAP_ENDPOINTS_CTN

Strings – Strings overlap endpoints contains

\[\mathit{str.contains}(\mathit{str.++}(t_1, t_2, t_3), s) = \mathit{str.contains}(t_2, s)\]

where $s$ is :math:mathit{str.++}(s_1, s_2, s_3), $t_1$ has no forward overlap with $s_1$ and $t_3$ has no reverse overlap with $s_3$. For details see $\texttt{Word::hasOverlap}$ in theory/strings/word.h.

enumerator CVC5_PROOF_REWRITE_RULE_STR_OVERLAP_ENDPOINTS_INDEXOF

Strings – Strings overlap endpoints indexof

\[\mathit{str.indexof}(\mathit{str.++}(t_1, t_2), s, n) = \mathit{str.indexof}(t_1, s, n)\]

where $s$ is :math:mathit{str.++}(s_1, s_2) and $t_2$ has no reverse overlap with $s_2$. For details see $\texttt{Word::hasOverlap}$ in theory/strings/word.h.

enumerator CVC5_PROOF_REWRITE_RULE_STR_OVERLAP_ENDPOINTS_REPLACE

Strings – Strings overlap endpoints replace

\[\mathit{str.replace}(\mathit{str.++}(t_1, t_2, t_3), s, r) = \mathit{str.++}(t_1, \mathit{str.replace}(t_2, s, r) t_3)\]

where $s$ is :math:mathit{str.++}(s_1, s_2, s_3), $t_1$ has no forward overlap with $s_1$ and $t_3$ has no reverse overlap with $s_3$. For details see $\texttt{Word::hasOverlap}$ in theory/strings/word.h.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_STR_COMPONENT_CTN

Strings – Macro string component contains

\[\mathit{str.contains}(t, s) = \top\]

where a substring of $t$ can be inferred to be a superstring of $s$ based on iterating on components of string concatenation terms as well as prefix and suffix reasoning.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_STR_CONST_NCTN_CONCAT

Strings – Macro string constant no contains concatenation

\[\mathit{str.contains}(c, \mathit{str.++}(t_1, \ldots, t_n)) = \bot\]

where $c$ is not contained in $R_t$, where the regular expression $R_t$ overapproximates the possible values of $\mathit{str.++}(t_1, \ldots, t_n)$.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_STR_IN_RE_INCLUSION

Strings – Macro string in regular expression inclusion

\[\mathit{str.in_re}(s, R) = \top\]

where $R$ includes the regular expression $R_s$ which overapproximates the possible values of string $s$.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_RE_INTER_UNION_CONST_ELIM

Strings – Macro regular expression intersection/union constant elimination

One of the following forms:

\[\mathit{re.union}(R) = \mathit{re.union}(R')\]

where $R$ is a list of regular expressions containing $R_i$ and $\mathit{str.to_re(c)}$ where $c$ is a string in $R_i$ and $R'$ is the result of removing $\mathit{str.to_re(c)}$ from $R$.

\[\mathit{re.inter}(R) = \mathit{re.inter}(R')\]

where $R$ is a list of regular expressions containing $R_i$ and $\mathit{str.to_re(c)}$ where $c$ is a string in $R_i$ and $R'$ is the result of removing $R_i$ from $R$.

\[\mathit{re.inter}(R) = \mathit{re.none}\]

where $R$ is a list of regular expressions containing $R_i$ and $\mathit{str.to_re(c)}$ where $c$ is a string not in $R_i$.

enumerator CVC5_PROOF_REWRITE_RULE_SEQ_EVAL_OP

Strings – Sequence evaluate operator

\[f(s_1, \ldots, s_n) = t\]

where $f$ is an operator over sequences and $s_1, \ldots, s_n$ are values, that is, the Node::isConst method returns true for each, and $t$ is the result of evaluating $f$ on them.

enumerator CVC5_PROOF_REWRITE_RULE_STR_INDEXOF_RE_EVAL

Strings – string indexof regex evaluation

\[str.indexof\_re(s,r,n) = m\]

where $s$ is a string values, $n$ is an integer value, $r$ is a ground regular expression and $m$ is the result of evaluating the left hand side.

enumerator CVC5_PROOF_REWRITE_RULE_STR_REPLACE_RE_EVAL

Strings – string replace regex evaluation

\[str.replace\_re(s,r,t) = u\]

where $s,t$ are string values, $r$ is a ground regular expression and $u$ is the result of evaluating the left hand side.

enumerator CVC5_PROOF_REWRITE_RULE_STR_REPLACE_RE_ALL_EVAL

Strings – string replace regex all evaluation

\[str.replace\_re\_all(s,r,t) = u\]

where $s,t$ are string values, $r$ is a ground regular expression and $u$ is the result of evaluating the left hand side.

enumerator CVC5_PROOF_REWRITE_RULE_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 CVC5_PROOF_REWRITE_RULE_RE_EQ_ELIM

Strings – regular expression equality elimination

\[(R1 = R2) = \forall s.\> (\mathit{str.in_re}(s, R1) = \mathit{str.in_re}(s, R2))\]

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_RE_INTER_UNION_INCLUSION

Strings – regular expression intersection/union inclusion

\[\mathit{re.inter}(R) = \mathit{re.inter}(\mathit{re.none}, R_0)\]

where $R$ is a list of regular expressions containing r_1, re.comp(r_2) and the list $R_0$ where r_2 is a superset of r_1.

or alternatively:

\[\mathit{re.union}(R) = \mathit{re.union}(\mathit{re}.\text{*}(\mathit{re.allchar}),\ R_0)\]

where $R$ is a list of regular expressions containing r_1, re.comp(r_2) and the list $R_0$, where r_1 is a superset of r_2.

enumerator CVC5_PROOF_REWRITE_RULE_RE_INTER_INCLUSION

Strings – regular expression intersection inclusion

\[\mathit{re.inter}(r_1, re.comp(r_2)) = \mathit{re.none}\]

where $r_2$ is a superset of $r_1$.

enumerator CVC5_PROOF_REWRITE_RULE_RE_UNION_INCLUSION

Strings – regular expression union inclusion

\[\mathit{re.union}(r_1, re.comp(r_2)) = \mathit{re}.\text{*}(\mathit{re.allchar})\]

where $r_1$ is a superset of $r_2$.

enumerator CVC5_PROOF_REWRITE_RULE_STR_IN_RE_EVAL

Strings – regular expression membership evaluation

\[\mathit{str.in\_re}(s, R) = c\]

where $s$ is a constant string, $R$ is a constant regular expression and $c$ is true or false.

enumerator CVC5_PROOF_REWRITE_RULE_STR_IN_RE_CONSUME

Strings – regular expression membership consume

\[\mathit{str.in_re}(s, R) = b\]

where $b$ is either $false$ or the result of stripping entailed prefixes and suffixes off of $s$ and $R$.

enumerator CVC5_PROOF_REWRITE_RULE_STR_IN_RE_CONCAT_STAR_CHAR

Strings – string in regular expression concatenation star character

\[\begin{split}\mathit{str.in\_re}(\mathit{str}.\text{++}(s_1, \ldots, s_n), \mathit{re}.\text{*}(R)) =\\ \mathit{str.in\_re}(s_1, \mathit{re}.\text{*}(R)) \wedge \ldots \wedge \mathit{str.in\_re}(s_n, \mathit{re}.\text{*}(R))\end{split}\]

where all strings in $R$ have length one.

enumerator CVC5_PROOF_REWRITE_RULE_STR_IN_RE_SIGMA

Strings – string in regular expression sigma

\[\mathit{str.in\_re}(s, \mathit{re}.\text{++}(\mathit{re.allchar}, \ldots, \mathit{re.allchar})) = (\mathit{str.len}(s) = n)\]

or alternatively:

\[\mathit{str.in\_re}(s, \mathit{re}.\text{++}(\mathit{re.allchar}, \ldots, \mathit{re.allchar}, \mathit{re}.\text{*}(\mathit{re.allchar}))) = (\mathit{str.len}(s) \ge n)\]

enumerator CVC5_PROOF_REWRITE_RULE_STR_IN_RE_SIGMA_STAR

Strings – string in regular expression sigma star

\[\mathit{str.in\_re}(s, \mathit{re}.\text{*}(\mathit{re}.\text{++}(\mathit{re.allchar}, \ldots, \mathit{re.allchar}))) = (\mathit{str.len}(s) \ \% \ n = 0)\]

where $n$ is the number of $\mathit{re.allchar}$ arguments to $\mathit{re}.\text{++}$.

enumerator CVC5_PROOF_REWRITE_RULE_MACRO_SUBSTR_STRIP_SYM_LENGTH

Strings – strings substring strip symbolic length

\[str.substr(s, n, m) = t\]

where $t$ is obtained by fully or partially stripping components of $s$ based on $n$ and $m$.

enumerator CVC5_PROOF_REWRITE_RULE_SETS_EVAL_OP

Sets – sets evaluate operator

\[\mathit{f}(t_1, t_2) = t\]

where $f$ is one of $\mathit{set.inter}, \mathit{set.minus}, \mathit{set.union}$, and $t$ is the result of evaluating $f$ on $t_1$ and $t_2$.

Note we use this rule only when $t_1$ and $t_2$ are set values, that is, the Node::isConst method returns true for both.

enumerator CVC5_PROOF_REWRITE_RULE_SETS_INSERT_ELIM

Sets – sets insert elimination

\[\mathit{set.insert}(t_1, \ldots, t_n, S) = \texttt{set.union}(\texttt{sets.singleton}(t_1), \ldots, \texttt{sets.singleton}(t_n), S)\]

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_DIV_TOTAL_ZERO_REAL: Auto-generated from RARE rule arith-div-total-zero-real

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_DIV_TOTAL_ZERO_INT: Auto-generated from RARE rule arith-div-total-zero-int

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_INT_DIV_TOTAL: Auto-generated from RARE rule arith-int-div-total

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_INT_DIV_TOTAL_ONE: Auto-generated from RARE rule arith-int-div-total-one

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_INT_DIV_TOTAL_ZERO: Auto-generated from RARE rule arith-int-div-total-zero

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_INT_DIV_TOTAL_NEG: Auto-generated from RARE rule arith-int-div-total-neg

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_INT_MOD_TOTAL: Auto-generated from RARE rule arith-int-mod-total

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_INT_MOD_TOTAL_ONE: Auto-generated from RARE rule arith-int-mod-total-one

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_INT_MOD_TOTAL_ZERO: Auto-generated from RARE rule arith-int-mod-total-zero

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_INT_MOD_TOTAL_NEG: Auto-generated from RARE rule arith-int-mod-total-neg

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_ELIM_GT: Auto-generated from RARE rule arith-elim-gt

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_ELIM_LT: Auto-generated from RARE rule arith-elim-lt

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_ELIM_INT_GT: Auto-generated from RARE rule arith-elim-int-gt

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_ELIM_INT_LT: Auto-generated from RARE rule arith-elim-int-lt

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_ELIM_LEQ: Auto-generated from RARE rule arith-elim-leq

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_LEQ_NORM: Auto-generated from RARE rule arith-leq-norm

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_GEQ_TIGHTEN: Auto-generated from RARE rule arith-geq-tighten

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_GEQ_NORM1_INT: Auto-generated from RARE rule arith-geq-norm1-int

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_GEQ_NORM1_REAL: Auto-generated from RARE rule arith-geq-norm1-real

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_EQ_ELIM_REAL: Auto-generated from RARE rule arith-eq-elim-real

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_EQ_ELIM_INT: Auto-generated from RARE rule arith-eq-elim-int

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_TO_INT_ELIM: Auto-generated from RARE rule arith-to-int-elim

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_TO_INT_ELIM_TO_REAL: Auto-generated from RARE rule arith-to-int-elim-to-real

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_DIV_ELIM_TO_REAL1: Auto-generated from RARE rule arith-div-elim-to-real1

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_DIV_ELIM_TO_REAL2: Auto-generated from RARE rule arith-div-elim-to-real2

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_MOD_OVER_MOD: Auto-generated from RARE rule arith-mod-over-mod

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_INT_EQ_CONFLICT: Auto-generated from RARE rule arith-int-eq-conflict

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_INT_GEQ_TIGHTEN: Auto-generated from RARE rule arith-int-geq-tighten

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_DIVISIBLE_ELIM: Auto-generated from RARE rule arith-divisible-elim

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_ABS_EQ: Auto-generated from RARE rule arith-abs-eq

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_ABS_INT_GT: Auto-generated from RARE rule arith-abs-int-gt

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_ABS_REAL_GT: Auto-generated from RARE rule arith-abs-real-gt

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_GEQ_ITE_LIFT: Auto-generated from RARE rule arith-geq-ite-lift

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_LEQ_ITE_LIFT: Auto-generated from RARE rule arith-leq-ite-lift

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_MIN_LT1: Auto-generated from RARE rule arith-min-lt1

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_MIN_LT2: Auto-generated from RARE rule arith-min-lt2

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_MAX_GEQ1: Auto-generated from RARE rule arith-max-geq1

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_MAX_GEQ2: Auto-generated from RARE rule arith-max-geq2

enumerator CVC5_PROOF_REWRITE_RULE_ARRAY_READ_OVER_WRITE: Auto-generated from RARE rule array-read-over-write

enumerator CVC5_PROOF_REWRITE_RULE_ARRAY_READ_OVER_WRITE2: Auto-generated from RARE rule array-read-over-write2

enumerator CVC5_PROOF_REWRITE_RULE_ARRAY_STORE_OVERWRITE: Auto-generated from RARE rule array-store-overwrite

enumerator CVC5_PROOF_REWRITE_RULE_ARRAY_STORE_SELF: Auto-generated from RARE rule array-store-self

enumerator CVC5_PROOF_REWRITE_RULE_ARRAY_READ_OVER_WRITE_SPLIT: Auto-generated from RARE rule array-read-over-write-split

enumerator CVC5_PROOF_REWRITE_RULE_ARRAY_STORE_SWAP: Auto-generated from RARE rule array-store-swap

enumerator CVC5_PROOF_REWRITE_RULE_BOOL_DOUBLE_NOT_ELIM: Auto-generated from RARE rule bool-double-not-elim

enumerator CVC5_PROOF_REWRITE_RULE_BOOL_NOT_TRUE: Auto-generated from RARE rule bool-not-true

enumerator CVC5_PROOF_REWRITE_RULE_BOOL_NOT_FALSE: Auto-generated from RARE rule bool-not-false

enumerator CVC5_PROOF_REWRITE_RULE_BOOL_EQ_TRUE: Auto-generated from RARE rule bool-eq-true

enumerator CVC5_PROOF_REWRITE_RULE_BOOL_EQ_FALSE: Auto-generated from RARE rule bool-eq-false

enumerator CVC5_PROOF_REWRITE_RULE_BOOL_EQ_NREFL: Auto-generated from RARE rule bool-eq-nrefl

enumerator CVC5_PROOF_REWRITE_RULE_BOOL_IMPL_FALSE1: Auto-generated from RARE rule bool-impl-false1

enumerator CVC5_PROOF_REWRITE_RULE_BOOL_IMPL_FALSE2: Auto-generated from RARE rule bool-impl-false2

enumerator CVC5_PROOF_REWRITE_RULE_BOOL_IMPL_TRUE1: Auto-generated from RARE rule bool-impl-true1

enumerator CVC5_PROOF_REWRITE_RULE_BOOL_IMPL_TRUE2: Auto-generated from RARE rule bool-impl-true2

enumerator CVC5_PROOF_REWRITE_RULE_BOOL_IMPL_ELIM: Auto-generated from RARE rule bool-impl-elim

enumerator CVC5_PROOF_REWRITE_RULE_BOOL_DUAL_IMPL_EQ: Auto-generated from RARE rule bool-dual-impl-eq

enumerator CVC5_PROOF_REWRITE_RULE_BOOL_AND_CONF: Auto-generated from RARE rule bool-and-conf

enumerator CVC5_PROOF_REWRITE_RULE_BOOL_AND_CONF2: Auto-generated from RARE rule bool-and-conf2

enumerator CVC5_PROOF_REWRITE_RULE_BOOL_OR_TAUT: Auto-generated from RARE rule bool-or-taut

enumerator CVC5_PROOF_REWRITE_RULE_BOOL_OR_TAUT2: Auto-generated from RARE rule bool-or-taut2

enumerator CVC5_PROOF_REWRITE_RULE_BOOL_OR_DE_MORGAN: Auto-generated from RARE rule bool-or-de-morgan

enumerator CVC5_PROOF_REWRITE_RULE_BOOL_IMPLIES_DE_MORGAN: Auto-generated from RARE rule bool-implies-de-morgan

enumerator CVC5_PROOF_REWRITE_RULE_BOOL_AND_DE_MORGAN: Auto-generated from RARE rule bool-and-de-morgan

enumerator CVC5_PROOF_REWRITE_RULE_BOOL_OR_AND_DISTRIB: Auto-generated from RARE rule bool-or-and-distrib

enumerator CVC5_PROOF_REWRITE_RULE_BOOL_IMPLIES_OR_DISTRIB: Auto-generated from RARE rule bool-implies-or-distrib

enumerator CVC5_PROOF_REWRITE_RULE_BOOL_XOR_REFL: Auto-generated from RARE rule bool-xor-refl

enumerator CVC5_PROOF_REWRITE_RULE_BOOL_XOR_NREFL: Auto-generated from RARE rule bool-xor-nrefl

enumerator CVC5_PROOF_REWRITE_RULE_BOOL_XOR_FALSE: Auto-generated from RARE rule bool-xor-false

enumerator CVC5_PROOF_REWRITE_RULE_BOOL_XOR_TRUE: Auto-generated from RARE rule bool-xor-true

enumerator CVC5_PROOF_REWRITE_RULE_BOOL_XOR_COMM: Auto-generated from RARE rule bool-xor-comm

enumerator CVC5_PROOF_REWRITE_RULE_BOOL_XOR_ELIM: Auto-generated from RARE rule bool-xor-elim

enumerator CVC5_PROOF_REWRITE_RULE_BOOL_NOT_XOR_ELIM: Auto-generated from RARE rule bool-not-xor-elim

enumerator CVC5_PROOF_REWRITE_RULE_BOOL_NOT_EQ_ELIM1: Auto-generated from RARE rule bool-not-eq-elim1

enumerator CVC5_PROOF_REWRITE_RULE_BOOL_NOT_EQ_ELIM2: Auto-generated from RARE rule bool-not-eq-elim2

enumerator CVC5_PROOF_REWRITE_RULE_ITE_NEG_BRANCH: Auto-generated from RARE rule ite-neg-branch

enumerator CVC5_PROOF_REWRITE_RULE_ITE_THEN_TRUE: Auto-generated from RARE rule ite-then-true

enumerator CVC5_PROOF_REWRITE_RULE_ITE_ELSE_FALSE: Auto-generated from RARE rule ite-else-false

enumerator CVC5_PROOF_REWRITE_RULE_ITE_THEN_FALSE: Auto-generated from RARE rule ite-then-false

enumerator CVC5_PROOF_REWRITE_RULE_ITE_ELSE_TRUE: Auto-generated from RARE rule ite-else-true

enumerator CVC5_PROOF_REWRITE_RULE_ITE_THEN_LOOKAHEAD_SELF: Auto-generated from RARE rule ite-then-lookahead-self

enumerator CVC5_PROOF_REWRITE_RULE_ITE_ELSE_LOOKAHEAD_SELF: Auto-generated from RARE rule ite-else-lookahead-self

enumerator CVC5_PROOF_REWRITE_RULE_ITE_THEN_LOOKAHEAD_NOT_SELF: Auto-generated from RARE rule ite-then-lookahead-not-self

enumerator CVC5_PROOF_REWRITE_RULE_ITE_ELSE_LOOKAHEAD_NOT_SELF: Auto-generated from RARE rule ite-else-lookahead-not-self

enumerator CVC5_PROOF_REWRITE_RULE_ITE_EXPAND: Auto-generated from RARE rule ite-expand

enumerator CVC5_PROOF_REWRITE_RULE_BOOL_NOT_ITE_ELIM: Auto-generated from RARE rule bool-not-ite-elim

enumerator CVC5_PROOF_REWRITE_RULE_ITE_TRUE_COND: Auto-generated from RARE rule ite-true-cond

enumerator CVC5_PROOF_REWRITE_RULE_ITE_FALSE_COND: Auto-generated from RARE rule ite-false-cond

enumerator CVC5_PROOF_REWRITE_RULE_ITE_NOT_COND: Auto-generated from RARE rule ite-not-cond

enumerator CVC5_PROOF_REWRITE_RULE_ITE_EQ_BRANCH: Auto-generated from RARE rule ite-eq-branch

enumerator CVC5_PROOF_REWRITE_RULE_ITE_THEN_LOOKAHEAD: Auto-generated from RARE rule ite-then-lookahead

enumerator CVC5_PROOF_REWRITE_RULE_ITE_ELSE_LOOKAHEAD: Auto-generated from RARE rule ite-else-lookahead

enumerator CVC5_PROOF_REWRITE_RULE_ITE_THEN_NEG_LOOKAHEAD: Auto-generated from RARE rule ite-then-neg-lookahead

enumerator CVC5_PROOF_REWRITE_RULE_ITE_ELSE_NEG_LOOKAHEAD: Auto-generated from RARE rule ite-else-neg-lookahead

enumerator CVC5_PROOF_REWRITE_RULE_BV_CONCAT_EXTRACT_MERGE: Auto-generated from RARE rule bv-concat-extract-merge

enumerator CVC5_PROOF_REWRITE_RULE_BV_EXTRACT_EXTRACT: Auto-generated from RARE rule bv-extract-extract

enumerator CVC5_PROOF_REWRITE_RULE_BV_EXTRACT_WHOLE: Auto-generated from RARE rule bv-extract-whole

enumerator CVC5_PROOF_REWRITE_RULE_BV_EXTRACT_CONCAT_1: Auto-generated from RARE rule bv-extract-concat-1

enumerator CVC5_PROOF_REWRITE_RULE_BV_EXTRACT_CONCAT_2: Auto-generated from RARE rule bv-extract-concat-2

enumerator CVC5_PROOF_REWRITE_RULE_BV_EXTRACT_CONCAT_3: Auto-generated from RARE rule bv-extract-concat-3

enumerator CVC5_PROOF_REWRITE_RULE_BV_EXTRACT_CONCAT_4: Auto-generated from RARE rule bv-extract-concat-4

enumerator CVC5_PROOF_REWRITE_RULE_BV_EQ_EXTRACT_ELIM1: Auto-generated from RARE rule bv-eq-extract-elim1

enumerator CVC5_PROOF_REWRITE_RULE_BV_EQ_EXTRACT_ELIM2: Auto-generated from RARE rule bv-eq-extract-elim2

enumerator CVC5_PROOF_REWRITE_RULE_BV_EQ_EXTRACT_ELIM3: Auto-generated from RARE rule bv-eq-extract-elim3

enumerator CVC5_PROOF_REWRITE_RULE_BV_EXTRACT_NOT: Auto-generated from RARE rule bv-extract-not

enumerator CVC5_PROOF_REWRITE_RULE_BV_EXTRACT_SIGN_EXTEND_1: Auto-generated from RARE rule bv-extract-sign-extend-1

enumerator CVC5_PROOF_REWRITE_RULE_BV_EXTRACT_SIGN_EXTEND_2: Auto-generated from RARE rule bv-extract-sign-extend-2

enumerator CVC5_PROOF_REWRITE_RULE_BV_EXTRACT_SIGN_EXTEND_3: Auto-generated from RARE rule bv-extract-sign-extend-3

enumerator CVC5_PROOF_REWRITE_RULE_BV_NOT_XOR: Auto-generated from RARE rule bv-not-xor

enumerator CVC5_PROOF_REWRITE_RULE_BV_AND_SIMPLIFY_1: Auto-generated from RARE rule bv-and-simplify-1

enumerator CVC5_PROOF_REWRITE_RULE_BV_AND_SIMPLIFY_2: Auto-generated from RARE rule bv-and-simplify-2

enumerator CVC5_PROOF_REWRITE_RULE_BV_OR_SIMPLIFY_1: Auto-generated from RARE rule bv-or-simplify-1

enumerator CVC5_PROOF_REWRITE_RULE_BV_OR_SIMPLIFY_2: Auto-generated from RARE rule bv-or-simplify-2

enumerator CVC5_PROOF_REWRITE_RULE_BV_XOR_SIMPLIFY_1: Auto-generated from RARE rule bv-xor-simplify-1

enumerator CVC5_PROOF_REWRITE_RULE_BV_XOR_SIMPLIFY_2: Auto-generated from RARE rule bv-xor-simplify-2

enumerator CVC5_PROOF_REWRITE_RULE_BV_XOR_SIMPLIFY_3: Auto-generated from RARE rule bv-xor-simplify-3

enumerator CVC5_PROOF_REWRITE_RULE_BV_ULT_ADD_ONE: Auto-generated from RARE rule bv-ult-add-one

enumerator CVC5_PROOF_REWRITE_RULE_BV_MULT_SLT_MULT_1: Auto-generated from RARE rule bv-mult-slt-mult-1

enumerator CVC5_PROOF_REWRITE_RULE_BV_MULT_SLT_MULT_2: Auto-generated from RARE rule bv-mult-slt-mult-2

enumerator CVC5_PROOF_REWRITE_RULE_BV_COMMUTATIVE_XOR: Auto-generated from RARE rule bv-commutative-xor

enumerator CVC5_PROOF_REWRITE_RULE_BV_COMMUTATIVE_COMP: Auto-generated from RARE rule bv-commutative-comp

enumerator CVC5_PROOF_REWRITE_RULE_BV_ZERO_EXTEND_ELIMINATE_0: Auto-generated from RARE rule bv-zero-extend-eliminate-0

enumerator CVC5_PROOF_REWRITE_RULE_BV_SIGN_EXTEND_ELIMINATE_0: Auto-generated from RARE rule bv-sign-extend-eliminate-0

enumerator CVC5_PROOF_REWRITE_RULE_BV_NOT_NEQ: Auto-generated from RARE rule bv-not-neq

enumerator CVC5_PROOF_REWRITE_RULE_BV_ULT_ONES: Auto-generated from RARE rule bv-ult-ones

enumerator CVC5_PROOF_REWRITE_RULE_BV_CONCAT_MERGE_CONST: Auto-generated from RARE rule bv-concat-merge-const

enumerator CVC5_PROOF_REWRITE_RULE_BV_COMMUTATIVE_ADD: Auto-generated from RARE rule bv-commutative-add

enumerator CVC5_PROOF_REWRITE_RULE_BV_SUB_ELIMINATE: Auto-generated from RARE rule bv-sub-eliminate

enumerator CVC5_PROOF_REWRITE_RULE_BV_ITE_WIDTH_ONE: Auto-generated from RARE rule bv-ite-width-one

enumerator CVC5_PROOF_REWRITE_RULE_BV_ITE_WIDTH_ONE_NOT: Auto-generated from RARE rule bv-ite-width-one-not

enumerator CVC5_PROOF_REWRITE_RULE_BV_EQ_XOR_SOLVE: Auto-generated from RARE rule bv-eq-xor-solve

enumerator CVC5_PROOF_REWRITE_RULE_BV_EQ_NOT_SOLVE: Auto-generated from RARE rule bv-eq-not-solve

enumerator CVC5_PROOF_REWRITE_RULE_BV_UGT_ELIMINATE: Auto-generated from RARE rule bv-ugt-eliminate

enumerator CVC5_PROOF_REWRITE_RULE_BV_UGE_ELIMINATE: Auto-generated from RARE rule bv-uge-eliminate

enumerator CVC5_PROOF_REWRITE_RULE_BV_SGT_ELIMINATE: Auto-generated from RARE rule bv-sgt-eliminate

enumerator CVC5_PROOF_REWRITE_RULE_BV_SGE_ELIMINATE: Auto-generated from RARE rule bv-sge-eliminate

enumerator CVC5_PROOF_REWRITE_RULE_BV_SLE_ELIMINATE: Auto-generated from RARE rule bv-sle-eliminate

enumerator CVC5_PROOF_REWRITE_RULE_BV_REDOR_ELIMINATE: Auto-generated from RARE rule bv-redor-eliminate

enumerator CVC5_PROOF_REWRITE_RULE_BV_REDAND_ELIMINATE: Auto-generated from RARE rule bv-redand-eliminate

enumerator CVC5_PROOF_REWRITE_RULE_BV_ULE_ELIMINATE: Auto-generated from RARE rule bv-ule-eliminate

enumerator CVC5_PROOF_REWRITE_RULE_BV_COMP_ELIMINATE: Auto-generated from RARE rule bv-comp-eliminate

enumerator CVC5_PROOF_REWRITE_RULE_BV_ROTATE_LEFT_ELIMINATE_1: Auto-generated from RARE rule bv-rotate-left-eliminate-1

enumerator CVC5_PROOF_REWRITE_RULE_BV_ROTATE_LEFT_ELIMINATE_2: Auto-generated from RARE rule bv-rotate-left-eliminate-2

enumerator CVC5_PROOF_REWRITE_RULE_BV_ROTATE_RIGHT_ELIMINATE_1: Auto-generated from RARE rule bv-rotate-right-eliminate-1

enumerator CVC5_PROOF_REWRITE_RULE_BV_ROTATE_RIGHT_ELIMINATE_2: Auto-generated from RARE rule bv-rotate-right-eliminate-2

enumerator CVC5_PROOF_REWRITE_RULE_BV_NAND_ELIMINATE: Auto-generated from RARE rule bv-nand-eliminate

enumerator CVC5_PROOF_REWRITE_RULE_BV_NOR_ELIMINATE: Auto-generated from RARE rule bv-nor-eliminate

enumerator CVC5_PROOF_REWRITE_RULE_BV_XNOR_ELIMINATE: Auto-generated from RARE rule bv-xnor-eliminate

enumerator CVC5_PROOF_REWRITE_RULE_BV_SDIV_ELIMINATE: Auto-generated from RARE rule bv-sdiv-eliminate

enumerator CVC5_PROOF_REWRITE_RULE_BV_ZERO_EXTEND_ELIMINATE: Auto-generated from RARE rule bv-zero-extend-eliminate

enumerator CVC5_PROOF_REWRITE_RULE_BV_UADDO_ELIMINATE: Auto-generated from RARE rule bv-uaddo-eliminate

enumerator CVC5_PROOF_REWRITE_RULE_BV_SADDO_ELIMINATE: Auto-generated from RARE rule bv-saddo-eliminate

enumerator CVC5_PROOF_REWRITE_RULE_BV_SDIVO_ELIMINATE: Auto-generated from RARE rule bv-sdivo-eliminate

enumerator CVC5_PROOF_REWRITE_RULE_BV_SMOD_ELIMINATE: Auto-generated from RARE rule bv-smod-eliminate

enumerator CVC5_PROOF_REWRITE_RULE_BV_SREM_ELIMINATE: Auto-generated from RARE rule bv-srem-eliminate

enumerator CVC5_PROOF_REWRITE_RULE_BV_USUBO_ELIMINATE: Auto-generated from RARE rule bv-usubo-eliminate

enumerator CVC5_PROOF_REWRITE_RULE_BV_SSUBO_ELIMINATE: Auto-generated from RARE rule bv-ssubo-eliminate

enumerator CVC5_PROOF_REWRITE_RULE_BV_NEGO_ELIMINATE: Auto-generated from RARE rule bv-nego-eliminate

enumerator CVC5_PROOF_REWRITE_RULE_BV_ITE_EQUAL_CHILDREN: Auto-generated from RARE rule bv-ite-equal-children

enumerator CVC5_PROOF_REWRITE_RULE_BV_ITE_CONST_CHILDREN_1: Auto-generated from RARE rule bv-ite-const-children-1

enumerator CVC5_PROOF_REWRITE_RULE_BV_ITE_CONST_CHILDREN_2: Auto-generated from RARE rule bv-ite-const-children-2

enumerator CVC5_PROOF_REWRITE_RULE_BV_ITE_EQUAL_COND_1: Auto-generated from RARE rule bv-ite-equal-cond-1

enumerator CVC5_PROOF_REWRITE_RULE_BV_ITE_EQUAL_COND_2: Auto-generated from RARE rule bv-ite-equal-cond-2

enumerator CVC5_PROOF_REWRITE_RULE_BV_ITE_EQUAL_COND_3: Auto-generated from RARE rule bv-ite-equal-cond-3

enumerator CVC5_PROOF_REWRITE_RULE_BV_ITE_MERGE_THEN_IF: Auto-generated from RARE rule bv-ite-merge-then-if

enumerator CVC5_PROOF_REWRITE_RULE_BV_ITE_MERGE_ELSE_IF: Auto-generated from RARE rule bv-ite-merge-else-if

enumerator CVC5_PROOF_REWRITE_RULE_BV_ITE_MERGE_THEN_ELSE: Auto-generated from RARE rule bv-ite-merge-then-else

enumerator CVC5_PROOF_REWRITE_RULE_BV_ITE_MERGE_ELSE_ELSE: Auto-generated from RARE rule bv-ite-merge-else-else

enumerator CVC5_PROOF_REWRITE_RULE_BV_SHL_BY_CONST_0: Auto-generated from RARE rule bv-shl-by-const-0

enumerator CVC5_PROOF_REWRITE_RULE_BV_SHL_BY_CONST_1: Auto-generated from RARE rule bv-shl-by-const-1

enumerator CVC5_PROOF_REWRITE_RULE_BV_SHL_BY_CONST_2: Auto-generated from RARE rule bv-shl-by-const-2

enumerator CVC5_PROOF_REWRITE_RULE_BV_LSHR_BY_CONST_0: Auto-generated from RARE rule bv-lshr-by-const-0

enumerator CVC5_PROOF_REWRITE_RULE_BV_LSHR_BY_CONST_1: Auto-generated from RARE rule bv-lshr-by-const-1

enumerator CVC5_PROOF_REWRITE_RULE_BV_LSHR_BY_CONST_2: Auto-generated from RARE rule bv-lshr-by-const-2

enumerator CVC5_PROOF_REWRITE_RULE_BV_ASHR_BY_CONST_0: Auto-generated from RARE rule bv-ashr-by-const-0

enumerator CVC5_PROOF_REWRITE_RULE_BV_ASHR_BY_CONST_1: Auto-generated from RARE rule bv-ashr-by-const-1

enumerator CVC5_PROOF_REWRITE_RULE_BV_ASHR_BY_CONST_2: Auto-generated from RARE rule bv-ashr-by-const-2

enumerator CVC5_PROOF_REWRITE_RULE_BV_AND_CONCAT_PULLUP: Auto-generated from RARE rule bv-and-concat-pullup

enumerator CVC5_PROOF_REWRITE_RULE_BV_OR_CONCAT_PULLUP: Auto-generated from RARE rule bv-or-concat-pullup

enumerator CVC5_PROOF_REWRITE_RULE_BV_XOR_CONCAT_PULLUP: Auto-generated from RARE rule bv-xor-concat-pullup

enumerator CVC5_PROOF_REWRITE_RULE_BV_AND_CONCAT_PULLUP2: Auto-generated from RARE rule bv-and-concat-pullup2

enumerator CVC5_PROOF_REWRITE_RULE_BV_OR_CONCAT_PULLUP2: Auto-generated from RARE rule bv-or-concat-pullup2

enumerator CVC5_PROOF_REWRITE_RULE_BV_XOR_CONCAT_PULLUP2: Auto-generated from RARE rule bv-xor-concat-pullup2

enumerator CVC5_PROOF_REWRITE_RULE_BV_AND_CONCAT_PULLUP3: Auto-generated from RARE rule bv-and-concat-pullup3

enumerator CVC5_PROOF_REWRITE_RULE_BV_OR_CONCAT_PULLUP3: Auto-generated from RARE rule bv-or-concat-pullup3

enumerator CVC5_PROOF_REWRITE_RULE_BV_XOR_CONCAT_PULLUP3: Auto-generated from RARE rule bv-xor-concat-pullup3

enumerator CVC5_PROOF_REWRITE_RULE_BV_XOR_DUPLICATE: Auto-generated from RARE rule bv-xor-duplicate

enumerator CVC5_PROOF_REWRITE_RULE_BV_XOR_ONES: Auto-generated from RARE rule bv-xor-ones

enumerator CVC5_PROOF_REWRITE_RULE_BV_XOR_NOT: Auto-generated from RARE rule bv-xor-not

enumerator CVC5_PROOF_REWRITE_RULE_BV_NOT_IDEMP: Auto-generated from RARE rule bv-not-idemp

enumerator CVC5_PROOF_REWRITE_RULE_BV_ULT_ZERO_1: Auto-generated from RARE rule bv-ult-zero-1

enumerator CVC5_PROOF_REWRITE_RULE_BV_ULT_ZERO_2: Auto-generated from RARE rule bv-ult-zero-2

enumerator CVC5_PROOF_REWRITE_RULE_BV_ULT_SELF: Auto-generated from RARE rule bv-ult-self

enumerator CVC5_PROOF_REWRITE_RULE_BV_LT_SELF: Auto-generated from RARE rule bv-lt-self

enumerator CVC5_PROOF_REWRITE_RULE_BV_ULE_SELF: Auto-generated from RARE rule bv-ule-self

enumerator CVC5_PROOF_REWRITE_RULE_BV_ULE_ZERO: Auto-generated from RARE rule bv-ule-zero

enumerator CVC5_PROOF_REWRITE_RULE_BV_ZERO_ULE: Auto-generated from RARE rule bv-zero-ule

enumerator CVC5_PROOF_REWRITE_RULE_BV_SLE_SELF: Auto-generated from RARE rule bv-sle-self

enumerator CVC5_PROOF_REWRITE_RULE_BV_ULE_MAX: Auto-generated from RARE rule bv-ule-max

enumerator CVC5_PROOF_REWRITE_RULE_BV_NOT_ULT: Auto-generated from RARE rule bv-not-ult

enumerator CVC5_PROOF_REWRITE_RULE_BV_MULT_POW2_1: Auto-generated from RARE rule bv-mult-pow2-1

enumerator CVC5_PROOF_REWRITE_RULE_BV_MULT_POW2_2: Auto-generated from RARE rule bv-mult-pow2-2

enumerator CVC5_PROOF_REWRITE_RULE_BV_MULT_POW2_2B: Auto-generated from RARE rule bv-mult-pow2-2b

enumerator CVC5_PROOF_REWRITE_RULE_BV_EXTRACT_MULT_LEADING_BIT: Auto-generated from RARE rule bv-extract-mult-leading-bit

enumerator CVC5_PROOF_REWRITE_RULE_BV_UDIV_POW2_NOT_ONE: Auto-generated from RARE rule bv-udiv-pow2-not-one

enumerator CVC5_PROOF_REWRITE_RULE_BV_UDIV_ZERO: Auto-generated from RARE rule bv-udiv-zero

enumerator CVC5_PROOF_REWRITE_RULE_BV_UDIV_ONE: Auto-generated from RARE rule bv-udiv-one

enumerator CVC5_PROOF_REWRITE_RULE_BV_UREM_POW2_NOT_ONE: Auto-generated from RARE rule bv-urem-pow2-not-one

enumerator CVC5_PROOF_REWRITE_RULE_BV_UREM_ONE: Auto-generated from RARE rule bv-urem-one

enumerator CVC5_PROOF_REWRITE_RULE_BV_UREM_SELF: Auto-generated from RARE rule bv-urem-self

enumerator CVC5_PROOF_REWRITE_RULE_BV_SHL_ZERO: Auto-generated from RARE rule bv-shl-zero

enumerator CVC5_PROOF_REWRITE_RULE_BV_LSHR_ZERO: Auto-generated from RARE rule bv-lshr-zero

enumerator CVC5_PROOF_REWRITE_RULE_BV_ASHR_ZERO: Auto-generated from RARE rule bv-ashr-zero

enumerator CVC5_PROOF_REWRITE_RULE_BV_UGT_UREM: Auto-generated from RARE rule bv-ugt-urem

enumerator CVC5_PROOF_REWRITE_RULE_BV_ULT_ONE: Auto-generated from RARE rule bv-ult-one

enumerator CVC5_PROOF_REWRITE_RULE_BV_MERGE_SIGN_EXTEND_1: Auto-generated from RARE rule bv-merge-sign-extend-1

enumerator CVC5_PROOF_REWRITE_RULE_BV_MERGE_SIGN_EXTEND_2: Auto-generated from RARE rule bv-merge-sign-extend-2

enumerator CVC5_PROOF_REWRITE_RULE_BV_SIGN_EXTEND_EQ_CONST_1: Auto-generated from RARE rule bv-sign-extend-eq-const-1

enumerator CVC5_PROOF_REWRITE_RULE_BV_SIGN_EXTEND_EQ_CONST_2: Auto-generated from RARE rule bv-sign-extend-eq-const-2

enumerator CVC5_PROOF_REWRITE_RULE_BV_ZERO_EXTEND_EQ_CONST_1: Auto-generated from RARE rule bv-zero-extend-eq-const-1

enumerator CVC5_PROOF_REWRITE_RULE_BV_ZERO_EXTEND_EQ_CONST_2: Auto-generated from RARE rule bv-zero-extend-eq-const-2

enumerator CVC5_PROOF_REWRITE_RULE_BV_ZERO_EXTEND_ULT_CONST_1: Auto-generated from RARE rule bv-zero-extend-ult-const-1

enumerator CVC5_PROOF_REWRITE_RULE_BV_ZERO_EXTEND_ULT_CONST_2: Auto-generated from RARE rule bv-zero-extend-ult-const-2

enumerator CVC5_PROOF_REWRITE_RULE_BV_SIGN_EXTEND_ULT_CONST_1: Auto-generated from RARE rule bv-sign-extend-ult-const-1

enumerator CVC5_PROOF_REWRITE_RULE_BV_SIGN_EXTEND_ULT_CONST_2: Auto-generated from RARE rule bv-sign-extend-ult-const-2

enumerator CVC5_PROOF_REWRITE_RULE_BV_SIGN_EXTEND_ULT_CONST_3: Auto-generated from RARE rule bv-sign-extend-ult-const-3

enumerator CVC5_PROOF_REWRITE_RULE_BV_SIGN_EXTEND_ULT_CONST_4: Auto-generated from RARE rule bv-sign-extend-ult-const-4

enumerator CVC5_PROOF_REWRITE_RULE_SETS_EQ_SINGLETON_EMP: Auto-generated from RARE rule sets-eq-singleton-emp

enumerator CVC5_PROOF_REWRITE_RULE_SETS_MEMBER_SINGLETON: Auto-generated from RARE rule sets-member-singleton

enumerator CVC5_PROOF_REWRITE_RULE_SETS_MEMBER_EMP: Auto-generated from RARE rule sets-member-emp

enumerator CVC5_PROOF_REWRITE_RULE_SETS_SUBSET_ELIM: Auto-generated from RARE rule sets-subset-elim

enumerator CVC5_PROOF_REWRITE_RULE_SETS_UNION_COMM: Auto-generated from RARE rule sets-union-comm

enumerator CVC5_PROOF_REWRITE_RULE_SETS_INTER_COMM: Auto-generated from RARE rule sets-inter-comm

enumerator CVC5_PROOF_REWRITE_RULE_SETS_INTER_EMP1: Auto-generated from RARE rule sets-inter-emp1

enumerator CVC5_PROOF_REWRITE_RULE_SETS_INTER_EMP2: Auto-generated from RARE rule sets-inter-emp2

enumerator CVC5_PROOF_REWRITE_RULE_SETS_MINUS_EMP1: Auto-generated from RARE rule sets-minus-emp1

enumerator CVC5_PROOF_REWRITE_RULE_SETS_MINUS_EMP2: Auto-generated from RARE rule sets-minus-emp2

enumerator CVC5_PROOF_REWRITE_RULE_SETS_UNION_EMP1: Auto-generated from RARE rule sets-union-emp1

enumerator CVC5_PROOF_REWRITE_RULE_SETS_UNION_EMP2: Auto-generated from RARE rule sets-union-emp2

enumerator CVC5_PROOF_REWRITE_RULE_SETS_INTER_MEMBER: Auto-generated from RARE rule sets-inter-member

enumerator CVC5_PROOF_REWRITE_RULE_SETS_MINUS_MEMBER: Auto-generated from RARE rule sets-minus-member

enumerator CVC5_PROOF_REWRITE_RULE_SETS_UNION_MEMBER: Auto-generated from RARE rule sets-union-member

enumerator CVC5_PROOF_REWRITE_RULE_SETS_CHOOSE_SINGLETON: Auto-generated from RARE rule sets-choose-singleton

enumerator CVC5_PROOF_REWRITE_RULE_SETS_MINUS_SELF: Auto-generated from RARE rule sets-minus-self

enumerator CVC5_PROOF_REWRITE_RULE_SETS_IS_EMPTY_ELIM: Auto-generated from RARE rule sets-is-empty-elim

enumerator CVC5_PROOF_REWRITE_RULE_SETS_IS_SINGLETON_ELIM: Auto-generated from RARE rule sets-is-singleton-elim

enumerator CVC5_PROOF_REWRITE_RULE_STR_EQ_CTN_FALSE: Auto-generated from RARE rule str-eq-ctn-false

enumerator CVC5_PROOF_REWRITE_RULE_STR_EQ_CTN_FULL_FALSE1: Auto-generated from RARE rule str-eq-ctn-full-false1

enumerator CVC5_PROOF_REWRITE_RULE_STR_EQ_CTN_FULL_FALSE2: Auto-generated from RARE rule str-eq-ctn-full-false2

enumerator CVC5_PROOF_REWRITE_RULE_STR_EQ_LEN_FALSE: Auto-generated from RARE rule str-eq-len-false

enumerator CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_EMPTY_STR: Auto-generated from RARE rule str-substr-empty-str

enumerator CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_EMPTY_RANGE: Auto-generated from RARE rule str-substr-empty-range

enumerator CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_EMPTY_START: Auto-generated from RARE rule str-substr-empty-start

enumerator CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_EMPTY_START_NEG: Auto-generated from RARE rule str-substr-empty-start-neg

enumerator CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_SUBSTR_START_GEQ_LEN: Auto-generated from RARE rule str-substr-substr-start-geq-len

enumerator CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_EQ_EMPTY: Auto-generated from RARE rule str-substr-eq-empty

enumerator CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_Z_EQ_EMPTY_LEQ: Auto-generated from RARE rule str-substr-z-eq-empty-leq

enumerator CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_EQ_EMPTY_LEQ_LEN: Auto-generated from RARE rule str-substr-eq-empty-leq-len

enumerator CVC5_PROOF_REWRITE_RULE_STR_LEN_REPLACE_INV: Auto-generated from RARE rule str-len-replace-inv

enumerator CVC5_PROOF_REWRITE_RULE_STR_LEN_REPLACE_ALL_INV: Auto-generated from RARE rule str-len-replace-all-inv

enumerator CVC5_PROOF_REWRITE_RULE_STR_LEN_UPDATE_INV: Auto-generated from RARE rule str-len-update-inv

enumerator CVC5_PROOF_REWRITE_RULE_STR_UPDATE_IN_FIRST_CONCAT: Auto-generated from RARE rule str-update-in-first-concat

enumerator CVC5_PROOF_REWRITE_RULE_STR_LEN_SUBSTR_IN_RANGE: Auto-generated from RARE rule str-len-substr-in-range

enumerator CVC5_PROOF_REWRITE_RULE_STR_CONCAT_CLASH: Auto-generated from RARE rule str-concat-clash

enumerator CVC5_PROOF_REWRITE_RULE_STR_CONCAT_CLASH_REV: Auto-generated from RARE rule str-concat-clash-rev

enumerator CVC5_PROOF_REWRITE_RULE_STR_CONCAT_CLASH2: Auto-generated from RARE rule str-concat-clash2

enumerator CVC5_PROOF_REWRITE_RULE_STR_CONCAT_CLASH2_REV: Auto-generated from RARE rule str-concat-clash2-rev

enumerator CVC5_PROOF_REWRITE_RULE_STR_CONCAT_UNIFY: Auto-generated from RARE rule str-concat-unify

enumerator CVC5_PROOF_REWRITE_RULE_STR_CONCAT_UNIFY_REV: Auto-generated from RARE rule str-concat-unify-rev

enumerator CVC5_PROOF_REWRITE_RULE_STR_CONCAT_UNIFY_BASE: Auto-generated from RARE rule str-concat-unify-base

enumerator CVC5_PROOF_REWRITE_RULE_STR_CONCAT_UNIFY_BASE_REV: Auto-generated from RARE rule str-concat-unify-base-rev

enumerator CVC5_PROOF_REWRITE_RULE_STR_PREFIXOF_ELIM: Auto-generated from RARE rule str-prefixof-elim

enumerator CVC5_PROOF_REWRITE_RULE_STR_SUFFIXOF_ELIM: Auto-generated from RARE rule str-suffixof-elim

enumerator CVC5_PROOF_REWRITE_RULE_STR_PREFIXOF_EQ: Auto-generated from RARE rule str-prefixof-eq

enumerator CVC5_PROOF_REWRITE_RULE_STR_SUFFIXOF_EQ: Auto-generated from RARE rule str-suffixof-eq

enumerator CVC5_PROOF_REWRITE_RULE_STR_PREFIXOF_ONE: Auto-generated from RARE rule str-prefixof-one

enumerator CVC5_PROOF_REWRITE_RULE_STR_SUFFIXOF_ONE: Auto-generated from RARE rule str-suffixof-one

enumerator CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_COMBINE1: Auto-generated from RARE rule str-substr-combine1

enumerator CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_COMBINE2: Auto-generated from RARE rule str-substr-combine2

enumerator CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_COMBINE3: Auto-generated from RARE rule str-substr-combine3

enumerator CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_COMBINE4: Auto-generated from RARE rule str-substr-combine4

enumerator CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_CONCAT1: Auto-generated from RARE rule str-substr-concat1

enumerator CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_CONCAT2: Auto-generated from RARE rule str-substr-concat2

enumerator CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_REPLACE: Auto-generated from RARE rule str-substr-replace

enumerator CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_FULL: Auto-generated from RARE rule str-substr-full

enumerator CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_FULL_EQ: Auto-generated from RARE rule str-substr-full-eq

enumerator CVC5_PROOF_REWRITE_RULE_STR_CONTAINS_REFL: Auto-generated from RARE rule str-contains-refl

enumerator CVC5_PROOF_REWRITE_RULE_STR_CONTAINS_CONCAT_FIND: Auto-generated from RARE rule str-contains-concat-find

enumerator CVC5_PROOF_REWRITE_RULE_STR_CONTAINS_CONCAT_FIND_CONTRA: Auto-generated from RARE rule str-contains-concat-find-contra

enumerator CVC5_PROOF_REWRITE_RULE_STR_CONTAINS_SPLIT_CHAR: Auto-generated from RARE rule str-contains-split-char

enumerator CVC5_PROOF_REWRITE_RULE_STR_CONTAINS_LEQ_LEN_EQ: Auto-generated from RARE rule str-contains-leq-len-eq

enumerator CVC5_PROOF_REWRITE_RULE_STR_CONTAINS_EMP: Auto-generated from RARE rule str-contains-emp

enumerator CVC5_PROOF_REWRITE_RULE_STR_CONTAINS_CHAR: Auto-generated from RARE rule str-contains-char

enumerator CVC5_PROOF_REWRITE_RULE_STR_AT_ELIM: Auto-generated from RARE rule str-at-elim

enumerator CVC5_PROOF_REWRITE_RULE_STR_REPLACE_SELF: Auto-generated from RARE rule str-replace-self

enumerator CVC5_PROOF_REWRITE_RULE_STR_REPLACE_ID: Auto-generated from RARE rule str-replace-id

enumerator CVC5_PROOF_REWRITE_RULE_STR_REPLACE_PREFIX: Auto-generated from RARE rule str-replace-prefix

enumerator CVC5_PROOF_REWRITE_RULE_STR_REPLACE_NO_CONTAINS: Auto-generated from RARE rule str-replace-no-contains

enumerator CVC5_PROOF_REWRITE_RULE_STR_REPLACE_FIND_BASE: Auto-generated from RARE rule str-replace-find-base

enumerator CVC5_PROOF_REWRITE_RULE_STR_REPLACE_FIND_FIRST_CONCAT: Auto-generated from RARE rule str-replace-find-first-concat

enumerator CVC5_PROOF_REWRITE_RULE_STR_REPLACE_EMPTY: Auto-generated from RARE rule str-replace-empty

enumerator CVC5_PROOF_REWRITE_RULE_STR_REPLACE_ONE_PRE: Auto-generated from RARE rule str-replace-one-pre

enumerator CVC5_PROOF_REWRITE_RULE_STR_REPLACE_FIND_PRE: Auto-generated from RARE rule str-replace-find-pre

enumerator CVC5_PROOF_REWRITE_RULE_STR_REPLACE_ALL_NO_CONTAINS: Auto-generated from RARE rule str-replace-all-no-contains

enumerator CVC5_PROOF_REWRITE_RULE_STR_REPLACE_RE_NONE: Auto-generated from RARE rule str-replace-re-none

enumerator CVC5_PROOF_REWRITE_RULE_STR_REPLACE_RE_ALL_NONE: Auto-generated from RARE rule str-replace-re-all-none

enumerator CVC5_PROOF_REWRITE_RULE_STR_LEN_CONCAT_REC: Auto-generated from RARE rule str-len-concat-rec

enumerator CVC5_PROOF_REWRITE_RULE_STR_LEN_EQ_ZERO_CONCAT_REC: Auto-generated from RARE rule str-len-eq-zero-concat-rec

enumerator CVC5_PROOF_REWRITE_RULE_STR_LEN_EQ_ZERO_BASE: Auto-generated from RARE rule str-len-eq-zero-base

enumerator CVC5_PROOF_REWRITE_RULE_STR_INDEXOF_SELF: Auto-generated from RARE rule str-indexof-self

enumerator CVC5_PROOF_REWRITE_RULE_STR_INDEXOF_NO_CONTAINS: Auto-generated from RARE rule str-indexof-no-contains

enumerator CVC5_PROOF_REWRITE_RULE_STR_INDEXOF_OOB: Auto-generated from RARE rule str-indexof-oob

enumerator CVC5_PROOF_REWRITE_RULE_STR_INDEXOF_OOB2: Auto-generated from RARE rule str-indexof-oob2

enumerator CVC5_PROOF_REWRITE_RULE_STR_INDEXOF_CONTAINS_PRE: Auto-generated from RARE rule str-indexof-contains-pre

enumerator CVC5_PROOF_REWRITE_RULE_STR_INDEXOF_FIND_EMP: Auto-generated from RARE rule str-indexof-find-emp

enumerator CVC5_PROOF_REWRITE_RULE_STR_INDEXOF_EQ_IRR: Auto-generated from RARE rule str-indexof-eq-irr

enumerator CVC5_PROOF_REWRITE_RULE_STR_INDEXOF_RE_NONE: Auto-generated from RARE rule str-indexof-re-none

enumerator CVC5_PROOF_REWRITE_RULE_STR_INDEXOF_RE_EMP_RE: Auto-generated from RARE rule str-indexof-re-emp-re

enumerator CVC5_PROOF_REWRITE_RULE_STR_TO_LOWER_CONCAT: Auto-generated from RARE rule str-to-lower-concat

enumerator CVC5_PROOF_REWRITE_RULE_STR_TO_UPPER_CONCAT: Auto-generated from RARE rule str-to-upper-concat

enumerator CVC5_PROOF_REWRITE_RULE_STR_TO_LOWER_UPPER: Auto-generated from RARE rule str-to-lower-upper

enumerator CVC5_PROOF_REWRITE_RULE_STR_TO_UPPER_LOWER: Auto-generated from RARE rule str-to-upper-lower

enumerator CVC5_PROOF_REWRITE_RULE_STR_TO_LOWER_LEN: Auto-generated from RARE rule str-to-lower-len

enumerator CVC5_PROOF_REWRITE_RULE_STR_TO_UPPER_LEN: Auto-generated from RARE rule str-to-upper-len

enumerator CVC5_PROOF_REWRITE_RULE_STR_TO_LOWER_FROM_INT: Auto-generated from RARE rule str-to-lower-from-int

enumerator CVC5_PROOF_REWRITE_RULE_STR_TO_UPPER_FROM_INT: Auto-generated from RARE rule str-to-upper-from-int

enumerator CVC5_PROOF_REWRITE_RULE_STR_TO_INT_CONCAT_NEG_ONE: Auto-generated from RARE rule str-to-int-concat-neg-one

enumerator CVC5_PROOF_REWRITE_RULE_STR_LEQ_EMPTY: Auto-generated from RARE rule str-leq-empty

enumerator CVC5_PROOF_REWRITE_RULE_STR_LEQ_EMPTY_EQ: Auto-generated from RARE rule str-leq-empty-eq

enumerator CVC5_PROOF_REWRITE_RULE_STR_LEQ_CONCAT_FALSE: Auto-generated from RARE rule str-leq-concat-false

enumerator CVC5_PROOF_REWRITE_RULE_STR_LEQ_CONCAT_TRUE: Auto-generated from RARE rule str-leq-concat-true

enumerator CVC5_PROOF_REWRITE_RULE_STR_LEQ_CONCAT_BASE_1: Auto-generated from RARE rule str-leq-concat-base-1

enumerator CVC5_PROOF_REWRITE_RULE_STR_LEQ_CONCAT_BASE_2: Auto-generated from RARE rule str-leq-concat-base-2

enumerator CVC5_PROOF_REWRITE_RULE_STR_LT_ELIM: Auto-generated from RARE rule str-lt-elim

enumerator CVC5_PROOF_REWRITE_RULE_STR_FROM_INT_NO_CTN_NONDIGIT: Auto-generated from RARE rule str-from-int-no-ctn-nondigit

enumerator CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_CTN_CONTRA: Auto-generated from RARE rule str-substr-ctn-contra

enumerator CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_CTN: Auto-generated from RARE rule str-substr-ctn

enumerator CVC5_PROOF_REWRITE_RULE_STR_REPLACE_DUAL_CTN: Auto-generated from RARE rule str-replace-dual-ctn

enumerator CVC5_PROOF_REWRITE_RULE_STR_REPLACE_DUAL_CTN_FALSE: Auto-generated from RARE rule str-replace-dual-ctn-false

enumerator CVC5_PROOF_REWRITE_RULE_STR_REPLACE_SELF_CTN_SIMP: Auto-generated from RARE rule str-replace-self-ctn-simp

enumerator CVC5_PROOF_REWRITE_RULE_STR_REPLACE_EMP_CTN_SRC: Auto-generated from RARE rule str-replace-emp-ctn-src

enumerator CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_CHAR_START_EQ_LEN: Auto-generated from RARE rule str-substr-char-start-eq-len

enumerator CVC5_PROOF_REWRITE_RULE_STR_CONTAINS_REPL_CHAR: Auto-generated from RARE rule str-contains-repl-char

enumerator CVC5_PROOF_REWRITE_RULE_STR_CONTAINS_REPL_SELF_TGT_CHAR: Auto-generated from RARE rule str-contains-repl-self-tgt-char

enumerator CVC5_PROOF_REWRITE_RULE_STR_CONTAINS_REPL_SELF: Auto-generated from RARE rule str-contains-repl-self

enumerator CVC5_PROOF_REWRITE_RULE_STR_CONTAINS_REPL_TGT: Auto-generated from RARE rule str-contains-repl-tgt

enumerator CVC5_PROOF_REWRITE_RULE_STR_REPL_REPL_LEN_ID: Auto-generated from RARE rule str-repl-repl-len-id

enumerator CVC5_PROOF_REWRITE_RULE_STR_REPL_REPL_SRC_TGT_NO_CTN: Auto-generated from RARE rule str-repl-repl-src-tgt-no-ctn

enumerator CVC5_PROOF_REWRITE_RULE_STR_REPL_REPL_TGT_SELF: Auto-generated from RARE rule str-repl-repl-tgt-self

enumerator CVC5_PROOF_REWRITE_RULE_STR_REPL_REPL_TGT_NO_CTN: Auto-generated from RARE rule str-repl-repl-tgt-no-ctn

enumerator CVC5_PROOF_REWRITE_RULE_STR_REPL_REPL_SRC_SELF: Auto-generated from RARE rule str-repl-repl-src-self

enumerator CVC5_PROOF_REWRITE_RULE_STR_REPL_REPL_SRC_INV_NO_CTN1: Auto-generated from RARE rule str-repl-repl-src-inv-no-ctn1

enumerator CVC5_PROOF_REWRITE_RULE_STR_REPL_REPL_SRC_INV_NO_CTN2: Auto-generated from RARE rule str-repl-repl-src-inv-no-ctn2

enumerator CVC5_PROOF_REWRITE_RULE_STR_REPL_REPL_SRC_INV_NO_CTN3: Auto-generated from RARE rule str-repl-repl-src-inv-no-ctn3

enumerator CVC5_PROOF_REWRITE_RULE_STR_REPL_REPL_DUAL_SELF: Auto-generated from RARE rule str-repl-repl-dual-self

enumerator CVC5_PROOF_REWRITE_RULE_STR_REPL_REPL_DUAL_ITE1: Auto-generated from RARE rule str-repl-repl-dual-ite1

enumerator CVC5_PROOF_REWRITE_RULE_STR_REPL_REPL_DUAL_ITE2: Auto-generated from RARE rule str-repl-repl-dual-ite2

enumerator CVC5_PROOF_REWRITE_RULE_STR_REPL_REPL_LOOKAHEAD_ID_SIMP: Auto-generated from RARE rule str-repl-repl-lookahead-id-simp

enumerator CVC5_PROOF_REWRITE_RULE_RE_ALL_ELIM: Auto-generated from RARE rule re-all-elim

enumerator CVC5_PROOF_REWRITE_RULE_RE_OPT_ELIM: Auto-generated from RARE rule re-opt-elim

enumerator CVC5_PROOF_REWRITE_RULE_RE_DIFF_ELIM: Auto-generated from RARE rule re-diff-elim

enumerator CVC5_PROOF_REWRITE_RULE_RE_PLUS_ELIM: Auto-generated from RARE rule re-plus-elim

enumerator CVC5_PROOF_REWRITE_RULE_RE_REPEAT_ELIM: Auto-generated from RARE rule re-repeat-elim

enumerator CVC5_PROOF_REWRITE_RULE_RE_CONCAT_STAR_SWAP: Auto-generated from RARE rule re-concat-star-swap

enumerator CVC5_PROOF_REWRITE_RULE_RE_CONCAT_STAR_REPEAT: Auto-generated from RARE rule re-concat-star-repeat

enumerator CVC5_PROOF_REWRITE_RULE_RE_CONCAT_STAR_SUBSUME1: Auto-generated from RARE rule re-concat-star-subsume1

enumerator CVC5_PROOF_REWRITE_RULE_RE_CONCAT_STAR_SUBSUME2: Auto-generated from RARE rule re-concat-star-subsume2

enumerator CVC5_PROOF_REWRITE_RULE_RE_CONCAT_MERGE: Auto-generated from RARE rule re-concat-merge

enumerator CVC5_PROOF_REWRITE_RULE_RE_UNION_ALL: Auto-generated from RARE rule re-union-all

enumerator CVC5_PROOF_REWRITE_RULE_RE_UNION_CONST_ELIM: Auto-generated from RARE rule re-union-const-elim

enumerator CVC5_PROOF_REWRITE_RULE_RE_INTER_ALL: Auto-generated from RARE rule re-inter-all

enumerator CVC5_PROOF_REWRITE_RULE_RE_STAR_NONE: Auto-generated from RARE rule re-star-none

enumerator CVC5_PROOF_REWRITE_RULE_RE_STAR_EMP: Auto-generated from RARE rule re-star-emp

enumerator CVC5_PROOF_REWRITE_RULE_RE_STAR_STAR: Auto-generated from RARE rule re-star-star

enumerator CVC5_PROOF_REWRITE_RULE_RE_STAR_UNION_DROP_EMP: Auto-generated from RARE rule re-star-union-drop-emp

enumerator CVC5_PROOF_REWRITE_RULE_RE_LOOP_NEG: Auto-generated from RARE rule re-loop-neg

enumerator CVC5_PROOF_REWRITE_RULE_RE_INTER_CSTRING: Auto-generated from RARE rule re-inter-cstring

enumerator CVC5_PROOF_REWRITE_RULE_RE_INTER_CSTRING_NEG: Auto-generated from RARE rule re-inter-cstring-neg

enumerator CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_LEN_INCLUDE: Auto-generated from RARE rule str-substr-len-include

enumerator CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_LEN_INCLUDE_PRE: Auto-generated from RARE rule str-substr-len-include-pre

enumerator CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_LEN_NORM: Auto-generated from RARE rule str-substr-len-norm

enumerator CVC5_PROOF_REWRITE_RULE_SEQ_LEN_REV: Auto-generated from RARE rule seq-len-rev

enumerator CVC5_PROOF_REWRITE_RULE_SEQ_REV_REV: Auto-generated from RARE rule seq-rev-rev

enumerator CVC5_PROOF_REWRITE_RULE_SEQ_REV_CONCAT: Auto-generated from RARE rule seq-rev-concat

enumerator CVC5_PROOF_REWRITE_RULE_STR_EQ_REPL_SELF_EMP: Auto-generated from RARE rule str-eq-repl-self-emp

enumerator CVC5_PROOF_REWRITE_RULE_STR_EQ_REPL_NO_CHANGE: Auto-generated from RARE rule str-eq-repl-no-change

enumerator CVC5_PROOF_REWRITE_RULE_STR_EQ_REPL_TGT_EQ_LEN: Auto-generated from RARE rule str-eq-repl-tgt-eq-len

enumerator CVC5_PROOF_REWRITE_RULE_STR_EQ_REPL_LEN_ONE_EMP_PREFIX: Auto-generated from RARE rule str-eq-repl-len-one-emp-prefix

enumerator CVC5_PROOF_REWRITE_RULE_STR_EQ_REPL_EMP_TGT_NEMP: Auto-generated from RARE rule str-eq-repl-emp-tgt-nemp

enumerator CVC5_PROOF_REWRITE_RULE_STR_EQ_REPL_NEMP_SRC_EMP: Auto-generated from RARE rule str-eq-repl-nemp-src-emp

enumerator CVC5_PROOF_REWRITE_RULE_STR_EQ_REPL_SELF_SRC: Auto-generated from RARE rule str-eq-repl-self-src

enumerator CVC5_PROOF_REWRITE_RULE_SEQ_LEN_UNIT: Auto-generated from RARE rule seq-len-unit

enumerator CVC5_PROOF_REWRITE_RULE_SEQ_NTH_UNIT: Auto-generated from RARE rule seq-nth-unit

enumerator CVC5_PROOF_REWRITE_RULE_SEQ_REV_UNIT: Auto-generated from RARE rule seq-rev-unit

enumerator CVC5_PROOF_REWRITE_RULE_SEQ_LEN_EMPTY: Auto-generated from RARE rule seq-len-empty

enumerator CVC5_PROOF_REWRITE_RULE_RE_IN_EMPTY: Auto-generated from RARE rule re-in-empty

enumerator CVC5_PROOF_REWRITE_RULE_RE_IN_SIGMA: Auto-generated from RARE rule re-in-sigma

enumerator CVC5_PROOF_REWRITE_RULE_RE_IN_SIGMA_STAR: Auto-generated from RARE rule re-in-sigma-star

enumerator CVC5_PROOF_REWRITE_RULE_RE_IN_CSTRING: Auto-generated from RARE rule re-in-cstring

enumerator CVC5_PROOF_REWRITE_RULE_RE_IN_COMP: Auto-generated from RARE rule re-in-comp

enumerator CVC5_PROOF_REWRITE_RULE_STR_IN_RE_UNION_ELIM: Auto-generated from RARE rule str-in-re-union-elim

enumerator CVC5_PROOF_REWRITE_RULE_STR_IN_RE_INTER_ELIM: Auto-generated from RARE rule str-in-re-inter-elim

enumerator CVC5_PROOF_REWRITE_RULE_STR_IN_RE_RANGE_ELIM: Auto-generated from RARE rule str-in-re-range-elim

enumerator CVC5_PROOF_REWRITE_RULE_STR_IN_RE_CONTAINS: Auto-generated from RARE rule str-in-re-contains

enumerator CVC5_PROOF_REWRITE_RULE_STR_IN_RE_FROM_INT_NEMP_DIG_RANGE: Auto-generated from RARE rule str-in-re-from-int-nemp-dig-range

enumerator CVC5_PROOF_REWRITE_RULE_STR_IN_RE_FROM_INT_DIG_RANGE: Auto-generated from RARE rule str-in-re-from-int-dig-range

enumerator CVC5_PROOF_REWRITE_RULE_EQ_REFL: Auto-generated from RARE rule eq-refl

enumerator CVC5_PROOF_REWRITE_RULE_EQ_SYMM: Auto-generated from RARE rule eq-symm

enumerator CVC5_PROOF_REWRITE_RULE_EQ_COND_DEQ: Auto-generated from RARE rule eq-cond-deq

enumerator CVC5_PROOF_REWRITE_RULE_EQ_ITE_LIFT: Auto-generated from RARE rule eq-ite-lift

enumerator CVC5_PROOF_REWRITE_RULE_DISTINCT_BINARY_ELIM: Auto-generated from RARE rule distinct-binary-elim

enumerator CVC5_PROOF_REWRITE_RULE_UF_BV2NAT_INT2BV: Auto-generated from RARE rule uf-bv2nat-int2bv

enumerator CVC5_PROOF_REWRITE_RULE_UF_BV2NAT_INT2BV_EXTEND: Auto-generated from RARE rule uf-bv2nat-int2bv-extend

enumerator CVC5_PROOF_REWRITE_RULE_UF_BV2NAT_INT2BV_EXTRACT: Auto-generated from RARE rule uf-bv2nat-int2bv-extract

enumerator CVC5_PROOF_REWRITE_RULE_UF_INT2BV_BV2NAT: Auto-generated from RARE rule uf-int2bv-bv2nat

enumerator CVC5_PROOF_REWRITE_RULE_UF_BV2NAT_GEQ_ELIM: Auto-generated from RARE rule uf-bv2nat-geq-elim

enumerator CVC5_PROOF_REWRITE_RULE_UF_INT2BV_BVULT_EQUIV: Auto-generated from RARE rule uf-int2bv-bvult-equiv

enumerator CVC5_PROOF_REWRITE_RULE_UF_INT2BV_BVULE_EQUIV: Auto-generated from RARE rule uf-int2bv-bvule-equiv

enumerator CVC5_PROOF_REWRITE_RULE_UF_SBV_TO_INT_ELIM: Auto-generated from RARE rule uf-sbv-to-int-elim

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_SINE_ZERO: Auto-generated from RARE rule arith-sine-zero

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_SINE_PI2: Auto-generated from RARE rule arith-sine-pi2

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_COSINE_ELIM: Auto-generated from RARE rule arith-cosine-elim

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_TANGENT_ELIM: Auto-generated from RARE rule arith-tangent-elim

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_SECENT_ELIM: Auto-generated from RARE rule arith-secent-elim

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_COSECENT_ELIM: Auto-generated from RARE rule arith-cosecent-elim

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_COTANGENT_ELIM: Auto-generated from RARE rule arith-cotangent-elim

enumerator CVC5_PROOF_REWRITE_RULE_ARITH_PI_NOT_INT: Auto-generated from RARE rule arith-pi-not-int

enumerator CVC5_PROOF_REWRITE_RULE_SETS_CARD_SINGLETON: Auto-generated from RARE rule sets-card-singleton

enumerator CVC5_PROOF_REWRITE_RULE_SETS_CARD_UNION: Auto-generated from RARE rule sets-card-union

enumerator CVC5_PROOF_REWRITE_RULE_SETS_CARD_MINUS: Auto-generated from RARE rule sets-card-minus

enumerator CVC5_PROOF_REWRITE_RULE_SETS_CARD_EMP: Auto-generated from RARE rule sets-card-emp

enumerator CVC5_PROOF_REWRITE_RULE_LAST

const char *cvc5_proof_rewrite_rule_to_string(Cvc5ProofRewriteRule rule)

Get a string representation of a Cvc5ProofRewriteRule.

Parameters:: rule – The proof rewrite rule.
Returns:: The string representation.

size_t cvc5_proof_rewrite_rule_hash(Cvc5ProofRewriteRule rule)

Hash function for Cvc5ProofRewriteRule.

Parameters:: rule – The proof rewrite rule.
Returns:: The hash value.