src/theory/bv/theory_bv_rewrite_rules_simplification.h

   1 /*********************                                                        */
   2 /*! \file theory_bv_rewrite_rules_simplification.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Liana Hadarean, Aina Niemetz, Mathias Preiner
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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 "cvc4_private.h"
  19
  20 #pragma once
  21
  22 #include "options/bv_options.h"
  23 #include "theory/bv/theory_bv_rewrite_rules.h"
  24 #include "theory/bv/theory_bv_utils.h"
  25 #include "theory/rewriter.h"
  26
  27 namespace CVC4 {
  28 namespace theory {
  29 namespace bv {
  30
  31 /* -------------------------------------------------------------------------- */
  32
  33 /**
  34  * BitOfConst
  35  */
  36 template <>
  37 inline bool RewriteRule<BitOfConst>::applies(TNode node)
  38 {
  39   return node.getKind() == kind::BITVECTOR_BITOF && node[0].isConst();
  40 }
  41
  42 template <>
  43 inline Node RewriteRule<BitOfConst>::apply(TNode node)
  44 {
  45   size_t pos = node.getOperator().getConst<BitVectorBitOf>().d_bitIndex;
  46   return utils::getBit(node[0], pos) ? utils::mkTrue() : utils::mkFalse();
  47 }
  48
  49 /* -------------------------------------------------------------------------- */
  50
  51 /**
  52  * BvIteConstCond
  53  *
  54  * BITVECTOR_ITE with constant condition
  55  */
  56 template <>
  57 inline bool RewriteRule<BvIteConstCond>::applies(TNode node)
  58 {
  59   return (node.getKind() == kind::BITVECTOR_ITE && node[0].isConst());
  60 }
  61
  62 template <>
  63 inline Node RewriteRule<BvIteConstCond>::apply(TNode node)
  64 {
  65   Debug("bv-rewrite") << "RewriteRule<BvIteConstCond>(" << node << ")"
  66                       << std::endl;
  67   return utils::isZero(node[0]) ? node[2] : node[1];
  68 }
  69
  70 /* -------------------------------------------------------------------------- */
  71
  72 /**
  73  * BvIteEqualChildren
  74  *
  75  * BITVECTOR_ITE with term_then = term_else
  76  */
  77 template <>
  78 inline bool RewriteRule<BvIteEqualChildren>::applies(TNode node)
  79 {
  80   return (node.getKind() == kind::BITVECTOR_ITE && node[1] == node[2]);
  81 }
  82
  83 template <>
  84 inline Node RewriteRule<BvIteEqualChildren>::apply(TNode node)
  85 {
  86   Debug("bv-rewrite") << "RewriteRule<BvIteEqualChildren>(" << node << ")"
  87                       << std::endl;
  88   return node[1];
  89 }
  90
  91 /* -------------------------------------------------------------------------- */
  92
  93 /**
  94  * BvIteConstChildren
  95  *
  96  * BITVECTOR_ITE with constant children of size one
  97  */
  98 template <>
  99 inline bool RewriteRule<BvIteConstChildren>::applies(TNode node)
 100 {
 101   return (node.getKind() == kind::BITVECTOR_ITE
 102           && utils::getSize(node[1]) == 1
 103           && node[1].isConst() && node[2].isConst());
 104 }
 105
 106 template <>
 107 inline Node RewriteRule<BvIteConstChildren>::apply(TNode node)
 108 {
 109   Debug("bv-rewrite") << "RewriteRule<BvIteConstChildren>(" << node << ")"
 110                       << std::endl;
 111   if (utils::isOne(node[1]) && utils::isZero(node[2]))
 112   {
 113     return node[0];
 114   }
 115   Assert(utils::isZero(node[1]) && utils::isOne(node[2]));
 116   return NodeManager::currentNM()->mkNode(kind::BITVECTOR_NOT, node[0]);
 117 }
 118
 119 /* -------------------------------------------------------------------------- */
 120
 121 /**
 122  * BvIteEqualCond
 123  *
 124  * Nested BITVECTOR_ITE with cond_outer == cond_inner
 125  *
 126  * c0 ? (c0 ? t0 : e0) : e1              ->  c0 ? t0 : e1
 127  * c0 ? t0             : (c0 ? t1 : e1)  ->  c0 ? t0 : e1
 128  * c0 ? (c0 ? t0 : e0) : (c0 ? t1 : e1)  ->  c0 ? t0 : e1
 129  */
 130 template <>
 131 inline bool RewriteRule<BvIteEqualCond>::applies(TNode node)
 132 {
 133   return (
 134       node.getKind() == kind::BITVECTOR_ITE
 135       && ((node[1].getKind() == kind::BITVECTOR_ITE && node[0] == node[1][0])
 136           || (node[2].getKind() == kind::BITVECTOR_ITE
 137               && node[0] == node[2][0])));
 138 }
 139
 140 template <>
 141 inline Node RewriteRule<BvIteEqualCond>::apply(TNode node)
 142 {
 143   Debug("bv-rewrite") << "RewriteRule<BvIteEqualCond>(" << node << ")"
 144                       << std::endl;
 145   Node t0 = node[1].getKind() == kind::BITVECTOR_ITE && node[0] == node[1][0]
 146                 ? node[1][1]
 147                 : node[1];
 148   Node e1 = node[2].getKind() == kind::BITVECTOR_ITE && node[0] == node[2][0]
 149                 ? node[2][2]
 150                 : node[2];
 151   return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ITE, node[0], t0, e1);
 152 }
 153
 154 /* -------------------------------------------------------------------------- */
 155
 156 /**
 157  * BvIteMergeThenIf
 158  *
 159  * Nested BITVECTOR_ITE of the form
 160  *   c0 ? (c1 ? t1 : e1) : t1  ->  c0 AND NOT(c1) ? e1 : t1
 161  */
 162 template <>
 163 inline bool RewriteRule<BvIteMergeThenIf>::applies(TNode node)
 164 {
 165   return (node.getKind() == kind::BITVECTOR_ITE
 166           && node[1].getKind() == kind::BITVECTOR_ITE
 167           && node[1][1] == node[2]);
 168 }
 169
 170 template <>
 171 inline Node RewriteRule<BvIteMergeThenIf>::apply(TNode node)
 172 {
 173   Debug("bv-rewrite") << "RewriteRule<BvIteMergeThenIf>(" << node << ")"
 174                       << std::endl;
 175   NodeManager* nm = NodeManager::currentNM();
 176   Assert(node[1].getKind() == kind::BITVECTOR_ITE);
 177   Node cond = nm->mkNode(kind::BITVECTOR_AND,
 178                          node[0],
 179                          nm->mkNode(kind::BITVECTOR_NOT, node[1][0]));
 180   return nm->mkNode(kind::BITVECTOR_ITE, cond, node[1][2], node[2]);
 181 }
 182
 183 /* -------------------------------------------------------------------------- */
 184
 185 /**
 186  * BvIteMergeElseIf
 187  *
 188  * Nested BITVECTOR_ITE of the form
 189  *   c0 ? (c1 ? t1 : e1) : e1  ->  c0 AND c1 ? t1 : e1
 190  */
 191 template <>
 192 inline bool RewriteRule<BvIteMergeElseIf>::applies(TNode node)
 193 {
 194   return (node.getKind() == kind::BITVECTOR_ITE
 195           && node[1].getKind() == kind::BITVECTOR_ITE
 196           && node[1][2] == node[2]);
 197 }
 198
 199 template <>
 200 inline Node RewriteRule<BvIteMergeElseIf>::apply(TNode node)
 201 {
 202   Debug("bv-rewrite") << "RewriteRule<BvIteMergeElseIf>(" << node << ")"
 203                       << std::endl;
 204   NodeManager* nm = NodeManager::currentNM();
 205   Assert(node[1].getKind() == kind::BITVECTOR_ITE);
 206   Node cond = nm->mkNode(kind::BITVECTOR_AND, node[0], node[1][0]);
 207   return nm->mkNode(kind::BITVECTOR_ITE, cond, node[1][1], node[2]);
 208 }
 209
 210 /* -------------------------------------------------------------------------- */
 211
 212 /**
 213  * BvIteMergeThenElse
 214  *
 215  * Nested BITVECTOR_ITE of the form
 216  *   c0 ? t0 : (c1 ? t0 : e1)  ->  NOT(c0) AND NOT(c1) ? e1 : t0
 217  */
 218 template <>
 219 inline bool RewriteRule<BvIteMergeThenElse>::applies(TNode node)
 220 {
 221   return (node.getKind() == kind::BITVECTOR_ITE
 222           && node[2].getKind() == kind::BITVECTOR_ITE
 223           && node[1] == node[2][1]);
 224 }
 225
 226 template <>
 227 inline Node RewriteRule<BvIteMergeThenElse>::apply(TNode node)
 228 {
 229   Debug("bv-rewrite") << "RewriteRule<BvIteMergeThenElse>(" << node << ")"
 230                       << std::endl;
 231   NodeManager* nm = NodeManager::currentNM();
 232   Assert(node[2].getKind() == kind::BITVECTOR_ITE);
 233   Node cond = nm->mkNode(kind::BITVECTOR_AND,
 234                          nm->mkNode(kind::BITVECTOR_NOT, node[0]),
 235                          nm->mkNode(kind::BITVECTOR_NOT, node[2][0]));
 236   return nm->mkNode(kind::BITVECTOR_ITE, cond, node[2][2], node[1]);
 237 }
 238
 239 /* -------------------------------------------------------------------------- */
 240
 241 /**
 242  * BvIteMergeElseElse
 243  *
 244  * Nested BITVECTOR_ITE of the form
 245  *   c0 ? t0 : (c1 ? t1 : t0)  ->  NOT(c0) AND c1 ? t1 : t0
 246  */
 247 template <>
 248 inline bool RewriteRule<BvIteMergeElseElse>::applies(TNode node)
 249 {
 250   return (node.getKind() == kind::BITVECTOR_ITE
 251           && node[2].getKind() == kind::BITVECTOR_ITE
 252           && node[1] == node[2][2]);
 253 }
 254
 255 template <>
 256 inline Node RewriteRule<BvIteMergeElseElse>::apply(TNode node)
 257 {
 258   Debug("bv-rewrite") << "RewriteRule<BvIteMergeElseElse>(" << node << ")"
 259                       << std::endl;
 260   NodeManager* nm = NodeManager::currentNM();
 261   Assert(node[2].getKind() == kind::BITVECTOR_ITE);
 262   Node cond = nm->mkNode(kind::BITVECTOR_AND,
 263                          nm->mkNode(kind::BITVECTOR_NOT, node[0]),
 264                          node[2][0]);
 265   return nm->mkNode(kind::BITVECTOR_ITE, cond, node[2][1], node[1]);
 266 }
 267
 268 /* -------------------------------------------------------------------------- */
 269
 270 /**
 271  * BvComp
 272  *
 273  * BITVECTOR_COMP of children of size 1 with one constant child
 274  */
 275 template <>
 276 inline bool RewriteRule<BvComp>::applies(TNode node)
 277 {
 278   return (node.getKind() == kind::BITVECTOR_COMP
 279           && utils::getSize(node[0]) == 1
 280           && (node[0].isConst() || node[1].isConst()));
 281 }
 282
 283 template <>
 284 inline Node RewriteRule<BvComp>::apply(TNode node)
 285 {
 286   Debug("bv-rewrite") << "RewriteRule<BvComp>(" << node << ")" << std::endl;
 287   NodeManager* nm = NodeManager::currentNM();
 288   if (node[0].isConst())
 289   {
 290     return utils::isZero(node[0]) ? nm->mkNode(kind::BITVECTOR_NOT, node[1])
 291                                   : Node(node[1]);
 292   }
 293   return utils::isZero(node[1]) ? nm->mkNode(kind::BITVECTOR_NOT, node[0])
 294                                 : Node(node[0]);
 295 }
 296
 297 /* -------------------------------------------------------------------------- */
 298
 299 /**
 300  * ShlByConst
 301  *
 302  * Left Shift by constant amount
 303  */
 304 template<> inline
 305 bool RewriteRule<ShlByConst>::applies(TNode node) {
 306   // if the shift amount is constant
 307   return (node.getKind() == kind::BITVECTOR_SHL &&
 308           node[1].getKind() == kind::CONST_BITVECTOR);
 309 }
 310
 311 template<> inline
 312 Node RewriteRule<ShlByConst>::apply(TNode node) {
 313   Debug("bv-rewrite") << "RewriteRule<ShlByConst>(" << node << ")" << std::endl;
 314   Integer amount = node[1].getConst<BitVector>().toInteger();
 315   if (amount == 0) {
 316     return node[0];
 317   }
 318   Node a = node[0];
 319   uint32_t size = utils::getSize(a);
 320
 321
 322   if (amount >= Integer(size)) {
 323     // if we are shifting more than the length of the bitvector return 0
 324     return utils::mkZero(size);
 325   }
 326
 327   // make sure we do not lose information casting
 328   Assert(amount < Integer(1).multiplyByPow2(32));
 329
 330   uint32_t uint32_amount = amount.toUnsignedInt();
 331
 332   Node left = utils::mkExtract(a, size - 1 - uint32_amount, 0);
 333   Node right = utils::mkZero(uint32_amount);
 334   return utils::mkConcat(left, right);
 335 }
 336
 337 /* -------------------------------------------------------------------------- */
 338
 339 /**
 340  * LshrByConst
 341  *
 342  * Right Logical Shift by constant amount
 343  */
 344
 345 template<> inline
 346 bool RewriteRule<LshrByConst>::applies(TNode node) {
 347   // if the shift amount is constant
 348   return (node.getKind() == kind::BITVECTOR_LSHR &&
 349           node[1].getKind() == kind::CONST_BITVECTOR);
 350 }
 351
 352 template<> inline
 353 Node RewriteRule<LshrByConst>::apply(TNode node) {
 354   Debug("bv-rewrite") << "RewriteRule<LshrByConst>(" << node << ")" << std::endl;
 355   Integer amount = node[1].getConst<BitVector>().toInteger();
 356   if (amount == 0) {
 357     return node[0];
 358   }
 359
 360   Node a = node[0];
 361   uint32_t size = utils::getSize(a);
 362
 363
 364   if (amount >= Integer(size)) {
 365     // if we are shifting more than the length of the bitvector return 0
 366     return utils::mkZero(size);
 367   }
 368
 369   // make sure we do not lose information casting
 370   Assert(amount < Integer(1).multiplyByPow2(32));
 371
 372   uint32_t uint32_amount = amount.toUnsignedInt();
 373   Node right = utils::mkExtract(a, size - 1, uint32_amount);
 374   Node left = utils::mkZero(uint32_amount);
 375   return utils::mkConcat(left, right);
 376 }
 377
 378 /* -------------------------------------------------------------------------- */
 379
 380 /**
 381  * AshrByConst
 382  *
 383  * Right Arithmetic Shift by constant amount
 384  */
 385
 386 template<> inline
 387 bool RewriteRule<AshrByConst>::applies(TNode node) {
 388   // if the shift amount is constant
 389   return (node.getKind() == kind::BITVECTOR_ASHR &&
 390           node[1].getKind() == kind::CONST_BITVECTOR);
 391 }
 392
 393 template<> inline
 394 Node RewriteRule<AshrByConst>::apply(TNode node) {
 395   Debug("bv-rewrite") << "RewriteRule<AshrByConst>(" << node << ")" << std::endl;
 396   Integer amount = node[1].getConst<BitVector>().toInteger();
 397   if (amount == 0) {
 398     return node[0];
 399   }
 400
 401   Node a = node[0];
 402   uint32_t size = utils::getSize(a);
 403   Node sign_bit = utils::mkExtract(a, size-1, size-1);
 404
 405   if (amount >= Integer(size)) {
 406     // if we are shifting more than the length of the bitvector return n repetitions
 407     // of the first bit
 408     return utils::mkConcat(sign_bit, size);
 409   }
 410
 411   // make sure we do not lose information casting
 412   Assert(amount < Integer(1).multiplyByPow2(32));
 413
 414   uint32_t uint32_amount = amount.toUnsignedInt();
 415   if (uint32_amount == 0) {
 416     return a;
 417   }
 418
 419   Node left = utils::mkConcat(sign_bit, uint32_amount);
 420   Node right = utils::mkExtract(a, size - 1, uint32_amount);
 421   return utils::mkConcat(left, right);
 422 }
 423
 424 /* -------------------------------------------------------------------------- */
 425
 426 /**
 427  * BitwiseIdemp
 428  *
 429  * (a bvand a) ==> a
 430  * (a bvor a)  ==> a
 431  */
 432
 433 template<> inline
 434 bool RewriteRule<BitwiseIdemp>::applies(TNode node) {
 435   Unreachable();
 436   return ((node.getKind() == kind::BITVECTOR_AND ||
 437            node.getKind() == kind::BITVECTOR_OR) &&
 438           node.getNumChildren() == 2 &&
 439           node[0] == node[1]);
 440 }
 441
 442 template<> inline
 443 Node RewriteRule<BitwiseIdemp>::apply(TNode node) {
 444   Unreachable();
 445   Debug("bv-rewrite") << "RewriteRule<BitwiseIdemp>(" << node << ")" << std::endl;
 446   return node[0];
 447 }
 448
 449 /* -------------------------------------------------------------------------- */
 450
 451 /**
 452  * AndZero
 453  *
 454  * (a bvand 0) ==> 0
 455  */
 456
 457 template<> inline
 458 bool RewriteRule<AndZero>::applies(TNode node) {
 459   Unreachable();
 460   unsigned size = utils::getSize(node);
 461   return (node.getKind() == kind::BITVECTOR_AND  &&
 462           node.getNumChildren() == 2 &&
 463           (node[0] == utils::mkConst(size, 0) ||
 464            node[1] == utils::mkConst(size, 0)));
 465 }
 466
 467 template<> inline
 468 Node RewriteRule<AndZero>::apply(TNode node) {
 469   Unreachable();
 470   Debug("bv-rewrite") << "RewriteRule<AndZero>(" << node << ")" << std::endl;
 471   return utils::mkConst(utils::getSize(node), 0);
 472 }
 473
 474 /* -------------------------------------------------------------------------- */
 475
 476 /**
 477  * AndOne
 478  *
 479  * (a bvand 1) ==> a
 480  */
 481
 482 template<> inline
 483 bool RewriteRule<AndOne>::applies(TNode node) {
 484   Unreachable();
 485   unsigned size = utils::getSize(node);
 486   Node ones = utils::mkOnes(size);
 487   return (node.getKind() == kind::BITVECTOR_AND  &&
 488           node.getNumChildren() == 2 &&
 489           (node[0] == ones ||
 490            node[1] == ones));
 491 }
 492
 493 template<> inline
 494 Node RewriteRule<AndOne>::apply(TNode node) {
 495   Unreachable();
 496   Debug("bv-rewrite") << "RewriteRule<AndOne>(" << node << ")" << std::endl;
 497   unsigned size = utils::getSize(node);
 498
 499   if (node[0] == utils::mkOnes(size)) {
 500     return node[1];
 501   } else {
 502     Assert(node[1] == utils::mkOnes(size));
 503     return node[0];
 504   }
 505 }
 506
 507 /* -------------------------------------------------------------------------- */
 508
 509 /**
 510  * AndOrXorConcatPullUp
 511  *
 512  * Match:       x_m <op> concat(y_my, <const>_n, z_mz)
 513  *              <const>_n in { 0_n, 1_n, ~0_n }
 514  *
 515  * Rewrites to: concat(x[m-1:m-my]  <op> y,
 516  *                     x[m-my-1:mz] <op> <const>_n,
 517  *                     x[mz-1:0]    <op> z)
 518  */
 519
 520 template <>
 521 inline bool RewriteRule<AndOrXorConcatPullUp>::applies(TNode node)
 522 {
 523   if (node.getKind() != kind::BITVECTOR_AND
 524       && node.getKind() != kind::BITVECTOR_OR
 525       && node.getKind() != kind::BITVECTOR_XOR)
 526   {
 527     return false;
 528   }
 529
 530   TNode n;
 531
 532   for (const TNode& c : node)
 533   {
 534     if (c.getKind() == kind::BITVECTOR_CONCAT)
 535     {
 536       for (const TNode& cc : c)
 537       {
 538         if (cc.isConst())
 539         {
 540           n = cc;
 541           break;
 542         }
 543       }
 544       break;
 545     }
 546   }
 547   if (n.isNull()) return false;
 548   return utils::isZero(n) || utils::isOne(n) || utils::isOnes(n);
 549 }
 550
 551 template <>
 552 inline Node RewriteRule<AndOrXorConcatPullUp>::apply(TNode node)
 553 {
 554   Debug("bv-rewrite") << "RewriteRule<AndOrXorConcatPullUp>(" << node << ")"
 555                       << std::endl;
 556   uint32_t m, my, mz;
 557   size_t nc;
 558   Kind kind = node.getKind();
 559   TNode concat;
 560   Node x, y, z, c;
 561   NodeBuilder<> xb(kind);
 562   NodeBuilder<> yb(kind::BITVECTOR_CONCAT);
 563   NodeBuilder<> zb(kind::BITVECTOR_CONCAT);
 564   NodeBuilder<> res(kind::BITVECTOR_CONCAT);
 565   NodeManager* nm = NodeManager::currentNM();
 566
 567   for (const TNode& child : node)
 568   {
 569     if (concat.isNull() && child.getKind() == kind::BITVECTOR_CONCAT)
 570     {
 571       concat = child;
 572     }
 573     else
 574     {
 575       xb << child;
 576     }
 577   }
 578   x = xb.getNumChildren() > 1 ? xb.constructNode() : xb[0];
 579
 580   for (const TNode& child : concat)
 581   {
 582     if (c.isNull())
 583     {
 584       if (utils::isZero(child) || utils::isOne(child) || utils::isOnes(child))
 585       {
 586         c = child;
 587       }
 588       else
 589       {
 590         yb << child;
 591       }
 592     }
 593     else
 594     {
 595       zb << child;
 596     }
 597   }
 598   Assert(!c.isNull());
 599   Assert(yb.getNumChildren() || zb.getNumChildren());
 600
 601   if ((nc = yb.getNumChildren()) > 0)
 602   {
 603     y = nc > 1 ? yb.constructNode() : yb[0];
 604   }
 605   if ((nc = zb.getNumChildren()) > 0)
 606   {
 607     z = nc > 1 ? zb.constructNode() : zb[0];
 608   }
 609   m = utils::getSize(x);
 610 #ifdef CVC4_ASSERTIONS
 611   uint32_t n = utils::getSize(c);
 612 #endif
 613   my = y.isNull() ? 0 : utils::getSize(y);
 614   mz = z.isNull() ? 0 : utils::getSize(z);
 615   Assert(mz == m - my - n);
 616   Assert(my || mz);
 617
 618   if (my)
 619   {
 620     res << nm->mkNode(kind, utils::mkExtract(x, m - 1, m - my), y);
 621   }
 622
 623   res << nm->mkNode(kind, utils::mkExtract(x, m - my - 1, mz), c);
 624
 625   if (mz)
 626   {
 627     res << nm->mkNode(kind, utils::mkExtract(x, mz - 1, 0), z);
 628   }
 629
 630   return res;
 631 }
 632
 633 /* -------------------------------------------------------------------------- */
 634
 635 /**
 636  * OrZero
 637  *
 638  * (a bvor 0) ==> a
 639  */
 640
 641 template<> inline
 642 bool RewriteRule<OrZero>::applies(TNode node) {
 643   Unreachable();
 644   unsigned size = utils::getSize(node);
 645   return (node.getKind() == kind::BITVECTOR_OR  &&
 646           node.getNumChildren() == 2 &&
 647           (node[0] == utils::mkConst(size, 0) ||
 648            node[1] == utils::mkConst(size, 0)));
 649 }
 650
 651 template<> inline
 652 Node RewriteRule<OrZero>::apply(TNode node) {
 653   Unreachable();
 654   Debug("bv-rewrite") << "RewriteRule<OrZero>(" << node << ")" << std::endl;
 655
 656   unsigned size = utils::getSize(node);
 657   if (node[0] == utils::mkConst(size, 0)) {
 658     return node[1];
 659   } else {
 660     Assert(node[1] == utils::mkConst(size, 0));
 661     return node[0];
 662   }
 663 }
 664
 665 /* -------------------------------------------------------------------------- */
 666
 667 /**
 668  * OrOne
 669  *
 670  * (a bvor 1) ==> 1
 671  */
 672
 673 template<> inline
 674 bool RewriteRule<OrOne>::applies(TNode node) {
 675   Unreachable();
 676   unsigned size = utils::getSize(node);
 677   Node ones = utils::mkOnes(size);
 678   return (node.getKind() == kind::BITVECTOR_OR  &&
 679           node.getNumChildren() == 2 &&
 680           (node[0] == ones ||
 681            node[1] == ones));
 682 }
 683
 684 template<> inline
 685 Node RewriteRule<OrOne>::apply(TNode node) {
 686   Unreachable();
 687   Debug("bv-rewrite") << "RewriteRule<OrOne>(" << node << ")" << std::endl;
 688   return utils::mkOnes(utils::getSize(node));
 689 }
 690
 691 /* -------------------------------------------------------------------------- */
 692
 693 /**
 694  * XorDuplicate
 695  *
 696  * (a bvxor a) ==> 0
 697  */
 698
 699 template<> inline
 700 bool RewriteRule<XorDuplicate>::applies(TNode node) {
 701   Unreachable();
 702   return (node.getKind() == kind::BITVECTOR_XOR &&
 703           node.getNumChildren() == 2 &&
 704           node[0] == node[1]);
 705 }
 706
 707 template<> inline
 708 Node RewriteRule<XorDuplicate>::apply(TNode node) {
 709   Unreachable();
 710   Debug("bv-rewrite") << "RewriteRule<XorDuplicate>(" << node << ")" << std::endl;
 711   return utils::mkZero(utils::getSize(node));
 712 }
 713
 714 /* -------------------------------------------------------------------------- */
 715
 716 /**
 717  * XorOne
 718  *
 719  * (a bvxor 1) ==> ~a
 720  */
 721
 722 template<> inline
 723 bool RewriteRule<XorOne>::applies(TNode node) {
 724   if (node.getKind() != kind::BITVECTOR_XOR) {
 725     return false;
 726   }
 727   Node ones = utils::mkOnes(utils::getSize(node));
 728   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
 729     if (node[i] == ones) {
 730       return true;
 731     }
 732   }
 733   return false;
 734 }
 735
 736 template <>
 737 inline Node RewriteRule<XorOne>::apply(TNode node)
 738 {
 739   Debug("bv-rewrite") << "RewriteRule<XorOne>(" << node << ")" << std::endl;
 740   NodeManager *nm = NodeManager::currentNM();
 741   Node ones = utils::mkOnes(utils::getSize(node));
 742   std::vector<Node> children;
 743   bool found_ones = false;
 744   // XorSimplify should have been called before
 745   for (unsigned i = 0; i < node.getNumChildren(); ++i)
 746   {
 747     if (node[i] == ones)
 748     {
 749       // make sure only ones occurs only once
 750       found_ones = !found_ones;
 751     }
 752     else
 753     {
 754       children.push_back(node[i]);
 755     }
 756   }
 757
 758   Node result = utils::mkNaryNode(kind::BITVECTOR_XOR, children);
 759   if (found_ones)
 760   {
 761     result = nm->mkNode(kind::BITVECTOR_NOT, result);
 762   }
 763   return result;
 764 }
 765
 766 /* -------------------------------------------------------------------------- */
 767
 768 /**
 769  * XorZero
 770  *
 771  * (a bvxor 0) ==> a
 772  */
 773
 774 template<> inline
 775 bool RewriteRule<XorZero>::applies(TNode node) {
 776   if (node.getKind() != kind::BITVECTOR_XOR) {
 777     return false;
 778   }
 779   Node zero = utils::mkConst(utils::getSize(node), 0);
 780   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
 781     if (node[i] == zero) {
 782       return true;
 783     }
 784   }
 785   return false;
 786 }
 787
 788 template <>
 789 inline Node RewriteRule<XorZero>::apply(TNode node)
 790 {
 791   Debug("bv-rewrite") << "RewriteRule<XorZero>(" << node << ")" << std::endl;
 792   std::vector<Node> children;
 793   Node zero = utils::mkConst(utils::getSize(node), 0);
 794
 795   // XorSimplify should have been called before
 796   for (unsigned i = 0; i < node.getNumChildren(); ++i)
 797   {
 798     if (node[i] != zero)
 799     {
 800       children.push_back(node[i]);
 801     }
 802   }
 803   Node res = utils::mkNaryNode(kind::BITVECTOR_XOR, children);
 804   return res;
 805 }
 806
 807 /* -------------------------------------------------------------------------- */
 808
 809 /**
 810  * BitwiseNotAnd
 811  *
 812  * (a bvand (~ a)) ==> 0
 813  */
 814
 815 template<> inline
 816 bool RewriteRule<BitwiseNotAnd>::applies(TNode node) {
 817   Unreachable();
 818   return (node.getKind() == kind::BITVECTOR_AND &&
 819           node.getNumChildren() == 2 &&
 820           ((node[0].getKind() == kind::BITVECTOR_NOT && node[0][0] == node[1]) ||
 821            (node[1].getKind() == kind::BITVECTOR_NOT && node[1][0] == node[0])));
 822 }
 823
 824 template<> inline
 825 Node RewriteRule<BitwiseNotAnd>::apply(TNode node) {
 826   Unreachable();
 827   Debug("bv-rewrite") << "RewriteRule<BitwiseNegAnd>(" << node << ")" << std::endl;
 828   return utils::mkZero(utils::getSize(node));
 829 }
 830
 831 /* -------------------------------------------------------------------------- */
 832
 833 /**
 834  * BitwiseNegOr
 835  *
 836  * (a bvor (~ a)) ==> 1
 837  */
 838
 839 template<> inline
 840 bool RewriteRule<BitwiseNotOr>::applies(TNode node) {
 841   Unreachable();
 842   return (node.getKind() == kind::BITVECTOR_OR &&
 843           node.getNumChildren() == 2 &&
 844           ((node[0].getKind() == kind::BITVECTOR_NOT && node[0][0] == node[1]) ||
 845            (node[1].getKind() == kind::BITVECTOR_NOT && node[1][0] == node[0])));
 846 }
 847
 848 template<> inline
 849 Node RewriteRule<BitwiseNotOr>::apply(TNode node) {
 850   Unreachable();
 851   Debug("bv-rewrite") << "RewriteRule<BitwiseNotOr>(" << node << ")" << std::endl;
 852   uint32_t size = utils::getSize(node);
 853   return utils::mkOnes(size);
 854 }
 855
 856 /* -------------------------------------------------------------------------- */
 857
 858 /**
 859  * XorNot
 860  *
 861  * ((~ a) bvxor (~ b)) ==> (a bvxor b)
 862  */
 863
 864 template<> inline
 865 bool RewriteRule<XorNot>::applies(TNode node) {
 866   Unreachable();
 867 }
 868
 869 template <>
 870 inline Node RewriteRule<XorNot>::apply(TNode node)
 871 {
 872   Unreachable();
 873   Debug("bv-rewrite") << "RewriteRule<XorNot>(" << node << ")" << std::endl;
 874   Node a = node[0][0];
 875   Node b = node[1][0];
 876   return NodeManager::currentNM()->mkNode(kind::BITVECTOR_XOR, a, b);
 877 }
 878
 879 /* -------------------------------------------------------------------------- */
 880
 881 /**
 882  * NotXor
 883  *
 884  * ~(a bvxor b) ==> (~ a bvxor b)
 885  */
 886
 887 template<> inline
 888 bool RewriteRule<NotXor>::applies(TNode node) {
 889   return (node.getKind() == kind::BITVECTOR_NOT &&
 890           node[0].getKind() == kind::BITVECTOR_XOR);
 891 }
 892
 893 template <>
 894 inline Node RewriteRule<NotXor>::apply(TNode node)
 895 {
 896   Debug("bv-rewrite") << "RewriteRule<NotXor>(" << node << ")" << std::endl;
 897   std::vector<Node> children;
 898   TNode::iterator child_it = node[0].begin();
 899   children.push_back(
 900       NodeManager::currentNM()->mkNode(kind::BITVECTOR_NOT, *child_it));
 901   for (++child_it; child_it != node[0].end(); ++child_it)
 902   {
 903     children.push_back(*child_it);
 904   }
 905   return utils::mkSortedNode(kind::BITVECTOR_XOR, children);
 906 }
 907
 908 /* -------------------------------------------------------------------------- */
 909
 910 /**
 911  * NotIdemp
 912  *
 913  * ~ (~ a) ==> a
 914  */
 915
 916 template<> inline
 917 bool RewriteRule<NotIdemp>::applies(TNode node) {
 918   return (node.getKind() == kind::BITVECTOR_NOT &&
 919           node[0].getKind() == kind::BITVECTOR_NOT);
 920 }
 921
 922 template<> inline
 923 Node RewriteRule<NotIdemp>::apply(TNode node) {
 924   Debug("bv-rewrite") << "RewriteRule<NotIdemp>(" << node << ")" << std::endl;
 925   return node[0][0];
 926 }
 927
 928 /* -------------------------------------------------------------------------- */
 929
 930 /**
 931  * LtSelf
 932  *
 933  * a < a ==> false
 934  */
 935
 936 template<> inline
 937 bool RewriteRule<LtSelf>::applies(TNode node) {
 938   return ((node.getKind() == kind::BITVECTOR_ULT ||
 939            node.getKind() == kind::BITVECTOR_SLT) &&
 940           node[0] == node[1]);
 941 }
 942
 943 template<> inline
 944 Node RewriteRule<LtSelf>::apply(TNode node) {
 945   Debug("bv-rewrite") << "RewriteRule<LtSelf>(" << node << ")" << std::endl;
 946   return utils::mkFalse();
 947 }
 948
 949 /* -------------------------------------------------------------------------- */
 950
 951 /**
 952  * LteSelf
 953  *
 954  * a <= a ==> true
 955  */
 956
 957 template<> inline
 958 bool RewriteRule<LteSelf>::applies(TNode node) {
 959   return ((node.getKind() == kind::BITVECTOR_ULE ||
 960            node.getKind() == kind::BITVECTOR_SLE) &&
 961           node[0] == node[1]);
 962 }
 963
 964 template<> inline
 965 Node RewriteRule<LteSelf>::apply(TNode node) {
 966   Debug("bv-rewrite") << "RewriteRule<LteSelf>(" << node << ")" << std::endl;
 967   return utils::mkTrue();
 968 }
 969
 970 /* -------------------------------------------------------------------------- */
 971
 972 /**
 973  * ZeroUlt
 974  *
 975  * 0 < a ==> a != 0
 976  */
 977
 978 template <>
 979 inline bool RewriteRule<ZeroUlt>::applies(TNode node)
 980 {
 981   return (node.getKind() == kind::BITVECTOR_ULT
 982           && node[0] == utils::mkZero(utils::getSize(node[0])));
 983 }
 984
 985 template <>
 986 inline Node RewriteRule<ZeroUlt>::apply(TNode node)
 987 {
 988   Debug("bv-rewrite") << "RewriteRule<ZeroUlt>(" << node << ")" << std::endl;
 989   NodeManager *nm = NodeManager::currentNM();
 990   return nm->mkNode(kind::NOT, nm->mkNode(kind::EQUAL, node[0], node[1]));
 991 }
 992
 993 /* -------------------------------------------------------------------------- */
 994
 995 /**
 996  * UltZero
 997  *
 998  * a < 0 ==> false
 999  */
1000
1001 template<> inline
1002 bool RewriteRule<UltZero>::applies(TNode node) {
1003   return (node.getKind() == kind::BITVECTOR_ULT &&
1004           node[1] == utils::mkZero(utils::getSize(node[0])));
1005 }
1006
1007 template<> inline
1008 Node RewriteRule<UltZero>::apply(TNode node) {
1009   Debug("bv-rewrite") << "RewriteRule<UltZero>(" << node << ")" << std::endl;
1010   return utils::mkFalse();
1011 }
1012
1013
1014 /* -------------------------------------------------------------------------- */
1015
1016 /**
1017  *
1018  */
1019 template<> inline
1020 bool RewriteRule<UltOne>::applies(TNode node) {
1021   return (node.getKind() == kind::BITVECTOR_ULT &&
1022           node[1] == utils::mkOne(utils::getSize(node[0])));
1023 }
1024
1025 template <>
1026 inline Node RewriteRule<UltOne>::apply(TNode node)
1027 {
1028   Debug("bv-rewrite") << "RewriteRule<UltOne>(" << node << ")" << std::endl;
1029   return NodeManager::currentNM()->mkNode(
1030       kind::EQUAL, node[0], utils::mkZero(utils::getSize(node[0])));
1031 }
1032
1033 /* -------------------------------------------------------------------------- */
1034
1035 /**
1036  *
1037  */
1038 template<> inline
1039 bool RewriteRule<SltZero>::applies(TNode node) {
1040   return (node.getKind() == kind::BITVECTOR_SLT &&
1041           node[1] == utils::mkZero(utils::getSize(node[0])));
1042 }
1043
1044 template <>
1045 inline Node RewriteRule<SltZero>::apply(TNode node)
1046 {
1047   Debug("bv-rewrite") << "RewriteRule<UltZero>(" << node << ")" << std::endl;
1048   unsigned size = utils::getSize(node[0]);
1049   Node most_significant_bit = utils::mkExtract(node[0], size - 1, size - 1);
1050   return NodeManager::currentNM()->mkNode(
1051       kind::EQUAL, most_significant_bit, utils::mkOne(1));
1052 }
1053
1054 /* -------------------------------------------------------------------------- */
1055
1056 /**
1057  * UltSelf
1058  *
1059  * a < a ==> false
1060  */
1061
1062 template<> inline
1063 bool RewriteRule<UltSelf>::applies(TNode node) {
1064   return (node.getKind() == kind::BITVECTOR_ULT &&
1065           node[1] == node[0]);
1066 }
1067
1068 template<> inline
1069 Node RewriteRule<UltSelf>::apply(TNode node) {
1070   Debug("bv-rewrite") << "RewriteRule<UltSelf>(" << node << ")" << std::endl;
1071   return utils::mkFalse();
1072 }
1073
1074
1075 /* -------------------------------------------------------------------------- */
1076
1077 /**
1078  * UleZero
1079  *
1080  * a <= 0 ==> a = 0
1081  */
1082
1083 template<> inline
1084 bool RewriteRule<UleZero>::applies(TNode node) {
1085   return (node.getKind() == kind::BITVECTOR_ULE &&
1086           node[1] == utils::mkZero(utils::getSize(node[0])));
1087 }
1088
1089 template <>
1090 inline Node RewriteRule<UleZero>::apply(TNode node)
1091 {
1092   Debug("bv-rewrite") << "RewriteRule<UleZero>(" << node << ")" << std::endl;
1093   return NodeManager::currentNM()->mkNode(kind::EQUAL, node[0], node[1]);
1094 }
1095
1096 /* -------------------------------------------------------------------------- */
1097
1098 /**
1099  * UleSelf
1100  *
1101  * a <= a ==> true
1102  */
1103
1104 template<> inline
1105 bool RewriteRule<UleSelf>::applies(TNode node) {
1106   return (node.getKind() == kind::BITVECTOR_ULE &&
1107           node[1] == node[0]);
1108 }
1109
1110 template<> inline
1111 Node RewriteRule<UleSelf>::apply(TNode node) {
1112   Debug("bv-rewrite") << "RewriteRule<UleSelf>(" << node << ")" << std::endl;
1113   return utils::mkTrue();
1114 }
1115
1116 /* -------------------------------------------------------------------------- */
1117
1118 /**
1119  * ZeroUle
1120  *
1121  * 0 <= a ==> true
1122  */
1123
1124 template<> inline
1125 bool RewriteRule<ZeroUle>::applies(TNode node) {
1126   return (node.getKind() == kind::BITVECTOR_ULE &&
1127           node[0] == utils::mkZero(utils::getSize(node[0])));
1128 }
1129
1130 template<> inline
1131 Node RewriteRule<ZeroUle>::apply(TNode node) {
1132   Debug("bv-rewrite") << "RewriteRule<ZeroUle>(" << node << ")" << std::endl;
1133   return utils::mkTrue();
1134 }
1135
1136 /* -------------------------------------------------------------------------- */
1137
1138 /**
1139  * UleMax
1140  *
1141  * a <= 11..1 ==> true
1142  */
1143
1144 template<> inline
1145 bool RewriteRule<UleMax>::applies(TNode node) {
1146   if (node.getKind()!= kind::BITVECTOR_ULE) {
1147     return false;
1148   }
1149   uint32_t size = utils::getSize(node[0]);
1150   return (node.getKind() == kind::BITVECTOR_ULE
1151           && node[1] == utils::mkOnes(size));
1152 }
1153
1154 template<> inline
1155 Node RewriteRule<UleMax>::apply(TNode node) {
1156   Debug("bv-rewrite") << "RewriteRule<UleMax>(" << node << ")" << std::endl;
1157   return utils::mkTrue();
1158 }
1159
1160 /* -------------------------------------------------------------------------- */
1161
1162 /**
1163  * NotUlt
1164  *
1165  * ~ ( a < b) ==> b <= a
1166  */
1167
1168 template<> inline
1169 bool RewriteRule<NotUlt>::applies(TNode node) {
1170   return (node.getKind() == kind::NOT &&
1171           node[0].getKind() == kind::BITVECTOR_ULT);
1172 }
1173
1174 template <>
1175 inline Node RewriteRule<NotUlt>::apply(TNode node)
1176 {
1177   Debug("bv-rewrite") << "RewriteRule<NotUlt>(" << node << ")" << std::endl;
1178   Node ult = node[0];
1179   Node a = ult[0];
1180   Node b = ult[1];
1181   return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULE, b, a);
1182 }
1183
1184 /* -------------------------------------------------------------------------- */
1185
1186 /**
1187  * NotUle
1188  *
1189  * ~ ( a <= b) ==> b < a
1190  */
1191
1192 template<> inline
1193 bool RewriteRule<NotUle>::applies(TNode node) {
1194   return (node.getKind() == kind::NOT &&
1195           node[0].getKind() == kind::BITVECTOR_ULE);
1196 }
1197
1198 template <>
1199 inline Node RewriteRule<NotUle>::apply(TNode node)
1200 {
1201   Debug("bv-rewrite") << "RewriteRule<NotUle>(" << node << ")" << std::endl;
1202   Node ult = node[0];
1203   Node a = ult[0];
1204   Node b = ult[1];
1205   return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, b, a);
1206 }
1207
1208 /* -------------------------------------------------------------------------- */
1209
1210 /**
1211  * MultPow2
1212  *
1213  * (a * 2^k) ==> a[n-k-1:0] 0_k
1214  */
1215
1216 template <>
1217 inline bool RewriteRule<MultPow2>::applies(TNode node)
1218 {
1219   if (node.getKind() != kind::BITVECTOR_MULT)
1220     return false;
1221
1222   for (const Node& cn : node)
1223   {
1224     bool cIsNeg = false;
1225     if (utils::isPow2Const(cn, cIsNeg))
1226     {
1227       return true;
1228     }
1229   }
1230   return false;
1231 }
1232
1233 template <>
1234 inline Node RewriteRule<MultPow2>::apply(TNode node)
1235 {
1236   Debug("bv-rewrite") << "RewriteRule<MultPow2>(" << node << ")" << std::endl;
1237   NodeManager *nm = NodeManager::currentNM();
1238   unsigned size = utils::getSize(node);
1239   std::vector<Node>  children;
1240   unsigned exponent = 0;
1241   bool isNeg = false;
1242   for (const Node& cn : node)
1243   {
1244     bool cIsNeg = false;
1245     unsigned exp = utils::isPow2Const(cn, cIsNeg);
1246     if (exp) {
1247       exponent += exp - 1;
1248       if (cIsNeg)
1249       {
1250         isNeg = !isNeg;
1251       }
1252     }
1253     else {
1254       children.push_back(cn);
1255     }
1256   }
1257   if (exponent >= size)
1258   {
1259     return utils::mkZero(size);
1260   }
1261
1262   Node a;
1263   if (children.empty())
1264   {
1265     a = utils::mkOne(size);
1266   }
1267   else
1268   {
1269     a = utils::mkNaryNode(kind::BITVECTOR_MULT, children);
1270   }
1271
1272   if (isNeg && size > 1)
1273   {
1274     a = nm->mkNode(kind::BITVECTOR_NEG, a);
1275   }
1276   if (exponent == 0)
1277   {
1278     return a;
1279   }
1280   Node extract = utils::mkExtract(a, size - exponent - 1, 0);
1281   Node zeros = utils::mkConst(exponent, 0);
1282   return utils::mkConcat(extract, zeros);
1283 }
1284
1285 /* -------------------------------------------------------------------------- */
1286
1287 /**
1288  * ExtractMultLeadingBit
1289  *
1290  * If the bit-vectors multiplied have enough leading zeros,
1291  * we can determine that the top bits of the multiplication
1292  * are zero and not compute them. Only apply for large bitwidths
1293  * as this can interfere with other mult normalization rewrites such
1294  * as flattening.
1295  */
1296
1297 template<> inline
1298 bool RewriteRule<ExtractMultLeadingBit>::applies(TNode node) {
1299   if (node.getKind() != kind::BITVECTOR_EXTRACT)
1300     return false;
1301   unsigned low = utils::getExtractLow(node);
1302   node = node[0];
1303
1304   if (node.getKind() != kind::BITVECTOR_MULT ||
1305       node.getNumChildren() != 2 ||
1306       utils::getSize(node) <= 64)
1307     return false;
1308
1309   if (node[0].getKind() != kind::BITVECTOR_CONCAT ||
1310       node[1].getKind() != kind::BITVECTOR_CONCAT ||
1311       !node[0][0].isConst() ||
1312       !node[1][0].isConst())
1313     return false;
1314
1315   unsigned n = utils::getSize(node);
1316   // count number of leading zeroes
1317   const Integer& int1 = node[0][0].getConst<BitVector>().toInteger();
1318   const Integer& int2 = node[1][0].getConst<BitVector>().toInteger();
1319   size_t int1_size = utils::getSize(node[0][0]);
1320   size_t int2_size = utils::getSize(node[1][0]);
1321   unsigned zeroes1 = int1.isZero() ? int1_size : int1_size - int1.length();
1322   unsigned zeroes2 = int2.isZero() ? int2_size : int2_size - int2.length();
1323
1324   // first k bits are not zero in the result
1325   unsigned k = 2 * n - (zeroes1 + zeroes2);
1326
1327   if (k > low)
1328     return false;
1329
1330   return true;
1331 }
1332
1333 template<> inline
1334 Node RewriteRule<ExtractMultLeadingBit>::apply(TNode node) {
1335   Debug("bv-rewrite") << "RewriteRule<MultLeadingBit>(" << node << ")" << std::endl;
1336
1337   unsigned bitwidth = utils::getSize(node);
1338
1339   // node = node[0];
1340   // const Integer& int1 = node[0][0].getConst<BitVector>().toInteger();
1341   // const Integer& int2 = node[1][0].getConst<BitVector>().toInteger();
1342   // unsigned zeroes1 = int1.isZero()? utils::getSize(node[0][0]) :
1343   //                                   int1.length();
1344
1345   // unsigned zeroes2 = int2.isZero()? utils::getSize(node[1][0]) :
1346   //                                   int2.length();
1347   // all bits >= k in the multiplier will have to be 0
1348   // unsigned n = utils::getSize(node);
1349   // unsigned k = 2 * n - (zeroes1 + zeroes2);
1350   // Node extract1 = utils::mkExtract(node[0], k - 1, 0);
1351   // Node extract2 = utils::mkExtract(node[1], k - 1, 0);
1352   // Node k_zeroes = utils::mkConst(n - k, 0u);
1353
1354   // NodeManager *nm = NodeManager::currentNM();
1355   // Node new_mult = nm->mkNode(kind::BITVECTOR_MULT, extract1, extract2);
1356   // Node result = utils::mkExtract(nm->mkNode(kind::BITVECTOR_CONCAT, k_zeroes, new_mult), high, low);
1357
1358   // since the extract is over multiplier bits that have to be 0, return 0
1359   Node result = utils::mkConst(bitwidth, 0u);
1360   //  std::cout << "MultLeadingBit " << node <<" => " << result <<"\n";
1361   return result;
1362 }
1363
1364 /* -------------------------------------------------------------------------- */
1365
1366 /**
1367  * NegIdemp
1368  *
1369  * -(-a) ==> a
1370  */
1371
1372 template<> inline
1373 bool RewriteRule<NegIdemp>::applies(TNode node) {
1374   return (node.getKind() == kind::BITVECTOR_NEG &&
1375           node[0].getKind() == kind::BITVECTOR_NEG);
1376 }
1377
1378 template<> inline
1379 Node RewriteRule<NegIdemp>::apply(TNode node) {
1380   Debug("bv-rewrite") << "RewriteRule<NegIdemp>(" << node << ")" << std::endl;
1381   return node[0][0];
1382 }
1383
1384 /* -------------------------------------------------------------------------- */
1385
1386 /**
1387  * UdivPow2
1388  *
1389  * (a udiv 2^k) ==> 0_k a[n-1: k]
1390  */
1391
1392 template <>
1393 inline bool RewriteRule<UdivPow2>::applies(TNode node)
1394 {
1395   bool isNeg = false;
1396   if (node.getKind() == kind::BITVECTOR_UDIV_TOTAL
1397       && utils::isPow2Const(node[1], isNeg))
1398   {
1399     return !isNeg;
1400   }
1401   return false;
1402 }
1403
1404 template <>
1405 inline Node RewriteRule<UdivPow2>::apply(TNode node)
1406 {
1407   Debug("bv-rewrite") << "RewriteRule<UdivPow2>(" << node << ")" << std::endl;
1408   NodeManager *nm = NodeManager::currentNM();
1409   unsigned size = utils::getSize(node);
1410   Node a = node[0];
1411   bool isNeg = false;
1412   unsigned power = utils::isPow2Const(node[1], isNeg) - 1;
1413   Node ret;
1414   if (power == 0)
1415   {
1416     ret = a;
1417   }
1418   else
1419   {
1420     Node extract = utils::mkExtract(a, size - 1, power);
1421     Node zeros = utils::mkConst(power, 0);
1422
1423     ret = nm->mkNode(kind::BITVECTOR_CONCAT, zeros, extract);
1424   }
1425   if (isNeg && size > 1)
1426   {
1427     ret = nm->mkNode(kind::BITVECTOR_NEG, ret);
1428   }
1429   return ret;
1430 }
1431
1432 /* -------------------------------------------------------------------------- */
1433
1434 /**
1435  * UdivZero
1436  *
1437  * (a udiv 0) ==> 111...1
1438  */
1439
1440 template <>
1441 inline bool RewriteRule<UdivZero>::applies(TNode node) {
1442   return (node.getKind() == kind::BITVECTOR_UDIV_TOTAL &&
1443           node[1] == utils::mkConst(utils::getSize(node), 0));
1444 }
1445
1446 template <>
1447 inline Node RewriteRule<UdivZero>::apply(TNode node) {
1448   Debug("bv-rewrite") << "RewriteRule<UdivZero>(" << node << ")" << std::endl;
1449   return utils::mkOnes(utils::getSize(node));
1450 }
1451
1452 /* -------------------------------------------------------------------------- */
1453
1454 /**
1455  * UdivOne
1456  *
1457  * (a udiv 1) ==> a
1458  */
1459
1460 template <>
1461 inline bool RewriteRule<UdivOne>::applies(TNode node) {
1462   return (node.getKind() == kind::BITVECTOR_UDIV_TOTAL &&
1463           node[1] == utils::mkConst(utils::getSize(node), 1));
1464 }
1465
1466 template <>
1467 inline Node RewriteRule<UdivOne>::apply(TNode node) {
1468   Debug("bv-rewrite") << "RewriteRule<UdivOne>(" << node << ")" << std::endl;
1469   return node[0];
1470 }
1471
1472 /* -------------------------------------------------------------------------- */
1473
1474 /**
1475  * UremPow2
1476  *
1477  * (a urem 2^k) ==> 0_(n-k) a[k-1:0]
1478  */
1479
1480 template <>
1481 inline bool RewriteRule<UremPow2>::applies(TNode node)
1482 {
1483   bool isNeg;
1484   if (node.getKind() == kind::BITVECTOR_UREM_TOTAL
1485       && utils::isPow2Const(node[1], isNeg))
1486   {
1487     return !isNeg;
1488   }
1489   return false;
1490 }
1491
1492 template <>
1493 inline Node RewriteRule<UremPow2>::apply(TNode node)
1494 {
1495   Debug("bv-rewrite") << "RewriteRule<UremPow2>(" << node << ")" << std::endl;
1496   TNode a = node[0];
1497   bool isNeg = false;
1498   unsigned power = utils::isPow2Const(node[1], isNeg) - 1;
1499   Node ret;
1500   if (power == 0)
1501   {
1502     ret = utils::mkZero(utils::getSize(node));
1503   }
1504   else
1505   {
1506     Node extract = utils::mkExtract(a, power - 1, 0);
1507     Node zeros = utils::mkZero(utils::getSize(node) - power);
1508     ret = NodeManager::currentNM()->mkNode(
1509         kind::BITVECTOR_CONCAT, zeros, extract);
1510   }
1511   return ret;
1512 }
1513
1514 /* -------------------------------------------------------------------------- */
1515
1516 /**
1517  * UremOne
1518  *
1519  * (a urem 1) ==> 0
1520  */
1521
1522 template<> inline
1523 bool RewriteRule<UremOne>::applies(TNode node) {
1524   return (node.getKind() == kind::BITVECTOR_UREM_TOTAL &&
1525           node[1] == utils::mkConst(utils::getSize(node), 1));
1526 }
1527
1528 template<> inline
1529 Node RewriteRule<UremOne>::apply(TNode node) {
1530   Debug("bv-rewrite") << "RewriteRule<UremOne>(" << node << ")" << std::endl;
1531   return utils::mkConst(utils::getSize(node), 0);
1532 }
1533
1534 /* -------------------------------------------------------------------------- */
1535
1536 /**
1537  * UremSelf
1538  *
1539  * (a urem a) ==> 0
1540  */
1541
1542 template<> inline
1543 bool RewriteRule<UremSelf>::applies(TNode node) {
1544   return (node.getKind() == kind::BITVECTOR_UREM_TOTAL &&
1545           node[0] == node[1]);
1546 }
1547
1548 template<> inline
1549 Node RewriteRule<UremSelf>::apply(TNode node) {
1550   Debug("bv-rewrite") << "RewriteRule<UremSelf>(" << node << ")" << std::endl;
1551   return utils::mkConst(utils::getSize(node), 0);
1552 }
1553
1554 /* -------------------------------------------------------------------------- */
1555
1556 /**
1557  * ShiftZero
1558  *
1559  * (0_k >> a) ==> 0_k
1560  */
1561
1562 template<> inline
1563 bool RewriteRule<ShiftZero>::applies(TNode node) {
1564   return ((node.getKind() == kind::BITVECTOR_SHL ||
1565            node.getKind() == kind::BITVECTOR_LSHR ||
1566            node.getKind() == kind::BITVECTOR_ASHR) &&
1567           node[0] == utils::mkConst(utils::getSize(node), 0));
1568 }
1569
1570 template<> inline
1571 Node RewriteRule<ShiftZero>::apply(TNode node) {
1572   Debug("bv-rewrite") << "RewriteRule<ShiftZero>(" << node << ")" << std::endl;
1573   return node[0];
1574 }
1575
1576 /* -------------------------------------------------------------------------- */
1577
1578 /**
1579  * UgtUrem
1580  *
1581  * (bvugt (bvurem T x) x)
1582  *   ==>  (ite (= x 0_k) (bvugt T x) false)
1583  *   ==>  (and (=> (= x 0_k) (bvugt T x)) (=> (not (= x 0_k)) false))
1584  *   ==>  (and (=> (= x 0_k) (bvugt T x)) (= x 0_k))
1585  *   ==>  (and (bvugt T x) (= x 0_k))
1586  *   ==>  (and (bvugt T 0_k) (= x 0_k))
1587  */
1588
1589 template <>
1590 inline bool RewriteRule<UgtUrem>::applies(TNode node)
1591 {
1592   return (node.getKind() == kind::BITVECTOR_UGT
1593           && node[0].getKind() == kind::BITVECTOR_UREM_TOTAL
1594           && node[0][1] == node[1]);
1595 }
1596
1597 template <>
1598 inline Node RewriteRule<UgtUrem>::apply(TNode node)
1599 {
1600   Debug("bv-rewrite") << "RewriteRule<UgtUrem>(" << node << ")" << std::endl;
1601   const Node& T = node[0][0];
1602   const Node& x = node[1];
1603   Node zero = utils::mkConst(utils::getSize(x), 0);
1604   NodeManager* nm = NodeManager::currentNM();
1605   return nm->mkNode(kind::AND,
1606                     nm->mkNode(kind::EQUAL, x, zero),
1607                     nm->mkNode(kind::BITVECTOR_UGT, T, zero));
1608 }
1609
1610 /* -------------------------------------------------------------------------- */
1611
1612 /**
1613  * BBPlusNeg
1614  *
1615  * -a1 - a2 - ... - an + ak + ..  ==> - (a1 + a2 + ... + an) + ak
1616  *
1617  */
1618
1619 template<> inline
1620 bool RewriteRule<BBPlusNeg>::applies(TNode node) {
1621   if (node.getKind() != kind::BITVECTOR_PLUS) {
1622     return false;
1623   }
1624
1625   unsigned neg_count = 0;
1626   for(unsigned i = 0; i < node.getNumChildren(); ++i) {
1627     if (node[i].getKind()== kind::BITVECTOR_NEG) {
1628       ++neg_count;
1629     }
1630   }
1631   return neg_count > 1;
1632 }
1633
1634 template <>
1635 inline Node RewriteRule<BBPlusNeg>::apply(TNode node)
1636 {
1637   Debug("bv-rewrite") << "RewriteRule<BBPlusNeg>(" << node << ")" << std::endl;
1638   NodeManager *nm = NodeManager::currentNM();
1639   std::vector<Node> children;
1640   unsigned neg_count = 0;
1641   for (unsigned i = 0; i < node.getNumChildren(); ++i)
1642   {
1643     if (node[i].getKind() == kind::BITVECTOR_NEG)
1644     {
1645       ++neg_count;
1646       children.push_back(nm->mkNode(kind::BITVECTOR_NOT, node[i][0]));
1647     }
1648     else
1649     {
1650       children.push_back(node[i]);
1651     }
1652   }
1653   Assert(neg_count != 0);
1654   children.push_back(utils::mkConst(utils::getSize(node), neg_count));
1655
1656   return utils::mkNaryNode(kind::BITVECTOR_PLUS, children);
1657 }
1658
1659 /* -------------------------------------------------------------------------- */
1660
1661 template<> inline
1662 bool RewriteRule<MergeSignExtend>::applies(TNode node) {
1663   if (node.getKind() != kind::BITVECTOR_SIGN_EXTEND ||
1664       (node[0].getKind() != kind::BITVECTOR_SIGN_EXTEND &&
1665        node[0].getKind() != kind::BITVECTOR_ZERO_EXTEND))
1666     return false;
1667   return true;
1668 }
1669
1670 template<> inline
1671 Node RewriteRule<MergeSignExtend>::apply(TNode node) {
1672   Debug("bv-rewrite") << "RewriteRule<MergeSignExtend>(" << node << ")" << std::endl;
1673   unsigned amount1 =
1674       node.getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount;
1675
1676   NodeManager* nm = NodeManager::currentNM();
1677   if (node[0].getKind() == kind::BITVECTOR_ZERO_EXTEND) {
1678     unsigned amount2 = node[0]
1679                            .getOperator()
1680                            .getConst<BitVectorZeroExtend>()
1681                            .d_zeroExtendAmount;
1682     if (amount2 == 0)
1683     {
1684       NodeBuilder<> nb(kind::BITVECTOR_SIGN_EXTEND);
1685       Node op = nm->mkConst<BitVectorSignExtend>(BitVectorSignExtend(amount1));
1686       nb << op << node[0][0];
1687       Node res = nb;
1688       return res;
1689     }
1690     NodeBuilder<> nb(kind::BITVECTOR_ZERO_EXTEND);
1691     Node op = nm->mkConst<BitVectorZeroExtend>(
1692         BitVectorZeroExtend(amount1 + amount2));
1693     nb << op << node[0][0];
1694     Node res = nb;
1695     return res;
1696   }
1697   Assert(node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND);
1698   unsigned amount2 =
1699       node[0].getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount;
1700   return utils::mkSignExtend(node[0][0], amount1 + amount2);
1701 }
1702
1703 /* -------------------------------------------------------------------------- */
1704
1705 /**
1706  * ZeroExtendEqConst
1707  *
1708  * Rewrite zero_extend(x^n, m) = c^n+m to
1709  *
1710  *   false         if c[n+m-1:n] != 0
1711  *   x = c[n-1:0]  otherwise.
1712  */
1713 template <>
1714 inline bool RewriteRule<ZeroExtendEqConst>::applies(TNode node) {
1715   return node.getKind() == kind::EQUAL &&
1716          ((node[0].getKind() == kind::BITVECTOR_ZERO_EXTEND &&
1717            node[1].isConst()) ||
1718           (node[1].getKind() == kind::BITVECTOR_ZERO_EXTEND &&
1719            node[0].isConst()));
1720 }
1721
1722 template <>
1723 inline Node RewriteRule<ZeroExtendEqConst>::apply(TNode node) {
1724   TNode t, c;
1725   if (node[0].getKind() == kind::BITVECTOR_ZERO_EXTEND) {
1726     t = node[0][0];
1727     c = node[1];
1728   } else {
1729     t = node[1][0];
1730     c = node[0];
1731   }
1732   BitVector c_hi =
1733       c.getConst<BitVector>().extract(utils::getSize(c) - 1, utils::getSize(t));
1734   BitVector c_lo = c.getConst<BitVector>().extract(utils::getSize(t) - 1, 0);
1735   BitVector zero = BitVector(c_hi.getSize(), Integer(0));
1736
1737   if (c_hi == zero) {
1738     return NodeManager::currentNM()->mkNode(kind::EQUAL, t,
1739                                             utils::mkConst(c_lo));
1740   }
1741   return utils::mkFalse();
1742 }
1743
1744 /* -------------------------------------------------------------------------- */
1745
1746 /**
1747  * SignExtendEqConst
1748  *
1749  * Rewrite sign_extend(x^n, m) = c^n+m to
1750  *
1751  *   x = c[n-1:0]   if (c[n-1:n-1] == 0 && c[n+m-1:n] == 0) ||
1752  *                     (c[n-1:n-1] == 1 && c[n+m-1:n] == ~0)
1753  *   false          otherwise.
1754  */
1755 template <>
1756 inline bool RewriteRule<SignExtendEqConst>::applies(TNode node) {
1757   return node.getKind() == kind::EQUAL &&
1758          ((node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND &&
1759            node[1].isConst()) ||
1760           (node[1].getKind() == kind::BITVECTOR_SIGN_EXTEND &&
1761            node[0].isConst()));
1762 }
1763
1764 template <>
1765 inline Node RewriteRule<SignExtendEqConst>::apply(TNode node) {
1766   TNode t, c;
1767   if (node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND) {
1768     t = node[0][0];
1769     c = node[1];
1770   } else {
1771     t = node[1][0];
1772     c = node[0];
1773   }
1774   unsigned pos_msb_t = utils::getSize(t) - 1;
1775   BitVector c_hi =
1776       c.getConst<BitVector>().extract(utils::getSize(c) - 1, pos_msb_t);
1777   BitVector c_lo = c.getConst<BitVector>().extract(pos_msb_t, 0);
1778   BitVector zero = BitVector(c_hi.getSize(), Integer(0));
1779
1780   if (c_hi == zero || c_hi == ~zero) {
1781     return NodeManager::currentNM()->mkNode(kind::EQUAL, t,
1782                                             utils::mkConst(c_lo));
1783   }
1784   return utils::mkFalse();
1785 }
1786
1787 /* -------------------------------------------------------------------------- */
1788
1789 /**
1790  * ZeroExtendUltConst
1791  *
1792  * Rewrite zero_extend(x^n,m) < c^n+m to
1793  *
1794  *   x < c[n-1:0]   if c[n+m-1:n] == 0.
1795  *
1796  * Rewrite c^n+m < Rewrite zero_extend(x^n,m) to
1797  *
1798  *   c[n-1:0] < x   if c[n+m-1:n] == 0.
1799  */
1800 template <>
1801 inline bool RewriteRule<ZeroExtendUltConst>::applies(TNode node) {
1802   if (node.getKind() == kind::BITVECTOR_ULT &&
1803       ((node[0].getKind() == kind::BITVECTOR_ZERO_EXTEND &&
1804         node[1].isConst()) ||
1805        (node[1].getKind() == kind::BITVECTOR_ZERO_EXTEND &&
1806         node[0].isConst()))) {
1807     TNode t, c;
1808     bool is_lhs = node[0].getKind() == kind::BITVECTOR_ZERO_EXTEND;
1809     if (is_lhs) {
1810       t = node[0][0];
1811       c = node[1];
1812     } else {
1813       t = node[1][0];
1814       c = node[0];
1815     }
1816
1817     if (utils::getSize(t) == utils::getSize(c))
1818     {
1819       return false;
1820     }
1821
1822     BitVector bv_c = c.getConst<BitVector>();
1823     BitVector c_hi = c.getConst<BitVector>().extract(utils::getSize(c) - 1,
1824                                                      utils::getSize(t));
1825     BitVector zero = BitVector(c_hi.getSize(), Integer(0));
1826
1827     return c_hi == zero;
1828   }
1829   return false;
1830 }
1831
1832 template <>
1833 inline Node RewriteRule<ZeroExtendUltConst>::apply(TNode node) {
1834   TNode t, c;
1835   bool is_lhs = node[0].getKind() == kind::BITVECTOR_ZERO_EXTEND;
1836   if (is_lhs) {
1837     t = node[0][0];
1838     c = node[1];
1839   } else {
1840     t = node[1][0];
1841     c = node[0];
1842   }
1843   Node c_lo =
1844       utils::mkConst(c.getConst<BitVector>().extract(utils::getSize(t) - 1, 0));
1845
1846   if (is_lhs) {
1847     return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, t, c_lo);
1848   }
1849   return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, c_lo, t);
1850 }
1851
1852 /* -------------------------------------------------------------------------- */
1853
1854 /**
1855  * SignExtendUltConst
1856  *
1857  * Rewrite sign_extend(x^n,m) < c^n+m to
1858  *
1859  *   x < c[n-1:0]   if (c <= (1 << (n - 1))) || (c >= (~0 << (n - 1)))
1860  *   x[n-1:n-1] = 0 if (1 << (n - 1)) < c <= (~0 << (n - 1)).
1861  *
1862  * Rewrite c^n+m < sign_extend(x^n,m) to
1863  *
1864  *   c[n-1:0] < x   if (c < (1 << (n - 1))) || (c >= ~(1 << (n-1)))
1865  *   x[n-1:n-1] = 1 if ~(~0 << (n-1)) <= c <= ~(1 << (n-1))
1866  *
1867  * where ~(~0 << (n - 1)) == (1 << (n - 1)) - 1
1868  *
1869  */
1870 template <>
1871 inline bool RewriteRule<SignExtendUltConst>::applies(TNode node)
1872 {
1873   if (node.getKind() == kind::BITVECTOR_ULT
1874       && ((node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND
1875            && node[1].isConst())
1876           || (node[1].getKind() == kind::BITVECTOR_SIGN_EXTEND
1877               && node[0].isConst())))
1878   {
1879     TNode x, c;
1880     bool is_lhs = node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND;
1881     if (is_lhs)
1882     {
1883       x = node[0][0];
1884       c = node[1];
1885     }
1886     else
1887     {
1888       x = node[1][0];
1889       c = node[0];
1890     }
1891     BitVector bv_c = c.getConst<BitVector>();
1892     unsigned size_c = utils::getSize(c);
1893     unsigned msb_x_pos = utils::getSize(x) - 1;
1894     // (1 << (n - 1)))
1895     BitVector bv_msb_x = BitVector(size_c).setBit(msb_x_pos, true);
1896     // (~0 << (n - 1))
1897     BitVector bv_upper_bits =
1898         (~BitVector(size_c)).leftShift(BitVector(size_c, msb_x_pos));
1899
1900     return (is_lhs
1901             && (bv_c <= bv_msb_x || bv_c >= bv_upper_bits
1902                 || (bv_msb_x < bv_c && bv_c <= bv_upper_bits)))
1903            || (!is_lhs
1904                && (bv_c < bv_msb_x || bv_c >= ~bv_msb_x
1905                    || (~bv_upper_bits <= bv_c && bv_c <= ~bv_msb_x)));
1906   }
1907   return false;
1908 }
1909
1910 template <>
1911 inline Node RewriteRule<SignExtendUltConst>::apply(TNode node)
1912 {
1913   TNode x, c;
1914   bool is_lhs = node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND;
1915   if (is_lhs)
1916   {
1917     x = node[0][0];
1918     c = node[1];
1919   }
1920   else
1921   {
1922     x = node[1][0];
1923     c = node[0];
1924   }
1925   BitVector bv_c = c.getConst<BitVector>();
1926
1927   unsigned size_c = utils::getSize(c);
1928   unsigned msb_x_pos = utils::getSize(x) - 1;
1929   Node c_lo = utils::mkConst(bv_c.extract(msb_x_pos, 0));
1930   // (1 << (n - 1)))
1931   BitVector bv_msb_x = BitVector(size_c).setBit(msb_x_pos, true);
1932   // (~0 << (n - 1))
1933   BitVector bv_upper_bits =
1934       (~BitVector(size_c)).leftShift(BitVector(size_c, msb_x_pos));
1935
1936   NodeManager* nm = NodeManager::currentNM();
1937   if (is_lhs)
1938   {
1939     // x[n-1:n-1] = 0
1940     if (bv_msb_x < bv_c && bv_c <= bv_upper_bits)
1941     {
1942       Node msb_x = utils::mkExtract(x, msb_x_pos, msb_x_pos);
1943       return nm->mkNode(kind::EQUAL, msb_x, utils::mkZero(1));
1944     }
1945     // x < c[n-1:0]
1946     Assert(bv_c <= bv_msb_x || bv_c >= bv_upper_bits);
1947     return nm->mkNode(kind::BITVECTOR_ULT, x, c_lo);
1948   }
1949
1950   // x[n-1:n-1] = 1
1951   if (~bv_upper_bits <= bv_c && bv_c <= ~bv_msb_x)
1952   {
1953     Node msb_x = utils::mkExtract(x, msb_x_pos, msb_x_pos);
1954     return nm->mkNode(kind::EQUAL, msb_x, utils::mkOne(1));
1955   }
1956   // c[n-1:0] < x
1957   Assert(bv_c < bv_msb_x || bv_c >= ~bv_msb_x);
1958   return nm->mkNode(kind::BITVECTOR_ULT, c_lo, x);
1959 }
1960
1961 /* -------------------------------------------------------------------------- */
1962
1963 template<> inline
1964 bool RewriteRule<MultSlice>::applies(TNode node) {
1965   if (node.getKind() != kind::BITVECTOR_MULT || node.getNumChildren() != 2) {
1966     return false;
1967   }
1968   return utils::getSize(node[0]) % 2 == 0;
1969 }
1970
1971 /**
1972  * Expressses the multiplication in terms of the top and bottom
1973  * slices of the terms. Note increases circuit size, but could
1974  * lead to simplifications (use wisely!).
1975  *
1976  * @param node
1977  *
1978  * @return
1979  */
1980 template <>
1981 inline Node RewriteRule<MultSlice>::apply(TNode node)
1982 {
1983   Debug("bv-rewrite") << "RewriteRule<MultSlice>(" << node << ")" << std::endl;
1984   NodeManager *nm = NodeManager::currentNM();
1985   unsigned bitwidth = utils::getSize(node[0]);
1986   Node zeros = utils::mkConst(bitwidth / 2, 0);
1987   TNode a = node[0];
1988   Node bottom_a = utils::mkExtract(a, bitwidth / 2 - 1, 0);
1989   Node top_a = utils::mkExtract(a, bitwidth - 1, bitwidth / 2);
1990   TNode b = node[1];
1991   Node bottom_b = utils::mkExtract(b, bitwidth / 2 - 1, 0);
1992   Node top_b = utils::mkExtract(b, bitwidth - 1, bitwidth / 2);
1993
1994   Node term1 = nm->mkNode(kind::BITVECTOR_MULT,
1995                           nm->mkNode(kind::BITVECTOR_CONCAT, zeros, bottom_a),
1996                           nm->mkNode(kind::BITVECTOR_CONCAT, zeros, bottom_b));
1997
1998   Node term2 = nm->mkNode(kind::BITVECTOR_CONCAT,
1999                           nm->mkNode(kind::BITVECTOR_MULT, top_b, bottom_a),
2000                           zeros);
2001   Node term3 = nm->mkNode(kind::BITVECTOR_CONCAT,
2002                           nm->mkNode(kind::BITVECTOR_MULT, top_a, bottom_b),
2003                           zeros);
2004   return nm->mkNode(kind::BITVECTOR_PLUS, term1, term2, term3);
2005 }
2006
2007 /* -------------------------------------------------------------------------- */
2008
2009 /**
2010  * x < y + 1 <=> (not y < x) and y != 1...1
2011  *
2012  * @param node
2013  *
2014  * @return
2015  */
2016 template<> inline
2017 bool RewriteRule<UltPlusOne>::applies(TNode node) {
2018   if (node.getKind() != kind::BITVECTOR_ULT) return false;
2019   TNode x = node[0];
2020   TNode y1 = node[1];
2021   if (y1.getKind() != kind::BITVECTOR_PLUS) return false;
2022   if (y1[0].getKind() != kind::CONST_BITVECTOR &&
2023       y1[1].getKind() != kind::CONST_BITVECTOR)
2024     return false;
2025
2026   if (y1[0].getKind() == kind::CONST_BITVECTOR &&
2027       y1[1].getKind() == kind::CONST_BITVECTOR)
2028     return false;
2029
2030   if (y1.getNumChildren() != 2)
2031     return false;
2032
2033   TNode one = y1[0].getKind() == kind::CONST_BITVECTOR ? y1[0] : y1[1];
2034   if (one != utils::mkConst(utils::getSize(one), 1)) return false;
2035   return true;
2036 }
2037
2038 template <>
2039 inline Node RewriteRule<UltPlusOne>::apply(TNode node)
2040 {
2041   Debug("bv-rewrite") << "RewriteRule<UltPlusOne>(" << node << ")" << std::endl;
2042   NodeManager *nm = NodeManager::currentNM();
2043   TNode x = node[0];
2044   TNode y1 = node[1];
2045   TNode y = y1[0].getKind() != kind::CONST_BITVECTOR ? y1[0] : y1[1];
2046   unsigned size = utils::getSize(x);
2047   Node not_y_eq_1 =
2048       nm->mkNode(kind::NOT, nm->mkNode(kind::EQUAL, y, utils::mkOnes(size)));
2049   Node not_y_lt_x =
2050       nm->mkNode(kind::NOT, nm->mkNode(kind::BITVECTOR_ULT, y, x));
2051   return nm->mkNode(kind::AND, not_y_eq_1, not_y_lt_x);
2052 }
2053
2054 /* -------------------------------------------------------------------------- */
2055
2056 /**
2057  * x ^(x-1) = 0 => 1 << sk
2058  * WARNING: this is an **EQUISATISFIABLE** transformation!
2059  * Only to be called on top level assertions.
2060  *
2061  * @param node
2062  *
2063  * @return
2064  */
2065 template<> inline
2066 bool RewriteRule<IsPowerOfTwo>::applies(TNode node) {
2067   if (node.getKind()!= kind::EQUAL) return false;
2068   if (node[0].getKind() != kind::BITVECTOR_AND &&
2069       node[1].getKind() != kind::BITVECTOR_AND)
2070     return false;
2071   if (!utils::isZero(node[0]) &&
2072       !utils::isZero(node[1]))
2073     return false;
2074
2075   TNode t = !utils::isZero(node[0])? node[0]: node[1];
2076   if (t.getNumChildren() != 2) return false;
2077   TNode a = t[0];
2078   TNode b = t[1];
2079   unsigned size = utils::getSize(t);
2080   if(size < 2) return false;
2081   Node diff = Rewriter::rewrite(
2082       NodeManager::currentNM()->mkNode(kind::BITVECTOR_SUB, a, b));
2083   return (diff.isConst() && (diff == utils::mkConst(size, 1u) || diff == utils::mkOnes(size)));
2084 }
2085
2086 template <>
2087 inline Node RewriteRule<IsPowerOfTwo>::apply(TNode node)
2088 {
2089   Debug("bv-rewrite") << "RewriteRule<IsPowerOfTwo>(" << node << ")"
2090                       << std::endl;
2091   NodeManager *nm = NodeManager::currentNM();
2092   TNode term = utils::isZero(node[0]) ? node[1] : node[0];
2093   TNode a = term[0];
2094   TNode b = term[1];
2095   unsigned size = utils::getSize(term);
2096   Node diff = Rewriter::rewrite(nm->mkNode(kind::BITVECTOR_SUB, a, b));
2097   Assert(diff.isConst());
2098   TNode x = diff == utils::mkConst(size, 1u) ? a : b;
2099   Node one = utils::mkConst(size, 1u);
2100   Node sk = utils::mkVar(size);
2101   Node sh = nm->mkNode(kind::BITVECTOR_SHL, one, sk);
2102   Node x_eq_sh = nm->mkNode(kind::EQUAL, x, sh);
2103   return x_eq_sh;
2104 }
2105
2106 /* -------------------------------------------------------------------------- */
2107
2108 /**
2109  * Rewrite
2110  *   sign_extend(x+t,n) * sign_extend(a,m) < sign_extend(x,n) * sign_extend(a,m)
2111  * to
2112  *   (and
2113  *    (not (= t zero))
2114  *    (not (= a zero))
2115  *    (= (bvslt (bvadd x t) x) (bvsgt a zero))
2116  *   )
2117  *
2118  * Rewrite
2119  *   zero_extend(x+t,n) * sign_extend(a,m) < zero_extend(x,n) * sign_extend(a,m)
2120  * to
2121  *   (and
2122  *    (not (= t zero))
2123  *    (not (= a zero))
2124  *    (= (bvult (bvadd x t) x) (bvsgt a zero))
2125  *   )
2126  * where n and m are sufficiently big to not produce an overflow for
2127  * the multiplications.
2128  *
2129  * These patterns occur in the quantified BV benchmark family 'ranking',
2130  * where the BV engine struggles due to the high bit widths of the
2131  * multiplication's operands.
2132  */
2133 static std::tuple<Node, Node, bool>
2134 extract_ext_tuple(TNode node)
2135 {
2136   TNode a = node[0];
2137   TNode b = node[1];
2138   for (unsigned i = 0; i < 2; ++i)
2139   {
2140     if (a.getKind() == kind::BITVECTOR_CONCAT
2141         && b.getKind() == kind::BITVECTOR_SIGN_EXTEND
2142         && a[0] == utils::mkZero(utils::getSize(a[0]))
2143         && utils::getSize(a[1]) <= utils::getSize(a[0])
2144         && utils::getSize(b[0]) <= utils::getSignExtendAmount(b))
2145     {
2146       return std::make_tuple(a[1], b[0], false);
2147     }
2148     else if (i == 0
2149              && a.getKind() == kind::BITVECTOR_SIGN_EXTEND
2150              && b.getKind() == kind::BITVECTOR_SIGN_EXTEND
2151              && utils::getSize(a[0]) <= utils::getSignExtendAmount(a)
2152              && utils::getSize(b[0]) <= utils::getSignExtendAmount(b))
2153     {
2154       return std::make_tuple(a[0], b[0], true);
2155     }
2156     std::swap(a, b);
2157   }
2158   return std::make_tuple(Node::null(), Node::null(), false);
2159 }
2160
2161 /* -------------------------------------------------------------------------- */
2162
2163 template<> inline
2164 bool RewriteRule<MultSltMult>::applies(TNode node)
2165 {
2166   if (node.getKind() != kind::BITVECTOR_SLT
2167       || node[0].getKind() != kind::BITVECTOR_MULT
2168       || node[1].getKind() != kind::BITVECTOR_MULT)
2169     return false;
2170
2171   if (node[0].getNumChildren() > 2 || node[1].getNumChildren() > 2)
2172     return false;
2173
2174   bool is_sext_l, is_sext_r;
2175   TNode ml[2], mr[2];
2176
2177   std::tie(ml[0], ml[1], is_sext_l) = extract_ext_tuple(node[0]);
2178   if (ml[0].isNull())
2179     return false;
2180
2181   std::tie(mr[0], mr[1], is_sext_r) = extract_ext_tuple(node[1]);
2182   if (mr[0].isNull())
2183     return false;
2184
2185   if (is_sext_l != is_sext_r)
2186     return false;
2187
2188   TNode addxt, x, a;
2189   if (ml[0].getKind() == kind::BITVECTOR_PLUS)
2190   {
2191     addxt = ml[0];
2192     a = ml[1];
2193   }
2194   else if (ml[1].getKind() == kind::BITVECTOR_PLUS)
2195   {
2196     addxt = ml[1];
2197     a = ml[0];
2198   }
2199   else
2200     return false;
2201
2202   if (addxt.getNumChildren() > 2)
2203     return false;
2204
2205   if (mr[0] == a)
2206   {
2207     x = mr[1];
2208   }
2209   else if (mr[1] == a)
2210   {
2211     x = mr[0];
2212   }
2213   else
2214     return false;
2215
2216   return (addxt[0] == x || addxt[1] == x);
2217 }
2218
2219 template<> inline
2220 Node RewriteRule<MultSltMult>::apply(TNode node)
2221 {
2222   bool is_sext;
2223   TNode ml[2], mr[2];
2224
2225   std::tie(ml[0], ml[1], is_sext) = extract_ext_tuple(node[0]);
2226   std::tie(mr[0], mr[1], std::ignore) = extract_ext_tuple(node[1]);
2227
2228   TNode addxt, x, t, a;
2229   if (ml[0].getKind() == kind::BITVECTOR_PLUS)
2230   {
2231     addxt = ml[0];
2232     a = ml[1];
2233   }
2234   else
2235   {
2236     Assert(ml[1].getKind() == kind::BITVECTOR_PLUS);
2237     addxt = ml[1];
2238     a = ml[0];
2239   }
2240
2241   x = (mr[0] == a) ? mr[1] : mr[0];
2242   t = (addxt[0] == x) ? addxt[1] : addxt[0];
2243
2244   NodeManager *nm = NodeManager::currentNM();
2245   Node zero_t = utils::mkZero(utils::getSize(t));
2246   Node zero_a = utils::mkZero(utils::getSize(a));
2247
2248   NodeBuilder<> nb(kind::AND);
2249   Kind k = is_sext ? kind::BITVECTOR_SLT : kind::BITVECTOR_ULT;
2250   nb << t.eqNode(zero_t).notNode();
2251   nb << a.eqNode(zero_a).notNode();
2252   nb << nm->mkNode(k, addxt, x)
2253             .eqNode(nm->mkNode(kind::BITVECTOR_SGT, a, zero_a));
2254   return nb.constructNode();
2255 }
2256
2257 }  // namespace bv
2258 }  // namespace theory
2259 }  // namespace CVC4