GCC Code Coverage Report
Directory: . Exec Total Coverage
File: build-coverage/src/expr/type_checker.cpp Lines: 831 933 89.1 %
Date: 2021-03-23 Branches: 1123 2204 51.0 %

Line Exec Source
1
/*********************                                                        */
2
/** type_checker.cpp
3
 **
4
 ** Copyright 2010-2014  New York University and The University of Iowa,
5
 ** and as below.
6
 **
7
 ** This file automatically generated by:
8
 **
9
 **     ../../../src/expr/mkexpr /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-23/src/expr/type_checker_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/type_checker_template.cpp */
30
31
/*********************                                                        */
32
/*! \file type_checker_template.cpp
33
 ** \verbatim
34
 ** Top contributors (to current version):
35
 **   Morgan Deters, Mathias Preiner, 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 TypeChecker implementation
43
 **
44
 ** TypeChecker implementation.
45
 **/
46
47
#include <sstream>
48
49
#include "expr/node_manager.h"
50
#include "expr/node_manager_attributes.h"
51
#include "expr/type_checker.h"
52
#include "expr/type_checker_util.h"
53
54
55
#include "theory/builtin/theory_builtin_type_rules.h"
56
#include "theory/booleans/theory_bool_type_rules.h"
57
#include "theory/uf/theory_uf_type_rules.h"
58
#include "theory/arith/theory_arith_type_rules.h"
59
#include "theory/bv/theory_bv_type_rules.h"
60
#include "theory/fp/theory_fp_type_rules.h"
61
#include "theory/arrays/theory_arrays_type_rules.h"
62
#include "theory/datatypes/theory_datatypes_type_rules.h"
63
#include "theory/sep/theory_sep_type_rules.h"
64
#include "theory/sets/theory_sets_type_rules.h"
65
#include "theory/bags/theory_bags_type_rules.h"
66
#include "theory/strings/theory_strings_type_rules.h"
67
#include "theory/quantifiers/theory_quantifiers_type_rules.h"
68
69
namespace CVC4 {
70
namespace expr {
71
72
26402693
TypeNode TypeChecker::computeType(NodeManager* nodeManager, TNode n, bool check)
73
{
74
26402693
  TypeNode typeNode;
75
76
  // Infer the type
77
26402693
  switch(n.getKind()) {
78
  case kind::VARIABLE:
79
  case kind::SKOLEM:
80
    typeNode = nodeManager->getAttribute(n, TypeAttr());
81
    break;
82
1877
  case kind::BUILTIN:
83
1877
    typeNode = nodeManager->builtinOperatorType();
84
1877
    break;
85
86
87
2559
  case kind::UNINTERPRETED_CONSTANT:
88
2559
    typeNode = ::CVC4::theory::builtin::UninterpretedConstantTypeRule::computeType(nodeManager, n, check);
89
2559
    break;
90
91
  case kind::ABSTRACT_VALUE:
92
    typeNode = ::CVC4::theory::builtin::AbstractValueTypeRule::computeType(nodeManager, n, check);
93
    break;
94
95
4946603
  case kind::EQUAL:
96
4946603
    typeNode = ::CVC4::theory::builtin::EqualityTypeRule::computeType(nodeManager, n, check);
97
4946525
    break;
98
99
10473
  case kind::DISTINCT:
100
10473
    typeNode = ::CVC4::theory::builtin::DistinctTypeRule::computeType(nodeManager, n, check);
101
10473
    break;
102
103
573910
  case kind::SEXPR:
104
573910
    typeNode = ::CVC4::theory::builtin::SExprTypeRule::computeType(nodeManager, n, check);
105
573910
    break;
106
107
22413
  case kind::LAMBDA:
108
22413
    typeNode = ::CVC4::theory::builtin::LambdaTypeRule::computeType(nodeManager, n, check);
109
22413
    break;
110
111
4368
  case kind::WITNESS:
112
4368
    typeNode = ::CVC4::theory::builtin::WitnessTypeRule::computeType(nodeManager, n, check);
113
4368
    break;
114
115
13376
  case kind::CONST_BOOLEAN:
116
13376
    typeNode = ::CVC4::theory::boolean::BooleanTypeRule::computeType(nodeManager, n, check);
117
13376
    break;
118
119
3958103
  case kind::NOT:
120
3958103
    typeNode = ::CVC4::theory::boolean::BooleanTypeRule::computeType(nodeManager, n, check);
121
3958089
    break;
122
123
3408762
  case kind::AND:
124
3408762
    typeNode = ::CVC4::theory::boolean::BooleanTypeRule::computeType(nodeManager, n, check);
125
3408684
    break;
126
127
461592
  case kind::IMPLIES:
128
461592
    typeNode = ::CVC4::theory::boolean::BooleanTypeRule::computeType(nodeManager, n, check);
129
461514
    break;
130
131
2704275
  case kind::OR:
132
2704275
    typeNode = ::CVC4::theory::boolean::BooleanTypeRule::computeType(nodeManager, n, check);
133
2704197
    break;
134
135
736668
  case kind::XOR:
136
736668
    typeNode = ::CVC4::theory::boolean::BooleanTypeRule::computeType(nodeManager, n, check);
137
736590
    break;
138
139
1786722
  case kind::ITE:
140
1786722
    typeNode = ::CVC4::theory::boolean::IteTypeRule::computeType(nodeManager, n, check);
141
1786690
    break;
142
143
451779
  case kind::APPLY_UF:
144
451779
    typeNode = ::CVC4::theory::uf::UfTypeRule::computeType(nodeManager, n, check);
145
451779
    break;
146
147
1038
  case kind::CARDINALITY_CONSTRAINT:
148
1038
    typeNode = ::CVC4::theory::uf::CardinalityConstraintTypeRule::computeType(nodeManager, n, check);
149
1038
    break;
150
151
587
  case kind::COMBINED_CARDINALITY_CONSTRAINT:
152
587
    typeNode = ::CVC4::theory::uf::CombinedCardinalityConstraintTypeRule::computeType(nodeManager, n, check);
153
587
    break;
154
155
  case kind::PARTIAL_APPLY_UF:
156
    typeNode = ::CVC4::theory::uf::PartialTypeRule::computeType(nodeManager, n, check);
157
    break;
158
159
  case kind::CARDINALITY_VALUE:
160
    typeNode = ::CVC4::theory::uf::CardinalityValueTypeRule::computeType(nodeManager, n, check);
161
    break;
162
163
14925
  case kind::HO_APPLY:
164
14925
    typeNode = ::CVC4::theory::uf::HoApplyTypeRule::computeType(nodeManager, n, check);
165
14925
    break;
166
167
2597634
  case kind::PLUS:
168
2597634
    typeNode = ::CVC4::theory::arith::ArithOperatorTypeRule::computeType(nodeManager, n, check);
169
2597634
    break;
170
171
582879
  case kind::MULT:
172
582879
    typeNode = ::CVC4::theory::arith::ArithOperatorTypeRule::computeType(nodeManager, n, check);
173
582879
    break;
174
175
24492
  case kind::NONLINEAR_MULT:
176
24492
    typeNode = ::CVC4::theory::arith::ArithOperatorTypeRule::computeType(nodeManager, n, check);
177
24492
    break;
178
179
263434
  case kind::MINUS:
180
263434
    typeNode = ::CVC4::theory::arith::ArithOperatorTypeRule::computeType(nodeManager, n, check);
181
263434
    break;
182
183
11741
  case kind::UMINUS:
184
11741
    typeNode = ::CVC4::theory::arith::ArithOperatorTypeRule::computeType(nodeManager, n, check);
185
11741
    break;
186
187
2540
  case kind::DIVISION:
188
2540
    typeNode = ::CVC4::theory::arith::ArithOperatorTypeRule::computeType(nodeManager, n, check);
189
2540
    break;
190
191
115
  case kind::POW:
192
115
    typeNode = ::CVC4::theory::arith::ArithOperatorTypeRule::computeType(nodeManager, n, check);
193
115
    break;
194
195
236097
  case kind::CONST_RATIONAL:
196
236097
    typeNode = ::CVC4::theory::arith::ArithConstantTypeRule::computeType(nodeManager, n, check);
197
236097
    break;
198
199
109210
  case kind::LT:
200
109210
    typeNode = SimpleTypeRule<RBool, AReal, AReal>::computeType(nodeManager, n, check);
201
109210
    break;
202
203
165865
  case kind::LEQ:
204
165865
    typeNode = SimpleTypeRule<RBool, AReal, AReal>::computeType(nodeManager, n, check);
205
165865
    break;
206
207
81014
  case kind::GT:
208
81014
    typeNode = SimpleTypeRule<RBool, AReal, AReal>::computeType(nodeManager, n, check);
209
81014
    break;
210
211
517431
  case kind::GEQ:
212
517431
    typeNode = SimpleTypeRule<RBool, AReal, AReal>::computeType(nodeManager, n, check);
213
517431
    break;
214
215
  case kind::INDEXED_ROOT_PREDICATE_OP:
216
    typeNode = SimpleTypeRule<RBuiltinOperator>::computeType(nodeManager, n, check);
217
    break;
218
219
  case kind::INDEXED_ROOT_PREDICATE:
220
    typeNode = ::CVC4::theory::arith::IndexedRootPredicateTypeRule::computeType(nodeManager, n, check);
221
    break;
222
223
54
  case kind::TO_REAL:
224
54
    typeNode = ::CVC4::theory::arith::ArithOperatorTypeRule::computeType(nodeManager, n, check);
225
54
    break;
226
227
1474
  case kind::CAST_TO_REAL:
228
1474
    typeNode = ::CVC4::theory::arith::ArithOperatorTypeRule::computeType(nodeManager, n, check);
229
1474
    break;
230
231
540
  case kind::TO_INTEGER:
232
540
    typeNode = ::CVC4::theory::arith::ArithOperatorTypeRule::computeType(nodeManager, n, check);
233
540
    break;
234
235
25
  case kind::IS_INTEGER:
236
25
    typeNode = SimpleTypeRule<RBool, AReal>::computeType(nodeManager, n, check);
237
25
    break;
238
239
22
  case kind::ABS:
240
22
    typeNode = SimpleTypeRule<RInteger, AInteger>::computeType(nodeManager, n, check);
241
22
    break;
242
243
437
  case kind::INTS_DIVISION:
244
437
    typeNode = SimpleTypeRule<RInteger, AInteger, AInteger>::computeType(nodeManager, n, check);
245
437
    break;
246
247
447
  case kind::INTS_MODULUS:
248
447
    typeNode = SimpleTypeRule<RInteger, AInteger, AInteger>::computeType(nodeManager, n, check);
249
447
    break;
250
251
6
  case kind::DIVISIBLE:
252
6
    typeNode = SimpleTypeRule<RBool, AInteger>::computeType(nodeManager, n, check);
253
4
    break;
254
255
8
  case kind::DIVISIBLE_OP:
256
8
    typeNode = SimpleTypeRule<RBuiltinOperator>::computeType(nodeManager, n, check);
257
8
    break;
258
259
242
  case kind::DIVISION_TOTAL:
260
242
    typeNode = ::CVC4::theory::arith::ArithOperatorTypeRule::computeType(nodeManager, n, check);
261
242
    break;
262
263
1888
  case kind::INTS_DIVISION_TOTAL:
264
1888
    typeNode = SimpleTypeRule<RInteger, AInteger, AInteger>::computeType(nodeManager, n, check);
265
1888
    break;
266
267
3349
  case kind::INTS_MODULUS_TOTAL:
268
3349
    typeNode = SimpleTypeRule<RInteger, AInteger, AInteger>::computeType(nodeManager, n, check);
269
3349
    break;
270
271
258
  case kind::EXPONENTIAL:
272
258
    typeNode = SimpleTypeRule<RReal, AReal>::computeType(nodeManager, n, check);
273
258
    break;
274
275
1532
  case kind::SINE:
276
1532
    typeNode = SimpleTypeRule<RReal, AReal>::computeType(nodeManager, n, check);
277
1532
    break;
278
279
72
  case kind::COSINE:
280
72
    typeNode = SimpleTypeRule<RReal, AReal>::computeType(nodeManager, n, check);
281
72
    break;
282
283
20
  case kind::TANGENT:
284
20
    typeNode = SimpleTypeRule<RReal, AReal>::computeType(nodeManager, n, check);
285
20
    break;
286
287
6
  case kind::COSECANT:
288
6
    typeNode = SimpleTypeRule<RReal, AReal>::computeType(nodeManager, n, check);
289
6
    break;
290
291
6
  case kind::SECANT:
292
6
    typeNode = SimpleTypeRule<RReal, AReal>::computeType(nodeManager, n, check);
293
6
    break;
294
295
12
  case kind::COTANGENT:
296
12
    typeNode = SimpleTypeRule<RReal, AReal>::computeType(nodeManager, n, check);
297
12
    break;
298
299
3
  case kind::ARCSINE:
300
3
    typeNode = SimpleTypeRule<RReal, AReal>::computeType(nodeManager, n, check);
301
3
    break;
302
303
3
  case kind::ARCCOSINE:
304
3
    typeNode = SimpleTypeRule<RReal, AReal>::computeType(nodeManager, n, check);
305
3
    break;
306
307
13
  case kind::ARCTANGENT:
308
13
    typeNode = SimpleTypeRule<RReal, AReal>::computeType(nodeManager, n, check);
309
13
    break;
310
311
  case kind::ARCCOSECANT:
312
    typeNode = SimpleTypeRule<RReal, AReal>::computeType(nodeManager, n, check);
313
    break;
314
315
  case kind::ARCSECANT:
316
    typeNode = SimpleTypeRule<RReal, AReal>::computeType(nodeManager, n, check);
317
    break;
318
319
  case kind::ARCCOTANGENT:
320
    typeNode = SimpleTypeRule<RReal, AReal>::computeType(nodeManager, n, check);
321
    break;
322
323
25
  case kind::SQRT:
324
25
    typeNode = SimpleTypeRule<RReal, AReal>::computeType(nodeManager, n, check);
325
25
    break;
326
327
1421
  case kind::PI:
328
1421
    typeNode = ::CVC4::theory::arith::RealNullaryOperatorTypeRule::computeType(nodeManager, n, check);
329
1421
    break;
330
331
61
  case kind::IAND_OP:
332
61
    typeNode = ::CVC4::theory::arith::IAndOpTypeRule::computeType(nodeManager, n, check);
333
61
    break;
334
335
259
  case kind::IAND:
336
259
    typeNode = ::CVC4::theory::arith::IAndTypeRule::computeType(nodeManager, n, check);
337
259
    break;
338
339
81523
  case kind::CONST_BITVECTOR:
340
81523
    typeNode = ::CVC4::theory::bv::BitVectorConstantTypeRule::computeType(nodeManager, n, check);
341
81523
    break;
342
343
112033
  case kind::BITVECTOR_CONCAT:
344
112033
    typeNode = ::CVC4::theory::bv::BitVectorConcatTypeRule::computeType(nodeManager, n, check);
345
112033
    break;
346
347
118220
  case kind::BITVECTOR_AND:
348
118220
    typeNode = ::CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check);
349
118220
    break;
350
351
152253
  case kind::BITVECTOR_COMP:
352
152253
    typeNode = ::CVC4::theory::bv::BitVectorBVPredTypeRule::computeType(nodeManager, n, check);
353
152253
    break;
354
355
325
  case kind::BITVECTOR_NAND:
356
325
    typeNode = ::CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check);
357
325
    break;
358
359
412
  case kind::BITVECTOR_NOR:
360
412
    typeNode = ::CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check);
361
412
    break;
362
363
74229
  case kind::BITVECTOR_NOT:
364
74229
    typeNode = ::CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check);
365
74229
    break;
366
367
172807
  case kind::BITVECTOR_OR:
368
172807
    typeNode = ::CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check);
369
172807
    break;
370
371
502
  case kind::BITVECTOR_XNOR:
372
502
    typeNode = ::CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check);
373
502
    break;
374
375
8155
  case kind::BITVECTOR_XOR:
376
8155
    typeNode = ::CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check);
377
8155
    break;
378
379
334367
  case kind::BITVECTOR_MULT:
380
334367
    typeNode = ::CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check);
381
334367
    break;
382
383
18313
  case kind::BITVECTOR_NEG:
384
18313
    typeNode = ::CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check);
385
18313
    break;
386
387
107338
  case kind::BITVECTOR_PLUS:
388
107338
    typeNode = ::CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check);
389
107338
    break;
390
391
2781
  case kind::BITVECTOR_SUB:
392
2781
    typeNode = ::CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check);
393
2781
    break;
394
395
25094
  case kind::BITVECTOR_UDIV:
396
25094
    typeNode = ::CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check);
397
25094
    break;
398
399
26100
  case kind::BITVECTOR_UREM:
400
26100
    typeNode = ::CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check);
401
26100
    break;
402
403
158
  case kind::BITVECTOR_SDIV:
404
158
    typeNode = ::CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check);
405
158
    break;
406
407
57
  case kind::BITVECTOR_SMOD:
408
57
    typeNode = ::CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check);
409
57
    break;
410
411
87
  case kind::BITVECTOR_SREM:
412
87
    typeNode = ::CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check);
413
87
    break;
414
415
2829
  case kind::BITVECTOR_ASHR:
416
2829
    typeNode = ::CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check);
417
2829
    break;
418
419
23166
  case kind::BITVECTOR_LSHR:
420
23166
    typeNode = ::CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check);
421
23166
    break;
422
423
19487
  case kind::BITVECTOR_SHL:
424
19487
    typeNode = ::CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check);
425
19487
    break;
426
427
5856
  case kind::BITVECTOR_ULE:
428
5856
    typeNode = ::CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(nodeManager, n, check);
429
5856
    break;
430
431
35993
  case kind::BITVECTOR_ULT:
432
35993
    typeNode = ::CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(nodeManager, n, check);
433
35993
    break;
434
435
2874
  case kind::BITVECTOR_UGE:
436
2874
    typeNode = ::CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(nodeManager, n, check);
437
2874
    break;
438
439
3291
  case kind::BITVECTOR_UGT:
440
3291
    typeNode = ::CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(nodeManager, n, check);
441
3291
    break;
442
443
5989
  case kind::BITVECTOR_SLE:
444
5989
    typeNode = ::CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(nodeManager, n, check);
445
5989
    break;
446
447
36341
  case kind::BITVECTOR_SLT:
448
36341
    typeNode = ::CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(nodeManager, n, check);
449
36341
    break;
450
451
2960
  case kind::BITVECTOR_SGE:
452
2960
    typeNode = ::CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(nodeManager, n, check);
453
2960
    break;
454
455
3217
  case kind::BITVECTOR_SGT:
456
3217
    typeNode = ::CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(nodeManager, n, check);
457
3217
    break;
458
459
1382
  case kind::BITVECTOR_ULTBV:
460
1382
    typeNode = ::CVC4::theory::bv::BitVectorBVPredTypeRule::computeType(nodeManager, n, check);
461
1382
    break;
462
463
4044
  case kind::BITVECTOR_SLTBV:
464
4044
    typeNode = ::CVC4::theory::bv::BitVectorBVPredTypeRule::computeType(nodeManager, n, check);
465
4044
    break;
466
467
10125
  case kind::BITVECTOR_ITE:
468
10125
    typeNode = ::CVC4::theory::bv::BitVectorITETypeRule::computeType(nodeManager, n, check);
469
10125
    break;
470
471
  case kind::BITVECTOR_REDAND:
472
    typeNode = ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule::computeType(nodeManager, n, check);
473
    break;
474
475
  case kind::BITVECTOR_REDOR:
476
    typeNode = ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule::computeType(nodeManager, n, check);
477
    break;
478
479
465
  case kind::BITVECTOR_TO_NAT:
480
465
    typeNode = ::CVC4::theory::bv::BitVectorConversionTypeRule::computeType(nodeManager, n, check);
481
465
    break;
482
483
  case kind::BITVECTOR_ACKERMANNIZE_UDIV:
484
    typeNode = ::CVC4::theory::bv::BitVectorAckermanizationUdivTypeRule::computeType(nodeManager, n, check);
485
    break;
486
487
  case kind::BITVECTOR_ACKERMANNIZE_UREM:
488
    typeNode = ::CVC4::theory::bv::BitVectorAckermanizationUremTypeRule::computeType(nodeManager, n, check);
489
    break;
490
491
237
  case kind::BITVECTOR_EAGER_ATOM:
492
237
    typeNode = ::CVC4::theory::bv::BitVectorEagerAtomTypeRule::computeType(nodeManager, n, check);
493
237
    break;
494
495
  case kind::BITVECTOR_BITOF_OP:
496
    typeNode = SimpleTypeRule<RBuiltinOperator>::computeType(nodeManager, n, check);
497
    break;
498
499
167018
  case kind::BITVECTOR_BITOF:
500
167018
    typeNode = ::CVC4::theory::bv::BitVectorBitOfTypeRule::computeType(nodeManager, n, check);
501
167018
    break;
502
503
1637
  case kind::BITVECTOR_EXTRACT_OP:
504
1637
    typeNode = SimpleTypeRule<RBuiltinOperator>::computeType(nodeManager, n, check);
505
1637
    break;
506
507
124012
  case kind::BITVECTOR_EXTRACT:
508
124012
    typeNode = ::CVC4::theory::bv::BitVectorExtractTypeRule::computeType(nodeManager, n, check);
509
124012
    break;
510
511
220
  case kind::BITVECTOR_REPEAT_OP:
512
220
    typeNode = SimpleTypeRule<RBuiltinOperator>::computeType(nodeManager, n, check);
513
220
    break;
514
515
419
  case kind::BITVECTOR_REPEAT:
516
419
    typeNode = ::CVC4::theory::bv::BitVectorRepeatTypeRule::computeType(nodeManager, n, check);
517
418
    break;
518
519
172
  case kind::BITVECTOR_ROTATE_LEFT_OP:
520
172
    typeNode = SimpleTypeRule<RBuiltinOperator>::computeType(nodeManager, n, check);
521
172
    break;
522
523
350
  case kind::BITVECTOR_ROTATE_LEFT:
524
350
    typeNode = ::CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check);
525
350
    break;
526
527
205
  case kind::BITVECTOR_ROTATE_RIGHT_OP:
528
205
    typeNode = SimpleTypeRule<RBuiltinOperator>::computeType(nodeManager, n, check);
529
205
    break;
530
531
397
  case kind::BITVECTOR_ROTATE_RIGHT:
532
397
    typeNode = ::CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check);
533
397
    break;
534
535
1202
  case kind::BITVECTOR_SIGN_EXTEND_OP:
536
1202
    typeNode = SimpleTypeRule<RBuiltinOperator>::computeType(nodeManager, n, check);
537
1202
    break;
538
539
21837
  case kind::BITVECTOR_SIGN_EXTEND:
540
21837
    typeNode = ::CVC4::theory::bv::BitVectorExtendTypeRule::computeType(nodeManager, n, check);
541
21837
    break;
542
543
1213
  case kind::BITVECTOR_ZERO_EXTEND_OP:
544
1213
    typeNode = SimpleTypeRule<RBuiltinOperator>::computeType(nodeManager, n, check);
545
1213
    break;
546
547
9605
  case kind::BITVECTOR_ZERO_EXTEND:
548
9605
    typeNode = ::CVC4::theory::bv::BitVectorExtendTypeRule::computeType(nodeManager, n, check);
549
9605
    break;
550
551
17
  case kind::INT_TO_BITVECTOR_OP:
552
17
    typeNode = ::CVC4::theory::bv::IntToBitVectorOpTypeRule::computeType(nodeManager, n, check);
553
16
    break;
554
555
530
  case kind::INT_TO_BITVECTOR:
556
530
    typeNode = ::CVC4::theory::bv::BitVectorConversionTypeRule::computeType(nodeManager, n, check);
557
530
    break;
558
559
480
  case kind::CONST_FLOATINGPOINT:
560
480
    typeNode = ::CVC4::theory::fp::FloatingPointConstantTypeRule::computeType(nodeManager, n, check);
561
480
    break;
562
563
6634
  case kind::CONST_ROUNDINGMODE:
564
6634
    typeNode = ::CVC4::theory::fp::RoundingModeConstantTypeRule::computeType(nodeManager, n, check);
565
6634
    break;
566
567
22
  case kind::FLOATINGPOINT_FP:
568
22
    typeNode = ::CVC4::theory::fp::FloatingPointFPTypeRule::computeType(nodeManager, n, check);
569
22
    break;
570
571
7
  case kind::FLOATINGPOINT_EQ:
572
7
    typeNode = ::CVC4::theory::fp::FloatingPointTestTypeRule::computeType(nodeManager, n, check);
573
7
    break;
574
575
34
  case kind::FLOATINGPOINT_ABS:
576
34
    typeNode = ::CVC4::theory::fp::FloatingPointOperationTypeRule::computeType(nodeManager, n, check);
577
34
    break;
578
579
311
  case kind::FLOATINGPOINT_NEG:
580
311
    typeNode = ::CVC4::theory::fp::FloatingPointOperationTypeRule::computeType(nodeManager, n, check);
581
311
    break;
582
583
1009
  case kind::FLOATINGPOINT_PLUS:
584
1009
    typeNode = ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule::computeType(nodeManager, n, check);
585
1009
    break;
586
587
54
  case kind::FLOATINGPOINT_SUB:
588
54
    typeNode = ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule::computeType(nodeManager, n, check);
589
54
    break;
590
591
228
  case kind::FLOATINGPOINT_MULT:
592
228
    typeNode = ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule::computeType(nodeManager, n, check);
593
228
    break;
594
595
265
  case kind::FLOATINGPOINT_DIV:
596
265
    typeNode = ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule::computeType(nodeManager, n, check);
597
265
    break;
598
599
  case kind::FLOATINGPOINT_FMA:
600
    typeNode = ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule::computeType(nodeManager, n, check);
601
    break;
602
603
42
  case kind::FLOATINGPOINT_SQRT:
604
42
    typeNode = ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule::computeType(nodeManager, n, check);
605
42
    break;
606
607
149
  case kind::FLOATINGPOINT_REM:
608
149
    typeNode = ::CVC4::theory::fp::FloatingPointOperationTypeRule::computeType(nodeManager, n, check);
609
149
    break;
610
611
131
  case kind::FLOATINGPOINT_RTI:
612
131
    typeNode = ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule::computeType(nodeManager, n, check);
613
131
    break;
614
615
  case kind::FLOATINGPOINT_MIN:
616
    typeNode = ::CVC4::theory::fp::FloatingPointOperationTypeRule::computeType(nodeManager, n, check);
617
    break;
618
619
333
  case kind::FLOATINGPOINT_MAX:
620
333
    typeNode = ::CVC4::theory::fp::FloatingPointOperationTypeRule::computeType(nodeManager, n, check);
621
333
    break;
622
623
  case kind::FLOATINGPOINT_MIN_TOTAL:
624
    typeNode = ::CVC4::theory::fp::FloatingPointPartialOperationTypeRule::computeType(nodeManager, n, check);
625
    break;
626
627
  case kind::FLOATINGPOINT_MAX_TOTAL:
628
    typeNode = ::CVC4::theory::fp::FloatingPointPartialOperationTypeRule::computeType(nodeManager, n, check);
629
    break;
630
631
208
  case kind::FLOATINGPOINT_LEQ:
632
208
    typeNode = ::CVC4::theory::fp::FloatingPointTestTypeRule::computeType(nodeManager, n, check);
633
208
    break;
634
635
63
  case kind::FLOATINGPOINT_LT:
636
63
    typeNode = ::CVC4::theory::fp::FloatingPointTestTypeRule::computeType(nodeManager, n, check);
637
63
    break;
638
639
17
  case kind::FLOATINGPOINT_GEQ:
640
17
    typeNode = ::CVC4::theory::fp::FloatingPointTestTypeRule::computeType(nodeManager, n, check);
641
17
    break;
642
643
4
  case kind::FLOATINGPOINT_GT:
644
4
    typeNode = ::CVC4::theory::fp::FloatingPointTestTypeRule::computeType(nodeManager, n, check);
645
4
    break;
646
647
13
  case kind::FLOATINGPOINT_ISN:
648
13
    typeNode = ::CVC4::theory::fp::FloatingPointTestTypeRule::computeType(nodeManager, n, check);
649
13
    break;
650
651
18
  case kind::FLOATINGPOINT_ISSN:
652
18
    typeNode = ::CVC4::theory::fp::FloatingPointTestTypeRule::computeType(nodeManager, n, check);
653
18
    break;
654
655
365
  case kind::FLOATINGPOINT_ISZ:
656
365
    typeNode = ::CVC4::theory::fp::FloatingPointTestTypeRule::computeType(nodeManager, n, check);
657
365
    break;
658
659
88
  case kind::FLOATINGPOINT_ISINF:
660
88
    typeNode = ::CVC4::theory::fp::FloatingPointTestTypeRule::computeType(nodeManager, n, check);
661
88
    break;
662
663
66
  case kind::FLOATINGPOINT_ISNAN:
664
66
    typeNode = ::CVC4::theory::fp::FloatingPointTestTypeRule::computeType(nodeManager, n, check);
665
66
    break;
666
667
85
  case kind::FLOATINGPOINT_ISNEG:
668
85
    typeNode = ::CVC4::theory::fp::FloatingPointTestTypeRule::computeType(nodeManager, n, check);
669
85
    break;
670
671
17
  case kind::FLOATINGPOINT_ISPOS:
672
17
    typeNode = ::CVC4::theory::fp::FloatingPointTestTypeRule::computeType(nodeManager, n, check);
673
17
    break;
674
675
2
  case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP:
676
2
    typeNode = ::CVC4::theory::fp::FloatingPointParametricOpTypeRule::computeType(nodeManager, n, check);
677
2
    break;
678
679
445
  case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
680
445
    typeNode = ::CVC4::theory::fp::FloatingPointToFPIEEEBitVectorTypeRule::computeType(nodeManager, n, check);
681
445
    break;
682
683
2
  case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP:
684
2
    typeNode = ::CVC4::theory::fp::FloatingPointParametricOpTypeRule::computeType(nodeManager, n, check);
685
2
    break;
686
687
6
  case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT:
688
6
    typeNode = ::CVC4::theory::fp::FloatingPointToFPFloatingPointTypeRule::computeType(nodeManager, n, check);
689
6
    break;
690
691
2
  case kind::FLOATINGPOINT_TO_FP_REAL_OP:
692
2
    typeNode = ::CVC4::theory::fp::FloatingPointParametricOpTypeRule::computeType(nodeManager, n, check);
693
2
    break;
694
695
17
  case kind::FLOATINGPOINT_TO_FP_REAL:
696
17
    typeNode = ::CVC4::theory::fp::FloatingPointToFPRealTypeRule::computeType(nodeManager, n, check);
697
17
    break;
698
699
2
  case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP:
700
2
    typeNode = ::CVC4::theory::fp::FloatingPointParametricOpTypeRule::computeType(nodeManager, n, check);
701
2
    break;
702
703
3
  case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
704
3
    typeNode = ::CVC4::theory::fp::FloatingPointToFPSignedBitVectorTypeRule::computeType(nodeManager, n, check);
705
3
    break;
706
707
2
  case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP:
708
2
    typeNode = ::CVC4::theory::fp::FloatingPointParametricOpTypeRule::computeType(nodeManager, n, check);
709
2
    break;
710
711
  case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR:
712
    typeNode = ::CVC4::theory::fp::FloatingPointToFPUnsignedBitVectorTypeRule::computeType(nodeManager, n, check);
713
    break;
714
715
19
  case kind::FLOATINGPOINT_TO_FP_GENERIC_OP:
716
19
    typeNode = ::CVC4::theory::fp::FloatingPointParametricOpTypeRule::computeType(nodeManager, n, check);
717
19
    break;
718
719
46
  case kind::FLOATINGPOINT_TO_FP_GENERIC:
720
46
    typeNode = ::CVC4::theory::fp::FloatingPointToFPGenericTypeRule::computeType(nodeManager, n, check);
721
46
    break;
722
723
2
  case kind::FLOATINGPOINT_TO_UBV_OP:
724
2
    typeNode = ::CVC4::theory::fp::FloatingPointParametricOpTypeRule::computeType(nodeManager, n, check);
725
2
    break;
726
727
  case kind::FLOATINGPOINT_TO_UBV:
728
    typeNode = ::CVC4::theory::fp::FloatingPointToUBVTypeRule::computeType(nodeManager, n, check);
729
    break;
730
731
  case kind::FLOATINGPOINT_TO_UBV_TOTAL_OP:
732
    typeNode = ::CVC4::theory::fp::FloatingPointParametricOpTypeRule::computeType(nodeManager, n, check);
733
    break;
734
735
  case kind::FLOATINGPOINT_TO_UBV_TOTAL:
736
    typeNode = ::CVC4::theory::fp::FloatingPointToUBVTotalTypeRule::computeType(nodeManager, n, check);
737
    break;
738
739
2
  case kind::FLOATINGPOINT_TO_SBV_OP:
740
2
    typeNode = ::CVC4::theory::fp::FloatingPointParametricOpTypeRule::computeType(nodeManager, n, check);
741
2
    break;
742
743
  case kind::FLOATINGPOINT_TO_SBV:
744
    typeNode = ::CVC4::theory::fp::FloatingPointToSBVTypeRule::computeType(nodeManager, n, check);
745
    break;
746
747
  case kind::FLOATINGPOINT_TO_SBV_TOTAL_OP:
748
    typeNode = ::CVC4::theory::fp::FloatingPointParametricOpTypeRule::computeType(nodeManager, n, check);
749
    break;
750
751
  case kind::FLOATINGPOINT_TO_SBV_TOTAL:
752
    typeNode = ::CVC4::theory::fp::FloatingPointToSBVTotalTypeRule::computeType(nodeManager, n, check);
753
    break;
754
755
6
  case kind::FLOATINGPOINT_TO_REAL:
756
6
    typeNode = ::CVC4::theory::fp::FloatingPointToRealTypeRule::computeType(nodeManager, n, check);
757
6
    break;
758
759
12
  case kind::FLOATINGPOINT_TO_REAL_TOTAL:
760
12
    typeNode = ::CVC4::theory::fp::FloatingPointToRealTotalTypeRule::computeType(nodeManager, n, check);
761
12
    break;
762
763
105
  case kind::FLOATINGPOINT_COMPONENT_NAN:
764
105
    typeNode = ::CVC4::theory::fp::FloatingPointComponentBit::computeType(nodeManager, n, check);
765
105
    break;
766
767
105
  case kind::FLOATINGPOINT_COMPONENT_INF:
768
105
    typeNode = ::CVC4::theory::fp::FloatingPointComponentBit::computeType(nodeManager, n, check);
769
105
    break;
770
771
105
  case kind::FLOATINGPOINT_COMPONENT_ZERO:
772
105
    typeNode = ::CVC4::theory::fp::FloatingPointComponentBit::computeType(nodeManager, n, check);
773
105
    break;
774
775
105
  case kind::FLOATINGPOINT_COMPONENT_SIGN:
776
105
    typeNode = ::CVC4::theory::fp::FloatingPointComponentBit::computeType(nodeManager, n, check);
777
105
    break;
778
779
105
  case kind::FLOATINGPOINT_COMPONENT_EXPONENT:
780
105
    typeNode = ::CVC4::theory::fp::FloatingPointComponentExponent::computeType(nodeManager, n, check);
781
105
    break;
782
783
105
  case kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND:
784
105
    typeNode = ::CVC4::theory::fp::FloatingPointComponentSignificand::computeType(nodeManager, n, check);
785
105
    break;
786
787
1
  case kind::ROUNDINGMODE_BITBLAST:
788
1
    typeNode = ::CVC4::theory::fp::RoundingModeBitBlast::computeType(nodeManager, n, check);
789
1
    break;
790
791
17948
  case kind::SELECT:
792
17948
    typeNode = ::CVC4::theory::arrays::ArraySelectTypeRule::computeType(nodeManager, n, check);
793
17948
    break;
794
795
11997
  case kind::STORE:
796
11997
    typeNode = ::CVC4::theory::arrays::ArrayStoreTypeRule::computeType(nodeManager, n, check);
797
11997
    break;
798
799
646
  case kind::STORE_ALL:
800
646
    typeNode = ::CVC4::theory::arrays::ArrayStoreTypeRule::computeType(nodeManager, n, check);
801
646
    break;
802
803
  case kind::ARR_TABLE_FUN:
804
    typeNode = ::CVC4::theory::arrays::ArrayTableFunTypeRule::computeType(nodeManager, n, check);
805
    break;
806
807
  case kind::ARRAY_LAMBDA:
808
    typeNode = ::CVC4::theory::arrays::ArrayLambdaTypeRule::computeType(nodeManager, n, check);
809
    break;
810
811
33
  case kind::EQ_RANGE:
812
33
    typeNode = ::CVC4::theory::arrays::ArrayEqRangeTypeRule::computeType(nodeManager, n, check);
813
33
    break;
814
815
  case kind::PARTIAL_SELECT_0:
816
    typeNode = ::CVC4::theory::arrays::ArrayPartialSelectTypeRule::computeType(nodeManager, n, check);
817
    break;
818
819
  case kind::PARTIAL_SELECT_1:
820
    typeNode = ::CVC4::theory::arrays::ArrayPartialSelectTypeRule::computeType(nodeManager, n, check);
821
    break;
822
823
134981
  case kind::APPLY_CONSTRUCTOR:
824
134981
    typeNode = ::CVC4::theory::datatypes::DatatypeConstructorTypeRule::computeType(nodeManager, n, check);
825
134975
    break;
826
827
16631
  case kind::APPLY_SELECTOR:
828
16631
    typeNode = ::CVC4::theory::datatypes::DatatypeSelectorTypeRule::computeType(nodeManager, n, check);
829
16631
    break;
830
831
43533
  case kind::APPLY_SELECTOR_TOTAL:
832
43533
    typeNode = ::CVC4::theory::datatypes::DatatypeSelectorTypeRule::computeType(nodeManager, n, check);
833
43533
    break;
834
835
31192
  case kind::APPLY_TESTER:
836
31192
    typeNode = ::CVC4::theory::datatypes::DatatypeTesterTypeRule::computeType(nodeManager, n, check);
837
31192
    break;
838
839
102
  case kind::APPLY_TYPE_ASCRIPTION:
840
102
    typeNode = ::CVC4::theory::datatypes::DatatypeAscriptionTypeRule::computeType(nodeManager, n, check);
841
102
    break;
842
843
3
  case kind::TUPLE_UPDATE_OP:
844
3
    typeNode = ::CVC4::theory::datatypes::TupleUpdateOpTypeRule::computeType(nodeManager, n, check);
845
3
    break;
846
847
2
  case kind::TUPLE_UPDATE:
848
2
    typeNode = ::CVC4::theory::datatypes::TupleUpdateTypeRule::computeType(nodeManager, n, check);
849
2
    break;
850
851
9
  case kind::RECORD_UPDATE_OP:
852
9
    typeNode = ::CVC4::theory::datatypes::RecordUpdateOpTypeRule::computeType(nodeManager, n, check);
853
9
    break;
854
855
8
  case kind::RECORD_UPDATE:
856
8
    typeNode = ::CVC4::theory::datatypes::RecordUpdateTypeRule::computeType(nodeManager, n, check);
857
8
    break;
858
859
17529
  case kind::DT_SIZE:
860
17529
    typeNode = ::CVC4::theory::datatypes::DtSizeTypeRule::computeType(nodeManager, n, check);
861
17529
    break;
862
863
  case kind::DT_HEIGHT_BOUND:
864
    typeNode = ::CVC4::theory::datatypes::DtBoundTypeRule::computeType(nodeManager, n, check);
865
    break;
866
867
  case kind::DT_SIZE_BOUND:
868
    typeNode = ::CVC4::theory::datatypes::DtBoundTypeRule::computeType(nodeManager, n, check);
869
    break;
870
871
761
  case kind::DT_SYGUS_BOUND:
872
761
    typeNode = ::CVC4::theory::datatypes::DtSygusBoundTypeRule::computeType(nodeManager, n, check);
873
761
    break;
874
875
123248
  case kind::DT_SYGUS_EVAL:
876
123248
    typeNode = ::CVC4::theory::datatypes::DtSyguEvalTypeRule::computeType(nodeManager, n, check);
877
123248
    break;
878
879
20
  case kind::MATCH:
880
20
    typeNode = ::CVC4::theory::datatypes::MatchTypeRule::computeType(nodeManager, n, check);
881
20
    break;
882
883
34
  case kind::MATCH_CASE:
884
34
    typeNode = ::CVC4::theory::datatypes::MatchCaseTypeRule::computeType(nodeManager, n, check);
885
34
    break;
886
887
15
  case kind::MATCH_BIND_CASE:
888
15
    typeNode = ::CVC4::theory::datatypes::MatchBindCaseTypeRule::computeType(nodeManager, n, check);
889
15
    break;
890
891
20
  case kind::TUPLE_PROJECT_OP:
892
20
    typeNode = SimpleTypeRule<RBuiltinOperator>::computeType(nodeManager, n, check);
893
20
    break;
894
895
18
  case kind::TUPLE_PROJECT:
896
18
    typeNode = ::CVC4::theory::datatypes::TupleProjectTypeRule::computeType(nodeManager, n, check);
897
14
    break;
898
899
51
  case kind::SEP_EMP:
900
51
    typeNode = ::CVC4::theory::sep::SepEmpTypeRule::computeType(nodeManager, n, check);
901
51
    break;
902
903
311
  case kind::SEP_PTO:
904
311
    typeNode = ::CVC4::theory::sep::SepPtoTypeRule::computeType(nodeManager, n, check);
905
311
    break;
906
907
211
  case kind::SEP_STAR:
908
211
    typeNode = ::CVC4::theory::sep::SepStarTypeRule::computeType(nodeManager, n, check);
909
211
    break;
910
911
28
  case kind::SEP_WAND:
912
28
    typeNode = ::CVC4::theory::sep::SepWandTypeRule::computeType(nodeManager, n, check);
913
28
    break;
914
915
885
  case kind::SEP_LABEL:
916
885
    typeNode = ::CVC4::theory::sep::SepLabelTypeRule::computeType(nodeManager, n, check);
917
885
    break;
918
919
1390
  case kind::SEP_NIL:
920
1390
    typeNode = ::CVC4::theory::sep::SepNilTypeRule::computeType(nodeManager, n, check);
921
1390
    break;
922
923
4930
  case kind::UNION:
924
4930
    typeNode = ::CVC4::theory::sets::SetsBinaryOperatorTypeRule::computeType(nodeManager, n, check);
925
4928
    break;
926
927
1353
  case kind::INTERSECTION:
928
1353
    typeNode = ::CVC4::theory::sets::SetsBinaryOperatorTypeRule::computeType(nodeManager, n, check);
929
1353
    break;
930
931
853
  case kind::SETMINUS:
932
853
    typeNode = ::CVC4::theory::sets::SetsBinaryOperatorTypeRule::computeType(nodeManager, n, check);
933
853
    break;
934
935
370
  case kind::SUBSET:
936
370
    typeNode = ::CVC4::theory::sets::SubsetTypeRule::computeType(nodeManager, n, check);
937
370
    break;
938
939
23843
  case kind::MEMBER:
940
23843
    typeNode = ::CVC4::theory::sets::MemberTypeRule::computeType(nodeManager, n, check);
941
23843
    break;
942
943
  case kind::SINGLETON_OP:
944
    typeNode = SimpleTypeRule<RBuiltinOperator>::computeType(nodeManager, n, check);
945
    break;
946
947
3784
  case kind::SINGLETON:
948
3784
    typeNode = ::CVC4::theory::sets::SingletonTypeRule::computeType(nodeManager, n, check);
949
3784
    break;
950
951
1695
  case kind::EMPTYSET:
952
1695
    typeNode = ::CVC4::theory::sets::EmptySetTypeRule::computeType(nodeManager, n, check);
953
1695
    break;
954
955
31
  case kind::INSERT:
956
31
    typeNode = ::CVC4::theory::sets::InsertTypeRule::computeType(nodeManager, n, check);
957
31
    break;
958
959
2791
  case kind::CARD:
960
2791
    typeNode = ::CVC4::theory::sets::CardTypeRule::computeType(nodeManager, n, check);
961
2791
    break;
962
963
23
  case kind::COMPLEMENT:
964
23
    typeNode = ::CVC4::theory::sets::ComplementTypeRule::computeType(nodeManager, n, check);
965
23
    break;
966
967
134
  case kind::UNIVERSE_SET:
968
134
    typeNode = ::CVC4::theory::sets::UniverseSetTypeRule::computeType(nodeManager, n, check);
969
134
    break;
970
971
52
  case kind::COMPREHENSION:
972
52
    typeNode = ::CVC4::theory::sets::ComprehensionTypeRule::computeType(nodeManager, n, check);
973
52
    break;
974
975
16
  case kind::CHOOSE:
976
16
    typeNode = ::CVC4::theory::sets::ChooseTypeRule::computeType(nodeManager, n, check);
977
16
    break;
978
979
18
  case kind::IS_SINGLETON:
980
18
    typeNode = ::CVC4::theory::sets::IsSingletonTypeRule::computeType(nodeManager, n, check);
981
18
    break;
982
983
326
  case kind::JOIN:
984
326
    typeNode = ::CVC4::theory::sets::RelBinaryOperatorTypeRule::computeType(nodeManager, n, check);
985
326
    break;
986
987
47
  case kind::PRODUCT:
988
47
    typeNode = ::CVC4::theory::sets::RelBinaryOperatorTypeRule::computeType(nodeManager, n, check);
989
47
    break;
990
991
119
  case kind::TRANSPOSE:
992
119
    typeNode = ::CVC4::theory::sets::RelTransposeTypeRule::computeType(nodeManager, n, check);
993
119
    break;
994
995
45
  case kind::TCLOSURE:
996
45
    typeNode = ::CVC4::theory::sets::RelTransClosureTypeRule::computeType(nodeManager, n, check);
997
45
    break;
998
999
38
  case kind::JOIN_IMAGE:
1000
38
    typeNode = ::CVC4::theory::sets::JoinImageTypeRule::computeType(nodeManager, n, check);
1001
38
    break;
1002
1003
9
  case kind::IDEN:
1004
9
    typeNode = ::CVC4::theory::sets::RelIdenTypeRule::computeType(nodeManager, n, check);
1005
9
    break;
1006
1007
70
  case kind::UNION_MAX:
1008
70
    typeNode = ::CVC4::theory::bags::BinaryOperatorTypeRule::computeType(nodeManager, n, check);
1009
70
    break;
1010
1011
149
  case kind::UNION_DISJOINT:
1012
149
    typeNode = ::CVC4::theory::bags::BinaryOperatorTypeRule::computeType(nodeManager, n, check);
1013
149
    break;
1014
1015
42
  case kind::INTERSECTION_MIN:
1016
42
    typeNode = ::CVC4::theory::bags::BinaryOperatorTypeRule::computeType(nodeManager, n, check);
1017
42
    break;
1018
1019
35
  case kind::DIFFERENCE_SUBTRACT:
1020
35
    typeNode = ::CVC4::theory::bags::BinaryOperatorTypeRule::computeType(nodeManager, n, check);
1021
35
    break;
1022
1023
20
  case kind::DIFFERENCE_REMOVE:
1024
20
    typeNode = ::CVC4::theory::bags::BinaryOperatorTypeRule::computeType(nodeManager, n, check);
1025
20
    break;
1026
1027
10
  case kind::SUBBAG:
1028
10
    typeNode = ::CVC4::theory::bags::SubBagTypeRule::computeType(nodeManager, n, check);
1029
10
    break;
1030
1031
496
  case kind::BAG_COUNT:
1032
496
    typeNode = ::CVC4::theory::bags::CountTypeRule::computeType(nodeManager, n, check);
1033
494
    break;
1034
1035
16
  case kind::DUPLICATE_REMOVAL:
1036
16
    typeNode = ::CVC4::theory::bags::DuplicateRemovalTypeRule::computeType(nodeManager, n, check);
1037
16
    break;
1038
1039
  case kind::MK_BAG_OP:
1040
    typeNode = SimpleTypeRule<RBuiltinOperator>::computeType(nodeManager, n, check);
1041
    break;
1042
1043
257
  case kind::MK_BAG:
1044
257
    typeNode = ::CVC4::theory::bags::MkBagTypeRule::computeType(nodeManager, n, check);
1045
257
    break;
1046
1047
1344
  case kind::EMPTYBAG:
1048
1344
    typeNode = ::CVC4::theory::bags::EmptyBagTypeRule::computeType(nodeManager, n, check);
1049
1344
    break;
1050
1051
14
  case kind::BAG_CARD:
1052
14
    typeNode = ::CVC4::theory::bags::CardTypeRule::computeType(nodeManager, n, check);
1053
14
    break;
1054
1055
8
  case kind::BAG_CHOOSE:
1056
8
    typeNode = ::CVC4::theory::bags::ChooseTypeRule::computeType(nodeManager, n, check);
1057
8
    break;
1058
1059
10
  case kind::BAG_IS_SINGLETON:
1060
10
    typeNode = ::CVC4::theory::bags::IsSingletonTypeRule::computeType(nodeManager, n, check);
1061
10
    break;
1062
1063
10
  case kind::BAG_FROM_SET:
1064
10
    typeNode = ::CVC4::theory::bags::FromSetTypeRule::computeType(nodeManager, n, check);
1065
10
    break;
1066
1067
10
  case kind::BAG_TO_SET:
1068
10
    typeNode = ::CVC4::theory::bags::ToSetTypeRule::computeType(nodeManager, n, check);
1069
10
    break;
1070
1071
78
  case kind::STRING_REPLACE_RE:
1072
78
    typeNode = SimpleTypeRule<RString, AString, ARegExp, AString>::computeType(nodeManager, n, check);
1073
78
    break;
1074
1075
72
  case kind::STRING_REPLACE_RE_ALL:
1076
72
    typeNode = SimpleTypeRule<RString, AString, ARegExp, AString>::computeType(nodeManager, n, check);
1077
72
    break;
1078
1079
126
  case kind::REGEXP_RV:
1080
126
    typeNode = SimpleTypeRule<RRegExp, AInteger>::computeType(nodeManager, n, check);
1081
126
    break;
1082
1083
1618
  case kind::REGEXP_CONCAT:
1084
1618
    typeNode = SimpleTypeRuleVar<RRegExp, ARegExp>::computeType(nodeManager, n, check);
1085
1618
    break;
1086
1087
368
  case kind::REGEXP_UNION:
1088
368
    typeNode = SimpleTypeRuleVar<RRegExp, ARegExp>::computeType(nodeManager, n, check);
1089
368
    break;
1090
1091
80
  case kind::REGEXP_INTER:
1092
80
    typeNode = SimpleTypeRuleVar<RRegExp, ARegExp>::computeType(nodeManager, n, check);
1093
80
    break;
1094
1095
29
  case kind::REGEXP_DIFF:
1096
29
    typeNode = SimpleTypeRuleVar<RRegExp, ARegExp>::computeType(nodeManager, n, check);
1097
29
    break;
1098
1099
7058
  case kind::REGEXP_STAR:
1100
7058
    typeNode = SimpleTypeRule<RRegExp, ARegExp>::computeType(nodeManager, n, check);
1101
7058
    break;
1102
1103
37
  case kind::REGEXP_PLUS:
1104
37
    typeNode = SimpleTypeRule<RRegExp, ARegExp>::computeType(nodeManager, n, check);
1105
37
    break;
1106
1107
28
  case kind::REGEXP_OPT:
1108
28
    typeNode = SimpleTypeRule<RRegExp, ARegExp>::computeType(nodeManager, n, check);
1109
28
    break;
1110
1111
158
  case kind::REGEXP_RANGE:
1112
158
    typeNode = ::CVC4::theory::strings::RegExpRangeTypeRule::computeType(nodeManager, n, check);
1113
158
    break;
1114
1115
4
  case kind::REGEXP_REPEAT_OP:
1116
4
    typeNode = SimpleTypeRule<RBuiltinOperator>::computeType(nodeManager, n, check);
1117
4
    break;
1118
1119
6
  case kind::REGEXP_REPEAT:
1120
6
    typeNode = SimpleTypeRule<RRegExp, ARegExp>::computeType(nodeManager, n, check);
1121
6
    break;
1122
1123
19
  case kind::REGEXP_LOOP_OP:
1124
19
    typeNode = SimpleTypeRule<RBuiltinOperator>::computeType(nodeManager, n, check);
1125
19
    break;
1126
1127
27
  case kind::REGEXP_LOOP:
1128
27
    typeNode = SimpleTypeRule<RRegExp, ARegExp>::computeType(nodeManager, n, check);
1129
27
    break;
1130
1131
58
  case kind::REGEXP_COMPLEMENT:
1132
58
    typeNode = SimpleTypeRule<RRegExp, ARegExp>::computeType(nodeManager, n, check);
1133
58
    break;
1134
1135
7653
  case kind::STRING_TO_REGEXP:
1136
7653
    typeNode = SimpleTypeRule<RRegExp, AString>::computeType(nodeManager, n, check);
1137
7653
    break;
1138
1139
6495
  case kind::STRING_IN_REGEXP:
1140
6495
    typeNode = SimpleTypeRule<RBool, AString, ARegExp>::computeType(nodeManager, n, check);
1141
6495
    break;
1142
1143
6417
  case kind::REGEXP_EMPTY:
1144
6417
    typeNode = SimpleTypeRule<RRegExp>::computeType(nodeManager, n, check);
1145
6417
    break;
1146
1147
6417
  case kind::REGEXP_SIGMA:
1148
6417
    typeNode = SimpleTypeRule<RRegExp>::computeType(nodeManager, n, check);
1149
6417
    break;
1150
1151
36439
  case kind::STRING_CONCAT:
1152
36439
    typeNode = ::CVC4::theory::strings::StringConcatTypeRule::computeType(nodeManager, n, check);
1153
36439
    break;
1154
1155
91238
  case kind::STRING_LENGTH:
1156
91238
    typeNode = ::CVC4::theory::strings::StringStrToIntTypeRule::computeType(nodeManager, n, check);
1157
91238
    break;
1158
1159
33343
  case kind::STRING_SUBSTR:
1160
33343
    typeNode = ::CVC4::theory::strings::StringSubstrTypeRule::computeType(nodeManager, n, check);
1161
33343
    break;
1162
1163
137
  case kind::STRING_UPDATE:
1164
137
    typeNode = ::CVC4::theory::strings::StringUpdateTypeRule::computeType(nodeManager, n, check);
1165
137
    break;
1166
1167
134
  case kind::STRING_CHARAT:
1168
134
    typeNode = ::CVC4::theory::strings::StringAtTypeRule::computeType(nodeManager, n, check);
1169
134
    break;
1170
1171
90178
  case kind::STRING_STRCTN:
1172
90178
    typeNode = ::CVC4::theory::strings::StringRelationTypeRule::computeType(nodeManager, n, check);
1173
90178
    break;
1174
1175
2708
  case kind::STRING_STRIDOF:
1176
2708
    typeNode = ::CVC4::theory::strings::StringIndexOfTypeRule::computeType(nodeManager, n, check);
1177
2708
    break;
1178
1179
2139
  case kind::STRING_STRREPL:
1180
2139
    typeNode = ::CVC4::theory::strings::StringReplaceTypeRule::computeType(nodeManager, n, check);
1181
2139
    break;
1182
1183
84
  case kind::STRING_STRREPLALL:
1184
84
    typeNode = ::CVC4::theory::strings::StringReplaceTypeRule::computeType(nodeManager, n, check);
1185
84
    break;
1186
1187
115
  case kind::STRING_PREFIX:
1188
115
    typeNode = ::CVC4::theory::strings::StringStrToBoolTypeRule::computeType(nodeManager, n, check);
1189
115
    break;
1190
1191
46
  case kind::STRING_SUFFIX:
1192
46
    typeNode = ::CVC4::theory::strings::StringStrToBoolTypeRule::computeType(nodeManager, n, check);
1193
46
    break;
1194
1195
158
  case kind::STRING_REV:
1196
158
    typeNode = ::CVC4::theory::strings::StringStrToStrTypeRule::computeType(nodeManager, n, check);
1197
158
    break;
1198
1199
30234
  case kind::CONST_STRING:
1200
30234
    typeNode = SimpleTypeRule<RString>::computeType(nodeManager, n, check);
1201
30234
    break;
1202
1203
17
  case kind::STRING_LT:
1204
17
    typeNode = SimpleTypeRule<RBool, AString, AString>::computeType(nodeManager, n, check);
1205
17
    break;
1206
1207
239
  case kind::STRING_LEQ:
1208
239
    typeNode = SimpleTypeRule<RBool, AString, AString>::computeType(nodeManager, n, check);
1209
239
    break;
1210
1211
8
  case kind::STRING_IS_DIGIT:
1212
8
    typeNode = SimpleTypeRule<RBool, AString>::computeType(nodeManager, n, check);
1213
8
    break;
1214
1215
479
  case kind::STRING_ITOS:
1216
479
    typeNode = SimpleTypeRule<RString, AInteger>::computeType(nodeManager, n, check);
1217
479
    break;
1218
1219
336
  case kind::STRING_STOI:
1220
336
    typeNode = SimpleTypeRule<RInteger, AString>::computeType(nodeManager, n, check);
1221
336
    break;
1222
1223
2227
  case kind::STRING_TO_CODE:
1224
2227
    typeNode = SimpleTypeRule<RInteger, AString>::computeType(nodeManager, n, check);
1225
2227
    break;
1226
1227
52
  case kind::STRING_FROM_CODE:
1228
52
    typeNode = SimpleTypeRule<RString, AInteger>::computeType(nodeManager, n, check);
1229
52
    break;
1230
1231
40
  case kind::STRING_TOUPPER:
1232
40
    typeNode = SimpleTypeRule<RString, AString>::computeType(nodeManager, n, check);
1233
40
    break;
1234
1235
108
  case kind::STRING_TOLOWER:
1236
108
    typeNode = SimpleTypeRule<RString, AString>::computeType(nodeManager, n, check);
1237
108
    break;
1238
1239
335
  case kind::CONST_SEQUENCE:
1240
335
    typeNode = ::CVC4::theory::strings::ConstSequenceTypeRule::computeType(nodeManager, n, check);
1241
335
    break;
1242
1243
190
  case kind::SEQ_UNIT:
1244
190
    typeNode = ::CVC4::theory::strings::SeqUnitTypeRule::computeType(nodeManager, n, check);
1245
190
    break;
1246
1247
182
  case kind::SEQ_NTH:
1248
182
    typeNode = ::CVC4::theory::strings::SeqNthTypeRule::computeType(nodeManager, n, check);
1249
182
    break;
1250
1251
4
  case kind::SEQ_NTH_TOTAL:
1252
4
    typeNode = ::CVC4::theory::strings::SeqNthTypeRule::computeType(nodeManager, n, check);
1253
4
    break;
1254
1255
98852
  case kind::FORALL:
1256
98852
    typeNode = ::CVC4::theory::quantifiers::QuantifierForallTypeRule::computeType(nodeManager, n, check);
1257
98852
    break;
1258
1259
9170
  case kind::EXISTS:
1260
9170
    typeNode = ::CVC4::theory::quantifiers::QuantifierExistsTypeRule::computeType(nodeManager, n, check);
1261
9170
    break;
1262
1263
66871
  case kind::BOUND_VAR_LIST:
1264
66871
    typeNode = ::CVC4::theory::quantifiers::QuantifierBoundVarListTypeRule::computeType(nodeManager, n, check);
1265
66871
    break;
1266
1267
7669
  case kind::INST_PATTERN:
1268
7669
    typeNode = ::CVC4::theory::quantifiers::QuantifierInstPatternTypeRule::computeType(nodeManager, n, check);
1269
7669
    break;
1270
1271
16
  case kind::INST_NO_PATTERN:
1272
16
    typeNode = ::CVC4::theory::quantifiers::QuantifierInstNoPatternTypeRule::computeType(nodeManager, n, check);
1273
16
    break;
1274
1275
953
  case kind::INST_ATTRIBUTE:
1276
953
    typeNode = ::CVC4::theory::quantifiers::QuantifierInstAttributeTypeRule::computeType(nodeManager, n, check);
1277
953
    break;
1278
1279
8319
  case kind::INST_PATTERN_LIST:
1280
8319
    typeNode = ::CVC4::theory::quantifiers::QuantifierInstPatternListTypeRule::computeType(nodeManager, n, check);
1281
8319
    break;
1282
1283
1284
  default:
1285
    Debug("getType") << "FAILURE" << std::endl;
1286
    Unhandled() << " " << n.getKind();
1287
  }
1288
1289
26402239
  nodeManager->setAttribute(n, TypeAttr(), typeNode);
1290
26402239
  nodeManager->setAttribute(n, TypeCheckedAttr(),
1291
52804478
                            check || nodeManager->getAttribute(n, TypeCheckedAttr()));
1292
1293
26402239
  return typeNode;
1294
1295
}/* TypeChecker::computeType */
1296
1297
4869650
bool TypeChecker::computeIsConst(NodeManager* nodeManager, TNode n)
1298
{
1299
4869650
  Assert(n.getMetaKind() == kind::metakind::OPERATOR
1300
         || n.getMetaKind() == kind::metakind::PARAMETERIZED
1301
         || n.getMetaKind() == kind::metakind::NULLARY_OPERATOR);
1302
1303
4869650
  switch(n.getKind()) {
1304
1305
2417
  case kind::LAMBDA:
1306
2417
    return ::CVC4::theory::builtin::LambdaTypeRule::computeIsConst(nodeManager, n);
1307
1308
8873
  case kind::STORE:
1309
8873
    return ::CVC4::theory::arrays::ArrayStoreTypeRule::computeIsConst(nodeManager, n);
1310
1311
118069
  case kind::APPLY_CONSTRUCTOR:
1312
118069
    return ::CVC4::theory::datatypes::DatatypeConstructorTypeRule::computeIsConst(nodeManager, n);
1313
1314
4287
  case kind::UNION:
1315
4287
    return ::CVC4::theory::sets::SetsBinaryOperatorTypeRule::computeIsConst(nodeManager, n);
1316
1317
3177
  case kind::SINGLETON:
1318
3177
    return ::CVC4::theory::sets::SingletonTypeRule::computeIsConst(nodeManager, n);
1319
1320
121
  case kind::UNION_DISJOINT:
1321
121
    return ::CVC4::theory::bags::BinaryOperatorTypeRule::computeIsConst(nodeManager, n);
1322
1323
204
  case kind::MK_BAG:
1324
204
    return ::CVC4::theory::bags::MkBagTypeRule::computeIsConst(nodeManager, n);
1325
1326
1327
4732502
    default:;
1328
  }
1329
1330
4732502
  return false;
1331
1332
}/* TypeChecker::computeIsConst */
1333
1334
}/* CVC4::expr namespace */
1335
26685
}/* CVC4 namespace */