libcvc4-dev 1.5-1 / usr / include / cvc4 / expr / kind.h

/*********************                                                        */
/** kind.h
 **
 ** Copyright 2010-2014  New York University and The University of Iowa,
 ** and as below.
 **
 ** This header file automatically generated by:
 **
 **     ../../../../../src/expr/mkkind ../../../../../src/expr/kind_template.h ../../../../../src/theory/builtin/kinds ../../../../../src/theory/booleans/kinds ../../../../../src/theory/uf/kinds ../../../../../src/theory/arith/kinds ../../../../../src/theory/bv/kinds ../../../../../src/theory/fp/kinds ../../../../../src/theory/arrays/kinds ../../../../../src/theory/datatypes/kinds ../../../../../src/theory/sep/kinds ../../../../../src/theory/sets/kinds ../../../../../src/theory/strings/kinds ../../../../../src/theory/quantifiers/kinds ../../../../../src/theory/idl/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:                     */
/* ../../../../../src/expr/kind_template.h */

/*********************                                                        */
/*! \file kind_template.h
 ** \verbatim
 ** Top contributors (to current version):
 **   Morgan Deters, Dejan Jovanovic, Paul Meng
 ** This file is part of the CVC4 project.
 ** Copyright (c) 2009-2017 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/cvc4_public.h>

#ifndef __CVC4__KIND_H
#define __CVC4__KIND_H

#include <iosfwd>
#include <sstream>

#include <cvc4/base/exception.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) */
  FUNCTION, /**< a defined function (6) */
  APPLY, /**< application of a defined function (7) */
  EQUAL, /**< equality (two parameters only, sorts must match) (8) */
  DISTINCT, /**< disequality (N-ary, sorts must match) (9) */
  VARIABLE, /**< a variable (not permitted in bindings) (10) */
  BOUND_VARIABLE, /**< a bound variable (permitted in bindings and the associated lambda and quantifier bodies only) (11) */
  SKOLEM, /**< a Skolem variable (internal only) (12) */
  SEXPR, /**< a symbolic expression (any arity) (13) */
  LAMBDA, /**< a lambda expression; first parameter is a BOUND_VAR_LIST, second is lambda body (14) */
  CHAIN, /**< chained operator (N-ary), turned into a conjunction of binary applications of the operator on adjoining parameters; first parameter is a CHAIN_OP representing a binary operator, rest are arguments to that operator (15) */
  CHAIN_OP, /**< the chained operator; payload is an instance of the CVC4::Chain class (16) */
  TYPE_CONSTANT, /**< a representation for basic types (17) */
  FUNCTION_TYPE, /**< a function type (18) */
  SEXPR_TYPE, /**< the type of a symbolic expression (19) */
  SUBTYPE_TYPE, /**< predicate subtype; payload is an instance of the CVC4::Predicate class (20) */

  /* from booleans */
  CONST_BOOLEAN, /**< truth and falsity; payload is a (C++) bool (21) */
  NOT, /**< logical not (22) */
  AND, /**< logical and (N-ary) (23) */
  IMPLIES, /**< logical implication (exactly two parameters) (24) */
  OR, /**< logical or (N-ary) (25) */
  XOR, /**< exclusive or (exactly two parameters) (26) */
  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 (27) */

  /* from uf */
  APPLY_UF, /**< application of an uninterpreted function; first parameter is the function, remaining ones are parameters to that function (28) */
  BOOLEAN_TERM_VARIABLE, /**< Boolean term variable (29) */
  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 (30) */
  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 (31) */
  PARTIAL_APPLY_UF, /**< partial uninterpreted function application (32) */
  CARDINALITY_VALUE, /**< cardinality value of sort S: first parameter is (any) term of sort S (33) */

  /* from arith */
  PLUS, /**< arithmetic addition (N-ary) (34) */
  MULT, /**< arithmetic multiplication (N-ary) (35) */
  NONLINEAR_MULT, /**< synonym for MULT (36) */
  MINUS, /**< arithmetic binary subtraction operator (37) */
  UMINUS, /**< arithmetic unary negation (38) */
  DIVISION, /**< real division, division by 0 undefined (user symbol) (39) */
  DIVISION_TOTAL, /**< real division with interpreted division by 0 (internal symbol) (40) */
  INTS_DIVISION, /**< integer division, division by 0 undefined (user symbol) (41) */
  INTS_DIVISION_TOTAL, /**< integer division with interpreted division by 0 (internal symbol) (42) */
  INTS_MODULUS, /**< integer modulus, division by 0 undefined (user symbol) (43) */
  INTS_MODULUS_TOTAL, /**< integer modulus with interpreted division by 0 (internal symbol) (44) */
  ABS, /**< absolute value (45) */
  DIVISIBLE, /**< divisibility-by-k predicate; first parameter is a DIVISIBLE_OP, second is integer term (46) */
  POW, /**< arithmetic power (47) */
  DIVISIBLE_OP, /**< operator for the divisibility-by-k predicate; payload is an instance of the CVC4::Divisible class (48) */
  SUBRANGE_TYPE, /**< the type of an integer subrange (49) */
  CONST_RATIONAL, /**< a multiple-precision rational constant; payload is an instance of the CVC4::Rational class (50) */
  LT, /**< less than, x < y (51) */
  LEQ, /**< less than or equal, x <= y (52) */
  GT, /**< greater than, x > y (53) */
  GEQ, /**< greater than or equal, x >= y (54) */
  IS_INTEGER, /**< term-is-integer predicate (parameter is a real-sorted term) (55) */
  TO_INTEGER, /**< convert term to integer by the floor function (parameter is a real-sorted term) (56) */
  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) (57) */

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

  /* from fp */
  CONST_FLOATINGPOINT, /**< a floating-point literal (116) */
  CONST_ROUNDINGMODE, /**< a floating-point rounding mode (117) */
  FLOATINGPOINT_TYPE, /**< floating-point type (118) */
  FLOATINGPOINT_FP, /**< construct a floating-point literal from bit vectors (119) */
  FLOATINGPOINT_EQ, /**< floating-point equality (120) */
  FLOATINGPOINT_ABS, /**< floating-point absolute value (121) */
  FLOATINGPOINT_NEG, /**< floating-point negation (122) */
  FLOATINGPOINT_PLUS, /**< floating-point addition (123) */
  FLOATINGPOINT_SUB, /**< floating-point sutraction (124) */
  FLOATINGPOINT_MULT, /**< floating-point multiply (125) */
  FLOATINGPOINT_DIV, /**< floating-point division (126) */
  FLOATINGPOINT_FMA, /**< floating-point fused multiply and add (127) */
  FLOATINGPOINT_SQRT, /**< floating-point square root (128) */
  FLOATINGPOINT_REM, /**< floating-point remainder (129) */
  FLOATINGPOINT_RTI, /**< floating-point round to integral (130) */
  FLOATINGPOINT_MIN, /**< floating-point minimum (131) */
  FLOATINGPOINT_MAX, /**< floating-point maximum (132) */
  FLOATINGPOINT_LEQ, /**< floating-point less than or equal (133) */
  FLOATINGPOINT_LT, /**< floating-point less than (134) */
  FLOATINGPOINT_GEQ, /**< floating-point greater than or equal (135) */
  FLOATINGPOINT_GT, /**< floating-point greater than (136) */
  FLOATINGPOINT_ISN, /**< floating-point is normal (137) */
  FLOATINGPOINT_ISSN, /**< floating-point is sub-normal (138) */
  FLOATINGPOINT_ISZ, /**< floating-point is zero (139) */
  FLOATINGPOINT_ISINF, /**< floating-point is infinite (140) */
  FLOATINGPOINT_ISNAN, /**< floating-point is NaN (141) */
  FLOATINGPOINT_ISNEG, /**< floating-point is negative (142) */
  FLOATINGPOINT_ISPOS, /**< floating-point is positive (143) */
  FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP, /**< operator for to_fp from bit vector (144) */
  FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, /**< convert an IEEE-754 bit vector to floating-point (145) */
  FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP, /**< operator for to_fp from floating point (146) */
  FLOATINGPOINT_TO_FP_FLOATINGPOINT, /**< convert between floating-point sorts (147) */
  FLOATINGPOINT_TO_FP_REAL_OP, /**< operator for to_fp from real (148) */
  FLOATINGPOINT_TO_FP_REAL, /**< convert a real to floating-point (149) */
  FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP, /**< operator for to_fp from signed bit vector (150) */
  FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, /**< convert a signed bit vector to floating-point (151) */
  FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP, /**< operator for to_fp from unsigned bit vector (152) */
  FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, /**< convert an unsigned bit vector to floating-point (153) */
  FLOATINGPOINT_TO_FP_GENERIC_OP, /**< operator for a generic to_fp (154) */
  FLOATINGPOINT_TO_FP_GENERIC, /**< a generic conversion to floating-point, used in parsing only (155) */
  FLOATINGPOINT_TO_UBV_OP, /**< operator for to_ubv (156) */
  FLOATINGPOINT_TO_UBV, /**< convert a floating-point value to an unsigned bit vector (157) */
  FLOATINGPOINT_TO_SBV_OP, /**< operator for to_sbv (158) */
  FLOATINGPOINT_TO_SBV, /**< convert a floating-point value to a signed bit vector (159) */
  FLOATINGPOINT_TO_REAL, /**< floating-point to real (160) */

  /* from arrays */
  ARRAY_TYPE, /**< array type (161) */
  SELECT, /**< array select; first parameter is an array term, second is the selection index (162) */
  STORE, /**< array store; first parameter is an array term, second is the store index, third is the term to store at the index (163) */
  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) (164) */
  ARR_TABLE_FUN, /**< array table function (internal-only symbol) (165) */
  ARRAY_LAMBDA, /**< array lambda (internal-only symbol) (166) */
  PARTIAL_SELECT_0, /**< partial array select, for internal use only (167) */
  PARTIAL_SELECT_1, /**< partial array select, for internal use only (168) */

  /* from datatypes */
  CONSTRUCTOR_TYPE, /**< constructor (169) */
  SELECTOR_TYPE, /**< selector (170) */
  TESTER_TYPE, /**< tester (171) */
  APPLY_CONSTRUCTOR, /**< constructor application; first parameter is the constructor, remaining parameters (if any) are parameters to the constructor (172) */
  APPLY_SELECTOR, /**< selector application; parameter is a datatype term (undefined if mis-applied) (173) */
  APPLY_SELECTOR_TOTAL, /**< selector application; parameter is a datatype term (defined rigidly if mis-applied) (174) */
  APPLY_TESTER, /**< tester application; first parameter is a tester, second is a datatype term (175) */
  DATATYPE_TYPE, /**< a datatype type index (176) */
  PARAMETRIC_DATATYPE, /**< parametric datatype (177) */
  APPLY_TYPE_ASCRIPTION, /**< type ascription, for datatype constructor applications; first parameter is an ASCRIPTION_TYPE, second is the datatype constructor application being ascribed (178) */
  ASCRIPTION_TYPE, /**< a type parameter for type ascription; payload is an instance of the CVC4::AscriptionType class (179) */
  TUPLE_UPDATE_OP, /**< operator for a tuple update; payload is an instance of the CVC4::TupleUpdate class (180) */
  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 (181) */
  RECORD_UPDATE_OP, /**< operator for a record update; payload is an instance CVC4::RecordUpdate class (182) */
  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 (183) */
  DT_SIZE, /**< datatypes size (184) */
  DT_HEIGHT_BOUND, /**< datatypes height bound (185) */

  /* from sep */
  SEP_NIL, /**< separation nil (186) */
  SEP_EMP, /**< separation empty heap (187) */
  SEP_PTO, /**< points to relation (188) */
  SEP_STAR, /**< separation star (189) */
  SEP_WAND, /**< separation magic wand (190) */
  SEP_LABEL, /**< separation label (internal use only) (191) */

  /* from sets */
  EMPTYSET, /**< the empty set constant; payload is an instance of the CVC4::EmptySet class (192) */
  SET_TYPE, /**< set type, takes as parameter the type of the elements (193) */
  UNION, /**< set union (194) */
  INTERSECTION, /**< set intersection (195) */
  SETMINUS, /**< set subtraction (196) */
  SUBSET, /**< subset predicate; first parameter a subset of second (197) */
  MEMBER, /**< set membership predicate; first parameter a member of second (198) */
  SINGLETON, /**< the set of the single element given as a parameter (199) */
  INSERT, /**< set obtained by inserting elements (first N-1 parameters) into a set (the last parameter) (200) */
  CARD, /**< set cardinality operator (201) */
  COMPLEMENT, /**< set COMPLEMENT (with respect to finite universe) (202) */
  UNIVERSE_SET, /**< (finite) universe set, all set variables must be interpreted as subsets of it. (203) */
  JOIN, /**< set join (204) */
  PRODUCT, /**< set cartesian product (205) */
  TRANSPOSE, /**< set transpose (206) */
  TCLOSURE, /**< set transitive closure (207) */
  JOIN_IMAGE, /**< set join image (208) */
  IDEN, /**< set identity (209) */

  /* from strings */
  STRING_CONCAT, /**< string concat (N-ary) (210) */
  STRING_IN_REGEXP, /**< membership (211) */
  STRING_LENGTH, /**< string length (212) */
  STRING_SUBSTR, /**< string substr (213) */
  STRING_CHARAT, /**< string charat (214) */
  STRING_STRCTN, /**< string contains (215) */
  STRING_STRIDOF, /**< string indexof (216) */
  STRING_STRREPL, /**< string replace (217) */
  STRING_PREFIX, /**< string prefixof (218) */
  STRING_SUFFIX, /**< string suffixof (219) */
  STRING_ITOS, /**< integer to string (220) */
  STRING_STOI, /**< string to integer (total function) (221) */
  STRING_U16TOS, /**< uint16 to string (222) */
  STRING_STOU16, /**< string to uint16 (223) */
  STRING_U32TOS, /**< uint32 to string (224) */
  STRING_STOU32, /**< string to uint32 (225) */
  CONST_STRING, /**< a string of characters (226) */
  CONST_REGEXP, /**< a regular expression (227) */
  STRING_TO_REGEXP, /**< convert string to regexp (228) */
  REGEXP_CONCAT, /**< regexp concat (229) */
  REGEXP_UNION, /**< regexp union (230) */
  REGEXP_INTER, /**< regexp intersection (231) */
  REGEXP_STAR, /**< regexp * (232) */
  REGEXP_PLUS, /**< regexp + (233) */
  REGEXP_OPT, /**< regexp ? (234) */
  REGEXP_RANGE, /**< regexp range (235) */
  REGEXP_LOOP, /**< regexp loop (236) */
  REGEXP_EMPTY, /**< regexp empty (237) */
  REGEXP_SIGMA, /**< regexp all characters (238) */
  REGEXP_RV, /**< regexp rv (internal use only) (239) */

  /* 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 (240) */
  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 (241) */
  INST_CONSTANT, /**< instantiation constant (242) */
  BOUND_VAR_LIST, /**< a list of bound variables (used to bind variables under a quantifier) (243) */
  INST_PATTERN, /**< instantiation pattern (244) */
  INST_NO_PATTERN, /**< instantiation no-pattern (245) */
  INST_ATTRIBUTE, /**< instantiation attribute (246) */
  INST_PATTERN_LIST, /**< a list of instantiation patterns (247) */
  INST_CLOSURE, /**< predicate for specifying term in instantiation closure. (248) */
  REWRITE_RULE, /**< general rewrite rule (for rewrite-rules theory) (249) */
  RR_REWRITE, /**< actual rewrite rule (for rewrite-rules theory) (250) */
  RR_REDUCTION, /**< actual reduction rule (for rewrite-rules theory) (251) */
  RR_DEDUCTION, /**< actual deduction rule (for rewrite-rules theory) (252) */

  /* from idl */

  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 {

inline std::ostream& operator<<(std::ostream&, CVC4::Kind) CVC4_PUBLIC;
inline std::ostream& operator<<(std::ostream& out, CVC4::Kind k) {
  using namespace CVC4::kind;

  switch(k) {

  /* special cases */
  case UNDEFINED_KIND: out << "UNDEFINED_KIND"; break;
  case NULL_EXPR: out << "NULL"; break;

  /* from builtin */
  case SORT_TAG: out << "SORT_TAG"; break;
  case SORT_TYPE: out << "SORT_TYPE"; break;
  case UNINTERPRETED_CONSTANT: out << "UNINTERPRETED_CONSTANT"; break;
  case ABSTRACT_VALUE: out << "ABSTRACT_VALUE"; break;
  case BUILTIN: out << "BUILTIN"; break;
  case FUNCTION: out << "FUNCTION"; break;
  case APPLY: out << "APPLY"; break;
  case EQUAL: out << "EQUAL"; break;
  case DISTINCT: out << "DISTINCT"; break;
  case VARIABLE: out << "VARIABLE"; break;
  case BOUND_VARIABLE: out << "BOUND_VARIABLE"; break;
  case SKOLEM: out << "SKOLEM"; break;
  case SEXPR: out << "SEXPR"; break;
  case LAMBDA: out << "LAMBDA"; break;
  case CHAIN: out << "CHAIN"; break;
  case CHAIN_OP: out << "CHAIN_OP"; break;
  case TYPE_CONSTANT: out << "TYPE_CONSTANT"; break;
  case FUNCTION_TYPE: out << "FUNCTION_TYPE"; break;
  case SEXPR_TYPE: out << "SEXPR_TYPE"; break;
  case SUBTYPE_TYPE: out << "SUBTYPE_TYPE"; break;

  /* from booleans */
  case CONST_BOOLEAN: out << "CONST_BOOLEAN"; break;
  case NOT: out << "NOT"; break;
  case AND: out << "AND"; break;
  case IMPLIES: out << "IMPLIES"; break;
  case OR: out << "OR"; break;
  case XOR: out << "XOR"; break;
  case ITE: out << "ITE"; break;

  /* from uf */
  case APPLY_UF: out << "APPLY_UF"; break;
  case BOOLEAN_TERM_VARIABLE: out << "BOOLEAN_TERM_VARIABLE"; break;
  case CARDINALITY_CONSTRAINT: out << "CARDINALITY_CONSTRAINT"; break;
  case COMBINED_CARDINALITY_CONSTRAINT: out << "COMBINED_CARDINALITY_CONSTRAINT"; break;
  case PARTIAL_APPLY_UF: out << "PARTIAL_APPLY_UF"; break;
  case CARDINALITY_VALUE: out << "CARDINALITY_VALUE"; break;

  /* from arith */
  case PLUS: out << "PLUS"; break;
  case MULT: out << "MULT"; break;
  case NONLINEAR_MULT: out << "NONLINEAR_MULT"; break;
  case MINUS: out << "MINUS"; break;
  case UMINUS: out << "UMINUS"; break;
  case DIVISION: out << "DIVISION"; break;
  case DIVISION_TOTAL: out << "DIVISION_TOTAL"; break;
  case INTS_DIVISION: out << "INTS_DIVISION"; break;
  case INTS_DIVISION_TOTAL: out << "INTS_DIVISION_TOTAL"; break;
  case INTS_MODULUS: out << "INTS_MODULUS"; break;
  case INTS_MODULUS_TOTAL: out << "INTS_MODULUS_TOTAL"; break;
  case ABS: out << "ABS"; break;
  case DIVISIBLE: out << "DIVISIBLE"; break;
  case POW: out << "POW"; break;
  case DIVISIBLE_OP: out << "DIVISIBLE_OP"; break;
  case SUBRANGE_TYPE: out << "SUBRANGE_TYPE"; break;
  case CONST_RATIONAL: out << "CONST_RATIONAL"; break;
  case LT: out << "LT"; break;
  case LEQ: out << "LEQ"; break;
  case GT: out << "GT"; break;
  case GEQ: out << "GEQ"; break;
  case IS_INTEGER: out << "IS_INTEGER"; break;
  case TO_INTEGER: out << "TO_INTEGER"; break;
  case TO_REAL: out << "TO_REAL"; break;

  /* from bv */
  case BITVECTOR_TYPE: out << "BITVECTOR_TYPE"; break;
  case CONST_BITVECTOR: out << "CONST_BITVECTOR"; break;
  case BITVECTOR_CONCAT: out << "BITVECTOR_CONCAT"; break;
  case BITVECTOR_AND: out << "BITVECTOR_AND"; break;
  case BITVECTOR_OR: out << "BITVECTOR_OR"; break;
  case BITVECTOR_XOR: out << "BITVECTOR_XOR"; break;
  case BITVECTOR_NOT: out << "BITVECTOR_NOT"; break;
  case BITVECTOR_NAND: out << "BITVECTOR_NAND"; break;
  case BITVECTOR_NOR: out << "BITVECTOR_NOR"; break;
  case BITVECTOR_XNOR: out << "BITVECTOR_XNOR"; break;
  case BITVECTOR_COMP: out << "BITVECTOR_COMP"; break;
  case BITVECTOR_MULT: out << "BITVECTOR_MULT"; break;
  case BITVECTOR_PLUS: out << "BITVECTOR_PLUS"; break;
  case BITVECTOR_SUB: out << "BITVECTOR_SUB"; break;
  case BITVECTOR_NEG: out << "BITVECTOR_NEG"; break;
  case BITVECTOR_UDIV: out << "BITVECTOR_UDIV"; break;
  case BITVECTOR_UREM: out << "BITVECTOR_UREM"; break;
  case BITVECTOR_SDIV: out << "BITVECTOR_SDIV"; break;
  case BITVECTOR_SREM: out << "BITVECTOR_SREM"; break;
  case BITVECTOR_SMOD: out << "BITVECTOR_SMOD"; break;
  case BITVECTOR_UDIV_TOTAL: out << "BITVECTOR_UDIV_TOTAL"; break;
  case BITVECTOR_UREM_TOTAL: out << "BITVECTOR_UREM_TOTAL"; break;
  case BITVECTOR_SHL: out << "BITVECTOR_SHL"; break;
  case BITVECTOR_LSHR: out << "BITVECTOR_LSHR"; break;
  case BITVECTOR_ASHR: out << "BITVECTOR_ASHR"; break;
  case BITVECTOR_ULT: out << "BITVECTOR_ULT"; break;
  case BITVECTOR_ULE: out << "BITVECTOR_ULE"; break;
  case BITVECTOR_UGT: out << "BITVECTOR_UGT"; break;
  case BITVECTOR_UGE: out << "BITVECTOR_UGE"; break;
  case BITVECTOR_SLT: out << "BITVECTOR_SLT"; break;
  case BITVECTOR_SLE: out << "BITVECTOR_SLE"; break;
  case BITVECTOR_SGT: out << "BITVECTOR_SGT"; break;
  case BITVECTOR_SGE: out << "BITVECTOR_SGE"; break;
  case BITVECTOR_ULTBV: out << "BITVECTOR_ULTBV"; break;
  case BITVECTOR_SLTBV: out << "BITVECTOR_SLTBV"; break;
  case BITVECTOR_ITE: out << "BITVECTOR_ITE"; break;
  case BITVECTOR_REDOR: out << "BITVECTOR_REDOR"; break;
  case BITVECTOR_REDAND: out << "BITVECTOR_REDAND"; break;
  case BITVECTOR_EAGER_ATOM: out << "BITVECTOR_EAGER_ATOM"; break;
  case BITVECTOR_ACKERMANIZE_UDIV: out << "BITVECTOR_ACKERMANIZE_UDIV"; break;
  case BITVECTOR_ACKERMANIZE_UREM: out << "BITVECTOR_ACKERMANIZE_UREM"; break;
  case BITVECTOR_BITOF_OP: out << "BITVECTOR_BITOF_OP"; break;
  case BITVECTOR_EXTRACT_OP: out << "BITVECTOR_EXTRACT_OP"; break;
  case BITVECTOR_REPEAT_OP: out << "BITVECTOR_REPEAT_OP"; break;
  case BITVECTOR_ZERO_EXTEND_OP: out << "BITVECTOR_ZERO_EXTEND_OP"; break;
  case BITVECTOR_SIGN_EXTEND_OP: out << "BITVECTOR_SIGN_EXTEND_OP"; break;
  case BITVECTOR_ROTATE_LEFT_OP: out << "BITVECTOR_ROTATE_LEFT_OP"; break;
  case BITVECTOR_ROTATE_RIGHT_OP: out << "BITVECTOR_ROTATE_RIGHT_OP"; break;
  case BITVECTOR_BITOF: out << "BITVECTOR_BITOF"; break;
  case BITVECTOR_EXTRACT: out << "BITVECTOR_EXTRACT"; break;
  case BITVECTOR_REPEAT: out << "BITVECTOR_REPEAT"; break;
  case BITVECTOR_ZERO_EXTEND: out << "BITVECTOR_ZERO_EXTEND"; break;
  case BITVECTOR_SIGN_EXTEND: out << "BITVECTOR_SIGN_EXTEND"; break;
  case BITVECTOR_ROTATE_LEFT: out << "BITVECTOR_ROTATE_LEFT"; break;
  case BITVECTOR_ROTATE_RIGHT: out << "BITVECTOR_ROTATE_RIGHT"; break;
  case INT_TO_BITVECTOR_OP: out << "INT_TO_BITVECTOR_OP"; break;
  case INT_TO_BITVECTOR: out << "INT_TO_BITVECTOR"; break;
  case BITVECTOR_TO_NAT: out << "BITVECTOR_TO_NAT"; break;

  /* from fp */
  case CONST_FLOATINGPOINT: out << "CONST_FLOATINGPOINT"; break;
  case CONST_ROUNDINGMODE: out << "CONST_ROUNDINGMODE"; break;
  case FLOATINGPOINT_TYPE: out << "FLOATINGPOINT_TYPE"; break;
  case FLOATINGPOINT_FP: out << "FLOATINGPOINT_FP"; break;
  case FLOATINGPOINT_EQ: out << "FLOATINGPOINT_EQ"; break;
  case FLOATINGPOINT_ABS: out << "FLOATINGPOINT_ABS"; break;
  case FLOATINGPOINT_NEG: out << "FLOATINGPOINT_NEG"; break;
  case FLOATINGPOINT_PLUS: out << "FLOATINGPOINT_PLUS"; break;
  case FLOATINGPOINT_SUB: out << "FLOATINGPOINT_SUB"; break;
  case FLOATINGPOINT_MULT: out << "FLOATINGPOINT_MULT"; break;
  case FLOATINGPOINT_DIV: out << "FLOATINGPOINT_DIV"; break;
  case FLOATINGPOINT_FMA: out << "FLOATINGPOINT_FMA"; break;
  case FLOATINGPOINT_SQRT: out << "FLOATINGPOINT_SQRT"; break;
  case FLOATINGPOINT_REM: out << "FLOATINGPOINT_REM"; break;
  case FLOATINGPOINT_RTI: out << "FLOATINGPOINT_RTI"; break;
  case FLOATINGPOINT_MIN: out << "FLOATINGPOINT_MIN"; break;
  case FLOATINGPOINT_MAX: out << "FLOATINGPOINT_MAX"; break;
  case FLOATINGPOINT_LEQ: out << "FLOATINGPOINT_LEQ"; break;
  case FLOATINGPOINT_LT: out << "FLOATINGPOINT_LT"; break;
  case FLOATINGPOINT_GEQ: out << "FLOATINGPOINT_GEQ"; break;
  case FLOATINGPOINT_GT: out << "FLOATINGPOINT_GT"; break;
  case FLOATINGPOINT_ISN: out << "FLOATINGPOINT_ISN"; break;
  case FLOATINGPOINT_ISSN: out << "FLOATINGPOINT_ISSN"; break;
  case FLOATINGPOINT_ISZ: out << "FLOATINGPOINT_ISZ"; break;
  case FLOATINGPOINT_ISINF: out << "FLOATINGPOINT_ISINF"; break;
  case FLOATINGPOINT_ISNAN: out << "FLOATINGPOINT_ISNAN"; break;
  case FLOATINGPOINT_ISNEG: out << "FLOATINGPOINT_ISNEG"; break;
  case FLOATINGPOINT_ISPOS: out << "FLOATINGPOINT_ISPOS"; break;
  case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP: out << "FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP"; break;
  case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: out << "FLOATINGPOINT_TO_FP_IEEE_BITVECTOR"; break;
  case FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP: out << "FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP"; break;
  case FLOATINGPOINT_TO_FP_FLOATINGPOINT: out << "FLOATINGPOINT_TO_FP_FLOATINGPOINT"; break;
  case FLOATINGPOINT_TO_FP_REAL_OP: out << "FLOATINGPOINT_TO_FP_REAL_OP"; break;
  case FLOATINGPOINT_TO_FP_REAL: out << "FLOATINGPOINT_TO_FP_REAL"; break;
  case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP: out << "FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP"; break;
  case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: out << "FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR"; break;
  case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP: out << "FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP"; break;
  case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: out << "FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR"; break;
  case FLOATINGPOINT_TO_FP_GENERIC_OP: out << "FLOATINGPOINT_TO_FP_GENERIC_OP"; break;
  case FLOATINGPOINT_TO_FP_GENERIC: out << "FLOATINGPOINT_TO_FP_GENERIC"; break;
  case FLOATINGPOINT_TO_UBV_OP: out << "FLOATINGPOINT_TO_UBV_OP"; break;
  case FLOATINGPOINT_TO_UBV: out << "FLOATINGPOINT_TO_UBV"; break;
  case FLOATINGPOINT_TO_SBV_OP: out << "FLOATINGPOINT_TO_SBV_OP"; break;
  case FLOATINGPOINT_TO_SBV: out << "FLOATINGPOINT_TO_SBV"; break;
  case FLOATINGPOINT_TO_REAL: out << "FLOATINGPOINT_TO_REAL"; break;

  /* from arrays */
  case ARRAY_TYPE: out << "ARRAY_TYPE"; break;
  case SELECT: out << "SELECT"; break;
  case STORE: out << "STORE"; break;
  case STORE_ALL: out << "STORE_ALL"; break;
  case ARR_TABLE_FUN: out << "ARR_TABLE_FUN"; break;
  case ARRAY_LAMBDA: out << "ARRAY_LAMBDA"; break;
  case PARTIAL_SELECT_0: out << "PARTIAL_SELECT_0"; break;
  case PARTIAL_SELECT_1: out << "PARTIAL_SELECT_1"; break;

  /* from datatypes */
  case CONSTRUCTOR_TYPE: out << "CONSTRUCTOR_TYPE"; break;
  case SELECTOR_TYPE: out << "SELECTOR_TYPE"; break;
  case TESTER_TYPE: out << "TESTER_TYPE"; break;
  case APPLY_CONSTRUCTOR: out << "APPLY_CONSTRUCTOR"; break;
  case APPLY_SELECTOR: out << "APPLY_SELECTOR"; break;
  case APPLY_SELECTOR_TOTAL: out << "APPLY_SELECTOR_TOTAL"; break;
  case APPLY_TESTER: out << "APPLY_TESTER"; break;
  case DATATYPE_TYPE: out << "DATATYPE_TYPE"; break;
  case PARAMETRIC_DATATYPE: out << "PARAMETRIC_DATATYPE"; break;
  case APPLY_TYPE_ASCRIPTION: out << "APPLY_TYPE_ASCRIPTION"; break;
  case ASCRIPTION_TYPE: out << "ASCRIPTION_TYPE"; break;
  case TUPLE_UPDATE_OP: out << "TUPLE_UPDATE_OP"; break;
  case TUPLE_UPDATE: out << "TUPLE_UPDATE"; break;
  case RECORD_UPDATE_OP: out << "RECORD_UPDATE_OP"; break;
  case RECORD_UPDATE: out << "RECORD_UPDATE"; break;
  case DT_SIZE: out << "DT_SIZE"; break;
  case DT_HEIGHT_BOUND: out << "DT_HEIGHT_BOUND"; break;

  /* from sep */
  case SEP_NIL: out << "SEP_NIL"; break;
  case SEP_EMP: out << "SEP_EMP"; break;
  case SEP_PTO: out << "SEP_PTO"; break;
  case SEP_STAR: out << "SEP_STAR"; break;
  case SEP_WAND: out << "SEP_WAND"; break;
  case SEP_LABEL: out << "SEP_LABEL"; break;

  /* from sets */
  case EMPTYSET: out << "EMPTYSET"; break;
  case SET_TYPE: out << "SET_TYPE"; break;
  case UNION: out << "UNION"; break;
  case INTERSECTION: out << "INTERSECTION"; break;
  case SETMINUS: out << "SETMINUS"; break;
  case SUBSET: out << "SUBSET"; break;
  case MEMBER: out << "MEMBER"; break;
  case SINGLETON: out << "SINGLETON"; break;
  case INSERT: out << "INSERT"; break;
  case CARD: out << "CARD"; break;
  case COMPLEMENT: out << "COMPLEMENT"; break;
  case UNIVERSE_SET: out << "UNIVERSE_SET"; break;
  case JOIN: out << "JOIN"; break;
  case PRODUCT: out << "PRODUCT"; break;
  case TRANSPOSE: out << "TRANSPOSE"; break;
  case TCLOSURE: out << "TCLOSURE"; break;
  case JOIN_IMAGE: out << "JOIN_IMAGE"; break;
  case IDEN: out << "IDEN"; break;

  /* from strings */
  case STRING_CONCAT: out << "STRING_CONCAT"; break;
  case STRING_IN_REGEXP: out << "STRING_IN_REGEXP"; break;
  case STRING_LENGTH: out << "STRING_LENGTH"; break;
  case STRING_SUBSTR: out << "STRING_SUBSTR"; break;
  case STRING_CHARAT: out << "STRING_CHARAT"; break;
  case STRING_STRCTN: out << "STRING_STRCTN"; break;
  case STRING_STRIDOF: out << "STRING_STRIDOF"; break;
  case STRING_STRREPL: out << "STRING_STRREPL"; break;
  case STRING_PREFIX: out << "STRING_PREFIX"; break;
  case STRING_SUFFIX: out << "STRING_SUFFIX"; break;
  case STRING_ITOS: out << "STRING_ITOS"; break;
  case STRING_STOI: out << "STRING_STOI"; break;
  case STRING_U16TOS: out << "STRING_U16TOS"; break;
  case STRING_STOU16: out << "STRING_STOU16"; break;
  case STRING_U32TOS: out << "STRING_U32TOS"; break;
  case STRING_STOU32: out << "STRING_STOU32"; break;
  case CONST_STRING: out << "CONST_STRING"; break;
  case CONST_REGEXP: out << "CONST_REGEXP"; break;
  case STRING_TO_REGEXP: out << "STRING_TO_REGEXP"; break;
  case REGEXP_CONCAT: out << "REGEXP_CONCAT"; break;
  case REGEXP_UNION: out << "REGEXP_UNION"; break;
  case REGEXP_INTER: out << "REGEXP_INTER"; break;
  case REGEXP_STAR: out << "REGEXP_STAR"; break;
  case REGEXP_PLUS: out << "REGEXP_PLUS"; break;
  case REGEXP_OPT: out << "REGEXP_OPT"; break;
  case REGEXP_RANGE: out << "REGEXP_RANGE"; break;
  case REGEXP_LOOP: out << "REGEXP_LOOP"; break;
  case REGEXP_EMPTY: out << "REGEXP_EMPTY"; break;
  case REGEXP_SIGMA: out << "REGEXP_SIGMA"; break;
  case REGEXP_RV: out << "REGEXP_RV"; break;

  /* from quantifiers */
  case FORALL: out << "FORALL"; break;
  case EXISTS: out << "EXISTS"; break;
  case INST_CONSTANT: out << "INST_CONSTANT"; break;
  case BOUND_VAR_LIST: out << "BOUND_VAR_LIST"; break;
  case INST_PATTERN: out << "INST_PATTERN"; break;
  case INST_NO_PATTERN: out << "INST_NO_PATTERN"; break;
  case INST_ATTRIBUTE: out << "INST_ATTRIBUTE"; break;
  case INST_PATTERN_LIST: out << "INST_PATTERN_LIST"; break;
  case INST_CLOSURE: out << "INST_CLOSURE"; break;
  case REWRITE_RULE: out << "REWRITE_RULE"; break;
  case RR_REWRITE: out << "RR_REWRITE"; break;
  case RR_REDUCTION: out << "RR_REDUCTION"; break;
  case RR_DEDUCTION: out << "RR_DEDUCTION"; break;

  /* from idl */

  case LAST_KIND: out << "LAST_KIND"; break;
  default: out << "UNKNOWNKIND!" << int(k); break;
  }

  return out;
}

#line 64 "../../../../../src/expr/kind_template.h"

/** 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. */
inline bool isAssociative(::CVC4::Kind k) {
  switch(k) {
  case kind::AND:
  case kind::OR:
  case kind::MULT:
  case kind::PLUS:
    return true;

  default:
    return false;
  }
}

inline std::string kindToString(::CVC4::Kind k) {
  std::stringstream ss;
  ss << k;
  return ss.str();
}

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 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 */
  RRHB_TYPE, /**< head and body of the rule type (for rewrite-rules theory) */

#line 102 "../../../../../src/expr/kind_template.h"
  LAST_TYPE
};/* enum TypeConstant */

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

inline std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) {
  switch(typeConstant) {
  case BUILTIN_OPERATOR_TYPE:  out << "the type for built-in operators"; break;
  case BOOLEAN_TYPE:  out << "Boolean type"; break;
  case REAL_TYPE:  out << "real type"; break;
  case INTEGER_TYPE:  out << "integer type"; break;
  case ROUNDINGMODE_TYPE:  out << "floating-point rounding mode"; break;
  case STRING_TYPE:  out << "String type"; break;
  case REGEXP_TYPE:  out << "RegExp type"; break;
  case BOUND_VAR_LIST_TYPE:  out << "the type of bound variable lists"; break;
  case INST_PATTERN_TYPE:  out << "instantiation pattern type"; break;
  case INST_PATTERN_LIST_TYPE:  out << "the type of instantiation pattern lists"; break;
  case RRHB_TYPE:  out << "head and body of the rule type (for rewrite-rules theory)"; break;

#line 118 "../../../../../src/expr/kind_template.h"
  default:
    out << "UNKNOWN_TYPE_CONSTANT";
    break;
  }
  return out;
}

namespace theory {

enum TheoryId {
  THEORY_BUILTIN,
  THEORY_BOOL,
  THEORY_UF,
  THEORY_ARITH,
  THEORY_BV,
  THEORY_FP,
  THEORY_ARRAY,
  THEORY_DATATYPES,
  THEORY_SEP,
  THEORY_SETS,
  THEORY_STRINGS,
  THEORY_QUANTIFIERS,

#line 130 "../../../../../src/expr/kind_template.h"
  THEORY_LAST
};/* enum TheoryId */

const TheoryId THEORY_FIRST = static_cast<TheoryId>(0);
const TheoryId THEORY_SAT_SOLVER = THEORY_LAST;

inline TheoryId& operator ++ (TheoryId& id) {
  return id = static_cast<TheoryId>(((int)id) + 1);
}

inline std::ostream& operator<<(std::ostream& out, TheoryId theoryId) {
  switch(theoryId) {
  case THEORY_BUILTIN: out << "THEORY_BUILTIN"; break;
  case THEORY_BOOL: out << "THEORY_BOOL"; break;
  case THEORY_UF: out << "THEORY_UF"; break;
  case THEORY_ARITH: out << "THEORY_ARITH"; break;
  case THEORY_BV: out << "THEORY_BV"; break;
  case THEORY_FP: out << "THEORY_FP"; break;
  case THEORY_ARRAY: out << "THEORY_ARRAY"; break;
  case THEORY_DATATYPES: out << "THEORY_DATATYPES"; break;
  case THEORY_SEP: out << "THEORY_SEP"; break;
  case THEORY_SETS: out << "THEORY_SETS"; break;
  case THEORY_STRINGS: out << "THEORY_STRINGS"; break;
  case THEORY_QUANTIFIERS: out << "THEORY_QUANTIFIERS"; break;

#line 144 "../../../../../src/expr/kind_template.h"
  default:
    out << "UNKNOWN_THEORY";
    break;
  }
  return out;
}

inline TheoryId kindToTheoryId(::CVC4::Kind k) {
  switch(k) {
  case kind::UNDEFINED_KIND:
  case kind::NULL_EXPR:
    break;
  case kind::SORT_TAG: return THEORY_BUILTIN;
  case kind::SORT_TYPE: return THEORY_BUILTIN;
  case kind::UNINTERPRETED_CONSTANT: return THEORY_BUILTIN;
  case kind::ABSTRACT_VALUE: return THEORY_BUILTIN;
  case kind::BUILTIN: return THEORY_BUILTIN;
  case kind::FUNCTION: return THEORY_BUILTIN;
  case kind::APPLY: return THEORY_BUILTIN;
  case kind::EQUAL: return THEORY_BUILTIN;
  case kind::DISTINCT: return THEORY_BUILTIN;
  case kind::VARIABLE: return THEORY_BUILTIN;
  case kind::BOUND_VARIABLE: return THEORY_BUILTIN;
  case kind::SKOLEM: return THEORY_BUILTIN;
  case kind::SEXPR: return THEORY_BUILTIN;
  case kind::LAMBDA: return THEORY_BUILTIN;
  case kind::CHAIN: return THEORY_BUILTIN;
  case kind::CHAIN_OP: return THEORY_BUILTIN;
  case kind::TYPE_CONSTANT: return THEORY_BUILTIN;
  case kind::FUNCTION_TYPE: return THEORY_BUILTIN;
  case kind::SEXPR_TYPE: return THEORY_BUILTIN;
  case kind::SUBTYPE_TYPE: return THEORY_BUILTIN;
  case kind::CONST_BOOLEAN: return THEORY_BOOL;
  case kind::NOT: return THEORY_BOOL;
  case kind::AND: return THEORY_BOOL;
  case kind::IMPLIES: return THEORY_BOOL;
  case kind::OR: return THEORY_BOOL;
  case kind::XOR: return THEORY_BOOL;
  case kind::ITE: return THEORY_BOOL;
  case kind::APPLY_UF: return THEORY_UF;
  case kind::BOOLEAN_TERM_VARIABLE: return THEORY_UF;
  case kind::CARDINALITY_CONSTRAINT: return THEORY_UF;
  case kind::COMBINED_CARDINALITY_CONSTRAINT: return THEORY_UF;
  case kind::PARTIAL_APPLY_UF: return THEORY_UF;
  case kind::CARDINALITY_VALUE: return THEORY_UF;
  case kind::PLUS: return THEORY_ARITH;
  case kind::MULT: return THEORY_ARITH;
  case kind::NONLINEAR_MULT: return THEORY_ARITH;
  case kind::MINUS: return THEORY_ARITH;
  case kind::UMINUS: return THEORY_ARITH;
  case kind::DIVISION: return THEORY_ARITH;
  case kind::DIVISION_TOTAL: return THEORY_ARITH;
  case kind::INTS_DIVISION: return THEORY_ARITH;
  case kind::INTS_DIVISION_TOTAL: return THEORY_ARITH;
  case kind::INTS_MODULUS: return THEORY_ARITH;
  case kind::INTS_MODULUS_TOTAL: return THEORY_ARITH;
  case kind::ABS: return THEORY_ARITH;
  case kind::DIVISIBLE: return THEORY_ARITH;
  case kind::POW: return THEORY_ARITH;
  case kind::DIVISIBLE_OP: return THEORY_ARITH;
  case kind::SUBRANGE_TYPE: return THEORY_ARITH;
  case kind::CONST_RATIONAL: return THEORY_ARITH;
  case kind::LT: return THEORY_ARITH;
  case kind::LEQ: return THEORY_ARITH;
  case kind::GT: return THEORY_ARITH;
  case kind::GEQ: return THEORY_ARITH;
  case kind::IS_INTEGER: return THEORY_ARITH;
  case kind::TO_INTEGER: return THEORY_ARITH;
  case kind::TO_REAL: return THEORY_ARITH;
  case kind::BITVECTOR_TYPE: return THEORY_BV;
  case kind::CONST_BITVECTOR: return THEORY_BV;
  case kind::BITVECTOR_CONCAT: return THEORY_BV;
  case kind::BITVECTOR_AND: return THEORY_BV;
  case kind::BITVECTOR_OR: return THEORY_BV;
  case kind::BITVECTOR_XOR: return THEORY_BV;
  case kind::BITVECTOR_NOT: return THEORY_BV;
  case kind::BITVECTOR_NAND: return THEORY_BV;
  case kind::BITVECTOR_NOR: return THEORY_BV;
  case kind::BITVECTOR_XNOR: return THEORY_BV;
  case kind::BITVECTOR_COMP: return THEORY_BV;
  case kind::BITVECTOR_MULT: return THEORY_BV;
  case kind::BITVECTOR_PLUS: return THEORY_BV;
  case kind::BITVECTOR_SUB: return THEORY_BV;
  case kind::BITVECTOR_NEG: return THEORY_BV;
  case kind::BITVECTOR_UDIV: return THEORY_BV;
  case kind::BITVECTOR_UREM: return THEORY_BV;
  case kind::BITVECTOR_SDIV: return THEORY_BV;
  case kind::BITVECTOR_SREM: return THEORY_BV;
  case kind::BITVECTOR_SMOD: return THEORY_BV;
  case kind::BITVECTOR_UDIV_TOTAL: return THEORY_BV;
  case kind::BITVECTOR_UREM_TOTAL: return THEORY_BV;
  case kind::BITVECTOR_SHL: return THEORY_BV;
  case kind::BITVECTOR_LSHR: return THEORY_BV;
  case kind::BITVECTOR_ASHR: return THEORY_BV;
  case kind::BITVECTOR_ULT: return THEORY_BV;
  case kind::BITVECTOR_ULE: return THEORY_BV;
  case kind::BITVECTOR_UGT: return THEORY_BV;
  case kind::BITVECTOR_UGE: return THEORY_BV;
  case kind::BITVECTOR_SLT: return THEORY_BV;
  case kind::BITVECTOR_SLE: return THEORY_BV;
  case kind::BITVECTOR_SGT: return THEORY_BV;
  case kind::BITVECTOR_SGE: return THEORY_BV;
  case kind::BITVECTOR_ULTBV: return THEORY_BV;
  case kind::BITVECTOR_SLTBV: return THEORY_BV;
  case kind::BITVECTOR_ITE: return THEORY_BV;
  case kind::BITVECTOR_REDOR: return THEORY_BV;
  case kind::BITVECTOR_REDAND: return THEORY_BV;
  case kind::BITVECTOR_EAGER_ATOM: return THEORY_BV;
  case kind::BITVECTOR_ACKERMANIZE_UDIV: return THEORY_BV;
  case kind::BITVECTOR_ACKERMANIZE_UREM: return THEORY_BV;
  case kind::BITVECTOR_BITOF_OP: return THEORY_BV;
  case kind::BITVECTOR_EXTRACT_OP: return THEORY_BV;
  case kind::BITVECTOR_REPEAT_OP: return THEORY_BV;
  case kind::BITVECTOR_ZERO_EXTEND_OP: return THEORY_BV;
  case kind::BITVECTOR_SIGN_EXTEND_OP: return THEORY_BV;
  case kind::BITVECTOR_ROTATE_LEFT_OP: return THEORY_BV;
  case kind::BITVECTOR_ROTATE_RIGHT_OP: return THEORY_BV;
  case kind::BITVECTOR_BITOF: return THEORY_BV;
  case kind::BITVECTOR_EXTRACT: return THEORY_BV;
  case kind::BITVECTOR_REPEAT: return THEORY_BV;
  case kind::BITVECTOR_ZERO_EXTEND: return THEORY_BV;
  case kind::BITVECTOR_SIGN_EXTEND: return THEORY_BV;
  case kind::BITVECTOR_ROTATE_LEFT: return THEORY_BV;
  case kind::BITVECTOR_ROTATE_RIGHT: return THEORY_BV;
  case kind::INT_TO_BITVECTOR_OP: return THEORY_BV;
  case kind::INT_TO_BITVECTOR: return THEORY_BV;
  case kind::BITVECTOR_TO_NAT: return THEORY_BV;
  case kind::CONST_FLOATINGPOINT: return THEORY_FP;
  case kind::CONST_ROUNDINGMODE: return THEORY_FP;
  case kind::FLOATINGPOINT_TYPE: return THEORY_FP;
  case kind::FLOATINGPOINT_FP: return THEORY_FP;
  case kind::FLOATINGPOINT_EQ: return THEORY_FP;
  case kind::FLOATINGPOINT_ABS: return THEORY_FP;
  case kind::FLOATINGPOINT_NEG: return THEORY_FP;
  case kind::FLOATINGPOINT_PLUS: return THEORY_FP;
  case kind::FLOATINGPOINT_SUB: return THEORY_FP;
  case kind::FLOATINGPOINT_MULT: return THEORY_FP;
  case kind::FLOATINGPOINT_DIV: return THEORY_FP;
  case kind::FLOATINGPOINT_FMA: return THEORY_FP;
  case kind::FLOATINGPOINT_SQRT: return THEORY_FP;
  case kind::FLOATINGPOINT_REM: return THEORY_FP;
  case kind::FLOATINGPOINT_RTI: return THEORY_FP;
  case kind::FLOATINGPOINT_MIN: return THEORY_FP;
  case kind::FLOATINGPOINT_MAX: return THEORY_FP;
  case kind::FLOATINGPOINT_LEQ: return THEORY_FP;
  case kind::FLOATINGPOINT_LT: return THEORY_FP;
  case kind::FLOATINGPOINT_GEQ: return THEORY_FP;
  case kind::FLOATINGPOINT_GT: return THEORY_FP;
  case kind::FLOATINGPOINT_ISN: return THEORY_FP;
  case kind::FLOATINGPOINT_ISSN: return THEORY_FP;
  case kind::FLOATINGPOINT_ISZ: return THEORY_FP;
  case kind::FLOATINGPOINT_ISINF: return THEORY_FP;
  case kind::FLOATINGPOINT_ISNAN: return THEORY_FP;
  case kind::FLOATINGPOINT_ISNEG: return THEORY_FP;
  case kind::FLOATINGPOINT_ISPOS: return THEORY_FP;
  case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP: return THEORY_FP;
  case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: return THEORY_FP;
  case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP: return THEORY_FP;
  case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT: return THEORY_FP;
  case kind::FLOATINGPOINT_TO_FP_REAL_OP: return THEORY_FP;
  case kind::FLOATINGPOINT_TO_FP_REAL: return THEORY_FP;
  case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP: return THEORY_FP;
  case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: return THEORY_FP;
  case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP: return THEORY_FP;
  case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: return THEORY_FP;
  case kind::FLOATINGPOINT_TO_FP_GENERIC_OP: return THEORY_FP;
  case kind::FLOATINGPOINT_TO_FP_GENERIC: return THEORY_FP;
  case kind::FLOATINGPOINT_TO_UBV_OP: return THEORY_FP;
  case kind::FLOATINGPOINT_TO_UBV: return THEORY_FP;
  case kind::FLOATINGPOINT_TO_SBV_OP: return THEORY_FP;
  case kind::FLOATINGPOINT_TO_SBV: return THEORY_FP;
  case kind::FLOATINGPOINT_TO_REAL: return THEORY_FP;
  case kind::ARRAY_TYPE: return THEORY_ARRAY;
  case kind::SELECT: return THEORY_ARRAY;
  case kind::STORE: return THEORY_ARRAY;
  case kind::STORE_ALL: return THEORY_ARRAY;
  case kind::ARR_TABLE_FUN: return THEORY_ARRAY;
  case kind::ARRAY_LAMBDA: return THEORY_ARRAY;
  case kind::PARTIAL_SELECT_0: return THEORY_ARRAY;
  case kind::PARTIAL_SELECT_1: return THEORY_ARRAY;
  case kind::CONSTRUCTOR_TYPE: return THEORY_DATATYPES;
  case kind::SELECTOR_TYPE: return THEORY_DATATYPES;
  case kind::TESTER_TYPE: return THEORY_DATATYPES;
  case kind::APPLY_CONSTRUCTOR: return THEORY_DATATYPES;
  case kind::APPLY_SELECTOR: return THEORY_DATATYPES;
  case kind::APPLY_SELECTOR_TOTAL: return THEORY_DATATYPES;
  case kind::APPLY_TESTER: return THEORY_DATATYPES;
  case kind::DATATYPE_TYPE: return THEORY_DATATYPES;
  case kind::PARAMETRIC_DATATYPE: return THEORY_DATATYPES;
  case kind::APPLY_TYPE_ASCRIPTION: return THEORY_DATATYPES;
  case kind::ASCRIPTION_TYPE: return THEORY_DATATYPES;
  case kind::TUPLE_UPDATE_OP: return THEORY_DATATYPES;
  case kind::TUPLE_UPDATE: return THEORY_DATATYPES;
  case kind::RECORD_UPDATE_OP: return THEORY_DATATYPES;
  case kind::RECORD_UPDATE: return THEORY_DATATYPES;
  case kind::DT_SIZE: return THEORY_DATATYPES;
  case kind::DT_HEIGHT_BOUND: return THEORY_DATATYPES;
  case kind::SEP_NIL: return THEORY_SEP;
  case kind::SEP_EMP: return THEORY_SEP;
  case kind::SEP_PTO: return THEORY_SEP;
  case kind::SEP_STAR: return THEORY_SEP;
  case kind::SEP_WAND: return THEORY_SEP;
  case kind::SEP_LABEL: return THEORY_SEP;
  case kind::EMPTYSET: return THEORY_SETS;
  case kind::SET_TYPE: return THEORY_SETS;
  case kind::UNION: return THEORY_SETS;
  case kind::INTERSECTION: return THEORY_SETS;
  case kind::SETMINUS: return THEORY_SETS;
  case kind::SUBSET: return THEORY_SETS;
  case kind::MEMBER: return THEORY_SETS;
  case kind::SINGLETON: return THEORY_SETS;
  case kind::INSERT: return THEORY_SETS;
  case kind::CARD: return THEORY_SETS;
  case kind::COMPLEMENT: return THEORY_SETS;
  case kind::UNIVERSE_SET: return THEORY_SETS;
  case kind::JOIN: return THEORY_SETS;
  case kind::PRODUCT: return THEORY_SETS;
  case kind::TRANSPOSE: return THEORY_SETS;
  case kind::TCLOSURE: return THEORY_SETS;
  case kind::JOIN_IMAGE: return THEORY_SETS;
  case kind::IDEN: return THEORY_SETS;
  case kind::STRING_CONCAT: return THEORY_STRINGS;
  case kind::STRING_IN_REGEXP: return THEORY_STRINGS;
  case kind::STRING_LENGTH: return THEORY_STRINGS;
  case kind::STRING_SUBSTR: return THEORY_STRINGS;
  case kind::STRING_CHARAT: return THEORY_STRINGS;
  case kind::STRING_STRCTN: return THEORY_STRINGS;
  case kind::STRING_STRIDOF: return THEORY_STRINGS;
  case kind::STRING_STRREPL: return THEORY_STRINGS;
  case kind::STRING_PREFIX: return THEORY_STRINGS;
  case kind::STRING_SUFFIX: return THEORY_STRINGS;
  case kind::STRING_ITOS: return THEORY_STRINGS;
  case kind::STRING_STOI: return THEORY_STRINGS;
  case kind::STRING_U16TOS: return THEORY_STRINGS;
  case kind::STRING_STOU16: return THEORY_STRINGS;
  case kind::STRING_U32TOS: return THEORY_STRINGS;
  case kind::STRING_STOU32: return THEORY_STRINGS;
  case kind::CONST_STRING: return THEORY_STRINGS;
  case kind::CONST_REGEXP: return THEORY_STRINGS;
  case kind::STRING_TO_REGEXP: return THEORY_STRINGS;
  case kind::REGEXP_CONCAT: return THEORY_STRINGS;
  case kind::REGEXP_UNION: return THEORY_STRINGS;
  case kind::REGEXP_INTER: return THEORY_STRINGS;
  case kind::REGEXP_STAR: return THEORY_STRINGS;
  case kind::REGEXP_PLUS: return THEORY_STRINGS;
  case kind::REGEXP_OPT: return THEORY_STRINGS;
  case kind::REGEXP_RANGE: return THEORY_STRINGS;
  case kind::REGEXP_LOOP: return THEORY_STRINGS;
  case kind::REGEXP_EMPTY: return THEORY_STRINGS;
  case kind::REGEXP_SIGMA: return THEORY_STRINGS;
  case kind::REGEXP_RV: return THEORY_STRINGS;
  case kind::FORALL: return THEORY_QUANTIFIERS;
  case kind::EXISTS: return THEORY_QUANTIFIERS;
  case kind::INST_CONSTANT: return THEORY_QUANTIFIERS;
  case kind::BOUND_VAR_LIST: return THEORY_QUANTIFIERS;
  case kind::INST_PATTERN: return THEORY_QUANTIFIERS;
  case kind::INST_NO_PATTERN: return THEORY_QUANTIFIERS;
  case kind::INST_ATTRIBUTE: return THEORY_QUANTIFIERS;
  case kind::INST_PATTERN_LIST: return THEORY_QUANTIFIERS;
  case kind::INST_CLOSURE: return THEORY_QUANTIFIERS;
  case kind::REWRITE_RULE: return THEORY_QUANTIFIERS;
  case kind::RR_REWRITE: return THEORY_QUANTIFIERS;
  case kind::RR_REDUCTION: return THEORY_QUANTIFIERS;
  case kind::RR_DEDUCTION: return THEORY_QUANTIFIERS;

#line 158 "../../../../../src/expr/kind_template.h"
  case kind::LAST_KIND:
    break;
  }
  throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad kind");
}

inline TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant) {
  switch(typeConstant) {
  case BUILTIN_OPERATOR_TYPE: return THEORY_BUILTIN;
  case BOOLEAN_TYPE: return THEORY_BOOL;
  case REAL_TYPE: return THEORY_ARITH;
  case INTEGER_TYPE: return THEORY_ARITH;
  case ROUNDINGMODE_TYPE: return THEORY_FP;
  case STRING_TYPE: return THEORY_STRINGS;
  case REGEXP_TYPE: return THEORY_STRINGS;
  case BOUND_VAR_LIST_TYPE: return THEORY_QUANTIFIERS;
  case INST_PATTERN_TYPE: return THEORY_QUANTIFIERS;
  case INST_PATTERN_LIST_TYPE: return THEORY_QUANTIFIERS;
  case RRHB_TYPE: return THEORY_QUANTIFIERS;

#line 168 "../../../../../src/expr/kind_template.h"
  case LAST_TYPE:
    break;
  }
  throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad type constant");
}

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

#endif /* __CVC4__KIND_H */