/*********************                                                        */
/** kind.h
 **
 ** Copyright 2010-2014  New York University and The University of Iowa,
 ** and as below.
 **
 ** This header file automatically generated by:
 **
 **     ${BD}/src/expr/mkkind ${BD}/src/expr/kind_template.h ${BD}/src/theory/builtin/kinds ${BD}/src/theory/booleans/kinds ${BD}/src/theory/uf/kinds ${BD}/src/theory/arith/kinds ${BD}/src/theory/bv/kinds ${BD}/src/theory/fp/kinds ${BD}/src/theory/arrays/kinds ${BD}/src/theory/datatypes/kinds ${BD}/src/theory/sep/kinds ${BD}/src/theory/sets/kinds ${BD}/src/theory/strings/kinds ${BD}/src/theory/quantifiers/kinds
 **
 ** for the CVC4 project.
 **/

/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */

/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */

/* Edit the template file instead:                     */
/* ${BD}/src/expr/kind_template.h */

/*********************                                                        */
/*! \file kind_template.h
 ** \verbatim
 ** Top contributors (to current version):
 **   Andres Noetzli, Morgan Deters, Dejan Jovanovic
 ** This file is part of the CVC4 project.
 ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
 ** in the top-level source directory) and their institutional affiliations.
 ** All rights reserved.  See the file COPYING in the top-level source
 ** directory for licensing information.\endverbatim
 **
 ** \brief Template for the Node kind header
 **
 ** Template for the Node kind header.
 **/

#include "cvc4_public.h"

#ifndef CVC4__KIND_H
#define CVC4__KIND_H

#include <iosfwd>

#include "base/exception.h"
#include "theory/theory_id.h"

namespace CVC4 {
namespace kind {

enum CVC4_PUBLIC Kind_t {
  UNDEFINED_KIND = -1, /**< undefined */
  NULL_EXPR, /**< Null kind */

  /* from builtin */
  SORT_TAG, /**< sort tag (1) */
  SORT_TYPE, /**< specifies types of user-declared 'uninterpreted' sorts (2) */
  UNINTERPRETED_CONSTANT, /**< the kind of expressions representing uninterpreted constants; payload is an instance of the CVC4::UninterpretedConstant class (used in models) (3) */
  ABSTRACT_VALUE, /**< the kind of expressions representing abstract values (other than uninterpreted sort constants); payload is an instance of the CVC4::AbstractValue class (used in models) (4) */
  BUILTIN, /**< the kind of expressions representing built-in operators (5) */
  EQUAL, /**< equality (two parameters only, sorts must match) (6) */
  DISTINCT, /**< disequality (N-ary, sorts must match) (7) */
  VARIABLE, /**< a variable (not permitted in bindings) (8) */
  BOUND_VARIABLE, /**< a bound variable (permitted in bindings and the associated lambda and quantifier bodies only) (9) */
  SKOLEM, /**< a Skolem variable (internal only) (10) */
  SEXPR, /**< a symbolic expression (any arity) (11) */
  LAMBDA, /**< a lambda expression; first parameter is a BOUND_VAR_LIST, second is lambda body (12) */
  WITNESS, /**< a witness expression; first parameter is a BOUND_VAR_LIST, second is the witness body (13) */
  TYPE_CONSTANT, /**< a representation for basic types (14) */
  FUNCTION_TYPE, /**< a function type (15) */
  SEXPR_TYPE, /**< the type of a symbolic expression (16) */

  /* from booleans */
  CONST_BOOLEAN, /**< truth and falsity; payload is a (C++) bool (17) */
  NOT, /**< logical not (18) */
  AND, /**< logical and (N-ary) (19) */
  IMPLIES, /**< logical implication (exactly two parameters) (20) */
  OR, /**< logical or (N-ary) (21) */
  XOR, /**< exclusive or (exactly two parameters) (22) */
  ITE, /**< if-then-else, used for both Boolean and term ITE constructs; first parameter is (Boolean-sorted) condition, second is 'then', third is 'else' and these two parameters must have same base sort (23) */

  /* from uf */
  APPLY_UF, /**< application of an uninterpreted function; first parameter is the function, remaining ones are parameters to that function (24) */
  BOOLEAN_TERM_VARIABLE, /**< Boolean term variable (25) */
  CARDINALITY_CONSTRAINT, /**< cardinality constraint on sort S: first parameter is (any) term of sort S, second is a positive integer constant k that bounds the cardinality of S (26) */
  COMBINED_CARDINALITY_CONSTRAINT, /**< combined cardinality constraint; parameter is a positive integer constant k that bounds the sum of the cardinalities of all sorts in the signature (27) */
  PARTIAL_APPLY_UF, /**< partial uninterpreted function application (28) */
  CARDINALITY_VALUE, /**< cardinality value of sort S: first parameter is (any) term of sort S (29) */
  HO_APPLY, /**< higher-order (partial) function application (30) */

  /* from arith */
  PLUS, /**< arithmetic addition (N-ary) (31) */
  MULT, /**< arithmetic multiplication (N-ary) (32) */
  NONLINEAR_MULT, /**< synonym for MULT (33) */
  MINUS, /**< arithmetic binary subtraction operator (34) */
  UMINUS, /**< arithmetic unary negation (35) */
  DIVISION, /**< real division, division by 0 undefined (user symbol) (36) */
  DIVISION_TOTAL, /**< real division with interpreted division by 0 (internal symbol) (37) */
  INTS_DIVISION, /**< integer division, division by 0 undefined (user symbol) (38) */
  INTS_DIVISION_TOTAL, /**< integer division with interpreted division by 0 (internal symbol) (39) */
  INTS_MODULUS, /**< integer modulus, division by 0 undefined (user symbol) (40) */
  INTS_MODULUS_TOTAL, /**< integer modulus with interpreted division by 0 (internal symbol) (41) */
  ABS, /**< absolute value (42) */
  DIVISIBLE, /**< divisibility-by-k predicate; first parameter is a DIVISIBLE_OP, second is integer term (43) */
  POW, /**< arithmetic power (44) */
  EXPONENTIAL, /**< exponential (45) */
  SINE, /**< sine (46) */
  COSINE, /**< consine (47) */
  TANGENT, /**< tangent (48) */
  COSECANT, /**< cosecant (49) */
  SECANT, /**< secant (50) */
  COTANGENT, /**< cotangent (51) */
  ARCSINE, /**< arc sine (52) */
  ARCCOSINE, /**< arc consine (53) */
  ARCTANGENT, /**< arc tangent (54) */
  ARCCOSECANT, /**< arc cosecant (55) */
  ARCSECANT, /**< arc secant (56) */
  ARCCOTANGENT, /**< arc cotangent (57) */
  SQRT, /**< square root (58) */
  DIVISIBLE_OP, /**< operator for the divisibility-by-k predicate; payload is an instance of the CVC4::Divisible class (59) */
  CONST_RATIONAL, /**< a multiple-precision rational constant; payload is an instance of the CVC4::Rational class (60) */
  LT, /**< less than, x < y (61) */
  LEQ, /**< less than or equal, x <= y (62) */
  GT, /**< greater than, x > y (63) */
  GEQ, /**< greater than or equal, x >= y (64) */
  IS_INTEGER, /**< term-is-integer predicate (parameter is a real-sorted term) (65) */
  TO_INTEGER, /**< convert term to integer by the floor function (parameter is a real-sorted term) (66) */
  TO_REAL, /**< cast term to real (parameter is an integer-sorted term; this is a no-op in CVC4, as integer is a subtype of real) (67) */
  PI, /**< pi (68) */

  /* from bv */
  BITVECTOR_TYPE, /**< bit-vector type (69) */
  CONST_BITVECTOR, /**< a fixed-width bit-vector constant; payload is an instance of the CVC4::BitVector class (70) */
  BITVECTOR_CONCAT, /**< concatenation of two or more bit-vectors (71) */
  BITVECTOR_AND, /**< bitwise and of two or more bit-vectors (72) */
  BITVECTOR_COMP, /**< equality comparison of two bit-vectors (returns one bit) (73) */
  BITVECTOR_OR, /**< bitwise or of two or more bit-vectors (74) */
  BITVECTOR_XOR, /**< bitwise xor of two or more bit-vectors (75) */
  BITVECTOR_NOT, /**< bitwise not of a bit-vector (76) */
  BITVECTOR_NAND, /**< bitwise nand of two bit-vectors (77) */
  BITVECTOR_NOR, /**< bitwise nor of two bit-vectors (78) */
  BITVECTOR_XNOR, /**< bitwise xnor of two bit-vectors (79) */
  BITVECTOR_MULT, /**< multiplication of two or more bit-vectors (80) */
  BITVECTOR_NEG, /**< unary negation of a bit-vector (81) */
  BITVECTOR_PLUS, /**< addition of two or more bit-vectors (82) */
  BITVECTOR_SUB, /**< subtraction of two bit-vectors (83) */
  BITVECTOR_UDIV, /**< unsigned division of two bit-vectors, truncating towards 0 (undefined if divisor is 0) (84) */
  BITVECTOR_UREM, /**< unsigned remainder from truncating division of two bit-vectors (undefined if divisor is 0) (85) */
  BITVECTOR_SDIV, /**< 2's complement signed division (86) */
  BITVECTOR_SMOD, /**< 2's complement signed remainder (sign follows divisor) (87) */
  BITVECTOR_SREM, /**< 2's complement signed remainder (sign follows dividend) (88) */
  BITVECTOR_UDIV_TOTAL, /**< unsigned division of two bit-vectors, truncating towards 0 (defined to be the all-ones bit pattern, if divisor is 0) (89) */
  BITVECTOR_UREM_TOTAL, /**< unsigned remainder from truncating division of two bit-vectors (defined to be equal to the dividend, if divisor is 0) (90) */
  BITVECTOR_ASHR, /**< bit-vector arithmetic shift right (the two bit-vector parameters must have same width) (91) */
  BITVECTOR_LSHR, /**< bit-vector logical shift right (the two bit-vector parameters must have same width) (92) */
  BITVECTOR_SHL, /**< bit-vector shift left (the two bit-vector parameters must have same width) (93) */
  BITVECTOR_ULE, /**< bit-vector unsigned less than or equal (the two bit-vector parameters must have same width) (94) */
  BITVECTOR_ULT, /**< bit-vector unsigned less than (the two bit-vector parameters must have same width) (95) */
  BITVECTOR_UGE, /**< bit-vector unsigned greater than or equal (the two bit-vector parameters must have same width) (96) */
  BITVECTOR_UGT, /**< bit-vector unsigned greater than (the two bit-vector parameters must have same width) (97) */
  BITVECTOR_SLE, /**< bit-vector signed less than or equal (the two bit-vector parameters must have same width) (98) */
  BITVECTOR_SLT, /**< bit-vector signed less than (the two bit-vector parameters must have same width) (99) */
  BITVECTOR_SGE, /**< bit-vector signed greater than or equal (the two bit-vector parameters must have same width) (100) */
  BITVECTOR_SGT, /**< bit-vector signed greater than (the two bit-vector parameters must have same width) (101) */
  BITVECTOR_ULTBV, /**< bit-vector unsigned less than but returns bv of size 1 instead of boolean (102) */
  BITVECTOR_SLTBV, /**< bit-vector signed less than but returns bv of size 1 instead of boolean (103) */
  BITVECTOR_REDAND, /**< bit-vector redand (104) */
  BITVECTOR_REDOR, /**< bit-vector redor (105) */
  BITVECTOR_ITE, /**< same semantics as regular ITE, but condition is bv of size 1 instead of Boolean (106) */
  BITVECTOR_TO_NAT, /**< bit-vector conversion to (nonnegative) integer; parameter is a bit-vector (107) */
  BITVECTOR_ACKERMANNIZE_UDIV, /**< term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvudiv (internal-only symbol) (108) */
  BITVECTOR_ACKERMANNIZE_UREM, /**< term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvurem (internal-only symbol) (109) */
  BITVECTOR_EAGER_ATOM, /**< formula to be treated as a bv atom via eager bit-blasting (internal-only symbol) (110) */
  BITVECTOR_BITOF_OP, /**< operator for the bit-vector boolean bit extract; payload is an instance of the CVC4::BitVectorBitOf class (111) */
  BITVECTOR_BITOF, /**< bit-vector boolean bit extract; first parameter is a BITVECTOR_BITOF_OP, second is a bit-vector term (112) */
  BITVECTOR_EXTRACT_OP, /**< operator for the bit-vector extract; payload is an instance of the CVC4::BitVectorExtract class (113) */
  BITVECTOR_EXTRACT, /**< bit-vector extract; first parameter is a BITVECTOR_EXTRACT_OP, second is a bit-vector term (114) */
  BITVECTOR_REPEAT_OP, /**< operator for the bit-vector repeat; payload is an instance of the CVC4::BitVectorRepeat class (115) */
  BITVECTOR_REPEAT, /**< bit-vector repeat; first parameter is a BITVECTOR_REPEAT_OP, second is a bit-vector term (116) */
  BITVECTOR_ROTATE_LEFT_OP, /**< operator for the bit-vector rotate left; payload is an instance of the CVC4::BitVectorRotateLeft class (117) */
  BITVECTOR_ROTATE_LEFT, /**< bit-vector rotate left; first parameter is a BITVECTOR_ROTATE_LEFT_OP, second is a bit-vector term (118) */
  BITVECTOR_ROTATE_RIGHT_OP, /**< operator for the bit-vector rotate right; payload is an instance of the CVC4::BitVectorRotateRight class (119) */
  BITVECTOR_ROTATE_RIGHT, /**< bit-vector rotate right; first parameter is a BITVECTOR_ROTATE_RIGHT_OP, second is a bit-vector term (120) */
  BITVECTOR_SIGN_EXTEND_OP, /**< operator for the bit-vector sign-extend; payload is an instance of the CVC4::BitVectorSignExtend class (121) */
  BITVECTOR_SIGN_EXTEND, /**< bit-vector sign-extend; first parameter is a BITVECTOR_SIGN_EXTEND_OP, second is a bit-vector term (122) */
  BITVECTOR_ZERO_EXTEND_OP, /**< operator for the bit-vector zero-extend; payload is an instance of the CVC4::BitVectorZeroExtend class (123) */
  BITVECTOR_ZERO_EXTEND, /**< bit-vector zero-extend; first parameter is a BITVECTOR_ZERO_EXTEND_OP, second is a bit-vector term (124) */
  INT_TO_BITVECTOR_OP, /**< operator for the integer conversion to bit-vector; payload is an instance of the CVC4::IntToBitVector class (125) */
  INT_TO_BITVECTOR, /**< integer conversion to bit-vector; first parameter is an INT_TO_BITVECTOR_OP, second is an integer term (126) */

  /* from fp */
  CONST_FLOATINGPOINT, /**< a floating-point literal (127) */
  CONST_ROUNDINGMODE, /**< a floating-point rounding mode (128) */
  FLOATINGPOINT_TYPE, /**< floating-point type (129) */
  FLOATINGPOINT_FP, /**< construct a floating-point literal from bit vectors (130) */
  FLOATINGPOINT_EQ, /**< floating-point equality (131) */
  FLOATINGPOINT_ABS, /**< floating-point absolute value (132) */
  FLOATINGPOINT_NEG, /**< floating-point negation (133) */
  FLOATINGPOINT_PLUS, /**< floating-point addition (134) */
  FLOATINGPOINT_SUB, /**< floating-point sutraction (135) */
  FLOATINGPOINT_MULT, /**< floating-point multiply (136) */
  FLOATINGPOINT_DIV, /**< floating-point division (137) */
  FLOATINGPOINT_FMA, /**< floating-point fused multiply and add (138) */
  FLOATINGPOINT_SQRT, /**< floating-point square root (139) */
  FLOATINGPOINT_REM, /**< floating-point remainder (140) */
  FLOATINGPOINT_RTI, /**< floating-point round to integral (141) */
  FLOATINGPOINT_MIN, /**< floating-point minimum (142) */
  FLOATINGPOINT_MAX, /**< floating-point maximum (143) */
  FLOATINGPOINT_MIN_TOTAL, /**< floating-point minimum (defined for all inputs) (144) */
  FLOATINGPOINT_MAX_TOTAL, /**< floating-point maximum (defined for all inputs) (145) */
  FLOATINGPOINT_LEQ, /**< floating-point less than or equal (146) */
  FLOATINGPOINT_LT, /**< floating-point less than (147) */
  FLOATINGPOINT_GEQ, /**< floating-point greater than or equal (148) */
  FLOATINGPOINT_GT, /**< floating-point greater than (149) */
  FLOATINGPOINT_ISN, /**< floating-point is normal (150) */
  FLOATINGPOINT_ISSN, /**< floating-point is sub-normal (151) */
  FLOATINGPOINT_ISZ, /**< floating-point is zero (152) */
  FLOATINGPOINT_ISINF, /**< floating-point is infinite (153) */
  FLOATINGPOINT_ISNAN, /**< floating-point is NaN (154) */
  FLOATINGPOINT_ISNEG, /**< floating-point is negative (155) */
  FLOATINGPOINT_ISPOS, /**< floating-point is positive (156) */
  FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP, /**< operator for to_fp from bit vector (157) */
  FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, /**< convert an IEEE-754 bit vector to floating-point (158) */
  FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP, /**< operator for to_fp from floating point (159) */
  FLOATINGPOINT_TO_FP_FLOATINGPOINT, /**< convert between floating-point sorts (160) */
  FLOATINGPOINT_TO_FP_REAL_OP, /**< operator for to_fp from real (161) */
  FLOATINGPOINT_TO_FP_REAL, /**< convert a real to floating-point (162) */
  FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP, /**< operator for to_fp from signed bit vector (163) */
  FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, /**< convert a signed bit vector to floating-point (164) */
  FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP, /**< operator for to_fp from unsigned bit vector (165) */
  FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, /**< convert an unsigned bit vector to floating-point (166) */
  FLOATINGPOINT_TO_FP_GENERIC_OP, /**< operator for a generic to_fp (167) */
  FLOATINGPOINT_TO_FP_GENERIC, /**< a generic conversion to floating-point, used in parsing only (168) */
  FLOATINGPOINT_TO_UBV_OP, /**< operator for to_ubv (169) */
  FLOATINGPOINT_TO_UBV, /**< convert a floating-point value to an unsigned bit vector (170) */
  FLOATINGPOINT_TO_UBV_TOTAL_OP, /**< operator for to_ubv_total (171) */
  FLOATINGPOINT_TO_UBV_TOTAL, /**< convert a floating-point value to an unsigned bit vector (defined for all inputs) (172) */
  FLOATINGPOINT_TO_SBV_OP, /**< operator for to_sbv (173) */
  FLOATINGPOINT_TO_SBV, /**< convert a floating-point value to a signed bit vector (174) */
  FLOATINGPOINT_TO_SBV_TOTAL_OP, /**< operator for to_sbv_total (175) */
  FLOATINGPOINT_TO_SBV_TOTAL, /**< convert a floating-point value to a signed bit vector (defined for all inputs) (176) */
  FLOATINGPOINT_TO_REAL, /**< floating-point to real (177) */
  FLOATINGPOINT_TO_REAL_TOTAL, /**< floating-point to real (defined for all inputs) (178) */
  FLOATINGPOINT_COMPONENT_NAN, /**< NaN component of a word-blasted floating-point number (179) */
  FLOATINGPOINT_COMPONENT_INF, /**< Inf component of a word-blasted floating-point number (180) */
  FLOATINGPOINT_COMPONENT_ZERO, /**< Zero component of a word-blasted floating-point number (181) */
  FLOATINGPOINT_COMPONENT_SIGN, /**< Sign component of a word-blasted floating-point number (182) */
  FLOATINGPOINT_COMPONENT_EXPONENT, /**< Exponent component of a word-blasted floating-point number (183) */
  FLOATINGPOINT_COMPONENT_SIGNIFICAND, /**< Significand component of a word-blasted floating-point number (184) */
  ROUNDINGMODE_BITBLAST, /**< The bit-vector for a non-deterministic rounding mode (185) */

  /* from arrays */
  ARRAY_TYPE, /**< array type (186) */
  SELECT, /**< array select; first parameter is an array term, second is the selection index (187) */
  STORE, /**< array store; first parameter is an array term, second is the store index, third is the term to store at the index (188) */
  STORE_ALL, /**< array store-all; payload is an instance of the CVC4::ArrayStoreAll class (this is not supported by arrays decision procedure yet, but it is used for returned array models) (189) */
  ARR_TABLE_FUN, /**< array table function (internal-only symbol) (190) */
  ARRAY_LAMBDA, /**< array lambda (internal-only symbol) (191) */
  PARTIAL_SELECT_0, /**< partial array select, for internal use only (192) */
  PARTIAL_SELECT_1, /**< partial array select, for internal use only (193) */

  /* from datatypes */
  CONSTRUCTOR_TYPE, /**< constructor (194) */
  SELECTOR_TYPE, /**< selector (195) */
  TESTER_TYPE, /**< tester (196) */
  APPLY_CONSTRUCTOR, /**< constructor application; first parameter is the constructor, remaining parameters (if any) are parameters to the constructor (197) */
  APPLY_SELECTOR, /**< selector application; parameter is a datatype term (undefined if mis-applied) (198) */
  APPLY_SELECTOR_TOTAL, /**< selector application; parameter is a datatype term (defined rigidly if mis-applied) (199) */
  APPLY_TESTER, /**< tester application; first parameter is a tester, second is a datatype term (200) */
  DATATYPE_TYPE, /**< a datatype type index (201) */
  PARAMETRIC_DATATYPE, /**< parametric datatype (202) */
  APPLY_TYPE_ASCRIPTION, /**< type ascription, for datatype constructor applications; first parameter is an ASCRIPTION_TYPE, second is the datatype constructor application being ascribed (203) */
  ASCRIPTION_TYPE, /**< a type parameter for type ascription; payload is an instance of the CVC4::AscriptionType class (204) */
  TUPLE_UPDATE_OP, /**< operator for a tuple update; payload is an instance of the CVC4::TupleUpdate class (205) */
  TUPLE_UPDATE, /**< tuple update; first parameter is a TUPLE_UPDATE_OP (which references an index), second is the tuple, third is the element to store in the tuple at the given index (206) */
  RECORD_UPDATE_OP, /**< operator for a record update; payload is an instance CVC4::RecordUpdate class (207) */
  RECORD_UPDATE, /**< record update; first parameter is a RECORD_UPDATE_OP (which references a field), second is a record term to update, third is the element to store in the record in the given field (208) */
  DT_SIZE, /**< datatypes size (209) */
  DT_HEIGHT_BOUND, /**< datatypes height bound (210) */
  DT_SIZE_BOUND, /**< datatypes height bound (211) */
  DT_SYGUS_BOUND, /**< datatypes sygus bound (212) */
  DT_SYGUS_EVAL, /**< datatypes sygus evaluation function (213) */
  MATCH, /**< match construct (214) */
  MATCH_CASE, /**< a match case (215) */
  MATCH_BIND_CASE, /**< a match case with bound variables (216) */

  /* from sep */
  SEP_NIL, /**< separation nil (217) */
  SEP_EMP, /**< separation empty heap (218) */
  SEP_PTO, /**< points to relation (219) */
  SEP_STAR, /**< separation star (220) */
  SEP_WAND, /**< separation magic wand (221) */
  SEP_LABEL, /**< separation label (internal use only) (222) */

  /* from sets */
  EMPTYSET, /**< the empty set constant; payload is an instance of the CVC4::EmptySet class (223) */
  SET_TYPE, /**< set type, takes as parameter the type of the elements (224) */
  UNION, /**< set union (225) */
  INTERSECTION, /**< set intersection (226) */
  SETMINUS, /**< set subtraction (227) */
  SUBSET, /**< subset predicate; first parameter a subset of second (228) */
  MEMBER, /**< set membership predicate; first parameter a member of second (229) */
  SINGLETON, /**< the set of the single element given as a parameter (230) */
  INSERT, /**< set obtained by inserting elements (first N-1 parameters) into a set (the last parameter) (231) */
  CARD, /**< set cardinality operator (232) */
  COMPLEMENT, /**< set COMPLEMENT (with respect to finite universe) (233) */
  UNIVERSE_SET, /**< (finite) universe set, all set variables must be interpreted as subsets of it. (234) */
  COMPREHENSION, /**< set comprehension specified by a bound variable list, a predicate, and a term. (235) */
  CHOOSE, /**< return an element in the set given as a parameter (236) */
  JOIN, /**< set join (237) */
  PRODUCT, /**< set cartesian product (238) */
  TRANSPOSE, /**< set transpose (239) */
  TCLOSURE, /**< set transitive closure (240) */
  JOIN_IMAGE, /**< set join image (241) */
  IDEN, /**< set identity (242) */

  /* from strings */
  STRING_CONCAT, /**< string concat (N-ary) (243) */
  STRING_IN_REGEXP, /**< membership (244) */
  STRING_LENGTH, /**< string length (245) */
  STRING_SUBSTR, /**< string substr (246) */
  STRING_CHARAT, /**< string charat (247) */
  STRING_STRCTN, /**< string contains (248) */
  STRING_LT, /**< string less than (249) */
  STRING_LEQ, /**< string less than or equal (250) */
  STRING_STRIDOF, /**< string indexof (251) */
  STRING_STRREPL, /**< string replace (252) */
  STRING_STRREPLALL, /**< string replace all (253) */
  STRING_REPLACE_RE, /**< string replace regular expression match (254) */
  STRING_REPLACE_RE_ALL, /**< string replace all regular expression matches (255) */
  STRING_PREFIX, /**< string prefixof (256) */
  STRING_SUFFIX, /**< string suffixof (257) */
  STRING_IS_DIGIT, /**< string isdigit, returns true if argument is a string of length one that represents a digit (258) */
  STRING_ITOS, /**< integer to string (259) */
  STRING_STOI, /**< string to integer (total function) (260) */
  STRING_TO_CODE, /**< string to code, returns the code of the first character of the string if it has length one, -1 otherwise (261) */
  STRING_FROM_CODE, /**< string from code, returns a string containing a single character whose code point matches the argument to this function, empty string if the argument is out-of-bounds (262) */
  STRING_TOLOWER, /**< string to lowercase conversion (263) */
  STRING_TOUPPER, /**< string to uppercase conversion (264) */
  STRING_REV, /**< string reverse (265) */
  CONST_STRING, /**< a string of characters (266) */
  SEQUENCE_TYPE, /**< seuence type, takes as parameter the type of the elements (267) */
  CONST_SEQUENCE, /**< a sequence of characters (268) */
  SEQ_UNIT, /**< a sequence of length one (269) */
  STRING_TO_REGEXP, /**< convert string to regexp (270) */
  REGEXP_CONCAT, /**< regexp concat (271) */
  REGEXP_UNION, /**< regexp union (272) */
  REGEXP_INTER, /**< regexp intersection (273) */
  REGEXP_DIFF, /**< regexp difference (274) */
  REGEXP_STAR, /**< regexp * (275) */
  REGEXP_PLUS, /**< regexp + (276) */
  REGEXP_OPT, /**< regexp ? (277) */
  REGEXP_RANGE, /**< regexp range (278) */
  REGEXP_COMPLEMENT, /**< regexp complement (279) */
  REGEXP_EMPTY, /**< regexp empty (280) */
  REGEXP_SIGMA, /**< regexp all characters (281) */
  REGEXP_REPEAT_OP, /**< operator for regular expression repeat; payload is an instance of the CVC4::RegExpRepeat class (282) */
  REGEXP_REPEAT, /**< regular expression repeat; first parameter is a REGEXP_REPEAT_OP, second is a regular expression term (283) */
  REGEXP_LOOP_OP, /**< operator for regular expression loop; payload is an instance of the CVC4::RegExpLoop class (284) */
  REGEXP_LOOP, /**< regular expression loop; first parameter is a REGEXP_LOOP_OP, second is a regular expression term (285) */
  REGEXP_RV, /**< regexp rv (internal use only) (286) */

  /* from quantifiers */
  FORALL, /**< universally quantified formula; first parameter is an BOUND_VAR_LIST, second is quantifier body, and an optional third parameter is an INST_PATTERN_LIST (287) */
  EXISTS, /**< existentially quantified formula; first parameter is an BOUND_VAR_LIST, second is quantifier body, and an optional third parameter is an INST_PATTERN_LIST (288) */
  INST_CONSTANT, /**< instantiation constant (289) */
  BOUND_VAR_LIST, /**< a list of bound variables (used to bind variables under a quantifier) (290) */
  INST_PATTERN, /**< instantiation pattern (291) */
  INST_NO_PATTERN, /**< instantiation no-pattern (292) */
  INST_ATTRIBUTE, /**< instantiation attribute (293) */
  INST_PATTERN_LIST, /**< a list of instantiation patterns (294) */
  INST_CLOSURE, /**< predicate for specifying term in instantiation closure. (295) */

  LAST_KIND /**< marks the upper-bound of this enumeration */

};/* enum Kind_t */

}/* CVC4::kind namespace */

// import Kind into the "CVC4" namespace but keep the individual kind
// constants under kind::
typedef ::CVC4::kind::Kind_t Kind;

namespace kind {

/**
 * Converts an kind to a string. Note: This function is also used in
 * `safe_print()`. Changing this functions name or signature will result in
 * `safe_print()` printing "<unsupported>" instead of the proper strings for
 * the enum values.
 *
 * @param k The kind
 * @return The name of the kind
 */
const char* toString(CVC4::Kind k);

/**
 * Writes a kind name to a stream.
 *
 * @param out The stream to write to
 * @param k The kind to write to the stream
 * @return The stream
 */
std::ostream& operator<<(std::ostream&, CVC4::Kind) CVC4_PUBLIC;

/** Returns true if the given kind is associative. This is used by ExprManager to
 * decide whether it's safe to modify big expressions by changing the grouping of
 * the arguments. */
/* TODO: This could be generated. */
bool isAssociative(::CVC4::Kind k) CVC4_PUBLIC;
std::string kindToString(::CVC4::Kind k) CVC4_PUBLIC;

struct KindHashFunction {
  inline size_t operator()(::CVC4::Kind k) const {
    return k;
  }
};/* struct KindHashFunction */

}/* CVC4::kind namespace */

/**
 * The enumeration for the built-in atomic types.
 */
enum CVC4_PUBLIC TypeConstant
{
    BUILTIN_OPERATOR_TYPE, /**< the type for built-in operators */
  BOOLEAN_TYPE, /**< Boolean type */
  REAL_TYPE, /**< real type */
  INTEGER_TYPE, /**< integer type */
  ROUNDINGMODE_TYPE, /**< floating-point rounding mode */
  STRING_TYPE, /**< String type */
  REGEXP_TYPE, /**< RegExp type */
  BOUND_VAR_LIST_TYPE, /**< the type of bound variable lists */
  INST_PATTERN_TYPE, /**< instantiation pattern type */
  INST_PATTERN_LIST_TYPE, /**< the type of instantiation pattern lists */

  LAST_TYPE
}; /* enum TypeConstant */

/**
 * We hash the constants with their values.
 */
struct TypeConstantHashFunction {
  inline size_t operator()(TypeConstant tc) const {
    return tc;
  }
};/* struct TypeConstantHashFunction */

std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant);

namespace theory {

::CVC4::theory::TheoryId kindToTheoryId(::CVC4::Kind k) CVC4_PUBLIC;
::CVC4::theory::TheoryId typeConstantToTheoryId(
    ::CVC4::TypeConstant typeConstant) CVC4_PUBLIC;

}/* CVC4::theory namespace */
}/* CVC4 namespace */

#endif /* CVC4__KIND_H */