GCC Code Coverage Report
Directory: . Exec Total Coverage
File: build-coverage/src/expr/kind.h Lines: 4 4 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/** kind.h
3
 **
4
 ** Copyright 2010-2014  New York University and The University of Iowa,
5
 ** and as below.
6
 **
7
 ** This header file automatically generated by:
8
 **
9
 **     ../../../src/expr/mkkind /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/expr/kind_template.h /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/builtin/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/booleans/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/uf/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/arith/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/bv/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/fp/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/arrays/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/datatypes/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/sep/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/sets/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/bags/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/strings/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/theory/quantifiers/kinds
10
 **
11
 ** for the CVC4 project.
12
 **/
13
14
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
15
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
16
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
17
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
18
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
19
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
20
21
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
22
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
23
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
24
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
25
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
26
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
27
28
/* Edit the template file instead:                     */
29
/* /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/expr/kind_template.h */
30
31
/*********************                                                        */
32
/*! \file kind_template.h
33
 ** \verbatim
34
 ** Top contributors (to current version):
35
 **   Andres Noetzli, Morgan Deters, Dejan Jovanovic
36
 ** This file is part of the CVC4 project.
37
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
38
 ** in the top-level source directory and their institutional affiliations.
39
 ** All rights reserved.  See the file COPYING in the top-level source
40
 ** directory for licensing information.\endverbatim
41
 **
42
 ** \brief Template for the Node kind header
43
 **
44
 ** Template for the Node kind header.
45
 **/
46
47
#include "cvc4_public.h"
48
49
#ifndef CVC4__KIND_H
50
#define CVC4__KIND_H
51
52
#include <iosfwd>
53
54
#include "base/exception.h"
55
#include "theory/theory_id.h"
56
57
namespace CVC4 {
58
namespace kind {
59
60
enum Kind_t
61
{
62
  UNDEFINED_KIND = -1,    /**< undefined */
63
  NULL_EXPR,              /**< Null kind */
64
65
  /* from builtin */
66
  SORT_TAG, /**< sort tag (1) */
67
  SORT_TYPE, /**< specifies types of user-declared 'uninterpreted' sorts (2) */
68
  UNINTERPRETED_CONSTANT, /**< the kind of expressions representing uninterpreted constants; payload is an instance of the CVC4::UninterpretedConstant class (used in models) (3) */
69
  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) */
70
  BUILTIN, /**< the kind of expressions representing built-in operators (5) */
71
  EQUAL, /**< equality (two parameters only, sorts must match) (6) */
72
  DISTINCT, /**< disequality (N-ary, sorts must match) (7) */
73
  VARIABLE, /**< a variable (not permitted in bindings) (8) */
74
  BOUND_VARIABLE, /**< a bound variable (permitted in bindings and the associated lambda and quantifier bodies only) (9) */
75
  SKOLEM, /**< a Skolem variable (internal only) (10) */
76
  SEXPR, /**< a symbolic expression (any arity) (11) */
77
  LAMBDA, /**< a lambda expression; first parameter is a BOUND_VAR_LIST, second is lambda body (12) */
78
  WITNESS, /**< a witness expression; first parameter is a BOUND_VAR_LIST, second is the witness body (13) */
79
  TYPE_CONSTANT, /**< a representation for basic types (14) */
80
  FUNCTION_TYPE, /**< a function type (15) */
81
  SEXPR_TYPE, /**< the type of a symbolic expression (16) */
82
83
  /* from booleans */
84
  CONST_BOOLEAN, /**< truth and falsity; payload is a (C++) bool (17) */
85
  NOT, /**< logical not (18) */
86
  AND, /**< logical and (N-ary) (19) */
87
  IMPLIES, /**< logical implication (exactly two parameters) (20) */
88
  OR, /**< logical or (N-ary) (21) */
89
  XOR, /**< exclusive or (exactly two parameters) (22) */
90
  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) */
91
92
  /* from uf */
93
  APPLY_UF, /**< application of an uninterpreted function; first parameter is the function, remaining ones are parameters to that function (24) */
94
  BOOLEAN_TERM_VARIABLE, /**< Boolean term variable (25) */
95
  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) */
96
  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) */
97
  PARTIAL_APPLY_UF, /**< partial uninterpreted function application (28) */
98
  CARDINALITY_VALUE, /**< cardinality value of sort S: first parameter is (any) term of sort S (29) */
99
  HO_APPLY, /**< higher-order (partial) function application (30) */
100
101
  /* from arith */
102
  PLUS, /**< arithmetic addition (N-ary) (31) */
103
  MULT, /**< arithmetic multiplication (N-ary) (32) */
104
  NONLINEAR_MULT, /**< synonym for MULT (33) */
105
  MINUS, /**< arithmetic binary subtraction operator (34) */
106
  UMINUS, /**< arithmetic unary negation (35) */
107
  DIVISION, /**< real division, division by 0 undefined (user symbol) (36) */
108
  DIVISION_TOTAL, /**< real division with interpreted division by 0 (internal symbol) (37) */
109
  INTS_DIVISION, /**< integer division, division by 0 undefined (user symbol) (38) */
110
  INTS_DIVISION_TOTAL, /**< integer division with interpreted division by 0 (internal symbol) (39) */
111
  INTS_MODULUS, /**< integer modulus, division by 0 undefined (user symbol) (40) */
112
  INTS_MODULUS_TOTAL, /**< integer modulus with interpreted division by 0 (internal symbol) (41) */
113
  ABS, /**< absolute value (42) */
114
  DIVISIBLE, /**< divisibility-by-k predicate; first parameter is a DIVISIBLE_OP, second is integer term (43) */
115
  POW, /**< arithmetic power (44) */
116
  EXPONENTIAL, /**< exponential (45) */
117
  SINE, /**< sine (46) */
118
  COSINE, /**< consine (47) */
119
  TANGENT, /**< tangent (48) */
120
  COSECANT, /**< cosecant (49) */
121
  SECANT, /**< secant (50) */
122
  COTANGENT, /**< cotangent (51) */
123
  ARCSINE, /**< arc sine (52) */
124
  ARCCOSINE, /**< arc consine (53) */
125
  ARCTANGENT, /**< arc tangent (54) */
126
  ARCCOSECANT, /**< arc cosecant (55) */
127
  ARCSECANT, /**< arc secant (56) */
128
  ARCCOTANGENT, /**< arc cotangent (57) */
129
  SQRT, /**< square root (58) */
130
  DIVISIBLE_OP, /**< operator for the divisibility-by-k predicate; payload is an instance of the CVC4::Divisible class (59) */
131
  CONST_RATIONAL, /**< a multiple-precision rational constant; payload is an instance of the CVC4::Rational class (60) */
132
  LT, /**< less than, x < y (61) */
133
  LEQ, /**< less than or equal, x <= y (62) */
134
  GT, /**< greater than, x > y (63) */
135
  GEQ, /**< greater than or equal, x >= y (64) */
136
  INDEXED_ROOT_PREDICATE_OP, /**< operator for the indexed root predicate; payload is an instance of the CVC4::IndexedRootPredicate class (65) */
137
  INDEXED_ROOT_PREDICATE, /**< indexed root predicate; first parameter is a INDEXED_ROOT_PREDICATE_OP, second is a real variable compared to zero, third is a polynomial (66) */
138
  IS_INTEGER, /**< term-is-integer predicate (parameter is a real-sorted term) (67) */
139
  TO_INTEGER, /**< convert term to integer by the floor function (parameter is a real-sorted term) (68) */
140
  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) (69) */
141
  CAST_TO_REAL, /**< cast term to real same as TO_REAL, but it is used internally, whereas TO_REAL is accessible in the API (70) */
142
  PI, /**< pi (71) */
143
  IAND_OP, /**< operator for integer AND; payload is an instance of the CVC4::IntAnd class (72) */
144
  IAND, /**< integer version of AND operator; first parameter is an IAND_OP, second and third are integer terms (73) */
145
146
  /* from bv */
147
  BITVECTOR_TYPE, /**< bit-vector type (74) */
148
  CONST_BITVECTOR, /**< a fixed-width bit-vector constant; payload is an instance of the CVC4::BitVector class (75) */
149
  BITVECTOR_CONCAT, /**< concatenation of two or more bit-vectors (76) */
150
  BITVECTOR_AND, /**< bitwise and of two or more bit-vectors (77) */
151
  BITVECTOR_COMP, /**< equality comparison of two bit-vectors (returns one bit) (78) */
152
  BITVECTOR_OR, /**< bitwise or of two or more bit-vectors (79) */
153
  BITVECTOR_XOR, /**< bitwise xor of two or more bit-vectors (80) */
154
  BITVECTOR_NOT, /**< bitwise not of a bit-vector (81) */
155
  BITVECTOR_NAND, /**< bitwise nand of two bit-vectors (82) */
156
  BITVECTOR_NOR, /**< bitwise nor of two bit-vectors (83) */
157
  BITVECTOR_XNOR, /**< bitwise xnor of two bit-vectors (84) */
158
  BITVECTOR_MULT, /**< multiplication of two or more bit-vectors (85) */
159
  BITVECTOR_NEG, /**< unary negation of a bit-vector (86) */
160
  BITVECTOR_PLUS, /**< addition of two or more bit-vectors (87) */
161
  BITVECTOR_SUB, /**< subtraction of two bit-vectors (88) */
162
  BITVECTOR_UDIV, /**< unsigned division of two bit-vectors, truncating towards 0 (defined to be the all-ones bit pattern, if divisor is 0) (89) */
163
  BITVECTOR_UREM, /**< unsigned remainder from truncating division of two bit-vectors (defined to be equal to the dividend, if divisor is 0) (90) */
164
  BITVECTOR_SDIV, /**< 2's complement signed division (91) */
165
  BITVECTOR_SMOD, /**< 2's complement signed remainder (sign follows divisor) (92) */
166
  BITVECTOR_SREM, /**< 2's complement signed remainder (sign follows dividend) (93) */
167
  BITVECTOR_ASHR, /**< bit-vector arithmetic shift right (the two bit-vector parameters must have same width) (94) */
168
  BITVECTOR_LSHR, /**< bit-vector logical shift right (the two bit-vector parameters must have same width) (95) */
169
  BITVECTOR_SHL, /**< bit-vector shift left (the two bit-vector parameters must have same width) (96) */
170
  BITVECTOR_ULE, /**< bit-vector unsigned less than or equal (the two bit-vector parameters must have same width) (97) */
171
  BITVECTOR_ULT, /**< bit-vector unsigned less than (the two bit-vector parameters must have same width) (98) */
172
  BITVECTOR_UGE, /**< bit-vector unsigned greater than or equal (the two bit-vector parameters must have same width) (99) */
173
  BITVECTOR_UGT, /**< bit-vector unsigned greater than (the two bit-vector parameters must have same width) (100) */
174
  BITVECTOR_SLE, /**< bit-vector signed less than or equal (the two bit-vector parameters must have same width) (101) */
175
  BITVECTOR_SLT, /**< bit-vector signed less than (the two bit-vector parameters must have same width) (102) */
176
  BITVECTOR_SGE, /**< bit-vector signed greater than or equal (the two bit-vector parameters must have same width) (103) */
177
  BITVECTOR_SGT, /**< bit-vector signed greater than (the two bit-vector parameters must have same width) (104) */
178
  BITVECTOR_ULTBV, /**< bit-vector unsigned less than but returns bv of size 1 instead of boolean (105) */
179
  BITVECTOR_SLTBV, /**< bit-vector signed less than but returns bv of size 1 instead of boolean (106) */
180
  BITVECTOR_REDAND, /**< bit-vector redand (107) */
181
  BITVECTOR_REDOR, /**< bit-vector redor (108) */
182
  BITVECTOR_ITE, /**< same semantics as regular ITE, but condition is bv of size 1 instead of Boolean (109) */
183
  BITVECTOR_TO_NAT, /**< bit-vector conversion to (nonnegative) integer; parameter is a bit-vector (110) */
184
  BITVECTOR_ACKERMANNIZE_UDIV, /**< term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvudiv (internal-only symbol) (111) */
185
  BITVECTOR_ACKERMANNIZE_UREM, /**< term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvurem (internal-only symbol) (112) */
186
  BITVECTOR_EAGER_ATOM, /**< formula to be treated as a bv atom via eager bit-blasting (internal-only symbol) (113) */
187
  BITVECTOR_BITOF_OP, /**< operator for the bit-vector boolean bit extract; payload is an instance of the CVC4::BitVectorBitOf class (114) */
188
  BITVECTOR_BITOF, /**< bit-vector boolean bit extract; first parameter is a BITVECTOR_BITOF_OP, second is a bit-vector term (115) */
189
  BITVECTOR_EXTRACT_OP, /**< operator for the bit-vector extract; payload is an instance of the CVC4::BitVectorExtract class (116) */
190
  BITVECTOR_EXTRACT, /**< bit-vector extract; first parameter is a BITVECTOR_EXTRACT_OP, second is a bit-vector term (117) */
191
  BITVECTOR_REPEAT_OP, /**< operator for the bit-vector repeat; payload is an instance of the CVC4::BitVectorRepeat class (118) */
192
  BITVECTOR_REPEAT, /**< bit-vector repeat; first parameter is a BITVECTOR_REPEAT_OP, second is a bit-vector term (119) */
193
  BITVECTOR_ROTATE_LEFT_OP, /**< operator for the bit-vector rotate left; payload is an instance of the CVC4::BitVectorRotateLeft class (120) */
194
  BITVECTOR_ROTATE_LEFT, /**< bit-vector rotate left; first parameter is a BITVECTOR_ROTATE_LEFT_OP, second is a bit-vector term (121) */
195
  BITVECTOR_ROTATE_RIGHT_OP, /**< operator for the bit-vector rotate right; payload is an instance of the CVC4::BitVectorRotateRight class (122) */
196
  BITVECTOR_ROTATE_RIGHT, /**< bit-vector rotate right; first parameter is a BITVECTOR_ROTATE_RIGHT_OP, second is a bit-vector term (123) */
197
  BITVECTOR_SIGN_EXTEND_OP, /**< operator for the bit-vector sign-extend; payload is an instance of the CVC4::BitVectorSignExtend class (124) */
198
  BITVECTOR_SIGN_EXTEND, /**< bit-vector sign-extend; first parameter is a BITVECTOR_SIGN_EXTEND_OP, second is a bit-vector term (125) */
199
  BITVECTOR_ZERO_EXTEND_OP, /**< operator for the bit-vector zero-extend; payload is an instance of the CVC4::BitVectorZeroExtend class (126) */
200
  BITVECTOR_ZERO_EXTEND, /**< bit-vector zero-extend; first parameter is a BITVECTOR_ZERO_EXTEND_OP, second is a bit-vector term (127) */
201
  INT_TO_BITVECTOR_OP, /**< operator for the integer conversion to bit-vector; payload is an instance of the CVC4::IntToBitVector class (128) */
202
  INT_TO_BITVECTOR, /**< integer conversion to bit-vector; first parameter is an INT_TO_BITVECTOR_OP, second is an integer term (129) */
203
204
  /* from fp */
205
  CONST_FLOATINGPOINT, /**< a floating-point literal (130) */
206
  CONST_ROUNDINGMODE, /**< a floating-point rounding mode (131) */
207
  FLOATINGPOINT_TYPE, /**< floating-point type (132) */
208
  FLOATINGPOINT_FP, /**< construct a floating-point literal from bit vectors (133) */
209
  FLOATINGPOINT_EQ, /**< floating-point equality (134) */
210
  FLOATINGPOINT_ABS, /**< floating-point absolute value (135) */
211
  FLOATINGPOINT_NEG, /**< floating-point negation (136) */
212
  FLOATINGPOINT_PLUS, /**< floating-point addition (137) */
213
  FLOATINGPOINT_SUB, /**< floating-point sutraction (138) */
214
  FLOATINGPOINT_MULT, /**< floating-point multiply (139) */
215
  FLOATINGPOINT_DIV, /**< floating-point division (140) */
216
  FLOATINGPOINT_FMA, /**< floating-point fused multiply and add (141) */
217
  FLOATINGPOINT_SQRT, /**< floating-point square root (142) */
218
  FLOATINGPOINT_REM, /**< floating-point remainder (143) */
219
  FLOATINGPOINT_RTI, /**< floating-point round to integral (144) */
220
  FLOATINGPOINT_MIN, /**< floating-point minimum (145) */
221
  FLOATINGPOINT_MAX, /**< floating-point maximum (146) */
222
  FLOATINGPOINT_MIN_TOTAL, /**< floating-point minimum (defined for all inputs) (147) */
223
  FLOATINGPOINT_MAX_TOTAL, /**< floating-point maximum (defined for all inputs) (148) */
224
  FLOATINGPOINT_LEQ, /**< floating-point less than or equal (149) */
225
  FLOATINGPOINT_LT, /**< floating-point less than (150) */
226
  FLOATINGPOINT_GEQ, /**< floating-point greater than or equal (151) */
227
  FLOATINGPOINT_GT, /**< floating-point greater than (152) */
228
  FLOATINGPOINT_ISN, /**< floating-point is normal (153) */
229
  FLOATINGPOINT_ISSN, /**< floating-point is sub-normal (154) */
230
  FLOATINGPOINT_ISZ, /**< floating-point is zero (155) */
231
  FLOATINGPOINT_ISINF, /**< floating-point is infinite (156) */
232
  FLOATINGPOINT_ISNAN, /**< floating-point is NaN (157) */
233
  FLOATINGPOINT_ISNEG, /**< floating-point is negative (158) */
234
  FLOATINGPOINT_ISPOS, /**< floating-point is positive (159) */
235
  FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP, /**< operator for to_fp from bit vector (160) */
236
  FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, /**< convert an IEEE-754 bit vector to floating-point (161) */
237
  FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP, /**< operator for to_fp from floating point (162) */
238
  FLOATINGPOINT_TO_FP_FLOATINGPOINT, /**< convert between floating-point sorts (163) */
239
  FLOATINGPOINT_TO_FP_REAL_OP, /**< operator for to_fp from real (164) */
240
  FLOATINGPOINT_TO_FP_REAL, /**< convert a real to floating-point (165) */
241
  FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP, /**< operator for to_fp from signed bit vector (166) */
242
  FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, /**< convert a signed bit vector to floating-point (167) */
243
  FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP, /**< operator for to_fp from unsigned bit vector (168) */
244
  FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, /**< convert an unsigned bit vector to floating-point (169) */
245
  FLOATINGPOINT_TO_FP_GENERIC_OP, /**< operator for a generic to_fp (170) */
246
  FLOATINGPOINT_TO_FP_GENERIC, /**< a generic conversion to floating-point, used in parsing only (171) */
247
  FLOATINGPOINT_TO_UBV_OP, /**< operator for to_ubv (172) */
248
  FLOATINGPOINT_TO_UBV, /**< convert a floating-point value to an unsigned bit vector (173) */
249
  FLOATINGPOINT_TO_UBV_TOTAL_OP, /**< operator for to_ubv_total (174) */
250
  FLOATINGPOINT_TO_UBV_TOTAL, /**< convert a floating-point value to an unsigned bit vector (defined for all inputs) (175) */
251
  FLOATINGPOINT_TO_SBV_OP, /**< operator for to_sbv (176) */
252
  FLOATINGPOINT_TO_SBV, /**< convert a floating-point value to a signed bit vector (177) */
253
  FLOATINGPOINT_TO_SBV_TOTAL_OP, /**< operator for to_sbv_total (178) */
254
  FLOATINGPOINT_TO_SBV_TOTAL, /**< convert a floating-point value to a signed bit vector (defined for all inputs) (179) */
255
  FLOATINGPOINT_TO_REAL, /**< floating-point to real (180) */
256
  FLOATINGPOINT_TO_REAL_TOTAL, /**< floating-point to real (defined for all inputs) (181) */
257
  FLOATINGPOINT_COMPONENT_NAN, /**< NaN component of a word-blasted floating-point number (182) */
258
  FLOATINGPOINT_COMPONENT_INF, /**< Inf component of a word-blasted floating-point number (183) */
259
  FLOATINGPOINT_COMPONENT_ZERO, /**< Zero component of a word-blasted floating-point number (184) */
260
  FLOATINGPOINT_COMPONENT_SIGN, /**< Sign component of a word-blasted floating-point number (185) */
261
  FLOATINGPOINT_COMPONENT_EXPONENT, /**< Exponent component of a word-blasted floating-point number (186) */
262
  FLOATINGPOINT_COMPONENT_SIGNIFICAND, /**< Significand component of a word-blasted floating-point number (187) */
263
  ROUNDINGMODE_BITBLAST, /**< The bit-vector for a non-deterministic rounding mode (188) */
264
265
  /* from arrays */
266
  ARRAY_TYPE, /**< array type (189) */
267
  SELECT, /**< array select; first parameter is an array term, second is the selection index (190) */
268
  STORE, /**< array store; first parameter is an array term, second is the store index, third is the term to store at the index (191) */
269
  EQ_RANGE, /**< equality of two arrays over an index range lower/upper (192) */
270
  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) (193) */
271
  ARR_TABLE_FUN, /**< array table function (internal-only symbol) (194) */
272
  ARRAY_LAMBDA, /**< array lambda (internal-only symbol) (195) */
273
  PARTIAL_SELECT_0, /**< partial array select, for internal use only (196) */
274
  PARTIAL_SELECT_1, /**< partial array select, for internal use only (197) */
275
276
  /* from datatypes */
277
  CONSTRUCTOR_TYPE, /**< constructor (198) */
278
  SELECTOR_TYPE, /**< selector (199) */
279
  TESTER_TYPE, /**< tester (200) */
280
  APPLY_CONSTRUCTOR, /**< constructor application; first parameter is the constructor, remaining parameters (if any) are parameters to the constructor (201) */
281
  APPLY_SELECTOR, /**< selector application; parameter is a datatype term (undefined if mis-applied) (202) */
282
  APPLY_SELECTOR_TOTAL, /**< selector application; parameter is a datatype term (defined rigidly if mis-applied) (203) */
283
  APPLY_TESTER, /**< tester application; first parameter is a tester, second is a datatype term (204) */
284
  DATATYPE_TYPE, /**< a datatype type index (205) */
285
  PARAMETRIC_DATATYPE, /**< parametric datatype (206) */
286
  APPLY_TYPE_ASCRIPTION, /**< type ascription, for datatype constructor applications; first parameter is an ASCRIPTION_TYPE, second is the datatype constructor application being ascribed (207) */
287
  ASCRIPTION_TYPE, /**< a type parameter for type ascription; payload is an instance of the CVC4::AscriptionType class (208) */
288
  TUPLE_UPDATE_OP, /**< operator for a tuple update; payload is an instance of the CVC4::TupleUpdate class (209) */
289
  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 (210) */
290
  RECORD_UPDATE_OP, /**< operator for a record update; payload is an instance CVC4::RecordUpdate class (211) */
291
  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 (212) */
292
  DT_SIZE, /**< datatypes size (213) */
293
  DT_HEIGHT_BOUND, /**< datatypes height bound (214) */
294
  DT_SIZE_BOUND, /**< datatypes height bound (215) */
295
  DT_SYGUS_BOUND, /**< datatypes sygus bound (216) */
296
  DT_SYGUS_EVAL, /**< datatypes sygus evaluation function (217) */
297
  MATCH, /**< match construct (218) */
298
  MATCH_CASE, /**< a match case (219) */
299
  MATCH_BIND_CASE, /**< a match case with bound variables (220) */
300
  TUPLE_PROJECT_OP, /**< operator for TUPLE_PROJECT; payload is an instance of the CVC4::TupleProjectOp class (221) */
301
  TUPLE_PROJECT, /**< projects a tuple from an existing tuple using indices passed in TupleProjectOp (222) */
302
303
  /* from sep */
304
  SEP_NIL, /**< separation nil (223) */
305
  SEP_EMP, /**< separation empty heap (224) */
306
  SEP_PTO, /**< points to relation (225) */
307
  SEP_STAR, /**< separation star (226) */
308
  SEP_WAND, /**< separation magic wand (227) */
309
  SEP_LABEL, /**< separation label (internal use only) (228) */
310
311
  /* from sets */
312
  EMPTYSET, /**< the empty set constant; payload is an instance of the CVC4::EmptySet class (229) */
313
  SET_TYPE, /**< set type, takes as parameter the type of the elements (230) */
314
  UNION, /**< set union (231) */
315
  INTERSECTION, /**< set intersection (232) */
316
  SETMINUS, /**< set subtraction (233) */
317
  SUBSET, /**< subset predicate; first parameter a subset of second (234) */
318
  MEMBER, /**< set membership predicate; first parameter a member of second (235) */
319
  SINGLETON_OP, /**< operator for singletons; payload is an instance of the CVC4::SingletonOp class (236) */
320
  SINGLETON, /**< constructs a set of a single element. First parameter is a SingletonOp. Second is a term (237) */
321
  INSERT, /**< set obtained by inserting elements (first N-1 parameters) into a set (the last parameter) (238) */
322
  CARD, /**< set cardinality operator (239) */
323
  COMPLEMENT, /**< set COMPLEMENT (with respect to finite universe) (240) */
324
  UNIVERSE_SET, /**< (finite) universe set, all set variables must be interpreted as subsets of it. (241) */
325
  COMPREHENSION, /**< set comprehension specified by a bound variable list, a predicate, and a term. (242) */
326
  CHOOSE, /**< return an element in the set given as a parameter (243) */
327
  IS_SINGLETON, /**< return whether the given set is a singleton (244) */
328
  JOIN, /**< set join (245) */
329
  PRODUCT, /**< set cartesian product (246) */
330
  TRANSPOSE, /**< set transpose (247) */
331
  TCLOSURE, /**< set transitive closure (248) */
332
  JOIN_IMAGE, /**< set join image (249) */
333
  IDEN, /**< set identity (250) */
334
335
  /* from bags */
336
  EMPTYBAG, /**< the empty bag constant; payload is an instance of the CVC4::EmptyBag class (251) */
337
  BAG_TYPE, /**< bag type, takes as parameter the type of the elements (252) */
338
  UNION_MAX, /**< union for bags (max) (253) */
339
  UNION_DISJOINT, /**< disjoint union for bags (sum) (254) */
340
  INTERSECTION_MIN, /**< bag intersection (min) (255) */
341
  DIFFERENCE_SUBTRACT, /**< bag difference1 (subtracts multiplicities) (256) */
342
  DIFFERENCE_REMOVE, /**< bag difference remove (removes shared elements) (257) */
343
  SUBBAG, /**< inclusion predicate for bags (less than or equal multiplicities) (258) */
344
  BAG_COUNT, /**< multiplicity of an element in a bag (259) */
345
  DUPLICATE_REMOVAL, /**< eliminate duplicates in a bag (also known as the delta operator,or the squash operator) (260) */
346
  MK_BAG_OP, /**< operator for MK_BAG; payload is an instance of the CVC4::MakeBagOp class (261) */
347
  MK_BAG, /**< constructs a bag from one element along with its multiplicity (262) */
348
  BAG_IS_SINGLETON, /**< return whether the given bag is a singleton (263) */
349
  BAG_CARD, /**< bag cardinality operator (264) */
350
  BAG_FROM_SET, /**< converts a set to a bag (265) */
351
  BAG_TO_SET, /**< converts a bag to a set (266) */
352
  BAG_CHOOSE, /**< return an element in the bag given as a parameter (267) */
353
354
  /* from strings */
355
  STRING_CONCAT, /**< string concat (N-ary) (268) */
356
  STRING_IN_REGEXP, /**< membership (269) */
357
  STRING_LENGTH, /**< string length (270) */
358
  STRING_SUBSTR, /**< string substr (271) */
359
  STRING_UPDATE, /**< string update (272) */
360
  STRING_CHARAT, /**< string charat (273) */
361
  STRING_STRCTN, /**< string contains (274) */
362
  STRING_LT, /**< string less than (275) */
363
  STRING_LEQ, /**< string less than or equal (276) */
364
  STRING_STRIDOF, /**< string indexof (277) */
365
  STRING_STRREPL, /**< string replace (278) */
366
  STRING_STRREPLALL, /**< string replace all (279) */
367
  STRING_REPLACE_RE, /**< string replace regular expression match (280) */
368
  STRING_REPLACE_RE_ALL, /**< string replace all regular expression matches (281) */
369
  STRING_PREFIX, /**< string prefixof (282) */
370
  STRING_SUFFIX, /**< string suffixof (283) */
371
  STRING_IS_DIGIT, /**< string isdigit, returns true if argument is a string of length one that represents a digit (284) */
372
  STRING_ITOS, /**< integer to string (285) */
373
  STRING_STOI, /**< string to integer (total function) (286) */
374
  STRING_TO_CODE, /**< string to code, returns the code of the first character of the string if it has length one, -1 otherwise (287) */
375
  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 (288) */
376
  STRING_TOLOWER, /**< string to lowercase conversion (289) */
377
  STRING_TOUPPER, /**< string to uppercase conversion (290) */
378
  STRING_REV, /**< string reverse (291) */
379
  CONST_STRING, /**< a string of characters (292) */
380
  SEQUENCE_TYPE, /**< seuence type, takes as parameter the type of the elements (293) */
381
  CONST_SEQUENCE, /**< a sequence of characters (294) */
382
  SEQ_UNIT, /**< a sequence of length one (295) */
383
  SEQ_NTH, /**< The nth element of a sequence (296) */
384
  SEQ_NTH_TOTAL, /**< The nth element of a sequence (internal, for responses to expand definitions only) (297) */
385
  STRING_TO_REGEXP, /**< convert string to regexp (298) */
386
  REGEXP_CONCAT, /**< regexp concat (299) */
387
  REGEXP_UNION, /**< regexp union (300) */
388
  REGEXP_INTER, /**< regexp intersection (301) */
389
  REGEXP_DIFF, /**< regexp difference (302) */
390
  REGEXP_STAR, /**< regexp * (303) */
391
  REGEXP_PLUS, /**< regexp + (304) */
392
  REGEXP_OPT, /**< regexp ? (305) */
393
  REGEXP_RANGE, /**< regexp range (306) */
394
  REGEXP_COMPLEMENT, /**< regexp complement (307) */
395
  REGEXP_EMPTY, /**< regexp empty (308) */
396
  REGEXP_SIGMA, /**< regexp all characters (309) */
397
  REGEXP_REPEAT_OP, /**< operator for regular expression repeat; payload is an instance of the CVC4::RegExpRepeat class (310) */
398
  REGEXP_REPEAT, /**< regular expression repeat; first parameter is a REGEXP_REPEAT_OP, second is a regular expression term (311) */
399
  REGEXP_LOOP_OP, /**< operator for regular expression loop; payload is an instance of the CVC4::RegExpLoop class (312) */
400
  REGEXP_LOOP, /**< regular expression loop; first parameter is a REGEXP_LOOP_OP, second is a regular expression term (313) */
401
  REGEXP_RV, /**< regexp rv (internal use only) (314) */
402
403
  /* from quantifiers */
404
  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 (315) */
405
  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 (316) */
406
  INST_CONSTANT, /**< instantiation constant (317) */
407
  BOUND_VAR_LIST, /**< a list of bound variables (used to bind variables under a quantifier) (318) */
408
  INST_PATTERN, /**< instantiation pattern (319) */
409
  INST_NO_PATTERN, /**< instantiation no-pattern (320) */
410
  INST_ATTRIBUTE, /**< instantiation attribute (321) */
411
  INST_PATTERN_LIST, /**< a list of instantiation patterns (322) */
412
 LAST_KIND /**< marks the upper-bound of this enumeration */
413
414
}; /* enum Kind_t */
415
416
}/* CVC4::kind namespace */
417
418
// import Kind into the "CVC4" namespace but keep the individual kind
419
// constants under kind::
420
typedef ::CVC4::kind::Kind_t Kind;
421
422
namespace kind {
423
424
/**
425
 * Converts an kind to a string. Note: This function is also used in
426
 * `safe_print()`. Changing this functions name or signature will result in
427
 * `safe_print()` printing "<unsupported>" instead of the proper strings for
428
 * the enum values.
429
 *
430
 * @param k The kind
431
 * @return The name of the kind
432
 */
433
const char* toString(CVC4::Kind k);
434
435
/**
436
 * Writes a kind name to a stream.
437
 *
438
 * @param out The stream to write to
439
 * @param k The kind to write to the stream
440
 * @return The stream
441
 */
442
std::ostream& operator<<(std::ostream&, CVC4::Kind);
443
444
/** Returns true if the given kind is associative. This is used by ExprManager to
445
 * decide whether it's safe to modify big expressions by changing the grouping of
446
 * the arguments. */
447
/* TODO: This could be generated. */
448
bool isAssociative(::CVC4::Kind k);
449
std::string kindToString(::CVC4::Kind k);
450
451
struct KindHashFunction {
452
13055676
  inline size_t operator()(::CVC4::Kind k) const {
453
13055676
    return k;
454
  }
455
};/* struct KindHashFunction */
456
457
}/* CVC4::kind namespace */
458
459
/**
460
 * The enumeration for the built-in atomic types.
461
 */
462
enum TypeConstant
463
{
464
    BUILTIN_OPERATOR_TYPE, /**< the type for built-in operators */
465
  BOOLEAN_TYPE, /**< Boolean type */
466
  REAL_TYPE, /**< real type */
467
  INTEGER_TYPE, /**< integer type */
468
  ROUNDINGMODE_TYPE, /**< floating-point rounding mode */
469
  STRING_TYPE, /**< String type */
470
  REGEXP_TYPE, /**< RegExp type */
471
  BOUND_VAR_LIST_TYPE, /**< the type of bound variable lists */
472
  INST_PATTERN_TYPE, /**< instantiation pattern type */
473
  INST_PATTERN_LIST_TYPE, /**< the type of instantiation pattern lists */
474
 LAST_TYPE
475
}; /* enum TypeConstant */
476
477
/**
478
 * We hash the constants with their values.
479
 */
480
struct TypeConstantHashFunction {
481
28709328
  inline size_t operator()(TypeConstant tc) const {
482
28709328
    return tc;
483
  }
484
};/* struct TypeConstantHashFunction */
485
486
std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant);
487
488
namespace theory {
489
490
::CVC4::theory::TheoryId kindToTheoryId(::CVC4::Kind k);
491
::CVC4::theory::TheoryId typeConstantToTheoryId(
492
    ::CVC4::TypeConstant typeConstant);
493
494
}/* CVC4::theory namespace */
495
}/* CVC4 namespace */
496
497
#endif /* CVC4__KIND_H */