src/theory/bv/theory_bv_rewrite_rules_simplification.h

   1 /*********************                                                        */
   2 /*! \file theory_bv_rewrite_rules_simplification.h
   3  ** \verbatim
   4  ** Original author: lianah
   5  ** Major contributors: none
   6  ** Minor contributors (to current version):
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief [[ Add one-line brief description here ]]
  15  **
  16  ** [[ Add lengthier description here ]]
  17  ** \todo document this file
  18  **/
  19
  20 #include "cvc4_private.h"
  21
  22 #pragma once
  23
  24 #include "theory/bv/theory_bv_rewrite_rules.h"
  25 #include "theory/bv/theory_bv_utils.h"
  26
  27 namespace CVC4 {
  28 namespace theory {
  29 namespace bv {
  30
  31 // FIXME: this rules subsume the constant evaluation ones
  32
  33
  34 /**
  35  * ShlByConst
  36  *
  37  * Left Shift by constant amount
  38  */
  39 template<> inline
  40 bool RewriteRule<ShlByConst>::applies(Node node) {
  41   // if the shift amount is constant
  42   return (node.getKind() == kind::BITVECTOR_SHL &&
  43           node[1].getKind() == kind::CONST_BITVECTOR);
  44 }
  45
  46 template<> inline
  47 Node RewriteRule<ShlByConst>::apply(Node node) {
  48   BVDebug("bv-rewrite") << "RewriteRule<ShlByConst>(" << node << ")" << std::endl;
  49   Integer amount = node[1].getConst<BitVector>().toInteger();
  50
  51   Node a = node[0];
  52   uint32_t size = utils::getSize(a);
  53
  54
  55   if (amount >= Integer(size)) {
  56     // if we are shifting more than the length of the bitvector return 0
  57     return utils::mkConst(BitVector(size, Integer(0)));
  58   }
  59
  60   // make sure we do not lose information casting
  61   Assert(amount < Integer(1).multiplyByPow2(32));
  62
  63   uint32_t uint32_amount = amount.toUnsignedInt();
  64   Node left = utils::mkExtract(a, size - 1 - uint32_amount, 0);
  65   Node right = utils::mkConst(BitVector(uint32_amount, Integer(0)));
  66   return utils::mkConcat(left, right);
  67 }
  68
  69 /**
  70  * LshrByConst
  71  *
  72  * Right Logical Shift by constant amount
  73  */
  74
  75 template<> inline
  76 bool RewriteRule<LshrByConst>::applies(Node node) {
  77   // if the shift amount is constant
  78   return (node.getKind() == kind::BITVECTOR_LSHR &&
  79           node[1].getKind() == kind::CONST_BITVECTOR);
  80 }
  81
  82 template<> inline
  83 Node RewriteRule<LshrByConst>::apply(Node node) {
  84   BVDebug("bv-rewrite") << "RewriteRule<LshrByConst>(" << node << ")" << std::endl;
  85   Integer amount = node[1].getConst<BitVector>().toInteger();
  86
  87   Node a = node[0];
  88   uint32_t size = utils::getSize(a);
  89
  90
  91   if (amount >= Integer(size)) {
  92     // if we are shifting more than the length of the bitvector return 0
  93     return utils::mkConst(BitVector(size, Integer(0)));
  94   }
  95
  96   // make sure we do not lose information casting
  97   Assert(amount < Integer(1).multiplyByPow2(32));
  98
  99   uint32_t uint32_amount = amount.toUnsignedInt();
 100   Node right = utils::mkExtract(a, size - 1, uint32_amount);
 101   Node left = utils::mkConst(BitVector(uint32_amount, Integer(0)));
 102   return utils::mkConcat(left, right);
 103 }
 104
 105 /**
 106  * AshrByConst
 107  *
 108  * Right Arithmetic Shift by constant amount
 109  */
 110
 111 template<> inline
 112 bool RewriteRule<AshrByConst>::applies(Node node) {
 113   // if the shift amount is constant
 114   return (node.getKind() == kind::BITVECTOR_ASHR &&
 115           node[1].getKind() == kind::CONST_BITVECTOR);
 116 }
 117
 118 template<> inline
 119 Node RewriteRule<AshrByConst>::apply(Node node) {
 120   BVDebug("bv-rewrite") << "RewriteRule<AshrByConst>(" << node << ")" << std::endl;
 121   Integer amount = node[1].getConst<BitVector>().toInteger();
 122
 123   Node a = node[0];
 124   uint32_t size = utils::getSize(a);
 125   Node sign_bit = utils::mkExtract(a, size-1, size-1);
 126
 127   if (amount >= Integer(size)) {
 128     // if we are shifting more than the length of the bitvector return n repetitions
 129     // of the first bit
 130     return utils::mkConcat(sign_bit, size);
 131   }
 132
 133   // make sure we do not lose information casting
 134   Assert(amount < Integer(1).multiplyByPow2(32));
 135
 136   uint32_t uint32_amount = amount.toUnsignedInt();
 137   if (uint32_amount == 0) {
 138     return a;
 139   }
 140
 141   Node left = utils::mkConcat(sign_bit, uint32_amount);
 142   Node right = utils::mkExtract(a, size - 1, uint32_amount);
 143   return utils::mkConcat(left, right);
 144 }
 145
 146 /**
 147  * BitwiseIdemp
 148  *
 149  * (a bvand a) ==> a
 150  * (a bvor a)  ==> a
 151  */
 152
 153 template<> inline
 154 bool RewriteRule<BitwiseIdemp>::applies(Node node) {
 155   return ((node.getKind() == kind::BITVECTOR_AND ||
 156            node.getKind() == kind::BITVECTOR_OR) &&
 157           node[0] == node[1]);
 158 }
 159
 160 template<> inline
 161 Node RewriteRule<BitwiseIdemp>::apply(Node node) {
 162   BVDebug("bv-rewrite") << "RewriteRule<BitwiseIdemp>(" << node << ")" << std::endl;
 163   return node[0];
 164 }
 165
 166 /**
 167  * AndZero
 168  *
 169  * (a bvand 0) ==> 0
 170  */
 171
 172 template<> inline
 173 bool RewriteRule<AndZero>::applies(Node node) {
 174   unsigned size = utils::getSize(node);
 175   return (node.getKind() == kind::BITVECTOR_AND  &&
 176           (node[0] == utils::mkConst(size, 0) ||
 177            node[1] == utils::mkConst(size, 0)));
 178 }
 179
 180 template<> inline
 181 Node RewriteRule<AndZero>::apply(Node node) {
 182   BVDebug("bv-rewrite") << "RewriteRule<AndZero>(" << node << ")" << std::endl;
 183   return utils::mkConst(utils::getSize(node), 0);
 184 }
 185
 186 /**
 187  * AndOne
 188  *
 189  * (a bvand 1) ==> a
 190  */
 191
 192 template<> inline
 193 bool RewriteRule<AndOne>::applies(Node node) {
 194   unsigned size = utils::getSize(node);
 195   Node ones = utils::mkOnes(size);
 196   return (node.getKind() == kind::BITVECTOR_AND  &&
 197           (node[0] == ones ||
 198            node[1] == ones));
 199 }
 200
 201 template<> inline
 202 Node RewriteRule<AndOne>::apply(Node node) {
 203   BVDebug("bv-rewrite") << "RewriteRule<AndOne>(" << node << ")" << std::endl;
 204   unsigned size = utils::getSize(node);
 205
 206   if (node[0] == utils::mkOnes(size)) {
 207     return node[1];
 208   } else {
 209     Assert (node[1] == utils::mkOnes(size));
 210     return node[0];
 211   }
 212 }
 213
 214 /**
 215  * OrZero
 216  *
 217  * (a bvor 0) ==> a
 218  */
 219
 220 template<> inline
 221 bool RewriteRule<OrZero>::applies(Node node) {
 222   unsigned size = utils::getSize(node);
 223   return (node.getKind() == kind::BITVECTOR_OR  &&
 224           (node[0] == utils::mkConst(size, 0) ||
 225            node[1] == utils::mkConst(size, 0)));
 226 }
 227
 228 template<> inline
 229 Node RewriteRule<OrZero>::apply(Node node) {
 230   BVDebug("bv-rewrite") << "RewriteRule<OrZero>(" << node << ")" << std::endl;
 231
 232   unsigned size = utils::getSize(node);
 233   if (node[0] == utils::mkConst(size, 0)) {
 234     return node[1];
 235   } else {
 236     Assert(node[1] == utils::mkConst(size, 0));
 237     return node[0];
 238   }
 239 }
 240
 241 /**
 242  * OrOne
 243  *
 244  * (a bvor 1) ==> 1
 245  */
 246
 247 template<> inline
 248 bool RewriteRule<OrOne>::applies(Node node) {
 249   unsigned size = utils::getSize(node);
 250   Node ones = utils::mkOnes(size);
 251   return (node.getKind() == kind::BITVECTOR_OR  &&
 252           (node[0] == ones ||
 253            node[1] == ones));
 254 }
 255
 256 template<> inline
 257 Node RewriteRule<OrOne>::apply(Node node) {
 258   BVDebug("bv-rewrite") << "RewriteRule<OrOne>(" << node << ")" << std::endl;
 259   return utils::mkOnes(utils::getSize(node));
 260 }
 261
 262
 263 /**
 264  * XorDuplicate
 265  *
 266  * (a bvxor a) ==> 0
 267  */
 268
 269 template<> inline
 270 bool RewriteRule<XorDuplicate>::applies(Node node) {
 271   return (node.getKind() == kind::BITVECTOR_XOR &&
 272           node[0] == node[1]);
 273 }
 274
 275 template<> inline
 276 Node RewriteRule<XorDuplicate>::apply(Node node) {
 277   BVDebug("bv-rewrite") << "RewriteRule<XorDuplicate>(" << node << ")" << std::endl;
 278   return utils::mkConst(BitVector(utils::getSize(node), Integer(0)));
 279 }
 280
 281 /**
 282  * XorOne
 283  *
 284  * (a bvxor 1) ==> ~a
 285  */
 286
 287 template<> inline
 288 bool RewriteRule<XorOne>::applies(Node node) {
 289   if (node.getKind() != kind::BITVECTOR_XOR) {
 290     return false;
 291   }
 292   Node ones = utils::mkOnes(utils::getSize(node));
 293   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
 294     if (node[i] == ones) {
 295       return true;
 296     }
 297   }
 298   return false;
 299 }
 300
 301 template<> inline
 302 Node RewriteRule<XorOne>::apply(Node node) {
 303   BVDebug("bv-rewrite") << "RewriteRule<XorOne>(" << node << ")" << std::endl;
 304   Node ones = utils::mkOnes(utils::getSize(node));
 305   std::vector<Node> children;
 306   bool found_ones = false;
 307   // XorSimplify should have been called before
 308   for(unsigned i = 0; i < node.getNumChildren(); ++i) {
 309     if (node[i] == ones) {
 310       // make sure only ones occurs only once
 311       Assert(!found_ones);
 312       found_ones = true;
 313     } else {
 314       children.push_back(node[i]);
 315     }
 316   }
 317
 318   children[0] = utils::mkNode(kind::BITVECTOR_NOT, children[0]);
 319   return utils::mkSortedNode(kind::BITVECTOR_XOR, children);
 320 }
 321
 322
 323 /**
 324  * XorZero
 325  *
 326  * (a bvxor 0) ==> a
 327  */
 328
 329 template<> inline
 330 bool RewriteRule<XorZero>::applies(Node node) {
 331   if (node.getKind() != kind::BITVECTOR_XOR) {
 332     return false;
 333   }
 334   Node zero = utils::mkConst(utils::getSize(node), 0);
 335   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
 336     if (node[i] == zero) {
 337       return true;
 338     }
 339   }
 340   return false;
 341 }
 342
 343 template<> inline
 344 Node RewriteRule<XorZero>::apply(Node node) {
 345   BVDebug("bv-rewrite") << "RewriteRule<XorZero>(" << node << ")" << std::endl;
 346   std::vector<Node> children;
 347   bool found_zero = false;
 348   Node zero = utils::mkConst(utils::getSize(node), 0);
 349
 350   // XorSimplify should have been called before
 351   for(unsigned i = 0; i < node.getNumChildren(); ++i) {
 352     if (node[i] == zero) {
 353       // make sure zero occurs only once
 354       Assert(!found_zero);
 355       found_zero = true;
 356     } else {
 357       children.push_back(node[i]);
 358     }
 359   }
 360
 361   return utils::mkNode(kind::BITVECTOR_XOR, children);
 362 }
 363
 364
 365 /**
 366  * BitwiseNotAnd
 367  *
 368  * (a bvand (~ a)) ==> 0
 369  */
 370
 371 template<> inline
 372 bool RewriteRule<BitwiseNotAnd>::applies(Node node) {
 373   return (node.getKind() == kind::BITVECTOR_AND &&
 374           ((node[0].getKind() == kind::BITVECTOR_NOT && node[0][0] == node[1]) ||
 375            (node[1].getKind() == kind::BITVECTOR_NOT && node[1][0] == node[0])));
 376 }
 377
 378 template<> inline
 379 Node RewriteRule<BitwiseNotAnd>::apply(Node node) {
 380   BVDebug("bv-rewrite") << "RewriteRule<BitwiseNegAnd>(" << node << ")" << std::endl;
 381   return utils::mkConst(BitVector(utils::getSize(node), Integer(0)));
 382 }
 383
 384 /**
 385  * BitwiseNegOr
 386  *
 387  * (a bvor (~ a)) ==> 1
 388  */
 389
 390 template<> inline
 391 bool RewriteRule<BitwiseNotOr>::applies(Node node) {
 392   return (node.getKind() == kind::BITVECTOR_OR &&
 393           ((node[0].getKind() == kind::BITVECTOR_NOT && node[0][0] == node[1]) ||
 394            (node[1].getKind() == kind::BITVECTOR_NOT && node[1][0] == node[0])));
 395 }
 396
 397 template<> inline
 398 Node RewriteRule<BitwiseNotOr>::apply(Node node) {
 399   BVDebug("bv-rewrite") << "RewriteRule<BitwiseNotOr>(" << node << ")" << std::endl;
 400   uint32_t size = utils::getSize(node);
 401   Integer ones = Integer(1).multiplyByPow2(size) - 1;
 402   return utils::mkConst(BitVector(size, ones));
 403 }
 404
 405 /**
 406  * XorNot
 407  *
 408  * ((~ a) bvxor (~ b)) ==> (a bvxor b)
 409  */
 410
 411 template<> inline
 412 bool RewriteRule<XorNot>::applies(Node node) {
 413   return (node.getKind() == kind::BITVECTOR_XOR &&
 414           node[0].getKind() == kind::BITVECTOR_NOT &&
 415           node[1].getKind() == kind::BITVECTOR_NOT);
 416 }
 417
 418 template<> inline
 419 Node RewriteRule<XorNot>::apply(Node node) {
 420   BVDebug("bv-rewrite") << "RewriteRule<XorNot>(" << node << ")" << std::endl;
 421   Node a = node[0][0];
 422   Node b = node[1][0];
 423   return utils::mkNode(kind::BITVECTOR_XOR, a, b);
 424 }
 425
 426 /**
 427  * NotXor
 428  *
 429  * ~(a bvxor b) ==> (~ a bvxor b)
 430  */
 431
 432 template<> inline
 433 bool RewriteRule<NotXor>::applies(Node node) {
 434   return (node.getKind() == kind::BITVECTOR_NOT &&
 435           node[0].getKind() == kind::BITVECTOR_XOR);
 436 }
 437
 438 template<> inline
 439 Node RewriteRule<NotXor>::apply(Node node) {
 440   BVDebug("bv-rewrite") << "RewriteRule<XorNot>(" << node << ")" << std::endl;
 441   Node a = node[0][0];
 442   Node b = node[0][1];
 443   Node nota = utils::mkNode(kind::BITVECTOR_NOT, a);
 444   return utils::mkSortedNode(kind::BITVECTOR_XOR, nota, b);
 445 }
 446
 447 /**
 448  * NotIdemp
 449  *
 450  * ~ (~ a) ==> a
 451  */
 452
 453 template<> inline
 454 bool RewriteRule<NotIdemp>::applies(Node node) {
 455   return (node.getKind() == kind::BITVECTOR_NOT &&
 456           node[0].getKind() == kind::BITVECTOR_NOT);
 457 }
 458
 459 template<> inline
 460 Node RewriteRule<NotIdemp>::apply(Node node) {
 461   BVDebug("bv-rewrite") << "RewriteRule<XorIdemp>(" << node << ")" << std::endl;
 462   return node[0][0];
 463 }
 464
 465
 466
 467 /**
 468  * LtSelf
 469  *
 470  * a < a ==> false
 471  */
 472
 473 template<> inline
 474 bool RewriteRule<LtSelf>::applies(Node node) {
 475   return ((node.getKind() == kind::BITVECTOR_ULT ||
 476            node.getKind() == kind::BITVECTOR_SLT) &&
 477           node[0] == node[1]);
 478 }
 479
 480 template<> inline
 481 Node RewriteRule<LtSelf>::apply(Node node) {
 482   BVDebug("bv-rewrite") << "RewriteRule<LtSelf>(" << node << ")" << std::endl;
 483   return utils::mkFalse();
 484 }
 485
 486 /**
 487  * LteSelf
 488  *
 489  * a <= a ==> true
 490  */
 491
 492 template<> inline
 493 bool RewriteRule<LteSelf>::applies(Node node) {
 494   return ((node.getKind() == kind::BITVECTOR_ULE ||
 495            node.getKind() == kind::BITVECTOR_SLE) &&
 496           node[0] == node[1]);
 497 }
 498
 499 template<> inline
 500 Node RewriteRule<LteSelf>::apply(Node node) {
 501   BVDebug("bv-rewrite") << "RewriteRule<LteSelf>(" << node << ")" << std::endl;
 502   return utils::mkTrue();
 503 }
 504
 505 /**
 506  * UltZero
 507  *
 508  * a < 0 ==> false
 509  */
 510
 511 template<> inline
 512 bool RewriteRule<UltZero>::applies(Node node) {
 513   return (node.getKind() == kind::BITVECTOR_ULT &&
 514           node[1] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0))));
 515 }
 516
 517 template<> inline
 518 Node RewriteRule<UltZero>::apply(Node node) {
 519   BVDebug("bv-rewrite") << "RewriteRule<UltZero>(" << node << ")" << std::endl;
 520   return utils::mkFalse();
 521 }
 522
 523 /**
 524  * UltSelf
 525  *
 526  * a < a ==> false
 527  */
 528
 529 template<> inline
 530 bool RewriteRule<UltSelf>::applies(Node node) {
 531   return (node.getKind() == kind::BITVECTOR_ULT &&
 532           node[1] == node[0]);
 533 }
 534
 535 template<> inline
 536 Node RewriteRule<UltSelf>::apply(Node node) {
 537   BVDebug("bv-rewrite") << "RewriteRule<UltSelf>(" << node << ")" << std::endl;
 538   return utils::mkFalse();
 539 }
 540
 541
 542 /**
 543  * UleZero
 544  *
 545  * a <= 0 ==> a = 0
 546  */
 547
 548 template<> inline
 549 bool RewriteRule<UleZero>::applies(Node node) {
 550   return (node.getKind() == kind::BITVECTOR_ULE &&
 551           node[1] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0))));
 552 }
 553
 554 template<> inline
 555 Node RewriteRule<UleZero>::apply(Node node) {
 556   BVDebug("bv-rewrite") << "RewriteRule<UleZero>(" << node << ")" << std::endl;
 557   return utils::mkNode(kind::EQUAL, node[0], node[1]);
 558 }
 559
 560 /**
 561  * UleSelf
 562  *
 563  * a <= a ==> true
 564  */
 565
 566 template<> inline
 567 bool RewriteRule<UleSelf>::applies(Node node) {
 568   return (node.getKind() == kind::BITVECTOR_ULE &&
 569           node[1] == node[0]);
 570 }
 571
 572 template<> inline
 573 Node RewriteRule<UleSelf>::apply(Node node) {
 574   BVDebug("bv-rewrite") << "RewriteRule<UleSelf>(" << node << ")" << std::endl;
 575   return utils::mkTrue();
 576 }
 577
 578
 579 /**
 580  * ZeroUle
 581  *
 582  * 0 <= a ==> true
 583  */
 584
 585 template<> inline
 586 bool RewriteRule<ZeroUle>::applies(Node node) {
 587   return (node.getKind() == kind::BITVECTOR_ULE &&
 588           node[0] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0))));
 589 }
 590
 591 template<> inline
 592 Node RewriteRule<ZeroUle>::apply(Node node) {
 593   BVDebug("bv-rewrite") << "RewriteRule<ZeroUle>(" << node << ")" << std::endl;
 594   return utils::mkTrue();
 595 }
 596
 597 /**
 598  * UleMax
 599  *
 600  * a <= 11..1 ==> true
 601  */
 602
 603 template<> inline
 604 bool RewriteRule<UleMax>::applies(Node node) {
 605   if (node.getKind()!= kind::BITVECTOR_ULE) {
 606     return false;
 607   }
 608   uint32_t size = utils::getSize(node[0]);
 609   Integer ones = Integer(1).multiplyByPow2(size) -1;
 610   return (node.getKind() == kind::BITVECTOR_ULE &&
 611           node[1] == utils::mkConst(BitVector(size, ones)));
 612 }
 613
 614 template<> inline
 615 Node RewriteRule<UleMax>::apply(Node node) {
 616   BVDebug("bv-rewrite") << "RewriteRule<UleMax>(" << node << ")" << std::endl;
 617   return utils::mkTrue();
 618 }
 619
 620 /**
 621  * NotUlt
 622  *
 623  * ~ ( a < b) ==> b <= a
 624  */
 625
 626 template<> inline
 627 bool RewriteRule<NotUlt>::applies(Node node) {
 628   return (node.getKind() == kind::NOT &&
 629           node[0].getKind() == kind::BITVECTOR_ULT);
 630 }
 631
 632 template<> inline
 633 Node RewriteRule<NotUlt>::apply(Node node) {
 634   BVDebug("bv-rewrite") << "RewriteRule<NotUlt>(" << node << ")" << std::endl;
 635   Node ult = node[0];
 636   Node a = ult[0];
 637   Node b = ult[1];
 638   return utils::mkNode(kind::BITVECTOR_ULE, b, a);
 639 }
 640
 641 /**
 642  * NotUle
 643  *
 644  * ~ ( a <= b) ==> b < a
 645  */
 646
 647 template<> inline
 648 bool RewriteRule<NotUle>::applies(Node node) {
 649   return (node.getKind() == kind::NOT &&
 650           node[0].getKind() == kind::BITVECTOR_ULE);
 651 }
 652
 653 template<> inline
 654 Node RewriteRule<NotUle>::apply(Node node) {
 655   BVDebug("bv-rewrite") << "RewriteRule<NotUle>(" << node << ")" << std::endl;
 656   Node ult = node[0];
 657   Node a = ult[0];
 658   Node b = ult[1];
 659   return utils::mkNode(kind::BITVECTOR_ULT, b, a);
 660 }
 661
 662 /**
 663  * MultOne
 664  *
 665  * (a * 1) ==> a
 666  */
 667
 668 template<> inline
 669 bool RewriteRule<MultOne>::applies(Node node) {
 670   unsigned size = utils::getSize(node);
 671   return (node.getKind() == kind::BITVECTOR_MULT &&
 672           (node[0] == utils::mkConst(size, 1) ||
 673            node[1] == utils::mkConst(size, 1)));
 674 }
 675
 676 template<> inline
 677 Node RewriteRule<MultOne>::apply(Node node) {
 678   BVDebug("bv-rewrite") << "RewriteRule<MultOne>(" << node << ")" << std::endl;
 679   unsigned size = utils::getSize(node);
 680   if (node[0] == utils::mkConst(size, 1)) {
 681     return node[1];
 682   }
 683   Assert(node[1] == utils::mkConst(size, 1));
 684   return node[0];
 685 }
 686
 687 /**
 688  * MultZero
 689  *
 690  * (a * 0) ==> 0
 691  */
 692
 693 template<> inline
 694 bool RewriteRule<MultZero>::applies(Node node) {
 695   unsigned size = utils::getSize(node);
 696   return (node.getKind() == kind::BITVECTOR_MULT &&
 697           (node[0] == utils::mkConst(size, 0) ||
 698            node[1] == utils::mkConst(size, 0)));
 699 }
 700
 701 template<> inline
 702 Node RewriteRule<MultZero>::apply(Node node) {
 703   BVDebug("bv-rewrite") << "RewriteRule<MultZero>(" << node << ")" << std::endl;
 704   return utils::mkConst(utils::getSize(node), 0);
 705 }
 706
 707 /**
 708  * MultPow2
 709  *
 710  * (a * 2^k) ==> a[n-k-1:0] 0_k
 711  */
 712
 713 template<> inline
 714 bool RewriteRule<MultPow2>::applies(Node node) {
 715   if (node.getKind() != kind::BITVECTOR_MULT)
 716     return false;
 717
 718   for(unsigned i = 0; i < node.getNumChildren(); ++i) {
 719     if (utils::isPow2Const(node[i])) {
 720       return true;
 721     }
 722   }
 723   return false;
 724 }
 725
 726 template<> inline
 727 Node RewriteRule<MultPow2>::apply(Node node) {
 728   BVDebug("bv-rewrite") << "RewriteRule<MultPow2>(" << node << ")" << std::endl;
 729
 730   std::vector<Node>  children;
 731   unsigned exponent = 0;
 732   for(unsigned i = 0; i < node.getNumChildren(); ++i) {
 733     unsigned exp = utils::isPow2Const(node[i]);
 734     if (exp) {
 735       exponent += exp - 1;
 736     }
 737     else {
 738       children.push_back(node[i]);
 739     }
 740   }
 741
 742   Node a = utils::mkSortedNode(kind::BITVECTOR_MULT, children);
 743
 744   Node extract = utils::mkExtract(a, utils::getSize(node) - exponent - 1, 0);
 745   Node zeros = utils::mkConst(exponent, 0);
 746   return utils::mkConcat(extract, zeros);
 747 }
 748
 749 /**
 750  * PlusZero
 751  *
 752  * (a + 0) ==> a
 753  */
 754
 755 template<> inline
 756 bool RewriteRule<PlusZero>::applies(Node node) {
 757   Node zero = utils::mkConst(utils::getSize(node), 0);
 758   return (node.getKind() == kind::BITVECTOR_PLUS &&
 759           (node[0] == zero ||
 760            node[1] == zero));
 761 }
 762
 763 template<> inline
 764 Node RewriteRule<PlusZero>::apply(Node node) {
 765   BVDebug("bv-rewrite") << "RewriteRule<PlusZero>(" << node << ")" << std::endl;
 766   Node zero = utils::mkConst(utils::getSize(node), 0);
 767   if (node[0] == zero) {
 768     return node[1];
 769   }
 770
 771   return node[0];
 772 }
 773
 774 /**
 775  * NegIdemp
 776  *
 777  * -(-a) ==> a
 778  */
 779
 780 template<> inline
 781 bool RewriteRule<NegIdemp>::applies(Node node) {
 782   return (node.getKind() == kind::BITVECTOR_NEG &&
 783           node[0].getKind() == kind::BITVECTOR_NEG);
 784 }
 785
 786 template<> inline
 787 Node RewriteRule<NegIdemp>::apply(Node node) {
 788   BVDebug("bv-rewrite") << "RewriteRule<NegIdemp>(" << node << ")" << std::endl;
 789   return node[0][0];
 790 }
 791
 792 /**
 793  * UdivPow2
 794  *
 795  * (a udiv 2^k) ==> 0_k a[n-1: k]
 796  */
 797
 798 template<> inline
 799 bool RewriteRule<UdivPow2>::applies(Node node) {
 800   return (node.getKind() == kind::BITVECTOR_UDIV &&
 801           utils::isPow2Const(node[1]));
 802 }
 803
 804 template<> inline
 805 Node RewriteRule<UdivPow2>::apply(Node node) {
 806   BVDebug("bv-rewrite") << "RewriteRule<UdivPow2>(" << node << ")" << std::endl;
 807   Node a = node[0];
 808   unsigned power = utils::isPow2Const(node[1]) -1;
 809
 810   Node extract = utils::mkExtract(a, utils::getSize(node) - 1, power);
 811   Node zeros = utils::mkConst(power, 0);
 812
 813   return utils::mkNode(kind::BITVECTOR_CONCAT, zeros, extract);
 814 }
 815
 816 /**
 817  * UdivOne
 818  *
 819  * (a udiv 1) ==> a
 820  */
 821
 822 template<> inline
 823 bool RewriteRule<UdivOne>::applies(Node node) {
 824   return (node.getKind() == kind::BITVECTOR_UDIV &&
 825           node[1] == utils::mkConst(utils::getSize(node), 1));
 826 }
 827
 828 template<> inline
 829 Node RewriteRule<UdivOne>::apply(Node node) {
 830   BVDebug("bv-rewrite") << "RewriteRule<UdivOne>(" << node << ")" << std::endl;
 831   return node[0];
 832 }
 833
 834 /**
 835  * UdivSelf
 836  *
 837  * (a udiv a) ==> 1
 838  */
 839
 840 template<> inline
 841 bool RewriteRule<UdivSelf>::applies(Node node) {
 842   return (node.getKind() == kind::BITVECTOR_UDIV &&
 843           node[0] == node[1]);
 844 }
 845
 846 template<> inline
 847 Node RewriteRule<UdivSelf>::apply(Node node) {
 848   BVDebug("bv-rewrite") << "RewriteRule<UdivSelf>(" << node << ")" << std::endl;
 849   return utils::mkConst(utils::getSize(node), 1);
 850 }
 851
 852 /**
 853  * UremPow2
 854  *
 855  * (a urem 2^k) ==> 0_(n-k) a[k-1:0]
 856  */
 857
 858 template<> inline
 859 bool RewriteRule<UremPow2>::applies(Node node) {
 860   return (node.getKind() == kind::BITVECTOR_UREM &&
 861           utils::isPow2Const(node[1]));
 862 }
 863
 864 template<> inline
 865 Node RewriteRule<UremPow2>::apply(Node node) {
 866   BVDebug("bv-rewrite") << "RewriteRule<UremPow2>(" << node << ")" << std::endl;
 867   TNode a = node[0];
 868   unsigned power = utils::isPow2Const(node[1]) - 1;
 869   if (power == 0) {
 870     return utils::mkConst(utils::getSize(node), 0);
 871   }
 872   Node extract = utils::mkExtract(a, power - 1, 0);
 873   Node zeros = utils::mkConst(utils::getSize(node) - power, 0);
 874   return utils::mkNode(kind::BITVECTOR_CONCAT, zeros, extract);
 875 }
 876
 877 /**
 878  * UremOne
 879  *
 880  * (a urem 1) ==> 0
 881  */
 882
 883 template<> inline
 884 bool RewriteRule<UremOne>::applies(Node node) {
 885   return (node.getKind() == kind::BITVECTOR_UREM &&
 886           node[1] == utils::mkConst(utils::getSize(node), 1));
 887 }
 888
 889 template<> inline
 890 Node RewriteRule<UremOne>::apply(Node node) {
 891   BVDebug("bv-rewrite") << "RewriteRule<UremOne>(" << node << ")" << std::endl;
 892   return utils::mkConst(utils::getSize(node), 0);
 893 }
 894
 895 /**
 896  * UremSelf
 897  *
 898  * (a urem a) ==> 0
 899  */
 900
 901 template<> inline
 902 bool RewriteRule<UremSelf>::applies(Node node) {
 903   return (node.getKind() == kind::BITVECTOR_UREM &&
 904           node[0] == node[1]);
 905 }
 906
 907 template<> inline
 908 Node RewriteRule<UremSelf>::apply(Node node) {
 909   BVDebug("bv-rewrite") << "RewriteRule<UremSelf>(" << node << ")" << std::endl;
 910   return utils::mkConst(utils::getSize(node), 0);
 911 }
 912
 913 /**
 914  * ShiftZero
 915  *
 916  * (0_k >> a) ==> 0_k
 917  */
 918
 919 template<> inline
 920 bool RewriteRule<ShiftZero>::applies(Node node) {
 921   return ((node.getKind() == kind::BITVECTOR_SHL ||
 922            node.getKind() == kind::BITVECTOR_LSHR ||
 923            node.getKind() == kind::BITVECTOR_ASHR) &&
 924           node[0] == utils::mkConst(utils::getSize(node), 0));
 925 }
 926
 927 template<> inline
 928 Node RewriteRule<ShiftZero>::apply(Node node) {
 929   BVDebug("bv-rewrite") << "RewriteRule<ShiftZero>(" << node << ")" << std::endl;
 930   return node[0];
 931 }
 932
 933 /**
 934  * BBPlusNeg
 935  *
 936  * -a1 - a2 - ... - an + ak + ..  ==> - (a1 + a2 + ... + an) + ak
 937  *
 938  */
 939
 940 template<> inline
 941 bool RewriteRule<BBPlusNeg>::applies(Node node) {
 942   if (node.getKind() != kind::BITVECTOR_PLUS) {
 943     return false;
 944   }
 945
 946   unsigned neg_count = 0;
 947   for(unsigned i = 0; i < node.getNumChildren(); ++i) {
 948     if (node[i].getKind()== kind::BITVECTOR_NEG) {
 949       ++neg_count;
 950     }
 951   }
 952   return neg_count > 1;
 953 }
 954
 955 template<> inline
 956 Node RewriteRule<BBPlusNeg>::apply(Node node) {
 957   BVDebug("bv-rewrite") << "RewriteRule<BBPlusNeg>(" << node << ")" << std::endl;
 958
 959   std::vector<Node> children;
 960   unsigned neg_count = 0;
 961   for(unsigned i = 0; i < node.getNumChildren(); ++i) {
 962     if (node[i].getKind() == kind::BITVECTOR_NEG) {
 963       ++neg_count;
 964       children.push_back(utils::mkNode(kind::BITVECTOR_NOT, node[i][0]));
 965     } else {
 966       children.push_back(node[i]);
 967     }
 968   }
 969   Assert(neg_count!= 0);
 970   children.push_back(utils::mkConst(utils::getSize(node), neg_count));
 971
 972   return utils::mkSortedNode(kind::BITVECTOR_PLUS, children);
 973 }
 974
 975 // /**
 976 //  *
 977 //  *
 978 //  *
 979 //  */
 980
 981 // template<> inline
 982 // bool RewriteRule<BBFactorOut>::applies(Node node) {
 983 //   if (node.getKind() != kind::BITVECTOR_PLUS) {
 984 //     return false;
 985 //   }
 986
 987 //   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
 988 //     if (node[i].getKind() != kind::BITVECTOR_MULT) {
 989 //       return false;
 990 //     }
 991 //   }
 992 // }
 993
 994 // template<> inline
 995 // Node RewriteRule<BBFactorOut>::apply(Node node) {
 996 //   BVDebug("bv-rewrite") << "RewriteRule<BBFactorOut>(" << node << ")" << std::endl;
 997 //   std::hash_set<TNode, TNodeHashFunction> factors;
 998
 999 //   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
1000 //     Assert (node[i].getKind() == kind::BITVECTOR_MULT);
1001 //     for (unsigned j = 0; j < node[i].getNumChildren(); ++j) {
1002 //       factors.insert(node[i][j]);
1003 //     }
1004 //   }
1005
1006 //   std::vector<TNode> gcd;
1007 //   std::hash_set<TNode, TNodeHashFunction>::const_iterator it;
1008 //   for (it = factors.begin(); it != factors.end(); ++it) {
1009 //     // for each factor check if it occurs in all children
1010 //     TNode f = *it;
1011 //     for (unsigned i = 0; i < node.getNumChildren
1012
1013 //     }
1014 //   }
1015 //   return ;
1016 // }
1017
1018
1019 // /**
1020 //  *
1021 //  *
1022 //  *
1023 //  */
1024
1025 // template<> inline
1026 // bool RewriteRule<>::applies(Node node) {
1027 //   return (node.getKind() == );
1028 // }
1029
1030 // template<> inline
1031 // Node RewriteRule<>::apply(Node node) {
1032 //   BVDebug("bv-rewrite") << "RewriteRule<>(" << node << ")" << std::endl;
1033 //   return ;
1034 // }
1035
1036
1037
1038 }
1039 }
1040 }