GCC Code Coverage Report
Directory: . Exec Total Coverage
File: build-coverage/src/expr/kind.cpp Lines: 390 700 55.7 %
Date: 2021-03-23 Branches: 376 686 54.8 %

Line Exec Source
1
/*********************                                                        */
2
/** kind.cpp
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.cpp /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.cpp */
30
31
/*********************                                                        */
32
/*! \file kind_template.cpp
33
 ** \verbatim
34
 ** Top contributors (to current version):
35
 **   Andres Noetzli, Christopher L. Conway, 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 [[ Add one-line brief description here ]]
43
 **
44
 ** [[ Add lengthier description here ]]
45
 ** \todo document this file
46
 **/
47
48
#include <sstream>
49
50
#include "expr/kind.h"
51
52
namespace CVC4 {
53
namespace kind {
54
55
10450
const char* toString(CVC4::Kind k)
56
{
57
  using namespace CVC4::kind;
58
59
10450
  switch (k)
60
  {
61
    /* special cases */
62
4
    case UNDEFINED_KIND: return "UNDEFINED_KIND";
63
4
    case NULL_EXPR: return "NULL";
64
65
  /* from builtin */
66
  case SORT_TAG: return "SORT_TAG";
67
  case SORT_TYPE: return "SORT_TYPE";
68
  case UNINTERPRETED_CONSTANT: return "UNINTERPRETED_CONSTANT";
69
  case ABSTRACT_VALUE: return "ABSTRACT_VALUE";
70
  case BUILTIN: return "BUILTIN";
71
657
  case EQUAL: return "EQUAL";
72
4
  case DISTINCT: return "DISTINCT";
73
33
  case VARIABLE: return "VARIABLE";
74
1001
  case BOUND_VARIABLE: return "BOUND_VARIABLE";
75
  case SKOLEM: return "SKOLEM";
76
2
  case SEXPR: return "SEXPR";
77
20
  case LAMBDA: return "LAMBDA";
78
  case WITNESS: return "WITNESS";
79
  case TYPE_CONSTANT: return "TYPE_CONSTANT";
80
  case FUNCTION_TYPE: return "FUNCTION_TYPE";
81
  case SEXPR_TYPE: return "SEXPR_TYPE";
82
83
  /* from booleans */
84
66
  case CONST_BOOLEAN: return "CONST_BOOLEAN";
85
552
  case NOT: return "NOT";
86
596
  case AND: return "AND";
87
4
  case IMPLIES: return "IMPLIES";
88
576
  case OR: return "OR";
89
24
  case XOR: return "XOR";
90
750
  case ITE: return "ITE";
91
92
  /* from uf */
93
158
  case APPLY_UF: return "APPLY_UF";
94
6
  case BOOLEAN_TERM_VARIABLE: return "BOOLEAN_TERM_VARIABLE";
95
  case CARDINALITY_CONSTRAINT: return "CARDINALITY_CONSTRAINT";
96
  case COMBINED_CARDINALITY_CONSTRAINT: return "COMBINED_CARDINALITY_CONSTRAINT";
97
  case PARTIAL_APPLY_UF: return "PARTIAL_APPLY_UF";
98
  case CARDINALITY_VALUE: return "CARDINALITY_VALUE";
99
  case HO_APPLY: return "HO_APPLY";
100
101
  /* from arith */
102
640
  case PLUS: return "PLUS";
103
12
  case MULT: return "MULT";
104
  case NONLINEAR_MULT: return "NONLINEAR_MULT";
105
532
  case MINUS: return "MINUS";
106
12
  case UMINUS: return "UMINUS";
107
44
  case DIVISION: return "DIVISION";
108
  case DIVISION_TOTAL: return "DIVISION_TOTAL";
109
1
  case INTS_DIVISION: return "INTS_DIVISION";
110
  case INTS_DIVISION_TOTAL: return "INTS_DIVISION_TOTAL";
111
5
  case INTS_MODULUS: return "INTS_MODULUS";
112
  case INTS_MODULUS_TOTAL: return "INTS_MODULUS_TOTAL";
113
  case ABS: return "ABS";
114
16
  case DIVISIBLE: return "DIVISIBLE";
115
  case POW: return "POW";
116
  case EXPONENTIAL: return "EXPONENTIAL";
117
  case SINE: return "SINE";
118
  case COSINE: return "COSINE";
119
  case TANGENT: return "TANGENT";
120
  case COSECANT: return "COSECANT";
121
  case SECANT: return "SECANT";
122
  case COTANGENT: return "COTANGENT";
123
  case ARCSINE: return "ARCSINE";
124
  case ARCCOSINE: return "ARCCOSINE";
125
  case ARCTANGENT: return "ARCTANGENT";
126
  case ARCCOSECANT: return "ARCCOSECANT";
127
  case ARCSECANT: return "ARCSECANT";
128
  case ARCCOTANGENT: return "ARCCOTANGENT";
129
  case SQRT: return "SQRT";
130
  case DIVISIBLE_OP: return "DIVISIBLE_OP";
131
444
  case CONST_RATIONAL: return "CONST_RATIONAL";
132
35
  case LT: return "LT";
133
526
  case LEQ: return "LEQ";
134
28
  case GT: return "GT";
135
40
  case GEQ: return "GEQ";
136
  case INDEXED_ROOT_PREDICATE_OP: return "INDEXED_ROOT_PREDICATE_OP";
137
  case INDEXED_ROOT_PREDICATE: return "INDEXED_ROOT_PREDICATE";
138
  case IS_INTEGER: return "IS_INTEGER";
139
  case TO_INTEGER: return "TO_INTEGER";
140
  case TO_REAL: return "TO_REAL";
141
  case CAST_TO_REAL: return "CAST_TO_REAL";
142
  case PI: return "PI";
143
  case IAND_OP: return "IAND_OP";
144
  case IAND: return "IAND";
145
146
  /* from bv */
147
  case BITVECTOR_TYPE: return "BITVECTOR_TYPE";
148
105
  case CONST_BITVECTOR: return "CONST_BITVECTOR";
149
2
  case BITVECTOR_CONCAT: return "BITVECTOR_CONCAT";
150
88
  case BITVECTOR_AND: return "BITVECTOR_AND";
151
14
  case BITVECTOR_COMP: return "BITVECTOR_COMP";
152
110
  case BITVECTOR_OR: return "BITVECTOR_OR";
153
69
  case BITVECTOR_XOR: return "BITVECTOR_XOR";
154
112
  case BITVECTOR_NOT: return "BITVECTOR_NOT";
155
  case BITVECTOR_NAND: return "BITVECTOR_NAND";
156
  case BITVECTOR_NOR: return "BITVECTOR_NOR";
157
  case BITVECTOR_XNOR: return "BITVECTOR_XNOR";
158
51
  case BITVECTOR_MULT: return "BITVECTOR_MULT";
159
58
  case BITVECTOR_NEG: return "BITVECTOR_NEG";
160
82
  case BITVECTOR_PLUS: return "BITVECTOR_PLUS";
161
50
  case BITVECTOR_SUB: return "BITVECTOR_SUB";
162
53
  case BITVECTOR_UDIV: return "BITVECTOR_UDIV";
163
53
  case BITVECTOR_UREM: return "BITVECTOR_UREM";
164
51
  case BITVECTOR_SDIV: return "BITVECTOR_SDIV";
165
  case BITVECTOR_SMOD: return "BITVECTOR_SMOD";
166
47
  case BITVECTOR_SREM: return "BITVECTOR_SREM";
167
43
  case BITVECTOR_ASHR: return "BITVECTOR_ASHR";
168
54
  case BITVECTOR_LSHR: return "BITVECTOR_LSHR";
169
54
  case BITVECTOR_SHL: return "BITVECTOR_SHL";
170
4
  case BITVECTOR_ULE: return "BITVECTOR_ULE";
171
46
  case BITVECTOR_ULT: return "BITVECTOR_ULT";
172
3
  case BITVECTOR_UGE: return "BITVECTOR_UGE";
173
2
  case BITVECTOR_UGT: return "BITVECTOR_UGT";
174
  case BITVECTOR_SLE: return "BITVECTOR_SLE";
175
3
  case BITVECTOR_SLT: return "BITVECTOR_SLT";
176
3
  case BITVECTOR_SGE: return "BITVECTOR_SGE";
177
  case BITVECTOR_SGT: return "BITVECTOR_SGT";
178
16
  case BITVECTOR_ULTBV: return "BITVECTOR_ULTBV";
179
4
  case BITVECTOR_SLTBV: return "BITVECTOR_SLTBV";
180
  case BITVECTOR_REDAND: return "BITVECTOR_REDAND";
181
  case BITVECTOR_REDOR: return "BITVECTOR_REDOR";
182
12
  case BITVECTOR_ITE: return "BITVECTOR_ITE";
183
  case BITVECTOR_TO_NAT: return "BITVECTOR_TO_NAT";
184
  case BITVECTOR_ACKERMANNIZE_UDIV: return "BITVECTOR_ACKERMANNIZE_UDIV";
185
  case BITVECTOR_ACKERMANNIZE_UREM: return "BITVECTOR_ACKERMANNIZE_UREM";
186
  case BITVECTOR_EAGER_ATOM: return "BITVECTOR_EAGER_ATOM";
187
  case BITVECTOR_BITOF_OP: return "BITVECTOR_BITOF_OP";
188
  case BITVECTOR_BITOF: return "BITVECTOR_BITOF";
189
  case BITVECTOR_EXTRACT_OP: return "BITVECTOR_EXTRACT_OP";
190
26
  case BITVECTOR_EXTRACT: return "BITVECTOR_EXTRACT";
191
  case BITVECTOR_REPEAT_OP: return "BITVECTOR_REPEAT_OP";
192
3
  case BITVECTOR_REPEAT: return "BITVECTOR_REPEAT";
193
  case BITVECTOR_ROTATE_LEFT_OP: return "BITVECTOR_ROTATE_LEFT_OP";
194
  case BITVECTOR_ROTATE_LEFT: return "BITVECTOR_ROTATE_LEFT";
195
  case BITVECTOR_ROTATE_RIGHT_OP: return "BITVECTOR_ROTATE_RIGHT_OP";
196
  case BITVECTOR_ROTATE_RIGHT: return "BITVECTOR_ROTATE_RIGHT";
197
  case BITVECTOR_SIGN_EXTEND_OP: return "BITVECTOR_SIGN_EXTEND_OP";
198
  case BITVECTOR_SIGN_EXTEND: return "BITVECTOR_SIGN_EXTEND";
199
  case BITVECTOR_ZERO_EXTEND_OP: return "BITVECTOR_ZERO_EXTEND_OP";
200
  case BITVECTOR_ZERO_EXTEND: return "BITVECTOR_ZERO_EXTEND";
201
1
  case INT_TO_BITVECTOR_OP: return "INT_TO_BITVECTOR_OP";
202
  case INT_TO_BITVECTOR: return "INT_TO_BITVECTOR";
203
204
  /* from fp */
205
  case CONST_FLOATINGPOINT: return "CONST_FLOATINGPOINT";
206
2
  case CONST_ROUNDINGMODE: return "CONST_ROUNDINGMODE";
207
  case FLOATINGPOINT_TYPE: return "FLOATINGPOINT_TYPE";
208
  case FLOATINGPOINT_FP: return "FLOATINGPOINT_FP";
209
  case FLOATINGPOINT_EQ: return "FLOATINGPOINT_EQ";
210
2
  case FLOATINGPOINT_ABS: return "FLOATINGPOINT_ABS";
211
2
  case FLOATINGPOINT_NEG: return "FLOATINGPOINT_NEG";
212
2
  case FLOATINGPOINT_PLUS: return "FLOATINGPOINT_PLUS";
213
4
  case FLOATINGPOINT_SUB: return "FLOATINGPOINT_SUB";
214
2
  case FLOATINGPOINT_MULT: return "FLOATINGPOINT_MULT";
215
2
  case FLOATINGPOINT_DIV: return "FLOATINGPOINT_DIV";
216
  case FLOATINGPOINT_FMA: return "FLOATINGPOINT_FMA";
217
2
  case FLOATINGPOINT_SQRT: return "FLOATINGPOINT_SQRT";
218
2
  case FLOATINGPOINT_REM: return "FLOATINGPOINT_REM";
219
  case FLOATINGPOINT_RTI: return "FLOATINGPOINT_RTI";
220
  case FLOATINGPOINT_MIN: return "FLOATINGPOINT_MIN";
221
2
  case FLOATINGPOINT_MAX: return "FLOATINGPOINT_MAX";
222
  case FLOATINGPOINT_MIN_TOTAL: return "FLOATINGPOINT_MIN_TOTAL";
223
  case FLOATINGPOINT_MAX_TOTAL: return "FLOATINGPOINT_MAX_TOTAL";
224
  case FLOATINGPOINT_LEQ: return "FLOATINGPOINT_LEQ";
225
  case FLOATINGPOINT_LT: return "FLOATINGPOINT_LT";
226
  case FLOATINGPOINT_GEQ: return "FLOATINGPOINT_GEQ";
227
  case FLOATINGPOINT_GT: return "FLOATINGPOINT_GT";
228
1
  case FLOATINGPOINT_ISN: return "FLOATINGPOINT_ISN";
229
1
  case FLOATINGPOINT_ISSN: return "FLOATINGPOINT_ISSN";
230
3
  case FLOATINGPOINT_ISZ: return "FLOATINGPOINT_ISZ";
231
2
  case FLOATINGPOINT_ISINF: return "FLOATINGPOINT_ISINF";
232
1
  case FLOATINGPOINT_ISNAN: return "FLOATINGPOINT_ISNAN";
233
3
  case FLOATINGPOINT_ISNEG: return "FLOATINGPOINT_ISNEG";
234
1
  case FLOATINGPOINT_ISPOS: return "FLOATINGPOINT_ISPOS";
235
  case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP: return "FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP";
236
  case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: return "FLOATINGPOINT_TO_FP_IEEE_BITVECTOR";
237
  case FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP: return "FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP";
238
  case FLOATINGPOINT_TO_FP_FLOATINGPOINT: return "FLOATINGPOINT_TO_FP_FLOATINGPOINT";
239
  case FLOATINGPOINT_TO_FP_REAL_OP: return "FLOATINGPOINT_TO_FP_REAL_OP";
240
  case FLOATINGPOINT_TO_FP_REAL: return "FLOATINGPOINT_TO_FP_REAL";
241
  case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP: return "FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP";
242
  case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: return "FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR";
243
  case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP: return "FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP";
244
  case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: return "FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR";
245
  case FLOATINGPOINT_TO_FP_GENERIC_OP: return "FLOATINGPOINT_TO_FP_GENERIC_OP";
246
2
  case FLOATINGPOINT_TO_FP_GENERIC: return "FLOATINGPOINT_TO_FP_GENERIC";
247
  case FLOATINGPOINT_TO_UBV_OP: return "FLOATINGPOINT_TO_UBV_OP";
248
  case FLOATINGPOINT_TO_UBV: return "FLOATINGPOINT_TO_UBV";
249
  case FLOATINGPOINT_TO_UBV_TOTAL_OP: return "FLOATINGPOINT_TO_UBV_TOTAL_OP";
250
  case FLOATINGPOINT_TO_UBV_TOTAL: return "FLOATINGPOINT_TO_UBV_TOTAL";
251
  case FLOATINGPOINT_TO_SBV_OP: return "FLOATINGPOINT_TO_SBV_OP";
252
  case FLOATINGPOINT_TO_SBV: return "FLOATINGPOINT_TO_SBV";
253
  case FLOATINGPOINT_TO_SBV_TOTAL_OP: return "FLOATINGPOINT_TO_SBV_TOTAL_OP";
254
  case FLOATINGPOINT_TO_SBV_TOTAL: return "FLOATINGPOINT_TO_SBV_TOTAL";
255
  case FLOATINGPOINT_TO_REAL: return "FLOATINGPOINT_TO_REAL";
256
  case FLOATINGPOINT_TO_REAL_TOTAL: return "FLOATINGPOINT_TO_REAL_TOTAL";
257
  case FLOATINGPOINT_COMPONENT_NAN: return "FLOATINGPOINT_COMPONENT_NAN";
258
  case FLOATINGPOINT_COMPONENT_INF: return "FLOATINGPOINT_COMPONENT_INF";
259
  case FLOATINGPOINT_COMPONENT_ZERO: return "FLOATINGPOINT_COMPONENT_ZERO";
260
  case FLOATINGPOINT_COMPONENT_SIGN: return "FLOATINGPOINT_COMPONENT_SIGN";
261
  case FLOATINGPOINT_COMPONENT_EXPONENT: return "FLOATINGPOINT_COMPONENT_EXPONENT";
262
  case FLOATINGPOINT_COMPONENT_SIGNIFICAND: return "FLOATINGPOINT_COMPONENT_SIGNIFICAND";
263
  case ROUNDINGMODE_BITBLAST: return "ROUNDINGMODE_BITBLAST";
264
265
  /* from arrays */
266
  case ARRAY_TYPE: return "ARRAY_TYPE";
267
17
  case SELECT: return "SELECT";
268
17
  case STORE: return "STORE";
269
  case EQ_RANGE: return "EQ_RANGE";
270
  case STORE_ALL: return "STORE_ALL";
271
  case ARR_TABLE_FUN: return "ARR_TABLE_FUN";
272
  case ARRAY_LAMBDA: return "ARRAY_LAMBDA";
273
  case PARTIAL_SELECT_0: return "PARTIAL_SELECT_0";
274
  case PARTIAL_SELECT_1: return "PARTIAL_SELECT_1";
275
276
  /* from datatypes */
277
  case CONSTRUCTOR_TYPE: return "CONSTRUCTOR_TYPE";
278
  case SELECTOR_TYPE: return "SELECTOR_TYPE";
279
  case TESTER_TYPE: return "TESTER_TYPE";
280
98
  case APPLY_CONSTRUCTOR: return "APPLY_CONSTRUCTOR";
281
56
  case APPLY_SELECTOR: return "APPLY_SELECTOR";
282
  case APPLY_SELECTOR_TOTAL: return "APPLY_SELECTOR_TOTAL";
283
  case APPLY_TESTER: return "APPLY_TESTER";
284
  case DATATYPE_TYPE: return "DATATYPE_TYPE";
285
  case PARAMETRIC_DATATYPE: return "PARAMETRIC_DATATYPE";
286
  case APPLY_TYPE_ASCRIPTION: return "APPLY_TYPE_ASCRIPTION";
287
  case ASCRIPTION_TYPE: return "ASCRIPTION_TYPE";
288
  case TUPLE_UPDATE_OP: return "TUPLE_UPDATE_OP";
289
2
  case TUPLE_UPDATE: return "TUPLE_UPDATE";
290
  case RECORD_UPDATE_OP: return "RECORD_UPDATE_OP";
291
2
  case RECORD_UPDATE: return "RECORD_UPDATE";
292
  case DT_SIZE: return "DT_SIZE";
293
  case DT_HEIGHT_BOUND: return "DT_HEIGHT_BOUND";
294
  case DT_SIZE_BOUND: return "DT_SIZE_BOUND";
295
  case DT_SYGUS_BOUND: return "DT_SYGUS_BOUND";
296
336
  case DT_SYGUS_EVAL: return "DT_SYGUS_EVAL";
297
  case MATCH: return "MATCH";
298
  case MATCH_CASE: return "MATCH_CASE";
299
  case MATCH_BIND_CASE: return "MATCH_BIND_CASE";
300
  case TUPLE_PROJECT_OP: return "TUPLE_PROJECT_OP";
301
  case TUPLE_PROJECT: return "TUPLE_PROJECT";
302
303
  /* from sep */
304
  case SEP_NIL: return "SEP_NIL";
305
  case SEP_EMP: return "SEP_EMP";
306
  case SEP_PTO: return "SEP_PTO";
307
  case SEP_STAR: return "SEP_STAR";
308
  case SEP_WAND: return "SEP_WAND";
309
  case SEP_LABEL: return "SEP_LABEL";
310
311
  /* from sets */
312
  case EMPTYSET: return "EMPTYSET";
313
  case SET_TYPE: return "SET_TYPE";
314
10
  case UNION: return "UNION";
315
8
  case INTERSECTION: return "INTERSECTION";
316
8
  case SETMINUS: return "SETMINUS";
317
  case SUBSET: return "SUBSET";
318
8
  case MEMBER: return "MEMBER";
319
  case SINGLETON_OP: return "SINGLETON_OP";
320
  case SINGLETON: return "SINGLETON";
321
  case INSERT: return "INSERT";
322
  case CARD: return "CARD";
323
  case COMPLEMENT: return "COMPLEMENT";
324
  case UNIVERSE_SET: return "UNIVERSE_SET";
325
  case COMPREHENSION: return "COMPREHENSION";
326
  case CHOOSE: return "CHOOSE";
327
  case IS_SINGLETON: return "IS_SINGLETON";
328
  case JOIN: return "JOIN";
329
  case PRODUCT: return "PRODUCT";
330
  case TRANSPOSE: return "TRANSPOSE";
331
  case TCLOSURE: return "TCLOSURE";
332
  case JOIN_IMAGE: return "JOIN_IMAGE";
333
  case IDEN: return "IDEN";
334
335
  /* from bags */
336
  case EMPTYBAG: return "EMPTYBAG";
337
  case BAG_TYPE: return "BAG_TYPE";
338
  case UNION_MAX: return "UNION_MAX";
339
  case UNION_DISJOINT: return "UNION_DISJOINT";
340
  case INTERSECTION_MIN: return "INTERSECTION_MIN";
341
  case DIFFERENCE_SUBTRACT: return "DIFFERENCE_SUBTRACT";
342
  case DIFFERENCE_REMOVE: return "DIFFERENCE_REMOVE";
343
  case SUBBAG: return "SUBBAG";
344
  case BAG_COUNT: return "BAG_COUNT";
345
  case DUPLICATE_REMOVAL: return "DUPLICATE_REMOVAL";
346
  case MK_BAG_OP: return "MK_BAG_OP";
347
  case MK_BAG: return "MK_BAG";
348
  case BAG_IS_SINGLETON: return "BAG_IS_SINGLETON";
349
  case BAG_CARD: return "BAG_CARD";
350
  case BAG_FROM_SET: return "BAG_FROM_SET";
351
  case BAG_TO_SET: return "BAG_TO_SET";
352
  case BAG_CHOOSE: return "BAG_CHOOSE";
353
354
  /* from strings */
355
69
  case STRING_CONCAT: return "STRING_CONCAT";
356
2
  case STRING_IN_REGEXP: return "STRING_IN_REGEXP";
357
49
  case STRING_LENGTH: return "STRING_LENGTH";
358
12
  case STRING_SUBSTR: return "STRING_SUBSTR";
359
  case STRING_UPDATE: return "STRING_UPDATE";
360
8
  case STRING_CHARAT: return "STRING_CHARAT";
361
7
  case STRING_STRCTN: return "STRING_STRCTN";
362
  case STRING_LT: return "STRING_LT";
363
  case STRING_LEQ: return "STRING_LEQ";
364
10
  case STRING_STRIDOF: return "STRING_STRIDOF";
365
8
  case STRING_STRREPL: return "STRING_STRREPL";
366
  case STRING_STRREPLALL: return "STRING_STRREPLALL";
367
  case STRING_REPLACE_RE: return "STRING_REPLACE_RE";
368
  case STRING_REPLACE_RE_ALL: return "STRING_REPLACE_RE_ALL";
369
7
  case STRING_PREFIX: return "STRING_PREFIX";
370
7
  case STRING_SUFFIX: return "STRING_SUFFIX";
371
  case STRING_IS_DIGIT: return "STRING_IS_DIGIT";
372
8
  case STRING_ITOS: return "STRING_ITOS";
373
10
  case STRING_STOI: return "STRING_STOI";
374
  case STRING_TO_CODE: return "STRING_TO_CODE";
375
  case STRING_FROM_CODE: return "STRING_FROM_CODE";
376
  case STRING_TOLOWER: return "STRING_TOLOWER";
377
  case STRING_TOUPPER: return "STRING_TOUPPER";
378
  case STRING_REV: return "STRING_REV";
379
111
  case CONST_STRING: return "CONST_STRING";
380
  case SEQUENCE_TYPE: return "SEQUENCE_TYPE";
381
  case CONST_SEQUENCE: return "CONST_SEQUENCE";
382
  case SEQ_UNIT: return "SEQ_UNIT";
383
  case SEQ_NTH: return "SEQ_NTH";
384
  case SEQ_NTH_TOTAL: return "SEQ_NTH_TOTAL";
385
12
  case STRING_TO_REGEXP: return "STRING_TO_REGEXP";
386
8
  case REGEXP_CONCAT: return "REGEXP_CONCAT";
387
6
  case REGEXP_UNION: return "REGEXP_UNION";
388
6
  case REGEXP_INTER: return "REGEXP_INTER";
389
2
  case REGEXP_DIFF: return "REGEXP_DIFF";
390
6
  case REGEXP_STAR: return "REGEXP_STAR";
391
2
  case REGEXP_PLUS: return "REGEXP_PLUS";
392
2
  case REGEXP_OPT: return "REGEXP_OPT";
393
  case REGEXP_RANGE: return "REGEXP_RANGE";
394
2
  case REGEXP_COMPLEMENT: return "REGEXP_COMPLEMENT";
395
  case REGEXP_EMPTY: return "REGEXP_EMPTY";
396
  case REGEXP_SIGMA: return "REGEXP_SIGMA";
397
  case REGEXP_REPEAT_OP: return "REGEXP_REPEAT_OP";
398
  case REGEXP_REPEAT: return "REGEXP_REPEAT";
399
  case REGEXP_LOOP_OP: return "REGEXP_LOOP_OP";
400
  case REGEXP_LOOP: return "REGEXP_LOOP";
401
  case REGEXP_RV: return "REGEXP_RV";
402
403
  /* from quantifiers */
404
  case FORALL: return "FORALL";
405
  case EXISTS: return "EXISTS";
406
1481
  case INST_CONSTANT: return "INST_CONSTANT";
407
  case BOUND_VAR_LIST: return "BOUND_VAR_LIST";
408
  case INST_PATTERN: return "INST_PATTERN";
409
  case INST_NO_PATTERN: return "INST_NO_PATTERN";
410
  case INST_ATTRIBUTE: return "INST_ATTRIBUTE";
411
  case INST_PATTERN_LIST: return "INST_PATTERN_LIST";
412
413
4
    case LAST_KIND: return "LAST_KIND";
414
2
    default: return "?";
415
  }
416
}
417
418
10450
std::ostream& operator<<(std::ostream& out, CVC4::Kind k)
419
{
420
10450
  out << toString(k);
421
10450
  return out;
422
}
423
424
/** Returns true if the given kind is associative. This is used by ExprManager to
425
 * decide whether it's safe to modify big expressions by changing the grouping of
426
 * the arguments. */
427
/* TODO: This could be generated. */
428
4260962
bool isAssociative(::CVC4::Kind k) {
429
4260962
  switch(k) {
430
2000888
  case kind::AND:
431
  case kind::OR:
432
  case kind::MULT:
433
  case kind::PLUS:
434
2000888
    return true;
435
436
2260074
  default:
437
2260074
    return false;
438
  }
439
}
440
441
5206
std::string kindToString(::CVC4::Kind k) {
442
10412
  std::stringstream ss;
443
5206
  ss << k;
444
10412
  return ss.str();
445
}
446
447
}/* CVC4::kind namespace */
448
449
std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) {
450
  switch(typeConstant) {
451
  case BUILTIN_OPERATOR_TYPE:  out << "the type for built-in operators"; break;
452
  case BOOLEAN_TYPE:  out << "Boolean type"; break;
453
  case REAL_TYPE:  out << "real type"; break;
454
  case INTEGER_TYPE:  out << "integer type"; break;
455
  case ROUNDINGMODE_TYPE:  out << "floating-point rounding mode"; break;
456
  case STRING_TYPE:  out << "String type"; break;
457
  case REGEXP_TYPE:  out << "RegExp type"; break;
458
  case BOUND_VAR_LIST_TYPE:  out << "the type of bound variable lists"; break;
459
  case INST_PATTERN_TYPE:  out << "instantiation pattern type"; break;
460
  case INST_PATTERN_LIST_TYPE:  out << "the type of instantiation pattern lists"; break;
461
462
  default:
463
    out << "UNKNOWN_TYPE_CONSTANT";
464
    break;
465
  }
466
  return out;
467
}
468
469
namespace theory {
470
471
301723827
TheoryId kindToTheoryId(::CVC4::Kind k) {
472
301723827
  switch(k) {
473
  case kind::UNDEFINED_KIND:
474
  case kind::NULL_EXPR:
475
    break;
476
  case kind::SORT_TAG: return THEORY_BUILTIN;
477
2800762
  case kind::SORT_TYPE: return THEORY_BUILTIN;
478
45910
  case kind::UNINTERPRETED_CONSTANT: return THEORY_BUILTIN;
479
  case kind::ABSTRACT_VALUE: return THEORY_BUILTIN;
480
  case kind::BUILTIN: return THEORY_BUILTIN;
481
4333438
  case kind::EQUAL: return THEORY_BUILTIN;
482
13081
  case kind::DISTINCT: return THEORY_BUILTIN;
483
5646168
  case kind::VARIABLE: return THEORY_BUILTIN;
484
11017020
  case kind::BOUND_VARIABLE: return THEORY_BUILTIN;
485
2076232
  case kind::SKOLEM: return THEORY_BUILTIN;
486
  case kind::SEXPR: return THEORY_BUILTIN;
487
23799
  case kind::LAMBDA: return THEORY_BUILTIN;
488
10881
  case kind::WITNESS: return THEORY_BUILTIN;
489
  case kind::TYPE_CONSTANT: return THEORY_BUILTIN;
490
27429
  case kind::FUNCTION_TYPE: return THEORY_BUILTIN;
491
  case kind::SEXPR_TYPE: return THEORY_BUILTIN;
492
9338487
  case kind::CONST_BOOLEAN: return THEORY_BOOL;
493
24486343
  case kind::NOT: return THEORY_BOOL;
494
11989415
  case kind::AND: return THEORY_BOOL;
495
2445033
  case kind::IMPLIES: return THEORY_BOOL;
496
19564802
  case kind::OR: return THEORY_BOOL;
497
2603731
  case kind::XOR: return THEORY_BOOL;
498
7264804
  case kind::ITE: return THEORY_BOOL;
499
29453863
  case kind::APPLY_UF: return THEORY_UF;
500
211935
  case kind::BOOLEAN_TERM_VARIABLE: return THEORY_UF;
501
90859
  case kind::CARDINALITY_CONSTRAINT: return THEORY_UF;
502
30103
  case kind::COMBINED_CARDINALITY_CONSTRAINT: return THEORY_UF;
503
  case kind::PARTIAL_APPLY_UF: return THEORY_UF;
504
  case kind::CARDINALITY_VALUE: return THEORY_UF;
505
63773
  case kind::HO_APPLY: return THEORY_UF;
506
35842567
  case kind::PLUS: return THEORY_ARITH;
507
4986176
  case kind::MULT: return THEORY_ARITH;
508
4359161
  case kind::NONLINEAR_MULT: return THEORY_ARITH;
509
843326
  case kind::MINUS: return THEORY_ARITH;
510
63743
  case kind::UMINUS: return THEORY_ARITH;
511
8674
  case kind::DIVISION: return THEORY_ARITH;
512
1407
  case kind::DIVISION_TOTAL: return THEORY_ARITH;
513
2231
  case kind::INTS_DIVISION: return THEORY_ARITH;
514
16379
  case kind::INTS_DIVISION_TOTAL: return THEORY_ARITH;
515
1859
  case kind::INTS_MODULUS: return THEORY_ARITH;
516
18460
  case kind::INTS_MODULUS_TOTAL: return THEORY_ARITH;
517
86
  case kind::ABS: return THEORY_ARITH;
518
  case kind::DIVISIBLE: return THEORY_ARITH;
519
394
  case kind::POW: return THEORY_ARITH;
520
22488
  case kind::EXPONENTIAL: return THEORY_ARITH;
521
99815
  case kind::SINE: return THEORY_ARITH;
522
381
  case kind::COSINE: return THEORY_ARITH;
523
51
  case kind::TANGENT: return THEORY_ARITH;
524
12
  case kind::COSECANT: return THEORY_ARITH;
525
12
  case kind::SECANT: return THEORY_ARITH;
526
24
  case kind::COTANGENT: return THEORY_ARITH;
527
36
  case kind::ARCSINE: return THEORY_ARITH;
528
36
  case kind::ARCCOSINE: return THEORY_ARITH;
529
109
  case kind::ARCTANGENT: return THEORY_ARITH;
530
  case kind::ARCCOSECANT: return THEORY_ARITH;
531
  case kind::ARCSECANT: return THEORY_ARITH;
532
  case kind::ARCCOTANGENT: return THEORY_ARITH;
533
524
  case kind::SQRT: return THEORY_ARITH;
534
  case kind::DIVISIBLE_OP: return THEORY_ARITH;
535
13135363
  case kind::CONST_RATIONAL: return THEORY_ARITH;
536
323719
  case kind::LT: return THEORY_ARITH;
537
683920
  case kind::LEQ: return THEORY_ARITH;
538
138103
  case kind::GT: return THEORY_ARITH;
539
16340244
  case kind::GEQ: return THEORY_ARITH;
540
  case kind::INDEXED_ROOT_PREDICATE_OP: return THEORY_ARITH;
541
  case kind::INDEXED_ROOT_PREDICATE: return THEORY_ARITH;
542
376
  case kind::IS_INTEGER: return THEORY_ARITH;
543
4380
  case kind::TO_INTEGER: return THEORY_ARITH;
544
91
  case kind::TO_REAL: return THEORY_ARITH;
545
17690
  case kind::CAST_TO_REAL: return THEORY_ARITH;
546
29309
  case kind::PI: return THEORY_ARITH;
547
  case kind::IAND_OP: return THEORY_ARITH;
548
14577
  case kind::IAND: return THEORY_ARITH;
549
7198731
  case kind::BITVECTOR_TYPE: return THEORY_BV;
550
6491633
  case kind::CONST_BITVECTOR: return THEORY_BV;
551
1023769
  case kind::BITVECTOR_CONCAT: return THEORY_BV;
552
594189
  case kind::BITVECTOR_AND: return THEORY_BV;
553
637707
  case kind::BITVECTOR_COMP: return THEORY_BV;
554
803554
  case kind::BITVECTOR_OR: return THEORY_BV;
555
38742
  case kind::BITVECTOR_XOR: return THEORY_BV;
556
532233
  case kind::BITVECTOR_NOT: return THEORY_BV;
557
1610
  case kind::BITVECTOR_NAND: return THEORY_BV;
558
2177
  case kind::BITVECTOR_NOR: return THEORY_BV;
559
2325
  case kind::BITVECTOR_XNOR: return THEORY_BV;
560
1038408
  case kind::BITVECTOR_MULT: return THEORY_BV;
561
244966
  case kind::BITVECTOR_NEG: return THEORY_BV;
562
829940
  case kind::BITVECTOR_PLUS: return THEORY_BV;
563
7346
  case kind::BITVECTOR_SUB: return THEORY_BV;
564
120238
  case kind::BITVECTOR_UDIV: return THEORY_BV;
565
127824
  case kind::BITVECTOR_UREM: return THEORY_BV;
566
378
  case kind::BITVECTOR_SDIV: return THEORY_BV;
567
306
  case kind::BITVECTOR_SMOD: return THEORY_BV;
568
193
  case kind::BITVECTOR_SREM: return THEORY_BV;
569
53539
  case kind::BITVECTOR_ASHR: return THEORY_BV;
570
250249
  case kind::BITVECTOR_LSHR: return THEORY_BV;
571
236355
  case kind::BITVECTOR_SHL: return THEORY_BV;
572
7474
  case kind::BITVECTOR_ULE: return THEORY_BV;
573
866017
  case kind::BITVECTOR_ULT: return THEORY_BV;
574
4068
  case kind::BITVECTOR_UGE: return THEORY_BV;
575
4409
  case kind::BITVECTOR_UGT: return THEORY_BV;
576
7885
  case kind::BITVECTOR_SLE: return THEORY_BV;
577
913531
  case kind::BITVECTOR_SLT: return THEORY_BV;
578
4241
  case kind::BITVECTOR_SGE: return THEORY_BV;
579
4548
  case kind::BITVECTOR_SGT: return THEORY_BV;
580
24124
  case kind::BITVECTOR_ULTBV: return THEORY_BV;
581
38622
  case kind::BITVECTOR_SLTBV: return THEORY_BV;
582
  case kind::BITVECTOR_REDAND: return THEORY_BV;
583
  case kind::BITVECTOR_REDOR: return THEORY_BV;
584
142335
  case kind::BITVECTOR_ITE: return THEORY_BV;
585
306027
  case kind::BITVECTOR_TO_NAT: return THEORY_BV;
586
  case kind::BITVECTOR_ACKERMANNIZE_UDIV: return THEORY_BV;
587
  case kind::BITVECTOR_ACKERMANNIZE_UREM: return THEORY_BV;
588
5298
  case kind::BITVECTOR_EAGER_ATOM: return THEORY_BV;
589
  case kind::BITVECTOR_BITOF_OP: return THEORY_BV;
590
3344393
  case kind::BITVECTOR_BITOF: return THEORY_BV;
591
  case kind::BITVECTOR_EXTRACT_OP: return THEORY_BV;
592
711168
  case kind::BITVECTOR_EXTRACT: return THEORY_BV;
593
  case kind::BITVECTOR_REPEAT_OP: return THEORY_BV;
594
2015
  case kind::BITVECTOR_REPEAT: return THEORY_BV;
595
  case kind::BITVECTOR_ROTATE_LEFT_OP: return THEORY_BV;
596
1673
  case kind::BITVECTOR_ROTATE_LEFT: return THEORY_BV;
597
  case kind::BITVECTOR_ROTATE_RIGHT_OP: return THEORY_BV;
598
2197
  case kind::BITVECTOR_ROTATE_RIGHT: return THEORY_BV;
599
  case kind::BITVECTOR_SIGN_EXTEND_OP: return THEORY_BV;
600
240352
  case kind::BITVECTOR_SIGN_EXTEND: return THEORY_BV;
601
  case kind::BITVECTOR_ZERO_EXTEND_OP: return THEORY_BV;
602
17879
  case kind::BITVECTOR_ZERO_EXTEND: return THEORY_BV;
603
  case kind::INT_TO_BITVECTOR_OP: return THEORY_BV;
604
10872
  case kind::INT_TO_BITVECTOR: return THEORY_BV;
605
21194
  case kind::CONST_FLOATINGPOINT: return THEORY_FP;
606
4783
  case kind::CONST_ROUNDINGMODE: return THEORY_FP;
607
35382
  case kind::FLOATINGPOINT_TYPE: return THEORY_FP;
608
872
  case kind::FLOATINGPOINT_FP: return THEORY_FP;
609
16
  case kind::FLOATINGPOINT_EQ: return THEORY_FP;
610
255
  case kind::FLOATINGPOINT_ABS: return THEORY_FP;
611
3174
  case kind::FLOATINGPOINT_NEG: return THEORY_FP;
612
7198
  case kind::FLOATINGPOINT_PLUS: return THEORY_FP;
613
36
  case kind::FLOATINGPOINT_SUB: return THEORY_FP;
614
1293
  case kind::FLOATINGPOINT_MULT: return THEORY_FP;
615
1351
  case kind::FLOATINGPOINT_DIV: return THEORY_FP;
616
  case kind::FLOATINGPOINT_FMA: return THEORY_FP;
617
120
  case kind::FLOATINGPOINT_SQRT: return THEORY_FP;
618
1160
  case kind::FLOATINGPOINT_REM: return THEORY_FP;
619
1800
  case kind::FLOATINGPOINT_RTI: return THEORY_FP;
620
  case kind::FLOATINGPOINT_MIN: return THEORY_FP;
621
1862
  case kind::FLOATINGPOINT_MAX: return THEORY_FP;
622
  case kind::FLOATINGPOINT_MIN_TOTAL: return THEORY_FP;
623
  case kind::FLOATINGPOINT_MAX_TOTAL: return THEORY_FP;
624
3150
  case kind::FLOATINGPOINT_LEQ: return THEORY_FP;
625
508
  case kind::FLOATINGPOINT_LT: return THEORY_FP;
626
24
  case kind::FLOATINGPOINT_GEQ: return THEORY_FP;
627
4
  case kind::FLOATINGPOINT_GT: return THEORY_FP;
628
68
  case kind::FLOATINGPOINT_ISN: return THEORY_FP;
629
223
  case kind::FLOATINGPOINT_ISSN: return THEORY_FP;
630
1882
  case kind::FLOATINGPOINT_ISZ: return THEORY_FP;
631
2403
  case kind::FLOATINGPOINT_ISINF: return THEORY_FP;
632
1125
  case kind::FLOATINGPOINT_ISNAN: return THEORY_FP;
633
1680
  case kind::FLOATINGPOINT_ISNEG: return THEORY_FP;
634
272
  case kind::FLOATINGPOINT_ISPOS: return THEORY_FP;
635
  case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP: return THEORY_FP;
636
1232
  case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: return THEORY_FP;
637
  case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP: return THEORY_FP;
638
160
  case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT: return THEORY_FP;
639
  case kind::FLOATINGPOINT_TO_FP_REAL_OP: return THEORY_FP;
640
69
  case kind::FLOATINGPOINT_TO_FP_REAL: return THEORY_FP;
641
  case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP: return THEORY_FP;
642
15
  case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: return THEORY_FP;
643
  case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP: return THEORY_FP;
644
  case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: return THEORY_FP;
645
  case kind::FLOATINGPOINT_TO_FP_GENERIC_OP: return THEORY_FP;
646
718
  case kind::FLOATINGPOINT_TO_FP_GENERIC: return THEORY_FP;
647
  case kind::FLOATINGPOINT_TO_UBV_OP: return THEORY_FP;
648
  case kind::FLOATINGPOINT_TO_UBV: return THEORY_FP;
649
  case kind::FLOATINGPOINT_TO_UBV_TOTAL_OP: return THEORY_FP;
650
  case kind::FLOATINGPOINT_TO_UBV_TOTAL: return THEORY_FP;
651
  case kind::FLOATINGPOINT_TO_SBV_OP: return THEORY_FP;
652
  case kind::FLOATINGPOINT_TO_SBV: return THEORY_FP;
653
  case kind::FLOATINGPOINT_TO_SBV_TOTAL_OP: return THEORY_FP;
654
  case kind::FLOATINGPOINT_TO_SBV_TOTAL: return THEORY_FP;
655
424
  case kind::FLOATINGPOINT_TO_REAL: return THEORY_FP;
656
56
  case kind::FLOATINGPOINT_TO_REAL_TOTAL: return THEORY_FP;
657
9950
  case kind::FLOATINGPOINT_COMPONENT_NAN: return THEORY_FP;
658
10564
  case kind::FLOATINGPOINT_COMPONENT_INF: return THEORY_FP;
659
9689
  case kind::FLOATINGPOINT_COMPONENT_ZERO: return THEORY_FP;
660
9439
  case kind::FLOATINGPOINT_COMPONENT_SIGN: return THEORY_FP;
661
15310
  case kind::FLOATINGPOINT_COMPONENT_EXPONENT: return THEORY_FP;
662
15721
  case kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND: return THEORY_FP;
663
343
  case kind::ROUNDINGMODE_BITBLAST: return THEORY_FP;
664
320644
  case kind::ARRAY_TYPE: return THEORY_ARRAYS;
665
1092594
  case kind::SELECT: return THEORY_ARRAYS;
666
630867
  case kind::STORE: return THEORY_ARRAYS;
667
486
  case kind::EQ_RANGE: return THEORY_ARRAYS;
668
12679
  case kind::STORE_ALL: return THEORY_ARRAYS;
669
  case kind::ARR_TABLE_FUN: return THEORY_ARRAYS;
670
  case kind::ARRAY_LAMBDA: return THEORY_ARRAYS;
671
  case kind::PARTIAL_SELECT_0: return THEORY_ARRAYS;
672
  case kind::PARTIAL_SELECT_1: return THEORY_ARRAYS;
673
  case kind::CONSTRUCTOR_TYPE: return THEORY_DATATYPES;
674
  case kind::SELECTOR_TYPE: return THEORY_DATATYPES;
675
  case kind::TESTER_TYPE: return THEORY_DATATYPES;
676
2373835
  case kind::APPLY_CONSTRUCTOR: return THEORY_DATATYPES;
677
257305
  case kind::APPLY_SELECTOR: return THEORY_DATATYPES;
678
3157261
  case kind::APPLY_SELECTOR_TOTAL: return THEORY_DATATYPES;
679
3647856
  case kind::APPLY_TESTER: return THEORY_DATATYPES;
680
2824344
  case kind::DATATYPE_TYPE: return THEORY_DATATYPES;
681
12125
  case kind::PARAMETRIC_DATATYPE: return THEORY_DATATYPES;
682
  case kind::APPLY_TYPE_ASCRIPTION: return THEORY_DATATYPES;
683
  case kind::ASCRIPTION_TYPE: return THEORY_DATATYPES;
684
  case kind::TUPLE_UPDATE_OP: return THEORY_DATATYPES;
685
24
  case kind::TUPLE_UPDATE: return THEORY_DATATYPES;
686
  case kind::RECORD_UPDATE_OP: return THEORY_DATATYPES;
687
67
  case kind::RECORD_UPDATE: return THEORY_DATATYPES;
688
5555430
  case kind::DT_SIZE: return THEORY_DATATYPES;
689
  case kind::DT_HEIGHT_BOUND: return THEORY_DATATYPES;
690
  case kind::DT_SIZE_BOUND: return THEORY_DATATYPES;
691
112522
  case kind::DT_SYGUS_BOUND: return THEORY_DATATYPES;
692
5425649
  case kind::DT_SYGUS_EVAL: return THEORY_DATATYPES;
693
36
  case kind::MATCH: return THEORY_DATATYPES;
694
80
  case kind::MATCH_CASE: return THEORY_DATATYPES;
695
32
  case kind::MATCH_BIND_CASE: return THEORY_DATATYPES;
696
  case kind::TUPLE_PROJECT_OP: return THEORY_DATATYPES;
697
12
  case kind::TUPLE_PROJECT: return THEORY_DATATYPES;
698
5067
  case kind::SEP_NIL: return THEORY_SEP;
699
1455
  case kind::SEP_EMP: return THEORY_SEP;
700
10918
  case kind::SEP_PTO: return THEORY_SEP;
701
7472
  case kind::SEP_STAR: return THEORY_SEP;
702
1101
  case kind::SEP_WAND: return THEORY_SEP;
703
21337
  case kind::SEP_LABEL: return THEORY_SEP;
704
17932
  case kind::EMPTYSET: return THEORY_SETS;
705
553542
  case kind::SET_TYPE: return THEORY_SETS;
706
84093
  case kind::UNION: return THEORY_SETS;
707
68234
  case kind::INTERSECTION: return THEORY_SETS;
708
45916
  case kind::SETMINUS: return THEORY_SETS;
709
2510
  case kind::SUBSET: return THEORY_SETS;
710
669016
  case kind::MEMBER: return THEORY_SETS;
711
  case kind::SINGLETON_OP: return THEORY_SETS;
712
128118
  case kind::SINGLETON: return THEORY_SETS;
713
40
  case kind::INSERT: return THEORY_SETS;
714
1369062
  case kind::CARD: return THEORY_SETS;
715
73
  case kind::COMPLEMENT: return THEORY_SETS;
716
4980
  case kind::UNIVERSE_SET: return THEORY_SETS;
717
827
  case kind::COMPREHENSION: return THEORY_SETS;
718
915
  case kind::CHOOSE: return THEORY_SETS;
719
221
  case kind::IS_SINGLETON: return THEORY_SETS;
720
27836
  case kind::JOIN: return THEORY_SETS;
721
3697
  case kind::PRODUCT: return THEORY_SETS;
722
12454
  case kind::TRANSPOSE: return THEORY_SETS;
723
4446
  case kind::TCLOSURE: return THEORY_SETS;
724
1435
  case kind::JOIN_IMAGE: return THEORY_SETS;
725
296
  case kind::IDEN: return THEORY_SETS;
726
552
  case kind::EMPTYBAG: return THEORY_BAGS;
727
19847
  case kind::BAG_TYPE: return THEORY_BAGS;
728
488
  case kind::UNION_MAX: return THEORY_BAGS;
729
2457
  case kind::UNION_DISJOINT: return THEORY_BAGS;
730
1452
  case kind::INTERSECTION_MIN: return THEORY_BAGS;
731
446
  case kind::DIFFERENCE_SUBTRACT: return THEORY_BAGS;
732
  case kind::DIFFERENCE_REMOVE: return THEORY_BAGS;
733
26
  case kind::SUBBAG: return THEORY_BAGS;
734
493775
  case kind::BAG_COUNT: return THEORY_BAGS;
735
701
  case kind::DUPLICATE_REMOVAL: return THEORY_BAGS;
736
  case kind::MK_BAG_OP: return THEORY_BAGS;
737
4509
  case kind::MK_BAG: return THEORY_BAGS;
738
  case kind::BAG_IS_SINGLETON: return THEORY_BAGS;
739
  case kind::BAG_CARD: return THEORY_BAGS;
740
  case kind::BAG_FROM_SET: return THEORY_BAGS;
741
  case kind::BAG_TO_SET: return THEORY_BAGS;
742
  case kind::BAG_CHOOSE: return THEORY_BAGS;
743
741457
  case kind::STRING_CONCAT: return THEORY_STRINGS;
744
164014
  case kind::STRING_IN_REGEXP: return THEORY_STRINGS;
745
28548150
  case kind::STRING_LENGTH: return THEORY_STRINGS;
746
563089
  case kind::STRING_SUBSTR: return THEORY_STRINGS;
747
1970
  case kind::STRING_UPDATE: return THEORY_STRINGS;
748
582
  case kind::STRING_CHARAT: return THEORY_STRINGS;
749
190326
  case kind::STRING_STRCTN: return THEORY_STRINGS;
750
65
  case kind::STRING_LT: return THEORY_STRINGS;
751
6367
  case kind::STRING_LEQ: return THEORY_STRINGS;
752
650020
  case kind::STRING_STRIDOF: return THEORY_STRINGS;
753
135003
  case kind::STRING_STRREPL: return THEORY_STRINGS;
754
2732
  case kind::STRING_STRREPLALL: return THEORY_STRINGS;
755
3433
  case kind::STRING_REPLACE_RE: return THEORY_STRINGS;
756
2669
  case kind::STRING_REPLACE_RE_ALL: return THEORY_STRINGS;
757
346
  case kind::STRING_PREFIX: return THEORY_STRINGS;
758
115
  case kind::STRING_SUFFIX: return THEORY_STRINGS;
759
26
  case kind::STRING_IS_DIGIT: return THEORY_STRINGS;
760
12938
  case kind::STRING_ITOS: return THEORY_STRINGS;
761
50093
  case kind::STRING_STOI: return THEORY_STRINGS;
762
1509567
  case kind::STRING_TO_CODE: return THEORY_STRINGS;
763
576
  case kind::STRING_FROM_CODE: return THEORY_STRINGS;
764
1106
  case kind::STRING_TOLOWER: return THEORY_STRINGS;
765
954
  case kind::STRING_TOUPPER: return THEORY_STRINGS;
766
2189
  case kind::STRING_REV: return THEORY_STRINGS;
767
647274
  case kind::CONST_STRING: return THEORY_STRINGS;
768
47787
  case kind::SEQUENCE_TYPE: return THEORY_STRINGS;
769
9682
  case kind::CONST_SEQUENCE: return THEORY_STRINGS;
770
5161
  case kind::SEQ_UNIT: return THEORY_STRINGS;
771
30620
  case kind::SEQ_NTH: return THEORY_STRINGS;
772
16
  case kind::SEQ_NTH_TOTAL: return THEORY_STRINGS;
773
28057
  case kind::STRING_TO_REGEXP: return THEORY_STRINGS;
774
29308
  case kind::REGEXP_CONCAT: return THEORY_STRINGS;
775
6745
  case kind::REGEXP_UNION: return THEORY_STRINGS;
776
1732
  case kind::REGEXP_INTER: return THEORY_STRINGS;
777
134
  case kind::REGEXP_DIFF: return THEORY_STRINGS;
778
22268
  case kind::REGEXP_STAR: return THEORY_STRINGS;
779
96
  case kind::REGEXP_PLUS: return THEORY_STRINGS;
780
74
  case kind::REGEXP_OPT: return THEORY_STRINGS;
781
7792
  case kind::REGEXP_RANGE: return THEORY_STRINGS;
782
1529
  case kind::REGEXP_COMPLEMENT: return THEORY_STRINGS;
783
341
  case kind::REGEXP_EMPTY: return THEORY_STRINGS;
784
4196
  case kind::REGEXP_SIGMA: return THEORY_STRINGS;
785
  case kind::REGEXP_REPEAT_OP: return THEORY_STRINGS;
786
12
  case kind::REGEXP_REPEAT: return THEORY_STRINGS;
787
  case kind::REGEXP_LOOP_OP: return THEORY_STRINGS;
788
76
  case kind::REGEXP_LOOP: return THEORY_STRINGS;
789
756
  case kind::REGEXP_RV: return THEORY_STRINGS;
790
1277629
  case kind::FORALL: return THEORY_QUANTIFIERS;
791
9580
  case kind::EXISTS: return THEORY_QUANTIFIERS;
792
122408
  case kind::INST_CONSTANT: return THEORY_QUANTIFIERS;
793
282308
  case kind::BOUND_VAR_LIST: return THEORY_QUANTIFIERS;
794
16152
  case kind::INST_PATTERN: return THEORY_QUANTIFIERS;
795
32
  case kind::INST_NO_PATTERN: return THEORY_QUANTIFIERS;
796
3789
  case kind::INST_ATTRIBUTE: return THEORY_QUANTIFIERS;
797
34736
  case kind::INST_PATTERN_LIST: return THEORY_QUANTIFIERS;
798
799
  case kind::LAST_KIND:
800
    break;
801
  }
802
  throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad kind");
803
}
804
805
36674973
TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant)
806
{
807
36674973
  switch (typeConstant)
808
  {
809
  case BUILTIN_OPERATOR_TYPE: return THEORY_BUILTIN;
810
4007432
  case BOOLEAN_TYPE: return THEORY_BOOL;
811
2294989
  case REAL_TYPE: return THEORY_ARITH;
812
27981012
  case INTEGER_TYPE: return THEORY_ARITH;
813
1405
  case ROUNDINGMODE_TYPE: return THEORY_FP;
814
2390095
  case STRING_TYPE: return THEORY_STRINGS;
815
40
  case REGEXP_TYPE: return THEORY_STRINGS;
816
  case BOUND_VAR_LIST_TYPE: return THEORY_QUANTIFIERS;
817
  case INST_PATTERN_TYPE: return THEORY_QUANTIFIERS;
818
  case INST_PATTERN_LIST_TYPE: return THEORY_QUANTIFIERS;
819
820
    case LAST_TYPE: break;
821
  }
822
  throw IllegalArgumentException(
823
      "", "k", __PRETTY_FUNCTION__, "bad type constant");
824
}
825
826
}/* CVC4::theory namespace */
827
}/* CVC4 namespace */