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