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, Clark Barrett, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2016 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 "theory/bv/theory_bv_rewrite_rules.h"
  23 #include "theory/bv/theory_bv_utils.h"
  24
  25 namespace CVC4 {
  26 namespace theory {
  27 namespace bv {
  28
  29 // FIXME: this rules subsume the constant evaluation ones
  30
  31
  32 /**
  33  * ShlByConst
  34  *
  35  * Left Shift by constant amount
  36  */
  37 template<> inline
  38 bool RewriteRule<ShlByConst>::applies(TNode node) {
  39   // if the shift amount is constant
  40   return (node.getKind() == kind::BITVECTOR_SHL &&
  41           node[1].getKind() == kind::CONST_BITVECTOR);
  42 }
  43
  44 template<> inline
  45 Node RewriteRule<ShlByConst>::apply(TNode node) {
  46   Debug("bv-rewrite") << "RewriteRule<ShlByConst>(" << node << ")" << std::endl;
  47   Integer amount = node[1].getConst<BitVector>().toInteger();
  48   if (amount == 0) {
  49     return node[0];
  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
  65   Node left = utils::mkExtract(a, size - 1 - uint32_amount, 0);
  66   Node right = utils::mkConst(BitVector(uint32_amount, Integer(0)));
  67   return utils::mkConcat(left, right);
  68 }
  69
  70 /**
  71  * LshrByConst
  72  *
  73  * Right Logical Shift by constant amount
  74  */
  75
  76 template<> inline
  77 bool RewriteRule<LshrByConst>::applies(TNode node) {
  78   // if the shift amount is constant
  79   return (node.getKind() == kind::BITVECTOR_LSHR &&
  80           node[1].getKind() == kind::CONST_BITVECTOR);
  81 }
  82
  83 template<> inline
  84 Node RewriteRule<LshrByConst>::apply(TNode node) {
  85   Debug("bv-rewrite") << "RewriteRule<LshrByConst>(" << node << ")" << std::endl;
  86   Integer amount = node[1].getConst<BitVector>().toInteger();
  87   if (amount == 0) {
  88     return node[0];
  89   }
  90
  91   Node a = node[0];
  92   uint32_t size = utils::getSize(a);
  93
  94
  95   if (amount >= Integer(size)) {
  96     // if we are shifting more than the length of the bitvector return 0
  97     return utils::mkConst(BitVector(size, Integer(0)));
  98   }
  99
 100   // make sure we do not lose information casting
 101   Assert(amount < Integer(1).multiplyByPow2(32));
 102
 103   uint32_t uint32_amount = amount.toUnsignedInt();
 104   Node right = utils::mkExtract(a, size - 1, uint32_amount);
 105   Node left = utils::mkConst(BitVector(uint32_amount, Integer(0)));
 106   return utils::mkConcat(left, right);
 107 }
 108
 109 /**
 110  * AshrByConst
 111  *
 112  * Right Arithmetic Shift by constant amount
 113  */
 114
 115 template<> inline
 116 bool RewriteRule<AshrByConst>::applies(TNode node) {
 117   // if the shift amount is constant
 118   return (node.getKind() == kind::BITVECTOR_ASHR &&
 119           node[1].getKind() == kind::CONST_BITVECTOR);
 120 }
 121
 122 template<> inline
 123 Node RewriteRule<AshrByConst>::apply(TNode node) {
 124   Debug("bv-rewrite") << "RewriteRule<AshrByConst>(" << node << ")" << std::endl;
 125   Integer amount = node[1].getConst<BitVector>().toInteger();
 126   if (amount == 0) {
 127     return node[0];
 128   }
 129
 130   Node a = node[0];
 131   uint32_t size = utils::getSize(a);
 132   Node sign_bit = utils::mkExtract(a, size-1, size-1);
 133
 134   if (amount >= Integer(size)) {
 135     // if we are shifting more than the length of the bitvector return n repetitions
 136     // of the first bit
 137     return utils::mkConcat(sign_bit, size);
 138   }
 139
 140   // make sure we do not lose information casting
 141   Assert(amount < Integer(1).multiplyByPow2(32));
 142
 143   uint32_t uint32_amount = amount.toUnsignedInt();
 144   if (uint32_amount == 0) {
 145     return a;
 146   }
 147
 148   Node left = utils::mkConcat(sign_bit, uint32_amount);
 149   Node right = utils::mkExtract(a, size - 1, uint32_amount);
 150   return utils::mkConcat(left, right);
 151 }
 152
 153 /**
 154  * BitwiseIdemp
 155  *
 156  * (a bvand a) ==> a
 157  * (a bvor a)  ==> a
 158  */
 159
 160 template<> inline
 161 bool RewriteRule<BitwiseIdemp>::applies(TNode node) {
 162   Unreachable();
 163   return ((node.getKind() == kind::BITVECTOR_AND ||
 164            node.getKind() == kind::BITVECTOR_OR) &&
 165           node.getNumChildren() == 2 &&
 166           node[0] == node[1]);
 167 }
 168
 169 template<> inline
 170 Node RewriteRule<BitwiseIdemp>::apply(TNode node) {
 171   Unreachable();
 172   Debug("bv-rewrite") << "RewriteRule<BitwiseIdemp>(" << node << ")" << std::endl;
 173   return node[0];
 174 }
 175
 176 /**
 177  * AndZero
 178  *
 179  * (a bvand 0) ==> 0
 180  */
 181
 182 template<> inline
 183 bool RewriteRule<AndZero>::applies(TNode node) {
 184   Unreachable();
 185   unsigned size = utils::getSize(node);
 186   return (node.getKind() == kind::BITVECTOR_AND  &&
 187           node.getNumChildren() == 2 &&
 188           (node[0] == utils::mkConst(size, 0) ||
 189            node[1] == utils::mkConst(size, 0)));
 190 }
 191
 192 template<> inline
 193 Node RewriteRule<AndZero>::apply(TNode node) {
 194   Unreachable();
 195   Debug("bv-rewrite") << "RewriteRule<AndZero>(" << node << ")" << std::endl;
 196   return utils::mkConst(utils::getSize(node), 0);
 197 }
 198
 199 /**
 200  * AndOne
 201  *
 202  * (a bvand 1) ==> a
 203  */
 204
 205 template<> inline
 206 bool RewriteRule<AndOne>::applies(TNode node) {
 207   Unreachable();
 208   unsigned size = utils::getSize(node);
 209   Node ones = utils::mkOnes(size);
 210   return (node.getKind() == kind::BITVECTOR_AND  &&
 211           node.getNumChildren() == 2 &&
 212           (node[0] == ones ||
 213            node[1] == ones));
 214 }
 215
 216 template<> inline
 217 Node RewriteRule<AndOne>::apply(TNode node) {
 218   Unreachable();
 219   Debug("bv-rewrite") << "RewriteRule<AndOne>(" << node << ")" << std::endl;
 220   unsigned size = utils::getSize(node);
 221
 222   if (node[0] == utils::mkOnes(size)) {
 223     return node[1];
 224   } else {
 225     Assert (node[1] == utils::mkOnes(size));
 226     return node[0];
 227   }
 228 }
 229
 230 /**
 231  * OrZero
 232  *
 233  * (a bvor 0) ==> a
 234  */
 235
 236 template<> inline
 237 bool RewriteRule<OrZero>::applies(TNode node) {
 238   Unreachable();
 239   unsigned size = utils::getSize(node);
 240   return (node.getKind() == kind::BITVECTOR_OR  &&
 241           node.getNumChildren() == 2 &&
 242           (node[0] == utils::mkConst(size, 0) ||
 243            node[1] == utils::mkConst(size, 0)));
 244 }
 245
 246 template<> inline
 247 Node RewriteRule<OrZero>::apply(TNode node) {
 248   Unreachable();
 249   Debug("bv-rewrite") << "RewriteRule<OrZero>(" << node << ")" << std::endl;
 250
 251   unsigned size = utils::getSize(node);
 252   if (node[0] == utils::mkConst(size, 0)) {
 253     return node[1];
 254   } else {
 255     Assert(node[1] == utils::mkConst(size, 0));
 256     return node[0];
 257   }
 258 }
 259
 260 /**
 261  * OrOne
 262  *
 263  * (a bvor 1) ==> 1
 264  */
 265
 266 template<> inline
 267 bool RewriteRule<OrOne>::applies(TNode node) {
 268   Unreachable();
 269   unsigned size = utils::getSize(node);
 270   Node ones = utils::mkOnes(size);
 271   return (node.getKind() == kind::BITVECTOR_OR  &&
 272           node.getNumChildren() == 2 &&
 273           (node[0] == ones ||
 274            node[1] == ones));
 275 }
 276
 277 template<> inline
 278 Node RewriteRule<OrOne>::apply(TNode node) {
 279   Unreachable();
 280   Debug("bv-rewrite") << "RewriteRule<OrOne>(" << node << ")" << std::endl;
 281   return utils::mkOnes(utils::getSize(node));
 282 }
 283
 284
 285 /**
 286  * XorDuplicate
 287  *
 288  * (a bvxor a) ==> 0
 289  */
 290
 291 template<> inline
 292 bool RewriteRule<XorDuplicate>::applies(TNode node) {
 293   Unreachable();
 294   return (node.getKind() == kind::BITVECTOR_XOR &&
 295           node.getNumChildren() == 2 &&
 296           node[0] == node[1]);
 297 }
 298
 299 template<> inline
 300 Node RewriteRule<XorDuplicate>::apply(TNode node) {
 301   Unreachable();
 302   Debug("bv-rewrite") << "RewriteRule<XorDuplicate>(" << node << ")" << std::endl;
 303   return utils::mkConst(BitVector(utils::getSize(node), Integer(0)));
 304 }
 305
 306 /**
 307  * XorOne
 308  *
 309  * (a bvxor 1) ==> ~a
 310  */
 311
 312 template<> inline
 313 bool RewriteRule<XorOne>::applies(TNode node) {
 314   if (node.getKind() != kind::BITVECTOR_XOR) {
 315     return false;
 316   }
 317   Node ones = utils::mkOnes(utils::getSize(node));
 318   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
 319     if (node[i] == ones) {
 320       return true;
 321     }
 322   }
 323   return false;
 324 }
 325
 326 template<> inline
 327 Node RewriteRule<XorOne>::apply(TNode node) {
 328   Debug("bv-rewrite") << "RewriteRule<XorOne>(" << node << ")" << std::endl;
 329   Node ones = utils::mkOnes(utils::getSize(node));
 330   std::vector<Node> children;
 331   bool found_ones = false;
 332   // XorSimplify should have been called before
 333   for(unsigned i = 0; i < node.getNumChildren(); ++i) {
 334     if (node[i] == ones) {
 335       // make sure only ones occurs only once
 336       found_ones = !found_ones;
 337     } else {
 338       children.push_back(node[i]);
 339     }
 340   }
 341
 342   Node result = utils::mkNode(kind::BITVECTOR_XOR, children);
 343   if (found_ones) {
 344     result = utils::mkNode(kind::BITVECTOR_NOT, result);
 345   }
 346   return result;
 347 }
 348
 349
 350 /**
 351  * XorZero
 352  *
 353  * (a bvxor 0) ==> a
 354  */
 355
 356 template<> inline
 357 bool RewriteRule<XorZero>::applies(TNode node) {
 358   if (node.getKind() != kind::BITVECTOR_XOR) {
 359     return false;
 360   }
 361   Node zero = utils::mkConst(utils::getSize(node), 0);
 362   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
 363     if (node[i] == zero) {
 364       return true;
 365     }
 366   }
 367   return false;
 368 }
 369
 370 template<> inline
 371 Node RewriteRule<XorZero>::apply(TNode node) {
 372   Debug("bv-rewrite") << "RewriteRule<XorZero>(" << node << ")" << std::endl;
 373   std::vector<Node> children;
 374   Node zero = utils::mkConst(utils::getSize(node), 0);
 375
 376   // XorSimplify should have been called before
 377   for(unsigned i = 0; i < node.getNumChildren(); ++i) {
 378     if (node[i] != zero) {
 379       children.push_back(node[i]);
 380     }
 381   }
 382   Node res = utils::mkNode(kind::BITVECTOR_XOR, children);
 383   return res;
 384 }
 385
 386
 387 /**
 388  * BitwiseNotAnd
 389  *
 390  * (a bvand (~ a)) ==> 0
 391  */
 392
 393 template<> inline
 394 bool RewriteRule<BitwiseNotAnd>::applies(TNode node) {
 395   Unreachable();
 396   return (node.getKind() == kind::BITVECTOR_AND &&
 397           node.getNumChildren() == 2 &&
 398           ((node[0].getKind() == kind::BITVECTOR_NOT && node[0][0] == node[1]) ||
 399            (node[1].getKind() == kind::BITVECTOR_NOT && node[1][0] == node[0])));
 400 }
 401
 402 template<> inline
 403 Node RewriteRule<BitwiseNotAnd>::apply(TNode node) {
 404   Unreachable();
 405   Debug("bv-rewrite") << "RewriteRule<BitwiseNegAnd>(" << node << ")" << std::endl;
 406   return utils::mkConst(BitVector(utils::getSize(node), Integer(0)));
 407 }
 408
 409 /**
 410  * BitwiseNegOr
 411  *
 412  * (a bvor (~ a)) ==> 1
 413  */
 414
 415 template<> inline
 416 bool RewriteRule<BitwiseNotOr>::applies(TNode node) {
 417   Unreachable();
 418   return (node.getKind() == kind::BITVECTOR_OR &&
 419           node.getNumChildren() == 2 &&
 420           ((node[0].getKind() == kind::BITVECTOR_NOT && node[0][0] == node[1]) ||
 421            (node[1].getKind() == kind::BITVECTOR_NOT && node[1][0] == node[0])));
 422 }
 423
 424 template<> inline
 425 Node RewriteRule<BitwiseNotOr>::apply(TNode node) {
 426   Unreachable();
 427   Debug("bv-rewrite") << "RewriteRule<BitwiseNotOr>(" << node << ")" << std::endl;
 428   uint32_t size = utils::getSize(node);
 429   Integer ones = Integer(1).multiplyByPow2(size) - 1;
 430   return utils::mkConst(BitVector(size, ones));
 431 }
 432
 433 /**
 434  * XorNot
 435  *
 436  * ((~ a) bvxor (~ b)) ==> (a bvxor b)
 437  */
 438
 439 template<> inline
 440 bool RewriteRule<XorNot>::applies(TNode node) {
 441   Unreachable();
 442 }
 443
 444 template<> inline
 445 Node RewriteRule<XorNot>::apply(TNode node) {
 446   Unreachable();
 447   Debug("bv-rewrite") << "RewriteRule<XorNot>(" << node << ")" << std::endl;
 448   Node a = node[0][0];
 449   Node b = node[1][0];
 450   return utils::mkNode(kind::BITVECTOR_XOR, a, b);
 451 }
 452
 453 /**
 454  * NotXor
 455  *
 456  * ~(a bvxor b) ==> (~ a bvxor b)
 457  */
 458
 459 template<> inline
 460 bool RewriteRule<NotXor>::applies(TNode node) {
 461   return (node.getKind() == kind::BITVECTOR_NOT &&
 462           node[0].getKind() == kind::BITVECTOR_XOR);
 463 }
 464
 465 template<> inline
 466 Node RewriteRule<NotXor>::apply(TNode node) {
 467   Debug("bv-rewrite") << "RewriteRule<NotXor>(" << node << ")" << std::endl;
 468   std::vector<Node> children;
 469   TNode::iterator child_it = node[0].begin();
 470   children.push_back(utils::mkNode(kind::BITVECTOR_NOT, *child_it));
 471   for(++child_it; child_it != node[0].end(); ++child_it) {
 472     children.push_back(*child_it);
 473   }
 474   return utils::mkSortedNode(kind::BITVECTOR_XOR, children);
 475 }
 476
 477 /**
 478  * NotIdemp
 479  *
 480  * ~ (~ a) ==> a
 481  */
 482
 483 template<> inline
 484 bool RewriteRule<NotIdemp>::applies(TNode node) {
 485   return (node.getKind() == kind::BITVECTOR_NOT &&
 486           node[0].getKind() == kind::BITVECTOR_NOT);
 487 }
 488
 489 template<> inline
 490 Node RewriteRule<NotIdemp>::apply(TNode node) {
 491   Debug("bv-rewrite") << "RewriteRule<NotIdemp>(" << node << ")" << std::endl;
 492   return node[0][0];
 493 }
 494
 495
 496
 497 /**
 498  * LtSelf
 499  *
 500  * a < a ==> false
 501  */
 502
 503 template<> inline
 504 bool RewriteRule<LtSelf>::applies(TNode node) {
 505   return ((node.getKind() == kind::BITVECTOR_ULT ||
 506            node.getKind() == kind::BITVECTOR_SLT) &&
 507           node[0] == node[1]);
 508 }
 509
 510 template<> inline
 511 Node RewriteRule<LtSelf>::apply(TNode node) {
 512   Debug("bv-rewrite") << "RewriteRule<LtSelf>(" << node << ")" << std::endl;
 513   return utils::mkFalse();
 514 }
 515
 516 /**
 517  * LteSelf
 518  *
 519  * a <= a ==> true
 520  */
 521
 522 template<> inline
 523 bool RewriteRule<LteSelf>::applies(TNode node) {
 524   return ((node.getKind() == kind::BITVECTOR_ULE ||
 525            node.getKind() == kind::BITVECTOR_SLE) &&
 526           node[0] == node[1]);
 527 }
 528
 529 template<> inline
 530 Node RewriteRule<LteSelf>::apply(TNode node) {
 531   Debug("bv-rewrite") << "RewriteRule<LteSelf>(" << node << ")" << std::endl;
 532   return utils::mkTrue();
 533 }
 534
 535 /**
 536  * ZeroUlt
 537  *
 538  * 0 < a ==> a != 0
 539  */
 540
 541 template<> inline
 542 bool RewriteRule<ZeroUlt>::applies(TNode node) {
 543   return (node.getKind() == kind::BITVECTOR_ULT &&
 544           node[0] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0))));
 545 }
 546
 547 template<> inline
 548 Node RewriteRule<ZeroUlt>::apply(TNode node) {
 549   Debug("bv-rewrite") << "RewriteRule<ZeroUlt>(" << node << ")" << std::endl;
 550   return utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, node[0], node[1]));
 551 }
 552
 553
 554 /**
 555  * UltZero
 556  *
 557  * a < 0 ==> false
 558  */
 559
 560 template<> inline
 561 bool RewriteRule<UltZero>::applies(TNode node) {
 562   return (node.getKind() == kind::BITVECTOR_ULT &&
 563           node[1] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0))));
 564 }
 565
 566 template<> inline
 567 Node RewriteRule<UltZero>::apply(TNode node) {
 568   Debug("bv-rewrite") << "RewriteRule<UltZero>(" << node << ")" << std::endl;
 569   return utils::mkFalse();
 570 }
 571
 572
 573 /**
 574  *
 575  */
 576 template<> inline
 577 bool RewriteRule<UltOne>::applies(TNode node) {
 578   return (node.getKind() == kind::BITVECTOR_ULT &&
 579           node[1] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(1))));
 580 }
 581
 582 template<> inline
 583 Node RewriteRule<UltOne>::apply(TNode node) {
 584   Debug("bv-rewrite") << "RewriteRule<UltOne>(" << node << ")" << std::endl;
 585   return utils::mkNode(kind::EQUAL, node[0], utils::mkConst(BitVector(utils::getSize(node[0]), 0u)));
 586 }
 587
 588 /**
 589  *
 590  */
 591 template<> inline
 592 bool RewriteRule<SltZero>::applies(TNode node) {
 593   return (node.getKind() == kind::BITVECTOR_SLT &&
 594           node[1] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0))));
 595 }
 596
 597 template<> inline
 598 Node RewriteRule<SltZero>::apply(TNode node) {
 599   Debug("bv-rewrite") << "RewriteRule<UltZero>(" << node << ")" << std::endl;
 600   unsigned size = utils::getSize(node[0]);
 601   Node most_significant_bit = utils::mkExtract(node[0], size - 1, size - 1);
 602   Node one = utils::mkConst(BitVector(1, 1u));
 603
 604   return utils::mkNode(kind::EQUAL, most_significant_bit, one);
 605 }
 606
 607
 608 /**
 609  * UltSelf
 610  *
 611  * a < a ==> false
 612  */
 613
 614 template<> inline
 615 bool RewriteRule<UltSelf>::applies(TNode node) {
 616   return (node.getKind() == kind::BITVECTOR_ULT &&
 617           node[1] == node[0]);
 618 }
 619
 620 template<> inline
 621 Node RewriteRule<UltSelf>::apply(TNode node) {
 622   Debug("bv-rewrite") << "RewriteRule<UltSelf>(" << node << ")" << std::endl;
 623   return utils::mkFalse();
 624 }
 625
 626
 627 /**
 628  * UleZero
 629  *
 630  * a <= 0 ==> a = 0
 631  */
 632
 633 template<> inline
 634 bool RewriteRule<UleZero>::applies(TNode node) {
 635   return (node.getKind() == kind::BITVECTOR_ULE &&
 636           node[1] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0))));
 637 }
 638
 639 template<> inline
 640 Node RewriteRule<UleZero>::apply(TNode node) {
 641   Debug("bv-rewrite") << "RewriteRule<UleZero>(" << node << ")" << std::endl;
 642   return utils::mkNode(kind::EQUAL, node[0], node[1]);
 643 }
 644
 645 /**
 646  * UleSelf
 647  *
 648  * a <= a ==> true
 649  */
 650
 651 template<> inline
 652 bool RewriteRule<UleSelf>::applies(TNode node) {
 653   return (node.getKind() == kind::BITVECTOR_ULE &&
 654           node[1] == node[0]);
 655 }
 656
 657 template<> inline
 658 Node RewriteRule<UleSelf>::apply(TNode node) {
 659   Debug("bv-rewrite") << "RewriteRule<UleSelf>(" << node << ")" << std::endl;
 660   return utils::mkTrue();
 661 }
 662
 663
 664 /**
 665  * ZeroUle
 666  *
 667  * 0 <= a ==> true
 668  */
 669
 670 template<> inline
 671 bool RewriteRule<ZeroUle>::applies(TNode node) {
 672   return (node.getKind() == kind::BITVECTOR_ULE &&
 673           node[0] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0))));
 674 }
 675
 676 template<> inline
 677 Node RewriteRule<ZeroUle>::apply(TNode node) {
 678   Debug("bv-rewrite") << "RewriteRule<ZeroUle>(" << node << ")" << std::endl;
 679   return utils::mkTrue();
 680 }
 681
 682 /**
 683  * UleMax
 684  *
 685  * a <= 11..1 ==> true
 686  */
 687
 688 template<> inline
 689 bool RewriteRule<UleMax>::applies(TNode node) {
 690   if (node.getKind()!= kind::BITVECTOR_ULE) {
 691     return false;
 692   }
 693   uint32_t size = utils::getSize(node[0]);
 694   Integer ones = Integer(1).multiplyByPow2(size) -1;
 695   return (node.getKind() == kind::BITVECTOR_ULE &&
 696           node[1] == utils::mkConst(BitVector(size, ones)));
 697 }
 698
 699 template<> inline
 700 Node RewriteRule<UleMax>::apply(TNode node) {
 701   Debug("bv-rewrite") << "RewriteRule<UleMax>(" << node << ")" << std::endl;
 702   return utils::mkTrue();
 703 }
 704
 705 /**
 706  * NotUlt
 707  *
 708  * ~ ( a < b) ==> b <= a
 709  */
 710
 711 template<> inline
 712 bool RewriteRule<NotUlt>::applies(TNode node) {
 713   return (node.getKind() == kind::NOT &&
 714           node[0].getKind() == kind::BITVECTOR_ULT);
 715 }
 716
 717 template<> inline
 718 Node RewriteRule<NotUlt>::apply(TNode node) {
 719   Debug("bv-rewrite") << "RewriteRule<NotUlt>(" << node << ")" << std::endl;
 720   Node ult = node[0];
 721   Node a = ult[0];
 722   Node b = ult[1];
 723   return utils::mkNode(kind::BITVECTOR_ULE, b, a);
 724 }
 725
 726 /**
 727  * NotUle
 728  *
 729  * ~ ( a <= b) ==> b < a
 730  */
 731
 732 template<> inline
 733 bool RewriteRule<NotUle>::applies(TNode node) {
 734   return (node.getKind() == kind::NOT &&
 735           node[0].getKind() == kind::BITVECTOR_ULE);
 736 }
 737
 738 template<> inline
 739 Node RewriteRule<NotUle>::apply(TNode node) {
 740   Debug("bv-rewrite") << "RewriteRule<NotUle>(" << node << ")" << std::endl;
 741   Node ult = node[0];
 742   Node a = ult[0];
 743   Node b = ult[1];
 744   return utils::mkNode(kind::BITVECTOR_ULT, b, a);
 745 }
 746
 747 /**
 748  * MultPow2
 749  *
 750  * (a * 2^k) ==> a[n-k-1:0] 0_k
 751  */
 752
 753 template<> inline
 754 bool RewriteRule<MultPow2>::applies(TNode node) {
 755   if (node.getKind() != kind::BITVECTOR_MULT)
 756     return false;
 757
 758   for(unsigned i = 0; i < node.getNumChildren(); ++i) {
 759     if (utils::isPow2Const(node[i])) {
 760       return true;
 761     }
 762   }
 763   return false;
 764 }
 765
 766 template<> inline
 767 Node RewriteRule<MultPow2>::apply(TNode node) {
 768   Debug("bv-rewrite") << "RewriteRule<MultPow2>(" << node << ")" << std::endl;
 769
 770   std::vector<Node>  children;
 771   unsigned exponent = 0;
 772   for(unsigned i = 0; i < node.getNumChildren(); ++i) {
 773     unsigned exp = utils::isPow2Const(node[i]);
 774     if (exp) {
 775       exponent += exp - 1;
 776     }
 777     else {
 778       children.push_back(node[i]);
 779     }
 780   }
 781
 782   Node a = utils::mkNode(kind::BITVECTOR_MULT, children);
 783
 784   Node extract = utils::mkExtract(a, utils::getSize(node) - exponent - 1, 0);
 785   Node zeros = utils::mkConst(exponent, 0);
 786   return utils::mkConcat(extract, zeros);
 787 }
 788
 789 /**
 790  * ExtractMultLeadingBit
 791  *
 792  * If the bit-vectors multiplied have enough leading zeros,
 793  * we can determine that the top bits of the multiplication
 794  * are zero and not compute them. Only apply for large bitwidths
 795  * as this can interfere with other mult normalization rewrites such
 796  * as flattening.
 797  */
 798
 799 template<> inline
 800 bool RewriteRule<ExtractMultLeadingBit>::applies(TNode node) {
 801   if (node.getKind() != kind::BITVECTOR_EXTRACT)
 802     return false;
 803   unsigned low = utils::getExtractLow(node);
 804   node = node[0];
 805
 806   if (node.getKind() != kind::BITVECTOR_MULT ||
 807       node.getNumChildren() != 2 ||
 808       utils::getSize(node) <= 64)
 809     return false;
 810
 811   if (node[0].getKind() != kind::BITVECTOR_CONCAT ||
 812       node[1].getKind() != kind::BITVECTOR_CONCAT ||
 813       !node[0][0].isConst() ||
 814       !node[1][0].isConst())
 815     return false;
 816
 817   unsigned n = utils::getSize(node);
 818   // count number of leading zeroes
 819   const Integer& int1 = node[0][0].getConst<BitVector>().toInteger();
 820   const Integer& int2 = node[1][0].getConst<BitVector>().toInteger();
 821   unsigned zeroes1 = int1.isZero()? utils::getSize(node[0][0]) :
 822                                     int1.length();
 823
 824   unsigned zeroes2 = int2.isZero()? utils::getSize(node[1][0]) :
 825                                     int2.length();
 826
 827   // first k bits are not zero in the result
 828   unsigned k = 2 * n - (zeroes1 + zeroes2);
 829
 830   if (k > low)
 831     return false;
 832
 833   return true;
 834 }
 835
 836 template<> inline
 837 Node RewriteRule<ExtractMultLeadingBit>::apply(TNode node) {
 838   Debug("bv-rewrite") << "RewriteRule<MultLeadingBit>(" << node << ")" << std::endl;
 839
 840   unsigned bitwidth = utils::getSize(node);
 841
 842   // node = node[0];
 843   // const Integer& int1 = node[0][0].getConst<BitVector>().toInteger();
 844   // const Integer& int2 = node[1][0].getConst<BitVector>().toInteger();
 845   // unsigned zeroes1 = int1.isZero()? utils::getSize(node[0][0]) :
 846   //                                   int1.length();
 847
 848   // unsigned zeroes2 = int2.isZero()? utils::getSize(node[1][0]) :
 849   //                                   int2.length();
 850   // all bits >= k in the multiplier will have to be 0
 851   // unsigned n = utils::getSize(node);
 852   // unsigned k = 2 * n - (zeroes1 + zeroes2);
 853   // Node extract1 = utils::mkExtract(node[0], k - 1, 0);
 854   // Node extract2 = utils::mkExtract(node[1], k - 1, 0);
 855   // Node k_zeroes = utils::mkConst(n - k, 0u);
 856
 857   // Node new_mult = utils::mkNode(kind::BITVECTOR_MULT, extract1, extract2);
 858   // Node result = utils::mkExtract(utils::mkNode(kind::BITVECTOR_CONCAT, k_zeroes, new_mult),
 859   //                                high, low);
 860
 861   // since the extract is over multiplier bits that have to be 0, return 0
 862   Node result = utils::mkConst(bitwidth, 0u);
 863   //  std::cout << "MultLeadingBit " << node <<" => " << result <<"\n";
 864   return result;
 865 }
 866
 867 /**
 868  * NegIdemp
 869  *
 870  * -(-a) ==> a
 871  */
 872
 873 template<> inline
 874 bool RewriteRule<NegIdemp>::applies(TNode node) {
 875   return (node.getKind() == kind::BITVECTOR_NEG &&
 876           node[0].getKind() == kind::BITVECTOR_NEG);
 877 }
 878
 879 template<> inline
 880 Node RewriteRule<NegIdemp>::apply(TNode node) {
 881   Debug("bv-rewrite") << "RewriteRule<NegIdemp>(" << node << ")" << std::endl;
 882   return node[0][0];
 883 }
 884
 885 /**
 886  * UdivPow2
 887  *
 888  * (a udiv 2^k) ==> 0_k a[n-1: k]
 889  */
 890
 891 template<> inline
 892 bool RewriteRule<UdivPow2>::applies(TNode node) {
 893   return (node.getKind() == kind::BITVECTOR_UDIV_TOTAL &&
 894           utils::isPow2Const(node[1]));
 895 }
 896
 897 template<> inline
 898 Node RewriteRule<UdivPow2>::apply(TNode node) {
 899   Debug("bv-rewrite") << "RewriteRule<UdivPow2>(" << node << ")" << std::endl;
 900   Node a = node[0];
 901   unsigned power = utils::isPow2Const(node[1]) -1;
 902   if (power == 0) {
 903     return a;
 904   }
 905   Node extract = utils::mkExtract(a, utils::getSize(node) - 1, power);
 906   Node zeros = utils::mkConst(power, 0);
 907
 908   return utils::mkNode(kind::BITVECTOR_CONCAT, zeros, extract);
 909 }
 910
 911 /**
 912  * UdivOne
 913  *
 914  * (a udiv 1) ==> a
 915  */
 916
 917 template<> inline
 918 bool RewriteRule<UdivOne>::applies(TNode node) {
 919   return (node.getKind() == kind::BITVECTOR_UDIV_TOTAL &&
 920           node[1] == utils::mkConst(utils::getSize(node), 1));
 921 }
 922
 923 template<> inline
 924 Node RewriteRule<UdivOne>::apply(TNode node) {
 925   Debug("bv-rewrite") << "RewriteRule<UdivOne>(" << node << ")" << std::endl;
 926   return node[0];
 927 }
 928
 929 /**
 930  * UdivSelf
 931  *
 932  * (a udiv a) ==> 1
 933  */
 934
 935 template<> inline
 936 bool RewriteRule<UdivSelf>::applies(TNode node) {
 937   return (node.getKind() == kind::BITVECTOR_UDIV_TOTAL &&
 938           node[0] == node[1]);
 939 }
 940
 941 template<> inline
 942 Node RewriteRule<UdivSelf>::apply(TNode node) {
 943   Debug("bv-rewrite") << "RewriteRule<UdivSelf>(" << node << ")" << std::endl;
 944   return utils::mkConst(utils::getSize(node), 1);
 945 }
 946
 947 /**
 948  * UremPow2
 949  *
 950  * (a urem 2^k) ==> 0_(n-k) a[k-1:0]
 951  */
 952
 953 template<> inline
 954 bool RewriteRule<UremPow2>::applies(TNode node) {
 955   return (node.getKind() == kind::BITVECTOR_UREM_TOTAL &&
 956           utils::isPow2Const(node[1]));
 957 }
 958
 959 template<> inline
 960 Node RewriteRule<UremPow2>::apply(TNode node) {
 961   Debug("bv-rewrite") << "RewriteRule<UremPow2>(" << node << ")" << std::endl;
 962   TNode a = node[0];
 963   unsigned power = utils::isPow2Const(node[1]) - 1;
 964   if (power == 0) {
 965     return utils::mkConst(utils::getSize(node), 0);
 966   }
 967   Node extract = utils::mkExtract(a, power - 1, 0);
 968   Node zeros = utils::mkConst(utils::getSize(node) - power, 0);
 969   return utils::mkNode(kind::BITVECTOR_CONCAT, zeros, extract);
 970 }
 971
 972 /**
 973  * UremOne
 974  *
 975  * (a urem 1) ==> 0
 976  */
 977
 978 template<> inline
 979 bool RewriteRule<UremOne>::applies(TNode node) {
 980   return (node.getKind() == kind::BITVECTOR_UREM_TOTAL &&
 981           node[1] == utils::mkConst(utils::getSize(node), 1));
 982 }
 983
 984 template<> inline
 985 Node RewriteRule<UremOne>::apply(TNode node) {
 986   Debug("bv-rewrite") << "RewriteRule<UremOne>(" << node << ")" << std::endl;
 987   return utils::mkConst(utils::getSize(node), 0);
 988 }
 989
 990 /**
 991  * UremSelf
 992  *
 993  * (a urem a) ==> 0
 994  */
 995
 996 template<> inline
 997 bool RewriteRule<UremSelf>::applies(TNode node) {
 998   return (node.getKind() == kind::BITVECTOR_UREM_TOTAL &&
 999           node[0] == node[1]);
1000 }
1001
1002 template<> inline
1003 Node RewriteRule<UremSelf>::apply(TNode node) {
1004   Debug("bv-rewrite") << "RewriteRule<UremSelf>(" << node << ")" << std::endl;
1005   return utils::mkConst(utils::getSize(node), 0);
1006 }
1007
1008 /**
1009  * ShiftZero
1010  *
1011  * (0_k >> a) ==> 0_k
1012  */
1013
1014 template<> inline
1015 bool RewriteRule<ShiftZero>::applies(TNode node) {
1016   return ((node.getKind() == kind::BITVECTOR_SHL ||
1017            node.getKind() == kind::BITVECTOR_LSHR ||
1018            node.getKind() == kind::BITVECTOR_ASHR) &&
1019           node[0] == utils::mkConst(utils::getSize(node), 0));
1020 }
1021
1022 template<> inline
1023 Node RewriteRule<ShiftZero>::apply(TNode node) {
1024   Debug("bv-rewrite") << "RewriteRule<ShiftZero>(" << node << ")" << std::endl;
1025   return node[0];
1026 }
1027
1028 /**
1029  * BBPlusNeg
1030  *
1031  * -a1 - a2 - ... - an + ak + ..  ==> - (a1 + a2 + ... + an) + ak
1032  *
1033  */
1034
1035 template<> inline
1036 bool RewriteRule<BBPlusNeg>::applies(TNode node) {
1037   if (node.getKind() != kind::BITVECTOR_PLUS) {
1038     return false;
1039   }
1040
1041   unsigned neg_count = 0;
1042   for(unsigned i = 0; i < node.getNumChildren(); ++i) {
1043     if (node[i].getKind()== kind::BITVECTOR_NEG) {
1044       ++neg_count;
1045     }
1046   }
1047   return neg_count > 1;
1048 }
1049
1050 template<> inline
1051 Node RewriteRule<BBPlusNeg>::apply(TNode node) {
1052   Debug("bv-rewrite") << "RewriteRule<BBPlusNeg>(" << node << ")" << std::endl;
1053
1054   std::vector<Node> children;
1055   unsigned neg_count = 0;
1056   for(unsigned i = 0; i < node.getNumChildren(); ++i) {
1057     if (node[i].getKind() == kind::BITVECTOR_NEG) {
1058       ++neg_count;
1059       children.push_back(utils::mkNode(kind::BITVECTOR_NOT, node[i][0]));
1060     } else {
1061       children.push_back(node[i]);
1062     }
1063   }
1064   Assert(neg_count!= 0);
1065   children.push_back(utils::mkConst(utils::getSize(node), neg_count));
1066
1067   return utils::mkNode(kind::BITVECTOR_PLUS, children);
1068 }
1069
1070 template<> inline
1071 bool RewriteRule<MergeSignExtend>::applies(TNode node) {
1072   if (node.getKind() != kind::BITVECTOR_SIGN_EXTEND ||
1073       (node[0].getKind() != kind::BITVECTOR_SIGN_EXTEND &&
1074        node[0].getKind() != kind::BITVECTOR_ZERO_EXTEND))
1075     return false;
1076   return true;
1077 }
1078
1079 template<> inline
1080 Node RewriteRule<MergeSignExtend>::apply(TNode node) {
1081   Debug("bv-rewrite") << "RewriteRule<MergeSignExtend>(" << node << ")" << std::endl;
1082   unsigned ammount1 = node.getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
1083
1084   NodeManager* nm = NodeManager::currentNM();
1085   if (node[0].getKind() == kind::BITVECTOR_ZERO_EXTEND) {
1086     unsigned ammount2 = node[0].getOperator().getConst<BitVectorZeroExtend>().zeroExtendAmount;
1087     if (ammount2 == 0) {
1088       NodeBuilder<> nb(kind::BITVECTOR_SIGN_EXTEND);
1089       Node op = nm->mkConst<BitVectorSignExtend>(BitVectorSignExtend(ammount1));
1090       nb << op << node[0][0];
1091       Node res = nb;
1092       return res;
1093     }
1094     NodeBuilder<> nb(kind::BITVECTOR_ZERO_EXTEND);
1095     Node op = nm->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(ammount1 + ammount2));
1096     nb << op << node[0][0];
1097     Node res = nb;
1098     return res;
1099   }
1100   Assert (node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND);
1101   unsigned ammount2 = node[0].getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
1102   NodeBuilder<> nb(kind::BITVECTOR_SIGN_EXTEND);
1103   Node op = nm->mkConst<BitVectorSignExtend>(BitVectorSignExtend(ammount1+ ammount2));
1104   nb << op << node[0][0];
1105   Node res = nb;
1106   return res;
1107 }
1108
1109
1110 template<> inline
1111 bool RewriteRule<MultSlice>::applies(TNode node) {
1112   if (node.getKind() != kind::BITVECTOR_MULT) {
1113     return false;
1114   }
1115   if (utils::getSize(node[0]) % 2 != 0) {
1116     return false;
1117   }
1118   return true;
1119 }
1120
1121 /**
1122  * Expressses the multiplication in terms of the top and bottom
1123  * slices of the terms. Note increases circuit size, but could
1124  * lead to simplifications (use wisely!).
1125  *
1126  * @param node
1127  *
1128  * @return
1129  */
1130 template<> inline
1131 Node RewriteRule<MultSlice>::apply(TNode node) {
1132   Debug("bv-rewrite") << "RewriteRule<MultSlice>(" << node << ")" << std::endl;
1133   unsigned bitwidth = utils::getSize(node[0]);
1134   Node zeros = utils::mkConst(bitwidth/2, 0);
1135   TNode a = node[0];
1136   Node bottom_a = utils::mkExtract(a, bitwidth/2 - 1, 0);
1137   Node top_a = utils::mkExtract(a, bitwidth -1, bitwidth/2);
1138   TNode b = node[1];
1139   Node bottom_b = utils::mkExtract(b, bitwidth/2 - 1, 0);
1140   Node top_b = utils::mkExtract(b, bitwidth -1, bitwidth/2);
1141
1142   Node term1 = utils::mkNode(kind::BITVECTOR_MULT,
1143                              utils::mkNode(kind::BITVECTOR_CONCAT, zeros, bottom_a),
1144                              utils::mkNode(kind::BITVECTOR_CONCAT, zeros, bottom_b));
1145
1146   Node term2 = utils::mkNode(kind::BITVECTOR_CONCAT,
1147                              utils::mkNode(kind::BITVECTOR_MULT, top_b, bottom_a),
1148                              zeros);
1149   Node term3 = utils::mkNode(kind::BITVECTOR_CONCAT,
1150                              utils::mkNode(kind::BITVECTOR_MULT, top_a, bottom_b),
1151                              zeros);
1152   return utils::mkNode(kind::BITVECTOR_PLUS, term1, term2, term3);
1153 }
1154
1155 /**
1156  * x < y + 1 <=> (not y < x) and y != 1...1
1157  *
1158  * @param node
1159  *
1160  * @return
1161  */
1162 template<> inline
1163 bool RewriteRule<UltPlusOne>::applies(TNode node) {
1164   if (node.getKind() != kind::BITVECTOR_ULT) return false;
1165   TNode x = node[0];
1166   TNode y1 = node[1];
1167   if (y1.getKind() != kind::BITVECTOR_PLUS) return false;
1168   if (y1[0].getKind() != kind::CONST_BITVECTOR &&
1169       y1[1].getKind() != kind::CONST_BITVECTOR)
1170     return false;
1171
1172   if (y1[0].getKind() == kind::CONST_BITVECTOR &&
1173       y1[1].getKind() == kind::CONST_BITVECTOR)
1174     return false;
1175
1176   if (y1.getNumChildren() != 2)
1177     return false;
1178
1179   TNode one = y1[0].getKind() == kind::CONST_BITVECTOR ? y1[0] : y1[1];
1180   if (one != utils::mkConst(utils::getSize(one), 1)) return false;
1181   return true;
1182 }
1183
1184 template<> inline
1185 Node RewriteRule<UltPlusOne>::apply(TNode node) {
1186   Debug("bv-rewrite") << "RewriteRule<UltPlusOne>(" << node << ")" << std::endl;
1187   TNode x = node[0];
1188   TNode y1 = node[1];
1189   TNode y = y1[0].getKind() != kind::CONST_BITVECTOR ? y1[0] : y1[1];
1190   unsigned size = utils::getSize(x);
1191   Node not_y_eq_1 = utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, y, utils::mkOnes(size)));
1192   Node not_y_lt_x = utils::mkNode(kind::NOT, utils::mkNode(kind::BITVECTOR_ULT, y, x));
1193   return utils::mkNode(kind::AND, not_y_eq_1, not_y_lt_x);
1194 }
1195
1196 /**
1197  * x ^(x-1) = 0 => 1 << sk
1198  * WARNING: this is an **EQUISATISFIABLE** transformation!
1199  * Only to be called on top level assertions.
1200  *
1201  * @param node
1202  *
1203  * @return
1204  */
1205 template<> inline
1206 bool RewriteRule<IsPowerOfTwo>::applies(TNode node) {
1207   if (node.getKind()!= kind::EQUAL) return false;
1208   if (node[0].getKind() != kind::BITVECTOR_AND &&
1209       node[1].getKind() != kind::BITVECTOR_AND)
1210     return false;
1211   if (!utils::isZero(node[0]) &&
1212       !utils::isZero(node[1]))
1213     return false;
1214
1215   TNode t = !utils::isZero(node[0])? node[0]: node[1];
1216   if (t.getNumChildren() != 2) return false;
1217   TNode a = t[0];
1218   TNode b = t[1];
1219   unsigned size = utils::getSize(t);
1220   if(size < 2) return false;
1221   Node diff = Rewriter::rewrite(utils::mkNode(kind::BITVECTOR_SUB, a, b));
1222   return (diff.isConst() && (diff == utils::mkConst(size, 1u) || diff == utils::mkOnes(size)));
1223 }
1224
1225 template<> inline
1226 Node RewriteRule<IsPowerOfTwo>::apply(TNode node) {
1227   Debug("bv-rewrite") << "RewriteRule<IsPowerOfTwo>(" << node << ")" << std::endl;
1228   TNode term = utils::isZero(node[0])? node[1] : node[0];
1229   TNode a = term[0];
1230   TNode b = term[1];
1231   unsigned size = utils::getSize(term);
1232   Node diff = Rewriter::rewrite(utils::mkNode(kind::BITVECTOR_SUB, a, b));
1233   Assert (diff.isConst());
1234   TNode x = diff == utils::mkConst(size, 1u) ? a : b;
1235   Node one = utils::mkConst(size, 1u);
1236   Node sk = utils::mkVar(size);
1237   Node sh = utils::mkNode(kind::BITVECTOR_SHL, one, sk);
1238   Node x_eq_sh = utils::mkNode(kind::EQUAL, x, sh);
1239   return x_eq_sh;
1240 }
1241
1242
1243
1244
1245 }
1246 }
1247 }