GCC Code Coverage Report
Directory: . Exec Total Coverage
File: build-coverage/src/expr/metakind.cpp Lines: 575 775 74.2 %
Date: 2021-03-22 Branches: 357 805 44.3 %

Line Exec Source
1
/*********************                                                        */
2
/** metakind.h
3
 **
4
 ** Copyright 2010-2014  New York University and The University of Iowa,
5
 ** and as below.
6
 **
7
 ** This header file automatically generated by:
8
 **
9
 **     ../../../src/expr/mkmetakind /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-22/src/expr/metakind_template.cpp /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-22/src/theory/builtin/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-22/src/theory/booleans/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-22/src/theory/uf/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-22/src/theory/arith/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-22/src/theory/bv/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-22/src/theory/fp/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-22/src/theory/arrays/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-22/src/theory/datatypes/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-22/src/theory/sep/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-22/src/theory/sets/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-22/src/theory/bags/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-22/src/theory/strings/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-22/src/theory/quantifiers/kinds
10
 **
11
 ** for the CVC4 project.
12
 **/
13
14
/*********************                                                        */
15
/*! \file metakind_template.cpp
16
 ** \verbatim
17
 ** Top contributors (to current version):
18
 **   Morgan Deters, Andres Noetzli, Mathias Preiner
19
 ** This file is part of the CVC4 project.
20
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
21
 ** in the top-level source directory and their institutional affiliations.
22
 ** All rights reserved.  See the file COPYING in the top-level source
23
 ** directory for licensing information.\endverbatim
24
 **
25
 ** \brief [[ Add one-line brief description here ]]
26
 **
27
 ** [[ Add lengthier description here ]]
28
 ** \todo document this file
29
 **/
30
31
#include "expr/metakind.h"
32
33
#include <iostream>
34
35
namespace CVC4 {
36
namespace kind {
37
38
/**
39
 * Get the metakind for a particular kind.
40
 */
41
5561210349
MetaKind metaKindOf(Kind k) {
42
  static const MetaKind metaKinds[] = {
43
    metakind::INVALID, /* UNDEFINED_KIND */
44
    metakind::INVALID, /* NULL_EXPR */
45
46
    /* from builtin */
47
    metakind::VARIABLE, /* SORT_TAG */
48
    metakind::PARAMETERIZED, /* SORT_TYPE */
49
    metakind::CONSTANT, /* UNINTERPRETED_CONSTANT */
50
    metakind::CONSTANT, /* ABSTRACT_VALUE */
51
    metakind::CONSTANT, /* BUILTIN */
52
    metakind::OPERATOR, /* EQUAL */
53
    metakind::OPERATOR, /* DISTINCT */
54
    metakind::VARIABLE, /* VARIABLE */
55
    metakind::VARIABLE, /* BOUND_VARIABLE */
56
    metakind::VARIABLE, /* SKOLEM */
57
    metakind::OPERATOR, /* SEXPR */
58
    metakind::OPERATOR, /* LAMBDA */
59
    metakind::OPERATOR, /* WITNESS */
60
    metakind::CONSTANT, /* TYPE_CONSTANT */
61
    metakind::OPERATOR, /* FUNCTION_TYPE */
62
    metakind::OPERATOR, /* SEXPR_TYPE */
63
64
    /* from booleans */
65
    metakind::CONSTANT, /* CONST_BOOLEAN */
66
    metakind::OPERATOR, /* NOT */
67
    metakind::OPERATOR, /* AND */
68
    metakind::OPERATOR, /* IMPLIES */
69
    metakind::OPERATOR, /* OR */
70
    metakind::OPERATOR, /* XOR */
71
    metakind::OPERATOR, /* ITE */
72
73
    /* from uf */
74
    metakind::PARAMETERIZED, /* APPLY_UF */
75
    metakind::VARIABLE, /* BOOLEAN_TERM_VARIABLE */
76
    metakind::OPERATOR, /* CARDINALITY_CONSTRAINT */
77
    metakind::OPERATOR, /* COMBINED_CARDINALITY_CONSTRAINT */
78
    metakind::PARAMETERIZED, /* PARTIAL_APPLY_UF */
79
    metakind::OPERATOR, /* CARDINALITY_VALUE */
80
    metakind::OPERATOR, /* HO_APPLY */
81
82
    /* from arith */
83
    metakind::OPERATOR, /* PLUS */
84
    metakind::OPERATOR, /* MULT */
85
    metakind::OPERATOR, /* NONLINEAR_MULT */
86
    metakind::OPERATOR, /* MINUS */
87
    metakind::OPERATOR, /* UMINUS */
88
    metakind::OPERATOR, /* DIVISION */
89
    metakind::OPERATOR, /* DIVISION_TOTAL */
90
    metakind::OPERATOR, /* INTS_DIVISION */
91
    metakind::OPERATOR, /* INTS_DIVISION_TOTAL */
92
    metakind::OPERATOR, /* INTS_MODULUS */
93
    metakind::OPERATOR, /* INTS_MODULUS_TOTAL */
94
    metakind::OPERATOR, /* ABS */
95
    metakind::PARAMETERIZED, /* DIVISIBLE */
96
    metakind::OPERATOR, /* POW */
97
    metakind::OPERATOR, /* EXPONENTIAL */
98
    metakind::OPERATOR, /* SINE */
99
    metakind::OPERATOR, /* COSINE */
100
    metakind::OPERATOR, /* TANGENT */
101
    metakind::OPERATOR, /* COSECANT */
102
    metakind::OPERATOR, /* SECANT */
103
    metakind::OPERATOR, /* COTANGENT */
104
    metakind::OPERATOR, /* ARCSINE */
105
    metakind::OPERATOR, /* ARCCOSINE */
106
    metakind::OPERATOR, /* ARCTANGENT */
107
    metakind::OPERATOR, /* ARCCOSECANT */
108
    metakind::OPERATOR, /* ARCSECANT */
109
    metakind::OPERATOR, /* ARCCOTANGENT */
110
    metakind::OPERATOR, /* SQRT */
111
    metakind::CONSTANT, /* DIVISIBLE_OP */
112
    metakind::CONSTANT, /* CONST_RATIONAL */
113
    metakind::OPERATOR, /* LT */
114
    metakind::OPERATOR, /* LEQ */
115
    metakind::OPERATOR, /* GT */
116
    metakind::OPERATOR, /* GEQ */
117
    metakind::CONSTANT, /* INDEXED_ROOT_PREDICATE_OP */
118
    metakind::PARAMETERIZED, /* INDEXED_ROOT_PREDICATE */
119
    metakind::OPERATOR, /* IS_INTEGER */
120
    metakind::OPERATOR, /* TO_INTEGER */
121
    metakind::OPERATOR, /* TO_REAL */
122
    metakind::OPERATOR, /* CAST_TO_REAL */
123
    metakind::NULLARY_OPERATOR, /* PI */
124
    metakind::CONSTANT, /* IAND_OP */
125
    metakind::PARAMETERIZED, /* IAND */
126
127
    /* from bv */
128
    metakind::CONSTANT, /* BITVECTOR_TYPE */
129
    metakind::CONSTANT, /* CONST_BITVECTOR */
130
    metakind::OPERATOR, /* BITVECTOR_CONCAT */
131
    metakind::OPERATOR, /* BITVECTOR_AND */
132
    metakind::OPERATOR, /* BITVECTOR_COMP */
133
    metakind::OPERATOR, /* BITVECTOR_OR */
134
    metakind::OPERATOR, /* BITVECTOR_XOR */
135
    metakind::OPERATOR, /* BITVECTOR_NOT */
136
    metakind::OPERATOR, /* BITVECTOR_NAND */
137
    metakind::OPERATOR, /* BITVECTOR_NOR */
138
    metakind::OPERATOR, /* BITVECTOR_XNOR */
139
    metakind::OPERATOR, /* BITVECTOR_MULT */
140
    metakind::OPERATOR, /* BITVECTOR_NEG */
141
    metakind::OPERATOR, /* BITVECTOR_PLUS */
142
    metakind::OPERATOR, /* BITVECTOR_SUB */
143
    metakind::OPERATOR, /* BITVECTOR_UDIV */
144
    metakind::OPERATOR, /* BITVECTOR_UREM */
145
    metakind::OPERATOR, /* BITVECTOR_SDIV */
146
    metakind::OPERATOR, /* BITVECTOR_SMOD */
147
    metakind::OPERATOR, /* BITVECTOR_SREM */
148
    metakind::OPERATOR, /* BITVECTOR_ASHR */
149
    metakind::OPERATOR, /* BITVECTOR_LSHR */
150
    metakind::OPERATOR, /* BITVECTOR_SHL */
151
    metakind::OPERATOR, /* BITVECTOR_ULE */
152
    metakind::OPERATOR, /* BITVECTOR_ULT */
153
    metakind::OPERATOR, /* BITVECTOR_UGE */
154
    metakind::OPERATOR, /* BITVECTOR_UGT */
155
    metakind::OPERATOR, /* BITVECTOR_SLE */
156
    metakind::OPERATOR, /* BITVECTOR_SLT */
157
    metakind::OPERATOR, /* BITVECTOR_SGE */
158
    metakind::OPERATOR, /* BITVECTOR_SGT */
159
    metakind::OPERATOR, /* BITVECTOR_ULTBV */
160
    metakind::OPERATOR, /* BITVECTOR_SLTBV */
161
    metakind::OPERATOR, /* BITVECTOR_REDAND */
162
    metakind::OPERATOR, /* BITVECTOR_REDOR */
163
    metakind::OPERATOR, /* BITVECTOR_ITE */
164
    metakind::OPERATOR, /* BITVECTOR_TO_NAT */
165
    metakind::OPERATOR, /* BITVECTOR_ACKERMANNIZE_UDIV */
166
    metakind::OPERATOR, /* BITVECTOR_ACKERMANNIZE_UREM */
167
    metakind::OPERATOR, /* BITVECTOR_EAGER_ATOM */
168
    metakind::CONSTANT, /* BITVECTOR_BITOF_OP */
169
    metakind::PARAMETERIZED, /* BITVECTOR_BITOF */
170
    metakind::CONSTANT, /* BITVECTOR_EXTRACT_OP */
171
    metakind::PARAMETERIZED, /* BITVECTOR_EXTRACT */
172
    metakind::CONSTANT, /* BITVECTOR_REPEAT_OP */
173
    metakind::PARAMETERIZED, /* BITVECTOR_REPEAT */
174
    metakind::CONSTANT, /* BITVECTOR_ROTATE_LEFT_OP */
175
    metakind::PARAMETERIZED, /* BITVECTOR_ROTATE_LEFT */
176
    metakind::CONSTANT, /* BITVECTOR_ROTATE_RIGHT_OP */
177
    metakind::PARAMETERIZED, /* BITVECTOR_ROTATE_RIGHT */
178
    metakind::CONSTANT, /* BITVECTOR_SIGN_EXTEND_OP */
179
    metakind::PARAMETERIZED, /* BITVECTOR_SIGN_EXTEND */
180
    metakind::CONSTANT, /* BITVECTOR_ZERO_EXTEND_OP */
181
    metakind::PARAMETERIZED, /* BITVECTOR_ZERO_EXTEND */
182
    metakind::CONSTANT, /* INT_TO_BITVECTOR_OP */
183
    metakind::PARAMETERIZED, /* INT_TO_BITVECTOR */
184
185
    /* from fp */
186
    metakind::CONSTANT, /* CONST_FLOATINGPOINT */
187
    metakind::CONSTANT, /* CONST_ROUNDINGMODE */
188
    metakind::CONSTANT, /* FLOATINGPOINT_TYPE */
189
    metakind::OPERATOR, /* FLOATINGPOINT_FP */
190
    metakind::OPERATOR, /* FLOATINGPOINT_EQ */
191
    metakind::OPERATOR, /* FLOATINGPOINT_ABS */
192
    metakind::OPERATOR, /* FLOATINGPOINT_NEG */
193
    metakind::OPERATOR, /* FLOATINGPOINT_PLUS */
194
    metakind::OPERATOR, /* FLOATINGPOINT_SUB */
195
    metakind::OPERATOR, /* FLOATINGPOINT_MULT */
196
    metakind::OPERATOR, /* FLOATINGPOINT_DIV */
197
    metakind::OPERATOR, /* FLOATINGPOINT_FMA */
198
    metakind::OPERATOR, /* FLOATINGPOINT_SQRT */
199
    metakind::OPERATOR, /* FLOATINGPOINT_REM */
200
    metakind::OPERATOR, /* FLOATINGPOINT_RTI */
201
    metakind::OPERATOR, /* FLOATINGPOINT_MIN */
202
    metakind::OPERATOR, /* FLOATINGPOINT_MAX */
203
    metakind::OPERATOR, /* FLOATINGPOINT_MIN_TOTAL */
204
    metakind::OPERATOR, /* FLOATINGPOINT_MAX_TOTAL */
205
    metakind::OPERATOR, /* FLOATINGPOINT_LEQ */
206
    metakind::OPERATOR, /* FLOATINGPOINT_LT */
207
    metakind::OPERATOR, /* FLOATINGPOINT_GEQ */
208
    metakind::OPERATOR, /* FLOATINGPOINT_GT */
209
    metakind::OPERATOR, /* FLOATINGPOINT_ISN */
210
    metakind::OPERATOR, /* FLOATINGPOINT_ISSN */
211
    metakind::OPERATOR, /* FLOATINGPOINT_ISZ */
212
    metakind::OPERATOR, /* FLOATINGPOINT_ISINF */
213
    metakind::OPERATOR, /* FLOATINGPOINT_ISNAN */
214
    metakind::OPERATOR, /* FLOATINGPOINT_ISNEG */
215
    metakind::OPERATOR, /* FLOATINGPOINT_ISPOS */
216
    metakind::CONSTANT, /* FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP */
217
    metakind::PARAMETERIZED, /* FLOATINGPOINT_TO_FP_IEEE_BITVECTOR */
218
    metakind::CONSTANT, /* FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP */
219
    metakind::PARAMETERIZED, /* FLOATINGPOINT_TO_FP_FLOATINGPOINT */
220
    metakind::CONSTANT, /* FLOATINGPOINT_TO_FP_REAL_OP */
221
    metakind::PARAMETERIZED, /* FLOATINGPOINT_TO_FP_REAL */
222
    metakind::CONSTANT, /* FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP */
223
    metakind::PARAMETERIZED, /* FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR */
224
    metakind::CONSTANT, /* FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP */
225
    metakind::PARAMETERIZED, /* FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR */
226
    metakind::CONSTANT, /* FLOATINGPOINT_TO_FP_GENERIC_OP */
227
    metakind::PARAMETERIZED, /* FLOATINGPOINT_TO_FP_GENERIC */
228
    metakind::CONSTANT, /* FLOATINGPOINT_TO_UBV_OP */
229
    metakind::PARAMETERIZED, /* FLOATINGPOINT_TO_UBV */
230
    metakind::CONSTANT, /* FLOATINGPOINT_TO_UBV_TOTAL_OP */
231
    metakind::PARAMETERIZED, /* FLOATINGPOINT_TO_UBV_TOTAL */
232
    metakind::CONSTANT, /* FLOATINGPOINT_TO_SBV_OP */
233
    metakind::PARAMETERIZED, /* FLOATINGPOINT_TO_SBV */
234
    metakind::CONSTANT, /* FLOATINGPOINT_TO_SBV_TOTAL_OP */
235
    metakind::PARAMETERIZED, /* FLOATINGPOINT_TO_SBV_TOTAL */
236
    metakind::OPERATOR, /* FLOATINGPOINT_TO_REAL */
237
    metakind::OPERATOR, /* FLOATINGPOINT_TO_REAL_TOTAL */
238
    metakind::OPERATOR, /* FLOATINGPOINT_COMPONENT_NAN */
239
    metakind::OPERATOR, /* FLOATINGPOINT_COMPONENT_INF */
240
    metakind::OPERATOR, /* FLOATINGPOINT_COMPONENT_ZERO */
241
    metakind::OPERATOR, /* FLOATINGPOINT_COMPONENT_SIGN */
242
    metakind::OPERATOR, /* FLOATINGPOINT_COMPONENT_EXPONENT */
243
    metakind::OPERATOR, /* FLOATINGPOINT_COMPONENT_SIGNIFICAND */
244
    metakind::OPERATOR, /* ROUNDINGMODE_BITBLAST */
245
246
    /* from arrays */
247
    metakind::OPERATOR, /* ARRAY_TYPE */
248
    metakind::OPERATOR, /* SELECT */
249
    metakind::OPERATOR, /* STORE */
250
    metakind::OPERATOR, /* EQ_RANGE */
251
    metakind::CONSTANT, /* STORE_ALL */
252
    metakind::OPERATOR, /* ARR_TABLE_FUN */
253
    metakind::OPERATOR, /* ARRAY_LAMBDA */
254
    metakind::OPERATOR, /* PARTIAL_SELECT_0 */
255
    metakind::OPERATOR, /* PARTIAL_SELECT_1 */
256
257
    /* from datatypes */
258
    metakind::OPERATOR, /* CONSTRUCTOR_TYPE */
259
    metakind::OPERATOR, /* SELECTOR_TYPE */
260
    metakind::OPERATOR, /* TESTER_TYPE */
261
    metakind::PARAMETERIZED, /* APPLY_CONSTRUCTOR */
262
    metakind::PARAMETERIZED, /* APPLY_SELECTOR */
263
    metakind::PARAMETERIZED, /* APPLY_SELECTOR_TOTAL */
264
    metakind::PARAMETERIZED, /* APPLY_TESTER */
265
    metakind::CONSTANT, /* DATATYPE_TYPE */
266
    metakind::OPERATOR, /* PARAMETRIC_DATATYPE */
267
    metakind::PARAMETERIZED, /* APPLY_TYPE_ASCRIPTION */
268
    metakind::CONSTANT, /* ASCRIPTION_TYPE */
269
    metakind::CONSTANT, /* TUPLE_UPDATE_OP */
270
    metakind::PARAMETERIZED, /* TUPLE_UPDATE */
271
    metakind::CONSTANT, /* RECORD_UPDATE_OP */
272
    metakind::PARAMETERIZED, /* RECORD_UPDATE */
273
    metakind::OPERATOR, /* DT_SIZE */
274
    metakind::OPERATOR, /* DT_HEIGHT_BOUND */
275
    metakind::OPERATOR, /* DT_SIZE_BOUND */
276
    metakind::OPERATOR, /* DT_SYGUS_BOUND */
277
    metakind::OPERATOR, /* DT_SYGUS_EVAL */
278
    metakind::OPERATOR, /* MATCH */
279
    metakind::OPERATOR, /* MATCH_CASE */
280
    metakind::OPERATOR, /* MATCH_BIND_CASE */
281
    metakind::CONSTANT, /* TUPLE_PROJECT_OP */
282
    metakind::PARAMETERIZED, /* TUPLE_PROJECT */
283
284
    /* from sep */
285
    metakind::NULLARY_OPERATOR, /* SEP_NIL */
286
    metakind::OPERATOR, /* SEP_EMP */
287
    metakind::OPERATOR, /* SEP_PTO */
288
    metakind::OPERATOR, /* SEP_STAR */
289
    metakind::OPERATOR, /* SEP_WAND */
290
    metakind::OPERATOR, /* SEP_LABEL */
291
292
    /* from sets */
293
    metakind::CONSTANT, /* EMPTYSET */
294
    metakind::OPERATOR, /* SET_TYPE */
295
    metakind::OPERATOR, /* UNION */
296
    metakind::OPERATOR, /* INTERSECTION */
297
    metakind::OPERATOR, /* SETMINUS */
298
    metakind::OPERATOR, /* SUBSET */
299
    metakind::OPERATOR, /* MEMBER */
300
    metakind::CONSTANT, /* SINGLETON_OP */
301
    metakind::PARAMETERIZED, /* SINGLETON */
302
    metakind::OPERATOR, /* INSERT */
303
    metakind::OPERATOR, /* CARD */
304
    metakind::OPERATOR, /* COMPLEMENT */
305
    metakind::NULLARY_OPERATOR, /* UNIVERSE_SET */
306
    metakind::OPERATOR, /* COMPREHENSION */
307
    metakind::OPERATOR, /* CHOOSE */
308
    metakind::OPERATOR, /* IS_SINGLETON */
309
    metakind::OPERATOR, /* JOIN */
310
    metakind::OPERATOR, /* PRODUCT */
311
    metakind::OPERATOR, /* TRANSPOSE */
312
    metakind::OPERATOR, /* TCLOSURE */
313
    metakind::OPERATOR, /* JOIN_IMAGE */
314
    metakind::OPERATOR, /* IDEN */
315
316
    /* from bags */
317
    metakind::CONSTANT, /* EMPTYBAG */
318
    metakind::OPERATOR, /* BAG_TYPE */
319
    metakind::OPERATOR, /* UNION_MAX */
320
    metakind::OPERATOR, /* UNION_DISJOINT */
321
    metakind::OPERATOR, /* INTERSECTION_MIN */
322
    metakind::OPERATOR, /* DIFFERENCE_SUBTRACT */
323
    metakind::OPERATOR, /* DIFFERENCE_REMOVE */
324
    metakind::OPERATOR, /* SUBBAG */
325
    metakind::OPERATOR, /* BAG_COUNT */
326
    metakind::OPERATOR, /* DUPLICATE_REMOVAL */
327
    metakind::CONSTANT, /* MK_BAG_OP */
328
    metakind::PARAMETERIZED, /* MK_BAG */
329
    metakind::OPERATOR, /* BAG_IS_SINGLETON */
330
    metakind::OPERATOR, /* BAG_CARD */
331
    metakind::OPERATOR, /* BAG_FROM_SET */
332
    metakind::OPERATOR, /* BAG_TO_SET */
333
    metakind::OPERATOR, /* BAG_CHOOSE */
334
335
    /* from strings */
336
    metakind::OPERATOR, /* STRING_CONCAT */
337
    metakind::OPERATOR, /* STRING_IN_REGEXP */
338
    metakind::OPERATOR, /* STRING_LENGTH */
339
    metakind::OPERATOR, /* STRING_SUBSTR */
340
    metakind::OPERATOR, /* STRING_UPDATE */
341
    metakind::OPERATOR, /* STRING_CHARAT */
342
    metakind::OPERATOR, /* STRING_STRCTN */
343
    metakind::OPERATOR, /* STRING_LT */
344
    metakind::OPERATOR, /* STRING_LEQ */
345
    metakind::OPERATOR, /* STRING_STRIDOF */
346
    metakind::OPERATOR, /* STRING_STRREPL */
347
    metakind::OPERATOR, /* STRING_STRREPLALL */
348
    metakind::OPERATOR, /* STRING_REPLACE_RE */
349
    metakind::OPERATOR, /* STRING_REPLACE_RE_ALL */
350
    metakind::OPERATOR, /* STRING_PREFIX */
351
    metakind::OPERATOR, /* STRING_SUFFIX */
352
    metakind::OPERATOR, /* STRING_IS_DIGIT */
353
    metakind::OPERATOR, /* STRING_ITOS */
354
    metakind::OPERATOR, /* STRING_STOI */
355
    metakind::OPERATOR, /* STRING_TO_CODE */
356
    metakind::OPERATOR, /* STRING_FROM_CODE */
357
    metakind::OPERATOR, /* STRING_TOLOWER */
358
    metakind::OPERATOR, /* STRING_TOUPPER */
359
    metakind::OPERATOR, /* STRING_REV */
360
    metakind::CONSTANT, /* CONST_STRING */
361
    metakind::OPERATOR, /* SEQUENCE_TYPE */
362
    metakind::CONSTANT, /* CONST_SEQUENCE */
363
    metakind::OPERATOR, /* SEQ_UNIT */
364
    metakind::OPERATOR, /* SEQ_NTH */
365
    metakind::OPERATOR, /* SEQ_NTH_TOTAL */
366
    metakind::OPERATOR, /* STRING_TO_REGEXP */
367
    metakind::OPERATOR, /* REGEXP_CONCAT */
368
    metakind::OPERATOR, /* REGEXP_UNION */
369
    metakind::OPERATOR, /* REGEXP_INTER */
370
    metakind::OPERATOR, /* REGEXP_DIFF */
371
    metakind::OPERATOR, /* REGEXP_STAR */
372
    metakind::OPERATOR, /* REGEXP_PLUS */
373
    metakind::OPERATOR, /* REGEXP_OPT */
374
    metakind::OPERATOR, /* REGEXP_RANGE */
375
    metakind::OPERATOR, /* REGEXP_COMPLEMENT */
376
    metakind::OPERATOR, /* REGEXP_EMPTY */
377
    metakind::OPERATOR, /* REGEXP_SIGMA */
378
    metakind::CONSTANT, /* REGEXP_REPEAT_OP */
379
    metakind::PARAMETERIZED, /* REGEXP_REPEAT */
380
    metakind::CONSTANT, /* REGEXP_LOOP_OP */
381
    metakind::PARAMETERIZED, /* REGEXP_LOOP */
382
    metakind::OPERATOR, /* REGEXP_RV */
383
384
    /* from quantifiers */
385
    metakind::OPERATOR, /* FORALL */
386
    metakind::OPERATOR, /* EXISTS */
387
    metakind::VARIABLE, /* INST_CONSTANT */
388
    metakind::OPERATOR, /* BOUND_VAR_LIST */
389
    metakind::OPERATOR, /* INST_PATTERN */
390
    metakind::OPERATOR, /* INST_NO_PATTERN */
391
    metakind::OPERATOR, /* INST_ATTRIBUTE */
392
    metakind::OPERATOR, /* INST_PATTERN_LIST */
393
394
    metakind::INVALID /* LAST_KIND */
395
  };/* metaKinds[] */
396
397
5561210349
  Assert(k >= kind::NULL_EXPR && k < kind::LAST_KIND);
398
399
  // We've asserted that k >= NULL_EXPR (which is 0), but we still
400
  // handle the UNDEFINED_KIND (-1) case.  If we don't, the compiler
401
  // emits warnings for non-assertion builds, since the check isn't done.
402
5561210349
  return metaKinds[k + 1];
403
}/* metaKindOf(k) */
404
405
}/* CVC4::kind namespace */
406
407
namespace expr {
408
409
410
// The reinterpret_cast of d_children to "::CVC4::UninterpretedConstant const*"
411
// flags a "strict aliasing" warning; it's okay, because we never access
412
// the embedded constant as a NodeValue* child, and never access an embedded
413
// NodeValue* child as a constant.
414
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
415
416
template <>
417
92713
::CVC4::UninterpretedConstant const& NodeValue::getConst< ::CVC4::UninterpretedConstant >() const {
418
92713
  AssertArgument(getKind() == ::CVC4::kind::UNINTERPRETED_CONSTANT, *this,
419
                 "Improper kind for getConst<::CVC4::UninterpretedConstant>()");
420
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
421
  // "constructed" when initially checking them against the NodeManager
422
  // pool), we must check d_nchildren here.
423
92713
  return d_nchildren == 0
424
92713
    ? *reinterpret_cast< ::CVC4::UninterpretedConstant const* >(d_children)
425
92713
    : *reinterpret_cast< ::CVC4::UninterpretedConstant const* >(d_children[0]);
426
}
427
428
// re-enable the warning
429
#pragma GCC diagnostic warning "-Wstrict-aliasing"
430
431
432
// The reinterpret_cast of d_children to "::CVC4::AbstractValue const*"
433
// flags a "strict aliasing" warning; it's okay, because we never access
434
// the embedded constant as a NodeValue* child, and never access an embedded
435
// NodeValue* child as a constant.
436
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
437
438
template <>
439
136
::CVC4::AbstractValue const& NodeValue::getConst< ::CVC4::AbstractValue >() const {
440
136
  AssertArgument(getKind() == ::CVC4::kind::ABSTRACT_VALUE, *this,
441
                 "Improper kind for getConst<::CVC4::AbstractValue>()");
442
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
443
  // "constructed" when initially checking them against the NodeManager
444
  // pool), we must check d_nchildren here.
445
136
  return d_nchildren == 0
446
136
    ? *reinterpret_cast< ::CVC4::AbstractValue const* >(d_children)
447
136
    : *reinterpret_cast< ::CVC4::AbstractValue const* >(d_children[0]);
448
}
449
450
// re-enable the warning
451
#pragma GCC diagnostic warning "-Wstrict-aliasing"
452
453
454
// The reinterpret_cast of d_children to "::CVC4::Kind const*"
455
// flags a "strict aliasing" warning; it's okay, because we never access
456
// the embedded constant as a NodeValue* child, and never access an embedded
457
// NodeValue* child as a constant.
458
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
459
460
template <>
461
17320196
::CVC4::Kind const& NodeValue::getConst< ::CVC4::Kind >() const {
462
17320196
  AssertArgument(getKind() == ::CVC4::kind::BUILTIN, *this,
463
                 "Improper kind for getConst<::CVC4::Kind>()");
464
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
465
  // "constructed" when initially checking them against the NodeManager
466
  // pool), we must check d_nchildren here.
467
17320196
  return d_nchildren == 0
468
17320196
    ? *reinterpret_cast< ::CVC4::Kind const* >(d_children)
469
17320196
    : *reinterpret_cast< ::CVC4::Kind const* >(d_children[0]);
470
}
471
472
// re-enable the warning
473
#pragma GCC diagnostic warning "-Wstrict-aliasing"
474
475
476
// The reinterpret_cast of d_children to "::CVC4::TypeConstant const*"
477
// flags a "strict aliasing" warning; it's okay, because we never access
478
// the embedded constant as a NodeValue* child, and never access an embedded
479
// NodeValue* child as a constant.
480
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
481
482
template <>
483
403320655
::CVC4::TypeConstant const& NodeValue::getConst< ::CVC4::TypeConstant >() const {
484
403320655
  AssertArgument(getKind() == ::CVC4::kind::TYPE_CONSTANT, *this,
485
                 "Improper kind for getConst<::CVC4::TypeConstant>()");
486
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
487
  // "constructed" when initially checking them against the NodeManager
488
  // pool), we must check d_nchildren here.
489
403320655
  return d_nchildren == 0
490
403320655
    ? *reinterpret_cast< ::CVC4::TypeConstant const* >(d_children)
491
403320655
    : *reinterpret_cast< ::CVC4::TypeConstant const* >(d_children[0]);
492
}
493
494
// re-enable the warning
495
#pragma GCC diagnostic warning "-Wstrict-aliasing"
496
497
498
// The reinterpret_cast of d_children to "bool const*"
499
// flags a "strict aliasing" warning; it's okay, because we never access
500
// the embedded constant as a NodeValue* child, and never access an embedded
501
// NodeValue* child as a constant.
502
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
503
504
template <>
505
85838672
bool const& NodeValue::getConst< bool >() const {
506
85838672
  AssertArgument(getKind() == ::CVC4::kind::CONST_BOOLEAN, *this,
507
                 "Improper kind for getConst<bool>()");
508
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
509
  // "constructed" when initially checking them against the NodeManager
510
  // pool), we must check d_nchildren here.
511
85838672
  return d_nchildren == 0
512
85838672
    ? *reinterpret_cast< bool const* >(d_children)
513
85838672
    : *reinterpret_cast< bool const* >(d_children[0]);
514
}
515
516
// re-enable the warning
517
#pragma GCC diagnostic warning "-Wstrict-aliasing"
518
519
520
// The reinterpret_cast of d_children to "::CVC4::Divisible const*"
521
// flags a "strict aliasing" warning; it's okay, because we never access
522
// the embedded constant as a NodeValue* child, and never access an embedded
523
// NodeValue* child as a constant.
524
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
525
526
template <>
527
74
::CVC4::Divisible const& NodeValue::getConst< ::CVC4::Divisible >() const {
528
74
  AssertArgument(getKind() == ::CVC4::kind::DIVISIBLE_OP, *this,
529
                 "Improper kind for getConst<::CVC4::Divisible>()");
530
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
531
  // "constructed" when initially checking them against the NodeManager
532
  // pool), we must check d_nchildren here.
533
74
  return d_nchildren == 0
534
74
    ? *reinterpret_cast< ::CVC4::Divisible const* >(d_children)
535
74
    : *reinterpret_cast< ::CVC4::Divisible const* >(d_children[0]);
536
}
537
538
// re-enable the warning
539
#pragma GCC diagnostic warning "-Wstrict-aliasing"
540
541
542
// The reinterpret_cast of d_children to "::CVC4::Rational const*"
543
// flags a "strict aliasing" warning; it's okay, because we never access
544
// the embedded constant as a NodeValue* child, and never access an embedded
545
// NodeValue* child as a constant.
546
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
547
548
template <>
549
748886444
::CVC4::Rational const& NodeValue::getConst< ::CVC4::Rational >() const {
550
748886444
  AssertArgument(getKind() == ::CVC4::kind::CONST_RATIONAL, *this,
551
                 "Improper kind for getConst<::CVC4::Rational>()");
552
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
553
  // "constructed" when initially checking them against the NodeManager
554
  // pool), we must check d_nchildren here.
555
748886444
  return d_nchildren == 0
556
748886444
    ? *reinterpret_cast< ::CVC4::Rational const* >(d_children)
557
748886444
    : *reinterpret_cast< ::CVC4::Rational const* >(d_children[0]);
558
}
559
560
// re-enable the warning
561
#pragma GCC diagnostic warning "-Wstrict-aliasing"
562
563
564
// The reinterpret_cast of d_children to "::CVC4::IndexedRootPredicate const*"
565
// flags a "strict aliasing" warning; it's okay, because we never access
566
// the embedded constant as a NodeValue* child, and never access an embedded
567
// NodeValue* child as a constant.
568
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
569
570
template <>
571
::CVC4::IndexedRootPredicate const& NodeValue::getConst< ::CVC4::IndexedRootPredicate >() const {
572
  AssertArgument(getKind() == ::CVC4::kind::INDEXED_ROOT_PREDICATE_OP, *this,
573
                 "Improper kind for getConst<::CVC4::IndexedRootPredicate>()");
574
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
575
  // "constructed" when initially checking them against the NodeManager
576
  // pool), we must check d_nchildren here.
577
  return d_nchildren == 0
578
    ? *reinterpret_cast< ::CVC4::IndexedRootPredicate const* >(d_children)
579
    : *reinterpret_cast< ::CVC4::IndexedRootPredicate const* >(d_children[0]);
580
}
581
582
// re-enable the warning
583
#pragma GCC diagnostic warning "-Wstrict-aliasing"
584
585
586
// The reinterpret_cast of d_children to "::CVC4::IntAnd const*"
587
// flags a "strict aliasing" warning; it's okay, because we never access
588
// the embedded constant as a NodeValue* child, and never access an embedded
589
// NodeValue* child as a constant.
590
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
591
592
template <>
593
976
::CVC4::IntAnd const& NodeValue::getConst< ::CVC4::IntAnd >() const {
594
976
  AssertArgument(getKind() == ::CVC4::kind::IAND_OP, *this,
595
                 "Improper kind for getConst<::CVC4::IntAnd>()");
596
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
597
  // "constructed" when initially checking them against the NodeManager
598
  // pool), we must check d_nchildren here.
599
976
  return d_nchildren == 0
600
976
    ? *reinterpret_cast< ::CVC4::IntAnd const* >(d_children)
601
976
    : *reinterpret_cast< ::CVC4::IntAnd const* >(d_children[0]);
602
}
603
604
// re-enable the warning
605
#pragma GCC diagnostic warning "-Wstrict-aliasing"
606
607
608
// The reinterpret_cast of d_children to "::CVC4::BitVectorSize const*"
609
// flags a "strict aliasing" warning; it's okay, because we never access
610
// the embedded constant as a NodeValue* child, and never access an embedded
611
// NodeValue* child as a constant.
612
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
613
614
template <>
615
6732465
::CVC4::BitVectorSize const& NodeValue::getConst< ::CVC4::BitVectorSize >() const {
616
6732465
  AssertArgument(getKind() == ::CVC4::kind::BITVECTOR_TYPE, *this,
617
                 "Improper kind for getConst<::CVC4::BitVectorSize>()");
618
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
619
  // "constructed" when initially checking them against the NodeManager
620
  // pool), we must check d_nchildren here.
621
6732465
  return d_nchildren == 0
622
6732465
    ? *reinterpret_cast< ::CVC4::BitVectorSize const* >(d_children)
623
6732465
    : *reinterpret_cast< ::CVC4::BitVectorSize const* >(d_children[0]);
624
}
625
626
// re-enable the warning
627
#pragma GCC diagnostic warning "-Wstrict-aliasing"
628
629
630
// The reinterpret_cast of d_children to "::CVC4::BitVector const*"
631
// flags a "strict aliasing" warning; it's okay, because we never access
632
// the embedded constant as a NodeValue* child, and never access an embedded
633
// NodeValue* child as a constant.
634
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
635
636
template <>
637
30929100
::CVC4::BitVector const& NodeValue::getConst< ::CVC4::BitVector >() const {
638
30929100
  AssertArgument(getKind() == ::CVC4::kind::CONST_BITVECTOR, *this,
639
                 "Improper kind for getConst<::CVC4::BitVector>()");
640
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
641
  // "constructed" when initially checking them against the NodeManager
642
  // pool), we must check d_nchildren here.
643
30929100
  return d_nchildren == 0
644
30929100
    ? *reinterpret_cast< ::CVC4::BitVector const* >(d_children)
645
30929100
    : *reinterpret_cast< ::CVC4::BitVector const* >(d_children[0]);
646
}
647
648
// re-enable the warning
649
#pragma GCC diagnostic warning "-Wstrict-aliasing"
650
651
652
// The reinterpret_cast of d_children to "::CVC4::BitVectorBitOf const*"
653
// flags a "strict aliasing" warning; it's okay, because we never access
654
// the embedded constant as a NodeValue* child, and never access an embedded
655
// NodeValue* child as a constant.
656
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
657
658
template <>
659
649619
::CVC4::BitVectorBitOf const& NodeValue::getConst< ::CVC4::BitVectorBitOf >() const {
660
649619
  AssertArgument(getKind() == ::CVC4::kind::BITVECTOR_BITOF_OP, *this,
661
                 "Improper kind for getConst<::CVC4::BitVectorBitOf>()");
662
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
663
  // "constructed" when initially checking them against the NodeManager
664
  // pool), we must check d_nchildren here.
665
649619
  return d_nchildren == 0
666
649619
    ? *reinterpret_cast< ::CVC4::BitVectorBitOf const* >(d_children)
667
649619
    : *reinterpret_cast< ::CVC4::BitVectorBitOf const* >(d_children[0]);
668
}
669
670
// re-enable the warning
671
#pragma GCC diagnostic warning "-Wstrict-aliasing"
672
673
674
// The reinterpret_cast of d_children to "::CVC4::BitVectorExtract const*"
675
// flags a "strict aliasing" warning; it's okay, because we never access
676
// the embedded constant as a NodeValue* child, and never access an embedded
677
// NodeValue* child as a constant.
678
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
679
680
template <>
681
1611589
::CVC4::BitVectorExtract const& NodeValue::getConst< ::CVC4::BitVectorExtract >() const {
682
1611589
  AssertArgument(getKind() == ::CVC4::kind::BITVECTOR_EXTRACT_OP, *this,
683
                 "Improper kind for getConst<::CVC4::BitVectorExtract>()");
684
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
685
  // "constructed" when initially checking them against the NodeManager
686
  // pool), we must check d_nchildren here.
687
1611589
  return d_nchildren == 0
688
1611589
    ? *reinterpret_cast< ::CVC4::BitVectorExtract const* >(d_children)
689
1611589
    : *reinterpret_cast< ::CVC4::BitVectorExtract const* >(d_children[0]);
690
}
691
692
// re-enable the warning
693
#pragma GCC diagnostic warning "-Wstrict-aliasing"
694
695
696
// The reinterpret_cast of d_children to "::CVC4::BitVectorRepeat const*"
697
// flags a "strict aliasing" warning; it's okay, because we never access
698
// the embedded constant as a NodeValue* child, and never access an embedded
699
// NodeValue* child as a constant.
700
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
701
702
template <>
703
9328
::CVC4::BitVectorRepeat const& NodeValue::getConst< ::CVC4::BitVectorRepeat >() const {
704
9328
  AssertArgument(getKind() == ::CVC4::kind::BITVECTOR_REPEAT_OP, *this,
705
                 "Improper kind for getConst<::CVC4::BitVectorRepeat>()");
706
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
707
  // "constructed" when initially checking them against the NodeManager
708
  // pool), we must check d_nchildren here.
709
9328
  return d_nchildren == 0
710
9328
    ? *reinterpret_cast< ::CVC4::BitVectorRepeat const* >(d_children)
711
9328
    : *reinterpret_cast< ::CVC4::BitVectorRepeat const* >(d_children[0]);
712
}
713
714
// re-enable the warning
715
#pragma GCC diagnostic warning "-Wstrict-aliasing"
716
717
718
// The reinterpret_cast of d_children to "::CVC4::BitVectorRotateLeft const*"
719
// flags a "strict aliasing" warning; it's okay, because we never access
720
// the embedded constant as a NodeValue* child, and never access an embedded
721
// NodeValue* child as a constant.
722
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
723
724
template <>
725
5078
::CVC4::BitVectorRotateLeft const& NodeValue::getConst< ::CVC4::BitVectorRotateLeft >() const {
726
5078
  AssertArgument(getKind() == ::CVC4::kind::BITVECTOR_ROTATE_LEFT_OP, *this,
727
                 "Improper kind for getConst<::CVC4::BitVectorRotateLeft>()");
728
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
729
  // "constructed" when initially checking them against the NodeManager
730
  // pool), we must check d_nchildren here.
731
5078
  return d_nchildren == 0
732
5078
    ? *reinterpret_cast< ::CVC4::BitVectorRotateLeft const* >(d_children)
733
5078
    : *reinterpret_cast< ::CVC4::BitVectorRotateLeft const* >(d_children[0]);
734
}
735
736
// re-enable the warning
737
#pragma GCC diagnostic warning "-Wstrict-aliasing"
738
739
740
// The reinterpret_cast of d_children to "::CVC4::BitVectorRotateRight const*"
741
// flags a "strict aliasing" warning; it's okay, because we never access
742
// the embedded constant as a NodeValue* child, and never access an embedded
743
// NodeValue* child as a constant.
744
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
745
746
template <>
747
5930
::CVC4::BitVectorRotateRight const& NodeValue::getConst< ::CVC4::BitVectorRotateRight >() const {
748
5930
  AssertArgument(getKind() == ::CVC4::kind::BITVECTOR_ROTATE_RIGHT_OP, *this,
749
                 "Improper kind for getConst<::CVC4::BitVectorRotateRight>()");
750
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
751
  // "constructed" when initially checking them against the NodeManager
752
  // pool), we must check d_nchildren here.
753
5930
  return d_nchildren == 0
754
5930
    ? *reinterpret_cast< ::CVC4::BitVectorRotateRight const* >(d_children)
755
5930
    : *reinterpret_cast< ::CVC4::BitVectorRotateRight const* >(d_children[0]);
756
}
757
758
// re-enable the warning
759
#pragma GCC diagnostic warning "-Wstrict-aliasing"
760
761
762
// The reinterpret_cast of d_children to "::CVC4::BitVectorSignExtend const*"
763
// flags a "strict aliasing" warning; it's okay, because we never access
764
// the embedded constant as a NodeValue* child, and never access an embedded
765
// NodeValue* child as a constant.
766
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
767
768
template <>
769
98024
::CVC4::BitVectorSignExtend const& NodeValue::getConst< ::CVC4::BitVectorSignExtend >() const {
770
98024
  AssertArgument(getKind() == ::CVC4::kind::BITVECTOR_SIGN_EXTEND_OP, *this,
771
                 "Improper kind for getConst<::CVC4::BitVectorSignExtend>()");
772
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
773
  // "constructed" when initially checking them against the NodeManager
774
  // pool), we must check d_nchildren here.
775
98024
  return d_nchildren == 0
776
98024
    ? *reinterpret_cast< ::CVC4::BitVectorSignExtend const* >(d_children)
777
98024
    : *reinterpret_cast< ::CVC4::BitVectorSignExtend const* >(d_children[0]);
778
}
779
780
// re-enable the warning
781
#pragma GCC diagnostic warning "-Wstrict-aliasing"
782
783
784
// The reinterpret_cast of d_children to "::CVC4::BitVectorZeroExtend const*"
785
// flags a "strict aliasing" warning; it's okay, because we never access
786
// the embedded constant as a NodeValue* child, and never access an embedded
787
// NodeValue* child as a constant.
788
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
789
790
template <>
791
128154
::CVC4::BitVectorZeroExtend const& NodeValue::getConst< ::CVC4::BitVectorZeroExtend >() const {
792
128154
  AssertArgument(getKind() == ::CVC4::kind::BITVECTOR_ZERO_EXTEND_OP, *this,
793
                 "Improper kind for getConst<::CVC4::BitVectorZeroExtend>()");
794
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
795
  // "constructed" when initially checking them against the NodeManager
796
  // pool), we must check d_nchildren here.
797
128154
  return d_nchildren == 0
798
128154
    ? *reinterpret_cast< ::CVC4::BitVectorZeroExtend const* >(d_children)
799
128154
    : *reinterpret_cast< ::CVC4::BitVectorZeroExtend const* >(d_children[0]);
800
}
801
802
// re-enable the warning
803
#pragma GCC diagnostic warning "-Wstrict-aliasing"
804
805
806
// The reinterpret_cast of d_children to "::CVC4::IntToBitVector const*"
807
// flags a "strict aliasing" warning; it's okay, because we never access
808
// the embedded constant as a NodeValue* child, and never access an embedded
809
// NodeValue* child as a constant.
810
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
811
812
template <>
813
3285
::CVC4::IntToBitVector const& NodeValue::getConst< ::CVC4::IntToBitVector >() const {
814
3285
  AssertArgument(getKind() == ::CVC4::kind::INT_TO_BITVECTOR_OP, *this,
815
                 "Improper kind for getConst<::CVC4::IntToBitVector>()");
816
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
817
  // "constructed" when initially checking them against the NodeManager
818
  // pool), we must check d_nchildren here.
819
3285
  return d_nchildren == 0
820
3285
    ? *reinterpret_cast< ::CVC4::IntToBitVector const* >(d_children)
821
3285
    : *reinterpret_cast< ::CVC4::IntToBitVector const* >(d_children[0]);
822
}
823
824
// re-enable the warning
825
#pragma GCC diagnostic warning "-Wstrict-aliasing"
826
827
828
// The reinterpret_cast of d_children to "::CVC4::FloatingPoint const*"
829
// flags a "strict aliasing" warning; it's okay, because we never access
830
// the embedded constant as a NodeValue* child, and never access an embedded
831
// NodeValue* child as a constant.
832
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
833
834
template <>
835
10670
::CVC4::FloatingPoint const& NodeValue::getConst< ::CVC4::FloatingPoint >() const {
836
10670
  AssertArgument(getKind() == ::CVC4::kind::CONST_FLOATINGPOINT, *this,
837
                 "Improper kind for getConst<::CVC4::FloatingPoint>()");
838
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
839
  // "constructed" when initially checking them against the NodeManager
840
  // pool), we must check d_nchildren here.
841
10670
  return d_nchildren == 0
842
10670
    ? *reinterpret_cast< ::CVC4::FloatingPoint const* >(d_children)
843
10670
    : *reinterpret_cast< ::CVC4::FloatingPoint const* >(d_children[0]);
844
}
845
846
// re-enable the warning
847
#pragma GCC diagnostic warning "-Wstrict-aliasing"
848
849
850
// The reinterpret_cast of d_children to "::CVC4::RoundingMode const*"
851
// flags a "strict aliasing" warning; it's okay, because we never access
852
// the embedded constant as a NodeValue* child, and never access an embedded
853
// NodeValue* child as a constant.
854
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
855
856
template <>
857
77144
::CVC4::RoundingMode const& NodeValue::getConst< ::CVC4::RoundingMode >() const {
858
77144
  AssertArgument(getKind() == ::CVC4::kind::CONST_ROUNDINGMODE, *this,
859
                 "Improper kind for getConst<::CVC4::RoundingMode>()");
860
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
861
  // "constructed" when initially checking them against the NodeManager
862
  // pool), we must check d_nchildren here.
863
77144
  return d_nchildren == 0
864
77144
    ? *reinterpret_cast< ::CVC4::RoundingMode const* >(d_children)
865
77144
    : *reinterpret_cast< ::CVC4::RoundingMode const* >(d_children[0]);
866
}
867
868
// re-enable the warning
869
#pragma GCC diagnostic warning "-Wstrict-aliasing"
870
871
872
// The reinterpret_cast of d_children to "::CVC4::FloatingPointSize const*"
873
// flags a "strict aliasing" warning; it's okay, because we never access
874
// the embedded constant as a NodeValue* child, and never access an embedded
875
// NodeValue* child as a constant.
876
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
877
878
template <>
879
65451
::CVC4::FloatingPointSize const& NodeValue::getConst< ::CVC4::FloatingPointSize >() const {
880
65451
  AssertArgument(getKind() == ::CVC4::kind::FLOATINGPOINT_TYPE, *this,
881
                 "Improper kind for getConst<::CVC4::FloatingPointSize>()");
882
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
883
  // "constructed" when initially checking them against the NodeManager
884
  // pool), we must check d_nchildren here.
885
65451
  return d_nchildren == 0
886
65451
    ? *reinterpret_cast< ::CVC4::FloatingPointSize const* >(d_children)
887
65451
    : *reinterpret_cast< ::CVC4::FloatingPointSize const* >(d_children[0]);
888
}
889
890
// re-enable the warning
891
#pragma GCC diagnostic warning "-Wstrict-aliasing"
892
893
894
// The reinterpret_cast of d_children to "::CVC4::FloatingPointToFPIEEEBitVector const*"
895
// flags a "strict aliasing" warning; it's okay, because we never access
896
// the embedded constant as a NodeValue* child, and never access an embedded
897
// NodeValue* child as a constant.
898
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
899
900
template <>
901
7478
::CVC4::FloatingPointToFPIEEEBitVector const& NodeValue::getConst< ::CVC4::FloatingPointToFPIEEEBitVector >() const {
902
7478
  AssertArgument(getKind() == ::CVC4::kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP, *this,
903
                 "Improper kind for getConst<::CVC4::FloatingPointToFPIEEEBitVector>()");
904
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
905
  // "constructed" when initially checking them against the NodeManager
906
  // pool), we must check d_nchildren here.
907
7478
  return d_nchildren == 0
908
7478
    ? *reinterpret_cast< ::CVC4::FloatingPointToFPIEEEBitVector const* >(d_children)
909
7478
    : *reinterpret_cast< ::CVC4::FloatingPointToFPIEEEBitVector const* >(d_children[0]);
910
}
911
912
// re-enable the warning
913
#pragma GCC diagnostic warning "-Wstrict-aliasing"
914
915
916
// The reinterpret_cast of d_children to "::CVC4::FloatingPointToFPFloatingPoint const*"
917
// flags a "strict aliasing" warning; it's okay, because we never access
918
// the embedded constant as a NodeValue* child, and never access an embedded
919
// NodeValue* child as a constant.
920
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
921
922
template <>
923
78
::CVC4::FloatingPointToFPFloatingPoint const& NodeValue::getConst< ::CVC4::FloatingPointToFPFloatingPoint >() const {
924
78
  AssertArgument(getKind() == ::CVC4::kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP, *this,
925
                 "Improper kind for getConst<::CVC4::FloatingPointToFPFloatingPoint>()");
926
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
927
  // "constructed" when initially checking them against the NodeManager
928
  // pool), we must check d_nchildren here.
929
78
  return d_nchildren == 0
930
78
    ? *reinterpret_cast< ::CVC4::FloatingPointToFPFloatingPoint const* >(d_children)
931
78
    : *reinterpret_cast< ::CVC4::FloatingPointToFPFloatingPoint const* >(d_children[0]);
932
}
933
934
// re-enable the warning
935
#pragma GCC diagnostic warning "-Wstrict-aliasing"
936
937
938
// The reinterpret_cast of d_children to "::CVC4::FloatingPointToFPReal const*"
939
// flags a "strict aliasing" warning; it's okay, because we never access
940
// the embedded constant as a NodeValue* child, and never access an embedded
941
// NodeValue* child as a constant.
942
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
943
944
template <>
945
167
::CVC4::FloatingPointToFPReal const& NodeValue::getConst< ::CVC4::FloatingPointToFPReal >() const {
946
167
  AssertArgument(getKind() == ::CVC4::kind::FLOATINGPOINT_TO_FP_REAL_OP, *this,
947
                 "Improper kind for getConst<::CVC4::FloatingPointToFPReal>()");
948
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
949
  // "constructed" when initially checking them against the NodeManager
950
  // pool), we must check d_nchildren here.
951
167
  return d_nchildren == 0
952
167
    ? *reinterpret_cast< ::CVC4::FloatingPointToFPReal const* >(d_children)
953
167
    : *reinterpret_cast< ::CVC4::FloatingPointToFPReal const* >(d_children[0]);
954
}
955
956
// re-enable the warning
957
#pragma GCC diagnostic warning "-Wstrict-aliasing"
958
959
960
// The reinterpret_cast of d_children to "::CVC4::FloatingPointToFPSignedBitVector const*"
961
// flags a "strict aliasing" warning; it's okay, because we never access
962
// the embedded constant as a NodeValue* child, and never access an embedded
963
// NodeValue* child as a constant.
964
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
965
966
template <>
967
56
::CVC4::FloatingPointToFPSignedBitVector const& NodeValue::getConst< ::CVC4::FloatingPointToFPSignedBitVector >() const {
968
56
  AssertArgument(getKind() == ::CVC4::kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP, *this,
969
                 "Improper kind for getConst<::CVC4::FloatingPointToFPSignedBitVector>()");
970
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
971
  // "constructed" when initially checking them against the NodeManager
972
  // pool), we must check d_nchildren here.
973
56
  return d_nchildren == 0
974
56
    ? *reinterpret_cast< ::CVC4::FloatingPointToFPSignedBitVector const* >(d_children)
975
56
    : *reinterpret_cast< ::CVC4::FloatingPointToFPSignedBitVector const* >(d_children[0]);
976
}
977
978
// re-enable the warning
979
#pragma GCC diagnostic warning "-Wstrict-aliasing"
980
981
982
// The reinterpret_cast of d_children to "::CVC4::FloatingPointToFPUnsignedBitVector const*"
983
// flags a "strict aliasing" warning; it's okay, because we never access
984
// the embedded constant as a NodeValue* child, and never access an embedded
985
// NodeValue* child as a constant.
986
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
987
988
template <>
989
20
::CVC4::FloatingPointToFPUnsignedBitVector const& NodeValue::getConst< ::CVC4::FloatingPointToFPUnsignedBitVector >() const {
990
20
  AssertArgument(getKind() == ::CVC4::kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP, *this,
991
                 "Improper kind for getConst<::CVC4::FloatingPointToFPUnsignedBitVector>()");
992
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
993
  // "constructed" when initially checking them against the NodeManager
994
  // pool), we must check d_nchildren here.
995
20
  return d_nchildren == 0
996
20
    ? *reinterpret_cast< ::CVC4::FloatingPointToFPUnsignedBitVector const* >(d_children)
997
20
    : *reinterpret_cast< ::CVC4::FloatingPointToFPUnsignedBitVector const* >(d_children[0]);
998
}
999
1000
// re-enable the warning
1001
#pragma GCC diagnostic warning "-Wstrict-aliasing"
1002
1003
1004
// The reinterpret_cast of d_children to "::CVC4::FloatingPointToFPGeneric const*"
1005
// flags a "strict aliasing" warning; it's okay, because we never access
1006
// the embedded constant as a NodeValue* child, and never access an embedded
1007
// NodeValue* child as a constant.
1008
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
1009
1010
template <>
1011
359
::CVC4::FloatingPointToFPGeneric const& NodeValue::getConst< ::CVC4::FloatingPointToFPGeneric >() const {
1012
359
  AssertArgument(getKind() == ::CVC4::kind::FLOATINGPOINT_TO_FP_GENERIC_OP, *this,
1013
                 "Improper kind for getConst<::CVC4::FloatingPointToFPGeneric>()");
1014
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
1015
  // "constructed" when initially checking them against the NodeManager
1016
  // pool), we must check d_nchildren here.
1017
359
  return d_nchildren == 0
1018
359
    ? *reinterpret_cast< ::CVC4::FloatingPointToFPGeneric const* >(d_children)
1019
359
    : *reinterpret_cast< ::CVC4::FloatingPointToFPGeneric const* >(d_children[0]);
1020
}
1021
1022
// re-enable the warning
1023
#pragma GCC diagnostic warning "-Wstrict-aliasing"
1024
1025
1026
// The reinterpret_cast of d_children to "::CVC4::FloatingPointToUBV const*"
1027
// flags a "strict aliasing" warning; it's okay, because we never access
1028
// the embedded constant as a NodeValue* child, and never access an embedded
1029
// NodeValue* child as a constant.
1030
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
1031
1032
template <>
1033
20
::CVC4::FloatingPointToUBV const& NodeValue::getConst< ::CVC4::FloatingPointToUBV >() const {
1034
20
  AssertArgument(getKind() == ::CVC4::kind::FLOATINGPOINT_TO_UBV_OP, *this,
1035
                 "Improper kind for getConst<::CVC4::FloatingPointToUBV>()");
1036
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
1037
  // "constructed" when initially checking them against the NodeManager
1038
  // pool), we must check d_nchildren here.
1039
20
  return d_nchildren == 0
1040
20
    ? *reinterpret_cast< ::CVC4::FloatingPointToUBV const* >(d_children)
1041
20
    : *reinterpret_cast< ::CVC4::FloatingPointToUBV const* >(d_children[0]);
1042
}
1043
1044
// re-enable the warning
1045
#pragma GCC diagnostic warning "-Wstrict-aliasing"
1046
1047
1048
// The reinterpret_cast of d_children to "::CVC4::FloatingPointToUBVTotal const*"
1049
// flags a "strict aliasing" warning; it's okay, because we never access
1050
// the embedded constant as a NodeValue* child, and never access an embedded
1051
// NodeValue* child as a constant.
1052
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
1053
1054
template <>
1055
::CVC4::FloatingPointToUBVTotal const& NodeValue::getConst< ::CVC4::FloatingPointToUBVTotal >() const {
1056
  AssertArgument(getKind() == ::CVC4::kind::FLOATINGPOINT_TO_UBV_TOTAL_OP, *this,
1057
                 "Improper kind for getConst<::CVC4::FloatingPointToUBVTotal>()");
1058
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
1059
  // "constructed" when initially checking them against the NodeManager
1060
  // pool), we must check d_nchildren here.
1061
  return d_nchildren == 0
1062
    ? *reinterpret_cast< ::CVC4::FloatingPointToUBVTotal const* >(d_children)
1063
    : *reinterpret_cast< ::CVC4::FloatingPointToUBVTotal const* >(d_children[0]);
1064
}
1065
1066
// re-enable the warning
1067
#pragma GCC diagnostic warning "-Wstrict-aliasing"
1068
1069
1070
// The reinterpret_cast of d_children to "::CVC4::FloatingPointToSBV const*"
1071
// flags a "strict aliasing" warning; it's okay, because we never access
1072
// the embedded constant as a NodeValue* child, and never access an embedded
1073
// NodeValue* child as a constant.
1074
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
1075
1076
template <>
1077
20
::CVC4::FloatingPointToSBV const& NodeValue::getConst< ::CVC4::FloatingPointToSBV >() const {
1078
20
  AssertArgument(getKind() == ::CVC4::kind::FLOATINGPOINT_TO_SBV_OP, *this,
1079
                 "Improper kind for getConst<::CVC4::FloatingPointToSBV>()");
1080
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
1081
  // "constructed" when initially checking them against the NodeManager
1082
  // pool), we must check d_nchildren here.
1083
20
  return d_nchildren == 0
1084
20
    ? *reinterpret_cast< ::CVC4::FloatingPointToSBV const* >(d_children)
1085
20
    : *reinterpret_cast< ::CVC4::FloatingPointToSBV const* >(d_children[0]);
1086
}
1087
1088
// re-enable the warning
1089
#pragma GCC diagnostic warning "-Wstrict-aliasing"
1090
1091
1092
// The reinterpret_cast of d_children to "::CVC4::FloatingPointToSBVTotal const*"
1093
// flags a "strict aliasing" warning; it's okay, because we never access
1094
// the embedded constant as a NodeValue* child, and never access an embedded
1095
// NodeValue* child as a constant.
1096
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
1097
1098
template <>
1099
::CVC4::FloatingPointToSBVTotal const& NodeValue::getConst< ::CVC4::FloatingPointToSBVTotal >() const {
1100
  AssertArgument(getKind() == ::CVC4::kind::FLOATINGPOINT_TO_SBV_TOTAL_OP, *this,
1101
                 "Improper kind for getConst<::CVC4::FloatingPointToSBVTotal>()");
1102
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
1103
  // "constructed" when initially checking them against the NodeManager
1104
  // pool), we must check d_nchildren here.
1105
  return d_nchildren == 0
1106
    ? *reinterpret_cast< ::CVC4::FloatingPointToSBVTotal const* >(d_children)
1107
    : *reinterpret_cast< ::CVC4::FloatingPointToSBVTotal const* >(d_children[0]);
1108
}
1109
1110
// re-enable the warning
1111
#pragma GCC diagnostic warning "-Wstrict-aliasing"
1112
1113
1114
// The reinterpret_cast of d_children to "::CVC4::ArrayStoreAll const*"
1115
// flags a "strict aliasing" warning; it's okay, because we never access
1116
// the embedded constant as a NodeValue* child, and never access an embedded
1117
// NodeValue* child as a constant.
1118
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
1119
1120
template <>
1121
34258
::CVC4::ArrayStoreAll const& NodeValue::getConst< ::CVC4::ArrayStoreAll >() const {
1122
34258
  AssertArgument(getKind() == ::CVC4::kind::STORE_ALL, *this,
1123
                 "Improper kind for getConst<::CVC4::ArrayStoreAll>()");
1124
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
1125
  // "constructed" when initially checking them against the NodeManager
1126
  // pool), we must check d_nchildren here.
1127
34258
  return d_nchildren == 0
1128
34258
    ? *reinterpret_cast< ::CVC4::ArrayStoreAll const* >(d_children)
1129
34258
    : *reinterpret_cast< ::CVC4::ArrayStoreAll const* >(d_children[0]);
1130
}
1131
1132
// re-enable the warning
1133
#pragma GCC diagnostic warning "-Wstrict-aliasing"
1134
1135
1136
// The reinterpret_cast of d_children to "::CVC4::DatatypeIndexConstant const*"
1137
// flags a "strict aliasing" warning; it's okay, because we never access
1138
// the embedded constant as a NodeValue* child, and never access an embedded
1139
// NodeValue* child as a constant.
1140
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
1141
1142
template <>
1143
5972214
::CVC4::DatatypeIndexConstant const& NodeValue::getConst< ::CVC4::DatatypeIndexConstant >() const {
1144
5972214
  AssertArgument(getKind() == ::CVC4::kind::DATATYPE_TYPE, *this,
1145
                 "Improper kind for getConst<::CVC4::DatatypeIndexConstant>()");
1146
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
1147
  // "constructed" when initially checking them against the NodeManager
1148
  // pool), we must check d_nchildren here.
1149
5972214
  return d_nchildren == 0
1150
5972214
    ? *reinterpret_cast< ::CVC4::DatatypeIndexConstant const* >(d_children)
1151
5972214
    : *reinterpret_cast< ::CVC4::DatatypeIndexConstant const* >(d_children[0]);
1152
}
1153
1154
// re-enable the warning
1155
#pragma GCC diagnostic warning "-Wstrict-aliasing"
1156
1157
1158
// The reinterpret_cast of d_children to "::CVC4::AscriptionType const*"
1159
// flags a "strict aliasing" warning; it's okay, because we never access
1160
// the embedded constant as a NodeValue* child, and never access an embedded
1161
// NodeValue* child as a constant.
1162
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
1163
1164
template <>
1165
1736
::CVC4::AscriptionType const& NodeValue::getConst< ::CVC4::AscriptionType >() const {
1166
1736
  AssertArgument(getKind() == ::CVC4::kind::ASCRIPTION_TYPE, *this,
1167
                 "Improper kind for getConst<::CVC4::AscriptionType>()");
1168
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
1169
  // "constructed" when initially checking them against the NodeManager
1170
  // pool), we must check d_nchildren here.
1171
1736
  return d_nchildren == 0
1172
1736
    ? *reinterpret_cast< ::CVC4::AscriptionType const* >(d_children)
1173
1736
    : *reinterpret_cast< ::CVC4::AscriptionType const* >(d_children[0]);
1174
}
1175
1176
// re-enable the warning
1177
#pragma GCC diagnostic warning "-Wstrict-aliasing"
1178
1179
1180
// The reinterpret_cast of d_children to "::CVC4::TupleUpdate const*"
1181
// flags a "strict aliasing" warning; it's okay, because we never access
1182
// the embedded constant as a NodeValue* child, and never access an embedded
1183
// NodeValue* child as a constant.
1184
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
1185
1186
template <>
1187
32
::CVC4::TupleUpdate const& NodeValue::getConst< ::CVC4::TupleUpdate >() const {
1188
32
  AssertArgument(getKind() == ::CVC4::kind::TUPLE_UPDATE_OP, *this,
1189
                 "Improper kind for getConst<::CVC4::TupleUpdate>()");
1190
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
1191
  // "constructed" when initially checking them against the NodeManager
1192
  // pool), we must check d_nchildren here.
1193
32
  return d_nchildren == 0
1194
32
    ? *reinterpret_cast< ::CVC4::TupleUpdate const* >(d_children)
1195
32
    : *reinterpret_cast< ::CVC4::TupleUpdate const* >(d_children[0]);
1196
}
1197
1198
// re-enable the warning
1199
#pragma GCC diagnostic warning "-Wstrict-aliasing"
1200
1201
1202
// The reinterpret_cast of d_children to "::CVC4::RecordUpdate const*"
1203
// flags a "strict aliasing" warning; it's okay, because we never access
1204
// the embedded constant as a NodeValue* child, and never access an embedded
1205
// NodeValue* child as a constant.
1206
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
1207
1208
template <>
1209
96
::CVC4::RecordUpdate const& NodeValue::getConst< ::CVC4::RecordUpdate >() const {
1210
96
  AssertArgument(getKind() == ::CVC4::kind::RECORD_UPDATE_OP, *this,
1211
                 "Improper kind for getConst<::CVC4::RecordUpdate>()");
1212
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
1213
  // "constructed" when initially checking them against the NodeManager
1214
  // pool), we must check d_nchildren here.
1215
96
  return d_nchildren == 0
1216
96
    ? *reinterpret_cast< ::CVC4::RecordUpdate const* >(d_children)
1217
96
    : *reinterpret_cast< ::CVC4::RecordUpdate const* >(d_children[0]);
1218
}
1219
1220
// re-enable the warning
1221
#pragma GCC diagnostic warning "-Wstrict-aliasing"
1222
1223
1224
// The reinterpret_cast of d_children to "::CVC4::TupleProjectOp const*"
1225
// flags a "strict aliasing" warning; it's okay, because we never access
1226
// the embedded constant as a NodeValue* child, and never access an embedded
1227
// NodeValue* child as a constant.
1228
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
1229
1230
template <>
1231
236
::CVC4::TupleProjectOp const& NodeValue::getConst< ::CVC4::TupleProjectOp >() const {
1232
236
  AssertArgument(getKind() == ::CVC4::kind::TUPLE_PROJECT_OP, *this,
1233
                 "Improper kind for getConst<::CVC4::TupleProjectOp>()");
1234
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
1235
  // "constructed" when initially checking them against the NodeManager
1236
  // pool), we must check d_nchildren here.
1237
236
  return d_nchildren == 0
1238
236
    ? *reinterpret_cast< ::CVC4::TupleProjectOp const* >(d_children)
1239
236
    : *reinterpret_cast< ::CVC4::TupleProjectOp const* >(d_children[0]);
1240
}
1241
1242
// re-enable the warning
1243
#pragma GCC diagnostic warning "-Wstrict-aliasing"
1244
1245
1246
// The reinterpret_cast of d_children to "::CVC4::EmptySet const*"
1247
// flags a "strict aliasing" warning; it's okay, because we never access
1248
// the embedded constant as a NodeValue* child, and never access an embedded
1249
// NodeValue* child as a constant.
1250
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
1251
1252
template <>
1253
19029
::CVC4::EmptySet const& NodeValue::getConst< ::CVC4::EmptySet >() const {
1254
19029
  AssertArgument(getKind() == ::CVC4::kind::EMPTYSET, *this,
1255
                 "Improper kind for getConst<::CVC4::EmptySet>()");
1256
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
1257
  // "constructed" when initially checking them against the NodeManager
1258
  // pool), we must check d_nchildren here.
1259
19029
  return d_nchildren == 0
1260
19029
    ? *reinterpret_cast< ::CVC4::EmptySet const* >(d_children)
1261
19029
    : *reinterpret_cast< ::CVC4::EmptySet const* >(d_children[0]);
1262
}
1263
1264
// re-enable the warning
1265
#pragma GCC diagnostic warning "-Wstrict-aliasing"
1266
1267
1268
// The reinterpret_cast of d_children to "::CVC4::SingletonOp const*"
1269
// flags a "strict aliasing" warning; it's okay, because we never access
1270
// the embedded constant as a NodeValue* child, and never access an embedded
1271
// NodeValue* child as a constant.
1272
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
1273
1274
template <>
1275
32306
::CVC4::SingletonOp const& NodeValue::getConst< ::CVC4::SingletonOp >() const {
1276
32306
  AssertArgument(getKind() == ::CVC4::kind::SINGLETON_OP, *this,
1277
                 "Improper kind for getConst<::CVC4::SingletonOp>()");
1278
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
1279
  // "constructed" when initially checking them against the NodeManager
1280
  // pool), we must check d_nchildren here.
1281
32306
  return d_nchildren == 0
1282
32306
    ? *reinterpret_cast< ::CVC4::SingletonOp const* >(d_children)
1283
32306
    : *reinterpret_cast< ::CVC4::SingletonOp const* >(d_children[0]);
1284
}
1285
1286
// re-enable the warning
1287
#pragma GCC diagnostic warning "-Wstrict-aliasing"
1288
1289
1290
// The reinterpret_cast of d_children to "::CVC4::EmptyBag const*"
1291
// flags a "strict aliasing" warning; it's okay, because we never access
1292
// the embedded constant as a NodeValue* child, and never access an embedded
1293
// NodeValue* child as a constant.
1294
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
1295
1296
template <>
1297
13716
::CVC4::EmptyBag const& NodeValue::getConst< ::CVC4::EmptyBag >() const {
1298
13716
  AssertArgument(getKind() == ::CVC4::kind::EMPTYBAG, *this,
1299
                 "Improper kind for getConst<::CVC4::EmptyBag>()");
1300
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
1301
  // "constructed" when initially checking them against the NodeManager
1302
  // pool), we must check d_nchildren here.
1303
13716
  return d_nchildren == 0
1304
13716
    ? *reinterpret_cast< ::CVC4::EmptyBag const* >(d_children)
1305
13716
    : *reinterpret_cast< ::CVC4::EmptyBag const* >(d_children[0]);
1306
}
1307
1308
// re-enable the warning
1309
#pragma GCC diagnostic warning "-Wstrict-aliasing"
1310
1311
1312
// The reinterpret_cast of d_children to "::CVC4::MakeBagOp const*"
1313
// flags a "strict aliasing" warning; it's okay, because we never access
1314
// the embedded constant as a NodeValue* child, and never access an embedded
1315
// NodeValue* child as a constant.
1316
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
1317
1318
template <>
1319
1480
::CVC4::MakeBagOp const& NodeValue::getConst< ::CVC4::MakeBagOp >() const {
1320
1480
  AssertArgument(getKind() == ::CVC4::kind::MK_BAG_OP, *this,
1321
                 "Improper kind for getConst<::CVC4::MakeBagOp>()");
1322
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
1323
  // "constructed" when initially checking them against the NodeManager
1324
  // pool), we must check d_nchildren here.
1325
1480
  return d_nchildren == 0
1326
1480
    ? *reinterpret_cast< ::CVC4::MakeBagOp const* >(d_children)
1327
1480
    : *reinterpret_cast< ::CVC4::MakeBagOp const* >(d_children[0]);
1328
}
1329
1330
// re-enable the warning
1331
#pragma GCC diagnostic warning "-Wstrict-aliasing"
1332
1333
1334
// The reinterpret_cast of d_children to "::CVC4::String const*"
1335
// flags a "strict aliasing" warning; it's okay, because we never access
1336
// the embedded constant as a NodeValue* child, and never access an embedded
1337
// NodeValue* child as a constant.
1338
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
1339
1340
template <>
1341
7131056
::CVC4::String const& NodeValue::getConst< ::CVC4::String >() const {
1342
7131056
  AssertArgument(getKind() == ::CVC4::kind::CONST_STRING, *this,
1343
                 "Improper kind for getConst<::CVC4::String>()");
1344
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
1345
  // "constructed" when initially checking them against the NodeManager
1346
  // pool), we must check d_nchildren here.
1347
7131056
  return d_nchildren == 0
1348
7131056
    ? *reinterpret_cast< ::CVC4::String const* >(d_children)
1349
7131056
    : *reinterpret_cast< ::CVC4::String const* >(d_children[0]);
1350
}
1351
1352
// re-enable the warning
1353
#pragma GCC diagnostic warning "-Wstrict-aliasing"
1354
1355
1356
// The reinterpret_cast of d_children to "::CVC4::Sequence const*"
1357
// flags a "strict aliasing" warning; it's okay, because we never access
1358
// the embedded constant as a NodeValue* child, and never access an embedded
1359
// NodeValue* child as a constant.
1360
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
1361
1362
template <>
1363
68403
::CVC4::Sequence const& NodeValue::getConst< ::CVC4::Sequence >() const {
1364
68403
  AssertArgument(getKind() == ::CVC4::kind::CONST_SEQUENCE, *this,
1365
                 "Improper kind for getConst<::CVC4::Sequence>()");
1366
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
1367
  // "constructed" when initially checking them against the NodeManager
1368
  // pool), we must check d_nchildren here.
1369
68403
  return d_nchildren == 0
1370
68403
    ? *reinterpret_cast< ::CVC4::Sequence const* >(d_children)
1371
68403
    : *reinterpret_cast< ::CVC4::Sequence const* >(d_children[0]);
1372
}
1373
1374
// re-enable the warning
1375
#pragma GCC diagnostic warning "-Wstrict-aliasing"
1376
1377
1378
// The reinterpret_cast of d_children to "::CVC4::RegExpRepeat const*"
1379
// flags a "strict aliasing" warning; it's okay, because we never access
1380
// the embedded constant as a NodeValue* child, and never access an embedded
1381
// NodeValue* child as a constant.
1382
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
1383
1384
template <>
1385
60
::CVC4::RegExpRepeat const& NodeValue::getConst< ::CVC4::RegExpRepeat >() const {
1386
60
  AssertArgument(getKind() == ::CVC4::kind::REGEXP_REPEAT_OP, *this,
1387
                 "Improper kind for getConst<::CVC4::RegExpRepeat>()");
1388
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
1389
  // "constructed" when initially checking them against the NodeManager
1390
  // pool), we must check d_nchildren here.
1391
60
  return d_nchildren == 0
1392
60
    ? *reinterpret_cast< ::CVC4::RegExpRepeat const* >(d_children)
1393
60
    : *reinterpret_cast< ::CVC4::RegExpRepeat const* >(d_children[0]);
1394
}
1395
1396
// re-enable the warning
1397
#pragma GCC diagnostic warning "-Wstrict-aliasing"
1398
1399
1400
// The reinterpret_cast of d_children to "::CVC4::RegExpLoop const*"
1401
// flags a "strict aliasing" warning; it's okay, because we never access
1402
// the embedded constant as a NodeValue* child, and never access an embedded
1403
// NodeValue* child as a constant.
1404
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
1405
1406
template <>
1407
281
::CVC4::RegExpLoop const& NodeValue::getConst< ::CVC4::RegExpLoop >() const {
1408
281
  AssertArgument(getKind() == ::CVC4::kind::REGEXP_LOOP_OP, *this,
1409
                 "Improper kind for getConst<::CVC4::RegExpLoop>()");
1410
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
1411
  // "constructed" when initially checking them against the NodeManager
1412
  // pool), we must check d_nchildren here.
1413
281
  return d_nchildren == 0
1414
281
    ? *reinterpret_cast< ::CVC4::RegExpLoop const* >(d_children)
1415
281
    : *reinterpret_cast< ::CVC4::RegExpLoop const* >(d_children[0]);
1416
}
1417
1418
// re-enable the warning
1419
#pragma GCC diagnostic warning "-Wstrict-aliasing"
1420
1421
1422
1423
}/* CVC4::expr namespace */
1424
1425
namespace kind {
1426
namespace metakind {
1427
1428
225141077
size_t NodeValueCompare::constHash(const ::CVC4::expr::NodeValue* nv)
1429
{
1430
225141077
  Assert(nv->getMetaKind() == kind::metakind::CONSTANT);
1431
1432
225141077
  switch (nv->d_kind)
1433
  {
1434
1435
29222
  case kind::UNINTERPRETED_CONSTANT:
1436
29222
    return ::CVC4::UninterpretedConstantHashFunction()(nv->getConst< ::CVC4::UninterpretedConstant >());
1437
1438
70
  case kind::ABSTRACT_VALUE:
1439
70
    return ::CVC4::AbstractValueHashFunction()(nv->getConst< ::CVC4::AbstractValue >());
1440
1441
9554061
  case kind::BUILTIN:
1442
9554061
    return ::CVC4::kind::KindHashFunction()(nv->getConst< ::CVC4::Kind >());
1443
1444
28687509
  case kind::TYPE_CONSTANT:
1445
28687509
    return ::CVC4::TypeConstantHashFunction()(nv->getConst< ::CVC4::TypeConstant >());
1446
1447
41898309
  case kind::CONST_BOOLEAN:
1448
41898309
    return ::CVC4::BoolHashFunction()(nv->getConst< bool >());
1449
1450
40
  case kind::DIVISIBLE_OP:
1451
40
    return ::CVC4::DivisibleHashFunction()(nv->getConst< ::CVC4::Divisible >());
1452
1453
137630902
  case kind::CONST_RATIONAL:
1454
137630902
    return ::CVC4::RationalHashFunction()(nv->getConst< ::CVC4::Rational >());
1455
1456
  case kind::INDEXED_ROOT_PREDICATE_OP:
1457
    return ::CVC4::IndexedRootPredicateHashFunction()(nv->getConst< ::CVC4::IndexedRootPredicate >());
1458
1459
365
  case kind::IAND_OP:
1460
365
    return ::CVC4::UnsignedHashFunction< ::CVC4::IntAnd >()(nv->getConst< ::CVC4::IntAnd >());
1461
1462
569035
  case kind::BITVECTOR_TYPE:
1463
569035
    return ::CVC4::UnsignedHashFunction< ::CVC4::BitVectorSize >()(nv->getConst< ::CVC4::BitVectorSize >());
1464
1465
3622353
  case kind::CONST_BITVECTOR:
1466
3622353
    return ::CVC4::BitVectorHashFunction()(nv->getConst< ::CVC4::BitVector >());
1467
1468
249485
  case kind::BITVECTOR_BITOF_OP:
1469
249485
    return ::CVC4::BitVectorBitOfHashFunction()(nv->getConst< ::CVC4::BitVectorBitOf >());
1470
1471
226951
  case kind::BITVECTOR_EXTRACT_OP:
1472
226951
    return ::CVC4::BitVectorExtractHashFunction()(nv->getConst< ::CVC4::BitVectorExtract >());
1473
1474
4164
  case kind::BITVECTOR_REPEAT_OP:
1475
4164
    return ::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRepeat >()(nv->getConst< ::CVC4::BitVectorRepeat >());
1476
1477
2285
  case kind::BITVECTOR_ROTATE_LEFT_OP:
1478
2285
    return ::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRotateLeft >()(nv->getConst< ::CVC4::BitVectorRotateLeft >());
1479
1480
2660
  case kind::BITVECTOR_ROTATE_RIGHT_OP:
1481
2660
    return ::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRotateRight >()(nv->getConst< ::CVC4::BitVectorRotateRight >());
1482
1483
33872
  case kind::BITVECTOR_SIGN_EXTEND_OP:
1484
33872
    return ::CVC4::UnsignedHashFunction< ::CVC4::BitVectorSignExtend >()(nv->getConst< ::CVC4::BitVectorSignExtend >());
1485
1486
54478
  case kind::BITVECTOR_ZERO_EXTEND_OP:
1487
54478
    return ::CVC4::UnsignedHashFunction< ::CVC4::BitVectorZeroExtend >()(nv->getConst< ::CVC4::BitVectorZeroExtend >());
1488
1489
1297
  case kind::INT_TO_BITVECTOR_OP:
1490
1297
    return ::CVC4::UnsignedHashFunction< ::CVC4::IntToBitVector >()(nv->getConst< ::CVC4::IntToBitVector >());
1491
1492
3381
  case kind::CONST_FLOATINGPOINT:
1493
3381
    return ::CVC4::FloatingPointHashFunction()(nv->getConst< ::CVC4::FloatingPoint >());
1494
1495
41317
  case kind::CONST_ROUNDINGMODE:
1496
41317
    return ::CVC4::RoundingModeHashFunction()(nv->getConst< ::CVC4::RoundingMode >());
1497
1498
31211
  case kind::FLOATINGPOINT_TYPE:
1499
31211
    return ::CVC4::FloatingPointSizeHashFunction()(nv->getConst< ::CVC4::FloatingPointSize >());
1500
1501
3430
  case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP:
1502
3430
    return ::CVC4::FloatingPointConvertSortHashFunction<0x1>()(nv->getConst< ::CVC4::FloatingPointToFPIEEEBitVector >());
1503
1504
36
  case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP:
1505
36
    return ::CVC4::FloatingPointConvertSortHashFunction<0x2>()(nv->getConst< ::CVC4::FloatingPointToFPFloatingPoint >());
1506
1507
70
  case kind::FLOATINGPOINT_TO_FP_REAL_OP:
1508
70
    return ::CVC4::FloatingPointConvertSortHashFunction<0x4>()(nv->getConst< ::CVC4::FloatingPointToFPReal >());
1509
1510
26
  case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP:
1511
26
    return ::CVC4::FloatingPointConvertSortHashFunction<0x8>()(nv->getConst< ::CVC4::FloatingPointToFPSignedBitVector >());
1512
1513
10
  case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP:
1514
10
    return ::CVC4::FloatingPointConvertSortHashFunction<0x10>()(nv->getConst< ::CVC4::FloatingPointToFPUnsignedBitVector >());
1515
1516
145
  case kind::FLOATINGPOINT_TO_FP_GENERIC_OP:
1517
145
    return ::CVC4::FloatingPointConvertSortHashFunction<0x11>()(nv->getConst< ::CVC4::FloatingPointToFPGeneric >());
1518
1519
10
  case kind::FLOATINGPOINT_TO_UBV_OP:
1520
10
    return ::CVC4::FloatingPointToBVHashFunction<0x1>()(nv->getConst< ::CVC4::FloatingPointToUBV >());
1521
1522
  case kind::FLOATINGPOINT_TO_UBV_TOTAL_OP:
1523
    return ::CVC4::FloatingPointToBVHashFunction<0x4>()(nv->getConst< ::CVC4::FloatingPointToUBVTotal >());
1524
1525
10
  case kind::FLOATINGPOINT_TO_SBV_OP:
1526
10
    return ::CVC4::FloatingPointToBVHashFunction<0x2>()(nv->getConst< ::CVC4::FloatingPointToSBV >());
1527
1528
  case kind::FLOATINGPOINT_TO_SBV_TOTAL_OP:
1529
    return ::CVC4::FloatingPointToBVHashFunction<0x8>()(nv->getConst< ::CVC4::FloatingPointToSBVTotal >());
1530
1531
9070
  case kind::STORE_ALL:
1532
9070
    return ::CVC4::ArrayStoreAllHashFunction()(nv->getConst< ::CVC4::ArrayStoreAll >());
1533
1534
30546
  case kind::DATATYPE_TYPE:
1535
30546
    return ::CVC4::DatatypeIndexConstantHashFunction()(nv->getConst< ::CVC4::DatatypeIndexConstant >());
1536
1537
856
  case kind::ASCRIPTION_TYPE:
1538
856
    return ::CVC4::AscriptionTypeHashFunction()(nv->getConst< ::CVC4::AscriptionType >());
1539
1540
15
  case kind::TUPLE_UPDATE_OP:
1541
15
    return ::CVC4::TupleUpdateHashFunction()(nv->getConst< ::CVC4::TupleUpdate >());
1542
1543
45
  case kind::RECORD_UPDATE_OP:
1544
45
    return ::CVC4::RecordUpdateHashFunction()(nv->getConst< ::CVC4::RecordUpdate >());
1545
1546
100
  case kind::TUPLE_PROJECT_OP:
1547
100
    return ::CVC4::TupleProjectOpHashFunction()(nv->getConst< ::CVC4::TupleProjectOp >());
1548
1549
9526
  case kind::EMPTYSET:
1550
9526
    return ::CVC4::EmptySetHashFunction()(nv->getConst< ::CVC4::EmptySet >());
1551
1552
14550
  case kind::SINGLETON_OP:
1553
14550
    return ::CVC4::SingletonOpHashFunction()(nv->getConst< ::CVC4::SingletonOp >());
1554
1555
6872
  case kind::EMPTYBAG:
1556
6872
    return ::CVC4::EmptyBagHashFunction()(nv->getConst< ::CVC4::EmptyBag >());
1557
1558
652
  case kind::MK_BAG_OP:
1559
652
    return ::CVC4::MakeBagOpHashFunction()(nv->getConst< ::CVC4::MakeBagOp >());
1560
1561
2400503
  case kind::CONST_STRING:
1562
2400503
    return ::CVC4::strings::StringHashFunction()(nv->getConst< ::CVC4::String >());
1563
1564
21481
  case kind::CONST_SEQUENCE:
1565
21481
    return ::CVC4::SequenceHashFunction()(nv->getConst< ::CVC4::Sequence >());
1566
1567
30
  case kind::REGEXP_REPEAT_OP:
1568
30
    return ::CVC4::RegExpRepeatHashFunction()(nv->getConst< ::CVC4::RegExpRepeat >());
1569
1570
127
  case kind::REGEXP_LOOP_OP:
1571
127
    return ::CVC4::RegExpLoopHashFunction()(nv->getConst< ::CVC4::RegExpLoop >());
1572
1573
    default: Unhandled() << ::CVC4::expr::NodeValue::dKindToKind(nv->d_kind);
1574
  }
1575
}
1576
1577
template <bool pool>
1578
672634727
bool NodeValueCompare::compare(const ::CVC4::expr::NodeValue* nv1,
1579
                               const ::CVC4::expr::NodeValue* nv2) {
1580
672634727
  if(nv1->d_kind != nv2->d_kind) {
1581
145186608
    return false;
1582
  }
1583
1584
527448119
  if (nv1->getMetaKind() == kind::metakind::CONSTANT)
1585
  {
1586
242467746
    switch (nv1->d_kind)
1587
    {
1588
1589
51791
    case kind::UNINTERPRETED_CONSTANT:
1590
51791
      return NodeValueConstCompare< kind::UNINTERPRETED_CONSTANT, pool >::compare(nv1, nv2);
1591
1592
34
    case kind::ABSTRACT_VALUE:
1593
34
      return NodeValueConstCompare< kind::ABSTRACT_VALUE, pool >::compare(nv1, nv2);
1594
1595
3814896
    case kind::BUILTIN:
1596
3814896
      return NodeValueConstCompare< kind::BUILTIN, pool >::compare(nv1, nv2);
1597
1598
28574415
    case kind::TYPE_CONSTANT:
1599
28574415
      return NodeValueConstCompare< kind::TYPE_CONSTANT, pool >::compare(nv1, nv2);
1600
1601
41857641
    case kind::CONST_BOOLEAN:
1602
41857641
      return NodeValueConstCompare< kind::CONST_BOOLEAN, pool >::compare(nv1, nv2);
1603
1604
16
    case kind::DIVISIBLE_OP:
1605
16
      return NodeValueConstCompare< kind::DIVISIBLE_OP, pool >::compare(nv1, nv2);
1606
1607
144199203
    case kind::CONST_RATIONAL:
1608
144199203
      return NodeValueConstCompare< kind::CONST_RATIONAL, pool >::compare(nv1, nv2);
1609
1610
    case kind::INDEXED_ROOT_PREDICATE_OP:
1611
      return NodeValueConstCompare< kind::INDEXED_ROOT_PREDICATE_OP, pool >::compare(nv1, nv2);
1612
1613
146
    case kind::IAND_OP:
1614
146
      return NodeValueConstCompare< kind::IAND_OP, pool >::compare(nv1, nv2);
1615
1616
544855
    case kind::BITVECTOR_TYPE:
1617
544855
      return NodeValueConstCompare< kind::BITVECTOR_TYPE, pool >::compare(nv1, nv2);
1618
1619
20522281
    case kind::CONST_BITVECTOR:
1620
20522281
      return NodeValueConstCompare< kind::CONST_BITVECTOR, pool >::compare(nv1, nv2);
1621
1622
200369
    case kind::BITVECTOR_BITOF_OP:
1623
200369
      return NodeValueConstCompare< kind::BITVECTOR_BITOF_OP, pool >::compare(nv1, nv2);
1624
1625
206626
    case kind::BITVECTOR_EXTRACT_OP:
1626
206626
      return NodeValueConstCompare< kind::BITVECTOR_EXTRACT_OP, pool >::compare(nv1, nv2);
1627
1628
3504
    case kind::BITVECTOR_REPEAT_OP:
1629
3504
      return NodeValueConstCompare< kind::BITVECTOR_REPEAT_OP, pool >::compare(nv1, nv2);
1630
1631
1769
    case kind::BITVECTOR_ROTATE_LEFT_OP:
1632
1769
      return NodeValueConstCompare< kind::BITVECTOR_ROTATE_LEFT_OP, pool >::compare(nv1, nv2);
1633
1634
2045
    case kind::BITVECTOR_ROTATE_RIGHT_OP:
1635
2045
      return NodeValueConstCompare< kind::BITVECTOR_ROTATE_RIGHT_OP, pool >::compare(nv1, nv2);
1636
1637
30083
    case kind::BITVECTOR_SIGN_EXTEND_OP:
1638
30083
      return NodeValueConstCompare< kind::BITVECTOR_SIGN_EXTEND_OP, pool >::compare(nv1, nv2);
1639
1640
50320
    case kind::BITVECTOR_ZERO_EXTEND_OP:
1641
50320
      return NodeValueConstCompare< kind::BITVECTOR_ZERO_EXTEND_OP, pool >::compare(nv1, nv2);
1642
1643
748
    case kind::INT_TO_BITVECTOR_OP:
1644
748
      return NodeValueConstCompare< kind::INT_TO_BITVECTOR_OP, pool >::compare(nv1, nv2);
1645
1646
2491
    case kind::CONST_FLOATINGPOINT:
1647
2491
      return NodeValueConstCompare< kind::CONST_FLOATINGPOINT, pool >::compare(nv1, nv2);
1648
1649
21445
    case kind::CONST_ROUNDINGMODE:
1650
21445
      return NodeValueConstCompare< kind::CONST_ROUNDINGMODE, pool >::compare(nv1, nv2);
1651
1652
15197
    case kind::FLOATINGPOINT_TYPE:
1653
15197
      return NodeValueConstCompare< kind::FLOATINGPOINT_TYPE, pool >::compare(nv1, nv2);
1654
1655
3352
    case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP:
1656
3352
      return NodeValueConstCompare< kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP, pool >::compare(nv1, nv2);
1657
1658
15
    case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP:
1659
15
      return NodeValueConstCompare< kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP, pool >::compare(nv1, nv2);
1660
1661
34
    case kind::FLOATINGPOINT_TO_FP_REAL_OP:
1662
34
      return NodeValueConstCompare< kind::FLOATINGPOINT_TO_FP_REAL_OP, pool >::compare(nv1, nv2);
1663
1664
11
    case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP:
1665
11
      return NodeValueConstCompare< kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP, pool >::compare(nv1, nv2);
1666
1667
4
    case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP:
1668
4
      return NodeValueConstCompare< kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP, pool >::compare(nv1, nv2);
1669
1670
88
    case kind::FLOATINGPOINT_TO_FP_GENERIC_OP:
1671
88
      return NodeValueConstCompare< kind::FLOATINGPOINT_TO_FP_GENERIC_OP, pool >::compare(nv1, nv2);
1672
1673
4
    case kind::FLOATINGPOINT_TO_UBV_OP:
1674
4
      return NodeValueConstCompare< kind::FLOATINGPOINT_TO_UBV_OP, pool >::compare(nv1, nv2);
1675
1676
    case kind::FLOATINGPOINT_TO_UBV_TOTAL_OP:
1677
      return NodeValueConstCompare< kind::FLOATINGPOINT_TO_UBV_TOTAL_OP, pool >::compare(nv1, nv2);
1678
1679
4
    case kind::FLOATINGPOINT_TO_SBV_OP:
1680
4
      return NodeValueConstCompare< kind::FLOATINGPOINT_TO_SBV_OP, pool >::compare(nv1, nv2);
1681
1682
    case kind::FLOATINGPOINT_TO_SBV_TOTAL_OP:
1683
      return NodeValueConstCompare< kind::FLOATINGPOINT_TO_SBV_TOTAL_OP, pool >::compare(nv1, nv2);
1684
1685
7213
    case kind::STORE_ALL:
1686
7213
      return NodeValueConstCompare< kind::STORE_ALL, pool >::compare(nv1, nv2);
1687
1688
13790
    case kind::DATATYPE_TYPE:
1689
13790
      return NodeValueConstCompare< kind::DATATYPE_TYPE, pool >::compare(nv1, nv2);
1690
1691
562
    case kind::ASCRIPTION_TYPE:
1692
562
      return NodeValueConstCompare< kind::ASCRIPTION_TYPE, pool >::compare(nv1, nv2);
1693
1694
6
    case kind::TUPLE_UPDATE_OP:
1695
6
      return NodeValueConstCompare< kind::TUPLE_UPDATE_OP, pool >::compare(nv1, nv2);
1696
1697
18
    case kind::RECORD_UPDATE_OP:
1698
18
      return NodeValueConstCompare< kind::RECORD_UPDATE_OP, pool >::compare(nv1, nv2);
1699
1700
56
    case kind::TUPLE_PROJECT_OP:
1701
56
      return NodeValueConstCompare< kind::TUPLE_PROJECT_OP, pool >::compare(nv1, nv2);
1702
1703
4390
    case kind::EMPTYSET:
1704
4390
      return NodeValueConstCompare< kind::EMPTYSET, pool >::compare(nv1, nv2);
1705
1706
12816
    case kind::SINGLETON_OP:
1707
12816
      return NodeValueConstCompare< kind::SINGLETON_OP, pool >::compare(nv1, nv2);
1708
1709
2798
    case kind::EMPTYBAG:
1710
2798
      return NodeValueConstCompare< kind::EMPTYBAG, pool >::compare(nv1, nv2);
1711
1712
409
    case kind::MK_BAG_OP:
1713
409
      return NodeValueConstCompare< kind::MK_BAG_OP, pool >::compare(nv1, nv2);
1714
1715
2301371
    case kind::CONST_STRING:
1716
2301371
      return NodeValueConstCompare< kind::CONST_STRING, pool >::compare(nv1, nv2);
1717
1718
20866
    case kind::CONST_SEQUENCE:
1719
20866
      return NodeValueConstCompare< kind::CONST_SEQUENCE, pool >::compare(nv1, nv2);
1720
1721
12
    case kind::REGEXP_REPEAT_OP:
1722
12
      return NodeValueConstCompare< kind::REGEXP_REPEAT_OP, pool >::compare(nv1, nv2);
1723
1724
52
    case kind::REGEXP_LOOP_OP:
1725
52
      return NodeValueConstCompare< kind::REGEXP_LOOP_OP, pool >::compare(nv1, nv2);
1726
1727
      default: Unhandled() << ::CVC4::expr::NodeValue::dKindToKind(nv1->d_kind);
1728
    }
1729
  }
1730
1731
284980373
  if(nv1->d_nchildren != nv2->d_nchildren) {
1732
    return false;
1733
  }
1734
1735
284980373
  ::CVC4::expr::NodeValue::const_nv_iterator i = nv1->nv_begin();
1736
284980373
  ::CVC4::expr::NodeValue::const_nv_iterator j = nv2->nv_begin();
1737
284980373
  ::CVC4::expr::NodeValue::const_nv_iterator i_end = nv1->nv_end();
1738
1739
1491370507
  while(i != i_end) {
1740
605370435
    if((*i) != (*j)) {
1741
2175368
      return false;
1742
    }
1743
603195067
    ++i;
1744
603195067
    ++j;
1745
  }
1746
1747
282805005
  return true;
1748
}
1749
1750
template bool NodeValueCompare::compare<true>(const ::CVC4::expr::NodeValue* nv1,
1751
                                              const ::CVC4::expr::NodeValue* nv2);
1752
template bool NodeValueCompare::compare<false>(const ::CVC4::expr::NodeValue* nv1,
1753
                                               const ::CVC4::expr::NodeValue* nv2);
1754
1755
8
void NodeValueConstPrinter::toStream(std::ostream& out,
1756
                                            const ::CVC4::expr::NodeValue* nv) {
1757
8
  Assert(nv->getMetaKind() == kind::metakind::CONSTANT);
1758
1759
8
  switch (nv->d_kind)
1760
  {
1761
1762
  case kind::UNINTERPRETED_CONSTANT:
1763
    out << nv->getConst< ::CVC4::UninterpretedConstant >();
1764
    break;
1765
1766
8
  case kind::ABSTRACT_VALUE:
1767
8
    out << nv->getConst< ::CVC4::AbstractValue >();
1768
8
    break;
1769
1770
  case kind::BUILTIN:
1771
    out << nv->getConst< ::CVC4::Kind >();
1772
    break;
1773
1774
  case kind::TYPE_CONSTANT:
1775
    out << nv->getConst< ::CVC4::TypeConstant >();
1776
    break;
1777
1778
  case kind::CONST_BOOLEAN:
1779
    out << nv->getConst< bool >();
1780
    break;
1781
1782
  case kind::DIVISIBLE_OP:
1783
    out << nv->getConst< ::CVC4::Divisible >();
1784
    break;
1785
1786
  case kind::CONST_RATIONAL:
1787
    out << nv->getConst< ::CVC4::Rational >();
1788
    break;
1789
1790
  case kind::INDEXED_ROOT_PREDICATE_OP:
1791
    out << nv->getConst< ::CVC4::IndexedRootPredicate >();
1792
    break;
1793
1794
  case kind::IAND_OP:
1795
    out << nv->getConst< ::CVC4::IntAnd >();
1796
    break;
1797
1798
  case kind::BITVECTOR_TYPE:
1799
    out << nv->getConst< ::CVC4::BitVectorSize >();
1800
    break;
1801
1802
  case kind::CONST_BITVECTOR:
1803
    out << nv->getConst< ::CVC4::BitVector >();
1804
    break;
1805
1806
  case kind::BITVECTOR_BITOF_OP:
1807
    out << nv->getConst< ::CVC4::BitVectorBitOf >();
1808
    break;
1809
1810
  case kind::BITVECTOR_EXTRACT_OP:
1811
    out << nv->getConst< ::CVC4::BitVectorExtract >();
1812
    break;
1813
1814
  case kind::BITVECTOR_REPEAT_OP:
1815
    out << nv->getConst< ::CVC4::BitVectorRepeat >();
1816
    break;
1817
1818
  case kind::BITVECTOR_ROTATE_LEFT_OP:
1819
    out << nv->getConst< ::CVC4::BitVectorRotateLeft >();
1820
    break;
1821
1822
  case kind::BITVECTOR_ROTATE_RIGHT_OP:
1823
    out << nv->getConst< ::CVC4::BitVectorRotateRight >();
1824
    break;
1825
1826
  case kind::BITVECTOR_SIGN_EXTEND_OP:
1827
    out << nv->getConst< ::CVC4::BitVectorSignExtend >();
1828
    break;
1829
1830
  case kind::BITVECTOR_ZERO_EXTEND_OP:
1831
    out << nv->getConst< ::CVC4::BitVectorZeroExtend >();
1832
    break;
1833
1834
  case kind::INT_TO_BITVECTOR_OP:
1835
    out << nv->getConst< ::CVC4::IntToBitVector >();
1836
    break;
1837
1838
  case kind::CONST_FLOATINGPOINT:
1839
    out << nv->getConst< ::CVC4::FloatingPoint >();
1840
    break;
1841
1842
  case kind::CONST_ROUNDINGMODE:
1843
    out << nv->getConst< ::CVC4::RoundingMode >();
1844
    break;
1845
1846
  case kind::FLOATINGPOINT_TYPE:
1847
    out << nv->getConst< ::CVC4::FloatingPointSize >();
1848
    break;
1849
1850
  case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP:
1851
    out << nv->getConst< ::CVC4::FloatingPointToFPIEEEBitVector >();
1852
    break;
1853
1854
  case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP:
1855
    out << nv->getConst< ::CVC4::FloatingPointToFPFloatingPoint >();
1856
    break;
1857
1858
  case kind::FLOATINGPOINT_TO_FP_REAL_OP:
1859
    out << nv->getConst< ::CVC4::FloatingPointToFPReal >();
1860
    break;
1861
1862
  case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP:
1863
    out << nv->getConst< ::CVC4::FloatingPointToFPSignedBitVector >();
1864
    break;
1865
1866
  case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP:
1867
    out << nv->getConst< ::CVC4::FloatingPointToFPUnsignedBitVector >();
1868
    break;
1869
1870
  case kind::FLOATINGPOINT_TO_FP_GENERIC_OP:
1871
    out << nv->getConst< ::CVC4::FloatingPointToFPGeneric >();
1872
    break;
1873
1874
  case kind::FLOATINGPOINT_TO_UBV_OP:
1875
    out << nv->getConst< ::CVC4::FloatingPointToUBV >();
1876
    break;
1877
1878
  case kind::FLOATINGPOINT_TO_UBV_TOTAL_OP:
1879
    out << nv->getConst< ::CVC4::FloatingPointToUBVTotal >();
1880
    break;
1881
1882
  case kind::FLOATINGPOINT_TO_SBV_OP:
1883
    out << nv->getConst< ::CVC4::FloatingPointToSBV >();
1884
    break;
1885
1886
  case kind::FLOATINGPOINT_TO_SBV_TOTAL_OP:
1887
    out << nv->getConst< ::CVC4::FloatingPointToSBVTotal >();
1888
    break;
1889
1890
  case kind::STORE_ALL:
1891
    out << nv->getConst< ::CVC4::ArrayStoreAll >();
1892
    break;
1893
1894
  case kind::DATATYPE_TYPE:
1895
    out << nv->getConst< ::CVC4::DatatypeIndexConstant >();
1896
    break;
1897
1898
  case kind::ASCRIPTION_TYPE:
1899
    out << nv->getConst< ::CVC4::AscriptionType >();
1900
    break;
1901
1902
  case kind::TUPLE_UPDATE_OP:
1903
    out << nv->getConst< ::CVC4::TupleUpdate >();
1904
    break;
1905
1906
  case kind::RECORD_UPDATE_OP:
1907
    out << nv->getConst< ::CVC4::RecordUpdate >();
1908
    break;
1909
1910
  case kind::TUPLE_PROJECT_OP:
1911
    out << nv->getConst< ::CVC4::TupleProjectOp >();
1912
    break;
1913
1914
  case kind::EMPTYSET:
1915
    out << nv->getConst< ::CVC4::EmptySet >();
1916
    break;
1917
1918
  case kind::SINGLETON_OP:
1919
    out << nv->getConst< ::CVC4::SingletonOp >();
1920
    break;
1921
1922
  case kind::EMPTYBAG:
1923
    out << nv->getConst< ::CVC4::EmptyBag >();
1924
    break;
1925
1926
  case kind::MK_BAG_OP:
1927
    out << nv->getConst< ::CVC4::MakeBagOp >();
1928
    break;
1929
1930
  case kind::CONST_STRING:
1931
    out << nv->getConst< ::CVC4::String >();
1932
    break;
1933
1934
  case kind::CONST_SEQUENCE:
1935
    out << nv->getConst< ::CVC4::Sequence >();
1936
    break;
1937
1938
  case kind::REGEXP_REPEAT_OP:
1939
    out << nv->getConst< ::CVC4::RegExpRepeat >();
1940
    break;
1941
1942
  case kind::REGEXP_LOOP_OP:
1943
    out << nv->getConst< ::CVC4::RegExpLoop >();
1944
    break;
1945
1946
    default: Unhandled() << ::CVC4::expr::NodeValue::dKindToKind(nv->d_kind);
1947
  }
1948
8
}
1949
1950
8
void NodeValueConstPrinter::toStream(std::ostream& out, TNode n) {
1951
8
  toStream(out, n.d_nv);
1952
8
}
1953
1954
// The reinterpret_cast of d_children to various constant payload types
1955
// in deleteNodeValueConstant(), below, can flag a "strict aliasing"
1956
// warning; it should actually be okay, because we never access the
1957
// embedded constant as a NodeValue* child, and never access an embedded
1958
// NodeValue* child as a constant.
1959
#pragma GCC diagnostic ignored "-Wstrict-aliasing"
1960
1961
/**
1962
 * Cleanup to be performed when a NodeValue zombie is collected, and
1963
 * it has CONSTANT metakind.  This calls the destructor for the underlying
1964
 * C++ type representing the constant value.  See
1965
 * NodeManager::reclaimZombies() for more information.
1966
 *
1967
 * This doesn't support "non-inlined" NodeValues, which shouldn't need this
1968
 * kind of cleanup.
1969
 */
1970
2433772
void deleteNodeValueConstant(::CVC4::expr::NodeValue* nv) {
1971
2433772
  Assert(nv->getMetaKind() == kind::metakind::CONSTANT);
1972
1973
2433772
  switch (nv->d_kind)
1974
  {
1975
1976
1959
  case kind::UNINTERPRETED_CONSTANT:
1977
1959
    std::allocator< ::CVC4::UninterpretedConstant >().destroy(reinterpret_cast< ::CVC4::UninterpretedConstant* >(nv->d_children));
1978
1959
    break;
1979
1980
12
  case kind::ABSTRACT_VALUE:
1981
12
    std::allocator< ::CVC4::AbstractValue >().destroy(reinterpret_cast< ::CVC4::AbstractValue* >(nv->d_children));
1982
12
    break;
1983
1984
1907448
  case kind::BUILTIN:
1985
1907448
    std::allocator< ::CVC4::Kind >().destroy(reinterpret_cast< ::CVC4::Kind* >(nv->d_children));
1986
1907448
    break;
1987
1988
37621
  case kind::TYPE_CONSTANT:
1989
37621
    std::allocator< ::CVC4::TypeConstant >().destroy(reinterpret_cast< ::CVC4::TypeConstant* >(nv->d_children));
1990
37621
    break;
1991
1992
13517
  case kind::CONST_BOOLEAN:
1993
13517
    std::allocator< bool >().destroy(reinterpret_cast< bool* >(nv->d_children));
1994
13517
    break;
1995
1996
8
  case kind::DIVISIBLE_OP:
1997
8
    std::allocator< ::CVC4::Divisible >().destroy(reinterpret_cast< ::CVC4::Divisible* >(nv->d_children));
1998
8
    break;
1999
2000
297519
  case kind::CONST_RATIONAL:
2001
297519
    std::allocator< ::CVC4::Rational >().destroy(reinterpret_cast< ::CVC4::Rational* >(nv->d_children));
2002
297519
    break;
2003
2004
  case kind::INDEXED_ROOT_PREDICATE_OP:
2005
    std::allocator< ::CVC4::IndexedRootPredicate >().destroy(reinterpret_cast< ::CVC4::IndexedRootPredicate* >(nv->d_children));
2006
    break;
2007
2008
73
  case kind::IAND_OP:
2009
73
    std::allocator< ::CVC4::IntAnd >().destroy(reinterpret_cast< ::CVC4::IntAnd* >(nv->d_children));
2010
73
    break;
2011
2012
8054
  case kind::BITVECTOR_TYPE:
2013
8054
    std::allocator< ::CVC4::BitVectorSize >().destroy(reinterpret_cast< ::CVC4::BitVectorSize* >(nv->d_children));
2014
8054
    break;
2015
2016
83446
  case kind::CONST_BITVECTOR:
2017
83446
    std::allocator< ::CVC4::BitVector >().destroy(reinterpret_cast< ::CVC4::BitVector* >(nv->d_children));
2018
83446
    break;
2019
2020
16364
  case kind::BITVECTOR_BITOF_OP:
2021
16364
    std::allocator< ::CVC4::BitVectorBitOf >().destroy(reinterpret_cast< ::CVC4::BitVectorBitOf* >(nv->d_children));
2022
16364
    break;
2023
2024
6789
  case kind::BITVECTOR_EXTRACT_OP:
2025
6789
    std::allocator< ::CVC4::BitVectorExtract >().destroy(reinterpret_cast< ::CVC4::BitVectorExtract* >(nv->d_children));
2026
6789
    break;
2027
2028
219
  case kind::BITVECTOR_REPEAT_OP:
2029
219
    std::allocator< ::CVC4::BitVectorRepeat >().destroy(reinterpret_cast< ::CVC4::BitVectorRepeat* >(nv->d_children));
2030
219
    break;
2031
2032
172
  case kind::BITVECTOR_ROTATE_LEFT_OP:
2033
172
    std::allocator< ::CVC4::BitVectorRotateLeft >().destroy(reinterpret_cast< ::CVC4::BitVectorRotateLeft* >(nv->d_children));
2034
172
    break;
2035
2036
205
  case kind::BITVECTOR_ROTATE_RIGHT_OP:
2037
205
    std::allocator< ::CVC4::BitVectorRotateRight >().destroy(reinterpret_cast< ::CVC4::BitVectorRotateRight* >(nv->d_children));
2038
205
    break;
2039
2040
1263
  case kind::BITVECTOR_SIGN_EXTEND_OP:
2041
1263
    std::allocator< ::CVC4::BitVectorSignExtend >().destroy(reinterpret_cast< ::CVC4::BitVectorSignExtend* >(nv->d_children));
2042
1263
    break;
2043
2044
1386
  case kind::BITVECTOR_ZERO_EXTEND_OP:
2045
1386
    std::allocator< ::CVC4::BitVectorZeroExtend >().destroy(reinterpret_cast< ::CVC4::BitVectorZeroExtend* >(nv->d_children));
2046
1386
    break;
2047
2048
182
  case kind::INT_TO_BITVECTOR_OP:
2049
182
    std::allocator< ::CVC4::IntToBitVector >().destroy(reinterpret_cast< ::CVC4::IntToBitVector* >(nv->d_children));
2050
182
    break;
2051
2052
327
  case kind::CONST_FLOATINGPOINT:
2053
327
    std::allocator< ::CVC4::FloatingPoint >().destroy(reinterpret_cast< ::CVC4::FloatingPoint* >(nv->d_children));
2054
327
    break;
2055
2056
6594
  case kind::CONST_ROUNDINGMODE:
2057
6594
    std::allocator< ::CVC4::RoundingMode >().destroy(reinterpret_cast< ::CVC4::RoundingMode* >(nv->d_children));
2058
6594
    break;
2059
2060
5314
  case kind::FLOATINGPOINT_TYPE:
2061
5314
    std::allocator< ::CVC4::FloatingPointSize >().destroy(reinterpret_cast< ::CVC4::FloatingPointSize* >(nv->d_children));
2062
5314
    break;
2063
2064
26
  case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP:
2065
26
    std::allocator< ::CVC4::FloatingPointToFPIEEEBitVector >().destroy(reinterpret_cast< ::CVC4::FloatingPointToFPIEEEBitVector* >(nv->d_children));
2066
26
    break;
2067
2068
7
  case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP:
2069
7
    std::allocator< ::CVC4::FloatingPointToFPFloatingPoint >().destroy(reinterpret_cast< ::CVC4::FloatingPointToFPFloatingPoint* >(nv->d_children));
2070
7
    break;
2071
2072
12
  case kind::FLOATINGPOINT_TO_FP_REAL_OP:
2073
12
    std::allocator< ::CVC4::FloatingPointToFPReal >().destroy(reinterpret_cast< ::CVC4::FloatingPointToFPReal* >(nv->d_children));
2074
12
    break;
2075
2076
5
  case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP:
2077
5
    std::allocator< ::CVC4::FloatingPointToFPSignedBitVector >().destroy(reinterpret_cast< ::CVC4::FloatingPointToFPSignedBitVector* >(nv->d_children));
2078
5
    break;
2079
2080
2
  case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP:
2081
2
    std::allocator< ::CVC4::FloatingPointToFPUnsignedBitVector >().destroy(reinterpret_cast< ::CVC4::FloatingPointToFPUnsignedBitVector* >(nv->d_children));
2082
2
    break;
2083
2084
19
  case kind::FLOATINGPOINT_TO_FP_GENERIC_OP:
2085
19
    std::allocator< ::CVC4::FloatingPointToFPGeneric >().destroy(reinterpret_cast< ::CVC4::FloatingPointToFPGeneric* >(nv->d_children));
2086
19
    break;
2087
2088
2
  case kind::FLOATINGPOINT_TO_UBV_OP:
2089
2
    std::allocator< ::CVC4::FloatingPointToUBV >().destroy(reinterpret_cast< ::CVC4::FloatingPointToUBV* >(nv->d_children));
2090
2
    break;
2091
2092
  case kind::FLOATINGPOINT_TO_UBV_TOTAL_OP:
2093
    std::allocator< ::CVC4::FloatingPointToUBVTotal >().destroy(reinterpret_cast< ::CVC4::FloatingPointToUBVTotal* >(nv->d_children));
2094
    break;
2095
2096
2
  case kind::FLOATINGPOINT_TO_SBV_OP:
2097
2
    std::allocator< ::CVC4::FloatingPointToSBV >().destroy(reinterpret_cast< ::CVC4::FloatingPointToSBV* >(nv->d_children));
2098
2
    break;
2099
2100
  case kind::FLOATINGPOINT_TO_SBV_TOTAL_OP:
2101
    std::allocator< ::CVC4::FloatingPointToSBVTotal >().destroy(reinterpret_cast< ::CVC4::FloatingPointToSBVTotal* >(nv->d_children));
2102
    break;
2103
2104
619
  case kind::STORE_ALL:
2105
619
    std::allocator< ::CVC4::ArrayStoreAll >().destroy(reinterpret_cast< ::CVC4::ArrayStoreAll* >(nv->d_children));
2106
619
    break;
2107
2108
5779
  case kind::DATATYPE_TYPE:
2109
5779
    std::allocator< ::CVC4::DatatypeIndexConstant >().destroy(reinterpret_cast< ::CVC4::DatatypeIndexConstant* >(nv->d_children));
2110
5779
    break;
2111
2112
98
  case kind::ASCRIPTION_TYPE:
2113
98
    std::allocator< ::CVC4::AscriptionType >().destroy(reinterpret_cast< ::CVC4::AscriptionType* >(nv->d_children));
2114
98
    break;
2115
2116
3
  case kind::TUPLE_UPDATE_OP:
2117
3
    std::allocator< ::CVC4::TupleUpdate >().destroy(reinterpret_cast< ::CVC4::TupleUpdate* >(nv->d_children));
2118
3
    break;
2119
2120
9
  case kind::RECORD_UPDATE_OP:
2121
9
    std::allocator< ::CVC4::RecordUpdate >().destroy(reinterpret_cast< ::CVC4::RecordUpdate* >(nv->d_children));
2122
9
    break;
2123
2124
20
  case kind::TUPLE_PROJECT_OP:
2125
20
    std::allocator< ::CVC4::TupleProjectOp >().destroy(reinterpret_cast< ::CVC4::TupleProjectOp* >(nv->d_children));
2126
20
    break;
2127
2128
1706
  case kind::EMPTYSET:
2129
1706
    std::allocator< ::CVC4::EmptySet >().destroy(reinterpret_cast< ::CVC4::EmptySet* >(nv->d_children));
2130
1706
    break;
2131
2132
578
  case kind::SINGLETON_OP:
2133
578
    std::allocator< ::CVC4::SingletonOp >().destroy(reinterpret_cast< ::CVC4::SingletonOp* >(nv->d_children));
2134
578
    break;
2135
2136
1352
  case kind::EMPTYBAG:
2137
1352
    std::allocator< ::CVC4::EmptyBag >().destroy(reinterpret_cast< ::CVC4::EmptyBag* >(nv->d_children));
2138
1352
    break;
2139
2140
81
  case kind::MK_BAG_OP:
2141
81
    std::allocator< ::CVC4::MakeBagOp >().destroy(reinterpret_cast< ::CVC4::MakeBagOp* >(nv->d_children));
2142
81
    break;
2143
2144
33029
  case kind::CONST_STRING:
2145
33029
    std::allocator< ::CVC4::String >().destroy(reinterpret_cast< ::CVC4::String* >(nv->d_children));
2146
33029
    break;
2147
2148
1920
  case kind::CONST_SEQUENCE:
2149
1920
    std::allocator< ::CVC4::Sequence >().destroy(reinterpret_cast< ::CVC4::Sequence* >(nv->d_children));
2150
1920
    break;
2151
2152
6
  case kind::REGEXP_REPEAT_OP:
2153
6
    std::allocator< ::CVC4::RegExpRepeat >().destroy(reinterpret_cast< ::CVC4::RegExpRepeat* >(nv->d_children));
2154
6
    break;
2155
2156
25
  case kind::REGEXP_LOOP_OP:
2157
25
    std::allocator< ::CVC4::RegExpLoop >().destroy(reinterpret_cast< ::CVC4::RegExpLoop* >(nv->d_children));
2158
25
    break;
2159
2160
    default: Unhandled() << ::CVC4::expr::NodeValue::dKindToKind(nv->d_kind);
2161
  }
2162
2433772
}
2163
2164
// re-enable the strict-aliasing warning
2165
# pragma GCC diagnostic warning "-Wstrict-aliasing"
2166
2167
259076015
uint32_t getMinArityForKind(::CVC4::Kind k)
2168
{
2169
  static const unsigned lbs[] = {
2170
    0, /* NULL_EXPR */
2171
2172
    0, /* SORT_TAG */
2173
    0, /* SORT_TYPE */
2174
    0, /* UNINTERPRETED_CONSTANT */
2175
    0, /* ABSTRACT_VALUE */
2176
    0, /* BUILTIN */
2177
    2, /* EQUAL */
2178
    2, /* DISTINCT */
2179
    0, /* VARIABLE */
2180
    0, /* BOUND_VARIABLE */
2181
    0, /* SKOLEM */
2182
    0, /* SEXPR */
2183
    2, /* LAMBDA */
2184
    2, /* WITNESS */
2185
    0, /* TYPE_CONSTANT */
2186
    2, /* FUNCTION_TYPE */
2187
    0, /* SEXPR_TYPE */
2188
    0, /* CONST_BOOLEAN */
2189
    1, /* NOT */
2190
    2, /* AND */
2191
    2, /* IMPLIES */
2192
    2, /* OR */
2193
    2, /* XOR */
2194
    3, /* ITE */
2195
    1, /* APPLY_UF */
2196
    0, /* BOOLEAN_TERM_VARIABLE */
2197
    2, /* CARDINALITY_CONSTRAINT */
2198
    1, /* COMBINED_CARDINALITY_CONSTRAINT */
2199
    1, /* PARTIAL_APPLY_UF */
2200
    1, /* CARDINALITY_VALUE */
2201
    2, /* HO_APPLY */
2202
    2, /* PLUS */
2203
    2, /* MULT */
2204
    2, /* NONLINEAR_MULT */
2205
    2, /* MINUS */
2206
    1, /* UMINUS */
2207
    2, /* DIVISION */
2208
    2, /* DIVISION_TOTAL */
2209
    2, /* INTS_DIVISION */
2210
    2, /* INTS_DIVISION_TOTAL */
2211
    2, /* INTS_MODULUS */
2212
    2, /* INTS_MODULUS_TOTAL */
2213
    1, /* ABS */
2214
    1, /* DIVISIBLE */
2215
    2, /* POW */
2216
    1, /* EXPONENTIAL */
2217
    1, /* SINE */
2218
    1, /* COSINE */
2219
    1, /* TANGENT */
2220
    1, /* COSECANT */
2221
    1, /* SECANT */
2222
    1, /* COTANGENT */
2223
    1, /* ARCSINE */
2224
    1, /* ARCCOSINE */
2225
    1, /* ARCTANGENT */
2226
    1, /* ARCCOSECANT */
2227
    1, /* ARCSECANT */
2228
    1, /* ARCCOTANGENT */
2229
    1, /* SQRT */
2230
    0, /* DIVISIBLE_OP */
2231
    0, /* CONST_RATIONAL */
2232
    2, /* LT */
2233
    2, /* LEQ */
2234
    2, /* GT */
2235
    2, /* GEQ */
2236
    0, /* INDEXED_ROOT_PREDICATE_OP */
2237
    2, /* INDEXED_ROOT_PREDICATE */
2238
    1, /* IS_INTEGER */
2239
    1, /* TO_INTEGER */
2240
    1, /* TO_REAL */
2241
    1, /* CAST_TO_REAL */
2242
    0, /* PI */
2243
    0, /* IAND_OP */
2244
    2, /* IAND */
2245
    0, /* BITVECTOR_TYPE */
2246
    0, /* CONST_BITVECTOR */
2247
    2, /* BITVECTOR_CONCAT */
2248
    2, /* BITVECTOR_AND */
2249
    2, /* BITVECTOR_COMP */
2250
    2, /* BITVECTOR_OR */
2251
    2, /* BITVECTOR_XOR */
2252
    1, /* BITVECTOR_NOT */
2253
    2, /* BITVECTOR_NAND */
2254
    2, /* BITVECTOR_NOR */
2255
    2, /* BITVECTOR_XNOR */
2256
    2, /* BITVECTOR_MULT */
2257
    1, /* BITVECTOR_NEG */
2258
    2, /* BITVECTOR_PLUS */
2259
    2, /* BITVECTOR_SUB */
2260
    2, /* BITVECTOR_UDIV */
2261
    2, /* BITVECTOR_UREM */
2262
    2, /* BITVECTOR_SDIV */
2263
    2, /* BITVECTOR_SMOD */
2264
    2, /* BITVECTOR_SREM */
2265
    2, /* BITVECTOR_ASHR */
2266
    2, /* BITVECTOR_LSHR */
2267
    2, /* BITVECTOR_SHL */
2268
    2, /* BITVECTOR_ULE */
2269
    2, /* BITVECTOR_ULT */
2270
    2, /* BITVECTOR_UGE */
2271
    2, /* BITVECTOR_UGT */
2272
    2, /* BITVECTOR_SLE */
2273
    2, /* BITVECTOR_SLT */
2274
    2, /* BITVECTOR_SGE */
2275
    2, /* BITVECTOR_SGT */
2276
    2, /* BITVECTOR_ULTBV */
2277
    2, /* BITVECTOR_SLTBV */
2278
    1, /* BITVECTOR_REDAND */
2279
    1, /* BITVECTOR_REDOR */
2280
    3, /* BITVECTOR_ITE */
2281
    1, /* BITVECTOR_TO_NAT */
2282
    1, /* BITVECTOR_ACKERMANNIZE_UDIV */
2283
    1, /* BITVECTOR_ACKERMANNIZE_UREM */
2284
    1, /* BITVECTOR_EAGER_ATOM */
2285
    0, /* BITVECTOR_BITOF_OP */
2286
    1, /* BITVECTOR_BITOF */
2287
    0, /* BITVECTOR_EXTRACT_OP */
2288
    1, /* BITVECTOR_EXTRACT */
2289
    0, /* BITVECTOR_REPEAT_OP */
2290
    1, /* BITVECTOR_REPEAT */
2291
    0, /* BITVECTOR_ROTATE_LEFT_OP */
2292
    1, /* BITVECTOR_ROTATE_LEFT */
2293
    0, /* BITVECTOR_ROTATE_RIGHT_OP */
2294
    1, /* BITVECTOR_ROTATE_RIGHT */
2295
    0, /* BITVECTOR_SIGN_EXTEND_OP */
2296
    1, /* BITVECTOR_SIGN_EXTEND */
2297
    0, /* BITVECTOR_ZERO_EXTEND_OP */
2298
    1, /* BITVECTOR_ZERO_EXTEND */
2299
    0, /* INT_TO_BITVECTOR_OP */
2300
    1, /* INT_TO_BITVECTOR */
2301
    0, /* CONST_FLOATINGPOINT */
2302
    0, /* CONST_ROUNDINGMODE */
2303
    0, /* FLOATINGPOINT_TYPE */
2304
    3, /* FLOATINGPOINT_FP */
2305
    2, /* FLOATINGPOINT_EQ */
2306
    1, /* FLOATINGPOINT_ABS */
2307
    1, /* FLOATINGPOINT_NEG */
2308
    3, /* FLOATINGPOINT_PLUS */
2309
    3, /* FLOATINGPOINT_SUB */
2310
    3, /* FLOATINGPOINT_MULT */
2311
    3, /* FLOATINGPOINT_DIV */
2312
    4, /* FLOATINGPOINT_FMA */
2313
    2, /* FLOATINGPOINT_SQRT */
2314
    2, /* FLOATINGPOINT_REM */
2315
    2, /* FLOATINGPOINT_RTI */
2316
    2, /* FLOATINGPOINT_MIN */
2317
    2, /* FLOATINGPOINT_MAX */
2318
    3, /* FLOATINGPOINT_MIN_TOTAL */
2319
    3, /* FLOATINGPOINT_MAX_TOTAL */
2320
    2, /* FLOATINGPOINT_LEQ */
2321
    2, /* FLOATINGPOINT_LT */
2322
    2, /* FLOATINGPOINT_GEQ */
2323
    2, /* FLOATINGPOINT_GT */
2324
    1, /* FLOATINGPOINT_ISN */
2325
    1, /* FLOATINGPOINT_ISSN */
2326
    1, /* FLOATINGPOINT_ISZ */
2327
    1, /* FLOATINGPOINT_ISINF */
2328
    1, /* FLOATINGPOINT_ISNAN */
2329
    1, /* FLOATINGPOINT_ISNEG */
2330
    1, /* FLOATINGPOINT_ISPOS */
2331
    0, /* FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP */
2332
    1, /* FLOATINGPOINT_TO_FP_IEEE_BITVECTOR */
2333
    0, /* FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP */
2334
    2, /* FLOATINGPOINT_TO_FP_FLOATINGPOINT */
2335
    0, /* FLOATINGPOINT_TO_FP_REAL_OP */
2336
    2, /* FLOATINGPOINT_TO_FP_REAL */
2337
    0, /* FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP */
2338
    2, /* FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR */
2339
    0, /* FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP */
2340
    2, /* FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR */
2341
    0, /* FLOATINGPOINT_TO_FP_GENERIC_OP */
2342
    1, /* FLOATINGPOINT_TO_FP_GENERIC */
2343
    0, /* FLOATINGPOINT_TO_UBV_OP */
2344
    2, /* FLOATINGPOINT_TO_UBV */
2345
    0, /* FLOATINGPOINT_TO_UBV_TOTAL_OP */
2346
    3, /* FLOATINGPOINT_TO_UBV_TOTAL */
2347
    0, /* FLOATINGPOINT_TO_SBV_OP */
2348
    2, /* FLOATINGPOINT_TO_SBV */
2349
    0, /* FLOATINGPOINT_TO_SBV_TOTAL_OP */
2350
    3, /* FLOATINGPOINT_TO_SBV_TOTAL */
2351
    1, /* FLOATINGPOINT_TO_REAL */
2352
    2, /* FLOATINGPOINT_TO_REAL_TOTAL */
2353
    1, /* FLOATINGPOINT_COMPONENT_NAN */
2354
    1, /* FLOATINGPOINT_COMPONENT_INF */
2355
    1, /* FLOATINGPOINT_COMPONENT_ZERO */
2356
    1, /* FLOATINGPOINT_COMPONENT_SIGN */
2357
    1, /* FLOATINGPOINT_COMPONENT_EXPONENT */
2358
    1, /* FLOATINGPOINT_COMPONENT_SIGNIFICAND */
2359
    1, /* ROUNDINGMODE_BITBLAST */
2360
    2, /* ARRAY_TYPE */
2361
    2, /* SELECT */
2362
    3, /* STORE */
2363
    4, /* EQ_RANGE */
2364
    0, /* STORE_ALL */
2365
    4, /* ARR_TABLE_FUN */
2366
    1, /* ARRAY_LAMBDA */
2367
    0, /* PARTIAL_SELECT_0 */
2368
    0, /* PARTIAL_SELECT_1 */
2369
    1, /* CONSTRUCTOR_TYPE */
2370
    2, /* SELECTOR_TYPE */
2371
    1, /* TESTER_TYPE */
2372
    0, /* APPLY_CONSTRUCTOR */
2373
    1, /* APPLY_SELECTOR */
2374
    1, /* APPLY_SELECTOR_TOTAL */
2375
    1, /* APPLY_TESTER */
2376
    0, /* DATATYPE_TYPE */
2377
    1, /* PARAMETRIC_DATATYPE */
2378
    1, /* APPLY_TYPE_ASCRIPTION */
2379
    0, /* ASCRIPTION_TYPE */
2380
    0, /* TUPLE_UPDATE_OP */
2381
    2, /* TUPLE_UPDATE */
2382
    0, /* RECORD_UPDATE_OP */
2383
    2, /* RECORD_UPDATE */
2384
    1, /* DT_SIZE */
2385
    2, /* DT_HEIGHT_BOUND */
2386
    2, /* DT_SIZE_BOUND */
2387
    2, /* DT_SYGUS_BOUND */
2388
    1, /* DT_SYGUS_EVAL */
2389
    2, /* MATCH */
2390
    2, /* MATCH_CASE */
2391
    3, /* MATCH_BIND_CASE */
2392
    0, /* TUPLE_PROJECT_OP */
2393
    1, /* TUPLE_PROJECT */
2394
    0, /* SEP_NIL */
2395
    2, /* SEP_EMP */
2396
    2, /* SEP_PTO */
2397
    2, /* SEP_STAR */
2398
    2, /* SEP_WAND */
2399
    2, /* SEP_LABEL */
2400
    0, /* EMPTYSET */
2401
    1, /* SET_TYPE */
2402
    2, /* UNION */
2403
    2, /* INTERSECTION */
2404
    2, /* SETMINUS */
2405
    2, /* SUBSET */
2406
    2, /* MEMBER */
2407
    0, /* SINGLETON_OP */
2408
    1, /* SINGLETON */
2409
    2, /* INSERT */
2410
    1, /* CARD */
2411
    1, /* COMPLEMENT */
2412
    0, /* UNIVERSE_SET */
2413
    3, /* COMPREHENSION */
2414
    1, /* CHOOSE */
2415
    1, /* IS_SINGLETON */
2416
    2, /* JOIN */
2417
    2, /* PRODUCT */
2418
    1, /* TRANSPOSE */
2419
    1, /* TCLOSURE */
2420
    2, /* JOIN_IMAGE */
2421
    1, /* IDEN */
2422
    0, /* EMPTYBAG */
2423
    1, /* BAG_TYPE */
2424
    2, /* UNION_MAX */
2425
    2, /* UNION_DISJOINT */
2426
    2, /* INTERSECTION_MIN */
2427
    2, /* DIFFERENCE_SUBTRACT */
2428
    2, /* DIFFERENCE_REMOVE */
2429
    2, /* SUBBAG */
2430
    2, /* BAG_COUNT */
2431
    1, /* DUPLICATE_REMOVAL */
2432
    0, /* MK_BAG_OP */
2433
    2, /* MK_BAG */
2434
    1, /* BAG_IS_SINGLETON */
2435
    1, /* BAG_CARD */
2436
    1, /* BAG_FROM_SET */
2437
    1, /* BAG_TO_SET */
2438
    1, /* BAG_CHOOSE */
2439
    2, /* STRING_CONCAT */
2440
    2, /* STRING_IN_REGEXP */
2441
    1, /* STRING_LENGTH */
2442
    3, /* STRING_SUBSTR */
2443
    3, /* STRING_UPDATE */
2444
    2, /* STRING_CHARAT */
2445
    2, /* STRING_STRCTN */
2446
    2, /* STRING_LT */
2447
    2, /* STRING_LEQ */
2448
    3, /* STRING_STRIDOF */
2449
    3, /* STRING_STRREPL */
2450
    3, /* STRING_STRREPLALL */
2451
    3, /* STRING_REPLACE_RE */
2452
    3, /* STRING_REPLACE_RE_ALL */
2453
    2, /* STRING_PREFIX */
2454
    2, /* STRING_SUFFIX */
2455
    1, /* STRING_IS_DIGIT */
2456
    1, /* STRING_ITOS */
2457
    1, /* STRING_STOI */
2458
    1, /* STRING_TO_CODE */
2459
    1, /* STRING_FROM_CODE */
2460
    1, /* STRING_TOLOWER */
2461
    1, /* STRING_TOUPPER */
2462
    1, /* STRING_REV */
2463
    0, /* CONST_STRING */
2464
    1, /* SEQUENCE_TYPE */
2465
    0, /* CONST_SEQUENCE */
2466
    1, /* SEQ_UNIT */
2467
    2, /* SEQ_NTH */
2468
    2, /* SEQ_NTH_TOTAL */
2469
    1, /* STRING_TO_REGEXP */
2470
    2, /* REGEXP_CONCAT */
2471
    2, /* REGEXP_UNION */
2472
    2, /* REGEXP_INTER */
2473
    2, /* REGEXP_DIFF */
2474
    1, /* REGEXP_STAR */
2475
    1, /* REGEXP_PLUS */
2476
    1, /* REGEXP_OPT */
2477
    2, /* REGEXP_RANGE */
2478
    1, /* REGEXP_COMPLEMENT */
2479
    0, /* REGEXP_EMPTY */
2480
    0, /* REGEXP_SIGMA */
2481
    0, /* REGEXP_REPEAT_OP */
2482
    1, /* REGEXP_REPEAT */
2483
    0, /* REGEXP_LOOP_OP */
2484
    1, /* REGEXP_LOOP */
2485
    1, /* REGEXP_RV */
2486
    2, /* FORALL */
2487
    2, /* EXISTS */
2488
    0, /* INST_CONSTANT */
2489
    1, /* BOUND_VAR_LIST */
2490
    1, /* INST_PATTERN */
2491
    1, /* INST_NO_PATTERN */
2492
    1, /* INST_ATTRIBUTE */
2493
    1, /* INST_PATTERN_LIST */
2494
2495
    0 /* LAST_KIND */
2496
  };
2497
2498
259076015
  return lbs[k];
2499
}
2500
2501
260353438
uint32_t getMaxArityForKind(::CVC4::Kind k)
2502
{
2503
  static const unsigned ubs[] = {
2504
    0, /* NULL_EXPR */
2505
2506
    0, /* SORT_TAG */
2507
    expr::NodeValue::MAX_CHILDREN, /* SORT_TYPE */
2508
    0, /* UNINTERPRETED_CONSTANT */
2509
    0, /* ABSTRACT_VALUE */
2510
    0, /* BUILTIN */
2511
    2, /* EQUAL */
2512
    expr::NodeValue::MAX_CHILDREN, /* DISTINCT */
2513
    0, /* VARIABLE */
2514
    0, /* BOUND_VARIABLE */
2515
    0, /* SKOLEM */
2516
    expr::NodeValue::MAX_CHILDREN, /* SEXPR */
2517
    2, /* LAMBDA */
2518
    2, /* WITNESS */
2519
    0, /* TYPE_CONSTANT */
2520
    expr::NodeValue::MAX_CHILDREN, /* FUNCTION_TYPE */
2521
    expr::NodeValue::MAX_CHILDREN, /* SEXPR_TYPE */
2522
    0, /* CONST_BOOLEAN */
2523
    1, /* NOT */
2524
    expr::NodeValue::MAX_CHILDREN, /* AND */
2525
    2, /* IMPLIES */
2526
    expr::NodeValue::MAX_CHILDREN, /* OR */
2527
    2, /* XOR */
2528
    3, /* ITE */
2529
    expr::NodeValue::MAX_CHILDREN, /* APPLY_UF */
2530
    0, /* BOOLEAN_TERM_VARIABLE */
2531
    2, /* CARDINALITY_CONSTRAINT */
2532
    1, /* COMBINED_CARDINALITY_CONSTRAINT */
2533
    expr::NodeValue::MAX_CHILDREN, /* PARTIAL_APPLY_UF */
2534
    1, /* CARDINALITY_VALUE */
2535
    2, /* HO_APPLY */
2536
    expr::NodeValue::MAX_CHILDREN, /* PLUS */
2537
    expr::NodeValue::MAX_CHILDREN, /* MULT */
2538
    expr::NodeValue::MAX_CHILDREN, /* NONLINEAR_MULT */
2539
    2, /* MINUS */
2540
    1, /* UMINUS */
2541
    2, /* DIVISION */
2542
    2, /* DIVISION_TOTAL */
2543
    2, /* INTS_DIVISION */
2544
    2, /* INTS_DIVISION_TOTAL */
2545
    2, /* INTS_MODULUS */
2546
    2, /* INTS_MODULUS_TOTAL */
2547
    1, /* ABS */
2548
    1, /* DIVISIBLE */
2549
    2, /* POW */
2550
    1, /* EXPONENTIAL */
2551
    1, /* SINE */
2552
    1, /* COSINE */
2553
    1, /* TANGENT */
2554
    1, /* COSECANT */
2555
    1, /* SECANT */
2556
    1, /* COTANGENT */
2557
    1, /* ARCSINE */
2558
    1, /* ARCCOSINE */
2559
    1, /* ARCTANGENT */
2560
    1, /* ARCCOSECANT */
2561
    1, /* ARCSECANT */
2562
    1, /* ARCCOTANGENT */
2563
    1, /* SQRT */
2564
    0, /* DIVISIBLE_OP */
2565
    0, /* CONST_RATIONAL */
2566
    2, /* LT */
2567
    2, /* LEQ */
2568
    2, /* GT */
2569
    2, /* GEQ */
2570
    0, /* INDEXED_ROOT_PREDICATE_OP */
2571
    2, /* INDEXED_ROOT_PREDICATE */
2572
    1, /* IS_INTEGER */
2573
    1, /* TO_INTEGER */
2574
    1, /* TO_REAL */
2575
    1, /* CAST_TO_REAL */
2576
    0, /* PI */
2577
    0, /* IAND_OP */
2578
    2, /* IAND */
2579
    0, /* BITVECTOR_TYPE */
2580
    0, /* CONST_BITVECTOR */
2581
    expr::NodeValue::MAX_CHILDREN, /* BITVECTOR_CONCAT */
2582
    expr::NodeValue::MAX_CHILDREN, /* BITVECTOR_AND */
2583
    2, /* BITVECTOR_COMP */
2584
    expr::NodeValue::MAX_CHILDREN, /* BITVECTOR_OR */
2585
    expr::NodeValue::MAX_CHILDREN, /* BITVECTOR_XOR */
2586
    1, /* BITVECTOR_NOT */
2587
    2, /* BITVECTOR_NAND */
2588
    2, /* BITVECTOR_NOR */
2589
    2, /* BITVECTOR_XNOR */
2590
    expr::NodeValue::MAX_CHILDREN, /* BITVECTOR_MULT */
2591
    1, /* BITVECTOR_NEG */
2592
    expr::NodeValue::MAX_CHILDREN, /* BITVECTOR_PLUS */
2593
    2, /* BITVECTOR_SUB */
2594
    2, /* BITVECTOR_UDIV */
2595
    2, /* BITVECTOR_UREM */
2596
    2, /* BITVECTOR_SDIV */
2597
    2, /* BITVECTOR_SMOD */
2598
    2, /* BITVECTOR_SREM */
2599
    2, /* BITVECTOR_ASHR */
2600
    2, /* BITVECTOR_LSHR */
2601
    2, /* BITVECTOR_SHL */
2602
    2, /* BITVECTOR_ULE */
2603
    2, /* BITVECTOR_ULT */
2604
    2, /* BITVECTOR_UGE */
2605
    2, /* BITVECTOR_UGT */
2606
    2, /* BITVECTOR_SLE */
2607
    2, /* BITVECTOR_SLT */
2608
    2, /* BITVECTOR_SGE */
2609
    2, /* BITVECTOR_SGT */
2610
    2, /* BITVECTOR_ULTBV */
2611
    2, /* BITVECTOR_SLTBV */
2612
    1, /* BITVECTOR_REDAND */
2613
    1, /* BITVECTOR_REDOR */
2614
    3, /* BITVECTOR_ITE */
2615
    1, /* BITVECTOR_TO_NAT */
2616
    1, /* BITVECTOR_ACKERMANNIZE_UDIV */
2617
    1, /* BITVECTOR_ACKERMANNIZE_UREM */
2618
    1, /* BITVECTOR_EAGER_ATOM */
2619
    0, /* BITVECTOR_BITOF_OP */
2620
    1, /* BITVECTOR_BITOF */
2621
    0, /* BITVECTOR_EXTRACT_OP */
2622
    1, /* BITVECTOR_EXTRACT */
2623
    0, /* BITVECTOR_REPEAT_OP */
2624
    1, /* BITVECTOR_REPEAT */
2625
    0, /* BITVECTOR_ROTATE_LEFT_OP */
2626
    1, /* BITVECTOR_ROTATE_LEFT */
2627
    0, /* BITVECTOR_ROTATE_RIGHT_OP */
2628
    1, /* BITVECTOR_ROTATE_RIGHT */
2629
    0, /* BITVECTOR_SIGN_EXTEND_OP */
2630
    1, /* BITVECTOR_SIGN_EXTEND */
2631
    0, /* BITVECTOR_ZERO_EXTEND_OP */
2632
    1, /* BITVECTOR_ZERO_EXTEND */
2633
    0, /* INT_TO_BITVECTOR_OP */
2634
    1, /* INT_TO_BITVECTOR */
2635
    0, /* CONST_FLOATINGPOINT */
2636
    0, /* CONST_ROUNDINGMODE */
2637
    0, /* FLOATINGPOINT_TYPE */
2638
    3, /* FLOATINGPOINT_FP */
2639
    expr::NodeValue::MAX_CHILDREN, /* FLOATINGPOINT_EQ */
2640
    1, /* FLOATINGPOINT_ABS */
2641
    1, /* FLOATINGPOINT_NEG */
2642
    3, /* FLOATINGPOINT_PLUS */
2643
    3, /* FLOATINGPOINT_SUB */
2644
    3, /* FLOATINGPOINT_MULT */
2645
    3, /* FLOATINGPOINT_DIV */
2646
    4, /* FLOATINGPOINT_FMA */
2647
    2, /* FLOATINGPOINT_SQRT */
2648
    2, /* FLOATINGPOINT_REM */
2649
    2, /* FLOATINGPOINT_RTI */
2650
    2, /* FLOATINGPOINT_MIN */
2651
    2, /* FLOATINGPOINT_MAX */
2652
    3, /* FLOATINGPOINT_MIN_TOTAL */
2653
    3, /* FLOATINGPOINT_MAX_TOTAL */
2654
    expr::NodeValue::MAX_CHILDREN, /* FLOATINGPOINT_LEQ */
2655
    expr::NodeValue::MAX_CHILDREN, /* FLOATINGPOINT_LT */
2656
    expr::NodeValue::MAX_CHILDREN, /* FLOATINGPOINT_GEQ */
2657
    expr::NodeValue::MAX_CHILDREN, /* FLOATINGPOINT_GT */
2658
    1, /* FLOATINGPOINT_ISN */
2659
    1, /* FLOATINGPOINT_ISSN */
2660
    1, /* FLOATINGPOINT_ISZ */
2661
    1, /* FLOATINGPOINT_ISINF */
2662
    1, /* FLOATINGPOINT_ISNAN */
2663
    1, /* FLOATINGPOINT_ISNEG */
2664
    1, /* FLOATINGPOINT_ISPOS */
2665
    0, /* FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP */
2666
    1, /* FLOATINGPOINT_TO_FP_IEEE_BITVECTOR */
2667
    0, /* FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP */
2668
    2, /* FLOATINGPOINT_TO_FP_FLOATINGPOINT */
2669
    0, /* FLOATINGPOINT_TO_FP_REAL_OP */
2670
    2, /* FLOATINGPOINT_TO_FP_REAL */
2671
    0, /* FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP */
2672
    2, /* FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR */
2673
    0, /* FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP */
2674
    2, /* FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR */
2675
    0, /* FLOATINGPOINT_TO_FP_GENERIC_OP */
2676
    2, /* FLOATINGPOINT_TO_FP_GENERIC */
2677
    0, /* FLOATINGPOINT_TO_UBV_OP */
2678
    2, /* FLOATINGPOINT_TO_UBV */
2679
    0, /* FLOATINGPOINT_TO_UBV_TOTAL_OP */
2680
    3, /* FLOATINGPOINT_TO_UBV_TOTAL */
2681
    0, /* FLOATINGPOINT_TO_SBV_OP */
2682
    2, /* FLOATINGPOINT_TO_SBV */
2683
    0, /* FLOATINGPOINT_TO_SBV_TOTAL_OP */
2684
    3, /* FLOATINGPOINT_TO_SBV_TOTAL */
2685
    1, /* FLOATINGPOINT_TO_REAL */
2686
    2, /* FLOATINGPOINT_TO_REAL_TOTAL */
2687
    1, /* FLOATINGPOINT_COMPONENT_NAN */
2688
    1, /* FLOATINGPOINT_COMPONENT_INF */
2689
    1, /* FLOATINGPOINT_COMPONENT_ZERO */
2690
    1, /* FLOATINGPOINT_COMPONENT_SIGN */
2691
    1, /* FLOATINGPOINT_COMPONENT_EXPONENT */
2692
    1, /* FLOATINGPOINT_COMPONENT_SIGNIFICAND */
2693
    1, /* ROUNDINGMODE_BITBLAST */
2694
    2, /* ARRAY_TYPE */
2695
    2, /* SELECT */
2696
    3, /* STORE */
2697
    4, /* EQ_RANGE */
2698
    0, /* STORE_ALL */
2699
    4, /* ARR_TABLE_FUN */
2700
    1, /* ARRAY_LAMBDA */
2701
    2, /* PARTIAL_SELECT_0 */
2702
    2, /* PARTIAL_SELECT_1 */
2703
    expr::NodeValue::MAX_CHILDREN, /* CONSTRUCTOR_TYPE */
2704
    2, /* SELECTOR_TYPE */
2705
    1, /* TESTER_TYPE */
2706
    expr::NodeValue::MAX_CHILDREN, /* APPLY_CONSTRUCTOR */
2707
    1, /* APPLY_SELECTOR */
2708
    1, /* APPLY_SELECTOR_TOTAL */
2709
    1, /* APPLY_TESTER */
2710
    0, /* DATATYPE_TYPE */
2711
    expr::NodeValue::MAX_CHILDREN, /* PARAMETRIC_DATATYPE */
2712
    1, /* APPLY_TYPE_ASCRIPTION */
2713
    0, /* ASCRIPTION_TYPE */
2714
    0, /* TUPLE_UPDATE_OP */
2715
    2, /* TUPLE_UPDATE */
2716
    0, /* RECORD_UPDATE_OP */
2717
    2, /* RECORD_UPDATE */
2718
    1, /* DT_SIZE */
2719
    2, /* DT_HEIGHT_BOUND */
2720
    2, /* DT_SIZE_BOUND */
2721
    2, /* DT_SYGUS_BOUND */
2722
    expr::NodeValue::MAX_CHILDREN, /* DT_SYGUS_EVAL */
2723
    expr::NodeValue::MAX_CHILDREN, /* MATCH */
2724
    2, /* MATCH_CASE */
2725
    3, /* MATCH_BIND_CASE */
2726
    0, /* TUPLE_PROJECT_OP */
2727
    1, /* TUPLE_PROJECT */
2728
    0, /* SEP_NIL */
2729
    2, /* SEP_EMP */
2730
    2, /* SEP_PTO */
2731
    expr::NodeValue::MAX_CHILDREN, /* SEP_STAR */
2732
    2, /* SEP_WAND */
2733
    2, /* SEP_LABEL */
2734
    0, /* EMPTYSET */
2735
    1, /* SET_TYPE */
2736
    2, /* UNION */
2737
    2, /* INTERSECTION */
2738
    2, /* SETMINUS */
2739
    2, /* SUBSET */
2740
    2, /* MEMBER */
2741
    0, /* SINGLETON_OP */
2742
    1, /* SINGLETON */
2743
    expr::NodeValue::MAX_CHILDREN, /* INSERT */
2744
    1, /* CARD */
2745
    1, /* COMPLEMENT */
2746
    0, /* UNIVERSE_SET */
2747
    3, /* COMPREHENSION */
2748
    1, /* CHOOSE */
2749
    1, /* IS_SINGLETON */
2750
    2, /* JOIN */
2751
    2, /* PRODUCT */
2752
    1, /* TRANSPOSE */
2753
    1, /* TCLOSURE */
2754
    2, /* JOIN_IMAGE */
2755
    1, /* IDEN */
2756
    0, /* EMPTYBAG */
2757
    1, /* BAG_TYPE */
2758
    2, /* UNION_MAX */
2759
    2, /* UNION_DISJOINT */
2760
    2, /* INTERSECTION_MIN */
2761
    2, /* DIFFERENCE_SUBTRACT */
2762
    2, /* DIFFERENCE_REMOVE */
2763
    2, /* SUBBAG */
2764
    2, /* BAG_COUNT */
2765
    1, /* DUPLICATE_REMOVAL */
2766
    0, /* MK_BAG_OP */
2767
    2, /* MK_BAG */
2768
    1, /* BAG_IS_SINGLETON */
2769
    1, /* BAG_CARD */
2770
    1, /* BAG_FROM_SET */
2771
    1, /* BAG_TO_SET */
2772
    1, /* BAG_CHOOSE */
2773
    expr::NodeValue::MAX_CHILDREN, /* STRING_CONCAT */
2774
    2, /* STRING_IN_REGEXP */
2775
    1, /* STRING_LENGTH */
2776
    3, /* STRING_SUBSTR */
2777
    3, /* STRING_UPDATE */
2778
    2, /* STRING_CHARAT */
2779
    2, /* STRING_STRCTN */
2780
    2, /* STRING_LT */
2781
    2, /* STRING_LEQ */
2782
    3, /* STRING_STRIDOF */
2783
    3, /* STRING_STRREPL */
2784
    3, /* STRING_STRREPLALL */
2785
    3, /* STRING_REPLACE_RE */
2786
    3, /* STRING_REPLACE_RE_ALL */
2787
    2, /* STRING_PREFIX */
2788
    2, /* STRING_SUFFIX */
2789
    1, /* STRING_IS_DIGIT */
2790
    1, /* STRING_ITOS */
2791
    1, /* STRING_STOI */
2792
    1, /* STRING_TO_CODE */
2793
    1, /* STRING_FROM_CODE */
2794
    1, /* STRING_TOLOWER */
2795
    1, /* STRING_TOUPPER */
2796
    1, /* STRING_REV */
2797
    0, /* CONST_STRING */
2798
    1, /* SEQUENCE_TYPE */
2799
    0, /* CONST_SEQUENCE */
2800
    1, /* SEQ_UNIT */
2801
    2, /* SEQ_NTH */
2802
    2, /* SEQ_NTH_TOTAL */
2803
    1, /* STRING_TO_REGEXP */
2804
    expr::NodeValue::MAX_CHILDREN, /* REGEXP_CONCAT */
2805
    expr::NodeValue::MAX_CHILDREN, /* REGEXP_UNION */
2806
    expr::NodeValue::MAX_CHILDREN, /* REGEXP_INTER */
2807
    2, /* REGEXP_DIFF */
2808
    1, /* REGEXP_STAR */
2809
    1, /* REGEXP_PLUS */
2810
    1, /* REGEXP_OPT */
2811
    2, /* REGEXP_RANGE */
2812
    1, /* REGEXP_COMPLEMENT */
2813
    0, /* REGEXP_EMPTY */
2814
    0, /* REGEXP_SIGMA */
2815
    0, /* REGEXP_REPEAT_OP */
2816
    1, /* REGEXP_REPEAT */
2817
    0, /* REGEXP_LOOP_OP */
2818
    1, /* REGEXP_LOOP */
2819
    1, /* REGEXP_RV */
2820
    3, /* FORALL */
2821
    3, /* EXISTS */
2822
    0, /* INST_CONSTANT */
2823
    expr::NodeValue::MAX_CHILDREN, /* BOUND_VAR_LIST */
2824
    expr::NodeValue::MAX_CHILDREN, /* INST_PATTERN */
2825
    1, /* INST_NO_PATTERN */
2826
    1, /* INST_ATTRIBUTE */
2827
    expr::NodeValue::MAX_CHILDREN, /* INST_PATTERN_LIST */
2828
2829
    0, /* LAST_KIND */
2830
  };
2831
2832
260353438
  return ubs[k];
2833
}
2834
}  // namespace metakind
2835
2836
/**
2837
 * Map a kind of the operator to the kind of the enclosing expression. For
2838
 * example, since the kind of functions is just VARIABLE, it should map
2839
 * VARIABLE to APPLY_UF.
2840
 */
2841
638779
Kind operatorToKind(::CVC4::expr::NodeValue* nv) {
2842
638779
  if(nv->getKind() == kind::BUILTIN) {
2843
136343
    return nv->getConst<Kind>();
2844
502436
  } else if(nv->getKind() == kind::LAMBDA) {
2845
1682
    return kind::APPLY_UF;
2846
  }
2847
2848
500754
  switch(Kind k CVC4_UNUSED = nv->getKind()) {
2849
2850
2851
    /* from builtin */
2852
    case kind::SORT_TAG: return kind::SORT_TYPE;
2853
2854
    /* from booleans */
2855
2856
    /* from uf */
2857
    case kind::VARIABLE: return kind::APPLY_UF;
2858
    case kind::APPLY_UF: return kind::PARTIAL_APPLY_UF;
2859
2860
    /* from arith */
2861
    case kind::DIVISIBLE_OP: return kind::DIVISIBLE;
2862
    case kind::INDEXED_ROOT_PREDICATE_OP: return kind::INDEXED_ROOT_PREDICATE;
2863
    case kind::IAND_OP: return kind::IAND;
2864
2865
    /* from bv */
2866
184013
    case kind::BITVECTOR_BITOF_OP: return kind::BITVECTOR_BITOF;
2867
59097
    case kind::BITVECTOR_EXTRACT_OP: return kind::BITVECTOR_EXTRACT;
2868
    case kind::BITVECTOR_REPEAT_OP: return kind::BITVECTOR_REPEAT;
2869
    case kind::BITVECTOR_ROTATE_LEFT_OP: return kind::BITVECTOR_ROTATE_LEFT;
2870
    case kind::BITVECTOR_ROTATE_RIGHT_OP: return kind::BITVECTOR_ROTATE_RIGHT;
2871
351
    case kind::BITVECTOR_SIGN_EXTEND_OP: return kind::BITVECTOR_SIGN_EXTEND;
2872
56
    case kind::BITVECTOR_ZERO_EXTEND_OP: return kind::BITVECTOR_ZERO_EXTEND;
2873
269
    case kind::INT_TO_BITVECTOR_OP: return kind::INT_TO_BITVECTOR;
2874
2875
    /* from fp */
2876
3324
    case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP: return kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR;
2877
6
    case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP: return kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT;
2878
12
    case kind::FLOATINGPOINT_TO_FP_REAL_OP: return kind::FLOATINGPOINT_TO_FP_REAL;
2879
4
    case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP: return kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR;
2880
    case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP: return kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR;
2881
    case kind::FLOATINGPOINT_TO_FP_GENERIC_OP: return kind::FLOATINGPOINT_TO_FP_GENERIC;
2882
    case kind::FLOATINGPOINT_TO_UBV_OP: return kind::FLOATINGPOINT_TO_UBV;
2883
    case kind::FLOATINGPOINT_TO_UBV_TOTAL_OP: return kind::FLOATINGPOINT_TO_UBV_TOTAL;
2884
    case kind::FLOATINGPOINT_TO_SBV_OP: return kind::FLOATINGPOINT_TO_SBV;
2885
    case kind::FLOATINGPOINT_TO_SBV_TOTAL_OP: return kind::FLOATINGPOINT_TO_SBV_TOTAL;
2886
2887
    /* from arrays */
2888
2889
    /* from datatypes */
2890
    case kind::APPLY_TYPE_ASCRIPTION: return kind::APPLY_CONSTRUCTOR;
2891
    case kind::SELECTOR_TYPE: return kind::APPLY_SELECTOR;
2892
    case kind::TESTER_TYPE: return kind::APPLY_TESTER;
2893
    case kind::ASCRIPTION_TYPE: return kind::APPLY_TYPE_ASCRIPTION;
2894
    case kind::TUPLE_UPDATE_OP: return kind::TUPLE_UPDATE;
2895
    case kind::RECORD_UPDATE_OP: return kind::RECORD_UPDATE;
2896
    case kind::TUPLE_PROJECT_OP: return kind::TUPLE_PROJECT;
2897
2898
    /* from sep */
2899
2900
    /* from sets */
2901
    case kind::SINGLETON_OP: return kind::SINGLETON;
2902
2903
    /* from bags */
2904
    case kind::MK_BAG_OP: return kind::MK_BAG;
2905
2906
    /* from strings */
2907
2
    case kind::REGEXP_REPEAT_OP: return kind::REGEXP_REPEAT;
2908
2
    case kind::REGEXP_LOOP_OP: return kind::REGEXP_LOOP;
2909
2910
    /* from quantifiers */
2911
2912
253618
  default:
2913
253618
    return kind::UNDEFINED_KIND;  /* LAST_KIND */
2914
  };
2915
}
2916
2917
}/* CVC4::kind namespace */
2918
26676
}/* CVC4 namespace */