5be0529474ecf689002135a10a468d4f33af3202
1 /********************* */
2 /*! \file theory_bv_rewrite_rules_normalization.h
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
14 ** \brief [[ Add one-line brief description here ]]
16 ** [[ Add lengthier description here ]]
17 ** \todo document this file
20 #include "cvc4_private.h"
24 #include "theory/bv/theory_bv_rewrite_rules.h"
25 #include "theory/bv/theory_bv_utils.h"
33 * (x bvop y) [i:j] ==> x[i:j] bvop y[i:j]
34 * where bvop is bvand,bvor, bvxor
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
));
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
));
53 Kind kind
= node
[0].getKind();
54 return utils::mkSortedNode(kind
, children
);
60 * (~ a) [i:j] ==> ~ (a[i:j])
63 bool RewriteRule
<ExtractNot
>::applies(TNode node
) {
64 return (node
.getKind() == kind::BITVECTOR_EXTRACT
&&
65 node
[0].getKind() == kind::BITVECTOR_NOT
);
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
);
80 * (a bvop b) [k:0] ==> (a[k:0] bvop b[k:0])
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
));
92 Node RewriteRule
<ExtractArith
>::apply(TNode node
) {
93 BVDebug("bv-rewrite") << "RewriteRule<ExtractArith>(" << node
<< ")" << std::endl
;
94 unsigned low
= utils::getExtractLow(node
);
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
));
101 Kind kind
= node
[0].getKind();
102 return utils::mkNode(kind
, children
);
109 * (a bvop b) [i:j] ==> (a[i:0] bvop b[i:0]) [i:j]
112 // careful not to apply in a loop
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
));
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));
129 Kind kind
= node
[0].getKind();
130 Node op_children
= utils::mkSortedNode(kind
, children
);
132 return utils::mkExtract(op_children
, high
, low
);
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
);
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();
153 while (! processingStack
.empty()) {
154 TNode current
= processingStack
.back();
155 processingStack
.pop_back();
157 // flatten expression
158 if (current
.getKind() == kind
) {
159 for (unsigned i
= 0; i
< current
.getNumChildren(); ++i
) {
160 processingStack
.push_back(current
[i
]);
163 children
.push_back(current
);
166 return utils::mkSortedNode(kind
, children
);
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
;
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
189 // figure out which part is the constant
190 if (current
[0].getKind() == kind::CONST_BITVECTOR
) {
191 coeff
= current
[0].getConst
<BitVector
>();
194 coeff
= current
[1].getConst
<BitVector
>();
197 if(term
.getKind() == kind::BITVECTOR_SUB
) {
200 addToCoefMap(factorToCoefficient
, a
, coeff
);
201 addToCoefMap(factorToCoefficient
, b
, -coeff
);
203 else if(term
.getKind() == kind::BITVECTOR_NEG
) {
204 addToCoefMap(factorToCoefficient
, term
[0], -BitVector(size
, coeff
));
207 addToCoefMap(factorToCoefficient
, term
, coeff
);
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));
215 else if (current
.getKind() == kind::BITVECTOR_NEG
) {
216 addToCoefMap(factorToCoefficient
, current
[0], -BitVector(size
, (unsigned)1));
218 else if (current
.getKind() == kind::CONST_BITVECTOR
) {
219 BitVector constValue
= current
.getConst
<BitVector
>();
220 constSum
= constSum
+ constValue
;
223 // store as 1 * current
224 addToCoefMap(factorToCoefficient
, current
, BitVector(size
, (unsigned)1));
229 static inline void addToChildren(TNode term
, unsigned size
, BitVector coeff
, std::vector
<Node
>& children
) {
230 if (coeff
== BitVector(size
, (unsigned)0)) {
233 else if (coeff
== BitVector(size
, (unsigned)1)) {
234 children
.push_back(term
);
236 else if (coeff
== -BitVector(size
, (unsigned)1)) {
237 // avoid introducing an extra multiplication
238 children
.push_back(utils::mkNode(kind::BITVECTOR_NEG
, term
));
241 Node coeffNode
= utils::mkConst(coeff
);
242 Node product
= utils::mkSortedNode(kind::BITVECTOR_MULT
, coeffNode
, term
);
243 children
.push_back(product
);
249 bool RewriteRule
<PlusCombineLikeTerms
>::applies(TNode node
) {
250 return (node
.getKind() == kind::BITVECTOR_PLUS
);
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
;
261 // combine like-terms
262 for(unsigned i
= 0; i
< node
.getNumChildren(); ++i
) {
263 TNode current
= node
[i
];
264 updateCoefMap(current
, size
, factorToCoefficient
, constSum
);
267 std::vector
<Node
> children
;
268 if ( constSum
!= BitVector(size
, (unsigned)0)) {
269 children
.push_back(utils::mkConst(constSum
));
273 std::map
<Node
, BitVector
>::const_iterator it
= factorToCoefficient
.begin();
275 for (; it
!= factorToCoefficient
.end(); ++it
) {
276 addToChildren(it
->first
, size
, it
->second
, children
);
279 if(children
.size() == 0) {
280 return utils::mkConst(size
, (unsigned)0);
283 return utils::mkSortedNode(kind::BITVECTOR_PLUS
, children
);
288 bool RewriteRule
<MultSimplify
>::applies(TNode node
) {
289 return (node
.getKind() == kind::BITVECTOR_MULT
);
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));
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);
306 constant
= constant
* current
.getConst
<BitVector
>();
308 children
.push_back(current
);
313 if(constant
!= BitVector(size
, (unsigned)1)) {
314 children
.push_back(utils::mkConst(constant
));
318 if(children
.size() == 0) {
319 return utils::mkConst(size
, (unsigned)1);
322 return utils::mkSortedNode(kind::BITVECTOR_MULT
, children
);
326 bool RewriteRule
<MultDistribConst
>::applies(TNode node
) {
327 if (node
.getKind() != kind::BITVECTOR_MULT
)
331 if (node
[0].getKind() == kind::CONST_BITVECTOR
) {
333 } else if (node
[1].getKind() == kind::CONST_BITVECTOR
) {
339 return (factor
.getKind() == kind::BITVECTOR_PLUS
||
340 factor
.getKind() == kind::BITVECTOR_SUB
||
341 factor
.getKind() == kind::BITVECTOR_NEG
);
345 Node RewriteRule
<MultDistribConst
>::apply(TNode node
) {
346 BVDebug("bv-rewrite") << "RewriteRule<MultDistribConst>(" << node
<< ")" << std::endl
;
350 if (node
[0].getKind() == kind::CONST_BITVECTOR
) {
354 Assert(node
[1].getKind() == kind::CONST_BITVECTOR
);
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
),
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
]));
372 return utils::mkSortedNode(factor
.getKind(), children
);
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]))) {
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
390 Node RewriteRule
<SolveEq
>::apply(TNode node
) {
391 BVDebug("bv-rewrite") << "RewriteRule<SolveEq>(" << node
<< ")" << std::endl
;
393 TNode left
= node
[0];
394 TNode right
= node
[1];
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
;
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
);
409 updateCoefMap(left
, size
, leftMap
, leftConst
);
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
);
419 updateCoefMap(right
, size
, rightMap
, rightConst
);
422 std::vector
<Node
> childrenLeft
, childrenRight
;
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
));
429 else if (leftConst
!= zero
) {
430 childrenLeft
.push_back(utils::mkConst(leftConst
));
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();
438 if (iLeft
!= iLeftEnd
) {
439 coeffLeft
= iLeft
->second
;
440 termLeft
= iLeft
->first
;
443 BitVector coeffRight
;
445 if (iRight
!= iRightEnd
) {
446 coeffRight
= iRight
->second
;
447 termRight
= iRight
->first
;
450 bool incLeft
, incRight
;
452 while (iLeft
!= iLeftEnd
|| iRight
!= iRightEnd
) {
453 incLeft
= incRight
= false;
454 if (iLeft
!= iLeftEnd
&& (iRight
== iRightEnd
|| termLeft
< termRight
)) {
455 addToChildren(termLeft
, size
, coeffLeft
, childrenLeft
);
458 else if (iLeft
== iLeftEnd
|| termRight
< termLeft
) {
459 Assert(iRight
!= iRightEnd
);
460 addToChildren(termRight
, size
, coeffRight
, childrenRight
);
464 if (coeffLeft
> coeffRight
) {
465 addToChildren(termLeft
, size
, coeffLeft
- coeffRight
, childrenLeft
);
467 else if (coeffRight
> coeffLeft
) {
468 addToChildren(termRight
, size
, coeffRight
- coeffLeft
, childrenRight
);
470 incLeft
= incRight
= true;
474 if (iLeft
!= iLeftEnd
) {
475 coeffLeft
= iLeft
->second
;
476 termLeft
= iLeft
->first
;
481 if (iRight
!= iRightEnd
) {
482 coeffRight
= iRight
->second
;
483 termRight
= iRight
->first
;
490 Node newLeft
, newRight
;
492 if(childrenRight
.size() == 0 && leftConst
!= zero
) {
493 Assert(childrenLeft
[0].isConst() && childrenLeft
[0].getConst
<BitVector
>() == leftConst
);
494 if (childrenLeft
.size() == 1) {
496 return utils::mkFalse();
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());
504 if(childrenLeft
.size() == 0) {
505 if (rightConst
!= zero
) {
506 Assert(childrenRight
[0].isConst() && childrenRight
[0].getConst
<BitVector
>() == rightConst
);
507 if (childrenRight
.size() == 1) {
509 return utils::mkFalse();
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());
517 newLeft
= utils::mkConst(size
, (unsigned)0);
520 else if (childrenLeft
.size() == 1) {
521 newLeft
= childrenLeft
[0];
524 newLeft
= utils::mkSortedNode(kind::BITVECTOR_PLUS
, childrenLeft
);
527 if (childrenRight
.size() == 0) {
528 newRight
= utils::mkConst(size
, (unsigned)0);
530 else if (childrenRight
.size() == 1) {
531 newRight
= childrenRight
[0];
534 newRight
= utils::mkSortedNode(kind::BITVECTOR_PLUS
, childrenRight
);
537 if (newLeft
== newRight
) {
538 Assert (newLeft
== utils::mkConst(size
, (unsigned)0));
539 return utils::mkTrue();
542 if (newLeft
< newRight
) {
543 return newRight
.eqNode(newLeft
);
546 return newLeft
.eqNode(newRight
);
551 bool RewriteRule
<BitwiseEq
>::applies(TNode node
) {
552 if (node
.getKind() != kind::EQUAL
||
553 utils::getSize(node
[0]) != 1) {
558 if (node
[0].getKind() == kind::CONST_BITVECTOR
) {
559 c
= node
[0].getConst
<BitVector
>();
562 else if (node
[1].getKind() == kind::CONST_BITVECTOR
) {
563 c
= node
[1].getConst
<BitVector
>();
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
:
588 static inline Node
mkNodeKind(Kind k
, TNode node
, TNode c
) {
590 unsigned nc
= node
.getNumChildren();
593 nb
<< node
[i
].eqNode(c
);
600 Node RewriteRule
<BitwiseEq
>::apply(TNode node
) {
601 BVDebug("bv-rewrite") << "RewriteRule<BitwiseEq>(" << node
<< ")" << std::endl
;
606 if (node
[0].getKind() == kind::CONST_BITVECTOR
) {
607 c
= node
[0].getConst
<BitVector
>();
610 else if (node
[1].getKind() == kind::CONST_BITVECTOR
) {
611 c
= node
[1].getConst
<BitVector
>();
615 bool eqOne
= (c
== BitVector(1,(unsigned)1));
617 switch (term
.getKind()) {
618 case kind::BITVECTOR_AND
:
620 return mkNodeKind(kind::AND
, term
, utils::mkConst(1, (unsigned)1));
623 return mkNodeKind(kind::OR
, term
, utils::mkConst(1, (unsigned)0));
626 case kind::BITVECTOR_NAND
:
628 return mkNodeKind(kind::OR
, term
, utils::mkConst(1, (unsigned)0));
631 return mkNodeKind(kind::AND
, term
, utils::mkConst(1, (unsigned)1));
634 case kind::BITVECTOR_OR
:
636 return mkNodeKind(kind::OR
, term
, utils::mkConst(1, (unsigned)1));
639 return mkNodeKind(kind::AND
, term
, utils::mkConst(1, (unsigned)0));
642 case kind::BITVECTOR_NOR
:
644 return mkNodeKind(kind::AND
, term
, utils::mkConst(1, (unsigned)0));
647 return mkNodeKind(kind::OR
, term
, utils::mkConst(1, (unsigned)1));
650 case kind::BITVECTOR_NOT
:
651 return term
[0].eqNode(utils::mkConst(~c
));
652 case kind::BITVECTOR_COMP
:
653 Assert(term
.getNumChildren() == 2);
655 return term
[0].eqNode(term
[1]);
658 return term
[0].eqNode(term
[1]).notNode();
660 case kind::BITVECTOR_NEG
:
661 return term
[0].eqNode(utils::mkConst(c
));
670 * -(c * expr) ==> (-c * expr)
671 * where c is a constant
674 bool RewriteRule
<NegMult
>::applies(TNode node
) {
675 if(node
.getKind()!= kind::BITVECTOR_NEG
||
676 node
[0].getKind() != kind::BITVECTOR_MULT
) {
679 TNode mult
= node
[0];
680 for (unsigned i
= 0; i
< mult
.getNumChildren(); ++i
) {
681 if (mult
[i
].getKind() == kind::CONST_BITVECTOR
) {
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
>();
698 children
.push_back(mult
[i
]);
701 children
.push_back(utils::mkConst(-bv
));
702 return utils::mkSortedNode(kind::BITVECTOR_MULT
, children
);
706 bool RewriteRule
<NegSub
>::applies(TNode node
) {
707 return (node
.getKind() == kind::BITVECTOR_NEG
&&
708 node
[0].getKind() == kind::BITVECTOR_SUB
);
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]);
718 bool RewriteRule
<NegPlus
>::applies(TNode node
) {
719 return (node
.getKind() == kind::BITVECTOR_NEG
&&
720 node
[0].getKind() == kind::BITVECTOR_PLUS
);
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
]));
730 return utils::mkSortedNode(kind::BITVECTOR_PLUS
, children
);
739 Count() : pos(0), neg(0) {}
740 Count(unsigned p
, unsigned n
):
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);
760 bool RewriteRule
<AndSimplify
>::applies(TNode node
) {
761 return (node
.getKind() == kind::BITVECTOR_AND
);
765 Node RewriteRule
<AndSimplify
>::apply(TNode node
) {
766 BVDebug("bv-rewrite") << "RewriteRule<AndSimplify>(" << node
<< ")" << std::endl
;
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
);
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
;
780 if (current
.getKind() == kind::BITVECTOR_NOT
) {
781 insert(subterms
, current
[0], true);
783 insert(subterms
, current
, false);
788 std::vector
<Node
> children
;
790 if (constant
== BitVector(size
, (unsigned)0)) {
791 return utils::mkConst(BitVector(size
, (unsigned)0));
794 if (constant
!= utils::mkBitVectorOnes(size
)) {
795 children
.push_back(utils::mkConst(constant
));
798 std::hash_map
<TNode
, Count
, TNodeHashFunction
>::const_iterator it
= subterms
.begin();
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));
806 if (it
->second
.neg
> 0) {
807 // if it only occured negated
808 children
.push_back(utils::mkNode(kind::BITVECTOR_NOT
, it
->first
));
810 // if it only occured positive
811 children
.push_back(it
->first
);
815 if (children
.size() == 0) {
816 return utils::mkOnes(size
);
819 return utils::mkSortedNode(kind::BITVECTOR_AND
, children
);
823 bool RewriteRule
<OrSimplify
>::applies(TNode node
) {
824 return (node
.getKind() == kind::BITVECTOR_OR
);
828 Node RewriteRule
<OrSimplify
>::apply(TNode node
) {
829 BVDebug("bv-rewrite") << "RewriteRule<OrSimplify>(" << node
<< ")" << std::endl
;
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);
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
;
843 if (current
.getKind() == kind::BITVECTOR_NOT
) {
844 insert(subterms
, current
[0], true);
846 insert(subterms
, current
, false);
851 std::vector
<Node
> children
;
853 if (constant
== utils::mkBitVectorOnes(size
)) {
854 return utils::mkOnes(size
);
857 if (constant
!= BitVector(size
, (unsigned)0)) {
858 children
.push_back(utils::mkConst(constant
));
861 std::hash_map
<TNode
, Count
, TNodeHashFunction
>::const_iterator it
= subterms
.begin();
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
);
869 if (it
->second
.neg
> 0) {
870 // if it only occured negated
871 children
.push_back(utils::mkNode(kind::BITVECTOR_NOT
, it
->first
));
873 // if it only occured positive
874 children
.push_back(it
->first
);
879 if (children
.size() == 0) {
880 return utils::mkConst(BitVector(size
, (unsigned)0));
882 return utils::mkSortedNode(kind::BITVECTOR_OR
, children
);
886 bool RewriteRule
<XorSimplify
>::applies(TNode node
) {
887 return (node
.getKind() == kind::BITVECTOR_XOR
);
891 Node RewriteRule
<XorSimplify
>::apply(TNode node
) {
892 BVDebug("bv-rewrite") << "RewriteRule<XorSimplify>(" << node
<< ")" << std::endl
;
895 std::hash_map
<TNode
, Count
, TNodeHashFunction
> subterms
;
896 unsigned size
= utils::getSize(node
);
898 bool const_set
= false;
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
>();
906 constant
= constant
^ bv
;
912 // collect number of occurances of each term and its negation
913 if (current
.getKind() == kind::BITVECTOR_NOT
) {
914 insert(subterms
, current
[0], true);
916 insert(subterms
, current
, false);
921 std::vector
<Node
> children
;
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
930 // remove duplicates using the following rules
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
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
));
945 // otherwise both reduced to false
948 std::vector
<BitVector
> xorConst
;
949 BitVector true_bv
= utils::mkBitVectorOnes(size
);
950 BitVector
false_bv(size
, (unsigned)0);
953 // true xor ... xor true ==> true (odd)
955 xorConst
.push_back(true_count
% 2? true_bv
: false_bv
);
958 xorConst
.push_back(false_bv
);
961 xorConst
.push_back(constant
);
964 if (xorConst
.size() > 0) {
965 BitVector result
= xorConst
[0];
966 for (unsigned i
= 1; i
< xorConst
.size(); ++i
) {
967 result
= result
^ xorConst
[i
];
969 children
.push_back(utils::mkConst(result
));
972 Assert(children
.size());
974 return utils::mkSortedNode(kind::BITVECTOR_XOR
, children
);
981 // bool RewriteRule<AndSimplify>::applies(TNode node) {
982 // return (node.getKind() == kind::BITVECTOR_AND);
986 // Node RewriteRule<AndSimplify>::apply(TNode node) {
987 // BVDebug("bv-rewrite") << "RewriteRule<AndSimplify>(" << node << ")" << std::endl;
988 // return resultNode;
993 // bool RewriteRule<>::applies(TNode node) {
994 // return (node.getKind() == kind::BITVECTOR_CONCAT);
998 // Node RewriteRule<>::apply(TNode node) {
999 // BVDebug("bv-rewrite") << "RewriteRule<>(" << node << ")" << std::endl;
1000 // return resultNode;