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 = 161 

APPLY_SELECTOR = 162 

APPLY_TESTER = 163 

APPLY_UF = 17 

APPLY_UPDATER = 164 

ARCCOSECANT = 46 

ARCCOSINE = 44 

ARCCOTANGENT = 48 

ARCSECANT = 47 

ARCSINE = 43 

ARCTANGENT = 45 

BAG_ALL = 220 

BAG_CARD = 216 

BAG_CHOOSE = 217 

BAG_COUNT = 212 

BAG_DIFFERENCE_REMOVE = 210 

BAG_DIFFERENCE_SUBTRACT = 209 

BAG_EMPTY = 205 

BAG_FILTER = 219 

BAG_FOLD = 222 

BAG_INTER_MIN = 208 

BAG_MAKE = 215 

BAG_MAP = 218 

BAG_MEMBER = 213 

BAG_PARTITION = 223 

BAG_SETOF = 214 

BAG_SOME = 221 

BAG_SUBBAG = 211 

BAG_UNION_DISJOINT = 207 

BAG_UNION_MAX = 206 

BITVECTOR_ADD = 73 

BITVECTOR_AND = 64 

BITVECTOR_ASHR = 83 

BITVECTOR_BIT = 116 

BITVECTOR_COMP = 71 

BITVECTOR_CONCAT = 63 

BITVECTOR_EXTRACT = 105 

BITVECTOR_FROM_BOOLS = 115 

BITVECTOR_ITE = 94 

BITVECTOR_LSHR = 82 

BITVECTOR_MULT = 72 

BITVECTOR_NAND = 68 

BITVECTOR_NEG = 75 

BITVECTOR_NEGO = 97 

BITVECTOR_NOR = 69 

BITVECTOR_NOT = 67 

BITVECTOR_OR = 65 

BITVECTOR_REDAND = 96 

BITVECTOR_REDOR = 95 

BITVECTOR_REPEAT = 106 

BITVECTOR_ROTATE_LEFT = 109 

BITVECTOR_ROTATE_RIGHT = 110 

BITVECTOR_SADDO = 99 

BITVECTOR_SBV_TO_INT = 114 

BITVECTOR_SDIV = 78 

BITVECTOR_SDIVO = 104 

BITVECTOR_SGE = 91 

BITVECTOR_SGT = 90 

BITVECTOR_SHL = 81 

BITVECTOR_SIGN_EXTEND = 108 

BITVECTOR_SLE = 89 

BITVECTOR_SLT = 88 

BITVECTOR_SLTBV = 93 

BITVECTOR_SMOD = 80 

BITVECTOR_SMULO = 101 

BITVECTOR_SREM = 79 

BITVECTOR_SSUBO = 103 

BITVECTOR_SUB = 74 

BITVECTOR_TO_NAT = 112 

BITVECTOR_UADDO = 98 

BITVECTOR_UBV_TO_INT = 113 

BITVECTOR_UDIV = 76 

BITVECTOR_UGE = 87 

BITVECTOR_UGT = 86 

BITVECTOR_ULE = 85 

BITVECTOR_ULT = 84 

BITVECTOR_ULTBV = 92 

BITVECTOR_UMULO = 100 

BITVECTOR_UREM = 77 

BITVECTOR_USUBO = 102 

BITVECTOR_XNOR = 70 

BITVECTOR_XOR = 66 

BITVECTOR_ZERO_EXTEND = 107 

CARDINALITY_CONSTRAINT = 18 

CONSTANT = 4 

CONST_ARRAY = 159 

CONST_BITVECTOR = 62 

CONST_BOOLEAN = 10 

CONST_FINITE_FIELD = 117 

CONST_FLOATINGPOINT = 122 

CONST_INTEGER = 52 

CONST_RATIONAL = 51 

CONST_ROUNDINGMODE = 123 

CONST_SEQUENCE = 282 

CONST_STRING = 254 

COSECANT = 40 

COSINE = 38 

COTANGENT = 42 

DISTINCT = 3 

DIVISIBLE = 50 

DIVISION = 28 

DIVISION_TOTAL = 29 

EQUAL = 2 

EQ_RANGE = 160 

EXISTS = 286 

EXPONENTIAL = 36 

FINITE_FIELD_ADD = 119 

FINITE_FIELD_BITSUM = 120 

FINITE_FIELD_MULT = 121 

FINITE_FIELD_NEG = 118 

FLOATINGPOINT_ABS = 126 

FLOATINGPOINT_ADD = 128 

FLOATINGPOINT_DIV = 131 

FLOATINGPOINT_EQ = 125 

FLOATINGPOINT_FMA = 132 

FLOATINGPOINT_FP = 124 

FLOATINGPOINT_GEQ = 140 

FLOATINGPOINT_GT = 141 

FLOATINGPOINT_IS_INF = 145 

FLOATINGPOINT_IS_NAN = 146 

FLOATINGPOINT_IS_NEG = 147 

FLOATINGPOINT_IS_NORMAL = 142 

FLOATINGPOINT_IS_POS = 148 

FLOATINGPOINT_IS_SUBNORMAL = 143 

FLOATINGPOINT_IS_ZERO = 144 

FLOATINGPOINT_LEQ = 138 

FLOATINGPOINT_LT = 139 

FLOATINGPOINT_MAX = 137 

FLOATINGPOINT_MIN = 136 

FLOATINGPOINT_MULT = 130 

FLOATINGPOINT_NEG = 127 

FLOATINGPOINT_REM = 134 

FLOATINGPOINT_RTI = 135 

FLOATINGPOINT_SQRT = 133 

FLOATINGPOINT_SUB = 129 

FLOATINGPOINT_TO_FP_FROM_FP = 150 

FLOATINGPOINT_TO_FP_FROM_IEEE_BV = 149 

FLOATINGPOINT_TO_FP_FROM_REAL = 151 

FLOATINGPOINT_TO_FP_FROM_SBV = 152 

FLOATINGPOINT_TO_FP_FROM_UBV = 153 

FLOATINGPOINT_TO_REAL = 156 

FLOATINGPOINT_TO_SBV = 155 

FLOATINGPOINT_TO_UBV = 154 

FORALL = 285 

GEQ = 56 

GT = 55 

HO_APPLY = 19 

IAND = 22 

IMPLIES = 13 

INST_ADD_TO_POOL = 291 

INST_ATTRIBUTE = 293 

INST_NO_PATTERN = 289 

INST_PATTERN = 288 

INST_PATTERN_LIST = 294 

INST_POOL = 290 

INTERNAL_KIND = -2 

INTS_DIVISION = 30 

INTS_DIVISION_TOTAL = 31 

INTS_MODULUS = 32 

INTS_MODULUS_TOTAL = 33 

INT_TO_BITVECTOR = 111 

IS_INTEGER = 57 

ITE = 16 

LAMBDA = 8 

LAST_KIND = 295 

LEQ = 54 

LOG2 = 25 

LT = 53 

MATCH = 165 

MATCH_BIND_CASE = 167 

MATCH_CASE = 166 

MULT = 21 

NEG = 27 

NOT = 11 

NULLABLE_LIFT = 169 

NULL_TERM = 0 

OR = 14 

PI = 60 

PIAND = 23 

POW = 35 

POW2 = 24 

REGEXP_ALL = 267 

REGEXP_ALLCHAR = 268 

REGEXP_COMPLEMENT = 269 

REGEXP_CONCAT = 256 

REGEXP_DIFF = 259 

REGEXP_INTER = 258 

REGEXP_LOOP = 265 

REGEXP_NONE = 266 

REGEXP_OPT = 262 

REGEXP_PLUS = 261 

REGEXP_RANGE = 263 

REGEXP_REPEAT = 264 

REGEXP_STAR = 260 

REGEXP_UNION = 257 

RELATION_AGGREGATE = 203 

RELATION_GROUP = 202 

RELATION_IDEN = 201 

RELATION_JOIN = 195 

RELATION_JOIN_IMAGE = 200 

RELATION_PRODUCT = 197 

RELATION_PROJECT = 204 

RELATION_TABLE_JOIN = 196 

RELATION_TCLOSURE = 199 

RELATION_TRANSPOSE = 198 

SECANT = 41 

SELECT = 157 

SEP_EMP = 171 

SEP_NIL = 170 

SEP_PTO = 172 

SEP_STAR = 173 

SEP_WAND = 174 

SEQ_AT = 274 

SEQ_CONCAT = 270 

SEQ_CONTAINS = 275 

SEQ_EXTRACT = 272 

SEQ_INDEXOF = 276 

SEQ_LENGTH = 271 

SEQ_NTH = 284 

SEQ_PREFIX = 280 

SEQ_REPLACE = 277 

SEQ_REPLACE_ALL = 278 

SEQ_REV = 279 

SEQ_SUFFIX = 281 

SEQ_UNIT = 283 

SEQ_UPDATE = 273 

SET_ALL = 192 

SET_CARD = 183 

SET_CHOOSE = 187 

SET_COMPLEMENT = 184 

SET_COMPREHENSION = 186 

SET_EMPTY = 175 

SET_FILTER = 191 

SET_FOLD = 194 

SET_INSERT = 182 

SET_INTER = 177 

SET_IS_EMPTY = 188 

SET_IS_SINGLETON = 189 

SET_MAP = 190 

SET_MEMBER = 180 

SET_MINUS = 178 

SET_SINGLETON = 181 

SET_SOME = 193 

SET_SUBSET = 179 

SET_UNION = 176 

SET_UNIVERSE = 185 

SEXPR = 7 

SINE = 37 

SKOLEM = 6 

SKOLEM_ADD_TO_POOL = 292 

SQRT = 49 

STAR_CONTAINS = 61 

STORE = 158 

STRING_CHARAT = 234 

STRING_CONCAT = 229 

STRING_CONTAINS = 235 

STRING_FROM_CODE = 246 

STRING_FROM_INT = 252 

STRING_INDEXOF = 236 

STRING_INDEXOF_RE = 237 

STRING_IN_REGEXP = 230 

STRING_IS_DIGIT = 251 

STRING_LENGTH = 231 

STRING_LEQ = 248 

STRING_LT = 247 

STRING_PREFIX = 249 

STRING_REPLACE = 238 

STRING_REPLACE_ALL = 239 

STRING_REPLACE_RE = 240 

STRING_REPLACE_RE_ALL = 241 

STRING_REV = 244 

STRING_SUBSTR = 232 

STRING_SUFFIX = 250 

STRING_TO_CODE = 245 

STRING_TO_INT = 253 

STRING_TO_LOWER = 242 

STRING_TO_REGEXP = 255 

STRING_TO_UPPER = 243 

STRING_UPDATE = 233 

SUB = 26 

TABLE_AGGREGATE = 226 

TABLE_GROUP = 228 

TABLE_JOIN = 227 

TABLE_PRODUCT = 224 

TABLE_PROJECT = 225 

TANGENT = 39 

TO_INTEGER = 58 

TO_REAL = 59 

TUPLE_PROJECT = 168 

UNDEFINED_KIND = -1 

UNINTERPRETED_SORT_VALUE = 1 

VARIABLE = 5 

VARIABLE_LIST = 287 

WITNESS = 9 

XOR = 15 