src/theory/fp/theory_fp_rewriter.cpp

   1 /*********************                                                        */
   2 /*! \file theory_fp_rewriter.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Martin Brain, Paul Meng, Tim King
   6  ** Copyright (c) 2013  University of Oxford
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
   9  ** in the top-level source directory) and their institutional affiliations.
  10  ** All rights reserved.  See the file COPYING in the top-level source
  11  ** directory for licensing information.\endverbatim
  12  **
  13  ** \brief [[ Rewrite rules for floating point theories. ]]
  14  **
  15  ** \todo [[ Constant folding
  16  **          Push negations up through arithmetic operators (include max and min? maybe not due to +0/-0)
  17  **          classifications to normal tests (maybe)
  18  **          (= x (fp.neg x)) --> (isNaN x)
  19  **          (fp.eq x (fp.neg x)) --> (isZero x)   (previous and reorganise should be sufficient)
  20  **          (fp.eq x const) --> various = depending on const
  21  **          (fp.abs (fp.neg x)) --> (fp.abs x)
  22  **          (fp.isPositive (fp.neg x)) --> (fp.isNegative x)
  23  **          (fp.isNegative (fp.neg x)) --> (fp.isPositive x)
  24  **          (fp.isPositive (fp.abs x)) --> (not (isNaN x))
  25  **          (fp.isNegative (fp.abs x)) --> false
  26  **       ]]
  27  **/
  28
  29 #include <algorithm>
  30
  31 #include "base/cvc4_assert.h"
  32 #include "theory/fp/theory_fp_rewriter.h"
  33
  34 namespace CVC4 {
  35 namespace theory {
  36 namespace fp {
  37
  38 namespace rewrite {
  39   /** Rewrite rules **/
  40   template <RewriteFunction first, RewriteFunction second>
  41   RewriteResponse then (TNode node, bool isPreRewrite) {
  42     RewriteResponse result(first(node, isPreRewrite));
  43
  44     if (result.status == REWRITE_DONE) {
  45       return second(result.node, isPreRewrite);
  46     } else {
  47       return result;
  48     }
  49   }
  50
  51   RewriteResponse notFP (TNode node, bool) {
  52     Unreachable("non floating-point kind (%d) in floating point rewrite?",node.getKind());
  53   }
  54
  55   RewriteResponse identity (TNode node, bool) {
  56     return RewriteResponse(REWRITE_DONE, node);
  57   }
  58
  59   RewriteResponse type (TNode node, bool) {
  60     Unreachable("sort kind (%d) found in expression?",node.getKind());
  61     return RewriteResponse(REWRITE_DONE, node);
  62   }
  63
  64   RewriteResponse removeDoubleNegation (TNode node, bool) {
  65     Assert(node.getKind() == kind::FLOATINGPOINT_NEG);
  66     if (node[0].getKind() == kind::FLOATINGPOINT_NEG) {
  67       RewriteResponse(REWRITE_AGAIN, node[0][0]);
  68     }
  69
  70     return RewriteResponse(REWRITE_DONE, node);
  71   }
  72
  73   RewriteResponse convertSubtractionToAddition (TNode node, bool) {
  74     Assert(node.getKind() == kind::FLOATINGPOINT_SUB);
  75     Node negation = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_NEG,node[2]);
  76     Node addition = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_PLUS,node[0],node[1],negation);
  77     return RewriteResponse(REWRITE_DONE, addition);
  78   }
  79
  80   RewriteResponse breakChain (TNode node, bool isPreRewrite) {
  81     Assert(isPreRewrite);  // Should be run first
  82
  83     Kind k = node.getKind();
  84     Assert(k == kind::FLOATINGPOINT_EQ ||
  85            k == kind::FLOATINGPOINT_GEQ ||
  86            k == kind::FLOATINGPOINT_LEQ ||
  87            k == kind::FLOATINGPOINT_GT ||
  88            k == kind::FLOATINGPOINT_LT);
  89
  90
  91     size_t children = node.getNumChildren();
  92     if (children > 2) {
  93
  94       NodeBuilder<> conjunction(kind::AND);
  95
  96       for (size_t i = 0; i < children - 1; ++i) {
  97         for (size_t j = i + 1; j < children; ++j) {
  98           conjunction << NodeManager::currentNM()->mkNode(k, node[i], node[j]);
  99         }
 100       }
 101       return RewriteResponse(REWRITE_AGAIN_FULL, conjunction);
 102
 103     } else {
 104       return RewriteResponse(REWRITE_DONE, node);
 105     }
 106   }
 107
 108
 109   /* Implies (fp.eq x x) --> (not (isNaN x))
 110    */
 111
 112   RewriteResponse ieeeEqToEq (TNode node, bool) {
 113     Assert(node.getKind() == kind::FLOATINGPOINT_EQ);
 114     NodeManager *nm = NodeManager::currentNM();
 115
 116     return RewriteResponse(REWRITE_DONE,
 117                            nm->mkNode(kind::AND,
 118                                       nm->mkNode(kind::AND,
 119                                                  nm->mkNode(kind::NOT, nm->mkNode(kind::FLOATINGPOINT_ISNAN, node[0])),
 120                                                  nm->mkNode(kind::NOT, nm->mkNode(kind::FLOATINGPOINT_ISNAN, node[1]))),
 121                                       nm->mkNode(kind::OR,
 122                                                  nm->mkNode(kind::EQUAL, node[0], node[1]),
 123                                                  nm->mkNode(kind::AND,
 124                                                             nm->mkNode(kind::FLOATINGPOINT_ISZ, node[0]),
 125                                                             nm->mkNode(kind::FLOATINGPOINT_ISZ, node[1])))));
 126   }
 127
 128
 129   RewriteResponse geqToleq (TNode node, bool) {
 130     Assert(node.getKind() == kind::FLOATINGPOINT_GEQ);
 131     return RewriteResponse(REWRITE_DONE,NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_LEQ,node[1],node[0]));
 132   }
 133
 134   RewriteResponse gtTolt (TNode node, bool) {
 135     Assert(node.getKind() == kind::FLOATINGPOINT_GT);
 136     return RewriteResponse(REWRITE_DONE,NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_LT,node[1],node[0]));
 137   }
 138
 139   RewriteResponse removed (TNode node, bool) {
 140     Unreachable("kind (%d) should have been removed?",node.getKind());
 141     return RewriteResponse(REWRITE_DONE, node);
 142   }
 143
 144   RewriteResponse variable (TNode node, bool) {
 145     // We should only get floating point and rounding mode variables to rewrite.
 146     TypeNode tn = node.getType(true);
 147     Assert(tn.isFloatingPoint() || tn.isRoundingMode());
 148
 149     // Not that we do anything with them...
 150     return RewriteResponse(REWRITE_DONE, node);
 151   }
 152
 153   RewriteResponse equal (TNode node, bool isPreRewrite) {
 154     // We should only get equalities of floating point or rounding mode types.
 155     Assert(node.getKind() == kind::EQUAL);
 156
 157     TypeNode tn = node[0].getType(true);
 158
 159     Assert(tn.isFloatingPoint() || tn.isRoundingMode());
 160     Assert(tn == node[1].getType(true));   // Should be ensured by the typing rules
 161
 162     if (node[0] == node[1]) {
 163       return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
 164     } else if (!isPreRewrite && (node[0] > node[1])) {
 165         Node normal = NodeManager::currentNM()->mkNode(kind::EQUAL,node[1],node[0]);
 166         return RewriteResponse(REWRITE_DONE, normal);
 167     } else {
 168       return RewriteResponse(REWRITE_DONE, node);
 169     }
 170   }
 171
 172   RewriteResponse convertFromRealLiteral (TNode node, bool) {
 173     Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_REAL);
 174
 175     // \todo Honour the rounding mode and work for something other than doubles!
 176
 177     if (node[1].getKind() == kind::CONST_RATIONAL) {
 178       TNode op = node.getOperator();
 179       const FloatingPointToFPReal &param = op.getConst<FloatingPointToFPReal>();
 180       Node lit =
 181         NodeManager::currentNM()->mkConst(FloatingPoint(param.t.exponent(),
 182                                                         param.t.significand(),
 183                                                         node[1].getConst<Rational>().getDouble()));
 184
 185       return RewriteResponse(REWRITE_DONE, lit);
 186     } else {
 187       return RewriteResponse(REWRITE_DONE, node);
 188     }
 189   }
 190
 191   RewriteResponse convertFromIEEEBitVectorLiteral (TNode node, bool) {
 192     Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR);
 193
 194     // \todo Handle arbitrary length bit vectors without using strings!
 195
 196     if (node[0].getKind() == kind::CONST_BITVECTOR) {
 197       TNode op = node.getOperator();
 198       const FloatingPointToFPIEEEBitVector &param = op.getConst<FloatingPointToFPIEEEBitVector>();
 199       const BitVector &bv = node[0].getConst<BitVector>();
 200       std::string bitString(bv.toString());
 201
 202       Node lit =
 203         NodeManager::currentNM()->mkConst(FloatingPoint(param.t.exponent(),
 204                                                         param.t.significand(),
 205                                                         bitString));
 206
 207       return RewriteResponse(REWRITE_DONE, lit);
 208     } else {
 209       return RewriteResponse(REWRITE_DONE, node);
 210     }
 211   }
 212
 213   RewriteResponse convertFromLiteral (TNode node, bool) {
 214     Assert(node.getKind() == kind::FLOATINGPOINT_FP);
 215
 216     // \todo Handle arbitrary length bit vectors without using strings!
 217
 218     if ((node[0].getKind() == kind::CONST_BITVECTOR) &&
 219         (node[1].getKind() == kind::CONST_BITVECTOR) &&
 220         (node[2].getKind() == kind::CONST_BITVECTOR)) {
 221
 222       BitVector bv(node[0].getConst<BitVector>());
 223       bv = bv.concat(node[1].getConst<BitVector>());
 224       bv = bv.concat(node[2].getConst<BitVector>());
 225
 226       std::string bitString(bv.toString());
 227       std::reverse(bitString.begin(), bitString.end());
 228
 229       // +1 to support the hidden bit
 230       Node lit =
 231         NodeManager::currentNM()->mkConst(FloatingPoint(node[1].getConst<BitVector>().getSize(),
 232                                                         node[2].getConst<BitVector>().getSize() + 1,
 233                                                         bitString));
 234
 235       return RewriteResponse(REWRITE_DONE, lit);
 236     } else {
 237       return RewriteResponse(REWRITE_DONE, node);
 238     }
 239   }
 240
 241   // Note these cannot be assumed to be symmetric for +0/-0, thus no symmetry reorder
 242   RewriteResponse compactMinMax (TNode node, bool isPreRewrite) {
 243 #ifdef CVC4_ASSERTIONS
 244     Kind k = node.getKind();
 245     Assert((k == kind::FLOATINGPOINT_MIN) || (k == kind::FLOATINGPOINT_MAX));
 246 #endif
 247     if (node[0] == node[1]) {
 248       return RewriteResponse(REWRITE_DONE, node[0]);
 249     } else {
 250       return RewriteResponse(REWRITE_DONE, node);
 251     }
 252   }
 253
 254
 255   RewriteResponse reorderFPEquality (TNode node, bool isPreRewrite) {
 256     Assert(node.getKind() == kind::FLOATINGPOINT_EQ);
 257     Assert(!isPreRewrite);    // Likely redundant in pre-rewrite
 258
 259     if (node[0] > node[1]) {
 260       Node normal = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_EQ,node[1],node[0]);
 261       return RewriteResponse(REWRITE_DONE, normal);
 262     } else {
 263       return RewriteResponse(REWRITE_DONE, node);
 264     }
 265   }
 266
 267   RewriteResponse reorderBinaryOperation (TNode node, bool isPreRewrite) {
 268     Kind k = node.getKind();
 269     Assert((k == kind::FLOATINGPOINT_PLUS) || (k == kind::FLOATINGPOINT_MULT));
 270     Assert(!isPreRewrite);    // Likely redundant in pre-rewrite
 271
 272     if (node[1] > node[2]) {
 273       Node normal = NodeManager::currentNM()->mkNode(k,node[0],node[2],node[1]);
 274       return RewriteResponse(REWRITE_DONE, normal);
 275     } else {
 276       return RewriteResponse(REWRITE_DONE, node);
 277     }
 278   }
 279
 280   RewriteResponse reorderFMA (TNode node, bool isPreRewrite) {
 281     Assert(node.getKind() == kind::FLOATINGPOINT_FMA);
 282     Assert(!isPreRewrite);    // Likely redundant in pre-rewrite
 283
 284     if (node[1] > node[2]) {
 285       Node normal = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_FMA,node[0],node[2],node[1],node[3]);
 286       return RewriteResponse(REWRITE_DONE, normal);
 287     } else {
 288       return RewriteResponse(REWRITE_DONE, node);
 289     }
 290   }
 291
 292   RewriteResponse removeSignOperations (TNode node, bool isPreRewrite) {
 293     Assert(node.getKind() == kind::FLOATINGPOINT_ISN   ||
 294            node.getKind() == kind::FLOATINGPOINT_ISSN  ||
 295            node.getKind() == kind::FLOATINGPOINT_ISZ   ||
 296            node.getKind() == kind::FLOATINGPOINT_ISINF ||
 297            node.getKind() == kind::FLOATINGPOINT_ISNAN);
 298     Assert(node.getNumChildren() == 1);
 299
 300     Kind childKind(node[0].getKind());
 301
 302     if ((childKind == kind::FLOATINGPOINT_NEG) ||
 303         (childKind == kind::FLOATINGPOINT_ABS)) {
 304
 305       Node rewritten = NodeManager::currentNM()->mkNode(node.getKind(),node[0][0]);
 306       return RewriteResponse(REWRITE_AGAIN, rewritten);
 307     } else {
 308       return RewriteResponse(REWRITE_DONE, node);
 309     }
 310   }
 311
 312
 313 }; /* CVC4::theory::fp::rewrite */
 314
 315 RewriteFunction TheoryFpRewriter::preRewriteTable[kind::LAST_KIND];
 316 RewriteFunction TheoryFpRewriter::postRewriteTable[kind::LAST_KIND];
 317
 318
 319   /**
 320    * Initialize the rewriter.
 321    */
 322   void TheoryFpRewriter::init() {
 323
 324     /* Set up the pre-rewrite dispatch table */
 325     for (unsigned i = 0; i < kind::LAST_KIND; ++i) {
 326       preRewriteTable[i] = rewrite::notFP;
 327     }
 328
 329     /******** Constants ********/
 330     /* No rewriting possible for constants */
 331     preRewriteTable[kind::CONST_FLOATINGPOINT] = rewrite::identity;
 332     preRewriteTable[kind::CONST_ROUNDINGMODE] = rewrite::identity;
 333
 334     /******** Sorts(?) ********/
 335     /* These kinds should only appear in types */
 336     //preRewriteTable[kind::ROUNDINGMODE_TYPE] = rewrite::type;
 337     preRewriteTable[kind::FLOATINGPOINT_TYPE] = rewrite::type;
 338
 339     /******** Operations ********/
 340     preRewriteTable[kind::FLOATINGPOINT_FP] = rewrite::identity;
 341     preRewriteTable[kind::FLOATINGPOINT_ABS] = rewrite::identity;
 342     preRewriteTable[kind::FLOATINGPOINT_NEG] = rewrite::removeDoubleNegation;
 343     preRewriteTable[kind::FLOATINGPOINT_PLUS] = rewrite::identity;
 344     preRewriteTable[kind::FLOATINGPOINT_SUB] = rewrite::convertSubtractionToAddition;
 345     preRewriteTable[kind::FLOATINGPOINT_MULT] = rewrite::identity;
 346     preRewriteTable[kind::FLOATINGPOINT_DIV] = rewrite::identity;
 347     preRewriteTable[kind::FLOATINGPOINT_FMA] = rewrite::identity;
 348     preRewriteTable[kind::FLOATINGPOINT_SQRT] = rewrite::identity;
 349     preRewriteTable[kind::FLOATINGPOINT_REM] = rewrite::identity;
 350     preRewriteTable[kind::FLOATINGPOINT_RTI] = rewrite::identity;
 351     preRewriteTable[kind::FLOATINGPOINT_MIN] = rewrite::compactMinMax;
 352     preRewriteTable[kind::FLOATINGPOINT_MAX] = rewrite::compactMinMax;
 353
 354     /******** Comparisons ********/
 355     preRewriteTable[kind::FLOATINGPOINT_EQ] = rewrite::then<rewrite::breakChain,rewrite::ieeeEqToEq>;
 356     preRewriteTable[kind::FLOATINGPOINT_LEQ] = rewrite::breakChain;
 357     preRewriteTable[kind::FLOATINGPOINT_LT] = rewrite::breakChain;
 358     preRewriteTable[kind::FLOATINGPOINT_GEQ] = rewrite::then<rewrite::breakChain,rewrite::geqToleq>;
 359     preRewriteTable[kind::FLOATINGPOINT_GT] = rewrite::then<rewrite::breakChain,rewrite::gtTolt>;
 360
 361     /******** Classifications ********/
 362     preRewriteTable[kind::FLOATINGPOINT_ISN] = rewrite::identity;
 363     preRewriteTable[kind::FLOATINGPOINT_ISSN] = rewrite::identity;
 364     preRewriteTable[kind::FLOATINGPOINT_ISZ] = rewrite::identity;
 365     preRewriteTable[kind::FLOATINGPOINT_ISINF] = rewrite::identity;
 366     preRewriteTable[kind::FLOATINGPOINT_ISNAN] = rewrite::identity;
 367     preRewriteTable[kind::FLOATINGPOINT_ISNEG] = rewrite::identity;
 368     preRewriteTable[kind::FLOATINGPOINT_ISPOS] = rewrite::identity;
 369
 370     /******** Conversions ********/
 371     preRewriteTable[kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR] = rewrite::identity;
 372     preRewriteTable[kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT] = rewrite::identity;
 373     preRewriteTable[kind::FLOATINGPOINT_TO_FP_REAL] = rewrite::identity;
 374     preRewriteTable[kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR] = rewrite::identity;
 375     preRewriteTable[kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR] = rewrite::identity;
 376     preRewriteTable[kind::FLOATINGPOINT_TO_FP_GENERIC] = rewrite::removed;
 377     preRewriteTable[kind::FLOATINGPOINT_TO_UBV] = rewrite::identity;
 378     preRewriteTable[kind::FLOATINGPOINT_TO_SBV] = rewrite::identity;
 379     preRewriteTable[kind::FLOATINGPOINT_TO_REAL] = rewrite::identity;
 380
 381     /******** Variables ********/
 382     preRewriteTable[kind::VARIABLE] = rewrite::variable;
 383     preRewriteTable[kind::BOUND_VARIABLE] = rewrite::variable;
 384
 385     preRewriteTable[kind::EQUAL] = rewrite::equal;
 386
 387
 388
 389
 390     /* Set up the post-rewrite dispatch table */
 391     for (unsigned i = 0; i < kind::LAST_KIND; ++i) {
 392       postRewriteTable[i] = rewrite::notFP;
 393     }
 394
 395     /******** Constants ********/
 396     /* No rewriting possible for constants */
 397     postRewriteTable[kind::CONST_FLOATINGPOINT] = rewrite::identity;
 398     postRewriteTable[kind::CONST_ROUNDINGMODE] = rewrite::identity;
 399
 400     /******** Sorts(?) ********/
 401     /* These kinds should only appear in types */
 402     //postRewriteTable[kind::ROUNDINGMODE_TYPE] = rewrite::type;
 403     postRewriteTable[kind::FLOATINGPOINT_TYPE] = rewrite::type;
 404
 405     /******** Operations ********/
 406     postRewriteTable[kind::FLOATINGPOINT_FP] = rewrite::convertFromLiteral;
 407     postRewriteTable[kind::FLOATINGPOINT_ABS] = rewrite::identity;
 408     postRewriteTable[kind::FLOATINGPOINT_NEG] = rewrite::removeDoubleNegation;
 409     postRewriteTable[kind::FLOATINGPOINT_PLUS] = rewrite::reorderBinaryOperation;
 410     postRewriteTable[kind::FLOATINGPOINT_SUB] = rewrite::removed;
 411     postRewriteTable[kind::FLOATINGPOINT_MULT] = rewrite::reorderBinaryOperation;
 412     postRewriteTable[kind::FLOATINGPOINT_DIV] = rewrite::identity;
 413     postRewriteTable[kind::FLOATINGPOINT_FMA] = rewrite::reorderFMA;
 414     postRewriteTable[kind::FLOATINGPOINT_SQRT] = rewrite::identity;
 415     postRewriteTable[kind::FLOATINGPOINT_REM] = rewrite::identity;
 416     postRewriteTable[kind::FLOATINGPOINT_RTI] = rewrite::identity;
 417     postRewriteTable[kind::FLOATINGPOINT_MIN] = rewrite::compactMinMax;
 418     postRewriteTable[kind::FLOATINGPOINT_MAX] = rewrite::compactMinMax;
 419
 420     /******** Comparisons ********/
 421     postRewriteTable[kind::FLOATINGPOINT_EQ] = rewrite::removed;
 422     postRewriteTable[kind::FLOATINGPOINT_LEQ] = rewrite::identity;
 423     postRewriteTable[kind::FLOATINGPOINT_LT] = rewrite::identity;
 424     postRewriteTable[kind::FLOATINGPOINT_GEQ] = rewrite::removed;
 425     postRewriteTable[kind::FLOATINGPOINT_GT] = rewrite::removed;
 426
 427     /******** Classifications ********/
 428     postRewriteTable[kind::FLOATINGPOINT_ISN] = rewrite::removeSignOperations;
 429     postRewriteTable[kind::FLOATINGPOINT_ISSN] = rewrite::removeSignOperations;
 430     postRewriteTable[kind::FLOATINGPOINT_ISZ] = rewrite::removeSignOperations;
 431     postRewriteTable[kind::FLOATINGPOINT_ISINF] = rewrite::removeSignOperations;
 432     postRewriteTable[kind::FLOATINGPOINT_ISNAN] = rewrite::removeSignOperations;
 433     postRewriteTable[kind::FLOATINGPOINT_ISNEG] = rewrite::identity;
 434     postRewriteTable[kind::FLOATINGPOINT_ISPOS] = rewrite::identity;
 435
 436     /******** Conversions ********/
 437     postRewriteTable[kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR] = rewrite::convertFromIEEEBitVectorLiteral;
 438     postRewriteTable[kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT] = rewrite::identity;
 439     postRewriteTable[kind::FLOATINGPOINT_TO_FP_REAL] = rewrite::convertFromRealLiteral;
 440     postRewriteTable[kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR] = rewrite::identity;
 441     postRewriteTable[kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR] = rewrite::identity;
 442     postRewriteTable[kind::FLOATINGPOINT_TO_FP_GENERIC] = rewrite::removed;
 443     postRewriteTable[kind::FLOATINGPOINT_TO_UBV] = rewrite::identity;
 444     postRewriteTable[kind::FLOATINGPOINT_TO_SBV] = rewrite::identity;
 445     postRewriteTable[kind::FLOATINGPOINT_TO_REAL] = rewrite::identity;
 446
 447     /******** Variables ********/
 448     postRewriteTable[kind::VARIABLE] = rewrite::variable;
 449     postRewriteTable[kind::BOUND_VARIABLE] = rewrite::variable;
 450
 451     postRewriteTable[kind::EQUAL] = rewrite::equal;
 452
 453
 454   }
 455
 456
 457
 458
 459   /**
 460    * Rewrite a node into the normal form for the theory of fp
 461    * in pre-order (really topological order)---meaning that the
 462    * children may not be in the normal form.  This is an optimization
 463    * for theories with cancelling terms (e.g., 0 * (big-nasty-expression)
 464    * in arithmetic rewrites to 0 without the need to look at the big
 465    * nasty expression).  Since it's only an optimization, the
 466    * implementation here can do nothing.
 467    */
 468
 469   RewriteResponse TheoryFpRewriter::preRewrite(TNode node) {
 470     Trace("fp-rewrite") << "TheoryFpRewriter::preRewrite(): " << node << std::endl;
 471     RewriteResponse res = preRewriteTable [node.getKind()] (node, true);
 472     if (res.node != node) {
 473       Debug("fp-rewrite") << "TheoryFpRewriter::preRewrite(): before " << node << std::endl;
 474       Debug("fp-rewrite") << "TheoryFpRewriter::preRewrite(): after  " << res.node << std::endl;
 475     }
 476     return res;
 477   }
 478
 479
 480   /**
 481    * Rewrite a node into the normal form for the theory of fp.
 482    * Called in post-order (really reverse-topological order) when
 483    * traversing the expression DAG during rewriting.  This is the
 484    * main function of the rewriter, and because of the ordering,
 485    * it can assume its children are all rewritten already.
 486    *
 487    * This function can return one of three rewrite response codes
 488    * along with the rewritten node:
 489    *
 490    *   REWRITE_DONE indicates that no more rewriting is needed.
 491    *   REWRITE_AGAIN means that the top-level expression should be
 492    *     rewritten again, but that its children are in final form.
 493    *   REWRITE_AGAIN_FULL means that the entire returned expression
 494    *     should be rewritten again (top-down with preRewrite(), then
 495    *     bottom-up with postRewrite()).
 496    *
 497    * Even if this function returns REWRITE_DONE, if the returned
 498    * expression belongs to a different theory, it will be fully
 499    * rewritten by that theory's rewriter.
 500    */
 501
 502   RewriteResponse TheoryFpRewriter::postRewrite(TNode node) {
 503     Trace("fp-rewrite") << "TheoryFpRewriter::postRewrite(): " << node << std::endl;
 504     RewriteResponse res = postRewriteTable [node.getKind()] (node, false);
 505     if (res.node != node) {
 506       Debug("fp-rewrite") << "TheoryFpRewriter::postRewrite(): before " << node << std::endl;
 507       Debug("fp-rewrite") << "TheoryFpRewriter::postRewrite(): after  " << res.node << std::endl;
 508     }
 509     return res;
 510   }
 511
 512
 513 }/* CVC4::theory::fp namespace */
 514 }/* CVC4::theory namespace */
 515 }/* CVC4 namespace */
 516