Enum ProofRewriteRule

Source

#[repr(u32)]pub enum ProofRewriteRule {
Show 521 variants    None = 0,
    DistinctElim = 1,
    DistinctCardConflict = 2,
    UbvToIntElim = 3,
    IntToBvElim = 4,
    MacroBoolNnfNorm = 5,
    MacroBoolBvInvertSolve = 6,
    MacroArithIntEqConflict = 7,
    MacroArithIntGeqTighten = 8,
    MacroArithStringPredEntail = 9,
    ArithStringPredEntail = 10,
    ArithStringPredSafeApprox = 11,
    ArithPowElim = 12,
    BetaReduce = 13,
    LambdaElim = 14,
    MacroLambdaCaptureAvoid = 15,
    ArraysSelectConst = 16,
    MacroArraysNormalizeOp = 17,
    MacroArraysNormalizeConstant = 18,
    ArraysEqRangeExpand = 19,
    ExistsElim = 20,
    QuantUnusedVars = 21,
    MacroQuantMergePrenex = 22,
    QuantMergePrenex = 23,
    MacroQuantPrenex = 24,
    MacroQuantMiniscope = 25,
    QuantMiniscopeAnd = 26,
    QuantMiniscopeOr = 27,
    QuantMiniscopeIte = 28,
    QuantDtSplit = 29,
    MacroQuantDtVarExpand = 30,
    MacroQuantPartitionConnectedFv = 31,
    MacroQuantVarElimEq = 32,
    QuantVarElimEq = 33,
    MacroQuantVarElimIneq = 34,
    MacroQuantRewriteBody = 35,
    DtInst = 36,
    DtCollapseSelector = 37,
    DtCollapseTester = 38,
    DtCollapseTesterSingleton = 39,
    MacroDtConsEq = 40,
    DtConsEq = 41,
    DtConsEqClash = 42,
    DtCycle = 43,
    DtCollapseUpdater = 44,
    DtUpdaterElim = 45,
    DtMatchElim = 46,
    MacroBvExtractConcat = 47,
    MacroBvOrSimplify = 48,
    MacroBvAndSimplify = 49,
    MacroBvXorSimplify = 50,
    MacroBvAndOrXorConcatPullup = 51,
    MacroBvMultSltMult = 52,
    MacroBvConcatExtractMerge = 53,
    MacroBvConcatConstantMerge = 54,
    MacroBvEqSolve = 55,
    BvUmuloElim = 56,
    BvSmuloElim = 57,
    BvBitwiseSlicing = 58,
    BvRepeatElim = 59,
    StrCtnMultisetSubset = 60,
    MacroStrEqLenUnifyPrefix = 61,
    MacroStrEqLenUnify = 62,
    MacroStrSplitCtn = 63,
    MacroStrStripEndpoints = 64,
    StrOverlapSplitCtn = 65,
    StrOverlapEndpointsCtn = 66,
    StrOverlapEndpointsIndexof = 67,
    StrOverlapEndpointsReplace = 68,
    MacroStrComponentCtn = 69,
    MacroStrConstNctnConcat = 70,
    MacroStrInReInclusion = 71,
    MacroReInterUnionConstElim = 72,
    SeqEvalOp = 73,
    StrIndexofReEval = 74,
    StrReplaceReEval = 75,
    StrReplaceReAllEval = 76,
    ReLoopElim = 77,
    ReEqElim = 78,
    MacroReInterUnionInclusion = 79,
    ReInterInclusion = 80,
    ReUnionInclusion = 81,
    StrInReEval = 82,
    StrInReConsume = 83,
    StrInReConcatStarChar = 84,
    StrInReSigma = 85,
    StrInReSigmaStar = 86,
    MacroSubstrStripSymLength = 87,
    SetsEvalOp = 88,
    SetsInsertElim = 89,
    ArithDivTotalZeroReal = 90,
    ArithDivTotalZeroInt = 91,
    ArithIntDivTotal = 92,
    ArithIntDivTotalOne = 93,
    ArithIntDivTotalZero = 94,
    ArithIntDivTotalNeg = 95,
    ArithIntModTotal = 96,
    ArithIntModTotalOne = 97,
    ArithIntModTotalZero = 98,
    ArithIntModTotalNeg = 99,
    ArithElimGt = 100,
    ArithElimLt = 101,
    ArithElimIntGt = 102,
    ArithElimIntLt = 103,
    ArithElimLeq = 104,
    ArithLeqNorm = 105,
    ArithGeqTighten = 106,
    ArithGeqNorm1Int = 107,
    ArithGeqNorm1Real = 108,
    ArithEqElimReal = 109,
    ArithEqElimInt = 110,
    ArithToIntElim = 111,
    ArithToIntElimToReal = 112,
    ArithDivElimToReal1 = 113,
    ArithDivElimToReal2 = 114,
    ArithModOverMod = 115,
    ArithIntEqConflict = 116,
    ArithIntGeqTighten = 117,
    ArithDivisibleElim = 118,
    ArithAbsEq = 119,
    ArithAbsIntGt = 120,
    ArithAbsRealGt = 121,
    ArithGeqIteLift = 122,
    ArithLeqIteLift = 123,
    ArithMinLt1 = 124,
    ArithMinLt2 = 125,
    ArithMaxGeq1 = 126,
    ArithMaxGeq2 = 127,
    ArrayReadOverWrite = 128,
    ArrayReadOverWrite2 = 129,
    ArrayStoreOverwrite = 130,
    ArrayStoreSelf = 131,
    ArrayReadOverWriteSplit = 132,
    ArrayStoreSwap = 133,
    BoolDoubleNotElim = 134,
    BoolNotTrue = 135,
    BoolNotFalse = 136,
    BoolEqTrue = 137,
    BoolEqFalse = 138,
    BoolEqNrefl = 139,
    BoolImplFalse1 = 140,
    BoolImplFalse2 = 141,
    BoolImplTrue1 = 142,
    BoolImplTrue2 = 143,
    BoolImplElim = 144,
    BoolDualImplEq = 145,
    BoolAndConf = 146,
    BoolAndConf2 = 147,
    BoolOrTaut = 148,
    BoolOrTaut2 = 149,
    BoolOrDeMorgan = 150,
    BoolImpliesDeMorgan = 151,
    BoolAndDeMorgan = 152,
    BoolOrAndDistrib = 153,
    BoolImpliesOrDistrib = 154,
    BoolXorRefl = 155,
    BoolXorNrefl = 156,
    BoolXorFalse = 157,
    BoolXorTrue = 158,
    BoolXorComm = 159,
    BoolXorElim = 160,
    BoolNotXorElim = 161,
    BoolNotEqElim1 = 162,
    BoolNotEqElim2 = 163,
    IteNegBranch = 164,
    IteThenTrue = 165,
    IteElseFalse = 166,
    IteThenFalse = 167,
    IteElseTrue = 168,
    IteThenLookaheadSelf = 169,
    IteElseLookaheadSelf = 170,
    IteThenLookaheadNotSelf = 171,
    IteElseLookaheadNotSelf = 172,
    IteExpand = 173,
    BoolNotIteElim = 174,
    IteTrueCond = 175,
    IteFalseCond = 176,
    IteNotCond = 177,
    IteEqBranch = 178,
    IteThenLookahead = 179,
    IteElseLookahead = 180,
    IteThenNegLookahead = 181,
    IteElseNegLookahead = 182,
    BvConcatExtractMerge = 183,
    BvExtractExtract = 184,
    BvExtractWhole = 185,
    BvExtractConcat1 = 186,
    BvExtractConcat2 = 187,
    BvExtractConcat3 = 188,
    BvExtractConcat4 = 189,
    BvEqExtractElim1 = 190,
    BvEqExtractElim2 = 191,
    BvEqExtractElim3 = 192,
    BvExtractNot = 193,
    BvExtractSignExtend1 = 194,
    BvExtractSignExtend2 = 195,
    BvExtractSignExtend3 = 196,
    BvNotXor = 197,
    BvAndSimplify1 = 198,
    BvAndSimplify2 = 199,
    BvOrSimplify1 = 200,
    BvOrSimplify2 = 201,
    BvXorSimplify1 = 202,
    BvXorSimplify2 = 203,
    BvXorSimplify3 = 204,
    BvUltAddOne = 205,
    BvMultSltMult1 = 206,
    BvMultSltMult2 = 207,
    BvCommutativeXor = 208,
    BvCommutativeComp = 209,
    BvZeroExtendEliminate0 = 210,
    BvSignExtendEliminate0 = 211,
    BvNotNeq = 212,
    BvUltOnes = 213,
    BvConcatMergeConst = 214,
    BvCommutativeAdd = 215,
    BvSubEliminate = 216,
    BvIteWidthOne = 217,
    BvIteWidthOneNot = 218,
    BvEqXorSolve = 219,
    BvEqNotSolve = 220,
    BvUgtEliminate = 221,
    BvUgeEliminate = 222,
    BvSgtEliminate = 223,
    BvSgeEliminate = 224,
    BvSleEliminate = 225,
    BvRedorEliminate = 226,
    BvRedandEliminate = 227,
    BvUleEliminate = 228,
    BvCompEliminate = 229,
    BvRotateLeftEliminate1 = 230,
    BvRotateLeftEliminate2 = 231,
    BvRotateRightEliminate1 = 232,
    BvRotateRightEliminate2 = 233,
    BvNandEliminate = 234,
    BvNorEliminate = 235,
    BvXnorEliminate = 236,
    BvSdivEliminate = 237,
    BvZeroExtendEliminate = 238,
    BvUaddoEliminate = 239,
    BvSaddoEliminate = 240,
    BvSdivoEliminate = 241,
    BvSmodEliminate = 242,
    BvSremEliminate = 243,
    BvUsuboEliminate = 244,
    BvSsuboEliminate = 245,
    BvNegoEliminate = 246,
    BvIteEqualChildren = 247,
    BvIteConstChildren1 = 248,
    BvIteConstChildren2 = 249,
    BvIteEqualCond1 = 250,
    BvIteEqualCond2 = 251,
    BvIteEqualCond3 = 252,
    BvIteMergeThenIf = 253,
    BvIteMergeElseIf = 254,
    BvIteMergeThenElse = 255,
    BvIteMergeElseElse = 256,
    BvShlByConst0 = 257,
    BvShlByConst1 = 258,
    BvShlByConst2 = 259,
    BvLshrByConst0 = 260,
    BvLshrByConst1 = 261,
    BvLshrByConst2 = 262,
    BvAshrByConst0 = 263,
    BvAshrByConst1 = 264,
    BvAshrByConst2 = 265,
    BvAndConcatPullup = 266,
    BvOrConcatPullup = 267,
    BvXorConcatPullup = 268,
    BvAndConcatPullup2 = 269,
    BvOrConcatPullup2 = 270,
    BvXorConcatPullup2 = 271,
    BvAndConcatPullup3 = 272,
    BvOrConcatPullup3 = 273,
    BvXorConcatPullup3 = 274,
    BvXorDuplicate = 275,
    BvXorOnes = 276,
    BvXorNot = 277,
    BvNotIdemp = 278,
    BvUltZero1 = 279,
    BvUltZero2 = 280,
    BvUltSelf = 281,
    BvLtSelf = 282,
    BvUleSelf = 283,
    BvUleZero = 284,
    BvZeroUle = 285,
    BvSleSelf = 286,
    BvUleMax = 287,
    BvNotUlt = 288,
    BvMultPow21 = 289,
    BvMultPow22 = 290,
    BvMultPow22b = 291,
    BvExtractMultLeadingBit = 292,
    BvUdivPow2NotOne = 293,
    BvUdivZero = 294,
    BvUdivOne = 295,
    BvUremPow2NotOne = 296,
    BvUremOne = 297,
    BvUremSelf = 298,
    BvShlZero = 299,
    BvLshrZero = 300,
    BvAshrZero = 301,
    BvUgtUrem = 302,
    BvUltOne = 303,
    BvMergeSignExtend1 = 304,
    BvMergeSignExtend2 = 305,
    BvSignExtendEqConst1 = 306,
    BvSignExtendEqConst2 = 307,
    BvZeroExtendEqConst1 = 308,
    BvZeroExtendEqConst2 = 309,
    BvZeroExtendUltConst1 = 310,
    BvZeroExtendUltConst2 = 311,
    BvSignExtendUltConst1 = 312,
    BvSignExtendUltConst2 = 313,
    BvSignExtendUltConst3 = 314,
    BvSignExtendUltConst4 = 315,
    SetsEqSingletonEmp = 316,
    SetsMemberSingleton = 317,
    SetsMemberEmp = 318,
    SetsSubsetElim = 319,
    SetsUnionComm = 320,
    SetsInterComm = 321,
    SetsInterEmp1 = 322,
    SetsInterEmp2 = 323,
    SetsMinusEmp1 = 324,
    SetsMinusEmp2 = 325,
    SetsUnionEmp1 = 326,
    SetsUnionEmp2 = 327,
    SetsInterMember = 328,
    SetsMinusMember = 329,
    SetsUnionMember = 330,
    SetsChooseSingleton = 331,
    SetsMinusSelf = 332,
    SetsIsEmptyElim = 333,
    SetsIsSingletonElim = 334,
    StrEqCtnFalse = 335,
    StrEqCtnFullFalse1 = 336,
    StrEqCtnFullFalse2 = 337,
    StrEqLenFalse = 338,
    StrSubstrEmptyStr = 339,
    StrSubstrEmptyRange = 340,
    StrSubstrEmptyStart = 341,
    StrSubstrEmptyStartNeg = 342,
    StrSubstrSubstrStartGeqLen = 343,
    StrSubstrEqEmpty = 344,
    StrSubstrZEqEmptyLeq = 345,
    StrSubstrEqEmptyLeqLen = 346,
    StrLenReplaceInv = 347,
    StrLenReplaceAllInv = 348,
    StrLenUpdateInv = 349,
    StrUpdateInFirstConcat = 350,
    StrLenSubstrInRange = 351,
    StrConcatClash = 352,
    StrConcatClashRev = 353,
    StrConcatClash2 = 354,
    StrConcatClash2Rev = 355,
    StrConcatUnify = 356,
    StrConcatUnifyRev = 357,
    StrConcatUnifyBase = 358,
    StrConcatUnifyBaseRev = 359,
    StrPrefixofElim = 360,
    StrSuffixofElim = 361,
    StrPrefixofEq = 362,
    StrSuffixofEq = 363,
    StrPrefixofOne = 364,
    StrSuffixofOne = 365,
    StrSubstrCombine1 = 366,
    StrSubstrCombine2 = 367,
    StrSubstrCombine3 = 368,
    StrSubstrCombine4 = 369,
    StrSubstrConcat1 = 370,
    StrSubstrConcat2 = 371,
    StrSubstrReplace = 372,
    StrSubstrFull = 373,
    StrSubstrFullEq = 374,
    StrContainsRefl = 375,
    StrContainsConcatFind = 376,
    StrContainsConcatFindContra = 377,
    StrContainsSplitChar = 378,
    StrContainsLeqLenEq = 379,
    StrContainsEmp = 380,
    StrContainsChar = 381,
    StrAtElim = 382,
    StrReplaceSelf = 383,
    StrReplaceId = 384,
    StrReplacePrefix = 385,
    StrReplaceNoContains = 386,
    StrReplaceFindBase = 387,
    StrReplaceFindFirstConcat = 388,
    StrReplaceEmpty = 389,
    StrReplaceOnePre = 390,
    StrReplaceFindPre = 391,
    StrReplaceAllNoContains = 392,
    StrReplaceReNone = 393,
    StrReplaceReAllNone = 394,
    StrLenConcatRec = 395,
    StrLenEqZeroConcatRec = 396,
    StrLenEqZeroBase = 397,
    StrIndexofSelf = 398,
    StrIndexofNoContains = 399,
    StrIndexofOob = 400,
    StrIndexofOob2 = 401,
    StrIndexofContainsPre = 402,
    StrIndexofFindEmp = 403,
    StrIndexofEqIrr = 404,
    StrIndexofReNone = 405,
    StrIndexofReEmpRe = 406,
    StrToLowerConcat = 407,
    StrToUpperConcat = 408,
    StrToLowerUpper = 409,
    StrToUpperLower = 410,
    StrToLowerLen = 411,
    StrToUpperLen = 412,
    StrToLowerFromInt = 413,
    StrToUpperFromInt = 414,
    StrToIntConcatNegOne = 415,
    StrLeqEmpty = 416,
    StrLeqEmptyEq = 417,
    StrLeqConcatFalse = 418,
    StrLeqConcatTrue = 419,
    StrLeqConcatBase1 = 420,
    StrLeqConcatBase2 = 421,
    StrLtElim = 422,
    StrFromIntNoCtnNondigit = 423,
    StrSubstrCtnContra = 424,
    StrSubstrCtn = 425,
    StrReplaceDualCtn = 426,
    StrReplaceDualCtnFalse = 427,
    StrReplaceSelfCtnSimp = 428,
    StrReplaceEmpCtnSrc = 429,
    StrSubstrCharStartEqLen = 430,
    StrContainsReplChar = 431,
    StrContainsReplSelfTgtChar = 432,
    StrContainsReplSelf = 433,
    StrContainsReplTgt = 434,
    StrReplReplLenId = 435,
    StrReplReplSrcTgtNoCtn = 436,
    StrReplReplTgtSelf = 437,
    StrReplReplTgtNoCtn = 438,
    StrReplReplSrcSelf = 439,
    StrReplReplSrcInvNoCtn1 = 440,
    StrReplReplSrcInvNoCtn2 = 441,
    StrReplReplSrcInvNoCtn3 = 442,
    StrReplReplDualSelf = 443,
    StrReplReplDualIte1 = 444,
    StrReplReplDualIte2 = 445,
    StrReplReplLookaheadIdSimp = 446,
    ReAllElim = 447,
    ReOptElim = 448,
    ReDiffElim = 449,
    RePlusElim = 450,
    ReRepeatElim = 451,
    ReConcatStarSwap = 452,
    ReConcatStarRepeat = 453,
    ReConcatStarSubsume1 = 454,
    ReConcatStarSubsume2 = 455,
    ReConcatMerge = 456,
    ReUnionAll = 457,
    ReUnionConstElim = 458,
    ReInterAll = 459,
    ReStarNone = 460,
    ReStarEmp = 461,
    ReStarStar = 462,
    ReStarUnionDropEmp = 463,
    ReLoopNeg = 464,
    ReInterCstring = 465,
    ReInterCstringNeg = 466,
    StrSubstrLenInclude = 467,
    StrSubstrLenIncludePre = 468,
    StrSubstrLenNorm = 469,
    SeqLenRev = 470,
    SeqRevRev = 471,
    SeqRevConcat = 472,
    StrEqReplSelfEmp = 473,
    StrEqReplNoChange = 474,
    StrEqReplTgtEqLen = 475,
    StrEqReplLenOneEmpPrefix = 476,
    StrEqReplEmpTgtNemp = 477,
    StrEqReplNempSrcEmp = 478,
    StrEqReplSelfSrc = 479,
    SeqLenUnit = 480,
    SeqNthUnit = 481,
    SeqRevUnit = 482,
    SeqLenEmpty = 483,
    ReInEmpty = 484,
    ReInSigma = 485,
    ReInSigmaStar = 486,
    ReInCstring = 487,
    ReInComp = 488,
    StrInReUnionElim = 489,
    StrInReInterElim = 490,
    StrInReRangeElim = 491,
    StrInReContains = 492,
    StrInReFromIntNempDigRange = 493,
    StrInReFromIntDigRange = 494,
    EqRefl = 495,
    EqSymm = 496,
    EqCondDeq = 497,
    EqIteLift = 498,
    DistinctBinaryElim = 499,
    UfBv2natInt2bv = 500,
    UfBv2natInt2bvExtend = 501,
    UfBv2natInt2bvExtract = 502,
    UfInt2bvBv2nat = 503,
    UfBv2natGeqElim = 504,
    UfInt2bvBvultEquiv = 505,
    UfInt2bvBvuleEquiv = 506,
    UfSbvToIntElim = 507,
    ArithSineZero = 508,
    ArithSinePi2 = 509,
    ArithCosineElim = 510,
    ArithTangentElim = 511,
    ArithSecentElim = 512,
    ArithCosecentElim = 513,
    ArithCotangentElim = 514,
    ArithPiNotInt = 515,
    SetsCardSingleton = 516,
    SetsCardUnion = 517,
    SetsCardMinus = 518,
    SetsCardEmp = 519,
    Last = 520,
}

Expand description

\verbatim embed:rst:leading-asterisk This enumeration represents the rewrite rules used in a rewrite proof. Some of the rules are internal ad-hoc rewrites, while others are rewrites specified by the RARE DSL. This enumeration is used as the first argument to the :cpp:enumerator:DSL_REWRITE <cvc5::ProofRule::DSL_REWRITE> proof rule and the :cpp:enumerator:THEORY_REWRITE <cvc5::ProofRule::THEORY_REWRITE> proof rule. \endverbatim