Kind

Every Term has an associated kind, represented as enum class cvc5.Kind. This kind distinguishes if the Term is a value, constant, variable or operator, and what kind of each. For example, a bit-vector value has kind CONST_BITVECTOR, a free constant symbol has kind CONSTANT, an equality over terms of any sort has kind EQUAL, and a universally quantified formula has kind FORALL.

The kinds below directly correspond to the enum values of the C++ Kind enum.

class cvc5.Kind(*values)

The Kind enum

ABS = 34

ADD = 20

AND = 12

APPLY_CONSTRUCTOR = 160

APPLY_SELECTOR = 161

APPLY_TESTER = 162

APPLY_UF = 17

APPLY_UPDATER = 163

ARCCOSECANT = 46

ARCCOSINE = 44

ARCCOTANGENT = 48

ARCSECANT = 47

ARCSINE = 43

ARCTANGENT = 45

BAG_ALL = 219

BAG_CARD = 215

BAG_CHOOSE = 216

BAG_COUNT = 211

BAG_DIFFERENCE_REMOVE = 209

BAG_DIFFERENCE_SUBTRACT = 208

BAG_EMPTY = 204

BAG_FILTER = 218

BAG_FOLD = 221

BAG_INTER_MIN = 207

BAG_MAKE = 214

BAG_MAP = 217

BAG_MEMBER = 212

BAG_PARTITION = 222

BAG_SETOF = 213

BAG_SOME = 220

BAG_SUBBAG = 210

BAG_UNION_DISJOINT = 206

BAG_UNION_MAX = 205

BITVECTOR_ADD = 72

BITVECTOR_AND = 63

BITVECTOR_ASHR = 82

BITVECTOR_BIT = 115

BITVECTOR_COMP = 70

BITVECTOR_CONCAT = 62

BITVECTOR_EXTRACT = 104

BITVECTOR_FROM_BOOLS = 114

BITVECTOR_ITE = 93

BITVECTOR_LSHR = 81

BITVECTOR_MULT = 71

BITVECTOR_NAND = 67

BITVECTOR_NEG = 74

BITVECTOR_NEGO = 96

BITVECTOR_NOR = 68

BITVECTOR_NOT = 66

BITVECTOR_OR = 64

BITVECTOR_REDAND = 95

BITVECTOR_REDOR = 94

BITVECTOR_REPEAT = 105

BITVECTOR_ROTATE_LEFT = 108

BITVECTOR_ROTATE_RIGHT = 109

BITVECTOR_SADDO = 98

BITVECTOR_SBV_TO_INT = 113

BITVECTOR_SDIV = 77

BITVECTOR_SDIVO = 103

BITVECTOR_SGE = 90

BITVECTOR_SGT = 89

BITVECTOR_SHL = 80

BITVECTOR_SIGN_EXTEND = 107

BITVECTOR_SLE = 88

BITVECTOR_SLT = 87

BITVECTOR_SLTBV = 92

BITVECTOR_SMOD = 79

BITVECTOR_SMULO = 100

BITVECTOR_SREM = 78

BITVECTOR_SSUBO = 102

BITVECTOR_SUB = 73

BITVECTOR_TO_NAT = 111

BITVECTOR_UADDO = 97

BITVECTOR_UBV_TO_INT = 112

BITVECTOR_UDIV = 75

BITVECTOR_UGE = 86

BITVECTOR_UGT = 85

BITVECTOR_ULE = 84

BITVECTOR_ULT = 83

BITVECTOR_ULTBV = 91

BITVECTOR_UMULO = 99

BITVECTOR_UREM = 76

BITVECTOR_USUBO = 101

BITVECTOR_XNOR = 69

BITVECTOR_XOR = 65

BITVECTOR_ZERO_EXTEND = 106

CARDINALITY_CONSTRAINT = 18

CONSTANT = 4

CONST_ARRAY = 158

CONST_BITVECTOR = 61

CONST_BOOLEAN = 10

CONST_FINITE_FIELD = 116

CONST_FLOATINGPOINT = 121

CONST_INTEGER = 52

CONST_RATIONAL = 51

CONST_ROUNDINGMODE = 122

CONST_SEQUENCE = 281

CONST_STRING = 253

COSECANT = 40

COSINE = 38

COTANGENT = 42

DISTINCT = 3

DIVISIBLE = 50

DIVISION = 28

DIVISION_TOTAL = 29

EQUAL = 2

EQ_RANGE = 159

EXISTS = 285

EXPONENTIAL = 36

FINITE_FIELD_ADD = 118

FINITE_FIELD_BITSUM = 119

FINITE_FIELD_MULT = 120

FINITE_FIELD_NEG = 117

FLOATINGPOINT_ABS = 125

FLOATINGPOINT_ADD = 127

FLOATINGPOINT_DIV = 130

FLOATINGPOINT_EQ = 124

FLOATINGPOINT_FMA = 131

FLOATINGPOINT_FP = 123

FLOATINGPOINT_GEQ = 139

FLOATINGPOINT_GT = 140

FLOATINGPOINT_IS_INF = 144

FLOATINGPOINT_IS_NAN = 145

FLOATINGPOINT_IS_NEG = 146

FLOATINGPOINT_IS_NORMAL = 141

FLOATINGPOINT_IS_POS = 147

FLOATINGPOINT_IS_SUBNORMAL = 142

FLOATINGPOINT_IS_ZERO = 143

FLOATINGPOINT_LEQ = 137

FLOATINGPOINT_LT = 138

FLOATINGPOINT_MAX = 136

FLOATINGPOINT_MIN = 135

FLOATINGPOINT_MULT = 129

FLOATINGPOINT_NEG = 126

FLOATINGPOINT_REM = 133

FLOATINGPOINT_RTI = 134

FLOATINGPOINT_SQRT = 132

FLOATINGPOINT_SUB = 128

FLOATINGPOINT_TO_FP_FROM_FP = 149

FLOATINGPOINT_TO_FP_FROM_IEEE_BV = 148

FLOATINGPOINT_TO_FP_FROM_REAL = 150

FLOATINGPOINT_TO_FP_FROM_SBV = 151

FLOATINGPOINT_TO_FP_FROM_UBV = 152

FLOATINGPOINT_TO_REAL = 155

FLOATINGPOINT_TO_SBV = 154

FLOATINGPOINT_TO_UBV = 153

FORALL = 284

GEQ = 56

GT = 55

HO_APPLY = 19

IAND = 22

IMPLIES = 13

INST_ADD_TO_POOL = 290

INST_ATTRIBUTE = 292

INST_NO_PATTERN = 288

INST_PATTERN = 287

INST_PATTERN_LIST = 293

INST_POOL = 289

INTERNAL_KIND = -2

INTS_DIVISION = 30

INTS_DIVISION_TOTAL = 31

INTS_MODULUS = 32

INTS_MODULUS_TOTAL = 33

INT_TO_BITVECTOR = 110

IS_INTEGER = 57

ITE = 16

LAMBDA = 8

LAST_KIND = 294

LEQ = 54

LOG2 = 25

LT = 53

MATCH = 164

MATCH_BIND_CASE = 166

MATCH_CASE = 165

MULT = 21

NEG = 27

NOT = 11

NULLABLE_LIFT = 168

NULL_TERM = 0

OR = 14

PI = 60

PIAND = 23

POW = 35

POW2 = 24

REGEXP_ALL = 266

REGEXP_ALLCHAR = 267

REGEXP_COMPLEMENT = 268

REGEXP_CONCAT = 255

REGEXP_DIFF = 258

REGEXP_INTER = 257

REGEXP_LOOP = 264

REGEXP_NONE = 265

REGEXP_OPT = 261

REGEXP_PLUS = 260

REGEXP_RANGE = 262

REGEXP_REPEAT = 263

REGEXP_STAR = 259

REGEXP_UNION = 256

RELATION_AGGREGATE = 202

RELATION_GROUP = 201

RELATION_IDEN = 200

RELATION_JOIN = 194

RELATION_JOIN_IMAGE = 199

RELATION_PRODUCT = 196

RELATION_PROJECT = 203

RELATION_TABLE_JOIN = 195

RELATION_TCLOSURE = 198

RELATION_TRANSPOSE = 197

SECANT = 41

SELECT = 156

SEP_EMP = 170

SEP_NIL = 169

SEP_PTO = 171

SEP_STAR = 172

SEP_WAND = 173

SEQ_AT = 273

SEQ_CONCAT = 269

SEQ_CONTAINS = 274

SEQ_EXTRACT = 271

SEQ_INDEXOF = 275

SEQ_LENGTH = 270

SEQ_NTH = 283

SEQ_PREFIX = 279

SEQ_REPLACE = 276

SEQ_REPLACE_ALL = 277

SEQ_REV = 278

SEQ_SUFFIX = 280

SEQ_UNIT = 282

SEQ_UPDATE = 272

SET_ALL = 191

SET_CARD = 182

SET_CHOOSE = 186

SET_COMPLEMENT = 183

SET_COMPREHENSION = 185

SET_EMPTY = 174

SET_FILTER = 190

SET_FOLD = 193

SET_INSERT = 181

SET_INTER = 176

SET_IS_EMPTY = 187

SET_IS_SINGLETON = 188

SET_MAP = 189

SET_MEMBER = 179

SET_MINUS = 177

SET_SINGLETON = 180

SET_SOME = 192

SET_SUBSET = 178

SET_UNION = 175

SET_UNIVERSE = 184

SEXPR = 7

SINE = 37

SKOLEM = 6

SKOLEM_ADD_TO_POOL = 291

SQRT = 49

STORE = 157

STRING_CHARAT = 233

STRING_CONCAT = 228

STRING_CONTAINS = 234

STRING_FROM_CODE = 245

STRING_FROM_INT = 251

STRING_INDEXOF = 235

STRING_INDEXOF_RE = 236

STRING_IN_REGEXP = 229

STRING_IS_DIGIT = 250

STRING_LENGTH = 230

STRING_LEQ = 247

STRING_LT = 246

STRING_PREFIX = 248

STRING_REPLACE = 237

STRING_REPLACE_ALL = 238

STRING_REPLACE_RE = 239

STRING_REPLACE_RE_ALL = 240

STRING_REV = 243

STRING_SUBSTR = 231

STRING_SUFFIX = 249

STRING_TO_CODE = 244

STRING_TO_INT = 252

STRING_TO_LOWER = 241

STRING_TO_REGEXP = 254

STRING_TO_UPPER = 242

STRING_UPDATE = 232

SUB = 26

TABLE_AGGREGATE = 225

TABLE_GROUP = 227

TABLE_JOIN = 226

TABLE_PRODUCT = 223

TABLE_PROJECT = 224

TANGENT = 39

TO_INTEGER = 58

TO_REAL = 59

TUPLE_PROJECT = 167

UNDEFINED_KIND = -1

UNINTERPRETED_SORT_VALUE = 1

VARIABLE = 5

VARIABLE_LIST = 286

WITNESS = 9

XOR = 15