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