GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/fp/theory_fp.cpp Lines: 373 589 63.3 %
Date: 2021-03-23 Branches: 840 3198 26.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_fp.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Martin Brain, Andrew Reynolds, Andres Noetzli
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 [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
18
#include "theory/fp/theory_fp.h"
19
20
#include <set>
21
#include <stack>
22
#include <unordered_set>
23
#include <vector>
24
25
#include "base/configuration.h"
26
#include "options/fp_options.h"
27
#include "smt/logic_exception.h"
28
#include "theory/fp/fp_converter.h"
29
#include "theory/fp/theory_fp_rewriter.h"
30
#include "theory/output_channel.h"
31
#include "theory/rewriter.h"
32
#include "theory/theory_model.h"
33
34
using namespace std;
35
36
namespace CVC4 {
37
namespace theory {
38
namespace fp {
39
40
namespace removeToFPGeneric {
41
42
40
Node removeToFPGeneric(TNode node) {
43
40
  Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_GENERIC);
44
45
  FloatingPointToFPGeneric info =
46
40
      node.getOperator().getConst<FloatingPointToFPGeneric>();
47
48
40
  size_t children = node.getNumChildren();
49
50
80
  Node op;
51
40
  NodeManager *nm = NodeManager::currentNM();
52
53
40
  if (children == 1) {
54
18
    op = nm->mkConst(FloatingPointToFPIEEEBitVector(info));
55
18
    return nm->mkNode(op, node[0]);
56
57
  } else {
58
22
    Assert(children == 2);
59
22
    Assert(node[0].getType().isRoundingMode());
60
61
44
    TypeNode t = node[1].getType();
62
63
22
    if (t.isFloatingPoint()) {
64
6
      op = nm->mkConst(FloatingPointToFPFloatingPoint(info));
65
16
    } else if (t.isReal()) {
66
12
      op = nm->mkConst(FloatingPointToFPReal(info));
67
4
    } else if (t.isBitVector()) {
68
4
      op = nm->mkConst(FloatingPointToFPSignedBitVector(info));
69
    } else {
70
      throw TypeCheckingExceptionPrivate(
71
          node,
72
          "cannot rewrite to_fp generic due to incorrect type of second "
73
          "argument");
74
    }
75
76
22
    return nm->mkNode(op, node[0], node[1]);
77
  }
78
79
  Unreachable() << "to_fp generic not rewritten";
80
}
81
}  // namespace removeToFPGeneric
82
83
namespace helper {
84
Node buildConjunct(const std::vector<TNode> &assumptions) {
85
  if (assumptions.size() == 0) {
86
    return NodeManager::currentNM()->mkConst<bool>(true);
87
88
  } else if (assumptions.size() == 1) {
89
    return assumptions[0];
90
91
  } else {
92
    // \todo see bv::utils::flattenAnd
93
94
    NodeBuilder<> conjunction(kind::AND);
95
    for (std::vector<TNode>::const_iterator it = assumptions.begin();
96
         it != assumptions.end(); ++it) {
97
      conjunction << *it;
98
    }
99
100
    return conjunction;
101
  }
102
}
103
}  // namespace helper
104
105
/** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
106
8997
TheoryFp::TheoryFp(context::Context* c,
107
                   context::UserContext* u,
108
                   OutputChannel& out,
109
                   Valuation valuation,
110
                   const LogicInfo& logicInfo,
111
8997
                   ProofNodeManager* pnm)
112
    : Theory(THEORY_FP, c, u, out, valuation, logicInfo, pnm),
113
      d_notification(*this),
114
      d_registeredTerms(u),
115
8997
      d_conv(new FpConverter(u)),
116
      d_expansionRequested(false),
117
      d_minMap(u),
118
      d_maxMap(u),
119
      d_toUBVMap(u),
120
      d_toSBVMap(u),
121
      d_toRealMap(u),
122
      d_realToFloatMap(u),
123
      d_floatToRealMap(u),
124
      d_abstractionMap(u),
125
      d_state(c, u, valuation),
126
17994
      d_im(*this, d_state, pnm, "theory::fp", false)
127
{
128
  // indicate we are using the default theory state and inference manager
129
8997
  d_theoryState = &d_state;
130
8997
  d_inferManager = &d_im;
131
8997
} /* TheoryFp::TheoryFp() */
132
133
8997
TheoryRewriter* TheoryFp::getTheoryRewriter() { return &d_rewriter; }
134
135
8997
bool TheoryFp::needsEqualityEngine(EeSetupInfo& esi)
136
{
137
8997
  esi.d_notify = &d_notification;
138
8997
  esi.d_name = "theory::fp::ee";
139
8997
  return true;
140
}
141
142
8997
void TheoryFp::finishInit()
143
{
144
8997
  Assert(d_equalityEngine != nullptr);
145
  // Kinds that are to be handled in the congruence closure
146
147
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ABS);
148
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_NEG);
149
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_PLUS);
150
  // d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_SUB); // Removed
151
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_MULT);
152
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_DIV);
153
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_FMA);
154
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_SQRT);
155
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_REM);
156
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_RTI);
157
  // d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_MIN); // Removed
158
  // d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_MAX); // Removed
159
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_MIN_TOTAL);
160
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_MAX_TOTAL);
161
162
  // d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_EQ); // Removed
163
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_LEQ);
164
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_LT);
165
  // d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_GEQ); // Removed
166
  // d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_GT); // Removed
167
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISN);
168
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISSN);
169
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISZ);
170
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISINF);
171
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISNAN);
172
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISNEG);
173
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISPOS);
174
175
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR);
176
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT);
177
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_REAL);
178
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR);
179
8997
  d_equalityEngine->addFunctionKind(
180
      kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR);
181
  // d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_GENERIC); //
182
  // Needed in parsing, should be rewritten away
183
184
  // d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_UBV); // Removed
185
  // d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_SBV); // Removed
186
  // d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_REAL); // Removed
187
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_UBV_TOTAL);
188
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_SBV_TOTAL);
189
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_REAL_TOTAL);
190
191
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_COMPONENT_NAN);
192
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_COMPONENT_INF);
193
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_COMPONENT_ZERO);
194
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_COMPONENT_SIGN);
195
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_COMPONENT_EXPONENT);
196
8997
  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND);
197
8997
  d_equalityEngine->addFunctionKind(kind::ROUNDINGMODE_BITBLAST);
198
8997
}
199
200
Node TheoryFp::minUF(Node node) {
201
  Assert(node.getKind() == kind::FLOATINGPOINT_MIN);
202
  TypeNode t(node.getType());
203
  Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
204
205
  NodeManager *nm = NodeManager::currentNM();
206
  ComparisonUFMap::const_iterator i(d_minMap.find(t));
207
208
  Node fun;
209
  if (i == d_minMap.end()) {
210
    std::vector<TypeNode> args(2);
211
    args[0] = t;
212
    args[1] = t;
213
    fun = nm->mkSkolem("floatingpoint_min_zero_case",
214
                       nm->mkFunctionType(args,
215
#ifdef SYMFPUPROPISBOOL
216
                                          nm->booleanType()
217
#else
218
                                          nm->mkBitVectorType(1U)
219
#endif
220
                                              ),
221
                       "floatingpoint_min_zero_case",
222
                       NodeManager::SKOLEM_EXACT_NAME);
223
    d_minMap.insert(t, fun);
224
  } else {
225
    fun = (*i).second;
226
  }
227
  return nm->mkNode(kind::APPLY_UF, fun, node[1],
228
                    node[0]);  // Application reverses the order or arguments
229
}
230
231
Node TheoryFp::maxUF(Node node) {
232
  Assert(node.getKind() == kind::FLOATINGPOINT_MAX);
233
  TypeNode t(node.getType());
234
  Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
235
236
  NodeManager *nm = NodeManager::currentNM();
237
  ComparisonUFMap::const_iterator i(d_maxMap.find(t));
238
239
  Node fun;
240
  if (i == d_maxMap.end()) {
241
    std::vector<TypeNode> args(2);
242
    args[0] = t;
243
    args[1] = t;
244
    fun = nm->mkSkolem("floatingpoint_max_zero_case",
245
                       nm->mkFunctionType(args,
246
#ifdef SYMFPUPROPISBOOL
247
                                          nm->booleanType()
248
#else
249
                                          nm->mkBitVectorType(1U)
250
#endif
251
                                              ),
252
                       "floatingpoint_max_zero_case",
253
                       NodeManager::SKOLEM_EXACT_NAME);
254
    d_maxMap.insert(t, fun);
255
  } else {
256
    fun = (*i).second;
257
  }
258
  return nm->mkNode(kind::APPLY_UF, fun, node[1], node[0]);
259
}
260
261
Node TheoryFp::toUBVUF(Node node) {
262
  Assert(node.getKind() == kind::FLOATINGPOINT_TO_UBV);
263
264
  TypeNode target(node.getType());
265
  Assert(target.getKind() == kind::BITVECTOR_TYPE);
266
267
  TypeNode source(node[1].getType());
268
  Assert(source.getKind() == kind::FLOATINGPOINT_TYPE);
269
270
  std::pair<TypeNode, TypeNode> p(source, target);
271
  NodeManager *nm = NodeManager::currentNM();
272
  ConversionUFMap::const_iterator i(d_toUBVMap.find(p));
273
274
  Node fun;
275
  if (i == d_toUBVMap.end()) {
276
    std::vector<TypeNode> args(2);
277
    args[0] = nm->roundingModeType();
278
    args[1] = source;
279
    fun = nm->mkSkolem("floatingpoint_to_ubv_out_of_range_case",
280
                       nm->mkFunctionType(args, target),
281
                       "floatingpoint_to_ubv_out_of_range_case",
282
                       NodeManager::SKOLEM_EXACT_NAME);
283
    d_toUBVMap.insert(p, fun);
284
  } else {
285
    fun = (*i).second;
286
  }
287
  return nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]);
288
}
289
290
Node TheoryFp::toSBVUF(Node node) {
291
  Assert(node.getKind() == kind::FLOATINGPOINT_TO_SBV);
292
293
  TypeNode target(node.getType());
294
  Assert(target.getKind() == kind::BITVECTOR_TYPE);
295
296
  TypeNode source(node[1].getType());
297
  Assert(source.getKind() == kind::FLOATINGPOINT_TYPE);
298
299
  std::pair<TypeNode, TypeNode> p(source, target);
300
  NodeManager *nm = NodeManager::currentNM();
301
  ConversionUFMap::const_iterator i(d_toSBVMap.find(p));
302
303
  Node fun;
304
  if (i == d_toSBVMap.end()) {
305
    std::vector<TypeNode> args(2);
306
    args[0] = nm->roundingModeType();
307
    args[1] = source;
308
    fun = nm->mkSkolem("floatingpoint_to_sbv_out_of_range_case",
309
                       nm->mkFunctionType(args, target),
310
                       "floatingpoint_to_sbv_out_of_range_case",
311
                       NodeManager::SKOLEM_EXACT_NAME);
312
    d_toSBVMap.insert(p, fun);
313
  } else {
314
    fun = (*i).second;
315
  }
316
  return nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]);
317
}
318
319
4
Node TheoryFp::toRealUF(Node node) {
320
4
  Assert(node.getKind() == kind::FLOATINGPOINT_TO_REAL);
321
8
  TypeNode t(node[0].getType());
322
4
  Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
323
324
4
  NodeManager *nm = NodeManager::currentNM();
325
4
  ComparisonUFMap::const_iterator i(d_toRealMap.find(t));
326
327
8
  Node fun;
328
4
  if (i == d_toRealMap.end()) {
329
8
    std::vector<TypeNode> args(1);
330
4
    args[0] = t;
331
12
    fun = nm->mkSkolem("floatingpoint_to_real_infinity_and_NaN_case",
332
8
                       nm->mkFunctionType(args, nm->realType()),
333
                       "floatingpoint_to_real_infinity_and_NaN_case",
334
                       NodeManager::SKOLEM_EXACT_NAME);
335
4
    d_toRealMap.insert(t, fun);
336
  } else {
337
    fun = (*i).second;
338
  }
339
8
  return nm->mkNode(kind::APPLY_UF, fun, node[0]);
340
}
341
342
Node TheoryFp::abstractRealToFloat(Node node)
343
{
344
  Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_REAL);
345
  TypeNode t(node.getType());
346
  Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
347
348
  NodeManager *nm = NodeManager::currentNM();
349
  ComparisonUFMap::const_iterator i(d_realToFloatMap.find(t));
350
351
  Node fun;
352
  if (i == d_realToFloatMap.end())
353
  {
354
    std::vector<TypeNode> args(2);
355
    args[0] = node[0].getType();
356
    args[1] = node[1].getType();
357
    fun = nm->mkSkolem("floatingpoint_abstract_real_to_float",
358
                       nm->mkFunctionType(args, node.getType()),
359
                       "floatingpoint_abstract_real_to_float",
360
                       NodeManager::SKOLEM_EXACT_NAME);
361
    d_realToFloatMap.insert(t, fun);
362
  }
363
  else
364
  {
365
    fun = (*i).second;
366
  }
367
  Node uf = nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]);
368
369
  d_abstractionMap.insert(uf, node);
370
371
  return uf;
372
}
373
374
4
Node TheoryFp::abstractFloatToReal(Node node)
375
{
376
4
  Assert(node.getKind() == kind::FLOATINGPOINT_TO_REAL_TOTAL);
377
8
  TypeNode t(node[0].getType());
378
4
  Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
379
380
4
  NodeManager *nm = NodeManager::currentNM();
381
4
  ComparisonUFMap::const_iterator i(d_floatToRealMap.find(t));
382
383
8
  Node fun;
384
4
  if (i == d_floatToRealMap.end())
385
  {
386
8
    std::vector<TypeNode> args(2);
387
4
    args[0] = t;
388
4
    args[1] = nm->realType();
389
12
    fun = nm->mkSkolem("floatingpoint_abstract_float_to_real",
390
8
                       nm->mkFunctionType(args, nm->realType()),
391
                       "floatingpoint_abstract_float_to_real",
392
                       NodeManager::SKOLEM_EXACT_NAME);
393
4
    d_floatToRealMap.insert(t, fun);
394
  }
395
  else
396
  {
397
    fun = (*i).second;
398
  }
399
4
  Node uf = nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]);
400
401
4
  d_abstractionMap.insert(uf, node);
402
403
8
  return uf;
404
}
405
406
2921
TrustNode TheoryFp::expandDefinition(Node node)
407
{
408
5842
  Trace("fp-expandDefinition") << "TheoryFp::expandDefinition(): " << node
409
2921
                               << std::endl;
410
411
5842
  Node res = node;
412
413
2921
  if (node.getKind() == kind::FLOATINGPOINT_TO_FP_GENERIC) {
414
40
    res = removeToFPGeneric::removeToFPGeneric(node);
415
416
2881
  } else if (node.getKind() == kind::FLOATINGPOINT_MIN) {
417
    res = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_MIN_TOTAL,
418
                                           node[0], node[1], minUF(node));
419
420
2881
  } else if (node.getKind() == kind::FLOATINGPOINT_MAX) {
421
    res = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_MAX_TOTAL,
422
                                           node[0], node[1], maxUF(node));
423
424
2881
  } else if (node.getKind() == kind::FLOATINGPOINT_TO_UBV) {
425
    FloatingPointToUBV info = node.getOperator().getConst<FloatingPointToUBV>();
426
    FloatingPointToUBVTotal newInfo(info);
427
428
    res =
429
        NodeManager::currentNM()->mkNode(  // kind::FLOATINGPOINT_TO_UBV_TOTAL,
430
            NodeManager::currentNM()->mkConst(newInfo), node[0], node[1],
431
            toUBVUF(node));
432
433
2881
  } else if (node.getKind() == kind::FLOATINGPOINT_TO_SBV) {
434
    FloatingPointToSBV info = node.getOperator().getConst<FloatingPointToSBV>();
435
    FloatingPointToSBVTotal newInfo(info);
436
437
    res =
438
        NodeManager::currentNM()->mkNode(  // kind::FLOATINGPOINT_TO_SBV_TOTAL,
439
            NodeManager::currentNM()->mkConst(newInfo), node[0], node[1],
440
            toSBVUF(node));
441
442
2881
  } else if (node.getKind() == kind::FLOATINGPOINT_TO_REAL) {
443
8
    res = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_TO_REAL_TOTAL,
444
8
                                           node[0], toRealUF(node));
445
446
  } else {
447
    // Do nothing
448
  }
449
450
2921
  if (res != node) {
451
88
    Trace("fp-expandDefinition") << "TheoryFp::expandDefinition(): " << node
452
44
                                 << " rewritten to " << res << std::endl;
453
44
    return TrustNode::mkTrustRewrite(node, res, nullptr);
454
  }
455
2877
  return TrustNode::null();
456
}
457
458
2915
TrustNode TheoryFp::ppRewrite(TNode node, std::vector<SkolemLemma>& lems)
459
{
460
2915
  Trace("fp-ppRewrite") << "TheoryFp::ppRewrite(): " << node << std::endl;
461
  // first, see if we need to expand definitions
462
5830
  TrustNode texp = expandDefinition(node);
463
2915
  if (!texp.isNull())
464
  {
465
44
    return texp;
466
  }
467
468
5742
  Node res = node;
469
470
  // Abstract conversion functions
471
2871
  if (node.getKind() == kind::FLOATINGPOINT_TO_REAL_TOTAL)
472
  {
473
4
    res = abstractFloatToReal(node);
474
475
    // Generate some lemmas
476
4
    NodeManager *nm = NodeManager::currentNM();
477
478
    Node pd =
479
        nm->mkNode(kind::IMPLIES,
480
16
                   nm->mkNode(kind::OR,
481
8
                              nm->mkNode(kind::FLOATINGPOINT_ISNAN, node[0]),
482
8
                              nm->mkNode(kind::FLOATINGPOINT_ISINF, node[0])),
483
16
                   nm->mkNode(kind::EQUAL, res, node[1]));
484
4
    handleLemma(pd);
485
486
    Node z =
487
        nm->mkNode(kind::IMPLIES,
488
8
                   nm->mkNode(kind::FLOATINGPOINT_ISZ, node[0]),
489
16
                   nm->mkNode(kind::EQUAL, res, nm->mkConst(Rational(0U))));
490
4
    handleLemma(z);
491
492
    // TODO : bounds on the output from largest floats, #1914
493
  }
494
2867
  else if (node.getKind() == kind::FLOATINGPOINT_TO_FP_REAL)
495
  {
496
    res = abstractRealToFloat(node);
497
498
    // Generate some lemmas
499
    NodeManager *nm = NodeManager::currentNM();
500
501
    Node nnan =
502
        nm->mkNode(kind::NOT, nm->mkNode(kind::FLOATINGPOINT_ISNAN, res));
503
    handleLemma(nnan);
504
505
    Node z = nm->mkNode(
506
        kind::IMPLIES,
507
        nm->mkNode(kind::EQUAL, node[1], nm->mkConst(Rational(0U))),
508
        nm->mkNode(kind::EQUAL,
509
                   res,
510
                   nm->mkConst(FloatingPoint::makeZero(
511
                       res.getType().getConst<FloatingPointSize>(), false))));
512
    handleLemma(z);
513
514
    // TODO : rounding-mode specific bounds on floats that don't give infinity
515
    // BEWARE of directed rounding!   #1914
516
  }
517
518
2871
  if (res != node)
519
  {
520
8
    Trace("fp-ppRewrite") << "TheoryFp::ppRewrite(): node " << node
521
4
                          << " rewritten to " << res << std::endl;
522
4
    return TrustNode::mkTrustRewrite(node, res, nullptr);
523
  }
524
525
2867
  return TrustNode::null();
526
}
527
528
8
bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
529
{
530
16
  Trace("fp-refineAbstraction") << "TheoryFp::refineAbstraction(): " << abstract
531
8
                                << " vs. " << concrete << std::endl;
532
8
  Kind k = concrete.getKind();
533
8
  if (k == kind::FLOATINGPOINT_TO_REAL_TOTAL)
534
  {
535
    // Get the values
536
8
    Assert(m->hasTerm(abstract));
537
8
    Assert(m->hasTerm(concrete[0]));
538
8
    Assert(m->hasTerm(concrete[1]));
539
540
16
    Node abstractValue = m->getValue(abstract);
541
16
    Node floatValue = m->getValue(concrete[0]);
542
16
    Node undefValue = m->getValue(concrete[1]);
543
544
8
    Assert(abstractValue.isConst());
545
8
    Assert(floatValue.isConst());
546
8
    Assert(undefValue.isConst());
547
548
    // Work out the actual value for those args
549
8
    NodeManager *nm = NodeManager::currentNM();
550
551
    Node evaluate =
552
16
        nm->mkNode(kind::FLOATINGPOINT_TO_REAL_TOTAL, floatValue, undefValue);
553
16
    Node concreteValue = Rewriter::rewrite(evaluate);
554
8
    Assert(concreteValue.isConst());
555
556
16
    Trace("fp-refineAbstraction")
557
16
        << "TheoryFp::refineAbstraction(): " << concrete[0] << " = "
558
8
        << floatValue << std::endl
559
16
        << "TheoryFp::refineAbstraction(): " << concrete[1] << " = "
560
8
        << undefValue << std::endl
561
8
        << "TheoryFp::refineAbstraction(): " << abstract << " = "
562
8
        << abstractValue << std::endl
563
8
        << "TheoryFp::refineAbstraction(): " << concrete << " = "
564
8
        << concreteValue << std::endl;
565
566
8
    if (abstractValue != concreteValue)
567
    {
568
      // Need refinement lemmas
569
      // only in the normal and subnormal case
570
4
      Assert(floatValue.getConst<FloatingPoint>().isNormal()
571
             || floatValue.getConst<FloatingPoint>().isSubnormal());
572
573
      Node defined = nm->mkNode(
574
          kind::AND,
575
8
          nm->mkNode(kind::NOT,
576
8
                     nm->mkNode(kind::FLOATINGPOINT_ISNAN, concrete[0])),
577
8
          nm->mkNode(kind::NOT,
578
24
                     nm->mkNode(kind::FLOATINGPOINT_ISINF, concrete[0])));
579
      // First the "forward" constraints
580
      Node fg = nm->mkNode(
581
          kind::IMPLIES,
582
          defined,
583
16
          nm->mkNode(
584
              kind::EQUAL,
585
8
              nm->mkNode(kind::FLOATINGPOINT_GEQ, concrete[0], floatValue),
586
16
              nm->mkNode(kind::GEQ, abstract, concreteValue)));
587
4
      handleLemma(fg);
588
589
      Node fl = nm->mkNode(
590
          kind::IMPLIES,
591
          defined,
592
16
          nm->mkNode(
593
              kind::EQUAL,
594
8
              nm->mkNode(kind::FLOATINGPOINT_LEQ, concrete[0], floatValue),
595
16
              nm->mkNode(kind::LEQ, abstract, concreteValue)));
596
4
      handleLemma(fl);
597
598
      // Then the backwards constraints
599
      Node floatAboveAbstract = Rewriter::rewrite(
600
24
          nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL,
601
8
                     nm->mkConst(FloatingPointToFPReal(
602
8
                         concrete[0].getType().getConst<FloatingPointSize>())),
603
8
                     nm->mkConst(ROUND_TOWARD_POSITIVE),
604
8
                     abstractValue));
605
606
      Node bg = nm->mkNode(
607
          kind::IMPLIES,
608
          defined,
609
16
          nm->mkNode(
610
              kind::EQUAL,
611
8
              nm->mkNode(
612
                  kind::FLOATINGPOINT_GEQ, concrete[0], floatAboveAbstract),
613
16
              nm->mkNode(kind::GEQ, abstract, abstractValue)));
614
4
      handleLemma(bg);
615
616
      Node floatBelowAbstract = Rewriter::rewrite(
617
24
          nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL,
618
8
                     nm->mkConst(FloatingPointToFPReal(
619
8
                         concrete[0].getType().getConst<FloatingPointSize>())),
620
8
                     nm->mkConst(ROUND_TOWARD_NEGATIVE),
621
8
                     abstractValue));
622
623
      Node bl = nm->mkNode(
624
          kind::IMPLIES,
625
          defined,
626
16
          nm->mkNode(
627
              kind::EQUAL,
628
8
              nm->mkNode(
629
                  kind::FLOATINGPOINT_LEQ, concrete[0], floatBelowAbstract),
630
16
              nm->mkNode(kind::LEQ, abstract, abstractValue)));
631
4
      handleLemma(bl);
632
      // TODO : see if the overflow conditions could be improved #1914
633
634
4
      return true;
635
    }
636
    else
637
    {
638
      // No refinement needed
639
4
      return false;
640
    }
641
  }
642
  else if (k == kind::FLOATINGPOINT_TO_FP_REAL)
643
  {
644
    // Get the values
645
    Assert(m->hasTerm(abstract));
646
    Assert(m->hasTerm(concrete[0]));
647
    Assert(m->hasTerm(concrete[1]));
648
649
    Node abstractValue = m->getValue(abstract);
650
    Node rmValue = m->getValue(concrete[0]);
651
    Node realValue = m->getValue(concrete[1]);
652
653
    Assert(abstractValue.isConst());
654
    Assert(rmValue.isConst());
655
    Assert(realValue.isConst());
656
657
    // Work out the actual value for those args
658
    NodeManager *nm = NodeManager::currentNM();
659
660
    Node evaluate =
661
        nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL,
662
                   nm->mkConst(FloatingPointToFPReal(
663
                       concrete.getType().getConst<FloatingPointSize>())),
664
                   rmValue,
665
                   realValue);
666
    Node concreteValue = Rewriter::rewrite(evaluate);
667
    Assert(concreteValue.isConst());
668
669
    Trace("fp-refineAbstraction")
670
        << "TheoryFp::refineAbstraction(): " << concrete[0] << " = " << rmValue
671
        << std::endl
672
        << "TheoryFp::refineAbstraction(): " << concrete[1] << " = "
673
        << realValue << std::endl
674
        << "TheoryFp::refineAbstraction(): " << abstract << " = "
675
        << abstractValue << std::endl
676
        << "TheoryFp::refineAbstraction(): " << concrete << " = "
677
        << concreteValue << std::endl;
678
679
    if (abstractValue != concreteValue)
680
    {
681
      Assert(!abstractValue.getConst<FloatingPoint>().isNaN());
682
      Assert(!concreteValue.getConst<FloatingPoint>().isNaN());
683
684
      Node correctRoundingMode = nm->mkNode(kind::EQUAL, concrete[0], rmValue);
685
      // TODO : Generalise to all rounding modes  #1914
686
687
      // First the "forward" constraints
688
      Node fg = nm->mkNode(
689
          kind::IMPLIES,
690
          correctRoundingMode,
691
          nm->mkNode(
692
              kind::EQUAL,
693
              nm->mkNode(kind::GEQ, concrete[1], realValue),
694
              nm->mkNode(kind::FLOATINGPOINT_GEQ, abstract, concreteValue)));
695
      handleLemma(fg);
696
697
      Node fl = nm->mkNode(
698
          kind::IMPLIES,
699
          correctRoundingMode,
700
          nm->mkNode(
701
              kind::EQUAL,
702
              nm->mkNode(kind::LEQ, concrete[1], realValue),
703
              nm->mkNode(kind::FLOATINGPOINT_LEQ, abstract, concreteValue)));
704
      handleLemma(fl);
705
706
      // Then the backwards constraints
707
      if (!abstractValue.getConst<FloatingPoint>().isInfinite())
708
      {
709
        Node realValueOfAbstract =
710
            Rewriter::rewrite(nm->mkNode(kind::FLOATINGPOINT_TO_REAL_TOTAL,
711
                                         abstractValue,
712
                                         nm->mkConst(Rational(0U))));
713
714
        Node bg = nm->mkNode(
715
            kind::IMPLIES,
716
            correctRoundingMode,
717
            nm->mkNode(
718
                kind::EQUAL,
719
                nm->mkNode(kind::GEQ, concrete[1], realValueOfAbstract),
720
                nm->mkNode(kind::FLOATINGPOINT_GEQ, abstract, abstractValue)));
721
        handleLemma(bg);
722
723
        Node bl = nm->mkNode(
724
            kind::IMPLIES,
725
            correctRoundingMode,
726
            nm->mkNode(
727
                kind::EQUAL,
728
                nm->mkNode(kind::LEQ, concrete[1], realValueOfAbstract),
729
                nm->mkNode(kind::FLOATINGPOINT_LEQ, abstract, abstractValue)));
730
        handleLemma(bl);
731
      }
732
733
      return true;
734
    }
735
    else
736
    {
737
      // No refinement needed
738
      return false;
739
    }
740
  }
741
  else
742
  {
743
    Unreachable() << "Unknown abstraction";
744
  }
745
746
  return false;
747
}
748
749
2176
void TheoryFp::convertAndEquateTerm(TNode node) {
750
2176
  Trace("fp-convertTerm") << "TheoryFp::convertTerm(): " << node << std::endl;
751
2176
  size_t oldAdditionalAssertions = d_conv->d_additionalAssertions.size();
752
753
4352
  Node converted(d_conv->convert(node));
754
755
2176
  if (converted != node) {
756
1098
    Debug("fp-convertTerm")
757
549
        << "TheoryFp::convertTerm(): before " << node << std::endl;
758
1098
    Debug("fp-convertTerm")
759
549
        << "TheoryFp::convertTerm(): after  " << converted << std::endl;
760
  }
761
762
2176
  size_t newAdditionalAssertions = d_conv->d_additionalAssertions.size();
763
2176
  Assert(oldAdditionalAssertions <= newAdditionalAssertions);
764
765
2476
  while (oldAdditionalAssertions < newAdditionalAssertions) {
766
300
    Node addA = d_conv->d_additionalAssertions[oldAdditionalAssertions];
767
768
300
    Debug("fp-convertTerm") << "TheoryFp::convertTerm(): additional assertion  "
769
150
                            << addA << std::endl;
770
771
#ifdef SYMFPUPROPISBOOL
772
    handleLemma(addA, false, true);
773
#else
774
150
    NodeManager *nm = NodeManager::currentNM();
775
776
150
    handleLemma(
777
300
        nm->mkNode(kind::EQUAL, addA, nm->mkConst(::CVC4::BitVector(1U, 1U))));
778
#endif
779
780
150
    ++oldAdditionalAssertions;
781
  }
782
783
  // Equate the floating-point atom and the converted one.
784
  // Also adds the bit-vectors to the bit-vector solver.
785
2176
  if (node.getType().isBoolean()) {
786
809
    if (converted != node) {
787
549
      Assert(converted.getType().isBitVector());
788
789
549
      NodeManager *nm = NodeManager::currentNM();
790
791
#ifdef SYMFPUPROPISBOOL
792
      handleLemma(nm->mkNode(kind::EQUAL, node, converted));
793
#else
794
549
      handleLemma(
795
1098
          nm->mkNode(kind::EQUAL, node,
796
1098
                     nm->mkNode(kind::EQUAL, converted,
797
1098
                                nm->mkConst(::CVC4::BitVector(1U, 1U)))));
798
#endif
799
800
    } else {
801
260
      Assert((node.getKind() == kind::EQUAL));
802
    }
803
804
1367
  } else if (node.getType().isBitVector()) {
805
843
    if (converted != node) {
806
      Assert(converted.getType().isBitVector());
807
808
      handleLemma(
809
          NodeManager::currentNM()->mkNode(kind::EQUAL, node, converted));
810
    }
811
  }
812
813
4352
  return;
814
}
815
816
3919
void TheoryFp::registerTerm(TNode node) {
817
3919
  Trace("fp-registerTerm") << "TheoryFp::registerTerm(): " << node << std::endl;
818
819
3919
  if (!isRegistered(node)) {
820
2176
    Kind k = node.getKind();
821
2176
    Assert(k != kind::FLOATINGPOINT_TO_FP_GENERIC
822
           && k != kind::FLOATINGPOINT_SUB && k != kind::FLOATINGPOINT_EQ
823
           && k != kind::FLOATINGPOINT_GEQ && k != kind::FLOATINGPOINT_GT);
824
825
2176
    bool success = d_registeredTerms.insert(node);
826
    (void)success;  // Only used for assertion
827
2176
    Assert(success);
828
829
    // Add to the equality engine
830
2176
    if (k == kind::EQUAL)
831
    {
832
643
      d_equalityEngine->addTriggerPredicate(node);
833
    }
834
    else
835
    {
836
1533
      d_equalityEngine->addTerm(node);
837
    }
838
839
    // Give the expansion of classifications in terms of equalities
840
    // This should make equality reasoning slightly more powerful.
841
2176
    if ((k == kind::FLOATINGPOINT_ISNAN) || (k == kind::FLOATINGPOINT_ISZ)
842
2147
        || (k == kind::FLOATINGPOINT_ISINF))
843
    {
844
75
      NodeManager *nm = NodeManager::currentNM();
845
75
      FloatingPointSize s = node[0].getType().getConst<FloatingPointSize>();
846
150
      Node equalityAlias = Node::null();
847
848
75
      if (k == kind::FLOATINGPOINT_ISNAN)
849
      {
850
22
        equalityAlias = nm->mkNode(
851
44
            kind::EQUAL, node[0], nm->mkConst(FloatingPoint::makeNaN(s)));
852
      }
853
53
      else if (k == kind::FLOATINGPOINT_ISZ)
854
      {
855
21
        equalityAlias = nm->mkNode(
856
            kind::OR,
857
14
            nm->mkNode(kind::EQUAL,
858
                       node[0],
859
14
                       nm->mkConst(FloatingPoint::makeZero(s, true))),
860
14
            nm->mkNode(kind::EQUAL,
861
                       node[0],
862
14
                       nm->mkConst(FloatingPoint::makeZero(s, false))));
863
      }
864
46
      else if (k == kind::FLOATINGPOINT_ISINF)
865
      {
866
138
        equalityAlias = nm->mkNode(
867
            kind::OR,
868
92
            nm->mkNode(kind::EQUAL,
869
                       node[0],
870
92
                       nm->mkConst(FloatingPoint::makeInf(s, true))),
871
92
            nm->mkNode(kind::EQUAL,
872
                       node[0],
873
92
                       nm->mkConst(FloatingPoint::makeInf(s, false))));
874
      }
875
      else
876
      {
877
        Unreachable() << "Only isNaN, isInf and isZero have aliases";
878
      }
879
880
75
      handleLemma(nm->mkNode(kind::EQUAL, node, equalityAlias));
881
    }
882
883
    // Use symfpu to produce an equivalent bit-vector statement
884
2176
    convertAndEquateTerm(node);
885
  }
886
3919
  return;
887
}
888
889
5897
bool TheoryFp::isRegistered(TNode node) {
890
5897
  return !(d_registeredTerms.find(node) == d_registeredTerms.end());
891
}
892
893
2636
void TheoryFp::preRegisterTerm(TNode node)
894
{
895
5312
  if (Configuration::isBuiltWithSymFPU() && !options::fpExp())
896
  {
897
974
    TypeNode tn = node.getType();
898
487
    if (tn.isFloatingPoint())
899
    {
900
131
      unsigned exp_sz = tn.getFloatingPointExponentSize();
901
131
      unsigned sig_sz = tn.getFloatingPointSignificandSize();
902
131
      if (!((exp_sz == 8 && sig_sz == 24) || (exp_sz == 11 && sig_sz == 53)))
903
      {
904
        std::stringstream ss;
905
        ss << "FP term " << node << " with type whose size is " << exp_sz << "/"
906
           << sig_sz
907
           << " is not supported, only Float32 (8/24) or Float64 (11/53) types "
908
              "are supported in default mode. Try the experimental solver via "
909
              "--fp-exp. Note: There are known issues with the experimental "
910
              "solver, use at your own risk.";
911
        throw LogicException(ss.str());
912
      }
913
    }
914
  }
915
5272
  Trace("fp-preRegisterTerm")
916
2636
      << "TheoryFp::preRegisterTerm(): " << node << std::endl;
917
2636
  registerTerm(node);
918
2636
  return;
919
}
920
921
798
void TheoryFp::handleLemma(Node node, InferenceId id)
922
{
923
798
  Trace("fp") << "TheoryFp::handleLemma(): asserting " << node << std::endl;
924
  // will be preprocessed when sent, which is important because it contains
925
  // embedded ITEs
926
798
  d_im.lemma(node, id);
927
798
}
928
929
1299
bool TheoryFp::propagateLit(TNode node)
930
{
931
1299
  Trace("fp") << "TheoryFp::propagateLit(): propagate " << node << std::endl;
932
1299
  return d_im.propagateLit(node);
933
}
934
935
void TheoryFp::conflictEqConstantMerge(TNode t1, TNode t2)
936
{
937
  Trace("fp") << "TheoryFp::conflictEqConstantMerge(): conflict detected"
938
              << std::endl;
939
  d_im.conflictEqConstantMerge(t1, t2);
940
}
941
942
943
5568
bool TheoryFp::needsCheckLastEffort()
944
{
945
  // only need to check if we have added to the abstraction map, otherwise
946
  // postCheck below is a no-op.
947
5568
  return !d_abstractionMap.empty();
948
}
949
950
20297
void TheoryFp::postCheck(Effort level)
951
{
952
  // Resolve the abstractions for the conversion lemmas
953
20297
  if (level == EFFORT_LAST_CALL)
954
  {
955
8
    Trace("fp") << "TheoryFp::check(): checking abstractions" << std::endl;
956
8
    TheoryModel* m = getValuation().getModel();
957
8
    bool lemmaAdded = false;
958
959
16
    for (AbstractionMap::const_iterator i = d_abstractionMap.begin();
960
16
         i != d_abstractionMap.end();
961
         ++i)
962
    {
963
8
      if (m->hasTerm((*i).first))
964
      {  // Is actually used in the model
965
8
        lemmaAdded |= refineAbstraction(m, (*i).first, (*i).second);
966
      }
967
    }
968
  }
969
970
20297
  Trace("fp") << "TheoryFp::check(): completed" << std::endl;
971
  /* Checking should be handled by the bit-vector engine */
972
20297
}
973
974
1567
bool TheoryFp::preNotifyFact(
975
    TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
976
{
977
1567
  if (atom.getKind() == kind::EQUAL)
978
  {
979
1283
    Assert(!(atom[0].getType().isFloatingPoint()
980
             || atom[0].getType().isRoundingMode())
981
           || isRegistered(atom[0]));
982
1283
    Assert(!(atom[1].getType().isFloatingPoint()
983
             || atom[1].getType().isRoundingMode())
984
           || isRegistered(atom[1]));
985
1283
    registerTerm(atom);  // Needed for float equalities
986
  }
987
  else
988
  {
989
    // A system-wide invariant; predicates are registered before they are
990
    // asserted
991
284
    Assert(isRegistered(atom));
992
993
284
    if (!d_equalityEngine->isFunctionKind(atom.getKind()))
994
    {
995
      return true;
996
    }
997
  }
998
1567
  return false;
999
}
1000
1001
TrustNode TheoryFp::explain(TNode n)
1002
{
1003
  Trace("fp") << "TheoryFp::explain(): explain " << n << std::endl;
1004
1005
  // All things we assert directly (and not via bit-vector) should
1006
  // come from the equality engine so this should be sufficient...
1007
  std::vector<TNode> assumptions;
1008
1009
  bool polarity = n.getKind() != kind::NOT;
1010
  TNode atom = polarity ? n : n[0];
1011
  if (atom.getKind() == kind::EQUAL) {
1012
    d_equalityEngine->explainEquality(atom[0], atom[1], polarity, assumptions);
1013
  } else {
1014
    d_equalityEngine->explainPredicate(atom, polarity, assumptions);
1015
  }
1016
1017
  Node exp = helper::buildConjunct(assumptions);
1018
  return TrustNode::mkTrustPropExp(n, exp, nullptr);
1019
}
1020
1021
Node TheoryFp::getModelValue(TNode var) {
1022
  return d_conv->getValue(d_valuation, var);
1023
}
1024
1025
4724
bool TheoryFp::collectModelInfo(TheoryModel* m,
1026
                                const std::set<Node>& relevantTerms)
1027
{
1028
  // this override behavior to not assert equality engine
1029
4724
  return collectModelValues(m, relevantTerms);
1030
}
1031
1032
4724
bool TheoryFp::collectModelValues(TheoryModel* m,
1033
                                  const std::set<Node>& relevantTerms)
1034
{
1035
9448
  Trace("fp-collectModelInfo")
1036
4724
      << "TheoryFp::collectModelInfo(): begin" << std::endl;
1037
4724
  if (Trace.isOn("fp-collectModelInfo")) {
1038
    for (std::set<Node>::const_iterator i(relevantTerms.begin());
1039
         i != relevantTerms.end(); ++i) {
1040
      Trace("fp-collectModelInfo")
1041
          << "TheoryFp::collectModelInfo(): relevantTerms " << *i << std::endl;
1042
    }
1043
  }
1044
1045
9448
  std::unordered_set<TNode, TNodeHashFunction> visited;
1046
9448
  std::stack<TNode> working;
1047
9448
  std::set<TNode> relevantVariables;
1048
13394
  for (std::set<Node>::const_iterator i(relevantTerms.begin());
1049
13394
       i != relevantTerms.end(); ++i) {
1050
8670
    working.push(*i);
1051
  }
1052
1053
34694
  while (!working.empty()) {
1054
29970
    TNode current = working.top();
1055
14985
    working.pop();
1056
1057
    // Ignore things that have already been explored
1058
14985
    if (visited.find(current) == visited.end()) {
1059
8906
      visited.insert(current);
1060
1061
17812
      TypeNode t(current.getType());
1062
1063
25638
      if ((t.isRoundingMode() || t.isFloatingPoint()) &&
1064
16732
          this->isLeaf(current)) {
1065
3457
        relevantVariables.insert(current);
1066
      }
1067
1068
15221
      for (size_t i = 0; i < current.getNumChildren(); ++i) {
1069
6315
        working.push(current[i]);
1070
      }
1071
    }
1072
  }
1073
1074
8181
  for (std::set<TNode>::const_iterator i(relevantVariables.begin());
1075
8181
       i != relevantVariables.end();
1076
       ++i)
1077
  {
1078
6914
    TNode node = *i;
1079
1080
6914
    Trace("fp-collectModelInfo")
1081
3457
        << "TheoryFp::collectModelInfo(): relevantVariable " << node
1082
3457
        << std::endl;
1083
1084
3457
    if (!m->assertEquality(node, d_conv->getValue(d_valuation, node), true))
1085
    {
1086
      return false;
1087
    }
1088
1089
10371
    if (Configuration::isAssertionBuild() && isLeaf(node) && !node.isConst()
1090
7625
        && node.getType().isFloatingPoint())
1091
    {
1092
      // Check that the equality engine has asssigned values to all the
1093
      // components of `node` except `(sign node)` (the sign component is
1094
      // assignable, meaning that the model builder can pick an arbitrary value
1095
      // for it if it hasn't been assigned in the equality engine).
1096
705
      NodeManager* nm = NodeManager::currentNM();
1097
1410
      Node compNaN = nm->mkNode(kind::FLOATINGPOINT_COMPONENT_NAN, node);
1098
1410
      Node compInf = nm->mkNode(kind::FLOATINGPOINT_COMPONENT_INF, node);
1099
1410
      Node compZero = nm->mkNode(kind::FLOATINGPOINT_COMPONENT_ZERO, node);
1100
      Node compExponent =
1101
1410
          nm->mkNode(kind::FLOATINGPOINT_COMPONENT_EXPONENT, node);
1102
      Node compSignificand =
1103
1410
          nm->mkNode(kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND, node);
1104
1105
705
      eq::EqualityEngine* ee = m->getEqualityEngine();
1106
705
      Assert(ee->hasTerm(compNaN) && ee->getRepresentative(compNaN).isConst());
1107
705
      Assert(ee->hasTerm(compInf) && ee->getRepresentative(compInf).isConst());
1108
705
      Assert(ee->hasTerm(compZero)
1109
             && ee->getRepresentative(compZero).isConst());
1110
705
      Assert(ee->hasTerm(compExponent)
1111
             && ee->getRepresentative(compExponent).isConst());
1112
705
      Assert(ee->hasTerm(compSignificand));
1113
705
      Assert(ee->getRepresentative(compSignificand).isConst());
1114
1115
      // At most one of the flags (NaN, inf, zero) can be set
1116
1410
      Node one = nm->mkConst(BitVector(1U, 1U));
1117
705
      size_t numFlags = 0;
1118
705
      numFlags += ee->getRepresentative(compNaN) == one ? 1 : 0;
1119
705
      numFlags += ee->getRepresentative(compInf) == one ? 1 : 0;
1120
705
      numFlags += ee->getRepresentative(compZero) == one ? 1 : 0;
1121
705
      Assert(numFlags <= 1);
1122
    }
1123
  }
1124
1125
4724
  return true;
1126
}
1127
1128
641
bool TheoryFp::NotifyClass::eqNotifyTriggerPredicate(TNode predicate,
1129
                                                     bool value) {
1130
1282
  Debug("fp-eq")
1131
641
      << "TheoryFp::eqNotifyTriggerPredicate(): call back as predicate "
1132
641
      << predicate << " is " << value << std::endl;
1133
1134
641
  if (value) {
1135
464
    return d_theorySolver.propagateLit(predicate);
1136
  }
1137
177
  return d_theorySolver.propagateLit(predicate.notNode());
1138
}
1139
1140
658
bool TheoryFp::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1,
1141
                                                        TNode t2, bool value) {
1142
1316
  Debug("fp-eq") << "TheoryFp::eqNotifyTriggerTermEquality(): call back as "
1143
658
                 << t1 << (value ? " = " : " != ") << t2 << std::endl;
1144
1145
658
  if (value) {
1146
443
    return d_theorySolver.propagateLit(t1.eqNode(t2));
1147
  }
1148
215
  return d_theorySolver.propagateLit(t1.eqNode(t2).notNode());
1149
}
1150
1151
void TheoryFp::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
1152
  Debug("fp-eq") << "TheoryFp::eqNotifyConstantTermMerge(): call back as " << t1
1153
                 << " = " << t2 << std::endl;
1154
  d_theorySolver.conflictEqConstantMerge(t1, t2);
1155
}
1156
1157
}  // namespace fp
1158
}  // namespace theory
1159
26685
}  // namespace CVC4