src/theory/bv/theory_bv_rewrite_rules_normalization.h

   1 /*********************                                                        */
   2 /*! \file theory_bv_rewrite_rules_normalization.h
   3  ** \verbatim
   4  ** Original author: lianah
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   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 /**
  32  * ExtractBitwise
  33  *   (x bvop y) [i:j] ==> x[i:j] bvop y[i:j]
  34  *  where bvop is bvand,bvor, bvxor
  35  */
  36 template<> inline
  37 bool RewriteRule<ExtractBitwise>::applies(TNode node) {
  38   return (node.getKind() == kind::BITVECTOR_EXTRACT &&
  39           (node[0].getKind() == kind::BITVECTOR_AND ||
  40            node[0].getKind() == kind::BITVECTOR_OR ||
  41            node[0].getKind() == kind::BITVECTOR_XOR ));
  42 }
  43
  44 template<> inline
  45 Node RewriteRule<ExtractBitwise>::apply(TNode node) {
  46   BVDebug("bv-rewrite") << "RewriteRule<ExtractBitwise>(" << node << ")" << std::endl;
  47   unsigned high = utils::getExtractHigh(node);
  48   unsigned low = utils::getExtractLow(node);
  49   std::vector<Node> children;
  50   for (unsigned i = 0; i < node[0].getNumChildren(); ++i) {
  51     children.push_back(utils::mkExtract(node[0][i], high, low));
  52   }
  53   Kind kind = node[0].getKind();
  54   return utils::mkSortedNode(kind, children);
  55 }
  56
  57 /**
  58  * ExtractNot
  59  *
  60  *  (~ a) [i:j] ==> ~ (a[i:j])
  61  */
  62 template<> inline
  63 bool RewriteRule<ExtractNot>::applies(TNode node) {
  64   return (node.getKind() == kind::BITVECTOR_EXTRACT &&
  65           node[0].getKind() == kind::BITVECTOR_NOT);
  66 }
  67
  68 template<> inline
  69 Node RewriteRule<ExtractNot>::apply(TNode node) {
  70   BVDebug("bv-rewrite") << "RewriteRule<ExtractNot>(" << node << ")" << std::endl;
  71   unsigned low = utils::getExtractLow(node);
  72   unsigned high = utils::getExtractHigh(node);
  73   Node a = utils::mkExtract(node[0][0], high, low);
  74   return utils::mkNode(kind::BITVECTOR_NOT, a);
  75 }
  76
  77 /**
  78  * ExtractArith
  79  *
  80  * (a bvop b) [k:0] ==> (a[k:0] bvop b[k:0])
  81  */
  82
  83 template<> inline
  84 bool RewriteRule<ExtractArith>::applies(TNode node) {
  85   return (node.getKind() == kind::BITVECTOR_EXTRACT &&
  86           utils::getExtractLow(node) == 0 &&
  87           (node[0].getKind() == kind::BITVECTOR_PLUS ||
  88            node[0].getKind() == kind::BITVECTOR_MULT));
  89 }
  90
  91 template<> inline
  92 Node RewriteRule<ExtractArith>::apply(TNode node) {
  93   BVDebug("bv-rewrite") << "RewriteRule<ExtractArith>(" << node << ")" << std::endl;
  94   unsigned low = utils::getExtractLow(node);
  95   Assert (low == 0);
  96   unsigned high = utils::getExtractHigh(node);
  97   std::vector<Node> children;
  98   for (unsigned i = 0; i < node[0].getNumChildren(); ++i) {
  99     children.push_back(utils::mkExtract(node[0][i], high, low));
 100   }
 101   Kind kind = node[0].getKind();
 102   return utils::mkNode(kind, children);
 103
 104 }
 105
 106 /**
 107  * ExtractArith2
 108  *
 109  * (a bvop b) [i:j] ==> (a[i:0] bvop b[i:0]) [i:j]
 110  */
 111
 112 // careful not to apply in a loop
 113 template<> inline
 114 bool RewriteRule<ExtractArith2>::applies(TNode node) {
 115   return (node.getKind() == kind::BITVECTOR_EXTRACT &&
 116           (node[0].getKind() == kind::BITVECTOR_PLUS ||
 117            node[0].getKind() == kind::BITVECTOR_MULT));
 118 }
 119
 120 template<> inline
 121 Node RewriteRule<ExtractArith2>::apply(TNode node) {
 122   BVDebug("bv-rewrite") << "RewriteRule<ExtractArith2>(" << node << ")" << std::endl;
 123   unsigned low = utils::getExtractLow(node);
 124   unsigned high = utils::getExtractHigh(node);
 125   std::vector<Node> children;
 126   for (unsigned i = 0; i < node[0].getNumChildren(); ++i) {
 127     children.push_back(utils::mkExtract(node[0][i], high, 0));
 128   }
 129   Kind kind = node[0].getKind();
 130   Node op_children = utils::mkSortedNode(kind, children);
 131
 132   return utils::mkExtract(op_children, high, low);
 133 }
 134
 135 template<> inline
 136 bool RewriteRule<FlattenAssocCommut>::applies(TNode node) {
 137   return (node.getKind() == kind::BITVECTOR_PLUS ||
 138           node.getKind() == kind::BITVECTOR_MULT ||
 139           node.getKind() == kind::BITVECTOR_OR ||
 140           node.getKind() == kind::BITVECTOR_XOR ||
 141           node.getKind() == kind::BITVECTOR_AND);
 142 }
 143
 144
 145 template<> inline
 146 Node RewriteRule<FlattenAssocCommut>::apply(TNode node) {
 147   BVDebug("bv-rewrite") << "RewriteRule<FlattenAssocCommut>(" << node << ")" << std::endl;
 148   std::vector<Node> processingStack;
 149   processingStack.push_back(node);
 150   std::vector<Node> children;
 151   Kind kind = node.getKind();
 152
 153   while (! processingStack.empty()) {
 154     TNode current = processingStack.back();
 155     processingStack.pop_back();
 156
 157     // flatten expression
 158     if (current.getKind() == kind) {
 159       for (unsigned i = 0; i < current.getNumChildren(); ++i) {
 160         processingStack.push_back(current[i]);
 161       }
 162     } else {
 163       children.push_back(current);
 164     }
 165   }
 166   return utils::mkSortedNode(kind, children);
 167 }
 168
 169 static inline void addToCoefMap(std::map<Node, BitVector>& map,
 170                                 TNode term, const BitVector& coef) {
 171   if (map.find(term) != map.end()) {
 172     map[term] = map[term] + coef;
 173   } else {
 174     map[term] = coef;
 175   }
 176 }
 177
 178
 179 static inline void updateCoefMap(TNode current, unsigned size,
 180                                  std::map<Node, BitVector>& factorToCoefficient,
 181                                  BitVector& constSum) {
 182   // look for c * x, where c is a constant
 183   if (current.getKind() == kind::BITVECTOR_MULT &&
 184       (current[0].getKind() == kind::CONST_BITVECTOR ||
 185        current[1].getKind() == kind::CONST_BITVECTOR)) {
 186     // if we are multiplying by a constant
 187     BitVector coeff;
 188     TNode term;
 189     // figure out which part is the constant
 190     if (current[0].getKind() == kind::CONST_BITVECTOR) {
 191       coeff = current[0].getConst<BitVector>();
 192       term = current[1];
 193     } else {
 194       coeff = current[1].getConst<BitVector>();
 195       term = current[0];
 196     }
 197     if(term.getKind() == kind::BITVECTOR_SUB) {
 198       TNode a = term[0];
 199       TNode b = term[1];
 200       addToCoefMap(factorToCoefficient, a, coeff);
 201       addToCoefMap(factorToCoefficient, b, -coeff);
 202     }
 203     else if(term.getKind() == kind::BITVECTOR_NEG) {
 204       addToCoefMap(factorToCoefficient, term[0], -BitVector(size, coeff));
 205     }
 206     else {
 207       addToCoefMap(factorToCoefficient, term, coeff);
 208     }
 209   }
 210   else if (current.getKind() == kind::BITVECTOR_SUB) {
 211     // turn into a + (-1)*b
 212     addToCoefMap(factorToCoefficient, current[0], BitVector(size, (unsigned)1));
 213     addToCoefMap(factorToCoefficient, current[1], -BitVector(size, (unsigned)1));
 214   }
 215   else if (current.getKind() == kind::BITVECTOR_NEG) {
 216     addToCoefMap(factorToCoefficient, current[0], -BitVector(size, (unsigned)1));
 217   }
 218   else if (current.getKind() == kind::CONST_BITVECTOR) {
 219     BitVector constValue = current.getConst<BitVector>();
 220     constSum = constSum + constValue;
 221   }
 222   else {
 223     // store as 1 * current
 224     addToCoefMap(factorToCoefficient, current, BitVector(size, (unsigned)1));
 225   }
 226 }
 227
 228
 229 static inline void addToChildren(TNode term, unsigned size, BitVector coeff, std::vector<Node>& children) {
 230   if (coeff == BitVector(size, (unsigned)0)) {
 231     return;
 232   }
 233   else if (coeff == BitVector(size, (unsigned)1)) {
 234     children.push_back(term);
 235   }
 236   else if (coeff == -BitVector(size, (unsigned)1)) {
 237     // avoid introducing an extra multiplication
 238     children.push_back(utils::mkNode(kind::BITVECTOR_NEG, term));
 239   }
 240   else {
 241     Node coeffNode = utils::mkConst(coeff);
 242     Node product = utils::mkSortedNode(kind::BITVECTOR_MULT, coeffNode, term);
 243     children.push_back(product);
 244   }
 245 }
 246
 247
 248 template<> inline
 249 bool RewriteRule<PlusCombineLikeTerms>::applies(TNode node) {
 250   return (node.getKind() == kind::BITVECTOR_PLUS);
 251 }
 252
 253
 254 template<> inline
 255 Node RewriteRule<PlusCombineLikeTerms>::apply(TNode node) {
 256   BVDebug("bv-rewrite") << "RewriteRule<PlusCombineLikeTerms>(" << node << ")" << std::endl;
 257   unsigned size = utils::getSize(node);
 258   BitVector constSum(size, (unsigned)0);
 259   std::map<Node, BitVector> factorToCoefficient;
 260
 261   // combine like-terms
 262   for(unsigned i= 0; i < node.getNumChildren(); ++i) {
 263     TNode current = node[i];
 264     updateCoefMap(current, size, factorToCoefficient, constSum);
 265   }
 266
 267   std::vector<Node> children;
 268   if ( constSum!= BitVector(size, (unsigned)0)) {
 269     children.push_back(utils::mkConst(constSum));
 270   }
 271
 272   // construct result
 273   std::map<Node, BitVector>::const_iterator it = factorToCoefficient.begin();
 274
 275   for (; it != factorToCoefficient.end(); ++it) {
 276     addToChildren(it->first, size, it->second, children);
 277   }
 278
 279   if(children.size() == 0) {
 280     return utils::mkConst(size, (unsigned)0);
 281   }
 282
 283   return utils::mkSortedNode(kind::BITVECTOR_PLUS, children);
 284 }
 285
 286
 287 template<> inline
 288 bool RewriteRule<MultSimplify>::applies(TNode node) {
 289   return (node.getKind() == kind::BITVECTOR_MULT);
 290 }
 291
 292 template<> inline
 293 Node RewriteRule<MultSimplify>::apply(TNode node) {
 294   BVDebug("bv-rewrite") << "RewriteRule<MultSimplify>(" << node << ")" << std::endl;
 295   unsigned size = utils::getSize(node);
 296   BitVector constant(size, Integer(1));
 297
 298   std::vector<Node> children;
 299   for(unsigned i = 0; i < node.getNumChildren(); ++i) {
 300     TNode current = node[i];
 301     if (current.getKind() == kind::CONST_BITVECTOR) {
 302       BitVector value = current.getConst<BitVector>();
 303       if(value == BitVector(size, (unsigned) 0)) {
 304         return utils::mkConst(size, 0);
 305       }
 306       constant = constant * current.getConst<BitVector>();
 307     } else {
 308       children.push_back(current);
 309     }
 310   }
 311
 312
 313   if(constant != BitVector(size, (unsigned)1)) {
 314     children.push_back(utils::mkConst(constant));
 315   }
 316
 317
 318   if(children.size() == 0) {
 319     return utils::mkConst(size, (unsigned)1);
 320   }
 321
 322   return utils::mkSortedNode(kind::BITVECTOR_MULT, children);
 323 }
 324
 325 template<> inline
 326 bool RewriteRule<MultDistribConst>::applies(TNode node) {
 327   if (node.getKind() != kind::BITVECTOR_MULT)
 328     return false;
 329
 330   TNode factor;
 331   if (node[0].getKind() == kind::CONST_BITVECTOR) {
 332     factor = node[1];
 333   } else if (node[1].getKind() == kind::CONST_BITVECTOR) {
 334     factor = node[0];
 335   } else {
 336     return false;
 337   }
 338
 339   return (factor.getKind() == kind::BITVECTOR_PLUS ||
 340           factor.getKind() == kind::BITVECTOR_SUB ||
 341           factor.getKind() == kind::BITVECTOR_NEG);
 342 }
 343
 344 template<> inline
 345 Node RewriteRule<MultDistribConst>::apply(TNode node) {
 346   BVDebug("bv-rewrite") << "RewriteRule<MultDistribConst>(" << node << ")" << std::endl;
 347
 348   TNode constant;
 349   TNode factor;
 350   if (node[0].getKind() == kind::CONST_BITVECTOR) {
 351     constant = node[0];
 352     factor = node[1];
 353   } else {
 354   Assert(node[1].getKind() == kind::CONST_BITVECTOR);
 355   constant = node[1];
 356   factor = node[0];
 357   }
 358
 359   if (factor.getKind() == kind::BITVECTOR_NEG) {
 360     // push negation on the constant part
 361     BitVector const_bv = constant.getConst<BitVector>();
 362     return utils::mkSortedNode(kind::BITVECTOR_MULT,
 363                                utils::mkConst(-const_bv),
 364                                factor[0]);
 365   }
 366
 367   std::vector<Node> children;
 368   for(unsigned i = 0; i < factor.getNumChildren(); ++i) {
 369     children.push_back(utils::mkSortedNode(kind::BITVECTOR_MULT, constant, factor[i]));
 370   }
 371
 372   return utils::mkSortedNode(factor.getKind(), children);
 373
 374 }
 375
 376
 377 template<> inline
 378 bool RewriteRule<SolveEq>::applies(TNode node) {
 379   if (node.getKind() != kind::EQUAL ||
 380       (node[0].getMetaKind() == kind::metakind::VARIABLE && !node[1].hasSubterm(node[0])) ||
 381       (node[1].getMetaKind() == kind::metakind::VARIABLE && !node[0].hasSubterm(node[1]))) {
 382     return false;
 383   }
 384   return true;
 385 }
 386
 387
 388 // Doesn't do full solving (yet), instead, if a term appears both on lhs and rhs, it subtracts from both sides so that one side's coeff is zero
 389 template<> inline
 390 Node RewriteRule<SolveEq>::apply(TNode node) {
 391   BVDebug("bv-rewrite") << "RewriteRule<SolveEq>(" << node << ")" << std::endl;
 392
 393   TNode left = node[0];
 394   TNode right = node[1];
 395
 396   unsigned size = utils::getSize(left);
 397   BitVector zero(size, (unsigned)0);
 398   BitVector leftConst(size, (unsigned)0);
 399   BitVector rightConst(size, (unsigned)0);
 400   std::map<Node, BitVector> leftMap, rightMap;
 401
 402   // Collect terms and coefficients plus constant for left
 403   if (left.getKind() == kind::BITVECTOR_PLUS) {
 404     for(unsigned i= 0; i < left.getNumChildren(); ++i) {
 405       updateCoefMap(left[i], size, leftMap, leftConst);
 406     }
 407   }
 408   else {
 409     updateCoefMap(left, size, leftMap, leftConst);
 410   }
 411
 412   // Collect terms and coefficients plus constant for right
 413   if (right.getKind() == kind::BITVECTOR_PLUS) {
 414     for(unsigned i= 0; i < right.getNumChildren(); ++i) {
 415       updateCoefMap(right[i], size, rightMap, rightConst);
 416     }
 417   }
 418   else {
 419     updateCoefMap(right, size, rightMap, rightConst);
 420   }
 421
 422   std::vector<Node> childrenLeft, childrenRight;
 423
 424   // If both constants are nonzero, combine on right, otherwise leave them where they are
 425   if (rightConst != zero) {
 426     rightConst = rightConst - leftConst;
 427     childrenRight.push_back(utils::mkConst(rightConst));
 428   }
 429   else if (leftConst != zero) {
 430     childrenLeft.push_back(utils::mkConst(leftConst));
 431   }
 432
 433   std::map<Node, BitVector>::const_iterator iLeft = leftMap.begin(), iLeftEnd = leftMap.end();
 434   std::map<Node, BitVector>::const_iterator iRight = rightMap.begin(), iRightEnd = rightMap.end();
 435
 436   BitVector coeffLeft;
 437   TNode termLeft;
 438   if (iLeft != iLeftEnd) {
 439     coeffLeft = iLeft->second;
 440     termLeft = iLeft->first;
 441   }
 442
 443   BitVector coeffRight;
 444   TNode termRight;
 445   if (iRight != iRightEnd) {
 446     coeffRight = iRight->second;
 447     termRight = iRight->first;
 448   }
 449
 450   bool incLeft, incRight;
 451
 452   while (iLeft != iLeftEnd || iRight != iRightEnd) {
 453     incLeft = incRight = false;
 454     if (iLeft != iLeftEnd && (iRight == iRightEnd || termLeft < termRight)) {
 455       addToChildren(termLeft, size, coeffLeft, childrenLeft);
 456       incLeft = true;
 457     }
 458     else if (iLeft == iLeftEnd || termRight < termLeft) {
 459       Assert(iRight != iRightEnd);
 460       addToChildren(termRight, size, coeffRight, childrenRight);
 461       incRight = true;
 462     }
 463     else {
 464       if (coeffLeft > coeffRight) {
 465         addToChildren(termLeft, size, coeffLeft - coeffRight, childrenLeft);
 466       }
 467       else if (coeffRight > coeffLeft) {
 468         addToChildren(termRight, size, coeffRight - coeffLeft, childrenRight);
 469       }
 470       incLeft = incRight = true;
 471     }
 472     if (incLeft) {
 473       ++iLeft;
 474       if (iLeft != iLeftEnd) {
 475         coeffLeft = iLeft->second;
 476         termLeft = iLeft->first;
 477       }
 478     }
 479     if (incRight) {
 480       ++iRight;
 481       if (iRight != iRightEnd) {
 482         coeffRight = iRight->second;
 483         termRight = iRight->first;
 484       }
 485     }
 486   }
 487
 488   // construct result
 489
 490   Node newLeft, newRight;
 491
 492   if(childrenRight.size() == 0 && leftConst != zero) {
 493     Assert(childrenLeft[0].isConst() && childrenLeft[0].getConst<BitVector>() == leftConst);
 494     if (childrenLeft.size() == 1) {
 495       // c = 0 ==> false
 496       return utils::mkFalse();
 497     }
 498     // special case - if right is empty and left has a constant, move the constant
 499     // TODO: this is inefficient - would be better if constant were at the end in the normal form
 500     childrenRight.push_back(utils::mkConst(-leftConst));
 501     childrenLeft.erase(childrenLeft.begin());
 502   }
 503
 504   if(childrenLeft.size() == 0) {
 505     if (rightConst != zero) {
 506       Assert(childrenRight[0].isConst() && childrenRight[0].getConst<BitVector>() == rightConst);
 507       if (childrenRight.size() == 1) {
 508         // 0 = c ==> false
 509         return utils::mkFalse();
 510       }
 511       // special case - if left is empty and right has a constant, move the constant
 512       // TODO: this is inefficient - would be better if constant were at the end in the normal form
 513       newLeft = utils::mkConst(-rightConst);
 514       childrenRight.erase(childrenRight.begin());
 515     }
 516     else {
 517       newLeft = utils::mkConst(size, (unsigned)0);
 518     }
 519   }
 520   else if (childrenLeft.size() == 1) {
 521     newLeft = childrenLeft[0];
 522   }
 523   else {
 524     newLeft = utils::mkSortedNode(kind::BITVECTOR_PLUS, childrenLeft);
 525   }
 526
 527   if (childrenRight.size() == 0) {
 528     newRight = utils::mkConst(size, (unsigned)0);
 529   }
 530   else if (childrenRight.size() == 1) {
 531     newRight = childrenRight[0];
 532   }
 533   else {
 534     newRight = utils::mkSortedNode(kind::BITVECTOR_PLUS, childrenRight);
 535   }
 536
 537   if (newLeft == newRight) {
 538     Assert (newLeft == utils::mkConst(size, (unsigned)0));
 539     return utils::mkTrue();
 540   }
 541
 542   if (newLeft < newRight) {
 543     return newRight.eqNode(newLeft);
 544   }
 545
 546   return newLeft.eqNode(newRight);
 547 }
 548
 549
 550 template<> inline
 551 bool RewriteRule<BitwiseEq>::applies(TNode node) {
 552   if (node.getKind() != kind::EQUAL ||
 553       utils::getSize(node[0]) != 1) {
 554     return false;
 555   }
 556   TNode term;
 557   BitVector c;
 558   if (node[0].getKind() == kind::CONST_BITVECTOR) {
 559     c = node[0].getConst<BitVector>();
 560     term = node[1];
 561   }
 562   else if (node[1].getKind() == kind::CONST_BITVECTOR) {
 563     c = node[1].getConst<BitVector>();
 564     term = node[0];
 565   }
 566   else {
 567     return false;
 568   }
 569   switch (term.getKind()) {
 570     case kind::BITVECTOR_AND:
 571     case kind::BITVECTOR_OR:
 572       //operator BITVECTOR_XOR 2: "bitwise xor"
 573     case kind::BITVECTOR_NOT:
 574     case kind::BITVECTOR_NAND:
 575     case kind::BITVECTOR_NOR:
 576       //operator BITVECTOR_XNOR 2 "bitwise xnor"
 577     case kind::BITVECTOR_COMP:
 578     case kind::BITVECTOR_NEG:
 579       return true;
 580       break;
 581     default:
 582       break;
 583   }
 584   return false;
 585 }
 586
 587
 588 static inline Node mkNodeKind(Kind k, TNode node, TNode c) {
 589   unsigned i = 0;
 590   unsigned nc = node.getNumChildren();
 591   NodeBuilder<> nb(k);
 592   for(; i < nc; ++i) {
 593     nb << node[i].eqNode(c);
 594   }
 595   return nb;
 596 }
 597
 598
 599 template<> inline
 600 Node RewriteRule<BitwiseEq>::apply(TNode node) {
 601   BVDebug("bv-rewrite") << "RewriteRule<BitwiseEq>(" << node << ")" << std::endl;
 602
 603   TNode term;
 604   BitVector c;
 605
 606   if (node[0].getKind() == kind::CONST_BITVECTOR) {
 607     c = node[0].getConst<BitVector>();
 608     term = node[1];
 609   }
 610   else if (node[1].getKind() == kind::CONST_BITVECTOR) {
 611     c = node[1].getConst<BitVector>();
 612     term = node[0];
 613   }
 614
 615   bool eqOne = (c == BitVector(1,(unsigned)1));
 616
 617   switch (term.getKind()) {
 618     case kind::BITVECTOR_AND:
 619       if (eqOne) {
 620         return mkNodeKind(kind::AND, term, utils::mkConst(1, (unsigned)1));
 621       }
 622       else {
 623         return mkNodeKind(kind::OR, term, utils::mkConst(1, (unsigned)0));
 624       }
 625       break;
 626     case kind::BITVECTOR_NAND:
 627       if (eqOne) {
 628         return mkNodeKind(kind::OR, term, utils::mkConst(1, (unsigned)0));
 629       }
 630       else {
 631         return mkNodeKind(kind::AND, term, utils::mkConst(1, (unsigned)1));
 632       }
 633       break;
 634     case kind::BITVECTOR_OR:
 635       if (eqOne) {
 636         return mkNodeKind(kind::OR, term, utils::mkConst(1, (unsigned)1));
 637       }
 638       else {
 639         return mkNodeKind(kind::AND, term, utils::mkConst(1, (unsigned)0));
 640       }
 641       break;
 642     case kind::BITVECTOR_NOR:
 643       if (eqOne) {
 644         return mkNodeKind(kind::AND, term, utils::mkConst(1, (unsigned)0));
 645       }
 646       else {
 647         return mkNodeKind(kind::OR, term, utils::mkConst(1, (unsigned)1));
 648       }
 649       break;
 650     case kind::BITVECTOR_NOT:
 651       return term[0].eqNode(utils::mkConst(~c));
 652     case kind::BITVECTOR_COMP:
 653       Assert(term.getNumChildren() == 2);
 654       if (eqOne) {
 655         return term[0].eqNode(term[1]);
 656       }
 657       else {
 658         return term[0].eqNode(term[1]).notNode();
 659       }
 660     case kind::BITVECTOR_NEG:
 661       return term[0].eqNode(utils::mkConst(c));
 662     default:
 663       break;
 664   }
 665   Unreachable();
 666 }
 667
 668
 669 /**
 670  * -(c * expr) ==> (-c * expr)
 671  * where c is a constant
 672  */
 673 template<> inline
 674 bool RewriteRule<NegMult>::applies(TNode node) {
 675   if(node.getKind()!= kind::BITVECTOR_NEG ||
 676      node[0].getKind() != kind::BITVECTOR_MULT) {
 677     return false;
 678   }
 679   TNode mult = node[0];
 680   for (unsigned i = 0; i < mult.getNumChildren(); ++i) {
 681     if (mult[i].getKind() == kind::CONST_BITVECTOR) {
 682       return true;
 683     }
 684   }
 685   return false;
 686 }
 687
 688 template<> inline
 689 Node RewriteRule<NegMult>::apply(TNode node) {
 690   BVDebug("bv-rewrite") << "RewriteRule<NegMult>(" << node << ")" << std::endl;
 691   TNode mult = node[0];
 692   std::vector<Node> children;
 693   BitVector bv(utils::getSize(node), (unsigned)1);
 694   for(unsigned i = 0; i < mult.getNumChildren(); ++i) {
 695     if(mult[i].getKind() == kind::CONST_BITVECTOR) {
 696       bv = bv * mult[i].getConst<BitVector>();
 697     } else {
 698       children.push_back(mult[i]);
 699     }
 700   }
 701   children.push_back(utils::mkConst(-bv));
 702   return utils::mkSortedNode(kind::BITVECTOR_MULT, children);
 703 }
 704
 705 template<> inline
 706 bool RewriteRule<NegSub>::applies(TNode node) {
 707   return (node.getKind() == kind::BITVECTOR_NEG &&
 708           node[0].getKind() == kind::BITVECTOR_SUB);
 709 }
 710
 711 template<> inline
 712 Node RewriteRule<NegSub>::apply(TNode node) {
 713   BVDebug("bv-rewrite") << "RewriteRule<NegSub>(" << node << ")" << std::endl;
 714   return utils::mkNode(kind::BITVECTOR_SUB, node[0][1], node[0][0]);
 715 }
 716
 717 template<> inline
 718 bool RewriteRule<NegPlus>::applies(TNode node) {
 719   return (node.getKind() == kind::BITVECTOR_NEG &&
 720           node[0].getKind() == kind::BITVECTOR_PLUS);
 721 }
 722
 723 template<> inline
 724 Node RewriteRule<NegPlus>::apply(TNode node) {
 725   BVDebug("bv-rewrite") << "RewriteRule<NegPlus>(" << node << ")" << std::endl;
 726   std::vector<Node> children;
 727   for (unsigned i = 0; i < node[0].getNumChildren(); ++i) {
 728     children.push_back(utils::mkNode(kind::BITVECTOR_NEG, node[0][i]));
 729   }
 730   return utils::mkSortedNode(kind::BITVECTOR_PLUS, children);
 731 }
 732
 733
 734
 735
 736 struct Count {
 737   unsigned pos;
 738   unsigned neg;
 739   Count() : pos(0), neg(0) {}
 740   Count(unsigned p, unsigned n):
 741     pos(p),
 742     neg(n)
 743   {}
 744 };
 745
 746 inline static void insert(std::hash_map<TNode, Count, TNodeHashFunction>& map, TNode node, bool neg) {
 747   if(map.find(node) == map.end()) {
 748     Count c = neg? Count(0,1) : Count(1, 0);
 749     map[node] = c;
 750   } else {
 751     if (neg) {
 752       ++(map[node].neg);
 753     } else {
 754       ++(map[node].pos);
 755     }
 756   }
 757 }
 758
 759 template<> inline
 760 bool RewriteRule<AndSimplify>::applies(TNode node) {
 761   return (node.getKind() == kind::BITVECTOR_AND);
 762 }
 763
 764 template<> inline
 765 Node RewriteRule<AndSimplify>::apply(TNode node) {
 766   BVDebug("bv-rewrite") << "RewriteRule<AndSimplify>(" << node << ")" << std::endl;
 767
 768   // this will remove duplicates
 769   std::hash_map<TNode, Count, TNodeHashFunction> subterms;
 770   unsigned size = utils::getSize(node);
 771   BitVector constant = utils::mkBitVectorOnes(size);
 772
 773   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
 774     TNode current = node[i];
 775     // simplify constants
 776     if (current.getKind() == kind::CONST_BITVECTOR) {
 777       BitVector bv = current.getConst<BitVector>();
 778       constant = constant & bv;
 779     } else {
 780       if (current.getKind() == kind::BITVECTOR_NOT) {
 781         insert(subterms, current[0], true);
 782       } else {
 783         insert(subterms, current, false);
 784       }
 785     }
 786   }
 787
 788   std::vector<Node> children;
 789
 790   if (constant == BitVector(size, (unsigned)0)) {
 791     return utils::mkConst(BitVector(size, (unsigned)0));
 792   }
 793
 794   if (constant != utils::mkBitVectorOnes(size)) {
 795     children.push_back(utils::mkConst(constant));
 796   }
 797
 798   std::hash_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin();
 799
 800   for (; it != subterms.end(); ++it) {
 801     if (it->second.pos > 0 && it->second.neg > 0) {
 802       // if we have a and ~a
 803       return utils::mkConst(BitVector(size, (unsigned)0));
 804     } else {
 805       // idempotence
 806       if (it->second.neg > 0) {
 807         // if it only occured negated
 808         children.push_back(utils::mkNode(kind::BITVECTOR_NOT, it->first));
 809       } else {
 810         // if it only occured positive
 811         children.push_back(it->first);
 812       }
 813     }
 814   }
 815   if (children.size() == 0) {
 816     return utils::mkOnes(size);
 817   }
 818
 819   return utils::mkSortedNode(kind::BITVECTOR_AND, children);
 820 }
 821
 822 template<> inline
 823 bool RewriteRule<OrSimplify>::applies(TNode node) {
 824   return (node.getKind() == kind::BITVECTOR_OR);
 825 }
 826
 827 template<> inline
 828 Node RewriteRule<OrSimplify>::apply(TNode node) {
 829   BVDebug("bv-rewrite") << "RewriteRule<OrSimplify>(" << node << ")" << std::endl;
 830
 831   // this will remove duplicates
 832   std::hash_map<TNode, Count, TNodeHashFunction> subterms;
 833   unsigned size = utils::getSize(node);
 834   BitVector constant(size, (unsigned)0);
 835
 836   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
 837     TNode current = node[i];
 838     // simplify constants
 839     if (current.getKind() == kind::CONST_BITVECTOR) {
 840       BitVector bv = current.getConst<BitVector>();
 841       constant = constant | bv;
 842     } else {
 843       if (current.getKind() == kind::BITVECTOR_NOT) {
 844         insert(subterms, current[0], true);
 845       } else {
 846         insert(subterms, current, false);
 847       }
 848     }
 849   }
 850
 851   std::vector<Node> children;
 852
 853   if (constant == utils::mkBitVectorOnes(size)) {
 854     return utils::mkOnes(size);
 855   }
 856
 857   if (constant != BitVector(size, (unsigned)0)) {
 858     children.push_back(utils::mkConst(constant));
 859   }
 860
 861   std::hash_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin();
 862
 863   for (; it != subterms.end(); ++it) {
 864     if (it->second.pos > 0 && it->second.neg > 0) {
 865       // if we have a or ~a
 866       return utils::mkOnes(size);
 867     } else {
 868       // idempotence
 869       if (it->second.neg > 0) {
 870         // if it only occured negated
 871         children.push_back(utils::mkNode(kind::BITVECTOR_NOT, it->first));
 872       } else {
 873         // if it only occured positive
 874         children.push_back(it->first);
 875       }
 876     }
 877   }
 878
 879   if (children.size() == 0) {
 880     return utils::mkConst(BitVector(size, (unsigned)0));
 881   }
 882   return utils::mkSortedNode(kind::BITVECTOR_OR, children);
 883 }
 884
 885 template<> inline
 886 bool RewriteRule<XorSimplify>::applies(TNode node) {
 887   return (node.getKind() == kind::BITVECTOR_XOR);
 888 }
 889
 890 template<> inline
 891 Node RewriteRule<XorSimplify>::apply(TNode node) {
 892   BVDebug("bv-rewrite") << "RewriteRule<XorSimplify>(" << node << ")" << std::endl;
 893
 894
 895   std::hash_map<TNode, Count, TNodeHashFunction> subterms;
 896   unsigned size = utils::getSize(node);
 897   BitVector constant;
 898   bool const_set = false;
 899
 900   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
 901     TNode current = node[i];
 902     // simplify constants
 903     if (current.getKind() == kind::CONST_BITVECTOR) {
 904       BitVector bv = current.getConst<BitVector>();
 905       if (const_set) {
 906         constant = constant ^ bv;
 907       } else {
 908         const_set = true;
 909         constant = bv;
 910       }
 911     } else {
 912       // collect number of occurances of each term and its negation
 913       if (current.getKind() == kind::BITVECTOR_NOT) {
 914         insert(subterms, current[0], true);
 915       } else {
 916         insert(subterms, current, false);
 917       }
 918     }
 919   }
 920
 921   std::vector<Node> children;
 922
 923   std::hash_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin();
 924   unsigned true_count = 0;
 925   bool seen_false = false;
 926   for (; it != subterms.end(); ++it) {
 927     unsigned pos = it->second.pos; // number of positive occurances
 928     unsigned neg = it->second.neg; // number of negated occurances
 929
 930     // remove duplicates using the following rules
 931     // a xor a ==> false
 932     // false xor false ==> false
 933     seen_false = seen_false? seen_false : (pos > 1 || neg > 1);
 934     // check what did not reduce
 935     if (pos % 2 && neg % 2) {
 936       // we have a xor ~a ==> true
 937       ++true_count;
 938     } else if (pos % 2) {
 939       // we had a positive occurence left
 940       children.push_back(it->first);
 941     } else if (neg % 2) {
 942       // we had a negative occurence left
 943       children.push_back(utils::mkNode(kind::BITVECTOR_NOT, it->first));
 944     }
 945     // otherwise both reduced to false
 946   }
 947
 948   std::vector<BitVector> xorConst;
 949   BitVector true_bv = utils::mkBitVectorOnes(size);
 950   BitVector false_bv(size, (unsigned)0);
 951
 952   if (true_count) {
 953     // true xor ... xor true ==> true (odd)
 954     //                       ==> false (even)
 955     xorConst.push_back(true_count % 2? true_bv : false_bv);
 956   }
 957   if (seen_false) {
 958     xorConst.push_back(false_bv);
 959   }
 960   if(const_set) {
 961     xorConst.push_back(constant);
 962   }
 963
 964   if (xorConst.size() > 0) {
 965     BitVector result = xorConst[0];
 966     for (unsigned i = 1; i < xorConst.size(); ++i) {
 967       result = result ^ xorConst[i];
 968     }
 969     children.push_back(utils::mkConst(result));
 970   }
 971
 972   Assert(children.size());
 973
 974   return utils::mkSortedNode(kind::BITVECTOR_XOR, children);
 975 }
 976
 977
 978
 979
 980 // template<> inline
 981 // bool RewriteRule<AndSimplify>::applies(TNode node) {
 982 //   return (node.getKind() == kind::BITVECTOR_AND);
 983 // }
 984
 985 // template<> inline
 986 // Node RewriteRule<AndSimplify>::apply(TNode node) {
 987 //   BVDebug("bv-rewrite") << "RewriteRule<AndSimplify>(" << node << ")" << std::endl;
 988 //   return resultNode;
 989 // }
 990
 991
 992 // template<> inline
 993 // bool RewriteRule<>::applies(TNode node) {
 994 //   return (node.getKind() == kind::BITVECTOR_CONCAT);
 995 // }
 996
 997 // template<> inline
 998 // Node RewriteRule<>::apply(TNode node) {
 999 //   BVDebug("bv-rewrite") << "RewriteRule<>(" << node << ")" << std::endl;
1000 //   return resultNode;
1001 // }
1002
1003
1004
1005 }
1006 }
1007 }