GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/fp/fp_converter.cpp Lines: 478 757 63.1 %
Date: 2021-03-22 Branches: 1007 3327 30.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file fp_converter.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Martin Brain, Mathias Preiner, Aina Niemetz
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief Conversion of floating-point operations to bit-vectors using symfpu.
13
 **/
14
15
#include "theory/fp/fp_converter.h"
16
17
#include <vector>
18
19
#include "base/check.h"
20
#include "expr/node_builder.h"
21
#include "theory/theory.h"  // theory.h Only needed for the leaf test
22
#include "util/floatingpoint.h"
23
#include "util/floatingpoint_literal_symfpu.h"
24
25
#ifdef CVC4_USE_SYMFPU
26
#include "symfpu/core/add.h"
27
#include "symfpu/core/classify.h"
28
#include "symfpu/core/compare.h"
29
#include "symfpu/core/convert.h"
30
#include "symfpu/core/divide.h"
31
#include "symfpu/core/fma.h"
32
#include "symfpu/core/ite.h"
33
#include "symfpu/core/multiply.h"
34
#include "symfpu/core/packing.h"
35
#include "symfpu/core/remainder.h"
36
#include "symfpu/core/sign.h"
37
#include "symfpu/core/sqrt.h"
38
#include "symfpu/utils/numberOfRoundingModes.h"
39
#include "symfpu/utils/properties.h"
40
#endif
41
42
#ifdef CVC4_USE_SYMFPU
43
namespace symfpu {
44
using namespace ::CVC4::theory::fp::symfpuSymbolic;
45
46
#define CVC4_SYM_ITE_DFN(T)                                                \
47
  template <>                                                              \
48
  struct ite<symbolicProposition, T>                                       \
49
  {                                                                        \
50
    static const T iteOp(const symbolicProposition &_cond,                 \
51
                         const T &_l,                                      \
52
                         const T &_r)                                      \
53
    {                                                                      \
54
      ::CVC4::NodeManager *nm = ::CVC4::NodeManager::currentNM();          \
55
                                                                           \
56
      ::CVC4::Node cond = _cond;                                           \
57
      ::CVC4::Node l = _l;                                                 \
58
      ::CVC4::Node r = _r;                                                 \
59
                                                                           \
60
      /* Handle some common symfpu idioms */                               \
61
      if (cond.isConst())                                                  \
62
      {                                                                    \
63
        return (cond == nm->mkConst(::CVC4::BitVector(1U, 1U))) ? l : r;   \
64
      }                                                                    \
65
      else                                                                 \
66
      {                                                                    \
67
        if (l.getKind() == ::CVC4::kind::BITVECTOR_ITE)                    \
68
        {                                                                  \
69
          if (l[1] == r)                                                   \
70
          {                                                                \
71
            return nm->mkNode(                                             \
72
                ::CVC4::kind::BITVECTOR_ITE,                               \
73
                nm->mkNode(::CVC4::kind::BITVECTOR_AND,                    \
74
                           cond,                                           \
75
                           nm->mkNode(::CVC4::kind::BITVECTOR_NOT, l[0])), \
76
                l[2],                                                      \
77
                r);                                                        \
78
          }                                                                \
79
          else if (l[2] == r)                                              \
80
          {                                                                \
81
            return nm->mkNode(                                             \
82
                ::CVC4::kind::BITVECTOR_ITE,                               \
83
                nm->mkNode(::CVC4::kind::BITVECTOR_AND, cond, l[0]),       \
84
                l[1],                                                      \
85
                r);                                                        \
86
          }                                                                \
87
        }                                                                  \
88
        else if (r.getKind() == ::CVC4::kind::BITVECTOR_ITE)               \
89
        {                                                                  \
90
          if (r[1] == l)                                                   \
91
          {                                                                \
92
            return nm->mkNode(                                             \
93
                ::CVC4::kind::BITVECTOR_ITE,                               \
94
                nm->mkNode(::CVC4::kind::BITVECTOR_AND,                    \
95
                           nm->mkNode(::CVC4::kind::BITVECTOR_NOT, cond),  \
96
                           nm->mkNode(::CVC4::kind::BITVECTOR_NOT, r[0])), \
97
                r[2],                                                      \
98
                l);                                                        \
99
          }                                                                \
100
          else if (r[2] == l)                                              \
101
          {                                                                \
102
            return nm->mkNode(                                             \
103
                ::CVC4::kind::BITVECTOR_ITE,                               \
104
                nm->mkNode(::CVC4::kind::BITVECTOR_AND,                    \
105
                           nm->mkNode(::CVC4::kind::BITVECTOR_NOT, cond),  \
106
                           r[0]),                                          \
107
                r[1],                                                      \
108
                l);                                                        \
109
          }                                                                \
110
        }                                                                  \
111
      }                                                                    \
112
      return T(nm->mkNode(::CVC4::kind::BITVECTOR_ITE, cond, l, r));       \
113
    }                                                                      \
114
  }
115
116
// Can (unsurprisingly) only ITE things which contain Nodes
117
CVC4_SYM_ITE_DFN(traits::rm);
118
3571
CVC4_SYM_ITE_DFN(traits::prop);
119
9240
CVC4_SYM_ITE_DFN(traits::sbv);
120
19196
CVC4_SYM_ITE_DFN(traits::ubv);
121
122
#undef CVC4_SYM_ITE_DFN
123
124
template <>
125
5075
traits::ubv orderEncode<traits, traits::ubv>(const traits::ubv &b)
126
{
127
5075
  return orderEncodeBitwise<traits, traits::ubv>(b);
128
}
129
130
template <>
131
26
stickyRightShiftResult<traits> stickyRightShift(const traits::ubv &input,
132
                                                const traits::ubv &shiftAmount)
133
{
134
26
  return stickyRightShiftBitwise<traits>(input, shiftAmount);
135
}
136
137
template <>
138
8585
void probabilityAnnotation<traits, traits::prop>(const traits::prop &p,
139
                                                 const probability &pr)
140
{
141
  // For now, do nothing...
142
8585
  return;
143
}
144
};
145
#endif
146
147
#ifndef CVC4_USE_SYMFPU
148
#define SYMFPU_NUMBER_OF_ROUNDING_MODES 5
149
#endif
150
151
namespace CVC4 {
152
namespace theory {
153
namespace fp {
154
namespace symfpuSymbolic {
155
156
324
symbolicRoundingMode traits::RNE(void) { return symbolicRoundingMode(0x01); };
157
308
symbolicRoundingMode traits::RNA(void) { return symbolicRoundingMode(0x02); };
158
308
symbolicRoundingMode traits::RTP(void) { return symbolicRoundingMode(0x04); };
159
356
symbolicRoundingMode traits::RTN(void) { return symbolicRoundingMode(0x08); };
160
263
symbolicRoundingMode traits::RTZ(void) { return symbolicRoundingMode(0x10); };
161
162
6615
void traits::precondition(const bool b)
163
{
164
6615
  Assert(b);
165
6615
  return;
166
}
167
3356
void traits::postcondition(const bool b)
168
{
169
3356
  Assert(b);
170
3356
  return;
171
}
172
56457
void traits::invariant(const bool b)
173
{
174
56457
  Assert(b);
175
56457
  return;
176
}
177
178
5494
void traits::precondition(const prop &p) { return; }
179
5499
void traits::postcondition(const prop &p) { return; }
180
17013
void traits::invariant(const prop &p) { return; }
181
// This allows us to use the symfpu literal / symbolic assertions in the
182
// symbolic back-end
183
typedef traits t;
184
185
539016
bool symbolicProposition::checkNodeType(const TNode node)
186
{
187
1078032
  TypeNode tn = node.getType(false);
188
1078032
  return tn.isBitVector() && tn.getBitVectorSize() == 1;
189
}
190
191
507980
symbolicProposition::symbolicProposition(const Node n) : nodeWrapper(n)
192
{
193
507980
  Assert(checkNodeType(*this));
194
507980
}  // Only used within this header so could be friend'd
195
20597
symbolicProposition::symbolicProposition(bool v)
196
    : nodeWrapper(
197
20597
          NodeManager::currentNM()->mkConst(BitVector(1U, (v ? 1U : 0U))))
198
{
199
20597
  Assert(checkNodeType(*this));
200
20597
}
201
202
10439
symbolicProposition::symbolicProposition(const symbolicProposition &old)
203
10439
    : nodeWrapper(old)
204
{
205
10439
  Assert(checkNodeType(*this));
206
10439
}
207
208
60396
symbolicProposition symbolicProposition::operator!(void)const
209
{
210
  return symbolicProposition(
211
60396
      NodeManager::currentNM()->mkNode(kind::BITVECTOR_NOT, *this));
212
}
213
214
82367
symbolicProposition symbolicProposition::operator&&(
215
    const symbolicProposition &op) const
216
{
217
  return symbolicProposition(
218
82367
      NodeManager::currentNM()->mkNode(kind::BITVECTOR_AND, *this, op));
219
}
220
221
135527
symbolicProposition symbolicProposition::operator||(
222
    const symbolicProposition &op) const
223
{
224
  return symbolicProposition(
225
135527
      NodeManager::currentNM()->mkNode(kind::BITVECTOR_OR, *this, op));
226
}
227
228
10027
symbolicProposition symbolicProposition::operator==(
229
    const symbolicProposition &op) const
230
{
231
  return symbolicProposition(
232
10027
      NodeManager::currentNM()->mkNode(kind::BITVECTOR_COMP, *this, op));
233
}
234
235
171
symbolicProposition symbolicProposition::operator^(
236
    const symbolicProposition &op) const
237
{
238
  return symbolicProposition(
239
171
      NodeManager::currentNM()->mkNode(kind::BITVECTOR_XOR, *this, op));
240
}
241
242
1640
bool symbolicRoundingMode::checkNodeType(const TNode n)
243
{
244
#ifdef CVC4_USE_SYMFPU
245
1640
  return n.getType(false).isBitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES);
246
#else
247
  return false;
248
#endif
249
}
250
251
15
symbolicRoundingMode::symbolicRoundingMode(const Node n) : nodeWrapper(n)
252
{
253
15
  Assert(checkNodeType(*this));
254
15
}
255
256
#ifdef CVC4_USE_SYMFPU
257
1559
symbolicRoundingMode::symbolicRoundingMode(const unsigned v)
258
4677
    : nodeWrapper(NodeManager::currentNM()->mkConst(
259
6236
          BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, v)))
260
{
261
1559
  Assert((v & (v - 1)) == 0 && v != 0);  // Exactly one bit set
262
1559
  Assert(checkNodeType(*this));
263
1559
}
264
#else
265
symbolicRoundingMode::symbolicRoundingMode(const unsigned v)
266
    : nodeWrapper(NodeManager::currentNM()->mkConst(
267
          BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, v)))
268
{
269
  Unreachable();
270
}
271
#endif
272
273
66
symbolicRoundingMode::symbolicRoundingMode(const symbolicRoundingMode &old)
274
66
    : nodeWrapper(old)
275
{
276
66
  Assert(checkNodeType(*this));
277
66
}
278
279
15
symbolicProposition symbolicRoundingMode::valid(void) const
280
{
281
15
  NodeManager *nm = NodeManager::currentNM();
282
30
  Node zero(nm->mkConst(BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, 0u)));
283
284
  // Is there a better encoding of this?
285
60
  return symbolicProposition(nm->mkNode(
286
      kind::BITVECTOR_AND,
287
60
      nm->mkNode(
288
          kind::BITVECTOR_COMP,
289
30
          nm->mkNode(kind::BITVECTOR_AND,
290
                     *this,
291
30
                     nm->mkNode(kind::BITVECTOR_SUB,
292
                                *this,
293
30
                                nm->mkConst(BitVector(
294
                                    SYMFPU_NUMBER_OF_ROUNDING_MODES, 1u)))),
295
          zero),
296
30
      nm->mkNode(kind::BITVECTOR_NOT,
297
60
                 nm->mkNode(kind::BITVECTOR_COMP, *this, zero))));
298
}
299
300
776
symbolicProposition symbolicRoundingMode::operator==(
301
    const symbolicRoundingMode &op) const
302
{
303
  return symbolicProposition(
304
776
      NodeManager::currentNM()->mkNode(kind::BITVECTOR_COMP, *this, op));
305
}
306
307
template <bool isSigned>
308
Node symbolicBitVector<isSigned>::boolNodeToBV(Node node) const
309
{
310
  Assert(node.getType().isBoolean());
311
  NodeManager *nm = NodeManager::currentNM();
312
  return nm->mkNode(kind::ITE,
313
                    node,
314
                    nm->mkConst(BitVector(1U, 1U)),
315
                    nm->mkConst(BitVector(1U, 0U)));
316
}
317
318
template <bool isSigned>
319
Node symbolicBitVector<isSigned>::BVToBoolNode(Node node) const
320
{
321
  Assert(node.getType().isBitVector());
322
  Assert(node.getType().getBitVectorSize() == 1);
323
  NodeManager *nm = NodeManager::currentNM();
324
  return nm->mkNode(kind::EQUAL, node, nm->mkConst(BitVector(1U, 1U)));
325
}
326
327
template <bool isSigned>
328
61764
Node symbolicBitVector<isSigned>::fromProposition(Node node) const
329
{
330
61764
  return node;
331
}
332
template <bool isSigned>
333
Node symbolicBitVector<isSigned>::toProposition(Node node) const
334
{
335
  return boolNodeToBV(node);
336
}
337
338
template <bool isSigned>
339
537063
symbolicBitVector<isSigned>::symbolicBitVector(const Node n) : nodeWrapper(n)
340
{
341
537063
  Assert(checkNodeType(*this));
342
537063
}
343
344
template <bool isSigned>
345
839275
bool symbolicBitVector<isSigned>::checkNodeType(const TNode n)
346
{
347
839275
  return n.getType(false).isBitVector();
348
}
349
350
template <bool isSigned>
351
286329
symbolicBitVector<isSigned>::symbolicBitVector(const bwt w, const unsigned v)
352
286329
    : nodeWrapper(NodeManager::currentNM()->mkConst(BitVector(w, v)))
353
{
354
286329
  Assert(checkNodeType(*this));
355
286329
}
356
template <bool isSigned>
357
61764
symbolicBitVector<isSigned>::symbolicBitVector(const symbolicProposition &p)
358
61764
    : nodeWrapper(fromProposition(p))
359
{
360
61764
}
361
template <bool isSigned>
362
15359
symbolicBitVector<isSigned>::symbolicBitVector(
363
    const symbolicBitVector<isSigned> &old)
364
15359
    : nodeWrapper(old)
365
{
366
15359
  Assert(checkNodeType(*this));
367
15359
}
368
template <bool isSigned>
369
524
symbolicBitVector<isSigned>::symbolicBitVector(const BitVector &old)
370
524
    : nodeWrapper(NodeManager::currentNM()->mkConst(old))
371
{
372
524
  Assert(checkNodeType(*this));
373
524
}
374
375
template <bool isSigned>
376
90020
bwt symbolicBitVector<isSigned>::getWidth(void) const
377
{
378
90020
  return this->getType(false).getBitVectorSize();
379
}
380
381
/*** Constant creation and test ***/
382
template <bool isSigned>
383
98905
symbolicBitVector<isSigned> symbolicBitVector<isSigned>::one(const bwt &w)
384
{
385
98905
  return symbolicBitVector<isSigned>(w, 1);
386
}
387
template <bool isSigned>
388
42176
symbolicBitVector<isSigned> symbolicBitVector<isSigned>::zero(const bwt &w)
389
{
390
42176
  return symbolicBitVector<isSigned>(w, 0);
391
}
392
template <bool isSigned>
393
4914
symbolicBitVector<isSigned> symbolicBitVector<isSigned>::allOnes(const bwt &w)
394
{
395
4914
  return symbolicBitVector<isSigned>(~zero(w));
396
}
397
398
template <bool isSigned>
399
1262
symbolicProposition symbolicBitVector<isSigned>::isAllOnes() const
400
{
401
1262
  return (*this == symbolicBitVector<isSigned>::allOnes(this->getWidth()));
402
}
403
template <bool isSigned>
404
11191
symbolicProposition symbolicBitVector<isSigned>::isAllZeros() const
405
{
406
11191
  return (*this == symbolicBitVector<isSigned>::zero(this->getWidth()));
407
}
408
409
template <>
410
61
symbolicBitVector<true> symbolicBitVector<true>::maxValue(const bwt &w)
411
{
412
122
  symbolicBitVector<true> leadingZero(symbolicBitVector<true>::zero(1));
413
122
  symbolicBitVector<true> base(symbolicBitVector<true>::allOnes(w - 1));
414
415
122
  return symbolicBitVector<true>(::CVC4::NodeManager::currentNM()->mkNode(
416
122
      ::CVC4::kind::BITVECTOR_CONCAT, leadingZero, base));
417
}
418
419
template <>
420
symbolicBitVector<false> symbolicBitVector<false>::maxValue(const bwt &w)
421
{
422
  return symbolicBitVector<false>::allOnes(w);
423
}
424
425
template <>
426
6
symbolicBitVector<true> symbolicBitVector<true>::minValue(const bwt &w)
427
{
428
12
  symbolicBitVector<true> leadingOne(symbolicBitVector<true>::one(1));
429
12
  symbolicBitVector<true> base(symbolicBitVector<true>::zero(w - 1));
430
431
12
  return symbolicBitVector<true>(::CVC4::NodeManager::currentNM()->mkNode(
432
12
      ::CVC4::kind::BITVECTOR_CONCAT, leadingOne, base));
433
}
434
435
template <>
436
symbolicBitVector<false> symbolicBitVector<false>::minValue(const bwt &w)
437
{
438
  return symbolicBitVector<false>::zero(w);
439
}
440
441
/*** Operators ***/
442
template <bool isSigned>
443
73632
symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator<<(
444
    const symbolicBitVector<isSigned> &op) const
445
{
446
  return symbolicBitVector<isSigned>(
447
73632
      NodeManager::currentNM()->mkNode(kind::BITVECTOR_SHL, *this, op));
448
}
449
450
template <bool isSigned>
451
3393
symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator>>(
452
    const symbolicBitVector<isSigned> &op) const
453
{
454
  return symbolicBitVector<isSigned>(NodeManager::currentNM()->mkNode(
455
3393
      (isSigned) ? kind::BITVECTOR_ASHR : kind::BITVECTOR_LSHR, *this, op));
456
}
457
458
template <bool isSigned>
459
53199
symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator|(
460
    const symbolicBitVector<isSigned> &op) const
461
{
462
  return symbolicBitVector<isSigned>(
463
53199
      NodeManager::currentNM()->mkNode(kind::BITVECTOR_OR, *this, op));
464
}
465
466
template <bool isSigned>
467
10673
symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator&(
468
    const symbolicBitVector<isSigned> &op) const
469
{
470
  return symbolicBitVector<isSigned>(
471
10673
      NodeManager::currentNM()->mkNode(kind::BITVECTOR_AND, *this, op));
472
}
473
474
template <bool isSigned>
475
4145
symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator+(
476
    const symbolicBitVector<isSigned> &op) const
477
{
478
  return symbolicBitVector<isSigned>(
479
4145
      NodeManager::currentNM()->mkNode(kind::BITVECTOR_PLUS, *this, op));
480
}
481
482
template <bool isSigned>
483
95676
symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator-(
484
    const symbolicBitVector<isSigned> &op) const
485
{
486
  return symbolicBitVector<isSigned>(
487
95676
      NodeManager::currentNM()->mkNode(kind::BITVECTOR_SUB, *this, op));
488
}
489
490
template <bool isSigned>
491
9
symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator*(
492
    const symbolicBitVector<isSigned> &op) const
493
{
494
  return symbolicBitVector<isSigned>(
495
9
      NodeManager::currentNM()->mkNode(kind::BITVECTOR_MULT, *this, op));
496
}
497
498
template <bool isSigned>
499
6
symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator/(
500
    const symbolicBitVector<isSigned> &op) const
501
{
502
  return symbolicBitVector<isSigned>(NodeManager::currentNM()->mkNode(
503
6
      (isSigned) ? kind::BITVECTOR_SDIV : kind::BITVECTOR_UDIV, *this, op));
504
}
505
506
template <bool isSigned>
507
6
symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator%(
508
    const symbolicBitVector<isSigned> &op) const
509
{
510
  return symbolicBitVector<isSigned>(NodeManager::currentNM()->mkNode(
511
6
      (isSigned) ? kind::BITVECTOR_SREM : kind::BITVECTOR_UREM, *this, op));
512
}
513
514
template <bool isSigned>
515
42590
symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator-(void) const
516
{
517
  return symbolicBitVector<isSigned>(
518
42590
      NodeManager::currentNM()->mkNode(kind::BITVECTOR_NEG, *this));
519
}
520
521
template <bool isSigned>
522
5083
symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator~(void)const
523
{
524
  return symbolicBitVector<isSigned>(
525
5083
      NodeManager::currentNM()->mkNode(kind::BITVECTOR_NOT, *this));
526
}
527
528
template <bool isSigned>
529
20
symbolicBitVector<isSigned> symbolicBitVector<isSigned>::increment() const
530
{
531
  return symbolicBitVector<isSigned>(NodeManager::currentNM()->mkNode(
532
20
      kind::BITVECTOR_PLUS, *this, one(this->getWidth())));
533
}
534
535
template <bool isSigned>
536
5177
symbolicBitVector<isSigned> symbolicBitVector<isSigned>::decrement() const
537
{
538
  return symbolicBitVector<isSigned>(NodeManager::currentNM()->mkNode(
539
5177
      kind::BITVECTOR_SUB, *this, one(this->getWidth())));
540
}
541
542
template <bool isSigned>
543
188
symbolicBitVector<isSigned> symbolicBitVector<isSigned>::signExtendRightShift(
544
    const symbolicBitVector<isSigned> &op) const
545
{
546
  return symbolicBitVector<isSigned>(
547
188
      NodeManager::currentNM()->mkNode(kind::BITVECTOR_ASHR, *this, op));
548
}
549
550
/*** Modular operations ***/
551
// No overflow checking so these are the same as other operations
552
template <bool isSigned>
553
5401
symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularLeftShift(
554
    const symbolicBitVector<isSigned> &op) const
555
{
556
5401
  return *this << op;
557
}
558
559
template <bool isSigned>
560
26
symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularRightShift(
561
    const symbolicBitVector<isSigned> &op) const
562
{
563
26
  return *this >> op;
564
}
565
566
template <bool isSigned>
567
symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularIncrement()
568
    const
569
{
570
  return this->increment();
571
}
572
573
template <bool isSigned>
574
5075
symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularDecrement()
575
    const
576
{
577
5075
  return this->decrement();
578
}
579
580
template <bool isSigned>
581
682
symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularAdd(
582
    const symbolicBitVector<isSigned> &op) const
583
{
584
682
  return *this + op;
585
}
586
587
template <bool isSigned>
588
673
symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularNegate() const
589
{
590
673
  return -(*this);
591
}
592
593
/*** Comparisons ***/
594
595
template <bool isSigned>
596
147433
symbolicProposition symbolicBitVector<isSigned>::operator==(
597
    const symbolicBitVector<isSigned> &op) const
598
{
599
  return symbolicProposition(
600
147433
      NodeManager::currentNM()->mkNode(kind::BITVECTOR_COMP, *this, op));
601
}
602
603
template <bool isSigned>
604
60015
symbolicProposition symbolicBitVector<isSigned>::operator<=(
605
    const symbolicBitVector<isSigned> &op) const
606
{
607
  // Consider adding kind::BITVECTOR_SLEBV and BITVECTOR_ULEBV
608
60015
  return (*this < op) || (*this == op);
609
}
610
611
template <bool isSigned>
612
5889
symbolicProposition symbolicBitVector<isSigned>::operator>=(
613
    const symbolicBitVector<isSigned> &op) const
614
{
615
5889
  return (*this > op) || (*this == op);
616
}
617
618
template <bool isSigned>
619
60484
symbolicProposition symbolicBitVector<isSigned>::operator<(
620
    const symbolicBitVector<isSigned> &op) const
621
{
622
  return symbolicProposition(NodeManager::currentNM()->mkNode(
623
60484
      (isSigned) ? kind::BITVECTOR_SLTBV : kind::BITVECTOR_ULTBV, *this, op));
624
}
625
626
template <bool isSigned>
627
6673
symbolicProposition symbolicBitVector<isSigned>::operator>(
628
    const symbolicBitVector<isSigned> &op) const
629
{
630
  return symbolicProposition(NodeManager::currentNM()->mkNode(
631
6673
      (isSigned) ? kind::BITVECTOR_SLTBV : kind::BITVECTOR_ULTBV, op, *this));
632
}
633
634
/*** Type conversion ***/
635
// CVC4 nodes make no distinction between signed and unsigned, thus ...
636
template <bool isSigned>
637
64
symbolicBitVector<true> symbolicBitVector<isSigned>::toSigned(void) const
638
{
639
64
  return symbolicBitVector<true>(*this);
640
}
641
template <bool isSigned>
642
11733
symbolicBitVector<false> symbolicBitVector<isSigned>::toUnsigned(void) const
643
{
644
11733
  return symbolicBitVector<false>(*this);
645
}
646
647
/*** Bit hacks ***/
648
template <>
649
697
symbolicBitVector<true> symbolicBitVector<true>::extend(bwt extension) const
650
{
651
1394
  NodeBuilder<> construct(kind::BITVECTOR_SIGN_EXTEND);
652
2091
  construct << NodeManager::currentNM()->mkConst<BitVectorSignExtend>(
653
2788
                   BitVectorSignExtend(extension))
654
697
            << *this;
655
656
1394
  return symbolicBitVector<true>(construct);
657
}
658
659
template <>
660
13882
symbolicBitVector<false> symbolicBitVector<false>::extend(bwt extension) const
661
{
662
27764
  NodeBuilder<> construct(kind::BITVECTOR_ZERO_EXTEND);
663
41646
  construct << NodeManager::currentNM()->mkConst<BitVectorZeroExtend>(
664
55528
                   BitVectorZeroExtend(extension))
665
13882
            << *this;
666
667
27764
  return symbolicBitVector<false>(construct);
668
}
669
670
template <bool isSigned>
671
67
symbolicBitVector<isSigned> symbolicBitVector<isSigned>::contract(
672
    bwt reduction) const
673
{
674
67
  Assert(this->getWidth() > reduction);
675
676
134
  NodeBuilder<> construct(kind::BITVECTOR_EXTRACT);
677
268
  construct << NodeManager::currentNM()->mkConst<BitVectorExtract>(
678
67
                   BitVectorExtract((this->getWidth() - 1) - reduction, 0))
679
134
            << *this;
680
681
134
  return symbolicBitVector<isSigned>(construct);
682
}
683
684
template <bool isSigned>
685
5151
symbolicBitVector<isSigned> symbolicBitVector<isSigned>::resize(
686
    bwt newSize) const
687
{
688
5151
  bwt width = this->getWidth();
689
690
5151
  if (newSize > width)
691
  {
692
5151
    return this->extend(newSize - width);
693
  }
694
  else if (newSize < width)
695
  {
696
    return this->contract(width - newSize);
697
  }
698
  else
699
  {
700
    return *this;
701
  }
702
}
703
704
template <bool isSigned>
705
8609
symbolicBitVector<isSigned> symbolicBitVector<isSigned>::matchWidth(
706
    const symbolicBitVector<isSigned> &op) const
707
{
708
8609
  Assert(this->getWidth() <= op.getWidth());
709
8609
  return this->extend(op.getWidth() - this->getWidth());
710
}
711
712
template <bool isSigned>
713
60186
symbolicBitVector<isSigned> symbolicBitVector<isSigned>::append(
714
    const symbolicBitVector<isSigned> &op) const
715
{
716
  return symbolicBitVector<isSigned>(
717
60186
      NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, *this, op));
718
}
719
720
// Inclusive of end points, thus if the same, extracts just one bit
721
template <bool isSigned>
722
127850
symbolicBitVector<isSigned> symbolicBitVector<isSigned>::extract(
723
    bwt upper, bwt lower) const
724
{
725
127850
  Assert(upper >= lower);
726
727
255700
  NodeBuilder<> construct(kind::BITVECTOR_EXTRACT);
728
383550
  construct << NodeManager::currentNM()->mkConst<BitVectorExtract>(
729
                   BitVectorExtract(upper, lower))
730
255700
            << *this;
731
732
255700
  return symbolicBitVector<isSigned>(construct);
733
}
734
735
4086
floatingPointTypeInfo::floatingPointTypeInfo(const TypeNode type)
736
4086
    : FloatingPointSize(type.getConst<FloatingPointSize>())
737
{
738
4086
  Assert(type.isFloatingPoint());
739
4086
}
740
41
floatingPointTypeInfo::floatingPointTypeInfo(unsigned exp, unsigned sig)
741
41
    : FloatingPointSize(exp, sig)
742
{
743
41
}
744
floatingPointTypeInfo::floatingPointTypeInfo(const floatingPointTypeInfo &old)
745
    : FloatingPointSize(old)
746
{
747
}
748
749
3306
TypeNode floatingPointTypeInfo::getTypeNode(void) const
750
{
751
3306
  return NodeManager::currentNM()->mkFloatingPointType(*this);
752
}
753
}
754
755
8995
FpConverter::FpConverter(context::UserContext* user)
756
    : d_additionalAssertions(user)
757
#ifdef CVC4_USE_SYMFPU
758
      ,
759
      d_fpMap(user),
760
      d_rmMap(user),
761
      d_boolMap(user),
762
      d_ubvMap(user),
763
8995
      d_sbvMap(user)
764
#endif
765
{
766
8995
}
767
768
8992
FpConverter::~FpConverter() {}
769
770
#ifdef CVC4_USE_SYMFPU
771
3306
Node FpConverter::ufToNode(const fpt &format, const uf &u) const
772
{
773
3306
  NodeManager *nm = NodeManager::currentNM();
774
775
3306
  FloatingPointSize fps(format.getTypeNode().getConst<FloatingPointSize>());
776
777
  // This is not entirely obvious but it builds a float from components
778
  // Particularly, if the components can be constant folded, it should
779
  // build a Node containing a constant FloatingPoint number
780
781
6612
  ubv packed(symfpu::pack<traits>(format, u));
782
  Node value =
783
3306
      nm->mkNode(nm->mkConst(FloatingPointToFPIEEEBitVector(fps)), packed);
784
6612
  return value;
785
}
786
787
151
Node FpConverter::rmToNode(const rm &r) const
788
{
789
151
  NodeManager *nm = NodeManager::currentNM();
790
791
302
  Node transVar = r;
792
793
302
  Node RNE = traits::RNE();
794
302
  Node RNA = traits::RNA();
795
302
  Node RTP = traits::RTP();
796
302
  Node RTN = traits::RTN();
797
302
  Node RTZ = traits::RTZ();
798
799
  Node value = nm->mkNode(
800
      kind::ITE,
801
302
      nm->mkNode(kind::EQUAL, transVar, RNE),
802
302
      nm->mkConst(ROUND_NEAREST_TIES_TO_EVEN),
803
906
      nm->mkNode(kind::ITE,
804
302
                 nm->mkNode(kind::EQUAL, transVar, RNA),
805
302
                 nm->mkConst(ROUND_NEAREST_TIES_TO_AWAY),
806
906
                 nm->mkNode(kind::ITE,
807
302
                            nm->mkNode(kind::EQUAL, transVar, RTP),
808
302
                            nm->mkConst(ROUND_TOWARD_POSITIVE),
809
906
                            nm->mkNode(kind::ITE,
810
302
                                       nm->mkNode(kind::EQUAL, transVar, RTN),
811
302
                                       nm->mkConst(ROUND_TOWARD_NEGATIVE),
812
1057
                                       nm->mkConst(ROUND_TOWARD_ZERO)))));
813
302
  return value;
814
}
815
816
Node FpConverter::propToNode(const prop &p) const
817
{
818
  NodeManager *nm = NodeManager::currentNM();
819
  Node value =
820
      nm->mkNode(kind::EQUAL, p, nm->mkConst(::CVC4::BitVector(1U, 1U)));
821
  return value;
822
}
823
Node FpConverter::ubvToNode(const ubv &u) const { return u; }
824
Node FpConverter::sbvToNode(const sbv &s) const { return s; }
825
// Creates the components constraint
826
135
FpConverter::uf FpConverter::buildComponents(TNode current)
827
{
828
135
  Assert(Theory::isLeafOf(current, THEORY_FP)
829
         || current.getKind() == kind::FLOATINGPOINT_TO_FP_REAL);
830
831
135
  NodeManager *nm = NodeManager::currentNM();
832
270
  uf tmp(nm->mkNode(kind::FLOATINGPOINT_COMPONENT_NAN, current),
833
270
         nm->mkNode(kind::FLOATINGPOINT_COMPONENT_INF, current),
834
270
         nm->mkNode(kind::FLOATINGPOINT_COMPONENT_ZERO, current),
835
270
         nm->mkNode(kind::FLOATINGPOINT_COMPONENT_SIGN, current),
836
270
         nm->mkNode(kind::FLOATINGPOINT_COMPONENT_EXPONENT, current),
837
1485
         nm->mkNode(kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND, current));
838
839
135
  d_additionalAssertions.push_back(tmp.valid(fpt(current.getType())));
840
841
135
  return tmp;
842
}
843
#endif
844
845
// Non-convertible things should only be added to the stack at the very start,
846
// thus...
847
#define CVC4_FPCONV_PASSTHROUGH Assert(workStack.empty())
848
849
2176
Node FpConverter::convert(TNode node)
850
{
851
#ifdef CVC4_USE_SYMFPU
852
4352
  std::vector<TNode> workStack;
853
4352
  TNode result = node;
854
855
2176
  workStack.push_back(node);
856
857
2176
  NodeManager *nm = NodeManager::currentNM();
858
859
6008
  while (!workStack.empty())
860
  {
861
4092
    TNode current = workStack.back();
862
2176
    workStack.pop_back();
863
2176
    result = current;
864
865
4092
    TypeNode t(current.getType());
866
867
2176
    if (t.isRoundingMode())
868
    {
869
33
      rmMap::const_iterator i(d_rmMap.find(current));
870
871
33
      if (i == d_rmMap.end())
872
      {
873
33
        if (Theory::isLeafOf(current, THEORY_FP))
874
        {
875
33
          if (current.getKind() == kind::CONST_ROUNDINGMODE)
876
          {
877
            /******** Constants ********/
878
18
            switch (current.getConst<RoundingMode>())
879
            {
880
10
              case ROUND_NEAREST_TIES_TO_EVEN:
881
10
                d_rmMap.insert(current, traits::RNE());
882
10
                break;
883
4
              case ROUND_NEAREST_TIES_TO_AWAY:
884
4
                d_rmMap.insert(current, traits::RNA());
885
4
                break;
886
4
              case ROUND_TOWARD_POSITIVE:
887
4
                d_rmMap.insert(current, traits::RTP());
888
4
                break;
889
              case ROUND_TOWARD_NEGATIVE:
890
                d_rmMap.insert(current, traits::RTN());
891
                break;
892
              case ROUND_TOWARD_ZERO:
893
                d_rmMap.insert(current, traits::RTZ());
894
                break;
895
              default: Unreachable() << "Unknown rounding mode"; break;
896
            }
897
          }
898
          else
899
          {
900
            /******** Variables ********/
901
30
            rm tmp(nm->mkNode(kind::ROUNDINGMODE_BITBLAST, current));
902
15
            d_rmMap.insert(current, tmp);
903
15
            d_additionalAssertions.push_back(tmp.valid());
904
          }
905
        }
906
        else
907
        {
908
          Unreachable() << "Unknown kind of type RoundingMode";
909
        }
910
      }
911
      // Returns a rounding-mode type so don't alter the return value
912
    }
913
2143
    else if (t.isFloatingPoint())
914
    {
915
491
      fpMap::const_iterator i(d_fpMap.find(current));
916
917
491
      if (i == d_fpMap.end())
918
      {
919
491
        if (Theory::isLeafOf(current, THEORY_FP))
920
        {
921
397
          if (current.getKind() == kind::CONST_FLOATINGPOINT)
922
          {
923
            /******** Constants ********/
924
524
            d_fpMap.insert(
925
                current,
926
786
                symfpu::unpackedFloat<traits>(current.getConst<FloatingPoint>()
927
                                                  .getLiteral()
928
262
                                                  ->getSymUF()));
929
          }
930
          else
931
          {
932
            /******** Variables ********/
933
135
            d_fpMap.insert(current, buildComponents(current));
934
          }
935
        }
936
        else
937
        {
938
94
          switch (current.getKind())
939
          {
940
            case kind::CONST_FLOATINGPOINT:
941
            case kind::VARIABLE:
942
            case kind::BOUND_VARIABLE:
943
            case kind::SKOLEM:
944
              Unreachable() << "Kind should have been handled as a leaf.";
945
              break;
946
947
            /******** Operations ********/
948
17
            case kind::FLOATINGPOINT_ABS:
949
            case kind::FLOATINGPOINT_NEG:
950
            {
951
17
              fpMap::const_iterator arg1(d_fpMap.find(current[0]));
952
953
17
              if (arg1 == d_fpMap.end())
954
              {
955
                workStack.push_back(current);
956
                workStack.push_back(current[0]);
957
                continue;  // i.e. recurse!
958
              }
959
960
17
              switch (current.getKind())
961
              {
962
9
                case kind::FLOATINGPOINT_ABS:
963
18
                  d_fpMap.insert(current,
964
27
                                 symfpu::absolute<traits>(
965
27
                                     fpt(current.getType()), (*arg1).second));
966
9
                  break;
967
8
                case kind::FLOATINGPOINT_NEG:
968
16
                  d_fpMap.insert(current,
969
16
                                 symfpu::negate<traits>(fpt(current.getType()),
970
8
                                                        (*arg1).second));
971
8
                  break;
972
                default:
973
                  Unreachable() << "Unknown unary floating-point function";
974
                  break;
975
17
              }
976
            }
977
17
            break;
978
979
20
            case kind::FLOATINGPOINT_SQRT:
980
            case kind::FLOATINGPOINT_RTI:
981
            {
982
20
              rmMap::const_iterator mode(d_rmMap.find(current[0]));
983
20
              fpMap::const_iterator arg1(d_fpMap.find(current[1]));
984
              bool recurseNeeded =
985
20
                  (mode == d_rmMap.end()) || (arg1 == d_fpMap.end());
986
987
20
              if (recurseNeeded)
988
              {
989
                workStack.push_back(current);
990
                if (mode == d_rmMap.end())
991
                {
992
                  workStack.push_back(current[0]);
993
                }
994
                if (arg1 == d_fpMap.end())
995
                {
996
                  workStack.push_back(current[1]);
997
                }
998
                continue;  // i.e. recurse!
999
              }
1000
1001
20
              switch (current.getKind())
1002
              {
1003
                case kind::FLOATINGPOINT_SQRT:
1004
                  d_fpMap.insert(current,
1005
                                 symfpu::sqrt<traits>(fpt(current.getType()),
1006
                                                      (*mode).second,
1007
                                                      (*arg1).second));
1008
                  break;
1009
20
                case kind::FLOATINGPOINT_RTI:
1010
40
                  d_fpMap.insert(
1011
                      current,
1012
60
                      symfpu::roundToIntegral<traits>(fpt(current.getType()),
1013
20
                                                      (*mode).second,
1014
20
                                                      (*arg1).second));
1015
20
                  break;
1016
                default:
1017
                  Unreachable()
1018
                      << "Unknown unary rounded floating-point function";
1019
                  break;
1020
20
              }
1021
            }
1022
20
            break;
1023
1024
10
            case kind::FLOATINGPOINT_REM:
1025
            {
1026
10
              fpMap::const_iterator arg1(d_fpMap.find(current[0]));
1027
10
              fpMap::const_iterator arg2(d_fpMap.find(current[1]));
1028
              bool recurseNeeded =
1029
10
                  (arg1 == d_fpMap.end()) || (arg2 == d_fpMap.end());
1030
1031
10
              if (recurseNeeded)
1032
              {
1033
                workStack.push_back(current);
1034
                if (arg1 == d_fpMap.end())
1035
                {
1036
                  workStack.push_back(current[0]);
1037
                }
1038
                if (arg2 == d_fpMap.end())
1039
                {
1040
                  workStack.push_back(current[1]);
1041
                }
1042
                continue;  // i.e. recurse!
1043
              }
1044
1045
20
              d_fpMap.insert(
1046
                  current,
1047
40
                  symfpu::remainder<traits>(
1048
40
                      fpt(current.getType()), (*arg1).second, (*arg2).second));
1049
            }
1050
10
            break;
1051
1052
            case kind::FLOATINGPOINT_MIN_TOTAL:
1053
            case kind::FLOATINGPOINT_MAX_TOTAL:
1054
            {
1055
              fpMap::const_iterator arg1(d_fpMap.find(current[0]));
1056
              fpMap::const_iterator arg2(d_fpMap.find(current[1]));
1057
              // current[2] is a bit-vector so we do not need to recurse down it
1058
1059
              bool recurseNeeded =
1060
                  (arg1 == d_fpMap.end()) || (arg2 == d_fpMap.end());
1061
1062
              if (recurseNeeded)
1063
              {
1064
                workStack.push_back(current);
1065
                if (arg1 == d_fpMap.end())
1066
                {
1067
                  workStack.push_back(current[0]);
1068
                }
1069
                if (arg2 == d_fpMap.end())
1070
                {
1071
                  workStack.push_back(current[1]);
1072
                }
1073
                continue;  // i.e. recurse!
1074
              }
1075
1076
              switch (current.getKind())
1077
              {
1078
                case kind::FLOATINGPOINT_MAX_TOTAL:
1079
                  d_fpMap.insert(current,
1080
                                 symfpu::max<traits>(fpt(current.getType()),
1081
                                                     (*arg1).second,
1082
                                                     (*arg2).second,
1083
                                                     prop(current[2])));
1084
                  break;
1085
1086
                case kind::FLOATINGPOINT_MIN_TOTAL:
1087
                  d_fpMap.insert(current,
1088
                                 symfpu::min<traits>(fpt(current.getType()),
1089
                                                     (*arg1).second,
1090
                                                     (*arg2).second,
1091
                                                     prop(current[2])));
1092
                  break;
1093
1094
                default:
1095
                  Unreachable()
1096
                      << "Unknown binary floating-point partial function";
1097
                  break;
1098
              }
1099
            }
1100
            break;
1101
1102
31
            case kind::FLOATINGPOINT_PLUS:
1103
            case kind::FLOATINGPOINT_SUB:
1104
            case kind::FLOATINGPOINT_MULT:
1105
            case kind::FLOATINGPOINT_DIV:
1106
            {
1107
31
              rmMap::const_iterator mode(d_rmMap.find(current[0]));
1108
31
              fpMap::const_iterator arg1(d_fpMap.find(current[1]));
1109
31
              fpMap::const_iterator arg2(d_fpMap.find(current[2]));
1110
62
              bool recurseNeeded = (mode == d_rmMap.end())
1111
62
                                   || (arg1 == d_fpMap.end())
1112
62
                                   || (arg2 == d_fpMap.end());
1113
1114
31
              if (recurseNeeded)
1115
              {
1116
                workStack.push_back(current);
1117
                if (mode == d_rmMap.end())
1118
                {
1119
                  workStack.push_back(current[0]);
1120
                }
1121
                if (arg1 == d_fpMap.end())
1122
                {
1123
                  workStack.push_back(current[1]);
1124
                }
1125
                if (arg2 == d_fpMap.end())
1126
                {
1127
                  workStack.push_back(current[2]);
1128
                }
1129
                continue;  // i.e. recurse!
1130
              }
1131
1132
31
              switch (current.getKind())
1133
              {
1134
16
                case kind::FLOATINGPOINT_PLUS:
1135
32
                  d_fpMap.insert(current,
1136
64
                                 symfpu::add<traits>(fpt(current.getType()),
1137
16
                                                     (*mode).second,
1138
16
                                                     (*arg1).second,
1139
16
                                                     (*arg2).second,
1140
32
                                                     prop(true)));
1141
16
                  break;
1142
1143
                case kind::FLOATINGPOINT_SUB:
1144
                  // Should have been removed by the rewriter
1145
                  Unreachable()
1146
                      << "Floating-point subtraction should be removed by the "
1147
                         "rewriter.";
1148
                  break;
1149
1150
9
                case kind::FLOATINGPOINT_MULT:
1151
18
                  d_fpMap.insert(
1152
                      current,
1153
36
                      symfpu::multiply<traits>(fpt(current.getType()),
1154
9
                                               (*mode).second,
1155
9
                                               (*arg1).second,
1156
9
                                               (*arg2).second));
1157
9
                  break;
1158
6
                case kind::FLOATINGPOINT_DIV:
1159
12
                  d_fpMap.insert(current,
1160
24
                                 symfpu::divide<traits>(fpt(current.getType()),
1161
6
                                                        (*mode).second,
1162
6
                                                        (*arg1).second,
1163
6
                                                        (*arg2).second));
1164
6
                  break;
1165
                case kind::FLOATINGPOINT_REM:
1166
                  /*
1167
                  d_fpMap.insert(current,
1168
                  symfpu::remainder<traits>(fpt(current.getType()),
1169
                                                             (*mode).second,
1170
                                                             (*arg1).second,
1171
                                                             (*arg2).second));
1172
                  */
1173
                  Unimplemented()
1174
                      << "Remainder with rounding mode not yet supported by "
1175
                         "SMT-LIB";
1176
                  break;
1177
1178
                default:
1179
                  Unreachable()
1180
                      << "Unknown binary rounded floating-point function";
1181
                  break;
1182
31
              }
1183
            }
1184
31
            break;
1185
1186
            case kind::FLOATINGPOINT_FMA:
1187
            {
1188
              rmMap::const_iterator mode(d_rmMap.find(current[0]));
1189
              fpMap::const_iterator arg1(d_fpMap.find(current[1]));
1190
              fpMap::const_iterator arg2(d_fpMap.find(current[2]));
1191
              fpMap::const_iterator arg3(d_fpMap.find(current[3]));
1192
              bool recurseNeeded =
1193
                  (mode == d_rmMap.end()) || (arg1 == d_fpMap.end())
1194
                  || (arg2 == d_fpMap.end() || (arg3 == d_fpMap.end()));
1195
1196
              if (recurseNeeded)
1197
              {
1198
                workStack.push_back(current);
1199
                if (mode == d_rmMap.end())
1200
                {
1201
                  workStack.push_back(current[0]);
1202
                }
1203
                if (arg1 == d_fpMap.end())
1204
                {
1205
                  workStack.push_back(current[1]);
1206
                }
1207
                if (arg2 == d_fpMap.end())
1208
                {
1209
                  workStack.push_back(current[2]);
1210
                }
1211
                if (arg3 == d_fpMap.end())
1212
                {
1213
                  workStack.push_back(current[3]);
1214
                }
1215
                continue;  // i.e. recurse!
1216
              }
1217
1218
              d_fpMap.insert(current,
1219
                             symfpu::fma<traits>(fpt(current.getType()),
1220
                                                 (*mode).second,
1221
                                                 (*arg1).second,
1222
                                                 (*arg2).second,
1223
                                                 (*arg3).second));
1224
            }
1225
            break;
1226
1227
            /******** Conversions ********/
1228
2
            case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT:
1229
            {
1230
2
              rmMap::const_iterator mode(d_rmMap.find(current[0]));
1231
2
              fpMap::const_iterator arg1(d_fpMap.find(current[1]));
1232
              bool recurseNeeded =
1233
2
                  (mode == d_rmMap.end()) || (arg1 == d_fpMap.end());
1234
1235
2
              if (recurseNeeded)
1236
              {
1237
                workStack.push_back(current);
1238
                if (mode == d_rmMap.end())
1239
                {
1240
                  workStack.push_back(current[0]);
1241
                }
1242
                if (arg1 == d_fpMap.end())
1243
                {
1244
                  workStack.push_back(current[1]);
1245
                }
1246
                continue;  // i.e. recurse!
1247
              }
1248
1249
4
              d_fpMap.insert(
1250
                  current,
1251
8
                  symfpu::convertFloatToFloat<traits>(fpt(current[1].getType()),
1252
4
                                                      fpt(current.getType()),
1253
2
                                                      (*mode).second,
1254
4
                                                      (*arg1).second));
1255
            }
1256
2
            break;
1257
1258
2
            case kind::FLOATINGPOINT_FP:
1259
            {
1260
              Node IEEEBV(nm->mkNode(
1261
4
                  kind::BITVECTOR_CONCAT, current[0], current[1], current[2]));
1262
4
              d_fpMap.insert(
1263
                  current,
1264
6
                  symfpu::unpack<traits>(fpt(current.getType()), IEEEBV));
1265
            }
1266
2
            break;
1267
1268
12
            case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
1269
24
              d_fpMap.insert(current,
1270
24
                             symfpu::unpack<traits>(fpt(current.getType()),
1271
24
                                                    ubv(current[0])));
1272
12
              break;
1273
1274
            case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
1275
            case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR:
1276
            {
1277
              rmMap::const_iterator mode(d_rmMap.find(current[0]));
1278
              bool recurseNeeded = (mode == d_rmMap.end());
1279
1280
              if (recurseNeeded)
1281
              {
1282
                workStack.push_back(current);
1283
                if (mode == d_rmMap.end())
1284
                {
1285
                  workStack.push_back(current[0]);
1286
                }
1287
                continue;  // i.e. recurse!
1288
              }
1289
1290
              switch (current.getKind())
1291
              {
1292
                case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
1293
                  d_fpMap.insert(
1294
                      current,
1295
                      symfpu::convertSBVToFloat<traits>(fpt(current.getType()),
1296
                                                        (*mode).second,
1297
                                                        sbv(current[1])));
1298
                  break;
1299
1300
                case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR:
1301
                  d_fpMap.insert(
1302
                      current,
1303
                      symfpu::convertUBVToFloat<traits>(fpt(current.getType()),
1304
                                                        (*mode).second,
1305
                                                        ubv(current[1])));
1306
                  break;
1307
1308
                default:
1309
                  Unreachable() << "Unknown converstion from bit-vector to "
1310
                                   "floating-point";
1311
                  break;
1312
              }
1313
            }
1314
            break;
1315
1316
            case kind::FLOATINGPOINT_TO_FP_REAL:
1317
            {
1318
              d_fpMap.insert(current, buildComponents(current));
1319
              // Rely on the real theory and theory combination
1320
              // to handle the value
1321
            }
1322
            break;
1323
1324
            case kind::FLOATINGPOINT_TO_FP_GENERIC:
1325
              Unreachable() << "Generic to_fp not removed";
1326
              break;
1327
1328
            default:
1329
              Unreachable() << "Unknown kind of type FloatingPoint";
1330
              break;
1331
          }
1332
        }
1333
      }
1334
      // Returns a floating-point type so don't alter the return value
1335
    }
1336
1652
    else if (t.isBoolean())
1337
    {
1338
809
      boolMap::const_iterator i(d_boolMap.find(current));
1339
1340
809
      if (i == d_boolMap.end())
1341
      {
1342
809
        switch (current.getKind())
1343
        {
1344
          /******** Comparisons ********/
1345
643
          case kind::EQUAL:
1346
          {
1347
1026
            TypeNode childType(current[0].getType());
1348
1349
643
            if (childType.isFloatingPoint())
1350
            {
1351
383
              fpMap::const_iterator arg1(d_fpMap.find(current[0]));
1352
383
              fpMap::const_iterator arg2(d_fpMap.find(current[1]));
1353
              bool recurseNeeded =
1354
383
                  (arg1 == d_fpMap.end()) || (arg2 == d_fpMap.end());
1355
1356
383
              if (recurseNeeded)
1357
              {
1358
                workStack.push_back(current);
1359
                if (arg1 == d_fpMap.end())
1360
                {
1361
                  workStack.push_back(current[0]);
1362
                }
1363
                if (arg2 == d_fpMap.end())
1364
                {
1365
                  workStack.push_back(current[1]);
1366
                }
1367
                continue;  // i.e. recurse!
1368
              }
1369
1370
766
              d_boolMap.insert(
1371
                  current,
1372
1532
                  symfpu::smtlibEqual<traits>(
1373
1532
                      fpt(childType), (*arg1).second, (*arg2).second));
1374
            }
1375
260
            else if (childType.isRoundingMode())
1376
            {
1377
              rmMap::const_iterator arg1(d_rmMap.find(current[0]));
1378
              rmMap::const_iterator arg2(d_rmMap.find(current[1]));
1379
              bool recurseNeeded =
1380
                  (arg1 == d_rmMap.end()) || (arg2 == d_rmMap.end());
1381
1382
              if (recurseNeeded)
1383
              {
1384
                workStack.push_back(current);
1385
                if (arg1 == d_rmMap.end())
1386
                {
1387
                  workStack.push_back(current[0]);
1388
                }
1389
                if (arg2 == d_rmMap.end())
1390
                {
1391
                  workStack.push_back(current[1]);
1392
                }
1393
                continue;  // i.e. recurse!
1394
              }
1395
1396
              d_boolMap.insert(current, (*arg1).second == (*arg2).second);
1397
            }
1398
            else
1399
            {
1400
260
              CVC4_FPCONV_PASSTHROUGH;
1401
260
              return result;
1402
383
            }
1403
          }
1404
383
          break;
1405
1406
48
          case kind::FLOATINGPOINT_LEQ:
1407
          case kind::FLOATINGPOINT_LT:
1408
          {
1409
96
            TypeNode childType(current[0].getType());
1410
1411
48
            fpMap::const_iterator arg1(d_fpMap.find(current[0]));
1412
48
            fpMap::const_iterator arg2(d_fpMap.find(current[1]));
1413
            bool recurseNeeded =
1414
48
                (arg1 == d_fpMap.end()) || (arg2 == d_fpMap.end());
1415
1416
48
            if (recurseNeeded)
1417
            {
1418
              workStack.push_back(current);
1419
              if (arg1 == d_fpMap.end())
1420
              {
1421
                workStack.push_back(current[0]);
1422
              }
1423
              if (arg2 == d_fpMap.end())
1424
              {
1425
                workStack.push_back(current[1]);
1426
              }
1427
              continue;  // i.e. recurse!
1428
            }
1429
1430
48
            switch (current.getKind())
1431
            {
1432
44
              case kind::FLOATINGPOINT_LEQ:
1433
88
                d_boolMap.insert(
1434
                    current,
1435
176
                    symfpu::lessThanOrEqual<traits>(
1436
176
                        fpt(childType), (*arg1).second, (*arg2).second));
1437
44
                break;
1438
1439
4
              case kind::FLOATINGPOINT_LT:
1440
8
                d_boolMap.insert(
1441
                    current,
1442
16
                    symfpu::lessThan<traits>(
1443
16
                        fpt(childType), (*arg1).second, (*arg2).second));
1444
4
                break;
1445
1446
              default:
1447
                Unreachable() << "Unknown binary floating-point relation";
1448
                break;
1449
48
            }
1450
          }
1451
48
          break;
1452
1453
118
          case kind::FLOATINGPOINT_ISN:
1454
          case kind::FLOATINGPOINT_ISSN:
1455
          case kind::FLOATINGPOINT_ISZ:
1456
          case kind::FLOATINGPOINT_ISINF:
1457
          case kind::FLOATINGPOINT_ISNAN:
1458
          case kind::FLOATINGPOINT_ISNEG:
1459
          case kind::FLOATINGPOINT_ISPOS:
1460
          {
1461
236
            TypeNode childType(current[0].getType());
1462
118
            fpMap::const_iterator arg1(d_fpMap.find(current[0]));
1463
1464
118
            if (arg1 == d_fpMap.end())
1465
            {
1466
              workStack.push_back(current);
1467
              workStack.push_back(current[0]);
1468
              continue;  // i.e. recurse!
1469
            }
1470
1471
118
            switch (current.getKind())
1472
            {
1473
              case kind::FLOATINGPOINT_ISN:
1474
                d_boolMap.insert(
1475
                    current,
1476
                    symfpu::isNormal<traits>(fpt(childType), (*arg1).second));
1477
                break;
1478
1479
3
              case kind::FLOATINGPOINT_ISSN:
1480
6
                d_boolMap.insert(current,
1481
6
                                 symfpu::isSubnormal<traits>(fpt(childType),
1482
3
                                                             (*arg1).second));
1483
3
                break;
1484
1485
7
              case kind::FLOATINGPOINT_ISZ:
1486
14
                d_boolMap.insert(
1487
                    current,
1488
14
                    symfpu::isZero<traits>(fpt(childType), (*arg1).second));
1489
7
                break;
1490
1491
46
              case kind::FLOATINGPOINT_ISINF:
1492
92
                d_boolMap.insert(
1493
                    current,
1494
92
                    symfpu::isInfinite<traits>(fpt(childType), (*arg1).second));
1495
46
                break;
1496
1497
22
              case kind::FLOATINGPOINT_ISNAN:
1498
44
                d_boolMap.insert(
1499
                    current,
1500
44
                    symfpu::isNaN<traits>(fpt(childType), (*arg1).second));
1501
22
                break;
1502
1503
6
              case kind::FLOATINGPOINT_ISPOS:
1504
12
                d_boolMap.insert(
1505
                    current,
1506
12
                    symfpu::isPositive<traits>(fpt(childType), (*arg1).second));
1507
6
                break;
1508
1509
34
              case kind::FLOATINGPOINT_ISNEG:
1510
68
                d_boolMap.insert(
1511
                    current,
1512
68
                    symfpu::isNegative<traits>(fpt(childType), (*arg1).second));
1513
34
                break;
1514
1515
              default:
1516
                Unreachable() << "Unknown unary floating-point relation";
1517
                break;
1518
118
            }
1519
          }
1520
118
          break;
1521
1522
          case kind::FLOATINGPOINT_EQ:
1523
          case kind::FLOATINGPOINT_GEQ:
1524
          case kind::FLOATINGPOINT_GT:
1525
            Unreachable() << "Kind should have been removed by rewriter.";
1526
            break;
1527
1528
          // Components will be registered as they are owned by
1529
          // the floating-point theory.  No action is required.
1530
          case kind::FLOATINGPOINT_COMPONENT_NAN:
1531
          case kind::FLOATINGPOINT_COMPONENT_INF:
1532
          case kind::FLOATINGPOINT_COMPONENT_ZERO:
1533
          case kind::FLOATINGPOINT_COMPONENT_SIGN:
1534
          /* Fall through... */
1535
1536
          default:
1537
            CVC4_FPCONV_PASSTHROUGH;
1538
            return result;
1539
            break;
1540
        }
1541
1542
549
        i = d_boolMap.find(current);
1543
      }
1544
1545
549
      result = (*i).second;
1546
    }
1547
843
    else if (t.isBitVector())
1548
    {
1549
843
      switch (current.getKind())
1550
      {
1551
        /******** Conversions ********/
1552
        case kind::FLOATINGPOINT_TO_UBV_TOTAL:
1553
        {
1554
          TypeNode childType(current[1].getType());
1555
          ubvMap::const_iterator i(d_ubvMap.find(current));
1556
1557
          if (i == d_ubvMap.end())
1558
          {
1559
            rmMap::const_iterator mode(d_rmMap.find(current[0]));
1560
            fpMap::const_iterator arg1(d_fpMap.find(current[1]));
1561
            bool recurseNeeded =
1562
                (mode == d_rmMap.end()) || (arg1 == d_fpMap.end());
1563
1564
            if (recurseNeeded)
1565
            {
1566
              workStack.push_back(current);
1567
              if (mode == d_rmMap.end())
1568
              {
1569
                workStack.push_back(current[0]);
1570
              }
1571
              if (arg1 == d_fpMap.end())
1572
              {
1573
                workStack.push_back(current[1]);
1574
              }
1575
              continue;  // i.e. recurse!
1576
            }
1577
1578
            FloatingPointToUBVTotal info =
1579
                current.getOperator().getConst<FloatingPointToUBVTotal>();
1580
1581
            d_ubvMap.insert(current,
1582
                            symfpu::convertFloatToUBV<traits>(fpt(childType),
1583
                                                              (*mode).second,
1584
                                                              (*arg1).second,
1585
                                                              info.d_bv_size,
1586
                                                              ubv(current[2])));
1587
            i = d_ubvMap.find(current);
1588
          }
1589
1590
          result = (*i).second;
1591
        }
1592
        break;
1593
1594
        case kind::FLOATINGPOINT_TO_SBV_TOTAL:
1595
        {
1596
          TypeNode childType(current[1].getType());
1597
          sbvMap::const_iterator i(d_sbvMap.find(current));
1598
1599
          if (i == d_sbvMap.end())
1600
          {
1601
            rmMap::const_iterator mode(d_rmMap.find(current[0]));
1602
            fpMap::const_iterator arg1(d_fpMap.find(current[1]));
1603
            bool recurseNeeded =
1604
                (mode == d_rmMap.end()) || (arg1 == d_fpMap.end());
1605
1606
            if (recurseNeeded)
1607
            {
1608
              workStack.push_back(current);
1609
              if (mode == d_rmMap.end())
1610
              {
1611
                workStack.push_back(current[0]);
1612
              }
1613
              if (arg1 == d_fpMap.end())
1614
              {
1615
                workStack.push_back(current[1]);
1616
              }
1617
              continue;  // i.e. recurse!
1618
            }
1619
1620
            FloatingPointToSBVTotal info =
1621
                current.getOperator().getConst<FloatingPointToSBVTotal>();
1622
1623
            d_sbvMap.insert(current,
1624
                            symfpu::convertFloatToSBV<traits>(fpt(childType),
1625
                                                              (*mode).second,
1626
                                                              (*arg1).second,
1627
                                                              info.d_bv_size,
1628
                                                              sbv(current[2])));
1629
1630
            i = d_sbvMap.find(current);
1631
          }
1632
1633
          result = (*i).second;
1634
        }
1635
        break;
1636
1637
        case kind::FLOATINGPOINT_TO_UBV:
1638
          Unreachable()
1639
              << "Partially defined fp.to_ubv should have been removed by "
1640
                 "expandDefinition";
1641
          break;
1642
1643
        case kind::FLOATINGPOINT_TO_SBV:
1644
          Unreachable()
1645
              << "Partially defined fp.to_sbv should have been removed by "
1646
                 "expandDefinition";
1647
          break;
1648
1649
        // Again, no action is needed
1650
843
        case kind::FLOATINGPOINT_COMPONENT_EXPONENT:
1651
        case kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND:
1652
        case kind::ROUNDINGMODE_BITBLAST:
1653
        /* Fall through ... */
1654
1655
843
        default: CVC4_FPCONV_PASSTHROUGH; break;
1656
      }
1657
    }
1658
    else if (t.isReal())
1659
    {
1660
      switch (current.getKind())
1661
      {
1662
        /******** Conversions ********/
1663
        case kind::FLOATINGPOINT_TO_REAL_TOTAL:
1664
        {
1665
          // We need to recurse so that any variables that are only
1666
          // used under this will have components created
1667
          // (via auxiliary constraints)
1668
1669
          TypeNode childType(current[0].getType());
1670
          fpMap::const_iterator arg1(d_fpMap.find(current[0]));
1671
1672
          if (arg1 == d_fpMap.end())
1673
          {
1674
            workStack.push_back(current);
1675
            workStack.push_back(current[0]);
1676
            continue;  // i.e. recurse!
1677
          }
1678
1679
          // However we don't need to do anything explicitly with
1680
          // this as it will be treated as an uninterpreted function
1681
          // by the real theory and we don't need to bit-blast the
1682
          // float expression unless we need to say something about
1683
          // its value.
1684
        }
1685
1686
        break;
1687
1688
        case kind::FLOATINGPOINT_TO_REAL:
1689
          Unreachable()
1690
              << "Partially defined fp.to_real should have been removed by "
1691
                 "expandDefinition";
1692
          break;
1693
1694
        default: CVC4_FPCONV_PASSTHROUGH; break;
1695
      }
1696
    }
1697
    else
1698
    {
1699
      CVC4_FPCONV_PASSTHROUGH;
1700
    }
1701
  }
1702
1703
1916
  return result;
1704
#else
1705
  Unimplemented() << "Conversion is dependent on SymFPU";
1706
#endif
1707
}
1708
1709
#undef CVC4_FPCONV_PASSTHROUGH
1710
1711
3457
Node FpConverter::getValue(Valuation &val, TNode var)
1712
{
1713
3457
  Assert(Theory::isLeafOf(var, THEORY_FP));
1714
1715
#ifdef CVC4_USE_SYMFPU
1716
6914
  TypeNode t(var.getType());
1717
1718
3457
  Assert(t.isRoundingMode() || t.isFloatingPoint())
1719
      << "Asking for the value of a type that is not managed by the "
1720
         "floating-point theory";
1721
1722
3457
  if (t.isRoundingMode())
1723
  {
1724
151
    rmMap::const_iterator i(d_rmMap.find(var));
1725
1726
151
    Assert(i != d_rmMap.end())
1727
        << "Asking for the value of an unregistered expression";
1728
151
    return rmToNode((*i).second);
1729
  }
1730
3306
  fpMap::const_iterator i(d_fpMap.find(var));
1731
1732
3306
  Assert(i != d_fpMap.end())
1733
      << "Asking for the value of an unregistered expression";
1734
3306
  return ufToNode(fpt(t), (*i).second);
1735
#else
1736
  Unimplemented() << "Conversion is dependent on SymFPU";
1737
#endif
1738
}
1739
1740
}  // namespace fp
1741
}  // namespace theory
1742
26676
}  // namespace CVC4