Proof Rules
This section introduces two enumerations: ProofRule
and ProofRewriteRule
.
The ProofRule
enumeration captures the reasoning steps performed by the SAT solver, the theory solvers or by the preprocessor. It represents the inference rules used to derive conclusions within a proof.
The ProofRewriteRule
enumeration pertains to rewrites performed on terms. These identifiers are arguments of the proof rules THEORY_REWRITE
and DSL_REWRITE
.
enum class
cvc5::ProofRule
std::ostream& cvc5::operator<< (std::ostream& out, ProofRule pc)
enum class
cvc5::ProofRewriteRule
std::ostream& cvc5::operator<< (std::ostream& out, ProofRewriteRule pc)

enum class cvc5::ProofRule
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 Nodelevel 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 postprocessing.Values:

enumerator ASSUME
Assumption (a leaf)
\[\inferrule{ \mid F}{F}\]This rule has special status, in that an application of assume is an open leaf in a proof that is not (yet) justified. An assume leaf is analogous to a free variable in a term, where we say “F is a free assumption in proof P” if it contains an application of F that is not bound by
SCOPE
(see below).

enumerator SCOPE
Scope (a binder for assumptions)
\[\inferruleSC{F \mid F_1 \dots F_n}{(F_1 \land \dots \land F_n) \Rightarrow F}{if $F\neq\bot$} \textrm{ or } \inferruleSC{F \mid F_1 \dots F_n}{\neg (F_1 \land \dots \land F_n)}{if $F=\bot$}\]This rule has a dual purpose with
ASSUME
. It is a way to close assumptions in a proof. We require that \(F_1 \dots F_n\) are free assumptions in P and say that \(F_1 \dots F_n\) are not free in(SCOPE P)
. In other words, they are bound by this application. For example, the proof node:(SCOPE (ASSUME F) :args F)
has the conclusion \(F \Rightarrow F\) and has no free assumptions. More generally, a proof with no free assumptions always concludes a valid formula.

enumerator SUBS
Builtin theory – Substitution
\[\inferrule{F_1 \dots F_n \mid t, ids?}{t = t \circ \sigma_{ids}(F_n) \circ \cdots \circ \sigma_{ids}(F_1)}\]where \(\sigma_{ids}(F_i)\) are substitutions, which notice are applied in reverse order. Notice that \(ids\) is a MethodId identifier, which determines how to convert the formulas \(F_1 \dots F_n\) into substitutions. It is an optional argument, where by default the premises are equalities of the form (= x y) and converted into substitutions \(x\mapsto y\).

enumerator MACRO_REWRITE
Builtin theory – Rewrite
\[\inferrule{ \mid t, idr}{t = \texttt{Rewriter}_{idr}(t)}\]where \(idr\) is a MethodId identifier, which determines the kind of rewriter to apply, e.g. Rewriter::rewrite.

enumerator EVALUATE
Builtin theory – Evaluate
\[\inferrule{ \mid t}{t = \texttt{Evaluator::evaluate}(t)}\]Note this is equivalent to:
(REWRITE t MethodId::RW_EVALUATE)
.

enumerator ACI_NORM
Builtin theory – associative/commutative/idempotency/identity normalization
\[\inferrule{ \mid t = s}{t = s}\]where \(\texttt{expr::isACNorm(t, s)} = \top\). This method normalizes currently based on two kinds of operators: (1) those that are associative, commutative, idempotent, and have an identity element (examples are or, and, bvand), (2) those that are associative and have an identity element (examples are str.++, re.++).

enumerator MACRO_SR_EQ_INTRO
Builtin theory – Substitution + Rewriting equality introduction
In this rule, we provide a term \(t\) and conclude that it is equal to its rewritten form under a (proven) substitution.
\[\inferrule{F_1 \dots F_n \mid t, (ids (ida (idr)?)?)?}{t = \texttt{Rewriter}_{idr}(t \circ \sigma_{ids, ida}(F_n) \circ \cdots \circ \sigma_{ids, ida}(F_1))}\]In other words, from the point of view of Skolem forms, this rule transforms \(t\) to \(t'\) by standard substitution + rewriting.
The arguments \(ids\), \(ida\) and \(idr\) are optional and specify the identifier of the substitution, the substitution application and rewriter respectively to be used. For details, see theory/builtin/proof_checker.h.

enumerator MACRO_SR_PRED_INTRO
Builtin theory – Substitution + Rewriting predicate introduction
In this rule, we provide a formula \(F\) and conclude it, under the condition that it rewrites to true under a proven substitution.
\[\inferrule{F_1 \dots F_n \mid F, (ids (ida (idr)?)?)?}{F}\]where \(\texttt{Rewriter}_{idr}(F \circ \sigma_{ids, ida}(F_n) \circ \cdots \circ \sigma_{ids, ida}(F_1)) = \top\) and \(ids\) and \(idr\) are method identifiers.
More generally, this rule also holds when \(\texttt{Rewriter::rewrite}(\texttt{toOriginal}(F')) = \top\) where \(F'\) is the result of the left hand side of the equality above. Here, notice that we apply rewriting on the original form of \(F'\), meaning that this rule may conclude an \(F\) whose Skolem form is justified by the definition of its (fresh) Skolem variables. For example, this rule may justify the conclusion \(k = t\) where \(k\) is the purification Skolem for \(t\), e.g. where the original form of \(k\) is \(t\).
Furthermore, notice that the rewriting and substitution is applied only within the side condition, meaning the rewritten form of the original form of \(F\) does not escape this rule.

enumerator MACRO_SR_PRED_ELIM
Builtin theory – Substitution + Rewriting predicate elimination
\[\inferrule{F, F_1 \dots F_n \mid (ids (ida (idr)?)?)?}{\texttt{Rewriter}_{idr}(F \circ \sigma_{ids, ida}(F_n) \circ \cdots \circ \sigma_{ids, ida}(F_1))}\]where \(ids\) and \(idr\) are method identifiers.
We rewrite only on the Skolem form of \(F\), similar to
MACRO_SR_EQ_INTRO
.

enumerator MACRO_SR_PRED_TRANSFORM
Builtin theory – Substitution + Rewriting predicate elimination
\[\inferrule{F, F_1 \dots F_n \mid G, (ids (ida (idr)?)?)?}{G}\]where \(\texttt{Rewriter}_{idr}(F \circ \sigma_{ids, ida}(F_n) \circ \cdots \circ \sigma_{ids, ida}(F_1)) = \texttt{Rewriter}_{idr}(G \circ \sigma_{ids, ida}(F_n) \circ \cdots \circ \sigma_{ids, ida}(F_1))\).
More generally, this rule also holds when: \(\texttt{Rewriter::rewrite}(\texttt{toOriginal}(F')) = \texttt{Rewriter::rewrite}(\texttt{toOriginal}(G'))\) where \(F'\) and \(G'\) are the result of each side of the equation above. Here, original forms are used in a similar manner to
MACRO_SR_PRED_INTRO
above.

enumerator ENCODE_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 noop in external proof formats.
Note this rule can be treated as a
REFL
when appropriate in external proof formats.

enumerator DSL_REWRITE
Builtin theory – DSL rewrite
\[\inferrule{F_1 \dots F_n \mid id t_1 \dots t_n}{F}\]where id is a
ProofRewriteRule
whose definition in the RARE DSL is \(\forall x_1 \dots x_n. (G_1 \wedge G_n) \Rightarrow G\) where for \(i=1, \dots n\), we have that \(F_i = \sigma(G_i)\) and \(F = \sigma(G)\) where \(\sigma\) is the substitution \(\{x_1\mapsto t_1,\dots,x_n\mapsto t_n\}\).Notice that the application of the substitution takes into account the possible list semantics of variables \(x_1 \ldots x_n\). If \(x_i\) is a variable with list semantics, then \(t_i\) denotes a list of terms. The substitution implemented by expr::narySubstitute replaces each \(x_i\) with the list \(t_i\) in its place.

enumerator THEORY_REWRITE
Other theory rewrite rules
\[\inferrule{ \mid id, t = t'}{t = t'}\]where id is the
ProofRewriteRule
of the theory rewrite rule which transforms \(t\) to \(t'\).In contrast to
DSL_REWRITE
, theory rewrite rules used by this proof rule are not necessarily expressible in RARE. Each rule that can be used in this proof rule are documented explicitly in cases within theProofRewriteRule
enum.

enumerator ANNOTATION
Builtin theory – Annotation
\[\inferrule{F \mid a_1 \dots a_n}{F}\]The terms \(a_1 \dots a_n\) can be anything used to annotate the proof node, one example is where \(a_1\) is a theory::InferenceId.

enumerator ITE_EQ
Processing rules – Ifthenelse equivalence
\[\inferrule{ \mid \ite{C}{t_1}{t_2}}{\ite{C}{((\ite{C}{t_1}{t_2}) = t_1)}{((\ite{C}{t_1}{t_2}) = t_2)}}\]

enumerator TRUST
Trusted rule
\[\inferrule{F_1 \dots F_n \mid tid, F, ...}{F}\]where \(tid\) is an identifier and \(F\) is a formula. This rule is used when a formal justification of an inference step cannot be provided. The formulas \(F_1 \dots F_n\) refer to a set of formulas that entail \(F\), which may or may not be provided.

enumerator TRUST_THEORY_REWRITE
Trusted rules – Theory rewrite
\[\inferrule{ \mid F, tid, rid}{F}\]where \(F\) is an equality of the form \(t = t'\) where \(t'\) is obtained by applying the kind of rewriting given by the method identifier \(rid\), which is one of:
RW_REWRITE_THEORY_PRE
,RW_REWRITE_THEORY_POST
,RW_REWRITE_EQ_EXT
. Notice that the checker for this rule does not replay the rewrite to ensure correctness, since theory rewriter methods are not static. For example, the quantifiers rewriter involves constructing new bound variables that are not guaranteed to be consistent on each call.

enumerator SAT_REFUTATION
SAT Refutation for assumptionbased unsat cores
\[\inferrule{F_1 \dots F_n \mid }{\bot}\]where \(F_1 \dots F_n\) correspond to the unsat core determined by the SAT solver.

enumerator DRAT_REFUTATION
DRAT Refutation
\[\inferrule{F_1 \dots F_n \mid D, P}{\bot}\]where \(F_1 \dots F_n\) correspond to the clauses in the DIMACS file given by filename D and P is a filename of a file storing a DRAT proof.

enumerator SAT_EXTERNAL_PROVE
SAT external prove Refutation
\[\inferrule{F_1 \dots F_n \mid D}{\bot}\]where \(F_1 \dots F_n\) correspond to the input clauses in the DIMACS file D.

enumerator RESOLUTION
Boolean – Resolution
\[\inferrule{C_1, C_2 \mid pol, L}{C}\]where
\(C_1\) and \(C_2\) are nodes viewed as clauses, i.e., either an
OR
node with each children viewed as a literal or a node viewed as a literal. Note that anOR
node could also be a literal.\(pol\) is either true or false, representing the polarity of the pivot on the first clause
\(L\) is the pivot of the resolution, which occurs as is (resp. under a
NOT
) in \(C_1\) and negatively (as is) in \(C_2\) if \(pol = \top\) (\(pol = \bot\)).
\(C\) is a clause resulting from collecting all the literals in \(C_1\), minus the first occurrence of the pivot or its negation, and \(C_2\), minus the first occurrence of the pivot or its negation, according to the policy above. If the resulting clause has a single literal, that literal itself is the result; if it has no literals, then the result is false; otherwise it’s an
OR
node of the resulting literals.Note that it may be the case that the pivot does not occur in the clauses. In this case the rule is not unsound, but it does not correspond to resolution but rather to a weakening of the clause that did not have a literal eliminated.

enumerator CHAIN_RESOLUTION
Boolean – Nary Resolution
\[\inferrule{C_1 \dots C_n \mid (pol_1 \dots pol_{n1}), (L_1 \dots L_{n1})}{C}\]where
let \(C_1 \dots C_n\) be nodes viewed as clauses, as defined above
let \(C_1 \diamond_{L,\mathit{pol}} C_2\) represent the resolution of \(C_1\) with \(C_2\) with pivot \(L\) and polarity \(pol\), as defined above
let \(C_1' = C_1\),
for each \(i > 1\), let \(C_i' = C_{i1} \diamond{L_{i1}, \mathit{pol}_{i1}} C_i'\)
Note the list of polarities and pivots are provided as sexpressions.
The result of the chain resolution is \(C = C_n'\)

enumerator FACTORING
Boolean – Factoring
\[\inferrule{C_1 \mid }{C_2}\]where \(C_2\) is the clause \(C_1\), but every occurrence of a literal after its first occurrence is omitted.

enumerator REORDERING
Boolean – Reordering
\[\inferrule{C_1 \mid C_2}{C_2}\]where the set representations of \(C_1\) and \(C_2\) are the same and the number of literals in \(C_2\) is the same of that of \(C_1\).

enumerator MACRO_RESOLUTION
Boolean – Nary Resolution + Factoring + Reordering
\[\inferrule{C_1 \dots C_n \mid C, pol_1,L_1 \dots pol_{n1},L_{n1}}{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_{i1} \diamond{L_{i1},\mathit{pol}_{i1}} C_i'\)
The result of the chain resolution is \(C\), which is equal, in its set representation, to \(C_n'\)

enumerator MACRO_RESOLUTION_TRUST
Boolean – Nary Resolution + Factoring + Reordering unchecked
Same as
MACRO_RESOLUTION
, but not checked by the internal proof checker.

enumerator SPLIT
Boolean – Split
\[\inferrule{ \mid F}{F \lor \neg F}\]

enumerator EQ_RESOLVE
Boolean – Equality resolution
\[\inferrule{F_1, (F_1 = F_2) \mid }{F_2}\]Note this can optionally be seen as a macro for
EQUIV_ELIM1
+RESOLUTION
.

enumerator MODUS_PONENS
Boolean – Modus Ponens
\[\inferrule{F_1, (F_1 \rightarrow F_2) \mid }{F_2}\]Note this can optionally be seen as a macro for
IMPLIES_ELIM
+RESOLUTION
.

enumerator NOT_NOT_ELIM
Boolean – Double negation elimination
\[\inferrule{\neg (\neg F) \mid }{F}\]

enumerator CONTRA
Boolean – Contradiction
\[\inferrule{F, \neg F \mid }{\bot}\]

enumerator AND_ELIM
Boolean – And elimination
\[\inferrule{(F_1 \land \dots \land F_n) \mid i}{F_i}\]

enumerator AND_INTRO
Boolean – And introduction
\[\inferrule{F_1 \dots F_n \mid }{(F_1 \land \dots \land F_n)}\]

enumerator NOT_OR_ELIM
Boolean – Not Or elimination
\[\inferrule{\neg(F_1 \lor \dots \lor F_n) \mid i}{\neg F_i}\]

enumerator IMPLIES_ELIM
Boolean – Implication elimination
\[\inferrule{F_1 \rightarrow F_2 \mid }{\neg F_1 \lor F_2}\]

enumerator NOT_IMPLIES_ELIM1
Boolean – Not Implication elimination version 1
\[\inferrule{\neg(F_1 \rightarrow F_2) \mid }{F_1}\]

enumerator NOT_IMPLIES_ELIM2
Boolean – Not Implication elimination version 2
\[\inferrule{\neg(F_1 \rightarrow F_2) \mid }{\neg F_2}\]

enumerator EQUIV_ELIM1
Boolean – Equivalence elimination version 1
\[\inferrule{F_1 = F_2 \mid }{\neg F_1 \lor F_2}\]

enumerator EQUIV_ELIM2
Boolean – Equivalence elimination version 2
\[\inferrule{F_1 = F_2 \mid }{F_1 \lor \neg F_2}\]

enumerator NOT_EQUIV_ELIM1
Boolean – Not Equivalence elimination version 1
\[\inferrule{F_1 \neq F_2 \mid }{F_1 \lor F_2}\]

enumerator NOT_EQUIV_ELIM2
Boolean – Not Equivalence elimination version 2
\[\inferrule{F_1 \neq F_2 \mid }{\neg F_1 \lor \neg F_2}\]

enumerator XOR_ELIM1
Boolean – XOR elimination version 1
\[\inferrule{F_1 \xor F_2 \mid }{F_1 \lor F_2}\]

enumerator XOR_ELIM2
Boolean – XOR elimination version 2
\[\inferrule{F_1 \xor F_2 \mid }{\neg F_1 \lor \neg F_2}\]

enumerator NOT_XOR_ELIM1
Boolean – Not XOR elimination version 1
\[\inferrule{\neg(F_1 \xor F_2) \mid }{F_1 \lor \neg F_2}\]

enumerator NOT_XOR_ELIM2
Boolean – Not XOR elimination version 2
\[\inferrule{\neg(F_1 \xor F_2) \mid }{\neg F_1 \lor F_2}\]

enumerator ITE_ELIM1
Boolean – ITE elimination version 1
\[\inferrule{(\ite{C}{F_1}{F_2}) \mid }{\neg C \lor F_1}\]

enumerator ITE_ELIM2
Boolean – ITE elimination version 2
\[\inferrule{(\ite{C}{F_1}{F_2}) \mid }{C \lor F_2}\]

enumerator NOT_ITE_ELIM1
Boolean – Not ITE elimination version 1
\[\inferrule{\neg(\ite{C}{F_1}{F_2}) \mid }{\neg C \lor \neg F_1}\]

enumerator NOT_ITE_ELIM2
Boolean – Not ITE elimination version 2
\[\inferrule{\neg(\ite{C}{F_1}{F_2}) \mid }{C \lor \neg F_2}\]

enumerator NOT_AND
Boolean – De Morgan – Not And
\[\inferrule{\neg(F_1 \land \dots \land F_n) \mid }{\neg F_1 \lor \dots \lor \neg F_n}\]

enumerator CNF_AND_POS
Boolean – CNF – And Positive
\[\inferrule{ \mid (F_1 \land \dots \land F_n), i}{\neg (F_1 \land \dots \land F_n) \lor F_i}\]

enumerator CNF_AND_NEG
Boolean – CNF – And Negative
\[\inferrule{ \mid (F_1 \land \dots \land F_n)}{(F_1 \land \dots \land F_n) \lor \neg F_1 \lor \dots \lor \neg F_n}\]

enumerator CNF_OR_POS
Boolean – CNF – Or Positive
\[\inferrule{ \mid (F_1 \lor \dots \lor F_n)}{\neg(F_1 \lor \dots \lor F_n) \lor F_1 \lor \dots \lor F_n}\]

enumerator CNF_OR_NEG
Boolean – CNF – Or Negative
\[\inferrule{ \mid (F_1 \lor \dots \lor F_n), i}{(F_1 \lor \dots \lor F_n) \lor \neg F_i}\]

enumerator CNF_IMPLIES_POS
Boolean – CNF – Implies Positive
\[\inferrule{ \mid F_1 \rightarrow F_2}{\neg(F_1 \rightarrow F_2) \lor \neg F_1 \lor F_2}\]

enumerator CNF_IMPLIES_NEG1
Boolean – CNF – Implies Negative 1
\[\inferrule{ \mid F_1 \rightarrow F_2}{(F_1 \rightarrow F_2) \lor F_1}\]

enumerator CNF_IMPLIES_NEG2
Boolean – CNF – Implies Negative 2
\[\inferrule{ \mid F_1 \rightarrow F_2}{(F_1 \rightarrow F_2) \lor \neg F_2}\]

enumerator CNF_EQUIV_POS1
Boolean – CNF – Equiv Positive 1
\[\inferrule{ \mid F_1 = F_2}{F_1 \neq F_2 \lor \neg F_1 \lor F_2}\]

enumerator CNF_EQUIV_POS2
Boolean – CNF – Equiv Positive 2
\[\inferrule{ \mid F_1 = F_2}{F_1 \neq F_2 \lor F_1 \lor \neg F_2}\]

enumerator CNF_EQUIV_NEG1
Boolean – CNF – Equiv Negative 1
\[\inferrule{ \mid F_1 = F_2}{(F_1 = F_2) \lor F_1 \lor F_2}\]

enumerator CNF_EQUIV_NEG2
Boolean – CNF – Equiv Negative 2
\[\inferrule{ \mid F_1 = F_2}{(F_1 = F_2) \lor \neg F_1 \lor \neg F_2}\]

enumerator CNF_XOR_POS1
Boolean – CNF – XOR Positive 1
\[\inferrule{ \mid F_1 \xor F_2}{\neg(F_1 \xor F_2) \lor F_1 \lor F_2}\]

enumerator CNF_XOR_POS2
Boolean – CNF – XOR Positive 2
\[\inferrule{ \mid F_1 \xor F_2}{\neg(F_1 \xor F_2) \lor \neg F_1 \lor \neg F_2}\]

enumerator CNF_XOR_NEG1
Boolean – CNF – XOR Negative 1
\[\inferrule{ \mid F_1 \xor F_2}{(F_1 \xor F_2) \lor \neg F_1 \lor F_2}\]

enumerator CNF_XOR_NEG2
Boolean – CNF – XOR Negative 2
\[\inferrule{ \mid F_1 \xor F_2}{(F_1 \xor F_2) \lor F_1 \lor \neg F_2}\]

enumerator CNF_ITE_POS1
Boolean – CNF – ITE Positive 1
\[\inferrule{ \mid (\ite{C}{F_1}{F_2})}{\neg(\ite{C}{F_1}{F_2}) \lor \neg C \lor F_1}\]

enumerator CNF_ITE_POS2
Boolean – CNF – ITE Positive 2
\[\inferrule{ \mid (\ite{C}{F_1}{F_2})}{\neg(\ite{C}{F_1}{F_2}) \lor C \lor F_2}\]

enumerator CNF_ITE_POS3
Boolean – CNF – ITE Positive 3
\[\inferrule{ \mid (\ite{C}{F_1}{F_2})}{\neg(\ite{C}{F_1}{F_2}) \lor F_1 \lor F_2}\]

enumerator CNF_ITE_NEG1
Boolean – CNF – ITE Negative 1
\[\inferrule{ \mid (\ite{C}{F_1}{F_2})}{(\ite{C}{F_1}{F_2}) \lor \neg C \lor \neg F_1}\]

enumerator CNF_ITE_NEG2
Boolean – CNF – ITE Negative 2
\[\inferrule{ \mid (\ite{C}{F_1}{F_2})}{(\ite{C}{F_1}{F_2}) \lor C \lor \neg F_2}\]

enumerator CNF_ITE_NEG3
Boolean – CNF – ITE Negative 3
\[\inferrule{ \mid (\ite{C}{F_1}{F_2})}{(\ite{C}{F_1}{F_2}) \lor \neg F_1 \lor \neg F_2}\]

enumerator REFL
Equality – Reflexivity
\[\inferrule{\mid t}{t = t}\]

enumerator SYMM
Equality – Symmetry
\[\inferrule{t_1 = t_2\mid }{t_2 = t_1}\]or
\[\inferrule{t_1 \neq t_2\mid }{t_2 \neq t_1}\]

enumerator TRANS
Equality – Transitivity
\[\inferrule{t_1=t_2,\dots,t_{n1}=t_n\mid }{t_1 = t_n}\]

enumerator CONG
Equality – Congruence
\[\inferrule{t_1=s_1,\dots,t_n=s_n\mid k, f?}{k(f?)(t_1,\dots, t_n) = k(f?)(s_1,\dots, s_n)}\]where \(k\) is the application kind. Notice that \(f\) must be provided iff \(k\) is a parameterized kind, e.g. cvc5::Kind::APPLY_UF. The actual node for \(k\) is constructible via
ProofRuleChecker::mkKindNode
. If \(k\) is a binder kind (e.g.cvc5::Kind::FORALL
) then \(f\) is a term of kindcvc5::Kind::VARIABLE_LIST
denoting the variables bound by both sides of the conclusion. This rule is used for kinds that have a fixed arity, such ascvc5::Kind::ITE
,cvc5::Kind::EQUAL
, and so on. It is also used forcvc5::Kind::APPLY_UF
where \(f\) must be provided. It is not used for equality betweencvc5::Kind::HO_APPLY
terms, which should use theHO_CONG
proof rule.

enumerator NARY_CONG
Equality – Nary Congruence
\[\inferrule{t_1=s_1,\dots,t_n=s_n\mid k}{k(t_1,\dots, t_n) = k(s_1,\dots, s_n)}\]where \(k\) is the application kind. The actual node for \(k\) is constructible via
ProofRuleChecker::mkKindNode
. This rule is used for kinds that have variadic arity, such ascvc5::Kind::AND
,cvc5::Kind::PLUS
and so on.

enumerator TRUE_INTRO
Equality – True intro
\[\inferrule{F\mid }{F = \top}\]

enumerator TRUE_ELIM
Equality – True elim
\[\inferrule{F=\top\mid }{F}\]

enumerator FALSE_INTRO
Equality – False intro
\[\inferrule{\neg F\mid }{F = \bot}\]

enumerator FALSE_ELIM
Equality – False elim
\[\inferrule{F=\bot\mid }{\neg F}\]

enumerator HO_APP_ENCODE
Equality – Higherorder application encoding
\[\inferrule{\mid t}{t= \texttt{TheoryUfRewriter::getHoApplyForApplyUf}(t)}\]For example, this rule concludes \(f(x,y) = @(@(f,x),y)\), where \(@\) isthe
HO_APPLY
kind.Note this rule can be treated as a
REFL
when appropriate in external proof formats.

enumerator HO_CONG
Equality – Higherorder congruence
\[\inferrule{f=g, t_1=s_1,\dots,t_n=s_n\mid k}{k(f, t_1,\dots, t_n) = k(g, s_1,\dots, s_n)}\]Notice that this rule is only used when the application kind \(k\) is either cvc5::Kind::APPLY_UF or cvc5::Kind::HO_APPLY.

enumerator ARRAYS_READ_OVER_WRITE
Arrays – Read over write
\[\inferrule{i_1 \neq i_2\mid \mathit{select}(\mathit{store}(a,i_1,e),i_2)} {\mathit{select}(\mathit{store}(a,i_1,e),i_2) = \mathit{select}(a,i_2)}\]

enumerator ARRAYS_READ_OVER_WRITE_CONTRA
Arrays – Read over write, contrapositive
\[\inferrule{\mathit{select}(\mathit{store}(a,i_2,e),i_1) \neq \mathit{select}(a,i_1)\mid }{i_1=i_2}\]

enumerator ARRAYS_READ_OVER_WRITE_1
Arrays – Read over write 1
\[\inferrule{\mid \mathit{select}(\mathit{store}(a,i,e),i)} {\mathit{select}(\mathit{store}(a,i,e),i)=e}\]

enumerator ARRAYS_EXT
Arrays – Arrays extensionality
\[\inferrule{a \neq b\mid } {\mathit{select}(a,k)\neq\mathit{select}(b,k)}\]where \(k\) is the \(\texttt{ARRAY_DEQ_DIFF}\) skolem for (a, b).

enumerator MACRO_BV_BITBLAST
Bitvectors – (Macro) Bitblast
\[\inferrule{\mid t}{t = \texttt{bitblast}(t)}\]where
bitblast()
represents the result of the bitblasted term as a bitvector consisting of the output bits of the bitblasted circuit representation of the term. Terms are bitblasted according to the strategies defined intheory/bv/bitblast/bitblast_strategies_template.h
.

enumerator BV_BITBLAST_STEP
Bitvectors – Bitblast bitvector constant, variable, and terms
For constant and variables:
\[\inferrule{\mid t}{t = \texttt{bitblast}(t)}\]For terms:
\[\inferrule{\mid k(\texttt{bitblast}(t_1),\dots,\texttt{bitblast}(t_n))} {k(\texttt{bitblast}(t_1),\dots,\texttt{bitblast}(t_n)) = \texttt{bitblast}(t)}\]where \(t\) is \(k(t_1,\dots,t_n)\).

enumerator BV_EAGER_ATOM
Bitvectors – Bitvector eager atom
\[\inferrule{\mid F}{F = F[0]}\]where \(F\) is of kind
BITVECTOR_EAGER_ATOM
.

enumerator DT_UNIF
Datatypes – Unification
\[\inferrule{C(t_1,\dots,t_n)= C(s_1,\dots,s_n)\mid i}{t_1 = s_i}\]where \(C\) is a constructor.

enumerator DT_SPLIT
Datatypes – Split
\[\inferrule{\mid t}{\mathit{is}_{C_1}(t)\vee\cdots\vee\mathit{is}_{C_n}(t)}\]where \(C_1,\dots,C_n\) are all the constructors of the type of \(t\).

enumerator DT_CLASH
Datatypes – Clash
\[\inferruleSC{\mathit{is}_{C_i}(t), \mathit{is}_{C_j}(t)\mid }{\bot} {if $i\neq j$}\]

enumerator SKOLEM_INTRO
Quantifiers – Skolem introduction
\[\inferrule{\mid k}{k = t}\]where \(t\) is the unpurified form of skolem \(k\).

enumerator SKOLEMIZE
Quantifiers – Skolemization
\[\inferrule{\exists x_1\dots x_n.\> F\mid }{F\sigma}\]or
\[\inferrule{\neg (\forall x_1\dots x_n.\> F)\mid }{\neg F\sigma}\]where \(\sigma\) maps \(x_1,\dots,x_n\) to their representative skolems obtained by
SkolemManager::mkSkolemize
, returned in the skolems argument of that method. The witness terms for the returned skolems can be obtained bySkolemManager::getWitnessForm
.

enumerator INSTANTIATE
Quantifiers – Instantiation
\[\inferrule{\forall x_1\dots x_n.\> F\mid (t_1 \dots t_n), (id\, (t)?)?} {F\{x_1\mapsto t_1,\dots,x_n\mapsto t_n\}}\]The list of terms to instantiate \((t_1 \dots t_n)\) is provided as an sexpression as the first argument. The optional argument \(id\) indicates the inference id that caused the instantiation. The term \(t\) indicates an additional term (e.g. the trigger) associated with the instantiation, which depends on the id. If the id has prefix
QUANTIFIERS_INST_E_MATCHING
, then \(t\) is the trigger that generated the instantiation.

enumerator ALPHA_EQUIV
Quantifiers – Alpha equivalence
\[\inferruleSC{\mid F, (y_1 \ldots y_n), (z_1,\dots, z_n)} {F = F\{y_1\mapsto z_1,\dots,y_n\mapsto z_n\}} {if $y_1,\dots,y_n, z_1,\dots,z_n$ are unique bound variables}\]Notice that this rule is correct only when \(z_1,\dots,z_n\) are not contained in \(FV(F) \setminus \{ y_1,\dots, y_n \}\), where \(FV(\varphi)\) are the free variables of \(\varphi\). The internal quantifiers proof checker does not currently check that this is the case.

enumerator SETS_SINGLETON_INJ
Sets – Singleton injectivity
\[\inferrule{\mathit{set.singleton}(t) = \mathit{set.singleton}(s)\mid }{t=s}\]

enumerator SETS_EXT
Sets – Sets extensionality
\[\inferrule{a \neq b\mid } {\mathit{set.member}(k,a)\neq\mathit{set.member}(k,b)}\]where \(k\) is the \(\texttt{SETS_DEQ_DIFF}\) skolem for (a, b).

enumerator CONCAT_EQ
Strings – Core rules – Concatenation equality
\[\inferrule{(t_1\cdot\ldots \cdot t_n \cdot t) = (t_1 \cdot\ldots \cdot t_n\cdot s)\mid b}{t = s}\]where \(\cdot\) stands for string concatenation and \(b\) indicates if the direction is reversed.
Notice that \(t\) or \(s\) may be empty, in which case they are implicit in the concatenation above. For example, if the premise is \(x\cdot z = x\), then this rule, with argument \(\bot\), concludes \(z = ''\).
Also note that constants are split, such that for \((\mathsf{'abc'} \cdot x) = (\mathsf{'a'} \cdot y)\), this rule, with argument \(\bot\), concludes \((\mathsf{'bc'} \cdot x) = y\). This splitting is done only for constants such that
Word::splitConstant
returns nonnull.

enumerator CONCAT_UNIFY
Strings – Core rules – Concatenation unification
\[\inferrule{(t_1\cdot t_2) = (s_1 \cdot s_2),\, \mathit{len}(t_1) = \mathit{len}(s_1)\mid b}{t_1 = s_1}\]where \(b\) indicates if the direction is reversed.

enumerator CONCAT_CONFLICT
Strings – Core rules – Concatenation conflict
\[\inferrule{(c_1\cdot t) = (c_2 \cdot s)\mid b}{\bot}\]where \(b\) indicates if the direction is reversed, \(c_1,\,c_2\) are constants such that \(\texttt{Word::splitConstant}(c_1,c_2, \mathit{index},b)\) is null, in other words, neither is a prefix of the other. Note it may be the case that one side of the equality denotes the empty string.
This rule is used exclusively for strings.

enumerator CONCAT_CONFLICT_DEQ
Strings – Core rules – Concatenation conflict for disequal characters
\[\inferrule{(t_1\cdot t) = (s_1 \cdot s), t_1 \neq s_1 \mid b}{\bot}\]where $t_1$ and $s_1$ are constants of length one, or otherwise one side of the equality is the empty sequence and $t_1$ or $s_1$ corresponding to that side is the empty sequence.
This rule is used exclusively for sequences.

enumerator CONCAT_SPLIT
Strings – Core rules – Concatenation split
\[\inferruleSC{(t_1\cdot t_2) = (s_1 \cdot s_2),\, \mathit{len}(t_1) \neq \mathit{len}(s_1)\mid b}{((t_1 = s_1\cdot r) \vee (s_1 = t_1\cdot r)) \wedge r \neq \epsilon \wedge \mathit{len}(r)>0}{if $b=\bot$}\]where \(r\) is \(\mathit{skolem}(\mathit{ite}( \mathit{len}(t_1) >= \mathit{len}(s_1), \mathit{suf}(t_1,\mathit{len}(s_1)), \mathit{suf}(s_1,\mathit{len}(t_1))))\) and epsilon is the empty string (or sequence).
\[\inferruleSC{(t_1\cdot t_2) = (s_1 \cdot s_2),\, \mathit{len}(t_2) \neq \mathit{len}(s_2)\mid b}{((t_2 = r \cdot s_2) \vee (s_2 = r \cdot t_2)) \wedge r \neq \epsilon \wedge \mathit{len}(r)>0}{if $b=\top$}\]where \(r\) is the purification Skolem for \(\mathit{ite}( \mathit{len}(t_2) >= \mathit{len}(s_2), \mathit{pre}(t_2,\mathit{len}(t_2)  \mathit{len}(s_2)), \mathit{pre}(s_2,\mathit{len}(s_2)  \mathit{len}(t_2)))\) and epsilon is the empty string (or sequence).
Above, \(\mathit{suf}(x,n)\) is shorthand for \(\mathit{substr}(x,n, \mathit{len}(x)  n)\) and \(\mathit{pre}(x,n)\) is shorthand for \(\mathit{substr}(x,0,n)\).

enumerator CONCAT_CSPLIT
Strings – Core rules – Concatenation split for constants
\[\inferrule{(t_1\cdot t_2) = (c \cdot s_2),\, \mathit{len}(t_1) \neq 0\mid \bot}{(t_1 = c\cdot r)}\]where \(r\) is \(\mathit{skolem}(\mathit{suf}(t_1,1))\).
Alternatively for the reverse:
\[\inferrule{(t_1\cdot t_2) = (s_1 \cdot c),\, \mathit{len}(t_2) \neq 0\mid \top}{(t_2 = r\cdot c)}\]where \(r\) is \(\mathit{skolem}(\mathit{pre}(t_2,\mathit{len}(t_2)  1))\).

enumerator CONCAT_LPROP
Strings – Core rules – Concatenation length propagation
\[\inferrule{(t_1\cdot t_2) = (s_1 \cdot s_2),\, \mathit{len}(t_1) > \mathit{len}(s_1)\mid \bot}{(t_1 = s_1\cdot r)}\]where \(r\) is the purification Skolem for \(\mathit{skolem}(\mathit{ite}( \mathit{len}(t_1) >= \mathit{len}(s_1), \mathit{suf}(t_1,\mathit{len}(s_1)), \mathit{suf}(s_1,\mathit{len}(t_1))))\).
Alternatively for the reverse:
\[\inferrule{(t_1\cdot t_2) = (s_1 \cdot s_2),\, \mathit{len}(t_2) > \mathit{len}(s_2)\mid \top}{(t_2 = r \cdot s_2)}\]where \(r\) is the purification Skolem for \(\mathit{ite}( \mathit{len}(t_2) >= \mathit{len}(s_2), \mathit{pre}(t_2,\mathit{len}(t_2)  \mathit{len}(s_2)), \mathit{pre}(s_2,\mathit{len}(s_2)  \mathit{len}(t_2)))\)

enumerator CONCAT_CPROP
Strings – Core rules – Concatenation constant propagation
\[\inferrule{(t_1\cdot w_1\cdot t_2) = (w_2 \cdot s),\, \mathit{len}(t_1) \neq 0\mid \bot}{(t_1 = t_3\cdot r)}\]where \(w_1,\,w_2\) are words, \(t_3\) is \(\mathit{pre}(w_2,p)\), \(p\) is \(\texttt{Word::overlap}(\mathit{suf}(w_2,1), w_1)\), and \(r\) is \(\mathit{skolem}(\mathit{suf}(t_1,\mathit{len}(w_3)))\). Note that \(\mathit{suf}(w_2,p)\) is the largest suffix of \(\mathit{suf}(w_2,1)\) that can contain a prefix of \(w_1\); since \(t_1\) is nonempty, \(w_3\) must therefore be contained in \(t_1\).
Alternatively for the reverse:
\[\inferrule{(t_1\cdot w_1\cdot t_2) = (s \cdot w_2),\, \mathit{len}(t_2) \neq 0\mid \top}{(t_2 = r\cdot t_3)}\]where \(w_1,\,w_2\) are words, \(t_3\) is \(\mathit{substr}(w_2, \mathit{len}(w_2)  p, p)\), \(p\) is \(\texttt{Word::roverlap}(\mathit{pre}(w_2, \mathit{len}(w_2)  1), w_1)\), and \(r\) is \(\mathit{skolem}(\mathit{pre}(t_2, \mathit{len}(t_2)  \mathit{len}(w_3)))\). Note that \(\mathit{pre}(w_2, \mathit{len}(w_2)  p)\) is the largest prefix of \(\mathit{pre}(w_2, \mathit{len}(w_2)  1)\) that can contain a suffix of \(w_1\); since \(t_2\) is nonempty, \(w_3\) must therefore be contained in \(t_2\).

enumerator STRING_DECOMPOSE
Strings – Core rules – String decomposition
\[\inferrule{\mathit{len}(t) \geq n\mid \bot}{t = w_1\cdot w_2 \wedge \mathit{len}(w_1) = n}\]where \(w_1\) is \(\mathit{skolem}(\mathit{pre}(t,n)\) and \(w_2\) is \(\mathit{skolem}(\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 STRING_LENGTH_POS
Strings – Core rules – Length positive
\[\inferrule{\mid t}{(\mathit{len}(t) = 0\wedge t= '')\vee \mathit{len}(t) > 0}\]

enumerator STRING_LENGTH_NON_EMPTY
Strings – Core rules – Length nonempty
\[\inferrule{t\neq ''\mid }{\mathit{len}(t) \neq 0}\]

enumerator STRING_REDUCTION
Strings – Extended functions – Reduction
\[\inferrule{\mid t}{R\wedge t = w}\]where \(w\) is \(\texttt{strings::StringsPreprocess::reduce}(t, R, \dots)\). In other words, \(R\) is the reduction predicate for extended term \(t\), and \(w\) is \(skolem(t)\).
Notice that the free variables of \(R\) are \(w\) and the free variables of \(t\).

enumerator STRING_EAGER_REDUCTION
Strings – Extended functions – Eager reduction
\[\inferrule{\mid t}{R}\]where \(R\) is \(\texttt{strings::TermRegistry::eagerReduce}(t)\).

enumerator RE_INTER
Strings – Regular expressions – Intersection
\[\inferrule{t\in R_1,\,t\in R_2\mid }{t\in \mathit{inter}(R_1,R_2)}\]

enumerator RE_UNFOLD_POS
Strings – Regular expressions – Positive Unfold
\[\inferrule{t\in R\mid }{\texttt{RegExpOpr::reduceRegExpPos}(t\in R)}\]corresponding to the onestep unfolding of the premise.

enumerator RE_UNFOLD_NEG
Strings – Regular expressions – Negative Unfold
\[\inferrule{t \not \in \mathit{re}.\text{*}(R) \mid }{t \neq \ '' \ \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 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_{n1})}\]where \(r_n\) has fixed length \(L\).

enumerator STRING_CODE_INJ
Strings – Code points
\[\inferrule{\mid t,s}{\mathit{to\_code}(t) = 1 \vee \mathit{to\_code}(t) \neq \mathit{to\_code}(s) \vee t = s}\]

enumerator STRING_SEQ_UNIT_INJ
Strings – Sequence unit
\[\inferrule{\mathit{unit}(x) = \mathit{unit}(y)\mid }{x = y}\]Also applies to the case where \(\mathit{unit}(y)\) is a constant sequence of length one.

enumerator MACRO_STRING_INFERENCE
Strings – (Macro) String inference
\[\inferrule{?\mid F,\mathit{id},\mathit{isRev},\mathit{exp}}{F}\]used to bookkeep an inference that has not yet been converted via \(\texttt{strings::InferProofCons::convert}\).

enumerator MACRO_RE_ELIM
Strings – Regular expressions – Macro elimination
\[\inferrule{\mid F,b}{F = \texttt{strings::RegExpElimination::eliminate}(F, b)}\]where \(b\) is a Boolean indicating whether we are using aggressive eliminations. Notice this rule concludes \(F = F\) if no eliminations are performed for \(F\).
rst .. note:: We do not currently support elaboration of this macro.

enumerator MACRO_ARITH_SCALE_SUM_UB
Arithmetic – Adding inequalities
An arithmetic literal is a term of the form \(p \diamond c\) where \(\diamond \in \{ <, \leq, =, \geq, > \}\), \(p\) a polynomial and \(c\) a rational constant.
\[\inferrule{l_1 \dots l_n \mid k_1 \dots k_n}{t_1 \diamond t_2}\]where \(k_i \in \mathbb{R}, k_i \neq 0\), \(\diamond\) is the fusion of the \(\diamond_i\) (flipping each if its \(k_i\) is negative) such that \(\diamond_i \in \{ <, \leq \}\) (this implies that lower bounds have negative \(k_i\) and upper bounds have positive \(k_i\)), \(t_1\) is the sum of the scaled polynomials and \(t_2\) is the sum of the scaled constants:
\[ \begin{align}\begin{aligned}t_1 \colon= k_1 \cdot p_1 + \cdots + k_n \cdot p_n\\t_2 \colon= k_1 \cdot c_1 + \cdots + k_n \cdot c_n\end{aligned}\end{align} \]

enumerator ARITH_SUM_UB
Arithmetic – Sum upper bounds
\[\inferrule{P_1 \dots P_n \mid }{L \diamond R}\]where \(P_i\) has the form \(L_i \diamond_i R_i\) and \(\diamond_i \in \{<, \leq, =\}\). Furthermore \(\diamond = <\) if \(\diamond_i = <\) for any \(i\) and \(\diamond = \leq\) otherwise, \(L = L_1 + \cdots + L_n\) and \(R = R_1 + \cdots + R_n\).

enumerator INT_TIGHT_UB
Arithmetic – Tighten strict integer upper bounds
\[\inferrule{i < c \mid }{i \leq \lfloor c \rfloor}\]where \(i\) has integer type.

enumerator INT_TIGHT_LB
Arithmetic – Tighten strict integer lower bounds
\[\inferrule{i > c \mid }{i \geq \lceil c \rceil}\]where \(i\) has integer type.

enumerator ARITH_TRICHOTOMY
Arithmetic – Trichotomy of the reals
\[\inferrule{A, B \mid }{C}\]where \(\neg A, \neg B, C\) are \(x < c, x = c, x > c\) in some order. Note that \(\neg\) here denotes arithmetic negation, i.e., flipping \(\geq\) to \(<\) etc.

enumerator ARITH_OP_ELIM_AXIOM
Arithmetic – Operator elimination
\[\inferrule{ \mid t}{\texttt{arith::OperatorElim::getAxiomFor(t)}}\]

enumerator ARITH_POLY_NORM
Arithmetic – Polynomial normalization
\[\inferrule{ \mid t = s}{t = s}\]where \(\texttt{arith::PolyNorm::isArithPolyNorm(t, s)} = \top\). This method normalizes polynomials over arithmetic or bitvectors.

enumerator ARITH_MULT_SIGN
Arithmetic – Sign inference
\[\inferrule{ \mid f_1 \dots f_k, m}{(f_1 \land \dots \land f_k) \rightarrow m \diamond 0}\]where \(f_1 \dots f_k\) are variables compared to zero (less, greater or not equal), \(m\) is a monomial from these variables and \(\diamond\) is the comparison (less or equal) that results from the signs of the variables. All variables with even exponent in \(m\) should be given as not equal to zero while all variables with odd exponent in \(m\) should be given as less or greater than zero.

enumerator ARITH_MULT_POS
Arithmetic – Multiplication with positive factor
\[\inferrule{ \mid m, l \diamond r}{(m > 0 \land l \diamond r) \rightarrow m \cdot l \diamond m \cdot r}\]where \(\diamond\) is a relation symbol.

enumerator ARITH_MULT_NEG
Arithmetic – Multiplication with negative factor
\[\inferrule{ \mid m, l \diamond r}{(m < 0 \land l \diamond r) \rightarrow m \cdot l \diamond_{inv} m \cdot r}\]where \(\diamond\) is a relation symbol and \(\diamond_{inv}\) the inverted relation symbol.

enumerator ARITH_MULT_TANGENT
Arithmetic – Multiplication tangent plane
\[ \begin{align}\begin{aligned}\inferruleSC{ \mid x, y, a, b, \sigma}{(t \leq tplane) \leftrightarrow ((x \leq a \land y \geq b) \lor (x \geq a \land y \leq b))}{if $\sigma = 1$}\\\inferruleSC{ \mid x, y, a, b, \sigma}{(t \geq tplane) \leftrightarrow ((x \leq a \land y \leq b) \lor (x \geq a \land y \geq b))}{if $\sigma = 1$}\end{aligned}\end{align} \]where \(x,y\) are real terms (variables or extended terms), \(t = x \cdot y\), \(a,b\) are real constants, \(\sigma \in \{ 1, 1\}\) and \(tplane := b \cdot x + a \cdot y  a \cdot b\) is the tangent plane of \(x \cdot y\) at \((a,b)\).

enumerator ARITH_TRANS_PI
Arithmetic – Transcendentals – Assert bounds on Pi
\[\inferrule{ \mid l, u}{\texttt{real.pi} \geq l \land \texttt{real.pi} \leq u}\]where \(l,u\) are valid lower and upper bounds on \(\pi\).

enumerator ARITH_TRANS_EXP_NEG
Arithmetic – Transcendentals – Exp at negative values
\[\inferrule{ \mid t}{(t < 0) \leftrightarrow (\exp(t) < 1)}\]

enumerator ARITH_TRANS_EXP_POSITIVITY
Arithmetic – Transcendentals – Exp is always positive
\[\inferrule{ \mid t}{\exp(t) > 0}\]

enumerator ARITH_TRANS_EXP_SUPER_LIN
Arithmetic – Transcendentals – Exp grows superlinearly for positive values
\[\inferrule{ \mid t}{t \leq 0 \lor \exp(t) > t+1}\]

enumerator ARITH_TRANS_EXP_ZERO
Arithmetic – Transcendentals – Exp at zero
\[\inferrule{ \mid t}{(t=0) \leftrightarrow (\exp(t) = 1)}\]

enumerator ARITH_TRANS_EXP_APPROX_ABOVE_NEG
Arithmetic – Transcendentals – Exp is approximated from above for negative values
\[\inferrule{ \mid d,t,l,u}{(t \geq l \land t \leq u) \rightarrow exp(t) \leq \texttt{secant}(\exp, l, u, t)}\]where \(d\) is an even positive number, \(t\) an arithmetic term and \(l,u\) are lower and upper bounds on \(t\). Let \(p\) be the \(d\)’th taylor polynomial at zero (also called the Maclaurin series) of the exponential function. \(\texttt{secant}(\exp, l, u, t)\) denotes the secant of \(p\) from \((l, \exp(l))\) to \((u, \exp(u))\) evaluated at \(t\), calculated as follows:
\[\frac{p(l)  p(u)}{l  u} \cdot (t  l) + p(l)\]The lemma states that if \(t\) is between \(l\) and \(u\), then \(\exp(t\) is below the secant of \(p\) from \(l\) to \(u\).

enumerator ARITH_TRANS_EXP_APPROX_ABOVE_POS
Arithmetic – Transcendentals – Exp is approximated from above for positive values
\[\inferrule{ \mid d,t,l,u}{(t \geq l \land t \leq u) \rightarrow exp(t) \leq \texttt{secantpos}(\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(d1)\) is the regular Maclaurin series of degree \(d1\):
\[p^* := p(d1) \cdot \frac{1 + t^n}{n!}\]\(\texttt{secantpos}(\exp, l, u, t)\) denotes the secant of \(p\) from \((l, \exp(l))\) to \((u, \exp(u))\) evaluated at \(t\), calculated as follows:
\[\frac{p(l)  p(u)}{l  u} \cdot (t  l) + p(l)\]The lemma states that if \(t\) is between \(l\) and \(u\), then \(\exp(t\) is below the secant of \(p\) from \(l\) to \(u\).

enumerator ARITH_TRANS_EXP_APPROX_BELOW
Arithmetic – Transcendentals – Exp is approximated from below
\[\inferrule{ \mid d,c,t}{t \geq c \rightarrow exp(t) \geq \texttt{maclaurin}(\exp, d, c)}\]where \(d\) is an odd positive number, \(t\) an arithmetic term and \(\texttt{maclaurin}(\exp, d, c)\) is the \(d\)’th taylor polynomial at zero (also called the Maclaurin series) of the exponential function evaluated at \(c\). The Maclaurin series for the exponential function is the following:
\[\exp(x) = \sum_{n=0}^{\infty} \frac{x^n}{n!}\]

enumerator ARITH_TRANS_SINE_BOUNDS
Arithmetic – Transcendentals – Sine is always between 1 and 1
\[\inferrule{ \mid t}{\sin(t) \leq 1 \land \sin(t) \geq 1}\]

enumerator ARITH_TRANS_SINE_SHIFT
Arithmetic – Transcendentals – Sine is shifted to pi…pi
\[\inferrule{ \mid x, y, s}{\pi \leq y \leq \pi \land \sin(y) = \sin(x) \land (\ite{\pi \leq x \leq \pi}{x = y}{x = y + 2 \pi s})}\]where \(x\) is the argument to sine, \(y\) is a new real skolem that is \(x\) shifted into \(\pi \dots \pi\) and \(s\) is a new integer slolem that is the number of phases \(y\) is shifted.

enumerator ARITH_TRANS_SINE_SYMMETRY
Arithmetic – Transcendentals – Sine is symmetric with respect to negation of the argument
\[\inferrule{ \mid t}{\sin(t)  \sin(t) = 0}\]

enumerator ARITH_TRANS_SINE_TANGENT_ZERO
Arithmetic – Transcendentals – Sine is bounded by the tangent at zero
\[\inferrule{ \mid t}{(t > 0 \rightarrow \sin(t) < t) \land (t < 0 \rightarrow \sin(t) > t)} \]

enumerator ARITH_TRANS_SINE_TANGENT_PI
Arithmetic – Transcendentals – Sine is bounded by the tangents at pi and pi
\[\inferrule{ \mid t}{(t > \pi \rightarrow \sin(t) > \pi  t) \land (t < \pi \rightarrow \sin(t) < \pi  t)} \]

enumerator ARITH_TRANS_SINE_APPROX_ABOVE_NEG
Arithmetic – Transcendentals – Sine is approximated from above for negative values
\[\inferrule{ \mid d,t,lb,ub,l,u}{(t \geq lb land t \leq ub) \rightarrow \sin(t) \leq \texttt{secant}(\sin, l, u, t)}\]where \(d\) is an even positive number, \(t\) an arithmetic term, \(lb,ub\) are symbolic lower and upper bounds on \(t\) (possibly containing \(\pi\)) and \(l,u\) the evaluated lower and upper bounds on \(t\). Let \(p\) be the \(d\)’th taylor polynomial at zero (also called the Maclaurin series) of the sine function. \(\texttt{secant}(\sin, l, u, t)\) denotes the secant of \(p\) from \((l, \sin(l))\) to \((u, \sin(u))\) evaluated at \(t\), calculated as follows:
\[\frac{p(l)  p(u)}{l  u} \cdot (t  l) + p(l)\]The lemma states that if \(t\) is between \(l\) and \(u\), then \(\sin(t)\) is below the secant of \(p\) from \(l\) to \(u\).

enumerator ARITH_TRANS_SINE_APPROX_ABOVE_POS
Arithmetic – Transcendentals – Sine is approximated from above for positive values
\[\inferrule{ \mid d,t,c,lb,ub}{(t \geq lb land t \leq ub) \rightarrow \sin(t) \leq \texttt{upper}(\sin, c)}\]where \(d\) is an even positive number, \(t\) an arithmetic term, \(c\) an arithmetic constant and \(lb,ub\) are symbolic lower and upper bounds on \(t\) (possibly containing \(\pi\)). Let \(p\) be the \(d\)’th taylor polynomial at zero (also called the Maclaurin series) of the sine function. \(\texttt{upper}(\sin, c)\) denotes the upper bound on \(\sin(c)\) given by \(p\) and \(lb,up\) such that \(\sin(t)\) is the maximum of the sine function on \((lb,ub)\).

enumerator ARITH_TRANS_SINE_APPROX_BELOW_NEG
Arithmetic – Transcendentals – Sine is approximated from below for negative values
\[\inferrule{ \mid d,t,c,lb,ub}{(t \geq lb land t \leq ub) \rightarrow \sin(t) \geq \texttt{lower}(\sin, c)}\]where \(d\) is an even positive number, \(t\) an arithmetic term, \(c\) an arithmetic constant and \(lb,ub\) are symbolic lower and upper bounds on \(t\) (possibly containing \(\pi\)). Let \(p\) be the \(d\)’th taylor polynomial at zero (also called the Maclaurin series) of the sine function. \(\texttt{lower}(\sin, c)\) denotes the lower bound on \(\sin(c)\) given by \(p\) and \(lb,up\) such that \(\sin(t)\) is the minimum of the sine function on \((lb,ub)\).

enumerator ARITH_TRANS_SINE_APPROX_BELOW_POS
Arithmetic – Transcendentals – Sine is approximated from below for positive values
\[\inferrule{ \mid d,t,lb,ub,l,u}{(t \geq lb land t \leq ub) \rightarrow \sin(t) \geq \texttt{secant}(\sin, l, u, t)}\]where \(d\) is an even positive number, \(t\) an arithmetic term, \(lb,ub\) are symbolic lower and upper bounds on \(t\) (possibly containing \(\pi\)) and \(l,u\) the evaluated lower and upper bounds on \(t\). Let \(p\) be the \(d\)’th taylor polynomial at zero (also called the Maclaurin series) of the sine function. \(\texttt{secant}(\sin, l, u, t)\) denotes the secant of \(p\) from \((l, \sin(l))\) to \((u, \sin(u))\) evaluated at \(t\), calculated as follows:
\[\frac{p(l)  p(u)}{l  u} \cdot (t  l) + p(l)\]The lemma states that if \(t\) is between \(l\) and \(u\), then \(\sin(t)\) is above the secant of \(p\) from \(l\) to \(u\).

enumerator LFSC_RULE
External – LFSC
Place holder for LFSC rules.
\[\inferrule{P_1, \dots, P_n\mid \texttt{id}, Q, A_1,\dots, A_m}{Q}\]Note that the premises and arguments are arbitrary. It’s expected that \(\texttt{id}\) refer to a proof rule in the external LFSC calculus.

enumerator ALETHE_RULE
External – Alethe
Place holder for Alethe rules.
\[\inferrule{P_1, \dots, P_n\mid \texttt{id}, Q, Q', A_1,\dots, A_m}{Q}\]Note that the premises and arguments are arbitrary. It’s expected that \(\texttt{id}\) refer to a proof rule in the external Alethe calculus, and that \(Q'\) be the representation of Q to be printed by the Alethe printer.

enumerator UNKNOWN

enumerator ASSUME

std::ostream &cvc5::operator<<(std::ostream &out, ProofRule rule)
Writes a proof rule name to a stream.
 Parameters:
out – The stream to write to
rule – The proof rule to write to the stream
 Returns:
The stream

std::string std::to_string(cvc5::ProofRule rule)
Converts a proof rule to a string.
 Parameters:
rule – The proof rule
 Returns:
The name of the proof rule

enum class cvc5::ProofRewriteRule
This enumeration represents the rewrite rules used in a rewrite proof. Some of the rules are internal adhoc rewrites, while others are rewrites specified by the RARE DSL. This enumeration is used as the first argument to the
DSL_REWRITE
proof rule and theTHEORY_REWRITE
proof rule.Values:

enumerator NONE

enumerator DISTINCT_ELIM
Builtin – Distinct elimination
\[\texttt{distinct}(t_1, \ldots, tn) = \bigwedge_{i \neq j} t_i \neq t_j\]

enumerator 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 ARITH_DIV_BY_CONST_ELIM
Arith – Division by constant elimination
\[t / c = t * 1/c\]where \(c\) is a constant.

enumerator 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 ARITH_STRING_PRED_SAFE_APPROX
Arithmetic  strings predicate entailment
\[(>= n 0) = (>= m 0)\]Where \(m\) is a safe underapproximation 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, “HighLevel Abstractions for Simplifying Extended String Constraints in SMT”.

enumerator BETA_REDUCE
Equality – Beta reduction
\[((\lambda x_1 \ldots x_n.\> t) \ t_1 \ldots t_n) = t\{x_1 \mapsto t_1, \ldots, x_n \mapsto t_n\}\]The right hand side of the equality in the conclusion is computed using standard substitution via
Node::substitute
.

enumerator ARRAYS_EQ_RANGE_EXPAND
Arrays – Expansion of array range equality
\[\mathit{eqrange}(a,b,i,j)= \forall x.\> i \leq x \leq j \rightarrow \mathit{select}(a,x)=\mathit{select}(b,x)\]

enumerator EXISTS_ELIM
Quantifiers – Exists elimination
\[\exists x_1\dots x_n.\> F = \neg \forall x_1\dots x_n.\> \neg F\]

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

enumerator 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 QUANT_MINISCOPE
Quantifiers – Miniscoping
\[\forall X.\> F_1 \wedge \ldots \wedge F_n = (\forall X.\> F_1) \wedge \ldots \wedge (\forall X.\> F_n)\]

enumerator 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 DT_INST
Datatypes – Instantiation
\[\mathit{is}_C(t) = (t = C(\mathit{sel}_1(t),\dots,\mathit{sel}_n(t)))\]where \(C\) is the \(n^{\mathit{th}}\) constructor of the type of \(t\), and \(\mathit{is}_C\) is the discriminator (tester) for \(C\).

enumerator DT_COLLAPSE_SELECTOR
Datatypes  collapse selector
\[s_i(c(t_1, \ldots, t_n)) = t_i\]where \(s_i\) is the \(i^{th}\) selector for constructor \(c\).

enumerator DT_COLLAPSE_TESTER
Datatypes  collapse tester
\[\mathit{is}_c(c(t_1, \ldots, t_n)) = true\]or alternatively
\[\mathit{is}_c(d(t_1, \ldots, t_n)) = false\]where \(c\) and \(d\) are distinct constructors.

enumerator DT_COLLAPSE_TESTER_SINGLETON
Datatypes  collapse tester
\[\mathit{is}_c(t) = true\]where \(c\) is the only constructor of its associated datatype.

enumerator DT_CONS_EQ
Datatypes  constructor equality
\[(c(t_1, \ldots, t_n) = c(s_1, \ldots, s_n)) = (t_1 = s_1 \wedge \ldots \wedge t_n = s_n)\]or alternatively
\[(c(t_1, \ldots, t_n) = d(s_1, \ldots, s_m)) = false\]where \(c\) and \(d\) are distinct constructors.

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

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

enumerator BV_ADD_COMBINE_LIKE_TERMS
Bitvectors  Combine like terms during addition by counting terms

enumerator BV_MULT_SIMPLIFY
Bitvectors  Extract negations from multiplicands
\[(a bvmul b bvmul c) \to (a bvmul b c)\]

enumerator BV_BITWISE_SLICING
Bitvectors  Extract continuous substrings of bitvectors
\[(a bvand c) \to (concat (bvand a[i0:j0] c0) ... (bvand a[in:jn] cn))\]where c0,…, cn are maximally continuous substrings of 0 or 1 in the constant c

enumerator RE_LOOP_ELIM
Strings  regular expression loop elimination
\[((\_\ re.loop\ l\ u)\ R) = (re.union\ R^l \ldots R^u)\]where \(u \geq l\).

enumerator 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 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 STR_IN_RE_CONCAT_STAR_CHAR
Strings  string in regular expression concatenation star character
\[\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))
where all strings in \(R\) have length one.

enumerator 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 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 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 SETS_IS_EMPTY_EVAL
Sets  empty tester evaluation
\[\mathit{sets.is\_empty}(as \ \mathit{set.empty} \ (\mathit{Set} \ T)) =\]top
or alternatively:
\[\mathit{sets.is\_empty}(c) = \bot\]where \(c\) is a constant set that is not the empty set.

enumerator ARITH_PLUS_ZERO
Autogenerated from RARE rule arithpluszero

enumerator ARITH_MUL_ONE
Autogenerated from RARE rule arithmulone

enumerator ARITH_MUL_ZERO
Autogenerated from RARE rule arithmulzero

enumerator ARITH_DIV_TOTAL
Autogenerated from RARE rule arithdivtotal

enumerator ARITH_INT_DIV_TOTAL
Autogenerated from RARE rule arithintdivtotal

enumerator ARITH_INT_DIV_TOTAL_ONE
Autogenerated from RARE rule arithintdivtotalone

enumerator ARITH_INT_DIV_TOTAL_ZERO
Autogenerated from RARE rule arithintdivtotalzero

enumerator ARITH_INT_MOD_TOTAL
Autogenerated from RARE rule arithintmodtotal

enumerator ARITH_INT_MOD_TOTAL_ONE
Autogenerated from RARE rule arithintmodtotalone

enumerator ARITH_INT_MOD_TOTAL_ZERO
Autogenerated from RARE rule arithintmodtotalzero

enumerator ARITH_NEG_NEG_ONE
Autogenerated from RARE rule arithnegnegone

enumerator ARITH_ELIM_UMINUS
Autogenerated from RARE rule arithelimuminus

enumerator ARITH_ELIM_MINUS
Autogenerated from RARE rule arithelimminus

enumerator ARITH_ELIM_GT
Autogenerated from RARE rule arithelimgt

enumerator ARITH_ELIM_LT
Autogenerated from RARE rule arithelimlt

enumerator ARITH_ELIM_INT_GT
Autogenerated from RARE rule arithelimintgt

enumerator ARITH_ELIM_INT_LT
Autogenerated from RARE rule arithelimintlt

enumerator ARITH_ELIM_LEQ
Autogenerated from RARE rule arithelimleq

enumerator ARITH_LEQ_NORM
Autogenerated from RARE rule arithleqnorm

enumerator ARITH_GEQ_TIGHTEN
Autogenerated from RARE rule arithgeqtighten

enumerator ARITH_GEQ_NORM1
Autogenerated from RARE rule arithgeqnorm1

enumerator ARITH_GEQ_NORM2
Autogenerated from RARE rule arithgeqnorm2

enumerator ARITH_REFL_LEQ
Autogenerated from RARE rule arithreflleq

enumerator ARITH_REFL_LT
Autogenerated from RARE rule arithrefllt

enumerator ARITH_REFL_GEQ
Autogenerated from RARE rule arithreflgeq

enumerator ARITH_REFL_GT
Autogenerated from RARE rule arithreflgt

enumerator ARITH_REAL_EQ_ELIM
Autogenerated from RARE rule arithrealeqelim

enumerator ARITH_INT_EQ_ELIM
Autogenerated from RARE rule arithinteqelim

enumerator ARITH_PLUS_FLATTEN
Autogenerated from RARE rule arithplusflatten

enumerator ARITH_MULT_FLATTEN
Autogenerated from RARE rule arithmultflatten

enumerator ARITH_MULT_DIST
Autogenerated from RARE rule arithmultdist

enumerator ARITH_PLUS_CANCEL1
Autogenerated from RARE rule arithpluscancel1

enumerator ARITH_PLUS_CANCEL2
Autogenerated from RARE rule arithpluscancel2

enumerator ARITH_ABS_ELIM
Autogenerated from RARE rule arithabselim

enumerator ARITH_TO_REAL_ELIM
Autogenerated from RARE rule arithtorealelim

enumerator ARITH_TO_INT_ELIM_TO_REAL
Autogenerated from RARE rule arithtointelimtoreal

enumerator ARITH_DIV_ELIM_TO_REAL1
Autogenerated from RARE rule arithdivelimtoreal1

enumerator ARITH_DIV_ELIM_TO_REAL2
Autogenerated from RARE rule arithdivelimtoreal2

enumerator ARRAY_READ_OVER_WRITE
Autogenerated from RARE rule arrayreadoverwrite

enumerator ARRAY_READ_OVER_WRITE2
Autogenerated from RARE rule arrayreadoverwrite2

enumerator ARRAY_STORE_OVERWRITE
Autogenerated from RARE rule arraystoreoverwrite

enumerator ARRAY_STORE_SELF
Autogenerated from RARE rule arraystoreself

enumerator BOOL_DOUBLE_NOT_ELIM
Autogenerated from RARE rule booldoublenotelim

enumerator BOOL_NOT_TRUE
Autogenerated from RARE rule boolnottrue

enumerator BOOL_NOT_FALSE
Autogenerated from RARE rule boolnotfalse

enumerator BOOL_EQ_TRUE
Autogenerated from RARE rule booleqtrue

enumerator BOOL_EQ_FALSE
Autogenerated from RARE rule booleqfalse

enumerator BOOL_EQ_NREFL
Autogenerated from RARE rule booleqnrefl

enumerator BOOL_IMPL_FALSE1
Autogenerated from RARE rule boolimplfalse1

enumerator BOOL_IMPL_FALSE2
Autogenerated from RARE rule boolimplfalse2

enumerator BOOL_IMPL_TRUE1
Autogenerated from RARE rule boolimpltrue1

enumerator BOOL_IMPL_TRUE2
Autogenerated from RARE rule boolimpltrue2

enumerator BOOL_IMPL_ELIM
Autogenerated from RARE rule boolimplelim

enumerator BOOL_OR_TRUE
Autogenerated from RARE rule boolortrue

enumerator BOOL_OR_FALSE
Autogenerated from RARE rule boolorfalse

enumerator BOOL_OR_FLATTEN
Autogenerated from RARE rule boolorflatten

enumerator BOOL_OR_DUP
Autogenerated from RARE rule boolordup

enumerator BOOL_AND_TRUE
Autogenerated from RARE rule boolandtrue

enumerator BOOL_AND_FALSE
Autogenerated from RARE rule boolandfalse

enumerator BOOL_AND_FLATTEN
Autogenerated from RARE rule boolandflatten

enumerator BOOL_AND_DUP
Autogenerated from RARE rule boolanddup

enumerator BOOL_AND_CONF
Autogenerated from RARE rule boolandconf

enumerator BOOL_OR_TAUT
Autogenerated from RARE rule boolortaut

enumerator BOOL_OR_DE_MORGAN
Autogenerated from RARE rule boolordemorgan

enumerator BOOL_IMPLIES_DE_MORGAN
Autogenerated from RARE rule boolimpliesdemorgan

enumerator BOOL_AND_DE_MORGAN
Autogenerated from RARE rule boolanddemorgan

enumerator BOOL_XOR_REFL
Autogenerated from RARE rule boolxorrefl

enumerator BOOL_XOR_NREFL
Autogenerated from RARE rule boolxornrefl

enumerator BOOL_XOR_FALSE
Autogenerated from RARE rule boolxorfalse

enumerator BOOL_XOR_TRUE
Autogenerated from RARE rule boolxortrue

enumerator BOOL_XOR_COMM
Autogenerated from RARE rule boolxorcomm

enumerator BOOL_XOR_ELIM
Autogenerated from RARE rule boolxorelim

enumerator BOOL_NOT_XOR_ELIM
Autogenerated from RARE rule boolnotxorelim

enumerator BOOL_NOT_EQ_ELIM
Autogenerated from RARE rule boolnoteqelim

enumerator ITE_NEG_BRANCH
Autogenerated from RARE rule itenegbranch

enumerator ITE_THEN_TRUE
Autogenerated from RARE rule itethentrue

enumerator ITE_ELSE_FALSE
Autogenerated from RARE rule iteelsefalse

enumerator ITE_THEN_FALSE
Autogenerated from RARE rule itethenfalse

enumerator ITE_ELSE_TRUE
Autogenerated from RARE rule iteelsetrue

enumerator ITE_THEN_LOOKAHEAD_SELF
Autogenerated from RARE rule itethenlookaheadself

enumerator ITE_ELSE_LOOKAHEAD_SELF
Autogenerated from RARE rule iteelselookaheadself

enumerator BOOL_NOT_ITE_ELIM
Autogenerated from RARE rule boolnotiteelim

enumerator ITE_TRUE_COND
Autogenerated from RARE rule itetruecond

enumerator ITE_FALSE_COND
Autogenerated from RARE rule itefalsecond

enumerator ITE_NOT_COND
Autogenerated from RARE rule itenotcond

enumerator ITE_EQ_BRANCH
Autogenerated from RARE rule iteeqbranch

enumerator ITE_THEN_LOOKAHEAD
Autogenerated from RARE rule itethenlookahead

enumerator ITE_ELSE_LOOKAHEAD
Autogenerated from RARE rule iteelselookahead

enumerator ITE_THEN_NEG_LOOKAHEAD
Autogenerated from RARE rule itethenneglookahead

enumerator ITE_ELSE_NEG_LOOKAHEAD
Autogenerated from RARE rule iteelseneglookahead

enumerator BV_CONCAT_FLATTEN
Autogenerated from RARE rule bvconcatflatten

enumerator BV_CONCAT_EXTRACT_MERGE
Autogenerated from RARE rule bvconcatextractmerge

enumerator BV_EXTRACT_EXTRACT
Autogenerated from RARE rule bvextractextract

enumerator BV_EXTRACT_WHOLE
Autogenerated from RARE rule bvextractwhole

enumerator BV_EXTRACT_CONCAT_1
Autogenerated from RARE rule bvextractconcat1

enumerator BV_EXTRACT_CONCAT_2
Autogenerated from RARE rule bvextractconcat2

enumerator BV_EXTRACT_CONCAT_3
Autogenerated from RARE rule bvextractconcat3

enumerator BV_EXTRACT_CONCAT_4
Autogenerated from RARE rule bvextractconcat4

enumerator BV_EXTRACT_BITWISE_AND
Autogenerated from RARE rule bvextractbitwiseand

enumerator BV_EXTRACT_BITWISE_OR
Autogenerated from RARE rule bvextractbitwiseor

enumerator BV_EXTRACT_BITWISE_XOR
Autogenerated from RARE rule bvextractbitwisexor

enumerator BV_EXTRACT_NOT
Autogenerated from RARE rule bvextractnot

enumerator BV_EXTRACT_SIGN_EXTEND_1
Autogenerated from RARE rule bvextractsignextend1

enumerator BV_EXTRACT_SIGN_EXTEND_2
Autogenerated from RARE rule bvextractsignextend2

enumerator BV_EXTRACT_SIGN_EXTEND_3
Autogenerated from RARE rule bvextractsignextend3

enumerator BV_NEG_MULT
Autogenerated from RARE rule bvnegmult

enumerator BV_NEG_ADD
Autogenerated from RARE rule bvnegadd

enumerator BV_MULT_DISTRIB_CONST_NEG
Autogenerated from RARE rule bvmultdistribconstneg

enumerator BV_MULT_DISTRIB_CONST_ADD
Autogenerated from RARE rule bvmultdistribconstadd

enumerator BV_MULT_DISTRIB_CONST_SUB
Autogenerated from RARE rule bvmultdistribconstsub

enumerator BV_MULT_DISTRIB_1
Autogenerated from RARE rule bvmultdistrib1

enumerator BV_MULT_DISTRIB_2
Autogenerated from RARE rule bvmultdistrib2

enumerator BV_NOT_XOR
Autogenerated from RARE rule bvnotxor

enumerator BV_AND_SIMPLIFY_1
Autogenerated from RARE rule bvandsimplify1

enumerator BV_AND_SIMPLIFY_2
Autogenerated from RARE rule bvandsimplify2

enumerator BV_OR_SIMPLIFY_1
Autogenerated from RARE rule bvorsimplify1

enumerator BV_OR_SIMPLIFY_2
Autogenerated from RARE rule bvorsimplify2

enumerator BV_XOR_SIMPLIFY_1
Autogenerated from RARE rule bvxorsimplify1

enumerator BV_XOR_SIMPLIFY_2
Autogenerated from RARE rule bvxorsimplify2

enumerator BV_XOR_SIMPLIFY_3
Autogenerated from RARE rule bvxorsimplify3

enumerator BV_ULT_ADD_ONE
Autogenerated from RARE rule bvultaddone

enumerator BV_CONCAT_TO_MULT
Autogenerated from RARE rule bvconcattomult

enumerator BV_MULT_SLT_MULT_1
Autogenerated from RARE rule bvmultsltmult1

enumerator BV_MULT_SLT_MULT_2
Autogenerated from RARE rule bvmultsltmult2

enumerator BV_COMMUTATIVE_AND
Autogenerated from RARE rule bvcommutativeand

enumerator BV_COMMUTATIVE_OR
Autogenerated from RARE rule bvcommutativeor

enumerator BV_COMMUTATIVE_XOR
Autogenerated from RARE rule bvcommutativexor

enumerator BV_COMMUTATIVE_MUL
Autogenerated from RARE rule bvcommutativemul

enumerator BV_OR_ZERO
Autogenerated from RARE rule bvorzero

enumerator BV_MUL_ONE
Autogenerated from RARE rule bvmulone

enumerator BV_MUL_ZERO
Autogenerated from RARE rule bvmulzero

enumerator BV_ADD_ZERO
Autogenerated from RARE rule bvaddzero

enumerator BV_ADD_TWO
Autogenerated from RARE rule bvaddtwo

enumerator BV_ZERO_EXTEND_ELIMINATE_0
Autogenerated from RARE rule bvzeroextendeliminate0

enumerator BV_SIGN_EXTEND_ELIMINATE_0
Autogenerated from RARE rule bvsignextendeliminate0

enumerator BV_NOT_NEQ
Autogenerated from RARE rule bvnotneq

enumerator BV_ULT_ONES
Autogenerated from RARE rule bvultones

enumerator BV_OR_FLATTEN
Autogenerated from RARE rule bvorflatten

enumerator BV_XOR_FLATTEN
Autogenerated from RARE rule bvxorflatten

enumerator BV_AND_FLATTEN
Autogenerated from RARE rule bvandflatten

enumerator BV_MUL_FLATTEN
Autogenerated from RARE rule bvmulflatten

enumerator BV_CONCAT_MERGE_CONST
Autogenerated from RARE rule bvconcatmergeconst

enumerator BV_COMMUTATIVE_ADD
Autogenerated from RARE rule bvcommutativeadd

enumerator BV_NEG_SUB
Autogenerated from RARE rule bvnegsub

enumerator BV_NEG_IDEMP
Autogenerated from RARE rule bvnegidemp

enumerator BV_SUB_ELIMINATE
Autogenerated from RARE rule bvsubeliminate

enumerator BV_UGT_ELIMINATE
Autogenerated from RARE rule bvugteliminate

enumerator BV_UGE_ELIMINATE
Autogenerated from RARE rule bvugeeliminate

enumerator BV_SGT_ELIMINATE
Autogenerated from RARE rule bvsgteliminate

enumerator BV_SGE_ELIMINATE
Autogenerated from RARE rule bvsgeeliminate

enumerator BV_SLT_ELIMINATE
Autogenerated from RARE rule bvslteliminate

enumerator BV_SLE_ELIMINATE
Autogenerated from RARE rule bvsleeliminate

enumerator BV_REDOR_ELIMINATE
Autogenerated from RARE rule bvredoreliminate

enumerator BV_REDAND_ELIMINATE
Autogenerated from RARE rule bvredandeliminate

enumerator BV_ULE_ELIMINATE
Autogenerated from RARE rule bvuleeliminate

enumerator BV_COMP_ELIMINATE
Autogenerated from RARE rule bvcompeliminate

enumerator BV_REPEAT_ELIMINATE_1
Autogenerated from RARE rule bvrepeateliminate1

enumerator BV_REPEAT_ELIMINATE_2
Autogenerated from RARE rule bvrepeateliminate2

enumerator BV_ROTATE_LEFT_ELIMINATE_1
Autogenerated from RARE rule bvrotatelefteliminate1

enumerator BV_ROTATE_LEFT_ELIMINATE_2
Autogenerated from RARE rule bvrotatelefteliminate2

enumerator BV_ROTATE_RIGHT_ELIMINATE_1
Autogenerated from RARE rule bvrotaterighteliminate1

enumerator BV_ROTATE_RIGHT_ELIMINATE_2
Autogenerated from RARE rule bvrotaterighteliminate2

enumerator BV_NAND_ELIMINATE
Autogenerated from RARE rule bvnandeliminate

enumerator BV_NOR_ELIMINATE
Autogenerated from RARE rule bvnoreliminate

enumerator BV_XNOR_ELIMINATE
Autogenerated from RARE rule bvxnoreliminate

enumerator BV_SDIV_ELIMINATE
Autogenerated from RARE rule bvsdiveliminate

enumerator BV_SDIV_ELIMINATE_FEWER_BITWISE_OPS
Autogenerated from RARE rule bvsdiveliminatefewerbitwiseops

enumerator BV_ZERO_EXTEND_ELIMINATE
Autogenerated from RARE rule bvzeroextendeliminate

enumerator BV_SIGN_EXTEND_ELIMINATE
Autogenerated from RARE rule bvsignextendeliminate

enumerator BV_UADDO_ELIMINATE
Autogenerated from RARE rule bvuaddoeliminate

enumerator BV_SADDO_ELIMINATE
Autogenerated from RARE rule bvsaddoeliminate

enumerator BV_SDIVO_ELIMINATE
Autogenerated from RARE rule bvsdivoeliminate

enumerator BV_SMOD_ELIMINATE
Autogenerated from RARE rule bvsmodeliminate

enumerator BV_SMOD_ELIMINATE_FEWER_BITWISE_OPS
Autogenerated from RARE rule bvsmodeliminatefewerbitwiseops

enumerator BV_SREM_ELIMINATE
Autogenerated from RARE rule bvsremeliminate

enumerator BV_SREM_ELIMINATE_FEWER_BITWISE_OPS
Autogenerated from RARE rule bvsremeliminatefewerbitwiseops

enumerator BV_USUBO_ELIMINATE
Autogenerated from RARE rule bvusuboeliminate

enumerator BV_SSUBO_ELIMINATE
Autogenerated from RARE rule bvssuboeliminate

enumerator BV_ITE_EQUAL_CHILDREN
Autogenerated from RARE rule bviteequalchildren

enumerator BV_ITE_CONST_CHILDREN_1
Autogenerated from RARE rule bviteconstchildren1

enumerator BV_ITE_CONST_CHILDREN_2
Autogenerated from RARE rule bviteconstchildren2

enumerator BV_ITE_EQUAL_COND_1
Autogenerated from RARE rule bviteequalcond1

enumerator BV_ITE_EQUAL_COND_2
Autogenerated from RARE rule bviteequalcond2

enumerator BV_ITE_EQUAL_COND_3
Autogenerated from RARE rule bviteequalcond3

enumerator BV_ITE_MERGE_THEN_IF
Autogenerated from RARE rule bvitemergethenif

enumerator BV_ITE_MERGE_ELSE_IF
Autogenerated from RARE rule bvitemergeelseif

enumerator BV_ITE_MERGE_THEN_ELSE
Autogenerated from RARE rule bvitemergethenelse

enumerator BV_ITE_MERGE_ELSE_ELSE
Autogenerated from RARE rule bvitemergeelseelse

enumerator BV_SHL_BY_CONST_0
Autogenerated from RARE rule bvshlbyconst0

enumerator BV_SHL_BY_CONST_1
Autogenerated from RARE rule bvshlbyconst1

enumerator BV_SHL_BY_CONST_2
Autogenerated from RARE rule bvshlbyconst2

enumerator BV_LSHR_BY_CONST_0
Autogenerated from RARE rule bvlshrbyconst0

enumerator BV_LSHR_BY_CONST_1
Autogenerated from RARE rule bvlshrbyconst1

enumerator BV_LSHR_BY_CONST_2
Autogenerated from RARE rule bvlshrbyconst2

enumerator BV_ASHR_BY_CONST_0
Autogenerated from RARE rule bvashrbyconst0

enumerator BV_ASHR_BY_CONST_1
Autogenerated from RARE rule bvashrbyconst1

enumerator BV_ASHR_BY_CONST_2
Autogenerated from RARE rule bvashrbyconst2

enumerator BV_AND_CONCAT_PULLUP
Autogenerated from RARE rule bvandconcatpullup

enumerator BV_OR_CONCAT_PULLUP
Autogenerated from RARE rule bvorconcatpullup

enumerator BV_XOR_CONCAT_PULLUP
Autogenerated from RARE rule bvxorconcatpullup

enumerator BV_BITWISE_IDEMP_1
Autogenerated from RARE rule bvbitwiseidemp1

enumerator BV_BITWISE_IDEMP_2
Autogenerated from RARE rule bvbitwiseidemp2

enumerator BV_AND_ZERO
Autogenerated from RARE rule bvandzero

enumerator BV_AND_ONE
Autogenerated from RARE rule bvandone

enumerator BV_OR_ONE
Autogenerated from RARE rule bvorone

enumerator BV_XOR_DUPLICATE
Autogenerated from RARE rule bvxorduplicate

enumerator BV_XOR_ONES
Autogenerated from RARE rule bvxorones

enumerator BV_XOR_ZERO
Autogenerated from RARE rule bvxorzero

enumerator BV_BITWISE_NOT_AND
Autogenerated from RARE rule bvbitwisenotand

enumerator BV_BITWISE_NOT_OR
Autogenerated from RARE rule bvbitwisenotor

enumerator BV_XOR_NOT
Autogenerated from RARE rule bvxornot

enumerator BV_NOT_IDEMP
Autogenerated from RARE rule bvnotidemp

enumerator BV_ULT_ZERO_1
Autogenerated from RARE rule bvultzero1

enumerator BV_ULT_ZERO_2
Autogenerated from RARE rule bvultzero2

enumerator BV_ULT_SELF
Autogenerated from RARE rule bvultself

enumerator BV_LT_SELF
Autogenerated from RARE rule bvltself

enumerator BV_ULE_SELF
Autogenerated from RARE rule bvuleself

enumerator BV_ULE_ZERO
Autogenerated from RARE rule bvulezero

enumerator BV_ZERO_ULE
Autogenerated from RARE rule bvzeroule

enumerator BV_SLE_SELF
Autogenerated from RARE rule bvsleself

enumerator BV_ULE_MAX
Autogenerated from RARE rule bvulemax

enumerator BV_NOT_ULT
Autogenerated from RARE rule bvnotult

enumerator BV_NOT_ULE
Autogenerated from RARE rule bvnotule

enumerator BV_NOT_SLE
Autogenerated from RARE rule bvnotsle

enumerator BV_MULT_POW2_1
Autogenerated from RARE rule bvmultpow21

enumerator BV_MULT_POW2_2
Autogenerated from RARE rule bvmultpow22

enumerator BV_MULT_POW2_2B
Autogenerated from RARE rule bvmultpow22b

enumerator BV_EXTRACT_MULT_LEADING_BIT
Autogenerated from RARE rule bvextractmultleadingbit

enumerator BV_UDIV_POW2_NOT_ONE
Autogenerated from RARE rule bvudivpow2notone

enumerator BV_UDIV_ZERO
Autogenerated from RARE rule bvudivzero

enumerator BV_UDIV_ONE
Autogenerated from RARE rule bvudivone

enumerator BV_UREM_POW2_NOT_ONE
Autogenerated from RARE rule bvurempow2notone

enumerator BV_UREM_ONE
Autogenerated from RARE rule bvuremone

enumerator BV_UREM_SELF
Autogenerated from RARE rule bvuremself

enumerator BV_SHL_ZERO
Autogenerated from RARE rule bvshlzero

enumerator BV_LSHR_ZERO
Autogenerated from RARE rule bvlshrzero

enumerator BV_ASHR_ZERO
Autogenerated from RARE rule bvashrzero

enumerator BV_UGT_UREM
Autogenerated from RARE rule bvugturem

enumerator BV_ULT_ONE
Autogenerated from RARE rule bvultone

enumerator BV_SLT_ZERO
Autogenerated from RARE rule bvsltzero

enumerator BV_MERGE_SIGN_EXTEND_1
Autogenerated from RARE rule bvmergesignextend1

enumerator BV_MERGE_SIGN_EXTEND_2
Autogenerated from RARE rule bvmergesignextend2

enumerator BV_MERGE_SIGN_EXTEND_3
Autogenerated from RARE rule bvmergesignextend3

enumerator BV_SIGN_EXTEND_EQ_CONST_1
Autogenerated from RARE rule bvsignextendeqconst1

enumerator BV_SIGN_EXTEND_EQ_CONST_2
Autogenerated from RARE rule bvsignextendeqconst2

enumerator BV_ZERO_EXTEND_EQ_CONST_1
Autogenerated from RARE rule bvzeroextendeqconst1

enumerator BV_ZERO_EXTEND_EQ_CONST_2
Autogenerated from RARE rule bvzeroextendeqconst2

enumerator BV_ZERO_EXTEND_ULT_CONST_1
Autogenerated from RARE rule bvzeroextendultconst1

enumerator BV_ZERO_EXTEND_ULT_CONST_2
Autogenerated from RARE rule bvzeroextendultconst2

enumerator BV_SIGN_EXTEND_ULT_CONST_1
Autogenerated from RARE rule bvsignextendultconst1

enumerator BV_SIGN_EXTEND_ULT_CONST_2
Autogenerated from RARE rule bvsignextendultconst2

enumerator BV_SIGN_EXTEND_ULT_CONST_3
Autogenerated from RARE rule bvsignextendultconst3

enumerator BV_SIGN_EXTEND_ULT_CONST_4
Autogenerated from RARE rule bvsignextendultconst4

enumerator SETS_EQ_SINGLETON_EMP
Autogenerated from RARE rule setseqsingletonemp

enumerator SETS_MEMBER_SINGLETON
Autogenerated from RARE rule setsmembersingleton

enumerator SETS_MEMBER_EMP
Autogenerated from RARE rule setsmemberemp

enumerator SETS_SUBSET_ELIM
Autogenerated from RARE rule setssubsetelim

enumerator SETS_UNION_COMM
Autogenerated from RARE rule setsunioncomm

enumerator SETS_INTER_COMM
Autogenerated from RARE rule setsintercomm

enumerator SETS_INTER_EMP1
Autogenerated from RARE rule setsinteremp1

enumerator SETS_INTER_EMP2
Autogenerated from RARE rule setsinteremp2

enumerator SETS_MINUS_EMP1
Autogenerated from RARE rule setsminusemp1

enumerator SETS_MINUS_EMP2
Autogenerated from RARE rule setsminusemp2

enumerator SETS_UNION_EMP1
Autogenerated from RARE rule setsunionemp1

enumerator SETS_UNION_EMP2
Autogenerated from RARE rule setsunionemp2

enumerator SETS_INTER_MEMBER
Autogenerated from RARE rule setsintermember

enumerator SETS_MINUS_MEMBER
Autogenerated from RARE rule setsminusmember

enumerator SETS_UNION_MEMBER
Autogenerated from RARE rule setsunionmember

enumerator SETS_CHOOSE_SINGLETON
Autogenerated from RARE rule setschoosesingleton

enumerator SETS_CARD_SINGLETON
Autogenerated from RARE rule setscardsingleton

enumerator SETS_CARD_UNION
Autogenerated from RARE rule setscardunion

enumerator SETS_CARD_MINUS
Autogenerated from RARE rule setscardminus

enumerator SETS_CARD_EMP
Autogenerated from RARE rule setscardemp

enumerator STR_EQ_CTN_FALSE
Autogenerated from RARE rule streqctnfalse

enumerator STR_EQ_CTN_FULL_FALSE1
Autogenerated from RARE rule streqctnfullfalse1

enumerator STR_EQ_CTN_FULL_FALSE2
Autogenerated from RARE rule streqctnfullfalse2

enumerator STR_CONCAT_FLATTEN
Autogenerated from RARE rule strconcatflatten

enumerator STR_CONCAT_FLATTEN_EQ
Autogenerated from RARE rule strconcatflatteneq

enumerator STR_CONCAT_FLATTEN_EQ_REV
Autogenerated from RARE rule strconcatflatteneqrev

enumerator STR_SUBSTR_EMPTY_STR
Autogenerated from RARE rule strsubstremptystr

enumerator STR_SUBSTR_EMPTY_RANGE
Autogenerated from RARE rule strsubstremptyrange

enumerator STR_SUBSTR_EMPTY_START
Autogenerated from RARE rule strsubstremptystart

enumerator STR_SUBSTR_EMPTY_START_NEG
Autogenerated from RARE rule strsubstremptystartneg

enumerator STR_SUBSTR_EQ_EMPTY
Autogenerated from RARE rule strsubstreqempty

enumerator STR_LEN_REPLACE_INV
Autogenerated from RARE rule strlenreplaceinv

enumerator STR_LEN_UPDATE_INV
Autogenerated from RARE rule strlenupdateinv

enumerator STR_LEN_SUBSTR_IN_RANGE
Autogenerated from RARE rule strlensubstrinrange

enumerator STR_LEN_SUBSTR_UB1
Autogenerated from RARE rule strlensubstrub1

enumerator STR_LEN_SUBSTR_UB2
Autogenerated from RARE rule strlensubstrub2

enumerator STR_CONCAT_CLASH
Autogenerated from RARE rule strconcatclash

enumerator STR_CONCAT_CLASH_REV
Autogenerated from RARE rule strconcatclashrev

enumerator STR_CONCAT_CLASH2
Autogenerated from RARE rule strconcatclash2

enumerator STR_CONCAT_CLASH2_REV
Autogenerated from RARE rule strconcatclash2rev

enumerator STR_CONCAT_UNIFY
Autogenerated from RARE rule strconcatunify

enumerator STR_CONCAT_UNIFY_REV
Autogenerated from RARE rule strconcatunifyrev

enumerator STR_CONCAT_UNIFY_BASE
Autogenerated from RARE rule strconcatunifybase

enumerator STR_CONCAT_UNIFY_BASE_REV
Autogenerated from RARE rule strconcatunifybaserev

enumerator STR_CONCAT_CLASH_CHAR
Autogenerated from RARE rule strconcatclashchar

enumerator STR_CONCAT_CLASH_CHAR_REV
Autogenerated from RARE rule strconcatclashcharrev

enumerator STR_PREFIXOF_ELIM
Autogenerated from RARE rule strprefixofelim

enumerator STR_SUFFIXOF_ELIM
Autogenerated from RARE rule strsuffixofelim

enumerator STR_PREFIXOF_ONE
Autogenerated from RARE rule strprefixofone

enumerator STR_SUFFIXOF_ONE
Autogenerated from RARE rule strsuffixofone

enumerator STR_SUBSTR_COMBINE1
Autogenerated from RARE rule strsubstrcombine1

enumerator STR_SUBSTR_COMBINE2
Autogenerated from RARE rule strsubstrcombine2

enumerator STR_SUBSTR_COMBINE3
Autogenerated from RARE rule strsubstrcombine3

enumerator STR_SUBSTR_COMBINE4
Autogenerated from RARE rule strsubstrcombine4

enumerator STR_SUBSTR_CONCAT1
Autogenerated from RARE rule strsubstrconcat1

enumerator STR_SUBSTR_CONCAT2
Autogenerated from RARE rule strsubstrconcat2

enumerator STR_SUBSTR_FULL
Autogenerated from RARE rule strsubstrfull

enumerator STR_SUBSTR_FULL_EQ
Autogenerated from RARE rule strsubstrfulleq

enumerator STR_CONTAINS_REFL
Autogenerated from RARE rule strcontainsrefl

enumerator STR_CONTAINS_CONCAT_FIND
Autogenerated from RARE rule strcontainsconcatfind

enumerator STR_CONTAINS_SPLIT_CHAR
Autogenerated from RARE rule strcontainssplitchar

enumerator STR_CONTAINS_LT_LEN
Autogenerated from RARE rule strcontainsltlen

enumerator STR_CONTAINS_LEQ_LEN_EQ
Autogenerated from RARE rule strcontainsleqleneq

enumerator STR_CONTAINS_EMP
Autogenerated from RARE rule strcontainsemp

enumerator STR_CONTAINS_IS_EMP
Autogenerated from RARE rule strcontainsisemp

enumerator STR_CONCAT_EMP
Autogenerated from RARE rule strconcatemp

enumerator STR_AT_ELIM
Autogenerated from RARE rule stratelim

enumerator STR_REPLACE_SELF
Autogenerated from RARE rule strreplaceself

enumerator STR_REPLACE_NO_CONTAINS
Autogenerated from RARE rule strreplacenocontains

enumerator STR_REPLACE_EMPTY
Autogenerated from RARE rule strreplaceempty

enumerator STR_LEN_CONCAT_REC
Autogenerated from RARE rule strlenconcatrec

enumerator STR_INDEXOF_SELF
Autogenerated from RARE rule strindexofself

enumerator STR_INDEXOF_NO_CONTAINS
Autogenerated from RARE rule strindexofnocontains

enumerator STR_TO_LOWER_CONCAT
Autogenerated from RARE rule strtolowerconcat

enumerator STR_TO_UPPER_CONCAT
Autogenerated from RARE rule strtoupperconcat

enumerator STR_TO_LOWER_UPPER
Autogenerated from RARE rule strtolowerupper

enumerator STR_TO_UPPER_LOWER
Autogenerated from RARE rule strtoupperlower

enumerator RE_ALL_ELIM
Autogenerated from RARE rule reallelim

enumerator RE_OPT_ELIM
Autogenerated from RARE rule reoptelim

enumerator RE_DIFF_ELIM
Autogenerated from RARE rule rediffelim

enumerator RE_CONCAT_EMP
Autogenerated from RARE rule reconcatemp

enumerator RE_CONCAT_NONE
Autogenerated from RARE rule reconcatnone

enumerator RE_CONCAT_FLATTEN
Autogenerated from RARE rule reconcatflatten

enumerator RE_CONCAT_STAR_SWAP
Autogenerated from RARE rule reconcatstarswap

enumerator RE_CONCAT_MERGE
Autogenerated from RARE rule reconcatmerge

enumerator RE_UNION_ALL
Autogenerated from RARE rule reunionall

enumerator RE_UNION_NONE
Autogenerated from RARE rule reunionnone

enumerator RE_UNION_FLATTEN
Autogenerated from RARE rule reunionflatten

enumerator RE_UNION_DUP
Autogenerated from RARE rule reuniondup

enumerator RE_INTER_ALL
Autogenerated from RARE rule reinterall

enumerator RE_INTER_NONE
Autogenerated from RARE rule reinternone

enumerator RE_INTER_FLATTEN
Autogenerated from RARE rule reinterflatten

enumerator RE_INTER_DUP
Autogenerated from RARE rule reinterdup

enumerator RE_LOOP_NEG
Autogenerated from RARE rule reloopneg

enumerator RE_INTER_CSTRING
Autogenerated from RARE rule reintercstring

enumerator RE_INTER_CSTRING_NEG
Autogenerated from RARE rule reintercstringneg

enumerator STR_NTH_ELIM_CODE
Autogenerated from RARE rule strnthelimcode

enumerator STR_SUBSTR_LEN_INCLUDE
Autogenerated from RARE rule strsubstrleninclude

enumerator STR_SUBSTR_LEN_INCLUDE_PRE
Autogenerated from RARE rule strsubstrlenincludepre

enumerator STR_SUBSTR_LEN_SKIP
Autogenerated from RARE rule strsubstrlenskip

enumerator SEQ_REV_CONCAT
Autogenerated from RARE rule seqrevconcat

enumerator SEQ_LEN_UNIT
Autogenerated from RARE rule seqlenunit

enumerator SEQ_NTH_UNIT
Autogenerated from RARE rule seqnthunit

enumerator SEQ_REV_UNIT
Autogenerated from RARE rule seqrevunit

enumerator RE_IN_EMPTY
Autogenerated from RARE rule reinempty

enumerator RE_IN_SIGMA
Autogenerated from RARE rule reinsigma

enumerator RE_IN_SIGMA_STAR
Autogenerated from RARE rule reinsigmastar

enumerator RE_IN_CSTRING
Autogenerated from RARE rule reincstring

enumerator RE_IN_COMP
Autogenerated from RARE rule reincomp

enumerator STR_IN_RE_UNION_ELIM
Autogenerated from RARE rule strinreunionelim

enumerator STR_IN_RE_INTER_ELIM
Autogenerated from RARE rule strinreinterelim

enumerator STR_IN_RE_RANGE_ELIM
Autogenerated from RARE rule strinrerangeelim

enumerator STR_IN_RE_CONTAINS
Autogenerated from RARE rule strinrecontains

enumerator STR_IN_RE_STRIP_PREFIX
Autogenerated from RARE rule strinrestripprefix

enumerator STR_IN_RE_STRIP_PREFIX_NEG
Autogenerated from RARE rule strinrestripprefixneg

enumerator STR_IN_RE_STRIP_PREFIX_SR_SINGLE
Autogenerated from RARE rule strinrestripprefixsrsingle

enumerator STR_IN_RE_STRIP_PREFIX_SR_SINGLE_NEG
Autogenerated from RARE rule strinrestripprefixsrsingleneg

enumerator STR_IN_RE_STRIP_PREFIX_SRS_SINGLE
Autogenerated from RARE rule strinrestripprefixsrssingle

enumerator STR_IN_RE_STRIP_PREFIX_SRS_SINGLE_NEG
Autogenerated from RARE rule strinrestripprefixsrssingleneg

enumerator STR_IN_RE_STRIP_PREFIX_S_SINGLE
Autogenerated from RARE rule strinrestripprefixssingle

enumerator STR_IN_RE_STRIP_PREFIX_S_SINGLE_NEG
Autogenerated from RARE rule strinrestripprefixssingleneg

enumerator STR_IN_RE_STRIP_PREFIX_BASE
Autogenerated from RARE rule strinrestripprefixbase

enumerator STR_IN_RE_STRIP_PREFIX_BASE_NEG
Autogenerated from RARE rule strinrestripprefixbaseneg

enumerator STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE
Autogenerated from RARE rule strinrestripprefixbasessingle

enumerator STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE_NEG
Autogenerated from RARE rule strinrestripprefixbasessingleneg

enumerator STR_IN_RE_STRIP_CHAR
Autogenerated from RARE rule strinrestripchar

enumerator STR_IN_RE_STRIP_CHAR_S_SINGLE
Autogenerated from RARE rule strinrestripcharssingle

enumerator STR_IN_RE_STRIP_PREFIX_REV
Autogenerated from RARE rule strinrestripprefixrev

enumerator STR_IN_RE_STRIP_PREFIX_NEG_REV
Autogenerated from RARE rule strinrestripprefixnegrev

enumerator STR_IN_RE_STRIP_PREFIX_SR_SINGLE_REV
Autogenerated from RARE rule strinrestripprefixsrsinglerev

enumerator STR_IN_RE_STRIP_PREFIX_SR_SINGLE_NEG_REV
Autogenerated from RARE rule strinrestripprefixsrsinglenegrev

enumerator STR_IN_RE_STRIP_PREFIX_SRS_SINGLE_REV
Autogenerated from RARE rule strinrestripprefixsrssinglerev

enumerator STR_IN_RE_STRIP_PREFIX_SRS_SINGLE_NEG_REV
Autogenerated from RARE rule strinrestripprefixsrssinglenegrev

enumerator STR_IN_RE_STRIP_PREFIX_S_SINGLE_REV
Autogenerated from RARE rule strinrestripprefixssinglerev

enumerator STR_IN_RE_STRIP_PREFIX_S_SINGLE_NEG_REV
Autogenerated from RARE rule strinrestripprefixssinglenegrev

enumerator STR_IN_RE_STRIP_PREFIX_BASE_REV
Autogenerated from RARE rule strinrestripprefixbaserev

enumerator STR_IN_RE_STRIP_PREFIX_BASE_NEG_REV
Autogenerated from RARE rule strinrestripprefixbasenegrev

enumerator STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE_REV
Autogenerated from RARE rule strinrestripprefixbasessinglerev

enumerator STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE_NEG_REV
Autogenerated from RARE rule strinrestripprefixbasessinglenegrev

enumerator STR_IN_RE_STRIP_CHAR_REV
Autogenerated from RARE rule strinrestripcharrev

enumerator STR_IN_RE_STRIP_CHAR_S_SINGLE_REV
Autogenerated from RARE rule strinrestripcharssinglerev

enumerator STR_IN_RE_NO_PREFIX
Autogenerated from RARE rule strinrenoprefix

enumerator STR_IN_RE_NO_PREFIX_REV
Autogenerated from RARE rule strinrenoprefixrev

enumerator STR_IN_RE_REQ_UNFOLD
Autogenerated from RARE rule strinrerequnfold

enumerator STR_IN_RE_REQ_UNFOLD_REV
Autogenerated from RARE rule strinrerequnfoldrev

enumerator STR_IN_RE_SKIP_UNFOLD
Autogenerated from RARE rule strinreskipunfold

enumerator STR_IN_RE_SKIP_UNFOLD_REV
Autogenerated from RARE rule strinreskipunfoldrev

enumerator STR_IN_RE_TEST_UNFOLD
Autogenerated from RARE rule strinretestunfold

enumerator STR_IN_RE_TEST_UNFOLD_REV
Autogenerated from RARE rule strinretestunfoldrev

enumerator EQ_REFL
Autogenerated from RARE rule eqrefl

enumerator EQ_SYMM
Autogenerated from RARE rule eqsymm

enumerator DISTINCT_BINARY_ELIM
Autogenerated from RARE rule distinctbinaryelim

enumerator UF_BV2NAT_GEQ_ELIM
Autogenerated from RARE rule ufbv2natgeqelim

enumerator NONE

std::ostream &cvc5::operator<<(std::ostream &out, ProofRewriteRule rule)
Writes a proof rewrite rule name to a stream.
 Parameters:
out – The stream to write to
rule – The proof rewrite rule to write to the stream
 Returns:
The stream

std::string std::to_string(cvc5::ProofRewriteRule rule)
Converts a proof rewrite rule to a string.
 Parameters:
rule – The proof rewrite rule
 Returns:
The name of the proof rewrite rule

template<>
struct hash<cvc5::ProofRewriteRule> Hash function for ProofRewriteRules.
Public Functions

size_t operator()(cvc5::ProofRewriteRule rule) const
Hashes a ProofRewriteRule to a size_t.
 Parameters:
rule – The proof rewrite rule.
 Returns:
The hash value.

size_t operator()(cvc5::ProofRewriteRule rule) const