src/theory/fp/theory_fp.cpp

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