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-08-17/src/expr/type_checker_template.cpp /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-17/src/theory/builtin/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-17/src/theory/booleans/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-17/src/theory/uf/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-17/src/theory/arith/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-17/src/theory/bv/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-17/src/theory/fp/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-17/src/theory/arrays/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-17/src/theory/datatypes/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-17/src/theory/sep/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-17/src/theory/sets/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-17/src/theory/bags/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-17/src/theory/strings/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-17/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-08-17/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 |
27338490 |
TypeNode TypeChecker::computeType(NodeManager* nodeManager, TNode n, bool check) |
77 |
|
{ |
78 |
27338490 |
TypeNode typeNode; |
79 |
|
|
80 |
|
// Infer the type |
81 |
27338490 |
switch (n.getKind()) |
82 |
|
{ |
83 |
|
case kind::VARIABLE: |
84 |
|
case kind::SKOLEM: |
85 |
|
typeNode = nodeManager->getAttribute(n, TypeAttr()); |
86 |
|
break; |
87 |
2829 |
case kind::BUILTIN: |
88 |
2829 |
typeNode = nodeManager->builtinOperatorType(); |
89 |
2829 |
break; |
90 |
|
|
91 |
|
// clang-format off |
92 |
|
|
93 |
2708 |
case kind::UNINTERPRETED_CONSTANT: |
94 |
2708 |
typeNode = ::cvc5::theory::builtin::UninterpretedConstantTypeRule::computeType(nodeManager, n, check); |
95 |
2708 |
break; |
96 |
|
|
97 |
|
case kind::ABSTRACT_VALUE: |
98 |
|
typeNode = ::cvc5::theory::builtin::AbstractValueTypeRule::computeType(nodeManager, n, check); |
99 |
|
break; |
100 |
|
|
101 |
5520113 |
case kind::EQUAL: |
102 |
5520113 |
typeNode = ::cvc5::theory::builtin::EqualityTypeRule::computeType(nodeManager, n, check); |
103 |
5520035 |
break; |
104 |
|
|
105 |
10411 |
case kind::DISTINCT: |
106 |
10411 |
typeNode = ::cvc5::theory::builtin::DistinctTypeRule::computeType(nodeManager, n, check); |
107 |
10411 |
break; |
108 |
|
|
109 |
825485 |
case kind::SEXPR: |
110 |
825485 |
typeNode = ::cvc5::theory::builtin::SExprTypeRule::computeType(nodeManager, n, check); |
111 |
825485 |
break; |
112 |
|
|
113 |
19502 |
case kind::LAMBDA: |
114 |
19502 |
typeNode = ::cvc5::theory::builtin::LambdaTypeRule::computeType(nodeManager, n, check); |
115 |
19502 |
break; |
116 |
|
|
117 |
3852 |
case kind::WITNESS: |
118 |
3852 |
typeNode = ::cvc5::theory::builtin::WitnessTypeRule::computeType(nodeManager, n, check); |
119 |
3852 |
break; |
120 |
|
|
121 |
21843 |
case kind::CONST_BOOLEAN: |
122 |
21843 |
typeNode = ::cvc5::theory::boolean::BooleanTypeRule::computeType(nodeManager, n, check); |
123 |
21843 |
break; |
124 |
|
|
125 |
3555092 |
case kind::NOT: |
126 |
3555092 |
typeNode = ::cvc5::theory::boolean::BooleanTypeRule::computeType(nodeManager, n, check); |
127 |
3555078 |
break; |
128 |
|
|
129 |
3224584 |
case kind::AND: |
130 |
3224584 |
typeNode = ::cvc5::theory::boolean::BooleanTypeRule::computeType(nodeManager, n, check); |
131 |
3224506 |
break; |
132 |
|
|
133 |
543903 |
case kind::IMPLIES: |
134 |
543903 |
typeNode = ::cvc5::theory::boolean::BooleanTypeRule::computeType(nodeManager, n, check); |
135 |
543825 |
break; |
136 |
|
|
137 |
3680944 |
case kind::OR: |
138 |
3680944 |
typeNode = ::cvc5::theory::boolean::BooleanTypeRule::computeType(nodeManager, n, check); |
139 |
3680866 |
break; |
140 |
|
|
141 |
773923 |
case kind::XOR: |
142 |
773923 |
typeNode = ::cvc5::theory::boolean::BooleanTypeRule::computeType(nodeManager, n, check); |
143 |
773845 |
break; |
144 |
|
|
145 |
1453116 |
case kind::ITE: |
146 |
1453116 |
typeNode = ::cvc5::theory::boolean::IteTypeRule::computeType(nodeManager, n, check); |
147 |
1453084 |
break; |
148 |
|
|
149 |
457386 |
case kind::APPLY_UF: |
150 |
457386 |
typeNode = ::cvc5::theory::uf::UfTypeRule::computeType(nodeManager, n, check); |
151 |
457386 |
break; |
152 |
|
|
153 |
1099 |
case kind::CARDINALITY_CONSTRAINT: |
154 |
1099 |
typeNode = ::cvc5::theory::uf::CardinalityConstraintTypeRule::computeType(nodeManager, n, check); |
155 |
1099 |
break; |
156 |
|
|
157 |
639 |
case kind::COMBINED_CARDINALITY_CONSTRAINT: |
158 |
639 |
typeNode = ::cvc5::theory::uf::CombinedCardinalityConstraintTypeRule::computeType(nodeManager, n, check); |
159 |
639 |
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 |
13789 |
case kind::HO_APPLY: |
170 |
13789 |
typeNode = ::cvc5::theory::uf::HoApplyTypeRule::computeType(nodeManager, n, check); |
171 |
13789 |
break; |
172 |
|
|
173 |
2776222 |
case kind::PLUS: |
174 |
2776222 |
typeNode = ::cvc5::theory::arith::ArithOperatorTypeRule::computeType(nodeManager, n, check); |
175 |
2776222 |
break; |
176 |
|
|
177 |
650813 |
case kind::MULT: |
178 |
650813 |
typeNode = ::cvc5::theory::arith::ArithOperatorTypeRule::computeType(nodeManager, n, check); |
179 |
650813 |
break; |
180 |
|
|
181 |
21532 |
case kind::NONLINEAR_MULT: |
182 |
21532 |
typeNode = ::cvc5::theory::arith::ArithOperatorTypeRule::computeType(nodeManager, n, check); |
183 |
21532 |
break; |
184 |
|
|
185 |
186179 |
case kind::MINUS: |
186 |
186179 |
typeNode = ::cvc5::theory::arith::ArithOperatorTypeRule::computeType(nodeManager, n, check); |
187 |
186179 |
break; |
188 |
|
|
189 |
10939 |
case kind::UMINUS: |
190 |
10939 |
typeNode = ::cvc5::theory::arith::ArithOperatorTypeRule::computeType(nodeManager, n, check); |
191 |
10939 |
break; |
192 |
|
|
193 |
2513 |
case kind::DIVISION: |
194 |
2513 |
typeNode = ::cvc5::theory::arith::ArithOperatorTypeRule::computeType(nodeManager, n, check); |
195 |
2513 |
break; |
196 |
|
|
197 |
140 |
case kind::POW: |
198 |
140 |
typeNode = ::cvc5::theory::arith::ArithOperatorTypeRule::computeType(nodeManager, n, check); |
199 |
140 |
break; |
200 |
|
|
201 |
256699 |
case kind::CONST_RATIONAL: |
202 |
256699 |
typeNode = ::cvc5::theory::arith::ArithConstantTypeRule::computeType(nodeManager, n, check); |
203 |
256699 |
break; |
204 |
|
|
205 |
127206 |
case kind::LT: |
206 |
127206 |
typeNode = SimpleTypeRule<RBool, AReal, AReal>::computeType(nodeManager, n, check); |
207 |
127206 |
break; |
208 |
|
|
209 |
174277 |
case kind::LEQ: |
210 |
174277 |
typeNode = SimpleTypeRule<RBool, AReal, AReal>::computeType(nodeManager, n, check); |
211 |
174277 |
break; |
212 |
|
|
213 |
76126 |
case kind::GT: |
214 |
76126 |
typeNode = SimpleTypeRule<RBool, AReal, AReal>::computeType(nodeManager, n, check); |
215 |
76126 |
break; |
216 |
|
|
217 |
507893 |
case kind::GEQ: |
218 |
507893 |
typeNode = SimpleTypeRule<RBool, AReal, AReal>::computeType(nodeManager, n, check); |
219 |
507893 |
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 |
1502 |
case kind::CAST_TO_REAL: |
234 |
1502 |
typeNode = ::cvc5::theory::arith::ArithOperatorTypeRule::computeType(nodeManager, n, check); |
235 |
1502 |
break; |
236 |
|
|
237 |
702 |
case kind::TO_INTEGER: |
238 |
702 |
typeNode = ::cvc5::theory::arith::ArithOperatorTypeRule::computeType(nodeManager, n, check); |
239 |
702 |
break; |
240 |
|
|
241 |
39 |
case kind::IS_INTEGER: |
242 |
39 |
typeNode = SimpleTypeRule<RBool, AReal>::computeType(nodeManager, n, check); |
243 |
39 |
break; |
244 |
|
|
245 |
39 |
case kind::ABS: |
246 |
39 |
typeNode = SimpleTypeRule<RInteger, AInteger>::computeType(nodeManager, n, check); |
247 |
39 |
break; |
248 |
|
|
249 |
630 |
case kind::INTS_DIVISION: |
250 |
630 |
typeNode = SimpleTypeRule<RInteger, AInteger, AInteger>::computeType(nodeManager, n, check); |
251 |
630 |
break; |
252 |
|
|
253 |
368 |
case kind::INTS_MODULUS: |
254 |
368 |
typeNode = SimpleTypeRule<RInteger, AInteger, AInteger>::computeType(nodeManager, n, check); |
255 |
368 |
break; |
256 |
|
|
257 |
6 |
case kind::DIVISIBLE: |
258 |
6 |
typeNode = SimpleTypeRule<RBool, AInteger>::computeType(nodeManager, n, check); |
259 |
4 |
break; |
260 |
|
|
261 |
12 |
case kind::DIVISIBLE_OP: |
262 |
12 |
typeNode = SimpleTypeRule<RBuiltinOperator>::computeType(nodeManager, n, check); |
263 |
12 |
break; |
264 |
|
|
265 |
220 |
case kind::DIVISION_TOTAL: |
266 |
220 |
typeNode = ::cvc5::theory::arith::ArithOperatorTypeRule::computeType(nodeManager, n, check); |
267 |
220 |
break; |
268 |
|
|
269 |
2651 |
case kind::INTS_DIVISION_TOTAL: |
270 |
2651 |
typeNode = SimpleTypeRule<RInteger, AInteger, AInteger>::computeType(nodeManager, n, check); |
271 |
2651 |
break; |
272 |
|
|
273 |
3236 |
case kind::INTS_MODULUS_TOTAL: |
274 |
3236 |
typeNode = SimpleTypeRule<RInteger, AInteger, AInteger>::computeType(nodeManager, n, check); |
275 |
3236 |
break; |
276 |
|
|
277 |
223 |
case kind::EXPONENTIAL: |
278 |
223 |
typeNode = SimpleTypeRule<RReal, AReal>::computeType(nodeManager, n, check); |
279 |
223 |
break; |
280 |
|
|
281 |
1610 |
case kind::SINE: |
282 |
1610 |
typeNode = SimpleTypeRule<RReal, AReal>::computeType(nodeManager, n, check); |
283 |
1610 |
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 |
58 |
case kind::POW2: |
330 |
58 |
typeNode = SimpleTypeRule<RInteger, AInteger>::computeType(nodeManager, n, check); |
331 |
58 |
break; |
332 |
|
|
333 |
25 |
case kind::SQRT: |
334 |
25 |
typeNode = SimpleTypeRule<RReal, AReal>::computeType(nodeManager, n, check); |
335 |
25 |
break; |
336 |
|
|
337 |
1668 |
case kind::PI: |
338 |
1668 |
typeNode = ::cvc5::theory::arith::RealNullaryOperatorTypeRule::computeType(nodeManager, n, check); |
339 |
1668 |
break; |
340 |
|
|
341 |
67 |
case kind::IAND_OP: |
342 |
67 |
typeNode = ::cvc5::theory::arith::IAndOpTypeRule::computeType(nodeManager, n, check); |
343 |
67 |
break; |
344 |
|
|
345 |
292 |
case kind::IAND: |
346 |
292 |
typeNode = ::cvc5::theory::arith::IAndTypeRule::computeType(nodeManager, n, check); |
347 |
292 |
break; |
348 |
|
|
349 |
69629 |
case kind::CONST_BITVECTOR: |
350 |
69629 |
typeNode = ::cvc5::theory::bv::BitVectorConstantTypeRule::computeType(nodeManager, n, check); |
351 |
69629 |
break; |
352 |
|
|
353 |
3634 |
case kind::BITVECTOR_BB_TERM: |
354 |
3634 |
typeNode = ::cvc5::theory::bv::BitVectorToBVTypeRule::computeType(nodeManager, n, check); |
355 |
3634 |
break; |
356 |
|
|
357 |
100266 |
case kind::BITVECTOR_CONCAT: |
358 |
100266 |
typeNode = ::cvc5::theory::bv::BitVectorConcatTypeRule::computeType(nodeManager, n, check); |
359 |
100266 |
break; |
360 |
|
|
361 |
92415 |
case kind::BITVECTOR_AND: |
362 |
92415 |
typeNode = ::cvc5::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check); |
363 |
92415 |
break; |
364 |
|
|
365 |
159573 |
case kind::BITVECTOR_COMP: |
366 |
159573 |
typeNode = ::cvc5::theory::bv::BitVectorBVPredTypeRule::computeType(nodeManager, n, check); |
367 |
159573 |
break; |
368 |
|
|
369 |
289 |
case kind::BITVECTOR_NAND: |
370 |
289 |
typeNode = ::cvc5::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check); |
371 |
289 |
break; |
372 |
|
|
373 |
346 |
case kind::BITVECTOR_NOR: |
374 |
346 |
typeNode = ::cvc5::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check); |
375 |
346 |
break; |
376 |
|
|
377 |
53318 |
case kind::BITVECTOR_NOT: |
378 |
53318 |
typeNode = ::cvc5::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check); |
379 |
53318 |
break; |
380 |
|
|
381 |
141434 |
case kind::BITVECTOR_OR: |
382 |
141434 |
typeNode = ::cvc5::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check); |
383 |
141434 |
break; |
384 |
|
|
385 |
432 |
case kind::BITVECTOR_XNOR: |
386 |
432 |
typeNode = ::cvc5::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check); |
387 |
432 |
break; |
388 |
|
|
389 |
6667 |
case kind::BITVECTOR_XOR: |
390 |
6667 |
typeNode = ::cvc5::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check); |
391 |
6667 |
break; |
392 |
|
|
393 |
255165 |
case kind::BITVECTOR_MULT: |
394 |
255165 |
typeNode = ::cvc5::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check); |
395 |
255165 |
break; |
396 |
|
|
397 |
16295 |
case kind::BITVECTOR_NEG: |
398 |
16295 |
typeNode = ::cvc5::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check); |
399 |
16295 |
break; |
400 |
|
|
401 |
86874 |
case kind::BITVECTOR_ADD: |
402 |
86874 |
typeNode = ::cvc5::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check); |
403 |
86874 |
break; |
404 |
|
|
405 |
3000 |
case kind::BITVECTOR_SUB: |
406 |
3000 |
typeNode = ::cvc5::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check); |
407 |
3000 |
break; |
408 |
|
|
409 |
14978 |
case kind::BITVECTOR_UDIV: |
410 |
14978 |
typeNode = ::cvc5::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check); |
411 |
14978 |
break; |
412 |
|
|
413 |
15192 |
case kind::BITVECTOR_UREM: |
414 |
15192 |
typeNode = ::cvc5::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check); |
415 |
15192 |
break; |
416 |
|
|
417 |
141 |
case kind::BITVECTOR_SDIV: |
418 |
141 |
typeNode = ::cvc5::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check); |
419 |
141 |
break; |
420 |
|
|
421 |
58 |
case kind::BITVECTOR_SMOD: |
422 |
58 |
typeNode = ::cvc5::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check); |
423 |
58 |
break; |
424 |
|
|
425 |
73 |
case kind::BITVECTOR_SREM: |
426 |
73 |
typeNode = ::cvc5::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check); |
427 |
73 |
break; |
428 |
|
|
429 |
2751 |
case kind::BITVECTOR_ASHR: |
430 |
2751 |
typeNode = ::cvc5::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check); |
431 |
2751 |
break; |
432 |
|
|
433 |
18202 |
case kind::BITVECTOR_LSHR: |
434 |
18202 |
typeNode = ::cvc5::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check); |
435 |
18202 |
break; |
436 |
|
|
437 |
15789 |
case kind::BITVECTOR_SHL: |
438 |
15789 |
typeNode = ::cvc5::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check); |
439 |
15789 |
break; |
440 |
|
|
441 |
5584 |
case kind::BITVECTOR_ULE: |
442 |
5584 |
typeNode = ::cvc5::theory::bv::BitVectorPredicateTypeRule::computeType(nodeManager, n, check); |
443 |
5584 |
break; |
444 |
|
|
445 |
31225 |
case kind::BITVECTOR_ULT: |
446 |
31225 |
typeNode = ::cvc5::theory::bv::BitVectorPredicateTypeRule::computeType(nodeManager, n, check); |
447 |
31225 |
break; |
448 |
|
|
449 |
2764 |
case kind::BITVECTOR_UGE: |
450 |
2764 |
typeNode = ::cvc5::theory::bv::BitVectorPredicateTypeRule::computeType(nodeManager, n, check); |
451 |
2764 |
break; |
452 |
|
|
453 |
3294 |
case kind::BITVECTOR_UGT: |
454 |
3294 |
typeNode = ::cvc5::theory::bv::BitVectorPredicateTypeRule::computeType(nodeManager, n, check); |
455 |
3294 |
break; |
456 |
|
|
457 |
5813 |
case kind::BITVECTOR_SLE: |
458 |
5813 |
typeNode = ::cvc5::theory::bv::BitVectorPredicateTypeRule::computeType(nodeManager, n, check); |
459 |
5813 |
break; |
460 |
|
|
461 |
32195 |
case kind::BITVECTOR_SLT: |
462 |
32195 |
typeNode = ::cvc5::theory::bv::BitVectorPredicateTypeRule::computeType(nodeManager, n, check); |
463 |
32195 |
break; |
464 |
|
|
465 |
2780 |
case kind::BITVECTOR_SGE: |
466 |
2780 |
typeNode = ::cvc5::theory::bv::BitVectorPredicateTypeRule::computeType(nodeManager, n, check); |
467 |
2780 |
break; |
468 |
|
|
469 |
3279 |
case kind::BITVECTOR_SGT: |
470 |
3279 |
typeNode = ::cvc5::theory::bv::BitVectorPredicateTypeRule::computeType(nodeManager, n, check); |
471 |
3279 |
break; |
472 |
|
|
473 |
1548 |
case kind::BITVECTOR_ULTBV: |
474 |
1548 |
typeNode = ::cvc5::theory::bv::BitVectorBVPredTypeRule::computeType(nodeManager, n, check); |
475 |
1548 |
break; |
476 |
|
|
477 |
4648 |
case kind::BITVECTOR_SLTBV: |
478 |
4648 |
typeNode = ::cvc5::theory::bv::BitVectorBVPredTypeRule::computeType(nodeManager, n, check); |
479 |
4648 |
break; |
480 |
|
|
481 |
12712 |
case kind::BITVECTOR_ITE: |
482 |
12712 |
typeNode = ::cvc5::theory::bv::BitVectorITETypeRule::computeType(nodeManager, n, check); |
483 |
12712 |
break; |
484 |
|
|
485 |
|
case kind::BITVECTOR_REDAND: |
486 |
|
typeNode = ::cvc5::theory::bv::BitVectorUnaryPredicateTypeRule::computeType(nodeManager, n, check); |
487 |
|
break; |
488 |
|
|
489 |
|
case kind::BITVECTOR_REDOR: |
490 |
|
typeNode = ::cvc5::theory::bv::BitVectorUnaryPredicateTypeRule::computeType(nodeManager, n, check); |
491 |
|
break; |
492 |
|
|
493 |
558 |
case kind::BITVECTOR_TO_NAT: |
494 |
558 |
typeNode = ::cvc5::theory::bv::BitVectorConversionTypeRule::computeType(nodeManager, n, check); |
495 |
558 |
break; |
496 |
|
|
497 |
|
case kind::BITVECTOR_ACKERMANNIZE_UDIV: |
498 |
|
typeNode = ::cvc5::theory::bv::BitVectorAckermanizationUdivTypeRule::computeType(nodeManager, n, check); |
499 |
|
break; |
500 |
|
|
501 |
|
case kind::BITVECTOR_ACKERMANNIZE_UREM: |
502 |
|
typeNode = ::cvc5::theory::bv::BitVectorAckermanizationUremTypeRule::computeType(nodeManager, n, check); |
503 |
|
break; |
504 |
|
|
505 |
250 |
case kind::BITVECTOR_EAGER_ATOM: |
506 |
250 |
typeNode = ::cvc5::theory::bv::BitVectorEagerAtomTypeRule::computeType(nodeManager, n, check); |
507 |
250 |
break; |
508 |
|
|
509 |
|
case kind::BITVECTOR_BITOF_OP: |
510 |
|
typeNode = SimpleTypeRule<RBuiltinOperator>::computeType(nodeManager, n, check); |
511 |
|
break; |
512 |
|
|
513 |
190736 |
case kind::BITVECTOR_BITOF: |
514 |
190736 |
typeNode = ::cvc5::theory::bv::BitVectorBitOfTypeRule::computeType(nodeManager, n, check); |
515 |
190736 |
break; |
516 |
|
|
517 |
1611 |
case kind::BITVECTOR_EXTRACT_OP: |
518 |
1611 |
typeNode = SimpleTypeRule<RBuiltinOperator>::computeType(nodeManager, n, check); |
519 |
1611 |
break; |
520 |
|
|
521 |
107753 |
case kind::BITVECTOR_EXTRACT: |
522 |
107753 |
typeNode = ::cvc5::theory::bv::BitVectorExtractTypeRule::computeType(nodeManager, n, check); |
523 |
107753 |
break; |
524 |
|
|
525 |
199 |
case kind::BITVECTOR_REPEAT_OP: |
526 |
199 |
typeNode = SimpleTypeRule<RBuiltinOperator>::computeType(nodeManager, n, check); |
527 |
199 |
break; |
528 |
|
|
529 |
357 |
case kind::BITVECTOR_REPEAT: |
530 |
357 |
typeNode = ::cvc5::theory::bv::BitVectorRepeatTypeRule::computeType(nodeManager, n, check); |
531 |
356 |
break; |
532 |
|
|
533 |
154 |
case kind::BITVECTOR_ROTATE_LEFT_OP: |
534 |
154 |
typeNode = SimpleTypeRule<RBuiltinOperator>::computeType(nodeManager, n, check); |
535 |
154 |
break; |
536 |
|
|
537 |
301 |
case kind::BITVECTOR_ROTATE_LEFT: |
538 |
301 |
typeNode = ::cvc5::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check); |
539 |
301 |
break; |
540 |
|
|
541 |
187 |
case kind::BITVECTOR_ROTATE_RIGHT_OP: |
542 |
187 |
typeNode = SimpleTypeRule<RBuiltinOperator>::computeType(nodeManager, n, check); |
543 |
187 |
break; |
544 |
|
|
545 |
350 |
case kind::BITVECTOR_ROTATE_RIGHT: |
546 |
350 |
typeNode = ::cvc5::theory::bv::BitVectorFixedWidthTypeRule::computeType(nodeManager, n, check); |
547 |
350 |
break; |
548 |
|
|
549 |
1167 |
case kind::BITVECTOR_SIGN_EXTEND_OP: |
550 |
1167 |
typeNode = SimpleTypeRule<RBuiltinOperator>::computeType(nodeManager, n, check); |
551 |
1167 |
break; |
552 |
|
|
553 |
18640 |
case kind::BITVECTOR_SIGN_EXTEND: |
554 |
18640 |
typeNode = ::cvc5::theory::bv::BitVectorExtendTypeRule::computeType(nodeManager, n, check); |
555 |
18640 |
break; |
556 |
|
|
557 |
1216 |
case kind::BITVECTOR_ZERO_EXTEND_OP: |
558 |
1216 |
typeNode = SimpleTypeRule<RBuiltinOperator>::computeType(nodeManager, n, check); |
559 |
1216 |
break; |
560 |
|
|
561 |
8927 |
case kind::BITVECTOR_ZERO_EXTEND: |
562 |
8927 |
typeNode = ::cvc5::theory::bv::BitVectorExtendTypeRule::computeType(nodeManager, n, check); |
563 |
8927 |
break; |
564 |
|
|
565 |
31 |
case kind::INT_TO_BITVECTOR_OP: |
566 |
31 |
typeNode = ::cvc5::theory::bv::IntToBitVectorOpTypeRule::computeType(nodeManager, n, check); |
567 |
30 |
break; |
568 |
|
|
569 |
642 |
case kind::INT_TO_BITVECTOR: |
570 |
642 |
typeNode = ::cvc5::theory::bv::BitVectorConversionTypeRule::computeType(nodeManager, n, check); |
571 |
642 |
break; |
572 |
|
|
573 |
460 |
case kind::CONST_FLOATINGPOINT: |
574 |
460 |
typeNode = ::cvc5::theory::fp::FloatingPointConstantTypeRule::computeType(nodeManager, n, check); |
575 |
460 |
break; |
576 |
|
|
577 |
7979 |
case kind::CONST_ROUNDINGMODE: |
578 |
7979 |
typeNode = ::cvc5::theory::fp::RoundingModeConstantTypeRule::computeType(nodeManager, n, check); |
579 |
7979 |
break; |
580 |
|
|
581 |
24 |
case kind::FLOATINGPOINT_FP: |
582 |
24 |
typeNode = ::cvc5::theory::fp::FloatingPointFPTypeRule::computeType(nodeManager, n, check); |
583 |
24 |
break; |
584 |
|
|
585 |
8 |
case kind::FLOATINGPOINT_EQ: |
586 |
8 |
typeNode = ::cvc5::theory::fp::FloatingPointTestTypeRule::computeType(nodeManager, n, check); |
587 |
8 |
break; |
588 |
|
|
589 |
44 |
case kind::FLOATINGPOINT_ABS: |
590 |
44 |
typeNode = ::cvc5::theory::fp::FloatingPointOperationTypeRule::computeType(nodeManager, n, check); |
591 |
44 |
break; |
592 |
|
|
593 |
216 |
case kind::FLOATINGPOINT_NEG: |
594 |
216 |
typeNode = ::cvc5::theory::fp::FloatingPointOperationTypeRule::computeType(nodeManager, n, check); |
595 |
216 |
break; |
596 |
|
|
597 |
789 |
case kind::FLOATINGPOINT_ADD: |
598 |
789 |
typeNode = ::cvc5::theory::fp::FloatingPointRoundingOperationTypeRule::computeType(nodeManager, n, check); |
599 |
789 |
break; |
600 |
|
|
601 |
54 |
case kind::FLOATINGPOINT_SUB: |
602 |
54 |
typeNode = ::cvc5::theory::fp::FloatingPointRoundingOperationTypeRule::computeType(nodeManager, n, check); |
603 |
54 |
break; |
604 |
|
|
605 |
254 |
case kind::FLOATINGPOINT_MULT: |
606 |
254 |
typeNode = ::cvc5::theory::fp::FloatingPointRoundingOperationTypeRule::computeType(nodeManager, n, check); |
607 |
254 |
break; |
608 |
|
|
609 |
276 |
case kind::FLOATINGPOINT_DIV: |
610 |
276 |
typeNode = ::cvc5::theory::fp::FloatingPointRoundingOperationTypeRule::computeType(nodeManager, n, check); |
611 |
276 |
break; |
612 |
|
|
613 |
|
case kind::FLOATINGPOINT_FMA: |
614 |
|
typeNode = ::cvc5::theory::fp::FloatingPointRoundingOperationTypeRule::computeType(nodeManager, n, check); |
615 |
|
break; |
616 |
|
|
617 |
46 |
case kind::FLOATINGPOINT_SQRT: |
618 |
46 |
typeNode = ::cvc5::theory::fp::FloatingPointRoundingOperationTypeRule::computeType(nodeManager, n, check); |
619 |
46 |
break; |
620 |
|
|
621 |
166 |
case kind::FLOATINGPOINT_REM: |
622 |
166 |
typeNode = ::cvc5::theory::fp::FloatingPointOperationTypeRule::computeType(nodeManager, n, check); |
623 |
166 |
break; |
624 |
|
|
625 |
131 |
case kind::FLOATINGPOINT_RTI: |
626 |
131 |
typeNode = ::cvc5::theory::fp::FloatingPointRoundingOperationTypeRule::computeType(nodeManager, n, check); |
627 |
131 |
break; |
628 |
|
|
629 |
|
case kind::FLOATINGPOINT_MIN: |
630 |
|
typeNode = ::cvc5::theory::fp::FloatingPointOperationTypeRule::computeType(nodeManager, n, check); |
631 |
|
break; |
632 |
|
|
633 |
11 |
case kind::FLOATINGPOINT_MAX: |
634 |
11 |
typeNode = ::cvc5::theory::fp::FloatingPointOperationTypeRule::computeType(nodeManager, n, check); |
635 |
11 |
break; |
636 |
|
|
637 |
|
case kind::FLOATINGPOINT_MIN_TOTAL: |
638 |
|
typeNode = ::cvc5::theory::fp::FloatingPointPartialOperationTypeRule::computeType(nodeManager, n, check); |
639 |
|
break; |
640 |
|
|
641 |
163 |
case kind::FLOATINGPOINT_MAX_TOTAL: |
642 |
163 |
typeNode = ::cvc5::theory::fp::FloatingPointPartialOperationTypeRule::computeType(nodeManager, n, check); |
643 |
163 |
break; |
644 |
|
|
645 |
158 |
case kind::FLOATINGPOINT_LEQ: |
646 |
158 |
typeNode = ::cvc5::theory::fp::FloatingPointTestTypeRule::computeType(nodeManager, n, check); |
647 |
158 |
break; |
648 |
|
|
649 |
61 |
case kind::FLOATINGPOINT_LT: |
650 |
61 |
typeNode = ::cvc5::theory::fp::FloatingPointTestTypeRule::computeType(nodeManager, n, check); |
651 |
61 |
break; |
652 |
|
|
653 |
12 |
case kind::FLOATINGPOINT_GEQ: |
654 |
12 |
typeNode = ::cvc5::theory::fp::FloatingPointTestTypeRule::computeType(nodeManager, n, check); |
655 |
12 |
break; |
656 |
|
|
657 |
4 |
case kind::FLOATINGPOINT_GT: |
658 |
4 |
typeNode = ::cvc5::theory::fp::FloatingPointTestTypeRule::computeType(nodeManager, n, check); |
659 |
4 |
break; |
660 |
|
|
661 |
14 |
case kind::FLOATINGPOINT_ISN: |
662 |
14 |
typeNode = ::cvc5::theory::fp::FloatingPointTestTypeRule::computeType(nodeManager, n, check); |
663 |
14 |
break; |
664 |
|
|
665 |
16 |
case kind::FLOATINGPOINT_ISSN: |
666 |
16 |
typeNode = ::cvc5::theory::fp::FloatingPointTestTypeRule::computeType(nodeManager, n, check); |
667 |
16 |
break; |
668 |
|
|
669 |
207 |
case kind::FLOATINGPOINT_ISZ: |
670 |
207 |
typeNode = ::cvc5::theory::fp::FloatingPointTestTypeRule::computeType(nodeManager, n, check); |
671 |
207 |
break; |
672 |
|
|
673 |
52 |
case kind::FLOATINGPOINT_ISINF: |
674 |
52 |
typeNode = ::cvc5::theory::fp::FloatingPointTestTypeRule::computeType(nodeManager, n, check); |
675 |
52 |
break; |
676 |
|
|
677 |
73 |
case kind::FLOATINGPOINT_ISNAN: |
678 |
73 |
typeNode = ::cvc5::theory::fp::FloatingPointTestTypeRule::computeType(nodeManager, n, check); |
679 |
73 |
break; |
680 |
|
|
681 |
57 |
case kind::FLOATINGPOINT_ISNEG: |
682 |
57 |
typeNode = ::cvc5::theory::fp::FloatingPointTestTypeRule::computeType(nodeManager, n, check); |
683 |
57 |
break; |
684 |
|
|
685 |
15 |
case kind::FLOATINGPOINT_ISPOS: |
686 |
15 |
typeNode = ::cvc5::theory::fp::FloatingPointTestTypeRule::computeType(nodeManager, n, check); |
687 |
15 |
break; |
688 |
|
|
689 |
6 |
case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP: |
690 |
6 |
typeNode = ::cvc5::theory::fp::FloatingPointParametricOpTypeRule::computeType(nodeManager, n, check); |
691 |
6 |
break; |
692 |
|
|
693 |
409 |
case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: |
694 |
409 |
typeNode = ::cvc5::theory::fp::FloatingPointToFPIEEEBitVectorTypeRule::computeType(nodeManager, n, check); |
695 |
409 |
break; |
696 |
|
|
697 |
6 |
case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP: |
698 |
6 |
typeNode = ::cvc5::theory::fp::FloatingPointParametricOpTypeRule::computeType(nodeManager, n, check); |
699 |
6 |
break; |
700 |
|
|
701 |
18 |
case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT: |
702 |
18 |
typeNode = ::cvc5::theory::fp::FloatingPointToFPFloatingPointTypeRule::computeType(nodeManager, n, check); |
703 |
18 |
break; |
704 |
|
|
705 |
6 |
case kind::FLOATINGPOINT_TO_FP_REAL_OP: |
706 |
6 |
typeNode = ::cvc5::theory::fp::FloatingPointParametricOpTypeRule::computeType(nodeManager, n, check); |
707 |
6 |
break; |
708 |
|
|
709 |
25 |
case kind::FLOATINGPOINT_TO_FP_REAL: |
710 |
25 |
typeNode = ::cvc5::theory::fp::FloatingPointToFPRealTypeRule::computeType(nodeManager, n, check); |
711 |
25 |
break; |
712 |
|
|
713 |
6 |
case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP: |
714 |
6 |
typeNode = ::cvc5::theory::fp::FloatingPointParametricOpTypeRule::computeType(nodeManager, n, check); |
715 |
6 |
break; |
716 |
|
|
717 |
13 |
case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: |
718 |
13 |
typeNode = ::cvc5::theory::fp::FloatingPointToFPSignedBitVectorTypeRule::computeType(nodeManager, n, check); |
719 |
13 |
break; |
720 |
|
|
721 |
15 |
case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP: |
722 |
15 |
typeNode = ::cvc5::theory::fp::FloatingPointParametricOpTypeRule::computeType(nodeManager, n, check); |
723 |
15 |
break; |
724 |
|
|
725 |
60 |
case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: |
726 |
60 |
typeNode = ::cvc5::theory::fp::FloatingPointToFPUnsignedBitVectorTypeRule::computeType(nodeManager, n, check); |
727 |
60 |
break; |
728 |
|
|
729 |
33 |
case kind::FLOATINGPOINT_TO_FP_GENERIC_OP: |
730 |
33 |
typeNode = ::cvc5::theory::fp::FloatingPointParametricOpTypeRule::computeType(nodeManager, n, check); |
731 |
33 |
break; |
732 |
|
|
733 |
68 |
case kind::FLOATINGPOINT_TO_FP_GENERIC: |
734 |
68 |
typeNode = ::cvc5::theory::fp::FloatingPointToFPGenericTypeRule::computeType(nodeManager, n, check); |
735 |
68 |
break; |
736 |
|
|
737 |
6 |
case kind::FLOATINGPOINT_TO_UBV_OP: |
738 |
6 |
typeNode = ::cvc5::theory::fp::FloatingPointParametricOpTypeRule::computeType(nodeManager, n, check); |
739 |
6 |
break; |
740 |
|
|
741 |
|
case kind::FLOATINGPOINT_TO_UBV: |
742 |
|
typeNode = ::cvc5::theory::fp::FloatingPointToUBVTypeRule::computeType(nodeManager, n, check); |
743 |
|
break; |
744 |
|
|
745 |
|
case kind::FLOATINGPOINT_TO_UBV_TOTAL_OP: |
746 |
|
typeNode = ::cvc5::theory::fp::FloatingPointParametricOpTypeRule::computeType(nodeManager, n, check); |
747 |
|
break; |
748 |
|
|
749 |
|
case kind::FLOATINGPOINT_TO_UBV_TOTAL: |
750 |
|
typeNode = ::cvc5::theory::fp::FloatingPointToUBVTotalTypeRule::computeType(nodeManager, n, check); |
751 |
|
break; |
752 |
|
|
753 |
9 |
case kind::FLOATINGPOINT_TO_SBV_OP: |
754 |
9 |
typeNode = ::cvc5::theory::fp::FloatingPointParametricOpTypeRule::computeType(nodeManager, n, check); |
755 |
9 |
break; |
756 |
|
|
757 |
6 |
case kind::FLOATINGPOINT_TO_SBV: |
758 |
6 |
typeNode = ::cvc5::theory::fp::FloatingPointToSBVTypeRule::computeType(nodeManager, n, check); |
759 |
6 |
break; |
760 |
|
|
761 |
|
case kind::FLOATINGPOINT_TO_SBV_TOTAL_OP: |
762 |
|
typeNode = ::cvc5::theory::fp::FloatingPointParametricOpTypeRule::computeType(nodeManager, n, check); |
763 |
|
break; |
764 |
|
|
765 |
4 |
case kind::FLOATINGPOINT_TO_SBV_TOTAL: |
766 |
4 |
typeNode = ::cvc5::theory::fp::FloatingPointToSBVTotalTypeRule::computeType(nodeManager, n, check); |
767 |
4 |
break; |
768 |
|
|
769 |
6 |
case kind::FLOATINGPOINT_TO_REAL: |
770 |
6 |
typeNode = ::cvc5::theory::fp::FloatingPointToRealTypeRule::computeType(nodeManager, n, check); |
771 |
6 |
break; |
772 |
|
|
773 |
8 |
case kind::FLOATINGPOINT_TO_REAL_TOTAL: |
774 |
8 |
typeNode = ::cvc5::theory::fp::FloatingPointToRealTotalTypeRule::computeType(nodeManager, n, check); |
775 |
8 |
break; |
776 |
|
|
777 |
96 |
case kind::FLOATINGPOINT_COMPONENT_NAN: |
778 |
96 |
typeNode = ::cvc5::theory::fp::FloatingPointComponentBit::computeType(nodeManager, n, check); |
779 |
96 |
break; |
780 |
|
|
781 |
96 |
case kind::FLOATINGPOINT_COMPONENT_INF: |
782 |
96 |
typeNode = ::cvc5::theory::fp::FloatingPointComponentBit::computeType(nodeManager, n, check); |
783 |
96 |
break; |
784 |
|
|
785 |
96 |
case kind::FLOATINGPOINT_COMPONENT_ZERO: |
786 |
96 |
typeNode = ::cvc5::theory::fp::FloatingPointComponentBit::computeType(nodeManager, n, check); |
787 |
96 |
break; |
788 |
|
|
789 |
96 |
case kind::FLOATINGPOINT_COMPONENT_SIGN: |
790 |
96 |
typeNode = ::cvc5::theory::fp::FloatingPointComponentBit::computeType(nodeManager, n, check); |
791 |
96 |
break; |
792 |
|
|
793 |
96 |
case kind::FLOATINGPOINT_COMPONENT_EXPONENT: |
794 |
96 |
typeNode = ::cvc5::theory::fp::FloatingPointComponentExponent::computeType(nodeManager, n, check); |
795 |
96 |
break; |
796 |
|
|
797 |
96 |
case kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND: |
798 |
96 |
typeNode = ::cvc5::theory::fp::FloatingPointComponentSignificand::computeType(nodeManager, n, check); |
799 |
96 |
break; |
800 |
|
|
801 |
7 |
case kind::ROUNDINGMODE_BITBLAST: |
802 |
7 |
typeNode = ::cvc5::theory::fp::RoundingModeBitBlast::computeType(nodeManager, n, check); |
803 |
7 |
break; |
804 |
|
|
805 |
17707 |
case kind::SELECT: |
806 |
17707 |
typeNode = ::cvc5::theory::arrays::ArraySelectTypeRule::computeType(nodeManager, n, check); |
807 |
17707 |
break; |
808 |
|
|
809 |
10951 |
case kind::STORE: |
810 |
10951 |
typeNode = ::cvc5::theory::arrays::ArrayStoreTypeRule::computeType(nodeManager, n, check); |
811 |
10951 |
break; |
812 |
|
|
813 |
673 |
case kind::STORE_ALL: |
814 |
673 |
typeNode = ::cvc5::theory::arrays::ArrayStoreTypeRule::computeType(nodeManager, n, check); |
815 |
673 |
break; |
816 |
|
|
817 |
|
case kind::ARR_TABLE_FUN: |
818 |
|
typeNode = ::cvc5::theory::arrays::ArrayTableFunTypeRule::computeType(nodeManager, n, check); |
819 |
|
break; |
820 |
|
|
821 |
|
case kind::ARRAY_LAMBDA: |
822 |
|
typeNode = ::cvc5::theory::arrays::ArrayLambdaTypeRule::computeType(nodeManager, n, check); |
823 |
|
break; |
824 |
|
|
825 |
33 |
case kind::EQ_RANGE: |
826 |
33 |
typeNode = ::cvc5::theory::arrays::ArrayEqRangeTypeRule::computeType(nodeManager, n, check); |
827 |
33 |
break; |
828 |
|
|
829 |
|
case kind::PARTIAL_SELECT_0: |
830 |
|
typeNode = ::cvc5::theory::arrays::ArrayPartialSelectTypeRule::computeType(nodeManager, n, check); |
831 |
|
break; |
832 |
|
|
833 |
|
case kind::PARTIAL_SELECT_1: |
834 |
|
typeNode = ::cvc5::theory::arrays::ArrayPartialSelectTypeRule::computeType(nodeManager, n, check); |
835 |
|
break; |
836 |
|
|
837 |
133958 |
case kind::APPLY_CONSTRUCTOR: |
838 |
133958 |
typeNode = ::cvc5::theory::datatypes::DatatypeConstructorTypeRule::computeType(nodeManager, n, check); |
839 |
133953 |
break; |
840 |
|
|
841 |
28797 |
case kind::APPLY_SELECTOR: |
842 |
28797 |
typeNode = ::cvc5::theory::datatypes::DatatypeSelectorTypeRule::computeType(nodeManager, n, check); |
843 |
28797 |
break; |
844 |
|
|
845 |
35423 |
case kind::APPLY_SELECTOR_TOTAL: |
846 |
35423 |
typeNode = ::cvc5::theory::datatypes::DatatypeSelectorTypeRule::computeType(nodeManager, n, check); |
847 |
35423 |
break; |
848 |
|
|
849 |
26160 |
case kind::APPLY_TESTER: |
850 |
26160 |
typeNode = ::cvc5::theory::datatypes::DatatypeTesterTypeRule::computeType(nodeManager, n, check); |
851 |
26160 |
break; |
852 |
|
|
853 |
35 |
case kind::APPLY_UPDATER: |
854 |
35 |
typeNode = ::cvc5::theory::datatypes::DatatypeUpdateTypeRule::computeType(nodeManager, n, check); |
855 |
33 |
break; |
856 |
|
|
857 |
103 |
case kind::APPLY_TYPE_ASCRIPTION: |
858 |
103 |
typeNode = ::cvc5::theory::datatypes::DatatypeAscriptionTypeRule::computeType(nodeManager, n, check); |
859 |
103 |
break; |
860 |
|
|
861 |
11157 |
case kind::DT_SIZE: |
862 |
11157 |
typeNode = ::cvc5::theory::datatypes::DtSizeTypeRule::computeType(nodeManager, n, check); |
863 |
11157 |
break; |
864 |
|
|
865 |
|
case kind::DT_HEIGHT_BOUND: |
866 |
|
typeNode = ::cvc5::theory::datatypes::DtBoundTypeRule::computeType(nodeManager, n, check); |
867 |
|
break; |
868 |
|
|
869 |
|
case kind::DT_SIZE_BOUND: |
870 |
|
typeNode = ::cvc5::theory::datatypes::DtBoundTypeRule::computeType(nodeManager, n, check); |
871 |
|
break; |
872 |
|
|
873 |
474 |
case kind::DT_SYGUS_BOUND: |
874 |
474 |
typeNode = ::cvc5::theory::datatypes::DtSygusBoundTypeRule::computeType(nodeManager, n, check); |
875 |
474 |
break; |
876 |
|
|
877 |
90666 |
case kind::DT_SYGUS_EVAL: |
878 |
90666 |
typeNode = ::cvc5::theory::datatypes::DtSyguEvalTypeRule::computeType(nodeManager, n, check); |
879 |
90666 |
break; |
880 |
|
|
881 |
17 |
case kind::MATCH: |
882 |
17 |
typeNode = ::cvc5::theory::datatypes::MatchTypeRule::computeType(nodeManager, n, check); |
883 |
17 |
break; |
884 |
|
|
885 |
27 |
case kind::MATCH_CASE: |
886 |
27 |
typeNode = ::cvc5::theory::datatypes::MatchCaseTypeRule::computeType(nodeManager, n, check); |
887 |
27 |
break; |
888 |
|
|
889 |
12 |
case kind::MATCH_BIND_CASE: |
890 |
12 |
typeNode = ::cvc5::theory::datatypes::MatchBindCaseTypeRule::computeType(nodeManager, n, check); |
891 |
12 |
break; |
892 |
|
|
893 |
22 |
case kind::TUPLE_PROJECT_OP: |
894 |
22 |
typeNode = SimpleTypeRule<RBuiltinOperator>::computeType(nodeManager, n, check); |
895 |
22 |
break; |
896 |
|
|
897 |
20 |
case kind::TUPLE_PROJECT: |
898 |
20 |
typeNode = ::cvc5::theory::datatypes::TupleProjectTypeRule::computeType(nodeManager, n, check); |
899 |
16 |
break; |
900 |
|
|
901 |
51 |
case kind::SEP_EMP: |
902 |
51 |
typeNode = ::cvc5::theory::sep::SepEmpTypeRule::computeType(nodeManager, n, check); |
903 |
51 |
break; |
904 |
|
|
905 |
304 |
case kind::SEP_PTO: |
906 |
304 |
typeNode = ::cvc5::theory::sep::SepPtoTypeRule::computeType(nodeManager, n, check); |
907 |
304 |
break; |
908 |
|
|
909 |
210 |
case kind::SEP_STAR: |
910 |
210 |
typeNode = ::cvc5::theory::sep::SepStarTypeRule::computeType(nodeManager, n, check); |
911 |
210 |
break; |
912 |
|
|
913 |
30 |
case kind::SEP_WAND: |
914 |
30 |
typeNode = ::cvc5::theory::sep::SepWandTypeRule::computeType(nodeManager, n, check); |
915 |
30 |
break; |
916 |
|
|
917 |
891 |
case kind::SEP_LABEL: |
918 |
891 |
typeNode = ::cvc5::theory::sep::SepLabelTypeRule::computeType(nodeManager, n, check); |
919 |
891 |
break; |
920 |
|
|
921 |
1638 |
case kind::SEP_NIL: |
922 |
1638 |
typeNode = ::cvc5::theory::sep::SepNilTypeRule::computeType(nodeManager, n, check); |
923 |
1638 |
break; |
924 |
|
|
925 |
4853 |
case kind::UNION: |
926 |
4853 |
typeNode = ::cvc5::theory::sets::SetsBinaryOperatorTypeRule::computeType(nodeManager, n, check); |
927 |
4851 |
break; |
928 |
|
|
929 |
1386 |
case kind::INTERSECTION: |
930 |
1386 |
typeNode = ::cvc5::theory::sets::SetsBinaryOperatorTypeRule::computeType(nodeManager, n, check); |
931 |
1386 |
break; |
932 |
|
|
933 |
1173 |
case kind::SETMINUS: |
934 |
1173 |
typeNode = ::cvc5::theory::sets::SetsBinaryOperatorTypeRule::computeType(nodeManager, n, check); |
935 |
1173 |
break; |
936 |
|
|
937 |
370 |
case kind::SUBSET: |
938 |
370 |
typeNode = ::cvc5::theory::sets::SubsetTypeRule::computeType(nodeManager, n, check); |
939 |
370 |
break; |
940 |
|
|
941 |
23331 |
case kind::MEMBER: |
942 |
23331 |
typeNode = ::cvc5::theory::sets::MemberTypeRule::computeType(nodeManager, n, check); |
943 |
23331 |
break; |
944 |
|
|
945 |
|
case kind::SINGLETON_OP: |
946 |
|
typeNode = SimpleTypeRule<RBuiltinOperator>::computeType(nodeManager, n, check); |
947 |
|
break; |
948 |
|
|
949 |
3150 |
case kind::SINGLETON: |
950 |
3150 |
typeNode = ::cvc5::theory::sets::SingletonTypeRule::computeType(nodeManager, n, check); |
951 |
3150 |
break; |
952 |
|
|
953 |
1965 |
case kind::EMPTYSET: |
954 |
1965 |
typeNode = ::cvc5::theory::sets::EmptySetTypeRule::computeType(nodeManager, n, check); |
955 |
1965 |
break; |
956 |
|
|
957 |
31 |
case kind::INSERT: |
958 |
31 |
typeNode = ::cvc5::theory::sets::InsertTypeRule::computeType(nodeManager, n, check); |
959 |
31 |
break; |
960 |
|
|
961 |
2719 |
case kind::CARD: |
962 |
2719 |
typeNode = ::cvc5::theory::sets::CardTypeRule::computeType(nodeManager, n, check); |
963 |
2719 |
break; |
964 |
|
|
965 |
23 |
case kind::COMPLEMENT: |
966 |
23 |
typeNode = ::cvc5::theory::sets::ComplementTypeRule::computeType(nodeManager, n, check); |
967 |
23 |
break; |
968 |
|
|
969 |
134 |
case kind::UNIVERSE_SET: |
970 |
134 |
typeNode = ::cvc5::theory::sets::UniverseSetTypeRule::computeType(nodeManager, n, check); |
971 |
134 |
break; |
972 |
|
|
973 |
53 |
case kind::COMPREHENSION: |
974 |
53 |
typeNode = ::cvc5::theory::sets::ComprehensionTypeRule::computeType(nodeManager, n, check); |
975 |
53 |
break; |
976 |
|
|
977 |
18 |
case kind::CHOOSE: |
978 |
18 |
typeNode = ::cvc5::theory::sets::ChooseTypeRule::computeType(nodeManager, n, check); |
979 |
18 |
break; |
980 |
|
|
981 |
29 |
case kind::IS_SINGLETON: |
982 |
29 |
typeNode = ::cvc5::theory::sets::IsSingletonTypeRule::computeType(nodeManager, n, check); |
983 |
29 |
break; |
984 |
|
|
985 |
318 |
case kind::JOIN: |
986 |
318 |
typeNode = ::cvc5::theory::sets::RelBinaryOperatorTypeRule::computeType(nodeManager, n, check); |
987 |
318 |
break; |
988 |
|
|
989 |
47 |
case kind::PRODUCT: |
990 |
47 |
typeNode = ::cvc5::theory::sets::RelBinaryOperatorTypeRule::computeType(nodeManager, n, check); |
991 |
47 |
break; |
992 |
|
|
993 |
119 |
case kind::TRANSPOSE: |
994 |
119 |
typeNode = ::cvc5::theory::sets::RelTransposeTypeRule::computeType(nodeManager, n, check); |
995 |
119 |
break; |
996 |
|
|
997 |
44 |
case kind::TCLOSURE: |
998 |
44 |
typeNode = ::cvc5::theory::sets::RelTransClosureTypeRule::computeType(nodeManager, n, check); |
999 |
44 |
break; |
1000 |
|
|
1001 |
38 |
case kind::JOIN_IMAGE: |
1002 |
38 |
typeNode = ::cvc5::theory::sets::JoinImageTypeRule::computeType(nodeManager, n, check); |
1003 |
38 |
break; |
1004 |
|
|
1005 |
9 |
case kind::IDEN: |
1006 |
9 |
typeNode = ::cvc5::theory::sets::RelIdenTypeRule::computeType(nodeManager, n, check); |
1007 |
9 |
break; |
1008 |
|
|
1009 |
70 |
case kind::UNION_MAX: |
1010 |
70 |
typeNode = ::cvc5::theory::bags::BinaryOperatorTypeRule::computeType(nodeManager, n, check); |
1011 |
70 |
break; |
1012 |
|
|
1013 |
145 |
case kind::UNION_DISJOINT: |
1014 |
145 |
typeNode = ::cvc5::theory::bags::BinaryOperatorTypeRule::computeType(nodeManager, n, check); |
1015 |
145 |
break; |
1016 |
|
|
1017 |
42 |
case kind::INTERSECTION_MIN: |
1018 |
42 |
typeNode = ::cvc5::theory::bags::BinaryOperatorTypeRule::computeType(nodeManager, n, check); |
1019 |
42 |
break; |
1020 |
|
|
1021 |
35 |
case kind::DIFFERENCE_SUBTRACT: |
1022 |
35 |
typeNode = ::cvc5::theory::bags::BinaryOperatorTypeRule::computeType(nodeManager, n, check); |
1023 |
35 |
break; |
1024 |
|
|
1025 |
20 |
case kind::DIFFERENCE_REMOVE: |
1026 |
20 |
typeNode = ::cvc5::theory::bags::BinaryOperatorTypeRule::computeType(nodeManager, n, check); |
1027 |
20 |
break; |
1028 |
|
|
1029 |
10 |
case kind::SUBBAG: |
1030 |
10 |
typeNode = ::cvc5::theory::bags::SubBagTypeRule::computeType(nodeManager, n, check); |
1031 |
10 |
break; |
1032 |
|
|
1033 |
515 |
case kind::BAG_COUNT: |
1034 |
515 |
typeNode = ::cvc5::theory::bags::CountTypeRule::computeType(nodeManager, n, check); |
1035 |
513 |
break; |
1036 |
|
|
1037 |
16 |
case kind::DUPLICATE_REMOVAL: |
1038 |
16 |
typeNode = ::cvc5::theory::bags::DuplicateRemovalTypeRule::computeType(nodeManager, n, check); |
1039 |
16 |
break; |
1040 |
|
|
1041 |
|
case kind::MK_BAG_OP: |
1042 |
|
typeNode = SimpleTypeRule<RBuiltinOperator>::computeType(nodeManager, n, check); |
1043 |
|
break; |
1044 |
|
|
1045 |
257 |
case kind::MK_BAG: |
1046 |
257 |
typeNode = ::cvc5::theory::bags::MkBagTypeRule::computeType(nodeManager, n, check); |
1047 |
257 |
break; |
1048 |
|
|
1049 |
1592 |
case kind::EMPTYBAG: |
1050 |
1592 |
typeNode = ::cvc5::theory::bags::EmptyBagTypeRule::computeType(nodeManager, n, check); |
1051 |
1592 |
break; |
1052 |
|
|
1053 |
14 |
case kind::BAG_CARD: |
1054 |
14 |
typeNode = ::cvc5::theory::bags::CardTypeRule::computeType(nodeManager, n, check); |
1055 |
14 |
break; |
1056 |
|
|
1057 |
8 |
case kind::BAG_CHOOSE: |
1058 |
8 |
typeNode = ::cvc5::theory::bags::ChooseTypeRule::computeType(nodeManager, n, check); |
1059 |
8 |
break; |
1060 |
|
|
1061 |
10 |
case kind::BAG_IS_SINGLETON: |
1062 |
10 |
typeNode = ::cvc5::theory::bags::IsSingletonTypeRule::computeType(nodeManager, n, check); |
1063 |
10 |
break; |
1064 |
|
|
1065 |
10 |
case kind::BAG_FROM_SET: |
1066 |
10 |
typeNode = ::cvc5::theory::bags::FromSetTypeRule::computeType(nodeManager, n, check); |
1067 |
10 |
break; |
1068 |
|
|
1069 |
10 |
case kind::BAG_TO_SET: |
1070 |
10 |
typeNode = ::cvc5::theory::bags::ToSetTypeRule::computeType(nodeManager, n, check); |
1071 |
10 |
break; |
1072 |
|
|
1073 |
130 |
case kind::REGEXP_RV: |
1074 |
130 |
typeNode = SimpleTypeRule<RRegExp, AInteger>::computeType(nodeManager, n, check); |
1075 |
130 |
break; |
1076 |
|
|
1077 |
2095 |
case kind::REGEXP_CONCAT: |
1078 |
2095 |
typeNode = SimpleTypeRuleVar<RRegExp, ARegExp>::computeType(nodeManager, n, check); |
1079 |
2095 |
break; |
1080 |
|
|
1081 |
536 |
case kind::REGEXP_UNION: |
1082 |
536 |
typeNode = SimpleTypeRuleVar<RRegExp, ARegExp>::computeType(nodeManager, n, check); |
1083 |
536 |
break; |
1084 |
|
|
1085 |
118 |
case kind::REGEXP_INTER: |
1086 |
118 |
typeNode = SimpleTypeRuleVar<RRegExp, ARegExp>::computeType(nodeManager, n, check); |
1087 |
118 |
break; |
1088 |
|
|
1089 |
51 |
case kind::REGEXP_DIFF: |
1090 |
51 |
typeNode = SimpleTypeRuleVar<RRegExp, ARegExp>::computeType(nodeManager, n, check); |
1091 |
51 |
break; |
1092 |
|
|
1093 |
8028 |
case kind::REGEXP_STAR: |
1094 |
8028 |
typeNode = SimpleTypeRule<RRegExp, ARegExp>::computeType(nodeManager, n, check); |
1095 |
8028 |
break; |
1096 |
|
|
1097 |
47 |
case kind::REGEXP_PLUS: |
1098 |
47 |
typeNode = SimpleTypeRule<RRegExp, ARegExp>::computeType(nodeManager, n, check); |
1099 |
47 |
break; |
1100 |
|
|
1101 |
36 |
case kind::REGEXP_OPT: |
1102 |
36 |
typeNode = SimpleTypeRule<RRegExp, ARegExp>::computeType(nodeManager, n, check); |
1103 |
36 |
break; |
1104 |
|
|
1105 |
181 |
case kind::REGEXP_RANGE: |
1106 |
181 |
typeNode = ::cvc5::theory::strings::RegExpRangeTypeRule::computeType(nodeManager, n, check); |
1107 |
181 |
break; |
1108 |
|
|
1109 |
4 |
case kind::REGEXP_REPEAT_OP: |
1110 |
4 |
typeNode = SimpleTypeRule<RBuiltinOperator>::computeType(nodeManager, n, check); |
1111 |
4 |
break; |
1112 |
|
|
1113 |
6 |
case kind::REGEXP_REPEAT: |
1114 |
6 |
typeNode = SimpleTypeRule<RRegExp, ARegExp>::computeType(nodeManager, n, check); |
1115 |
6 |
break; |
1116 |
|
|
1117 |
23 |
case kind::REGEXP_LOOP_OP: |
1118 |
23 |
typeNode = SimpleTypeRule<RBuiltinOperator>::computeType(nodeManager, n, check); |
1119 |
23 |
break; |
1120 |
|
|
1121 |
27 |
case kind::REGEXP_LOOP: |
1122 |
27 |
typeNode = SimpleTypeRule<RRegExp, ARegExp>::computeType(nodeManager, n, check); |
1123 |
27 |
break; |
1124 |
|
|
1125 |
108 |
case kind::REGEXP_COMPLEMENT: |
1126 |
108 |
typeNode = SimpleTypeRule<RRegExp, ARegExp>::computeType(nodeManager, n, check); |
1127 |
108 |
break; |
1128 |
|
|
1129 |
8665 |
case kind::STRING_TO_REGEXP: |
1130 |
8665 |
typeNode = SimpleTypeRule<RRegExp, AString>::computeType(nodeManager, n, check); |
1131 |
8665 |
break; |
1132 |
|
|
1133 |
8856 |
case kind::STRING_IN_REGEXP: |
1134 |
8856 |
typeNode = SimpleTypeRule<RBool, AString, ARegExp>::computeType(nodeManager, n, check); |
1135 |
8856 |
break; |
1136 |
|
|
1137 |
7193 |
case kind::REGEXP_EMPTY: |
1138 |
7193 |
typeNode = SimpleTypeRule<RRegExp>::computeType(nodeManager, n, check); |
1139 |
7193 |
break; |
1140 |
|
|
1141 |
7193 |
case kind::REGEXP_SIGMA: |
1142 |
7193 |
typeNode = SimpleTypeRule<RRegExp>::computeType(nodeManager, n, check); |
1143 |
7193 |
break; |
1144 |
|
|
1145 |
45842 |
case kind::STRING_CONCAT: |
1146 |
45842 |
typeNode = ::cvc5::theory::strings::StringConcatTypeRule::computeType(nodeManager, n, check); |
1147 |
45842 |
break; |
1148 |
|
|
1149 |
116053 |
case kind::STRING_LENGTH: |
1150 |
116053 |
typeNode = ::cvc5::theory::strings::StringStrToIntTypeRule::computeType(nodeManager, n, check); |
1151 |
116053 |
break; |
1152 |
|
|
1153 |
37584 |
case kind::STRING_SUBSTR: |
1154 |
37584 |
typeNode = ::cvc5::theory::strings::StringSubstrTypeRule::computeType(nodeManager, n, check); |
1155 |
37584 |
break; |
1156 |
|
|
1157 |
136 |
case kind::STRING_UPDATE: |
1158 |
136 |
typeNode = ::cvc5::theory::strings::StringUpdateTypeRule::computeType(nodeManager, n, check); |
1159 |
136 |
break; |
1160 |
|
|
1161 |
131 |
case kind::STRING_CHARAT: |
1162 |
131 |
typeNode = ::cvc5::theory::strings::StringAtTypeRule::computeType(nodeManager, n, check); |
1163 |
131 |
break; |
1164 |
|
|
1165 |
31520 |
case kind::STRING_CONTAINS: |
1166 |
31520 |
typeNode = ::cvc5::theory::strings::StringRelationTypeRule::computeType(nodeManager, n, check); |
1167 |
31520 |
break; |
1168 |
|
|
1169 |
3555 |
case kind::STRING_INDEXOF: |
1170 |
3555 |
typeNode = ::cvc5::theory::strings::StringIndexOfTypeRule::computeType(nodeManager, n, check); |
1171 |
3555 |
break; |
1172 |
|
|
1173 |
574 |
case kind::STRING_INDEXOF_RE: |
1174 |
574 |
typeNode = SimpleTypeRule<RInteger, AString, ARegExp, AInteger>::computeType(nodeManager, n, check); |
1175 |
574 |
break; |
1176 |
|
|
1177 |
3042 |
case kind::STRING_REPLACE: |
1178 |
3042 |
typeNode = ::cvc5::theory::strings::StringReplaceTypeRule::computeType(nodeManager, n, check); |
1179 |
3042 |
break; |
1180 |
|
|
1181 |
119 |
case kind::STRING_REPLACE_ALL: |
1182 |
119 |
typeNode = ::cvc5::theory::strings::StringReplaceTypeRule::computeType(nodeManager, n, check); |
1183 |
119 |
break; |
1184 |
|
|
1185 |
233 |
case kind::STRING_REPLACE_RE: |
1186 |
233 |
typeNode = SimpleTypeRule<RString, AString, ARegExp, AString>::computeType(nodeManager, n, check); |
1187 |
233 |
break; |
1188 |
|
|
1189 |
134 |
case kind::STRING_REPLACE_RE_ALL: |
1190 |
134 |
typeNode = SimpleTypeRule<RString, AString, ARegExp, AString>::computeType(nodeManager, n, check); |
1191 |
134 |
break; |
1192 |
|
|
1193 |
139 |
case kind::STRING_PREFIX: |
1194 |
139 |
typeNode = ::cvc5::theory::strings::StringStrToBoolTypeRule::computeType(nodeManager, n, check); |
1195 |
139 |
break; |
1196 |
|
|
1197 |
42 |
case kind::STRING_SUFFIX: |
1198 |
42 |
typeNode = ::cvc5::theory::strings::StringStrToBoolTypeRule::computeType(nodeManager, n, check); |
1199 |
42 |
break; |
1200 |
|
|
1201 |
163 |
case kind::STRING_REV: |
1202 |
163 |
typeNode = ::cvc5::theory::strings::StringStrToStrTypeRule::computeType(nodeManager, n, check); |
1203 |
163 |
break; |
1204 |
|
|
1205 |
31878 |
case kind::CONST_STRING: |
1206 |
31878 |
typeNode = SimpleTypeRule<RString>::computeType(nodeManager, n, check); |
1207 |
31878 |
break; |
1208 |
|
|
1209 |
16 |
case kind::STRING_LT: |
1210 |
16 |
typeNode = SimpleTypeRule<RBool, AString, AString>::computeType(nodeManager, n, check); |
1211 |
16 |
break; |
1212 |
|
|
1213 |
234 |
case kind::STRING_LEQ: |
1214 |
234 |
typeNode = SimpleTypeRule<RBool, AString, AString>::computeType(nodeManager, n, check); |
1215 |
234 |
break; |
1216 |
|
|
1217 |
8 |
case kind::STRING_IS_DIGIT: |
1218 |
8 |
typeNode = SimpleTypeRule<RBool, AString>::computeType(nodeManager, n, check); |
1219 |
8 |
break; |
1220 |
|
|
1221 |
462 |
case kind::STRING_ITOS: |
1222 |
462 |
typeNode = SimpleTypeRule<RString, AInteger>::computeType(nodeManager, n, check); |
1223 |
462 |
break; |
1224 |
|
|
1225 |
312 |
case kind::STRING_STOI: |
1226 |
312 |
typeNode = SimpleTypeRule<RInteger, AString>::computeType(nodeManager, n, check); |
1227 |
312 |
break; |
1228 |
|
|
1229 |
3138 |
case kind::STRING_TO_CODE: |
1230 |
3138 |
typeNode = SimpleTypeRule<RInteger, AString>::computeType(nodeManager, n, check); |
1231 |
3138 |
break; |
1232 |
|
|
1233 |
58 |
case kind::STRING_FROM_CODE: |
1234 |
58 |
typeNode = SimpleTypeRule<RString, AInteger>::computeType(nodeManager, n, check); |
1235 |
58 |
break; |
1236 |
|
|
1237 |
42 |
case kind::STRING_TOUPPER: |
1238 |
42 |
typeNode = SimpleTypeRule<RString, AString>::computeType(nodeManager, n, check); |
1239 |
42 |
break; |
1240 |
|
|
1241 |
104 |
case kind::STRING_TOLOWER: |
1242 |
104 |
typeNode = SimpleTypeRule<RString, AString>::computeType(nodeManager, n, check); |
1243 |
104 |
break; |
1244 |
|
|
1245 |
429 |
case kind::CONST_SEQUENCE: |
1246 |
429 |
typeNode = ::cvc5::theory::strings::ConstSequenceTypeRule::computeType(nodeManager, n, check); |
1247 |
429 |
break; |
1248 |
|
|
1249 |
272 |
case kind::SEQ_UNIT: |
1250 |
272 |
typeNode = ::cvc5::theory::strings::SeqUnitTypeRule::computeType(nodeManager, n, check); |
1251 |
272 |
break; |
1252 |
|
|
1253 |
222 |
case kind::SEQ_NTH: |
1254 |
222 |
typeNode = ::cvc5::theory::strings::SeqNthTypeRule::computeType(nodeManager, n, check); |
1255 |
222 |
break; |
1256 |
|
|
1257 |
4 |
case kind::SEQ_NTH_TOTAL: |
1258 |
4 |
typeNode = ::cvc5::theory::strings::SeqNthTypeRule::computeType(nodeManager, n, check); |
1259 |
4 |
break; |
1260 |
|
|
1261 |
101248 |
case kind::FORALL: |
1262 |
101248 |
typeNode = ::cvc5::theory::quantifiers::QuantifierTypeRule::computeType(nodeManager, n, check); |
1263 |
101248 |
break; |
1264 |
|
|
1265 |
7487 |
case kind::EXISTS: |
1266 |
7487 |
typeNode = ::cvc5::theory::quantifiers::QuantifierTypeRule::computeType(nodeManager, n, check); |
1267 |
7487 |
break; |
1268 |
|
|
1269 |
64167 |
case kind::BOUND_VAR_LIST: |
1270 |
64167 |
typeNode = ::cvc5::theory::quantifiers::QuantifierBoundVarListTypeRule::computeType(nodeManager, n, check); |
1271 |
64167 |
break; |
1272 |
|
|
1273 |
10105 |
case kind::INST_PATTERN_LIST: |
1274 |
10105 |
typeNode = ::cvc5::theory::quantifiers::QuantifierInstPatternListTypeRule::computeType(nodeManager, n, check); |
1275 |
10105 |
break; |
1276 |
|
|
1277 |
9033 |
case kind::INST_PATTERN: |
1278 |
9033 |
typeNode = ::cvc5::theory::quantifiers::QuantifierInstPatternTypeRule::computeType(nodeManager, n, check); |
1279 |
9033 |
break; |
1280 |
|
|
1281 |
16 |
case kind::INST_NO_PATTERN: |
1282 |
16 |
typeNode = ::cvc5::theory::quantifiers::QuantifierAnnotationTypeRule::computeType(nodeManager, n, check); |
1283 |
16 |
break; |
1284 |
|
|
1285 |
1431 |
case kind::INST_ATTRIBUTE: |
1286 |
1431 |
typeNode = ::cvc5::theory::quantifiers::QuantifierAnnotationTypeRule::computeType(nodeManager, n, check); |
1287 |
1431 |
break; |
1288 |
|
|
1289 |
3 |
case kind::INST_POOL: |
1290 |
3 |
typeNode = ::cvc5::theory::quantifiers::QuantifierAnnotationTypeRule::computeType(nodeManager, n, check); |
1291 |
3 |
break; |
1292 |
|
|
1293 |
|
case kind::INST_ADD_TO_POOL: |
1294 |
|
typeNode = ::cvc5::theory::quantifiers::QuantifierAnnotationTypeRule::computeType(nodeManager, n, check); |
1295 |
|
break; |
1296 |
|
|
1297 |
20 |
case kind::SKOLEM_ADD_TO_POOL: |
1298 |
20 |
typeNode = ::cvc5::theory::quantifiers::QuantifierAnnotationTypeRule::computeType(nodeManager, n, check); |
1299 |
20 |
break; |
1300 |
|
|
1301 |
|
// clang-format on |
1302 |
|
|
1303 |
|
default: |
1304 |
|
Debug("getType") << "FAILURE" << std::endl; |
1305 |
|
Unhandled() << " " << n.getKind(); |
1306 |
|
} |
1307 |
|
|
1308 |
27338035 |
nodeManager->setAttribute(n, TypeAttr(), typeNode); |
1309 |
27338035 |
nodeManager->setAttribute(n, TypeCheckedAttr(), |
1310 |
54676070 |
check || nodeManager->getAttribute(n, TypeCheckedAttr())); |
1311 |
|
|
1312 |
27338035 |
return typeNode; |
1313 |
|
|
1314 |
|
}/* TypeChecker::computeType */ |
1315 |
|
|
1316 |
5099566 |
bool TypeChecker::computeIsConst(NodeManager* nodeManager, TNode n) |
1317 |
|
{ |
1318 |
5099566 |
Assert(n.getMetaKind() == kind::metakind::OPERATOR |
1319 |
|
|| n.getMetaKind() == kind::metakind::PARAMETERIZED |
1320 |
|
|| n.getMetaKind() == kind::metakind::NULLARY_OPERATOR); |
1321 |
|
|
1322 |
5099566 |
switch (n.getKind()) |
1323 |
|
{ |
1324 |
|
// clang-format off |
1325 |
|
|
1326 |
1712 |
case kind::LAMBDA: |
1327 |
1712 |
return ::cvc5::theory::builtin::LambdaTypeRule::computeIsConst(nodeManager, n); |
1328 |
|
|
1329 |
8307 |
case kind::STORE: |
1330 |
8307 |
return ::cvc5::theory::arrays::ArrayStoreTypeRule::computeIsConst(nodeManager, n); |
1331 |
|
|
1332 |
74151 |
case kind::APPLY_CONSTRUCTOR: |
1333 |
74151 |
return ::cvc5::theory::datatypes::DatatypeConstructorTypeRule::computeIsConst(nodeManager, n); |
1334 |
|
|
1335 |
4233 |
case kind::UNION: |
1336 |
4233 |
return ::cvc5::theory::sets::SetsBinaryOperatorTypeRule::computeIsConst(nodeManager, n); |
1337 |
|
|
1338 |
2941 |
case kind::SINGLETON: |
1339 |
2941 |
return ::cvc5::theory::sets::SingletonTypeRule::computeIsConst(nodeManager, n); |
1340 |
|
|
1341 |
117 |
case kind::UNION_DISJOINT: |
1342 |
117 |
return ::cvc5::theory::bags::BinaryOperatorTypeRule::computeIsConst(nodeManager, n); |
1343 |
|
|
1344 |
204 |
case kind::MK_BAG: |
1345 |
204 |
return ::cvc5::theory::bags::MkBagTypeRule::computeIsConst(nodeManager, n); |
1346 |
|
|
1347 |
|
// clang-format on |
1348 |
|
|
1349 |
5007901 |
default:; |
1350 |
|
} |
1351 |
|
|
1352 |
5007901 |
return false; |
1353 |
|
|
1354 |
|
}/* TypeChecker::computeIsConst */ |
1355 |
|
|
1356 |
|
} // namespace expr |
1357 |
29337 |
} // namespace cvc5 |