Enum Kind

Source

#[repr(i32)]pub enum Kind {
Show 295 variants    InternalKind = -2,
    UndefinedKind = -1,
    NullTerm = 0,
    UninterpretedSortValue = 1,
    Equal = 2,
    Distinct = 3,
    Constant = 4,
    Variable = 5,
    Skolem = 6,
    Sexpr = 7,
    Lambda = 8,
    Witness = 9,
    ConstBoolean = 10,
    Not = 11,
    And = 12,
    Implies = 13,
    Or = 14,
    Xor = 15,
    Ite = 16,
    ApplyUf = 17,
    CardinalityConstraint = 18,
    HoApply = 19,
    Add = 20,
    Mult = 21,
    Iand = 22,
    Pow2 = 23,
    Sub = 24,
    Neg = 25,
    Division = 26,
    DivisionTotal = 27,
    IntsDivision = 28,
    IntsDivisionTotal = 29,
    IntsModulus = 30,
    IntsModulusTotal = 31,
    Abs = 32,
    Pow = 33,
    Exponential = 34,
    Sine = 35,
    Cosine = 36,
    Tangent = 37,
    Cosecant = 38,
    Secant = 39,
    Cotangent = 40,
    Arcsine = 41,
    Arccosine = 42,
    Arctangent = 43,
    Arccosecant = 44,
    Arcsecant = 45,
    Arccotangent = 46,
    Sqrt = 47,
    Divisible = 48,
    ConstRational = 49,
    ConstInteger = 50,
    Lt = 51,
    Leq = 52,
    Gt = 53,
    Geq = 54,
    IsInteger = 55,
    ToInteger = 56,
    ToReal = 57,
    Pi = 58,
    ConstBitvector = 59,
    BitvectorConcat = 60,
    BitvectorAnd = 61,
    BitvectorOr = 62,
    BitvectorXor = 63,
    BitvectorNot = 64,
    BitvectorNand = 65,
    BitvectorNor = 66,
    BitvectorXnor = 67,
    BitvectorComp = 68,
    BitvectorMult = 69,
    BitvectorAdd = 70,
    BitvectorSub = 71,
    BitvectorNeg = 72,
    BitvectorUdiv = 73,
    BitvectorUrem = 74,
    BitvectorSdiv = 75,
    BitvectorSrem = 76,
    BitvectorSmod = 77,
    BitvectorShl = 78,
    BitvectorLshr = 79,
    BitvectorAshr = 80,
    BitvectorUlt = 81,
    BitvectorUle = 82,
    BitvectorUgt = 83,
    BitvectorUge = 84,
    BitvectorSlt = 85,
    BitvectorSle = 86,
    BitvectorSgt = 87,
    BitvectorSge = 88,
    BitvectorUltbv = 89,
    BitvectorSltbv = 90,
    BitvectorIte = 91,
    BitvectorRedor = 92,
    BitvectorRedand = 93,
    BitvectorNego = 94,
    BitvectorUaddo = 95,
    BitvectorSaddo = 96,
    BitvectorUmulo = 97,
    BitvectorSmulo = 98,
    BitvectorUsubo = 99,
    BitvectorSsubo = 100,
    BitvectorSdivo = 101,
    BitvectorExtract = 102,
    BitvectorRepeat = 103,
    BitvectorZeroExtend = 104,
    BitvectorSignExtend = 105,
    BitvectorRotateLeft = 106,
    BitvectorRotateRight = 107,
    IntToBitvector = 108,
    BitvectorToNat = 109,
    BitvectorUbvToInt = 110,
    BitvectorSbvToInt = 111,
    BitvectorFromBools = 112,
    BitvectorBit = 113,
    ConstFiniteField = 114,
    FiniteFieldNeg = 115,
    FiniteFieldAdd = 116,
    FiniteFieldBitsum = 117,
    FiniteFieldMult = 118,
    ConstFloatingpoint = 119,
    ConstRoundingmode = 120,
    FloatingpointFp = 121,
    FloatingpointEq = 122,
    FloatingpointAbs = 123,
    FloatingpointNeg = 124,
    FloatingpointAdd = 125,
    FloatingpointSub = 126,
    FloatingpointMult = 127,
    FloatingpointDiv = 128,
    FloatingpointFma = 129,
    FloatingpointSqrt = 130,
    FloatingpointRem = 131,
    FloatingpointRti = 132,
    FloatingpointMin = 133,
    FloatingpointMax = 134,
    FloatingpointLeq = 135,
    FloatingpointLt = 136,
    FloatingpointGeq = 137,
    FloatingpointGt = 138,
    FloatingpointIsNormal = 139,
    FloatingpointIsSubnormal = 140,
    FloatingpointIsZero = 141,
    FloatingpointIsInf = 142,
    FloatingpointIsNan = 143,
    FloatingpointIsNeg = 144,
    FloatingpointIsPos = 145,
    FloatingpointToFpFromIeeeBv = 146,
    FloatingpointToFpFromFp = 147,
    FloatingpointToFpFromReal = 148,
    FloatingpointToFpFromSbv = 149,
    FloatingpointToFpFromUbv = 150,
    FloatingpointToUbv = 151,
    FloatingpointToSbv = 152,
    FloatingpointToReal = 153,
    Select = 154,
    Store = 155,
    ConstArray = 156,
    EqRange = 157,
    ApplyConstructor = 158,
    ApplySelector = 159,
    ApplyTester = 160,
    ApplyUpdater = 161,
    Match = 162,
    MatchCase = 163,
    MatchBindCase = 164,
    TupleProject = 165,
    NullableLift = 166,
    SepNil = 167,
    SepEmp = 168,
    SepPto = 169,
    SepStar = 170,
    SepWand = 171,
    SetEmpty = 172,
    SetUnion = 173,
    SetInter = 174,
    SetMinus = 175,
    SetSubset = 176,
    SetMember = 177,
    SetSingleton = 178,
    SetInsert = 179,
    SetCard = 180,
    SetComplement = 181,
    SetUniverse = 182,
    SetComprehension = 183,
    SetChoose = 184,
    SetIsEmpty = 185,
    SetIsSingleton = 186,
    SetMap = 187,
    SetFilter = 188,
    SetAll = 189,
    SetSome = 190,
    SetFold = 191,
    RelationJoin = 192,
    RelationTableJoin = 193,
    RelationProduct = 194,
    RelationTranspose = 195,
    RelationTclosure = 196,
    RelationJoinImage = 197,
    RelationIden = 198,
    RelationGroup = 199,
    RelationAggregate = 200,
    RelationProject = 201,
    BagEmpty = 202,
    BagUnionMax = 203,
    BagUnionDisjoint = 204,
    BagInterMin = 205,
    BagDifferenceSubtract = 206,
    BagDifferenceRemove = 207,
    BagSubbag = 208,
    BagCount = 209,
    BagMember = 210,
    BagSetof = 211,
    BagMake = 212,
    BagCard = 213,
    BagChoose = 214,
    BagMap = 215,
    BagFilter = 216,
    BagAll = 217,
    BagSome = 218,
    BagFold = 219,
    BagPartition = 220,
    TableProduct = 221,
    TableProject = 222,
    TableAggregate = 223,
    TableJoin = 224,
    TableGroup = 225,
    StringConcat = 226,
    StringInRegexp = 227,
    StringLength = 228,
    StringSubstr = 229,
    StringUpdate = 230,
    StringCharat = 231,
    StringContains = 232,
    StringIndexof = 233,
    StringIndexofRe = 234,
    StringReplace = 235,
    StringReplaceAll = 236,
    StringReplaceRe = 237,
    StringReplaceReAll = 238,
    StringToLower = 239,
    StringToUpper = 240,
    StringRev = 241,
    StringToCode = 242,
    StringFromCode = 243,
    StringLt = 244,
    StringLeq = 245,
    StringPrefix = 246,
    StringSuffix = 247,
    StringIsDigit = 248,
    StringFromInt = 249,
    StringToInt = 250,
    ConstString = 251,
    StringToRegexp = 252,
    RegexpConcat = 253,
    RegexpUnion = 254,
    RegexpInter = 255,
    RegexpDiff = 256,
    RegexpStar = 257,
    RegexpPlus = 258,
    RegexpOpt = 259,
    RegexpRange = 260,
    RegexpRepeat = 261,
    RegexpLoop = 262,
    RegexpNone = 263,
    RegexpAll = 264,
    RegexpAllchar = 265,
    RegexpComplement = 266,
    SeqConcat = 267,
    SeqLength = 268,
    SeqExtract = 269,
    SeqUpdate = 270,
    SeqAt = 271,
    SeqContains = 272,
    SeqIndexof = 273,
    SeqReplace = 274,
    SeqReplaceAll = 275,
    SeqRev = 276,
    SeqPrefix = 277,
    SeqSuffix = 278,
    ConstSequence = 279,
    SeqUnit = 280,
    SeqNth = 281,
    Forall = 282,
    Exists = 283,
    VariableList = 284,
    InstPattern = 285,
    InstNoPattern = 286,
    InstPool = 287,
    InstAddToPool = 288,
    SkolemAddToPool = 289,
    InstAttribute = 290,
    InstPatternList = 291,
    LastKind = 292,
}

Expand description

The kind of a cvc5 Term.

\internal

Note that the API type cvc5::Kind roughly corresponds to cvc5::internal::Kind, but is a different type. It hides internal kinds that should not be exported to the API, and maps all kinds that we want to export to its corresponding internal kinds. The underlying type of cvc5::Kind must be signed (to enable range checks for validity). The size of this type depends on the size of cvc5::internal::Kind (NodeValue::NBITS_KIND, currently 10 bits, see expr/node_value.h).