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