GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/util/floatingpoint.cpp Lines: 206 280 73.6 %
Date: 2021-03-23 Branches: 235 794 29.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file floatingpoint.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Martin Brain, Haniel Barbosa
6
 ** Copyright (c) 2013  University of Oxford
7
 ** This file is part of the CVC4 project.
8
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
9
 ** in the top-level source directory and their institutional affiliations.
10
 ** All rights reserved.  See the file COPYING in the top-level source
11
 ** directory for licensing information.\endverbatim
12
 **
13
 ** \brief A floating-point value.
14
 **
15
 ** This file contains the data structures used by the constant and parametric
16
 ** types of the floating point theory.
17
 **/
18
19
#include "util/floatingpoint.h"
20
21
#include <math.h>
22
23
#include <limits>
24
25
#include "base/check.h"
26
#include "util/floatingpoint_literal_symfpu.h"
27
#include "util/integer.h"
28
29
#ifdef CVC4_USE_SYMFPU
30
#include "symfpu/core/add.h"
31
#include "symfpu/core/classify.h"
32
#include "symfpu/core/compare.h"
33
#include "symfpu/core/convert.h"
34
#include "symfpu/core/divide.h"
35
#include "symfpu/core/fma.h"
36
#include "symfpu/core/ite.h"
37
#include "symfpu/core/multiply.h"
38
#include "symfpu/core/packing.h"
39
#include "symfpu/core/remainder.h"
40
#include "symfpu/core/sign.h"
41
#include "symfpu/core/sqrt.h"
42
#include "symfpu/utils/numberOfRoundingModes.h"
43
#include "symfpu/utils/properties.h"
44
#endif
45
46
/* -------------------------------------------------------------------------- */
47
48
#ifdef CVC4_USE_SYMFPU
49
namespace symfpu {
50
51
#define CVC4_LIT_ITE_DFN(T)                                            \
52
  template <>                                                          \
53
  struct ite<::CVC4::symfpuLiteral::CVC4Prop, T>                       \
54
  {                                                                    \
55
    static const T& iteOp(const ::CVC4::symfpuLiteral::CVC4Prop& cond, \
56
                          const T& l,                                  \
57
                          const T& r)                                  \
58
    {                                                                  \
59
      return cond ? l : r;                                             \
60
    }                                                                  \
61
  }
62
63
CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::rm);
64
72965
CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::prop);
65
46247
CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::sbv);
66
54578
CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::ubv);
67
68
#undef CVC4_LIT_ITE_DFN
69
}
70
#endif
71
72
/* -------------------------------------------------------------------------- */
73
74
namespace CVC4 {
75
76
/* -------------------------------------------------------------------------- */
77
78
105
uint32_t FloatingPoint::getUnpackedExponentWidth(FloatingPointSize& size)
79
{
80
#ifdef CVC4_USE_SYMFPU
81
105
  return SymFPUUnpackedFloatLiteral::exponentWidth(size);
82
#else
83
  Unreachable() << "no concrete implementation of FloatingPointLiteral";
84
  return 2;
85
#endif
86
}
87
88
105
uint32_t FloatingPoint::getUnpackedSignificandWidth(FloatingPointSize& size)
89
{
90
#ifdef CVC4_USE_SYMFPU
91
105
  return SymFPUUnpackedFloatLiteral::significandWidth(size);
92
#else
93
  Unreachable() << "no concrete implementation of FloatingPointLiteral";
94
  return 2;
95
#endif
96
}
97
98
249
FloatingPoint::FloatingPoint(uint32_t d_exp_size,
99
                             uint32_t d_sig_size,
100
249
                             const BitVector& bv)
101
    : d_fp_size(d_exp_size, d_sig_size),
102
#ifdef CVC4_USE_SYMFPU
103
996
      d_fpl(new FloatingPointLiteral(symfpu::unpack<symfpuLiteral::traits>(
104
996
          symfpuLiteral::CVC4FPSize(d_exp_size, d_sig_size), bv)))
105
#else
106
      d_fpl(new FloatingPointLiteral(d_exp_size, d_sig_size, 0.0))
107
#endif
108
{
109
249
}
110
111
64
FloatingPoint::FloatingPoint(const FloatingPointSize& size, const BitVector& bv)
112
    : d_fp_size(size),
113
#ifdef CVC4_USE_SYMFPU
114
      d_fpl(new FloatingPointLiteral(
115
64
          symfpu::unpack<symfpuLiteral::traits>(size, bv)))
116
#else
117
      d_fpl(new FloatingPointLiteral(
118
          size.exponentWidth(), size.significandWidth(), 0.0))
119
#endif
120
{
121
64
}
122
123
4
FloatingPoint::FloatingPoint(const FloatingPointSize& size,
124
                             const RoundingMode& rm,
125
                             const BitVector& bv,
126
4
                             bool signedBV)
127
4
    : d_fp_size(size)
128
{
129
#ifdef CVC4_USE_SYMFPU
130
4
  if (signedBV)
131
  {
132
12
    d_fpl.reset(new FloatingPointLiteral(
133
16
        symfpu::convertSBVToFloat<symfpuLiteral::traits>(
134
8
            symfpuLiteral::CVC4FPSize(size),
135
8
            symfpuLiteral::CVC4RM(rm),
136
12
            symfpuLiteral::CVC4SignedBitVector(bv))));
137
  }
138
  else
139
  {
140
    d_fpl.reset(new FloatingPointLiteral(
141
        symfpu::convertUBVToFloat<symfpuLiteral::traits>(
142
            symfpuLiteral::CVC4FPSize(size),
143
            symfpuLiteral::CVC4RM(rm),
144
            symfpuLiteral::CVC4UnsignedBitVector(bv))));
145
  }
146
#else
147
  d_fpl.reset(new FloatingPointLiteral(2, 2, 0.0));
148
#endif
149
4
}
150
151
2012
FloatingPoint::FloatingPoint(const FloatingPointSize& fp_size,
152
2012
                             FloatingPointLiteral* fpl)
153
2012
    : d_fp_size(fp_size)
154
{
155
2012
  d_fpl.reset(fpl);
156
2012
}
157
158
3383
FloatingPoint::FloatingPoint(const FloatingPoint& fp) : d_fp_size(fp.d_fp_size)
159
{
160
3383
  d_fpl.reset(new FloatingPointLiteral(*fp.d_fpl));
161
3383
}
162
163
20
FloatingPoint::FloatingPoint(const FloatingPointSize& size,
164
                             const RoundingMode& rm,
165
20
                             const Rational& r)
166
20
    : d_fp_size(size)
167
{
168
40
  Rational two(2, 1);
169
170
20
  if (r.isZero())
171
  {
172
#ifdef CVC4_USE_SYMFPU
173
    // In keeping with the SMT-LIB standard
174
24
    d_fpl.reset(new FloatingPointLiteral(
175
24
        SymFPUUnpackedFloatLiteral::makeZero(size, false)));
176
#else
177
    d_fpl.reset(new FloatingPointLiteral(2, 2, 0.0));
178
#endif
179
  }
180
  else
181
  {
182
#ifdef CVC4_USE_SYMFPU
183
12
    uint32_t negative = (r.sgn() < 0) ? 1 : 0;
184
#endif
185
24
    Rational rabs(r.abs());
186
187
    // Compute the exponent
188
24
    Integer exp(0U);
189
24
    Integer inc(1U);
190
24
    Rational working(1, 1);
191
192
12
    if (rabs != working)
193
    {
194
8
      if (rabs < working)
195
      {
196
56
        while (rabs < working)
197
        {
198
24
          exp -= inc;
199
24
          working /= two;
200
        }
201
      }
202
      else
203
      {
204
        while (rabs >= working)
205
        {
206
          exp += inc;
207
          working *= two;
208
        }
209
        exp -= inc;
210
        working /= two;
211
      }
212
    }
213
214
12
    Assert(working <= rabs);
215
12
    Assert(rabs < working * two);
216
217
    // Work out the number of bits required to represent the exponent for a
218
    // normal number
219
12
    uint32_t expBits = 2;  // No point starting with an invalid amount
220
221
24
    Integer doubleInt(2);
222
12
    if (exp.strictlyPositive())
223
    {
224
      // 1 more than exactly representable with expBits
225
      Integer representable(4);
226
      while (representable <= exp)
227
      {  // hence <=
228
        representable *= doubleInt;
229
        ++expBits;
230
      }
231
    }
232
12
    else if (exp.strictlyNegative())
233
    {
234
16
      Integer representable(-4);  // Exactly representable with expBits + sign
235
                                  // but -2^n and -(2^n - 1) are both subnormal
236
16
      while ((representable + doubleInt) > exp)
237
      {
238
4
        representable *= doubleInt;
239
4
        ++expBits;
240
      }
241
    }
242
12
    ++expBits;  // To allow for sign
243
244
24
    BitVector exactExp(expBits, exp);
245
246
    // Compute the significand.
247
12
    uint32_t sigBits = size.significandWidth() + 2;  // guard and sticky bits
248
24
    BitVector sig(sigBits, 0U);
249
24
    BitVector one(sigBits, 1U);
250
24
    Rational workingSig(0, 1);
251
544
    for (uint32_t i = 0; i < sigBits - 1; ++i)
252
    {
253
1064
      Rational mid(workingSig + working);
254
255
532
      if (mid <= rabs)
256
      {
257
184
        sig = sig.setBit(0, true);
258
184
        workingSig = mid;
259
      }
260
261
532
      sig = sig.leftShift(one);
262
532
      working /= two;
263
    }
264
265
    // Compute the sticky bit
266
24
    Rational remainder(rabs - workingSig);
267
12
    Assert(Rational(0, 1) <= remainder);
268
269
12
    if (!remainder.isZero())
270
    {
271
8
      sig = sig.setBit(0, true);
272
    }
273
274
    // Build an exact float
275
12
    FloatingPointSize exactFormat(expBits, sigBits);
276
277
    // A small subtlety... if the format has expBits the unpacked format
278
    // may have more to allow subnormals to be normalised.
279
    // Thus...
280
#ifdef CVC4_USE_SYMFPU
281
    uint32_t extension =
282
12
        SymFPUUnpackedFloatLiteral::exponentWidth(exactFormat) - expBits;
283
284
    FloatingPointLiteral exactFloat(
285
24
        negative, exactExp.signExtend(extension), sig);
286
287
    // Then cast...
288
24
    d_fpl.reset(new FloatingPointLiteral(symfpu::convertFloatToFloat(
289
12
        exactFormat, size, rm, exactFloat.d_symuf)));
290
#else
291
    Unreachable() << "no concrete implementation of FloatingPointLiteral";
292
#endif
293
  }
294
20
}
295
296
5732
FloatingPoint::~FloatingPoint()
297
{
298
5732
}
299
300
26
FloatingPoint FloatingPoint::makeNaN(const FloatingPointSize& size)
301
{
302
#ifdef CVC4_USE_SYMFPU
303
  return FloatingPoint(
304
      size,
305
26
      new FloatingPointLiteral(SymFPUUnpackedFloatLiteral::makeNaN(size)));
306
#else
307
  return FloatingPoint(2, 2, BitVector(4U, 0U));
308
#endif
309
}
310
311
100
FloatingPoint FloatingPoint::makeInf(const FloatingPointSize& size, bool sign)
312
{
313
#ifdef CVC4_USE_SYMFPU
314
  return FloatingPoint(size,
315
                       new FloatingPointLiteral(
316
100
                           SymFPUUnpackedFloatLiteral::makeInf(size, sign)));
317
#else
318
  return FloatingPoint(2, 2, BitVector(4U, 0U));
319
#endif
320
}
321
322
22
FloatingPoint FloatingPoint::makeZero(const FloatingPointSize& size, bool sign)
323
{
324
#ifdef CVC4_USE_SYMFPU
325
  return FloatingPoint(size,
326
                       new FloatingPointLiteral(
327
22
                           SymFPUUnpackedFloatLiteral::makeZero(size, sign)));
328
#else
329
  return FloatingPoint(2, 2, BitVector(4U, 0U));
330
#endif
331
}
332
333
16
FloatingPoint FloatingPoint::makeMinSubnormal(const FloatingPointSize& size,
334
                                              bool sign)
335
{
336
32
  BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1);
337
32
  BitVector bvexp = BitVector::mkZero(size.packedExponentWidth());
338
32
  BitVector bvsig = BitVector::mkOne(size.packedSignificandWidth());
339
32
  return FloatingPoint(size, bvsign.concat(bvexp).concat(bvsig));
340
}
341
342
16
FloatingPoint FloatingPoint::makeMaxSubnormal(const FloatingPointSize& size,
343
                                              bool sign)
344
{
345
32
  BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1);
346
32
  BitVector bvexp = BitVector::mkZero(size.packedExponentWidth());
347
32
  BitVector bvsig = BitVector::mkOnes(size.packedSignificandWidth());
348
32
  return FloatingPoint(size, bvsign.concat(bvexp).concat(bvsig));
349
}
350
351
16
FloatingPoint FloatingPoint::makeMinNormal(const FloatingPointSize& size,
352
                                           bool sign)
353
{
354
32
  BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1);
355
32
  BitVector bvexp = BitVector::mkOne(size.packedExponentWidth());
356
32
  BitVector bvsig = BitVector::mkZero(size.packedSignificandWidth());
357
32
  return FloatingPoint(size, bvsign.concat(bvexp).concat(bvsig));
358
}
359
360
16
FloatingPoint FloatingPoint::makeMaxNormal(const FloatingPointSize& size,
361
                                           bool sign)
362
{
363
32
  BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1);
364
32
  BitVector bvexp = BitVector::mkOnes(size.packedExponentWidth());
365
16
  bvexp.setBit(0, false);
366
32
  BitVector bvsig = BitVector::mkOnes(size.packedSignificandWidth());
367
32
  return FloatingPoint(size, bvsign.concat(bvexp).concat(bvsig));
368
}
369
370
/* Operations implemented using symfpu */
371
9
FloatingPoint FloatingPoint::absolute(void) const
372
{
373
#ifdef CVC4_USE_SYMFPU
374
  return FloatingPoint(
375
      d_fp_size,
376
      new FloatingPointLiteral(
377
9
          symfpu::absolute<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf)));
378
#else
379
  return *this;
380
#endif
381
}
382
383
204
FloatingPoint FloatingPoint::negate(void) const
384
{
385
#ifdef CVC4_USE_SYMFPU
386
  return FloatingPoint(
387
      d_fp_size,
388
      new FloatingPointLiteral(
389
204
          symfpu::negate<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf)));
390
#else
391
  return *this;
392
#endif
393
}
394
395
640
FloatingPoint FloatingPoint::plus(const RoundingMode& rm,
396
                                  const FloatingPoint& arg) const
397
{
398
#ifdef CVC4_USE_SYMFPU
399
640
  Assert(d_fp_size == arg.d_fp_size);
400
  return FloatingPoint(
401
      d_fp_size,
402
2560
      new FloatingPointLiteral(symfpu::add<symfpuLiteral::traits>(
403
2560
          d_fp_size, rm, d_fpl->d_symuf, arg.d_fpl->d_symuf, true)));
404
#else
405
  return *this;
406
#endif
407
}
408
409
FloatingPoint FloatingPoint::sub(const RoundingMode& rm,
410
                                 const FloatingPoint& arg) const
411
{
412
#ifdef CVC4_USE_SYMFPU
413
  Assert(d_fp_size == arg.d_fp_size);
414
  return FloatingPoint(
415
      d_fp_size,
416
      new FloatingPointLiteral(symfpu::add<symfpuLiteral::traits>(
417
          d_fp_size, rm, d_fpl->d_symuf, arg.d_fpl->d_symuf, false)));
418
#else
419
  return *this;
420
#endif
421
}
422
423
132
FloatingPoint FloatingPoint::mult(const RoundingMode& rm,
424
                                  const FloatingPoint& arg) const
425
{
426
#ifdef CVC4_USE_SYMFPU
427
132
  Assert(d_fp_size == arg.d_fp_size);
428
  return FloatingPoint(
429
      d_fp_size,
430
396
      new FloatingPointLiteral(symfpu::multiply<symfpuLiteral::traits>(
431
528
          d_fp_size, rm, d_fpl->d_symuf, arg.d_fpl->d_symuf)));
432
#else
433
  return *this;
434
#endif
435
}
436
437
FloatingPoint FloatingPoint::fma(const RoundingMode& rm,
438
                                 const FloatingPoint& arg1,
439
                                 const FloatingPoint& arg2) const
440
{
441
#ifdef CVC4_USE_SYMFPU
442
  Assert(d_fp_size == arg1.d_fp_size);
443
  Assert(d_fp_size == arg2.d_fp_size);
444
  return FloatingPoint(
445
      d_fp_size,
446
      new FloatingPointLiteral(
447
          symfpu::fma<symfpuLiteral::traits>(d_fp_size,
448
                                             rm,
449
                                             d_fpl->d_symuf,
450
                                             arg1.d_fpl->d_symuf,
451
                                             arg2.d_fpl->d_symuf)));
452
#else
453
  return *this;
454
#endif
455
}
456
457
188
FloatingPoint FloatingPoint::div(const RoundingMode& rm,
458
                                 const FloatingPoint& arg) const
459
{
460
#ifdef CVC4_USE_SYMFPU
461
188
  Assert(d_fp_size == arg.d_fp_size);
462
  return FloatingPoint(
463
      d_fp_size,
464
564
      new FloatingPointLiteral(symfpu::divide<symfpuLiteral::traits>(
465
752
          d_fp_size, rm, d_fpl->d_symuf, arg.d_fpl->d_symuf)));
466
#else
467
  return *this;
468
#endif
469
}
470
471
27
FloatingPoint FloatingPoint::sqrt(const RoundingMode& rm) const
472
{
473
#ifdef CVC4_USE_SYMFPU
474
  return FloatingPoint(
475
      d_fp_size,
476
      new FloatingPointLiteral(
477
27
          symfpu::sqrt<symfpuLiteral::traits>(d_fp_size, rm, d_fpl->d_symuf)));
478
#else
479
  return *this;
480
#endif
481
}
482
483
140
FloatingPoint FloatingPoint::rti(const RoundingMode& rm) const
484
{
485
#ifdef CVC4_USE_SYMFPU
486
  return FloatingPoint(
487
      d_fp_size,
488
280
      new FloatingPointLiteral(symfpu::roundToIntegral<symfpuLiteral::traits>(
489
420
          d_fp_size, rm, d_fpl->d_symuf)));
490
#else
491
  return *this;
492
#endif
493
}
494
495
95
FloatingPoint FloatingPoint::rem(const FloatingPoint& arg) const
496
{
497
#ifdef CVC4_USE_SYMFPU
498
95
  Assert(d_fp_size == arg.d_fp_size);
499
  return FloatingPoint(
500
      d_fp_size,
501
285
      new FloatingPointLiteral(symfpu::remainder<symfpuLiteral::traits>(
502
380
          d_fp_size, d_fpl->d_symuf, arg.d_fpl->d_symuf)));
503
#else
504
  return *this;
505
#endif
506
}
507
508
424
FloatingPoint FloatingPoint::maxTotal(const FloatingPoint& arg,
509
                                      bool zeroCaseLeft) const
510
{
511
#ifdef CVC4_USE_SYMFPU
512
424
  Assert(d_fp_size == arg.d_fp_size);
513
  return FloatingPoint(
514
      d_fp_size,
515
1272
      new FloatingPointLiteral(symfpu::max<symfpuLiteral::traits>(
516
1696
          d_fp_size, d_fpl->d_symuf, arg.d_fpl->d_symuf, zeroCaseLeft)));
517
#else
518
  return *this;
519
#endif
520
}
521
522
FloatingPoint FloatingPoint::minTotal(const FloatingPoint& arg,
523
                                      bool zeroCaseLeft) const
524
{
525
#ifdef CVC4_USE_SYMFPU
526
  Assert(d_fp_size == arg.d_fp_size);
527
  return FloatingPoint(
528
      d_fp_size,
529
      new FloatingPointLiteral(symfpu::min<symfpuLiteral::traits>(
530
          d_fp_size, d_fpl->d_symuf, arg.d_fpl->d_symuf, zeroCaseLeft)));
531
#else
532
  return *this;
533
#endif
534
}
535
536
212
FloatingPoint::PartialFloatingPoint FloatingPoint::max(
537
    const FloatingPoint& arg) const
538
{
539
424
  FloatingPoint tmp(maxTotal(arg, true));
540
424
  return PartialFloatingPoint(tmp, tmp == maxTotal(arg, false));
541
}
542
543
FloatingPoint::PartialFloatingPoint FloatingPoint::min(
544
    const FloatingPoint& arg) const
545
{
546
  FloatingPoint tmp(minTotal(arg, true));
547
  return PartialFloatingPoint(tmp, tmp == minTotal(arg, false));
548
}
549
550
2722
bool FloatingPoint::operator==(const FloatingPoint& fp) const
551
{
552
#ifdef CVC4_USE_SYMFPU
553
2722
  return ((d_fp_size == fp.d_fp_size)
554
8166
          && symfpu::smtlibEqual<symfpuLiteral::traits>(
555
8166
              d_fp_size, d_fpl->d_symuf, fp.d_fpl->d_symuf));
556
#else
557
  return ((d_fp_size == fp.d_fp_size));
558
#endif
559
}
560
561
28
bool FloatingPoint::operator<=(const FloatingPoint& arg) const
562
{
563
#ifdef CVC4_USE_SYMFPU
564
28
  Assert(d_fp_size == arg.d_fp_size);
565
56
  return symfpu::lessThanOrEqual<symfpuLiteral::traits>(
566
84
      d_fp_size, d_fpl->d_symuf, arg.d_fpl->d_symuf);
567
#else
568
  return false;
569
#endif
570
}
571
572
2
bool FloatingPoint::operator<(const FloatingPoint& arg) const
573
{
574
#ifdef CVC4_USE_SYMFPU
575
2
  Assert(d_fp_size == arg.d_fp_size);
576
4
  return symfpu::lessThan<symfpuLiteral::traits>(
577
6
      d_fp_size, d_fpl->d_symuf, arg.d_fpl->d_symuf);
578
#else
579
  return false;
580
#endif
581
}
582
583
5
BitVector FloatingPoint::getExponent() const
584
{
585
#ifdef CVC4_USE_SYMFPU
586
5
  return d_fpl->d_symuf.exponent;
587
#else
588
  Unreachable() << "no concrete implementation of FloatingPointLiteral";
589
  return BitVector();
590
#endif
591
}
592
593
5
BitVector FloatingPoint::getSignificand() const
594
{
595
#ifdef CVC4_USE_SYMFPU
596
5
  return d_fpl->d_symuf.significand;
597
#else
598
  Unreachable() << "no concrete implementation of FloatingPointLiteral";
599
  return BitVector();
600
#endif
601
}
602
603
5
bool FloatingPoint::getSign() const
604
{
605
#ifdef CVC4_USE_SYMFPU
606
5
  return d_fpl->d_symuf.sign;
607
#else
608
  Unreachable() << "no concrete implementation of FloatingPointLiteral";
609
  return false;
610
#endif
611
}
612
613
43
bool FloatingPoint::isNormal(void) const
614
{
615
#ifdef CVC4_USE_SYMFPU
616
43
  return symfpu::isNormal<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf);
617
#else
618
  return false;
619
#endif
620
}
621
622
41
bool FloatingPoint::isSubnormal(void) const
623
{
624
#ifdef CVC4_USE_SYMFPU
625
41
  return symfpu::isSubnormal<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf);
626
#else
627
  return false;
628
#endif
629
}
630
631
263
bool FloatingPoint::isZero(void) const
632
{
633
#ifdef CVC4_USE_SYMFPU
634
263
  return symfpu::isZero<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf);
635
#else
636
  return false;
637
#endif
638
}
639
640
23
bool FloatingPoint::isInfinite(void) const
641
{
642
#ifdef CVC4_USE_SYMFPU
643
23
  return symfpu::isInfinite<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf);
644
#else
645
  return false;
646
#endif
647
}
648
649
34
bool FloatingPoint::isNaN(void) const
650
{
651
#ifdef CVC4_USE_SYMFPU
652
34
  return symfpu::isNaN<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf);
653
#else
654
  return false;
655
#endif
656
}
657
658
13
bool FloatingPoint::isNegative(void) const
659
{
660
#ifdef CVC4_USE_SYMFPU
661
13
  return symfpu::isNegative<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf);
662
#else
663
  return false;
664
#endif
665
}
666
667
7
bool FloatingPoint::isPositive(void) const
668
{
669
#ifdef CVC4_USE_SYMFPU
670
7
  return symfpu::isPositive<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf);
671
#else
672
  return false;
673
#endif
674
}
675
676
5
FloatingPoint FloatingPoint::convert(const FloatingPointSize& target,
677
                                     const RoundingMode& rm) const
678
{
679
#ifdef CVC4_USE_SYMFPU
680
  return FloatingPoint(target,
681
                       new FloatingPointLiteral(
682
10
                           symfpu::convertFloatToFloat<symfpuLiteral::traits>(
683
15
                               d_fp_size, target, rm, d_fpl->d_symuf)));
684
#else
685
  return *this;
686
#endif
687
}
688
689
BitVector FloatingPoint::convertToBVTotal(BitVectorSize width,
690
                                          const RoundingMode& rm,
691
                                          bool signedBV,
692
                                          BitVector undefinedCase) const
693
{
694
#ifdef CVC4_USE_SYMFPU
695
    if (signedBV)
696
      return symfpu::convertFloatToSBV<symfpuLiteral::traits>(
697
          d_fp_size, rm, d_fpl->d_symuf, width, undefinedCase);
698
    else
699
      return symfpu::convertFloatToUBV<symfpuLiteral::traits>(
700
          d_fp_size, rm, d_fpl->d_symuf, width, undefinedCase);
701
#else
702
  return undefinedCase;
703
#endif
704
}
705
706
8
Rational FloatingPoint::convertToRationalTotal(Rational undefinedCase) const
707
{
708
16
  PartialRational p(convertToRational());
709
710
16
  return p.second ? p.first : undefinedCase;
711
}
712
713
FloatingPoint::PartialBitVector FloatingPoint::convertToBV(
714
    BitVectorSize width, const RoundingMode& rm, bool signedBV) const
715
{
716
  BitVector tmp(convertToBVTotal(width, rm, signedBV, BitVector(width, 0U)));
717
  BitVector confirm(
718
      convertToBVTotal(width, rm, signedBV, BitVector(width, 1U)));
719
720
  return PartialBitVector(tmp, tmp == confirm);
721
}
722
723
10
FloatingPoint::PartialRational FloatingPoint::convertToRational(void) const
724
{
725
10
  if (isNaN() || isInfinite())
726
  {
727
    return PartialRational(Rational(0U, 1U), false);
728
  }
729
10
  if (isZero())
730
  {
731
6
    return PartialRational(Rational(0U, 1U), true);
732
  }
733
  else
734
  {
735
#ifdef CVC4_USE_SYMFPU
736
8
    Integer sign((d_fpl->d_symuf.getSign()) ? -1 : 1);
737
    Integer exp(
738
8
        d_fpl->d_symuf.getExponent().toSignedInteger()
739
8
        - (Integer(d_fp_size.significandWidth()
740
8
                   - 1)));  // -1 as forcibly normalised into the [1,2) range
741
8
    Integer significand(d_fpl->d_symuf.getSignificand().toInteger());
742
#else
743
      Integer sign(0);
744
      Integer exp(0);
745
      Integer significand(0);
746
#endif
747
8
      Integer signedSignificand(sign * significand);
748
749
      // We only have multiplyByPow(uint32_t) so we can't convert all numbers.
750
      // As we convert Integer -> unsigned int -> uint32_t we need that
751
      // unsigned int is not smaller than uint32_t
752
      static_assert(sizeof(unsigned int) >= sizeof(uint32_t),
753
		    "Conversion float -> real could loose data");
754
#ifdef CVC4_ASSERTIONS
755
      // Note that multipling by 2^n requires n bits of space (worst case)
756
      // so, in effect, these tests limit us to cases where the resultant
757
      // number requires up to 2^32 bits = 512 megabyte to represent.
758
8
      Integer shiftLimit(std::numeric_limits<uint32_t>::max());
759
#endif
760
761
4
      if (!(exp.strictlyNegative())) {
762
2
	Assert(exp <= shiftLimit);
763
4
	Integer r(signedSignificand.multiplyByPow2(exp.toUnsignedInt()));
764
2
	return PartialRational(Rational(r), true);
765
      } else {
766
4
	Integer one(1U);
767
2
	Assert((-exp) <= shiftLimit);
768
4
	Integer q(one.multiplyByPow2((-exp).toUnsignedInt()));
769
4
	Rational r(signedSignificand, q);
770
2
	return PartialRational(r, true);
771
      }
772
  }
773
774
    Unreachable() << "Convert float literal to real broken.";
775
}
776
777
3381
BitVector FloatingPoint::pack(void) const
778
{
779
#ifdef CVC4_USE_SYMFPU
780
3381
  BitVector bv(symfpu::pack<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf));
781
#else
782
  BitVector bv(4u, 0u);
783
#endif
784
3381
  return bv;
785
}
786
787
std::string FloatingPoint::toString(bool printAsIndexed) const
788
{
789
  std::string str;
790
  // retrive BV value
791
  BitVector bv(pack());
792
  uint32_t largestSignificandBit =
793
      d_fp_size.significandWidth() - 2;  // -1 for -inclusive, -1 for hidden
794
  uint32_t largestExponentBit =
795
      (d_fp_size.exponentWidth() - 1) + (largestSignificandBit + 1);
796
  BitVector v[3];
797
  v[0] = bv.extract(largestExponentBit + 1, largestExponentBit + 1);
798
  v[1] = bv.extract(largestExponentBit, largestSignificandBit + 1);
799
  v[2] = bv.extract(largestSignificandBit, 0);
800
  str.append("(fp ");
801
  for (uint32_t i = 0; i < 3; ++i)
802
  {
803
    if (printAsIndexed)
804
    {
805
      str.append("(_ bv");
806
      str.append(v[i].getValue().toString());
807
      str.append(" ");
808
      str.append(std::to_string(v[i].getSize()));
809
      str.append(")");
810
    }
811
    else
812
    {
813
      str.append("#b");
814
      str.append(v[i].toString());
815
    }
816
    if (i < 2)
817
    {
818
      str.append(" ");
819
    }
820
  }
821
  str.append(")");
822
  return str;
823
}
824
825
std::ostream& operator<<(std::ostream& os, const FloatingPoint& fp)
826
{
827
  // print in binary notation
828
  return os << fp.toString();
829
}
830
831
std::ostream& operator<<(std::ostream& os, const FloatingPointSize& fps)
832
{
833
  return os << "(_ FloatingPoint " << fps.exponentWidth() << " "
834
            << fps.significandWidth() << ")";
835
}
836
837
std::ostream& operator<<(std::ostream& os, const FloatingPointConvertSort& fpcs)
838
{
839
  return os << "(_ to_fp " << fpcs.d_fp_size.exponentWidth() << " "
840
            << fpcs.d_fp_size.significandWidth() << ")";
841
}
842
26685
}/* CVC4 namespace */