#[repr(u32)]pub enum ProofRule {
Show 158 variants
Assume = 0,
Scope = 1,
Subs = 2,
MacroRewrite = 3,
Evaluate = 4,
DistinctValues = 5,
AciNorm = 6,
Absorb = 7,
MacroSrEqIntro = 8,
MacroSrPredIntro = 9,
MacroSrPredElim = 10,
MacroSrPredTransform = 11,
EncodeEqIntro = 12,
DslRewrite = 13,
TheoryRewrite = 14,
IteEq = 15,
Trust = 16,
TrustTheoryRewrite = 17,
SatRefutation = 18,
DratRefutation = 19,
SatExternalProve = 20,
Resolution = 21,
ChainResolution = 22,
Factoring = 23,
Reordering = 24,
MacroResolution = 25,
MacroResolutionTrust = 26,
ChainMResolution = 27,
Split = 28,
EqResolve = 29,
ModusPonens = 30,
NotNotElim = 31,
Contra = 32,
AndElim = 33,
AndIntro = 34,
NotOrElim = 35,
ImpliesElim = 36,
NotImpliesElim1 = 37,
NotImpliesElim2 = 38,
EquivElim1 = 39,
EquivElim2 = 40,
NotEquivElim1 = 41,
NotEquivElim2 = 42,
XorElim1 = 43,
XorElim2 = 44,
NotXorElim1 = 45,
NotXorElim2 = 46,
IteElim1 = 47,
IteElim2 = 48,
NotIteElim1 = 49,
NotIteElim2 = 50,
NotAnd = 51,
CnfAndPos = 52,
CnfAndNeg = 53,
CnfOrPos = 54,
CnfOrNeg = 55,
CnfImpliesPos = 56,
CnfImpliesNeg1 = 57,
CnfImpliesNeg2 = 58,
CnfEquivPos1 = 59,
CnfEquivPos2 = 60,
CnfEquivNeg1 = 61,
CnfEquivNeg2 = 62,
CnfXorPos1 = 63,
CnfXorPos2 = 64,
CnfXorNeg1 = 65,
CnfXorNeg2 = 66,
CnfItePos1 = 67,
CnfItePos2 = 68,
CnfItePos3 = 69,
CnfIteNeg1 = 70,
CnfIteNeg2 = 71,
CnfIteNeg3 = 72,
Refl = 73,
Symm = 74,
Trans = 75,
Cong = 76,
NaryCong = 77,
TrueIntro = 78,
TrueElim = 79,
FalseIntro = 80,
FalseElim = 81,
HoAppEncode = 82,
HoCong = 83,
ArraysReadOverWrite = 84,
ArraysReadOverWriteContra = 85,
ArraysReadOverWrite1 = 86,
ArraysExt = 87,
MacroBvBitblast = 88,
BvBitblastStep = 89,
BvEagerAtom = 90,
BvPolyNorm = 91,
BvPolyNormEq = 92,
DtSplit = 93,
SkolemIntro = 94,
Skolemize = 95,
Instantiate = 96,
AlphaEquiv = 97,
QuantVarReordering = 98,
ExistsStringLength = 99,
SetsSingletonInj = 100,
SetsExt = 101,
SetsFilterUp = 102,
SetsFilterDown = 103,
ConcatEq = 104,
ConcatUnify = 105,
ConcatSplit = 106,
ConcatCsplit = 107,
ConcatLprop = 108,
ConcatCprop = 109,
StringDecompose = 110,
StringLengthPos = 111,
StringLengthNonEmpty = 112,
StringReduction = 113,
StringEagerReduction = 114,
ReInter = 115,
ReConcat = 116,
ReUnfoldPos = 117,
ReUnfoldNeg = 118,
ReUnfoldNegConcatFixed = 119,
StringCodeInj = 120,
StringSeqUnitInj = 121,
StringExt = 122,
MacroStringInference = 123,
MacroArithScaleSumUb = 124,
ArithMultAbsComparison = 125,
ArithSumUb = 126,
IntTightUb = 127,
IntTightLb = 128,
ArithTrichotomy = 129,
ArithReduction = 130,
ArithPolyNorm = 131,
ArithPolyNormRel = 132,
ArithMultSign = 133,
ArithMultPos = 134,
ArithMultNeg = 135,
ArithMultTangent = 136,
ArithTransPi = 137,
ArithTransExpNeg = 138,
ArithTransExpPositivity = 139,
ArithTransExpSuperLin = 140,
ArithTransExpZero = 141,
ArithTransExpApproxAboveNeg = 142,
ArithTransExpApproxAbovePos = 143,
ArithTransExpApproxBelow = 144,
ArithTransSineBounds = 145,
ArithTransSineShift = 146,
ArithTransSineSymmetry = 147,
ArithTransSineTangentZero = 148,
ArithTransSineTangentPi = 149,
ArithTransSineApproxAboveNeg = 150,
ArithTransSineApproxAbovePos = 151,
ArithTransSineApproxBelowNeg = 152,
ArithTransSineApproxBelowPos = 153,
LfscRule = 154,
AletheRule = 155,
Unknown = 156,
Last = 157,
}Expand description
\internal This documentation is target for the online documentation that can be found at https://cvc5.github.io/docs/latest/proofs/proof_rules.html \endinternal
\verbatim embed:rst:leading-asterisk 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:
.. math::
\texttt{RULENAME}: \inferruleSC{\varphi_1 \dots \varphi_n \mid t_1 \dots t_m}{\psi}{if $C$}
where we call :math:\varphi_i its premises or children, :math:t_i its
arguments, :math:\psi its conclusion, and :math: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) :cpp:enumerator:ASSUME <cvc5::ProofRule::ASSUME>, which represents an
open leaf in a proof; and
(2) :cpp:enumerator:SCOPE <cvc5::ProofRule::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.
\endverbatim