1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Aina Niemetz, Martin Brain, Tim King |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Type rules for the theory of floating-point arithmetic. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/fp/theory_fp_type_rules.h" |
17 |
|
|
18 |
|
// This is only needed for checking that components are only applied to leaves. |
19 |
|
#include "theory/theory.h" |
20 |
|
#include "util/roundingmode.h" |
21 |
|
|
22 |
|
namespace cvc5 { |
23 |
|
namespace theory { |
24 |
|
namespace fp { |
25 |
|
|
26 |
|
#define TRACE(FUNCTION) \ |
27 |
|
Trace("fp-type") << FUNCTION "::computeType(" << check << "): " << n \ |
28 |
|
<< std::endl |
29 |
|
|
30 |
481 |
TypeNode FloatingPointConstantTypeRule::computeType(NodeManager* nodeManager, |
31 |
|
TNode n, |
32 |
|
bool check) |
33 |
|
{ |
34 |
481 |
TRACE("FloatingPointConstantTypeRule"); |
35 |
|
|
36 |
481 |
const FloatingPoint& f = n.getConst<FloatingPoint>(); |
37 |
|
|
38 |
481 |
if (check) |
39 |
|
{ |
40 |
315 |
if (!(validExponentSize(f.getSize().exponentWidth()))) |
41 |
|
{ |
42 |
|
throw TypeCheckingExceptionPrivate(n, |
43 |
|
"constant with invalid exponent size"); |
44 |
|
} |
45 |
315 |
if (!(validSignificandSize(f.getSize().significandWidth()))) |
46 |
|
{ |
47 |
|
throw TypeCheckingExceptionPrivate( |
48 |
|
n, "constant with invalid significand size"); |
49 |
|
} |
50 |
|
} |
51 |
481 |
return nodeManager->mkFloatingPointType(f.getSize()); |
52 |
|
} |
53 |
|
|
54 |
7259 |
TypeNode RoundingModeConstantTypeRule::computeType(NodeManager* nodeManager, |
55 |
|
TNode n, |
56 |
|
bool check) |
57 |
|
{ |
58 |
7259 |
TRACE("RoundingModeConstantTypeRule"); |
59 |
|
|
60 |
|
// Nothing to check! |
61 |
7259 |
return nodeManager->roundingModeType(); |
62 |
|
} |
63 |
|
|
64 |
24 |
TypeNode FloatingPointFPTypeRule::computeType(NodeManager* nodeManager, |
65 |
|
TNode n, |
66 |
|
bool check) |
67 |
|
{ |
68 |
24 |
TRACE("FloatingPointFPTypeRule"); |
69 |
|
|
70 |
48 |
TypeNode signType = n[0].getType(check); |
71 |
48 |
TypeNode exponentType = n[1].getType(check); |
72 |
48 |
TypeNode significandType = n[2].getType(check); |
73 |
|
|
74 |
72 |
if (!signType.isBitVector() || !exponentType.isBitVector() |
75 |
48 |
|| !significandType.isBitVector()) |
76 |
|
{ |
77 |
|
throw TypeCheckingExceptionPrivate(n, |
78 |
|
"arguments to fp must be bit vectors"); |
79 |
|
} |
80 |
|
|
81 |
24 |
uint32_t signBits = signType.getBitVectorSize(); |
82 |
24 |
uint32_t exponentBits = exponentType.getBitVectorSize(); |
83 |
24 |
uint32_t significandBits = significandType.getBitVectorSize(); |
84 |
|
|
85 |
24 |
if (check) |
86 |
|
{ |
87 |
24 |
if (signBits != 1) |
88 |
|
{ |
89 |
|
throw TypeCheckingExceptionPrivate( |
90 |
|
n, "sign bit vector in fp must be 1 bit long"); |
91 |
|
} |
92 |
24 |
else if (!(validExponentSize(exponentBits))) |
93 |
|
{ |
94 |
|
throw TypeCheckingExceptionPrivate( |
95 |
|
n, "exponent bit vector in fp is an invalid size"); |
96 |
|
} |
97 |
24 |
else if (!(validSignificandSize(significandBits))) |
98 |
|
{ |
99 |
|
throw TypeCheckingExceptionPrivate( |
100 |
|
n, "significand bit vector in fp is an invalid size"); |
101 |
|
} |
102 |
|
} |
103 |
|
|
104 |
|
// The +1 is for the implicit hidden bit |
105 |
48 |
return nodeManager->mkFloatingPointType(exponentBits, significandBits + 1); |
106 |
|
} |
107 |
|
|
108 |
700 |
TypeNode FloatingPointTestTypeRule::computeType(NodeManager* nodeManager, |
109 |
|
TNode n, |
110 |
|
bool check) |
111 |
|
{ |
112 |
700 |
TRACE("FloatingPointTestTypeRule"); |
113 |
|
|
114 |
700 |
if (check) |
115 |
|
{ |
116 |
1400 |
TypeNode firstOperand = n[0].getType(check); |
117 |
|
|
118 |
700 |
if (!firstOperand.isFloatingPoint()) |
119 |
|
{ |
120 |
|
throw TypeCheckingExceptionPrivate( |
121 |
|
n, "floating-point test applied to a non floating-point sort"); |
122 |
|
} |
123 |
|
|
124 |
700 |
size_t children = n.getNumChildren(); |
125 |
966 |
for (size_t i = 1; i < children; ++i) |
126 |
|
{ |
127 |
266 |
if (!(n[i].getType(check) == firstOperand)) |
128 |
|
{ |
129 |
|
throw TypeCheckingExceptionPrivate( |
130 |
|
n, "floating-point test applied to mixed sorts"); |
131 |
|
} |
132 |
|
} |
133 |
|
} |
134 |
|
|
135 |
700 |
return nodeManager->booleanType(); |
136 |
|
} |
137 |
|
|
138 |
410 |
TypeNode FloatingPointOperationTypeRule::computeType(NodeManager* nodeManager, |
139 |
|
TNode n, |
140 |
|
bool check) |
141 |
|
{ |
142 |
410 |
TRACE("FloatingPointOperationTypeRule"); |
143 |
|
|
144 |
410 |
TypeNode firstOperand = n[0].getType(check); |
145 |
|
|
146 |
410 |
if (check) |
147 |
|
{ |
148 |
410 |
if (!firstOperand.isFloatingPoint()) |
149 |
|
{ |
150 |
|
throw TypeCheckingExceptionPrivate( |
151 |
|
n, "floating-point operation applied to a non floating-point sort"); |
152 |
|
} |
153 |
|
|
154 |
410 |
size_t children = n.getNumChildren(); |
155 |
574 |
for (size_t i = 1; i < children; ++i) |
156 |
|
{ |
157 |
164 |
if (!(n[i].getType(check) == firstOperand)) |
158 |
|
{ |
159 |
|
throw TypeCheckingExceptionPrivate( |
160 |
|
n, "floating-point test applied to mixed sorts"); |
161 |
|
} |
162 |
|
} |
163 |
|
} |
164 |
|
|
165 |
410 |
return firstOperand; |
166 |
|
} |
167 |
|
|
168 |
1469 |
TypeNode FloatingPointRoundingOperationTypeRule::computeType( |
169 |
|
NodeManager* nodeManager, TNode n, bool check) |
170 |
|
{ |
171 |
1469 |
TRACE("FloatingPointRoundingOperationTypeRule"); |
172 |
|
|
173 |
1469 |
if (check) |
174 |
|
{ |
175 |
2938 |
TypeNode roundingModeType = n[0].getType(check); |
176 |
|
|
177 |
1469 |
if (!roundingModeType.isRoundingMode()) |
178 |
|
{ |
179 |
|
throw TypeCheckingExceptionPrivate( |
180 |
|
n, "first argument must be a rounding mode"); |
181 |
|
} |
182 |
|
} |
183 |
|
|
184 |
1469 |
TypeNode firstOperand = n[1].getType(check); |
185 |
|
|
186 |
1469 |
if (check) |
187 |
|
{ |
188 |
1469 |
if (!firstOperand.isFloatingPoint()) |
189 |
|
{ |
190 |
|
throw TypeCheckingExceptionPrivate( |
191 |
|
n, "floating-point operation applied to a non floating-point sort"); |
192 |
|
} |
193 |
|
|
194 |
1469 |
size_t children = n.getNumChildren(); |
195 |
2765 |
for (size_t i = 2; i < children; ++i) |
196 |
|
{ |
197 |
1296 |
if (!(n[i].getType(check) == firstOperand)) |
198 |
|
{ |
199 |
|
throw TypeCheckingExceptionPrivate( |
200 |
|
n, "floating-point operation applied to mixed sorts"); |
201 |
|
} |
202 |
|
} |
203 |
|
} |
204 |
|
|
205 |
1469 |
return firstOperand; |
206 |
|
} |
207 |
|
|
208 |
163 |
TypeNode FloatingPointPartialOperationTypeRule::computeType( |
209 |
|
NodeManager* nodeManager, TNode n, bool check) |
210 |
|
{ |
211 |
163 |
TRACE("FloatingPointOperationTypeRule"); |
212 |
163 |
AlwaysAssert(n.getNumChildren() > 0); |
213 |
|
|
214 |
163 |
TypeNode firstOperand = n[0].getType(check); |
215 |
|
|
216 |
163 |
if (check) |
217 |
|
{ |
218 |
163 |
if (!firstOperand.isFloatingPoint()) |
219 |
|
{ |
220 |
|
throw TypeCheckingExceptionPrivate( |
221 |
|
n, "floating-point operation applied to a non floating-point sort"); |
222 |
|
} |
223 |
|
|
224 |
163 |
const size_t children = n.getNumChildren(); |
225 |
326 |
for (size_t i = 1; i < children - 1; ++i) |
226 |
|
{ |
227 |
163 |
if (n[i].getType(check) != firstOperand) |
228 |
|
{ |
229 |
|
throw TypeCheckingExceptionPrivate( |
230 |
|
n, "floating-point partial operation applied to mixed sorts"); |
231 |
|
} |
232 |
|
} |
233 |
|
|
234 |
326 |
TypeNode UFValueType = n[children - 1].getType(check); |
235 |
|
|
236 |
163 |
if (!(UFValueType.isBitVector()) || !(UFValueType.getBitVectorSize() == 1)) |
237 |
|
{ |
238 |
|
throw TypeCheckingExceptionPrivate( |
239 |
|
n, |
240 |
|
"floating-point partial operation final argument must be a " |
241 |
|
"bit-vector of length 1"); |
242 |
|
} |
243 |
|
} |
244 |
|
|
245 |
163 |
return firstOperand; |
246 |
|
} |
247 |
|
|
248 |
65 |
TypeNode FloatingPointParametricOpTypeRule::computeType( |
249 |
|
NodeManager* nodeManager, TNode n, bool check) |
250 |
|
{ |
251 |
65 |
TRACE("FloatingPointParametricOpTypeRule"); |
252 |
|
|
253 |
65 |
return nodeManager->builtinOperatorType(); |
254 |
|
} |
255 |
|
|
256 |
418 |
TypeNode FloatingPointToFPIEEEBitVectorTypeRule::computeType( |
257 |
|
NodeManager* nodeManager, TNode n, bool check) |
258 |
|
{ |
259 |
418 |
TRACE("FloatingPointToFPIEEEBitVectorTypeRule"); |
260 |
418 |
AlwaysAssert(n.getNumChildren() == 1); |
261 |
|
|
262 |
|
FloatingPointToFPIEEEBitVector info = |
263 |
418 |
n.getOperator().getConst<FloatingPointToFPIEEEBitVector>(); |
264 |
|
|
265 |
418 |
if (check) |
266 |
|
{ |
267 |
836 |
TypeNode operandType = n[0].getType(check); |
268 |
|
|
269 |
418 |
if (!(operandType.isBitVector())) |
270 |
|
{ |
271 |
|
throw TypeCheckingExceptionPrivate(n, |
272 |
|
"conversion to floating-point from " |
273 |
|
"bit vector used with sort other " |
274 |
|
"than bit vector"); |
275 |
|
} |
276 |
1254 |
else if (!(operandType.getBitVectorSize() |
277 |
836 |
== info.getSize().exponentWidth() |
278 |
836 |
+ info.getSize().significandWidth())) |
279 |
|
{ |
280 |
|
throw TypeCheckingExceptionPrivate( |
281 |
|
n, |
282 |
|
"conversion to floating-point from bit vector used with bit vector " |
283 |
|
"length that does not match floating point parameters"); |
284 |
|
} |
285 |
|
} |
286 |
|
|
287 |
418 |
return nodeManager->mkFloatingPointType(info.getSize()); |
288 |
|
} |
289 |
|
|
290 |
18 |
TypeNode FloatingPointToFPFloatingPointTypeRule::computeType( |
291 |
|
NodeManager* nodeManager, TNode n, bool check) |
292 |
|
{ |
293 |
18 |
TRACE("FloatingPointToFPFloatingPointTypeRule"); |
294 |
18 |
AlwaysAssert(n.getNumChildren() == 2); |
295 |
|
|
296 |
|
FloatingPointToFPFloatingPoint info = |
297 |
18 |
n.getOperator().getConst<FloatingPointToFPFloatingPoint>(); |
298 |
|
|
299 |
18 |
if (check) |
300 |
|
{ |
301 |
36 |
TypeNode roundingModeType = n[0].getType(check); |
302 |
|
|
303 |
18 |
if (!roundingModeType.isRoundingMode()) |
304 |
|
{ |
305 |
|
throw TypeCheckingExceptionPrivate( |
306 |
|
n, "first argument must be a rounding mode"); |
307 |
|
} |
308 |
|
|
309 |
36 |
TypeNode operandType = n[1].getType(check); |
310 |
|
|
311 |
18 |
if (!(operandType.isFloatingPoint())) |
312 |
|
{ |
313 |
|
throw TypeCheckingExceptionPrivate(n, |
314 |
|
"conversion to floating-point from " |
315 |
|
"floating-point used with sort " |
316 |
|
"other than floating-point"); |
317 |
|
} |
318 |
|
} |
319 |
|
|
320 |
18 |
return nodeManager->mkFloatingPointType(info.getSize()); |
321 |
|
} |
322 |
|
|
323 |
33 |
TypeNode FloatingPointToFPRealTypeRule::computeType(NodeManager* nodeManager, |
324 |
|
TNode n, |
325 |
|
bool check) |
326 |
|
{ |
327 |
33 |
TRACE("FloatingPointToFPRealTypeRule"); |
328 |
33 |
AlwaysAssert(n.getNumChildren() == 2); |
329 |
|
|
330 |
|
FloatingPointToFPReal info = |
331 |
33 |
n.getOperator().getConst<FloatingPointToFPReal>(); |
332 |
|
|
333 |
33 |
if (check) |
334 |
|
{ |
335 |
66 |
TypeNode roundingModeType = n[0].getType(check); |
336 |
|
|
337 |
33 |
if (!roundingModeType.isRoundingMode()) |
338 |
|
{ |
339 |
|
throw TypeCheckingExceptionPrivate( |
340 |
|
n, "first argument must be a rounding mode"); |
341 |
|
} |
342 |
|
|
343 |
66 |
TypeNode operandType = n[1].getType(check); |
344 |
|
|
345 |
33 |
if (!(operandType.isReal())) |
346 |
|
{ |
347 |
|
throw TypeCheckingExceptionPrivate(n, |
348 |
|
"conversion to floating-point from " |
349 |
|
"real used with sort other than " |
350 |
|
"real"); |
351 |
|
} |
352 |
|
} |
353 |
|
|
354 |
33 |
return nodeManager->mkFloatingPointType(info.getSize()); |
355 |
|
} |
356 |
|
|
357 |
13 |
TypeNode FloatingPointToFPSignedBitVectorTypeRule::computeType( |
358 |
|
NodeManager* nodeManager, TNode n, bool check) |
359 |
|
{ |
360 |
13 |
TRACE("FloatingPointToFPSignedBitVectorTypeRule"); |
361 |
13 |
AlwaysAssert(n.getNumChildren() == 2); |
362 |
|
|
363 |
|
FloatingPointToFPSignedBitVector info = |
364 |
13 |
n.getOperator().getConst<FloatingPointToFPSignedBitVector>(); |
365 |
|
|
366 |
13 |
if (check) |
367 |
|
{ |
368 |
26 |
TypeNode roundingModeType = n[0].getType(check); |
369 |
|
|
370 |
13 |
if (!roundingModeType.isRoundingMode()) |
371 |
|
{ |
372 |
|
throw TypeCheckingExceptionPrivate( |
373 |
|
n, "first argument must be a rounding mode"); |
374 |
|
} |
375 |
|
|
376 |
26 |
TypeNode operandType = n[1].getType(check); |
377 |
|
|
378 |
13 |
if (!(operandType.isBitVector())) |
379 |
|
{ |
380 |
|
throw TypeCheckingExceptionPrivate(n, |
381 |
|
"conversion to floating-point from " |
382 |
|
"signed bit vector used with sort " |
383 |
|
"other than bit vector"); |
384 |
|
} |
385 |
|
} |
386 |
|
|
387 |
13 |
return nodeManager->mkFloatingPointType(info.getSize()); |
388 |
|
} |
389 |
|
|
390 |
60 |
TypeNode FloatingPointToFPUnsignedBitVectorTypeRule::computeType( |
391 |
|
NodeManager* nodeManager, TNode n, bool check) |
392 |
|
{ |
393 |
60 |
TRACE("FloatingPointToFPUnsignedBitVectorTypeRule"); |
394 |
60 |
AlwaysAssert(n.getNumChildren() == 2); |
395 |
|
|
396 |
|
FloatingPointToFPUnsignedBitVector info = |
397 |
60 |
n.getOperator().getConst<FloatingPointToFPUnsignedBitVector>(); |
398 |
|
|
399 |
60 |
if (check) |
400 |
|
{ |
401 |
120 |
TypeNode roundingModeType = n[0].getType(check); |
402 |
|
|
403 |
60 |
if (!roundingModeType.isRoundingMode()) |
404 |
|
{ |
405 |
|
throw TypeCheckingExceptionPrivate( |
406 |
|
n, "first argument must be a rounding mode"); |
407 |
|
} |
408 |
|
|
409 |
120 |
TypeNode operandType = n[1].getType(check); |
410 |
|
|
411 |
60 |
if (!(operandType.isBitVector())) |
412 |
|
{ |
413 |
|
throw TypeCheckingExceptionPrivate(n, |
414 |
|
"conversion to floating-point from " |
415 |
|
"unsigned bit vector used with sort " |
416 |
|
"other than bit vector"); |
417 |
|
} |
418 |
|
} |
419 |
|
|
420 |
60 |
return nodeManager->mkFloatingPointType(info.getSize()); |
421 |
|
} |
422 |
|
|
423 |
59 |
TypeNode FloatingPointToFPGenericTypeRule::computeType(NodeManager* nodeManager, |
424 |
|
TNode n, |
425 |
|
bool check) |
426 |
|
{ |
427 |
59 |
TRACE("FloatingPointToFPGenericTypeRule"); |
428 |
|
|
429 |
|
FloatingPointToFPGeneric info = |
430 |
59 |
n.getOperator().getConst<FloatingPointToFPGeneric>(); |
431 |
|
|
432 |
59 |
if (check) |
433 |
|
{ |
434 |
59 |
uint32_t nchildren = n.getNumChildren(); |
435 |
59 |
if (nchildren == 1) |
436 |
|
{ |
437 |
18 |
if (!n[0].getType(check).isBitVector()) |
438 |
|
{ |
439 |
|
throw TypeCheckingExceptionPrivate( |
440 |
|
n, "first argument must be a bit-vector"); |
441 |
|
} |
442 |
|
} |
443 |
|
else |
444 |
|
{ |
445 |
41 |
Assert(nchildren == 2); |
446 |
41 |
if (!n[0].getType(check).isRoundingMode()) |
447 |
|
{ |
448 |
|
throw TypeCheckingExceptionPrivate( |
449 |
|
n, "first argument must be a roundingmode"); |
450 |
|
} |
451 |
82 |
TypeNode tn = n[1].getType(check); |
452 |
41 |
if (!tn.isBitVector() && !tn.isFloatingPoint() && !tn.isReal()) |
453 |
|
{ |
454 |
|
throw TypeCheckingExceptionPrivate( |
455 |
|
n, "second argument must be a bit-vector, floating-point or Real"); |
456 |
|
} |
457 |
|
} |
458 |
|
} |
459 |
59 |
return nodeManager->mkFloatingPointType(info.getSize()); |
460 |
|
} |
461 |
|
|
462 |
|
TypeNode FloatingPointToUBVTypeRule::computeType(NodeManager* nodeManager, |
463 |
|
TNode n, |
464 |
|
bool check) |
465 |
|
{ |
466 |
|
TRACE("FloatingPointToUBVTypeRule"); |
467 |
|
AlwaysAssert(n.getNumChildren() == 2); |
468 |
|
|
469 |
|
FloatingPointToUBV info = n.getOperator().getConst<FloatingPointToUBV>(); |
470 |
|
|
471 |
|
if (check) |
472 |
|
{ |
473 |
|
TypeNode roundingModeType = n[0].getType(check); |
474 |
|
|
475 |
|
if (!roundingModeType.isRoundingMode()) |
476 |
|
{ |
477 |
|
throw TypeCheckingExceptionPrivate( |
478 |
|
n, "first argument must be a rounding mode"); |
479 |
|
} |
480 |
|
|
481 |
|
TypeNode operandType = n[1].getType(check); |
482 |
|
|
483 |
|
if (!(operandType.isFloatingPoint())) |
484 |
|
{ |
485 |
|
throw TypeCheckingExceptionPrivate(n, |
486 |
|
"conversion to unsigned bit vector " |
487 |
|
"used with a sort other than " |
488 |
|
"floating-point"); |
489 |
|
} |
490 |
|
} |
491 |
|
|
492 |
|
return nodeManager->mkBitVectorType(info.d_bv_size); |
493 |
|
} |
494 |
|
|
495 |
|
TypeNode FloatingPointToSBVTypeRule::computeType(NodeManager* nodeManager, |
496 |
|
TNode n, |
497 |
|
bool check) |
498 |
|
{ |
499 |
|
TRACE("FloatingPointToSBVTypeRule"); |
500 |
|
AlwaysAssert(n.getNumChildren() == 2); |
501 |
|
|
502 |
|
FloatingPointToSBV info = n.getOperator().getConst<FloatingPointToSBV>(); |
503 |
|
|
504 |
|
if (check) |
505 |
|
{ |
506 |
|
TypeNode roundingModeType = n[0].getType(check); |
507 |
|
|
508 |
|
if (!roundingModeType.isRoundingMode()) |
509 |
|
{ |
510 |
|
throw TypeCheckingExceptionPrivate( |
511 |
|
n, "first argument must be a rounding mode"); |
512 |
|
} |
513 |
|
|
514 |
|
TypeNode operandType = n[1].getType(check); |
515 |
|
|
516 |
|
if (!(operandType.isFloatingPoint())) |
517 |
|
{ |
518 |
|
throw TypeCheckingExceptionPrivate(n, |
519 |
|
"conversion to signed bit vector " |
520 |
|
"used with a sort other than " |
521 |
|
"floating-point"); |
522 |
|
} |
523 |
|
} |
524 |
|
|
525 |
|
return nodeManager->mkBitVectorType(info.d_bv_size); |
526 |
|
} |
527 |
|
|
528 |
|
TypeNode FloatingPointToUBVTotalTypeRule::computeType(NodeManager* nodeManager, |
529 |
|
TNode n, |
530 |
|
bool check) |
531 |
|
{ |
532 |
|
TRACE("FloatingPointToUBVTotalTypeRule"); |
533 |
|
AlwaysAssert(n.getNumChildren() == 3); |
534 |
|
|
535 |
|
FloatingPointToUBVTotal info = |
536 |
|
n.getOperator().getConst<FloatingPointToUBVTotal>(); |
537 |
|
|
538 |
|
if (check) |
539 |
|
{ |
540 |
|
TypeNode roundingModeType = n[0].getType(check); |
541 |
|
|
542 |
|
if (!roundingModeType.isRoundingMode()) |
543 |
|
{ |
544 |
|
throw TypeCheckingExceptionPrivate( |
545 |
|
n, "first argument must be a rounding mode"); |
546 |
|
} |
547 |
|
|
548 |
|
TypeNode operandType = n[1].getType(check); |
549 |
|
|
550 |
|
if (!(operandType.isFloatingPoint())) |
551 |
|
{ |
552 |
|
throw TypeCheckingExceptionPrivate( |
553 |
|
n, |
554 |
|
"conversion to unsigned bit vector total" |
555 |
|
"used with a sort other than " |
556 |
|
"floating-point"); |
557 |
|
} |
558 |
|
|
559 |
|
TypeNode defaultValueType = n[2].getType(check); |
560 |
|
|
561 |
|
if (!(defaultValueType.isBitVector()) |
562 |
|
|| !(defaultValueType.getBitVectorSize() == info)) |
563 |
|
{ |
564 |
|
throw TypeCheckingExceptionPrivate( |
565 |
|
n, |
566 |
|
"conversion to unsigned bit vector total" |
567 |
|
"needs a bit vector of the same length" |
568 |
|
"as last argument"); |
569 |
|
} |
570 |
|
} |
571 |
|
|
572 |
|
return nodeManager->mkBitVectorType(info.d_bv_size); |
573 |
|
} |
574 |
|
|
575 |
|
TypeNode FloatingPointToSBVTotalTypeRule::computeType(NodeManager* nodeManager, |
576 |
|
TNode n, |
577 |
|
bool check) |
578 |
|
{ |
579 |
|
TRACE("FloatingPointToSBVTotalTypeRule"); |
580 |
|
AlwaysAssert(n.getNumChildren() == 3); |
581 |
|
|
582 |
|
FloatingPointToSBVTotal info = |
583 |
|
n.getOperator().getConst<FloatingPointToSBVTotal>(); |
584 |
|
|
585 |
|
if (check) |
586 |
|
{ |
587 |
|
TypeNode roundingModeType = n[0].getType(check); |
588 |
|
|
589 |
|
if (!roundingModeType.isRoundingMode()) |
590 |
|
{ |
591 |
|
throw TypeCheckingExceptionPrivate( |
592 |
|
n, "first argument must be a rounding mode"); |
593 |
|
} |
594 |
|
|
595 |
|
TypeNode operandType = n[1].getType(check); |
596 |
|
|
597 |
|
if (!(operandType.isFloatingPoint())) |
598 |
|
{ |
599 |
|
throw TypeCheckingExceptionPrivate(n, |
600 |
|
"conversion to signed bit vector " |
601 |
|
"used with a sort other than " |
602 |
|
"floating-point"); |
603 |
|
} |
604 |
|
|
605 |
|
TypeNode defaultValueType = n[2].getType(check); |
606 |
|
|
607 |
|
if (!(defaultValueType.isBitVector()) |
608 |
|
|| !(defaultValueType.getBitVectorSize() == info)) |
609 |
|
{ |
610 |
|
throw TypeCheckingExceptionPrivate(n, |
611 |
|
"conversion to signed bit vector total" |
612 |
|
"needs a bit vector of the same length" |
613 |
|
"as last argument"); |
614 |
|
} |
615 |
|
} |
616 |
|
|
617 |
|
return nodeManager->mkBitVectorType(info.d_bv_size); |
618 |
|
} |
619 |
|
|
620 |
6 |
TypeNode FloatingPointToRealTypeRule::computeType(NodeManager* nodeManager, |
621 |
|
TNode n, |
622 |
|
bool check) |
623 |
|
{ |
624 |
6 |
TRACE("FloatingPointToRealTypeRule"); |
625 |
6 |
AlwaysAssert(n.getNumChildren() == 1); |
626 |
|
|
627 |
6 |
if (check) |
628 |
|
{ |
629 |
12 |
TypeNode operandType = n[0].getType(check); |
630 |
|
|
631 |
6 |
if (!operandType.isFloatingPoint()) |
632 |
|
{ |
633 |
|
throw TypeCheckingExceptionPrivate( |
634 |
|
n, "floating-point to real applied to a non floating-point sort"); |
635 |
|
} |
636 |
|
} |
637 |
|
|
638 |
6 |
return nodeManager->realType(); |
639 |
|
} |
640 |
|
|
641 |
12 |
TypeNode FloatingPointToRealTotalTypeRule::computeType(NodeManager* nodeManager, |
642 |
|
TNode n, |
643 |
|
bool check) |
644 |
|
{ |
645 |
12 |
TRACE("FloatingPointToRealTotalTypeRule"); |
646 |
12 |
AlwaysAssert(n.getNumChildren() == 2); |
647 |
|
|
648 |
12 |
if (check) |
649 |
|
{ |
650 |
24 |
TypeNode operandType = n[0].getType(check); |
651 |
|
|
652 |
12 |
if (!operandType.isFloatingPoint()) |
653 |
|
{ |
654 |
|
throw TypeCheckingExceptionPrivate( |
655 |
|
n, |
656 |
|
"floating-point to real total applied to a non floating-point sort"); |
657 |
|
} |
658 |
|
|
659 |
24 |
TypeNode defaultValueType = n[1].getType(check); |
660 |
|
|
661 |
12 |
if (!defaultValueType.isReal()) |
662 |
|
{ |
663 |
|
throw TypeCheckingExceptionPrivate( |
664 |
|
n, "floating-point to real total needs a real second argument"); |
665 |
|
} |
666 |
|
} |
667 |
|
|
668 |
12 |
return nodeManager->realType(); |
669 |
|
} |
670 |
|
|
671 |
356 |
TypeNode FloatingPointComponentBit::computeType(NodeManager* nodeManager, |
672 |
|
TNode n, |
673 |
|
bool check) |
674 |
|
{ |
675 |
356 |
TRACE("FloatingPointComponentBit"); |
676 |
|
|
677 |
356 |
if (check) |
678 |
|
{ |
679 |
712 |
TypeNode operandType = n[0].getType(check); |
680 |
|
|
681 |
356 |
if (!operandType.isFloatingPoint()) |
682 |
|
{ |
683 |
|
throw TypeCheckingExceptionPrivate(n, |
684 |
|
"floating-point bit component " |
685 |
|
"applied to a non floating-point " |
686 |
|
"sort"); |
687 |
|
} |
688 |
712 |
if (!(Theory::isLeafOf(n[0], THEORY_FP) |
689 |
356 |
|| n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL)) |
690 |
|
{ |
691 |
|
throw TypeCheckingExceptionPrivate(n, |
692 |
|
"floating-point bit component " |
693 |
|
"applied to a non leaf / to_fp leaf " |
694 |
|
"node"); |
695 |
|
} |
696 |
|
} |
697 |
|
|
698 |
356 |
return nodeManager->mkBitVectorType(1); |
699 |
|
} |
700 |
|
|
701 |
89 |
TypeNode FloatingPointComponentExponent::computeType(NodeManager* nodeManager, |
702 |
|
TNode n, |
703 |
|
bool check) |
704 |
|
{ |
705 |
89 |
TRACE("FloatingPointComponentExponent"); |
706 |
|
|
707 |
178 |
TypeNode operandType = n[0].getType(check); |
708 |
|
|
709 |
89 |
if (check) |
710 |
|
{ |
711 |
89 |
if (!operandType.isFloatingPoint()) |
712 |
|
{ |
713 |
|
throw TypeCheckingExceptionPrivate(n, |
714 |
|
"floating-point exponent component " |
715 |
|
"applied to a non floating-point " |
716 |
|
"sort"); |
717 |
|
} |
718 |
178 |
if (!(Theory::isLeafOf(n[0], THEORY_FP) |
719 |
89 |
|| n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL)) |
720 |
|
{ |
721 |
|
throw TypeCheckingExceptionPrivate(n, |
722 |
|
"floating-point exponent component " |
723 |
|
"applied to a non leaf / to_fp " |
724 |
|
"node"); |
725 |
|
} |
726 |
|
} |
727 |
|
|
728 |
|
#ifdef CVC5_USE_SYMFPU |
729 |
|
/* Need to create some symfpu objects as the size of bit-vector |
730 |
|
* that is needed for this component is dependent on the encoding |
731 |
|
* used (i.e. whether subnormals are forcibly normalised or not). |
732 |
|
* Here we use types from floatingpoint.h which are the literal |
733 |
|
* back-end but it should't make a difference. */ |
734 |
89 |
FloatingPointSize fps = operandType.getConst<FloatingPointSize>(); |
735 |
89 |
uint32_t bw = FloatingPoint::getUnpackedExponentWidth(fps); |
736 |
|
#else |
737 |
|
uint32_t bw = 2; |
738 |
|
#endif |
739 |
178 |
return nodeManager->mkBitVectorType(bw); |
740 |
|
} |
741 |
|
|
742 |
89 |
TypeNode FloatingPointComponentSignificand::computeType( |
743 |
|
NodeManager* nodeManager, TNode n, bool check) |
744 |
|
{ |
745 |
89 |
TRACE("FloatingPointComponentSignificand"); |
746 |
|
|
747 |
178 |
TypeNode operandType = n[0].getType(check); |
748 |
|
|
749 |
89 |
if (check) |
750 |
|
{ |
751 |
89 |
if (!operandType.isFloatingPoint()) |
752 |
|
{ |
753 |
|
throw TypeCheckingExceptionPrivate(n, |
754 |
|
"floating-point significand " |
755 |
|
"component applied to a non " |
756 |
|
"floating-point sort"); |
757 |
|
} |
758 |
178 |
if (!(Theory::isLeafOf(n[0], THEORY_FP) |
759 |
89 |
|| n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL)) |
760 |
|
{ |
761 |
|
throw TypeCheckingExceptionPrivate(n, |
762 |
|
"floating-point significand " |
763 |
|
"component applied to a non leaf / " |
764 |
|
"to_fp node"); |
765 |
|
} |
766 |
|
} |
767 |
|
|
768 |
|
#ifdef CVC5_USE_SYMFPU |
769 |
|
/* As before we need to use some of sympfu. */ |
770 |
89 |
FloatingPointSize fps = operandType.getConst<FloatingPointSize>(); |
771 |
89 |
uint32_t bw = FloatingPoint::getUnpackedSignificandWidth(fps); |
772 |
|
#else |
773 |
|
uint32_t bw = 1; |
774 |
|
#endif |
775 |
178 |
return nodeManager->mkBitVectorType(bw); |
776 |
|
} |
777 |
|
|
778 |
7 |
TypeNode RoundingModeBitBlast::computeType(NodeManager* nodeManager, |
779 |
|
TNode n, |
780 |
|
bool check) |
781 |
|
{ |
782 |
7 |
TRACE("RoundingModeBitBlast"); |
783 |
|
|
784 |
7 |
if (check) |
785 |
|
{ |
786 |
14 |
TypeNode operandType = n[0].getType(check); |
787 |
|
|
788 |
7 |
if (!operandType.isRoundingMode()) |
789 |
|
{ |
790 |
|
throw TypeCheckingExceptionPrivate( |
791 |
|
n, "rounding mode bit-blast applied to a non rounding-mode sort"); |
792 |
|
} |
793 |
7 |
if (!Theory::isLeafOf(n[0], THEORY_FP)) |
794 |
|
{ |
795 |
|
throw TypeCheckingExceptionPrivate( |
796 |
|
n, "rounding mode bit-blast applied to a non leaf node"); |
797 |
|
} |
798 |
|
} |
799 |
|
|
800 |
7 |
return nodeManager->mkBitVectorType(CVC5_NUM_ROUNDING_MODES); |
801 |
|
} |
802 |
|
|
803 |
12 |
Cardinality CardinalityComputer::computeCardinality(TypeNode type) |
804 |
|
{ |
805 |
12 |
Assert(type.getKind() == kind::FLOATINGPOINT_TYPE); |
806 |
|
|
807 |
12 |
FloatingPointSize fps = type.getConst<FloatingPointSize>(); |
808 |
|
|
809 |
|
/* |
810 |
|
* 1 NaN |
811 |
|
* 2*1 Infinities |
812 |
|
* 2*1 Zeros |
813 |
|
* 2*2^(s-1) Subnormal |
814 |
|
* 2*((2^e)-2)*2^(s-1) Normal |
815 |
|
* |
816 |
|
* = 1 + 2*2 + 2*((2^e)-1)*2^(s-1) |
817 |
|
* = 5 + ((2^e)-1)*2^s |
818 |
|
*/ |
819 |
|
|
820 |
24 |
Integer significandValues = Integer(2).pow(fps.significandWidth()); |
821 |
24 |
Integer exponentValues = Integer(2).pow(fps.exponentWidth()); |
822 |
12 |
exponentValues -= Integer(1); |
823 |
|
|
824 |
24 |
return Integer(5) + exponentValues * significandValues; |
825 |
|
} |
826 |
|
|
827 |
|
} // namespace fp |
828 |
|
} // namespace theory |
829 |
28194 |
} // namespace cvc5 |