1 /********************* */
2 /*! \file theory_bv_rewrite_rules_simplification.h
4 ** Original author: lianah
5 ** Major contributors: none
6 ** Minor contributors (to current version):
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
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"
31 // FIXME: this rules subsume the constant evaluation ones
37 * Left Shift by constant amount
40 bool RewriteRule
<ShlByConst
>::applies(Node node
) {
41 // if the shift amount is constant
42 return (node
.getKind() == kind::BITVECTOR_SHL
&&
43 node
[1].getKind() == kind::CONST_BITVECTOR
);
47 Node RewriteRule
<ShlByConst
>::apply(Node node
) {
48 BVDebug("bv-rewrite") << "RewriteRule<ShlByConst>(" << node
<< ")" << std::endl
;
49 Integer amount
= node
[1].getConst
<BitVector
>().toInteger();
52 uint32_t size
= utils::getSize(a
);
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)));
60 // make sure we do not lose information casting
61 Assert(amount
< Integer(1).multiplyByPow2(32));
63 uint32_t uint32_amount
= amount
.toUnsignedInt();
64 Node left
= utils::mkExtract(a
, size
- 1 - uint32_amount
, 0);
65 Node right
= utils::mkConst(BitVector(uint32_amount
, Integer(0)));
66 return utils::mkConcat(left
, right
);
72 * Right Logical Shift by constant amount
76 bool RewriteRule
<LshrByConst
>::applies(Node node
) {
77 // if the shift amount is constant
78 return (node
.getKind() == kind::BITVECTOR_LSHR
&&
79 node
[1].getKind() == kind::CONST_BITVECTOR
);
83 Node RewriteRule
<LshrByConst
>::apply(Node node
) {
84 BVDebug("bv-rewrite") << "RewriteRule<LshrByConst>(" << node
<< ")" << std::endl
;
85 Integer amount
= node
[1].getConst
<BitVector
>().toInteger();
88 uint32_t size
= utils::getSize(a
);
91 if (amount
>= Integer(size
)) {
92 // if we are shifting more than the length of the bitvector return 0
93 return utils::mkConst(BitVector(size
, Integer(0)));
96 // make sure we do not lose information casting
97 Assert(amount
< Integer(1).multiplyByPow2(32));
99 uint32_t uint32_amount
= amount
.toUnsignedInt();
100 Node right
= utils::mkExtract(a
, size
- 1, uint32_amount
);
101 Node left
= utils::mkConst(BitVector(uint32_amount
, Integer(0)));
102 return utils::mkConcat(left
, right
);
108 * Right Arithmetic Shift by constant amount
112 bool RewriteRule
<AshrByConst
>::applies(Node node
) {
113 // if the shift amount is constant
114 return (node
.getKind() == kind::BITVECTOR_ASHR
&&
115 node
[1].getKind() == kind::CONST_BITVECTOR
);
119 Node RewriteRule
<AshrByConst
>::apply(Node node
) {
120 BVDebug("bv-rewrite") << "RewriteRule<AshrByConst>(" << node
<< ")" << std::endl
;
121 Integer amount
= node
[1].getConst
<BitVector
>().toInteger();
124 uint32_t size
= utils::getSize(a
);
125 Node sign_bit
= utils::mkExtract(a
, size
-1, size
-1);
127 if (amount
>= Integer(size
)) {
128 // if we are shifting more than the length of the bitvector return n repetitions
130 return utils::mkConcat(sign_bit
, size
);
133 // make sure we do not lose information casting
134 Assert(amount
< Integer(1).multiplyByPow2(32));
136 uint32_t uint32_amount
= amount
.toUnsignedInt();
137 if (uint32_amount
== 0) {
141 Node left
= utils::mkConcat(sign_bit
, uint32_amount
);
142 Node right
= utils::mkExtract(a
, size
- 1, uint32_amount
);
143 return utils::mkConcat(left
, right
);
154 bool RewriteRule
<BitwiseIdemp
>::applies(Node node
) {
155 return ((node
.getKind() == kind::BITVECTOR_AND
||
156 node
.getKind() == kind::BITVECTOR_OR
) &&
161 Node RewriteRule
<BitwiseIdemp
>::apply(Node node
) {
162 BVDebug("bv-rewrite") << "RewriteRule<BitwiseIdemp>(" << node
<< ")" << std::endl
;
173 bool RewriteRule
<AndZero
>::applies(Node node
) {
174 unsigned size
= utils::getSize(node
);
175 return (node
.getKind() == kind::BITVECTOR_AND
&&
176 (node
[0] == utils::mkConst(size
, 0) ||
177 node
[1] == utils::mkConst(size
, 0)));
181 Node RewriteRule
<AndZero
>::apply(Node node
) {
182 BVDebug("bv-rewrite") << "RewriteRule<AndZero>(" << node
<< ")" << std::endl
;
183 return utils::mkConst(utils::getSize(node
), 0);
193 bool RewriteRule
<AndOne
>::applies(Node node
) {
194 unsigned size
= utils::getSize(node
);
195 Node ones
= utils::mkOnes(size
);
196 return (node
.getKind() == kind::BITVECTOR_AND
&&
202 Node RewriteRule
<AndOne
>::apply(Node node
) {
203 BVDebug("bv-rewrite") << "RewriteRule<AndOne>(" << node
<< ")" << std::endl
;
204 unsigned size
= utils::getSize(node
);
206 if (node
[0] == utils::mkOnes(size
)) {
209 Assert (node
[1] == utils::mkOnes(size
));
221 bool RewriteRule
<OrZero
>::applies(Node node
) {
222 unsigned size
= utils::getSize(node
);
223 return (node
.getKind() == kind::BITVECTOR_OR
&&
224 (node
[0] == utils::mkConst(size
, 0) ||
225 node
[1] == utils::mkConst(size
, 0)));
229 Node RewriteRule
<OrZero
>::apply(Node node
) {
230 BVDebug("bv-rewrite") << "RewriteRule<OrZero>(" << node
<< ")" << std::endl
;
232 unsigned size
= utils::getSize(node
);
233 if (node
[0] == utils::mkConst(size
, 0)) {
236 Assert(node
[1] == utils::mkConst(size
, 0));
248 bool RewriteRule
<OrOne
>::applies(Node node
) {
249 unsigned size
= utils::getSize(node
);
250 Node ones
= utils::mkOnes(size
);
251 return (node
.getKind() == kind::BITVECTOR_OR
&&
257 Node RewriteRule
<OrOne
>::apply(Node node
) {
258 BVDebug("bv-rewrite") << "RewriteRule<OrOne>(" << node
<< ")" << std::endl
;
259 return utils::mkOnes(utils::getSize(node
));
270 bool RewriteRule
<XorDuplicate
>::applies(Node node
) {
271 return (node
.getKind() == kind::BITVECTOR_XOR
&&
276 Node RewriteRule
<XorDuplicate
>::apply(Node node
) {
277 BVDebug("bv-rewrite") << "RewriteRule<XorDuplicate>(" << node
<< ")" << std::endl
;
278 return utils::mkConst(BitVector(utils::getSize(node
), Integer(0)));
288 bool RewriteRule
<XorOne
>::applies(Node node
) {
289 if (node
.getKind() != kind::BITVECTOR_XOR
) {
292 Node ones
= utils::mkOnes(utils::getSize(node
));
293 for (unsigned i
= 0; i
< node
.getNumChildren(); ++i
) {
294 if (node
[i
] == ones
) {
302 Node RewriteRule
<XorOne
>::apply(Node node
) {
303 BVDebug("bv-rewrite") << "RewriteRule<XorOne>(" << node
<< ")" << std::endl
;
304 Node ones
= utils::mkOnes(utils::getSize(node
));
305 std::vector
<Node
> children
;
306 bool found_ones
= false;
307 // XorSimplify should have been called before
308 for(unsigned i
= 0; i
< node
.getNumChildren(); ++i
) {
309 if (node
[i
] == ones
) {
310 // make sure only ones occurs only once
314 children
.push_back(node
[i
]);
318 children
[0] = utils::mkNode(kind::BITVECTOR_NOT
, children
[0]);
319 return utils::mkSortedNode(kind::BITVECTOR_XOR
, children
);
330 bool RewriteRule
<XorZero
>::applies(Node node
) {
331 if (node
.getKind() != kind::BITVECTOR_XOR
) {
334 Node zero
= utils::mkConst(utils::getSize(node
), 0);
335 for (unsigned i
= 0; i
< node
.getNumChildren(); ++i
) {
336 if (node
[i
] == zero
) {
344 Node RewriteRule
<XorZero
>::apply(Node node
) {
345 BVDebug("bv-rewrite") << "RewriteRule<XorZero>(" << node
<< ")" << std::endl
;
346 std::vector
<Node
> children
;
347 bool found_zero
= false;
348 Node zero
= utils::mkConst(utils::getSize(node
), 0);
350 // XorSimplify should have been called before
351 for(unsigned i
= 0; i
< node
.getNumChildren(); ++i
) {
352 if (node
[i
] == zero
) {
353 // make sure zero occurs only once
357 children
.push_back(node
[i
]);
361 return utils::mkNode(kind::BITVECTOR_XOR
, children
);
368 * (a bvand (~ a)) ==> 0
372 bool RewriteRule
<BitwiseNotAnd
>::applies(Node node
) {
373 return (node
.getKind() == kind::BITVECTOR_AND
&&
374 ((node
[0].getKind() == kind::BITVECTOR_NOT
&& node
[0][0] == node
[1]) ||
375 (node
[1].getKind() == kind::BITVECTOR_NOT
&& node
[1][0] == node
[0])));
379 Node RewriteRule
<BitwiseNotAnd
>::apply(Node node
) {
380 BVDebug("bv-rewrite") << "RewriteRule<BitwiseNegAnd>(" << node
<< ")" << std::endl
;
381 return utils::mkConst(BitVector(utils::getSize(node
), Integer(0)));
387 * (a bvor (~ a)) ==> 1
391 bool RewriteRule
<BitwiseNotOr
>::applies(Node node
) {
392 return (node
.getKind() == kind::BITVECTOR_OR
&&
393 ((node
[0].getKind() == kind::BITVECTOR_NOT
&& node
[0][0] == node
[1]) ||
394 (node
[1].getKind() == kind::BITVECTOR_NOT
&& node
[1][0] == node
[0])));
398 Node RewriteRule
<BitwiseNotOr
>::apply(Node node
) {
399 BVDebug("bv-rewrite") << "RewriteRule<BitwiseNotOr>(" << node
<< ")" << std::endl
;
400 uint32_t size
= utils::getSize(node
);
401 Integer ones
= Integer(1).multiplyByPow2(size
) - 1;
402 return utils::mkConst(BitVector(size
, ones
));
408 * ((~ a) bvxor (~ b)) ==> (a bvxor b)
412 bool RewriteRule
<XorNot
>::applies(Node node
) {
413 return (node
.getKind() == kind::BITVECTOR_XOR
&&
414 node
[0].getKind() == kind::BITVECTOR_NOT
&&
415 node
[1].getKind() == kind::BITVECTOR_NOT
);
419 Node RewriteRule
<XorNot
>::apply(Node node
) {
420 BVDebug("bv-rewrite") << "RewriteRule<XorNot>(" << node
<< ")" << std::endl
;
423 return utils::mkNode(kind::BITVECTOR_XOR
, a
, b
);
429 * ~(a bvxor b) ==> (~ a bvxor b)
433 bool RewriteRule
<NotXor
>::applies(Node node
) {
434 return (node
.getKind() == kind::BITVECTOR_NOT
&&
435 node
[0].getKind() == kind::BITVECTOR_XOR
);
439 Node RewriteRule
<NotXor
>::apply(Node node
) {
440 BVDebug("bv-rewrite") << "RewriteRule<XorNot>(" << node
<< ")" << std::endl
;
443 Node nota
= utils::mkNode(kind::BITVECTOR_NOT
, a
);
444 return utils::mkSortedNode(kind::BITVECTOR_XOR
, nota
, b
);
454 bool RewriteRule
<NotIdemp
>::applies(Node node
) {
455 return (node
.getKind() == kind::BITVECTOR_NOT
&&
456 node
[0].getKind() == kind::BITVECTOR_NOT
);
460 Node RewriteRule
<NotIdemp
>::apply(Node node
) {
461 BVDebug("bv-rewrite") << "RewriteRule<XorIdemp>(" << node
<< ")" << std::endl
;
474 bool RewriteRule
<LtSelf
>::applies(Node node
) {
475 return ((node
.getKind() == kind::BITVECTOR_ULT
||
476 node
.getKind() == kind::BITVECTOR_SLT
) &&
481 Node RewriteRule
<LtSelf
>::apply(Node node
) {
482 BVDebug("bv-rewrite") << "RewriteRule<LtSelf>(" << node
<< ")" << std::endl
;
483 return utils::mkFalse();
493 bool RewriteRule
<LteSelf
>::applies(Node node
) {
494 return ((node
.getKind() == kind::BITVECTOR_ULE
||
495 node
.getKind() == kind::BITVECTOR_SLE
) &&
500 Node RewriteRule
<LteSelf
>::apply(Node node
) {
501 BVDebug("bv-rewrite") << "RewriteRule<LteSelf>(" << node
<< ")" << std::endl
;
502 return utils::mkTrue();
512 bool RewriteRule
<UltZero
>::applies(Node node
) {
513 return (node
.getKind() == kind::BITVECTOR_ULT
&&
514 node
[1] == utils::mkConst(BitVector(utils::getSize(node
[0]), Integer(0))));
518 Node RewriteRule
<UltZero
>::apply(Node node
) {
519 BVDebug("bv-rewrite") << "RewriteRule<UltZero>(" << node
<< ")" << std::endl
;
520 return utils::mkFalse();
530 bool RewriteRule
<UltSelf
>::applies(Node node
) {
531 return (node
.getKind() == kind::BITVECTOR_ULT
&&
536 Node RewriteRule
<UltSelf
>::apply(Node node
) {
537 BVDebug("bv-rewrite") << "RewriteRule<UltSelf>(" << node
<< ")" << std::endl
;
538 return utils::mkFalse();
549 bool RewriteRule
<UleZero
>::applies(Node node
) {
550 return (node
.getKind() == kind::BITVECTOR_ULE
&&
551 node
[1] == utils::mkConst(BitVector(utils::getSize(node
[0]), Integer(0))));
555 Node RewriteRule
<UleZero
>::apply(Node node
) {
556 BVDebug("bv-rewrite") << "RewriteRule<UleZero>(" << node
<< ")" << std::endl
;
557 return utils::mkNode(kind::EQUAL
, node
[0], node
[1]);
567 bool RewriteRule
<UleSelf
>::applies(Node node
) {
568 return (node
.getKind() == kind::BITVECTOR_ULE
&&
573 Node RewriteRule
<UleSelf
>::apply(Node node
) {
574 BVDebug("bv-rewrite") << "RewriteRule<UleSelf>(" << node
<< ")" << std::endl
;
575 return utils::mkTrue();
586 bool RewriteRule
<ZeroUle
>::applies(Node node
) {
587 return (node
.getKind() == kind::BITVECTOR_ULE
&&
588 node
[0] == utils::mkConst(BitVector(utils::getSize(node
[0]), Integer(0))));
592 Node RewriteRule
<ZeroUle
>::apply(Node node
) {
593 BVDebug("bv-rewrite") << "RewriteRule<ZeroUle>(" << node
<< ")" << std::endl
;
594 return utils::mkTrue();
600 * a <= 11..1 ==> true
604 bool RewriteRule
<UleMax
>::applies(Node node
) {
605 if (node
.getKind()!= kind::BITVECTOR_ULE
) {
608 uint32_t size
= utils::getSize(node
[0]);
609 Integer ones
= Integer(1).multiplyByPow2(size
) -1;
610 return (node
.getKind() == kind::BITVECTOR_ULE
&&
611 node
[1] == utils::mkConst(BitVector(size
, ones
)));
615 Node RewriteRule
<UleMax
>::apply(Node node
) {
616 BVDebug("bv-rewrite") << "RewriteRule<UleMax>(" << node
<< ")" << std::endl
;
617 return utils::mkTrue();
623 * ~ ( a < b) ==> b <= a
627 bool RewriteRule
<NotUlt
>::applies(Node node
) {
628 return (node
.getKind() == kind::NOT
&&
629 node
[0].getKind() == kind::BITVECTOR_ULT
);
633 Node RewriteRule
<NotUlt
>::apply(Node node
) {
634 BVDebug("bv-rewrite") << "RewriteRule<NotUlt>(" << node
<< ")" << std::endl
;
638 return utils::mkNode(kind::BITVECTOR_ULE
, b
, a
);
644 * ~ ( a <= b) ==> b < a
648 bool RewriteRule
<NotUle
>::applies(Node node
) {
649 return (node
.getKind() == kind::NOT
&&
650 node
[0].getKind() == kind::BITVECTOR_ULE
);
654 Node RewriteRule
<NotUle
>::apply(Node node
) {
655 BVDebug("bv-rewrite") << "RewriteRule<NotUle>(" << node
<< ")" << std::endl
;
659 return utils::mkNode(kind::BITVECTOR_ULT
, b
, a
);
669 bool RewriteRule
<MultOne
>::applies(Node node
) {
670 unsigned size
= utils::getSize(node
);
671 return (node
.getKind() == kind::BITVECTOR_MULT
&&
672 (node
[0] == utils::mkConst(size
, 1) ||
673 node
[1] == utils::mkConst(size
, 1)));
677 Node RewriteRule
<MultOne
>::apply(Node node
) {
678 BVDebug("bv-rewrite") << "RewriteRule<MultOne>(" << node
<< ")" << std::endl
;
679 unsigned size
= utils::getSize(node
);
680 if (node
[0] == utils::mkConst(size
, 1)) {
683 Assert(node
[1] == utils::mkConst(size
, 1));
694 bool RewriteRule
<MultZero
>::applies(Node node
) {
695 unsigned size
= utils::getSize(node
);
696 return (node
.getKind() == kind::BITVECTOR_MULT
&&
697 (node
[0] == utils::mkConst(size
, 0) ||
698 node
[1] == utils::mkConst(size
, 0)));
702 Node RewriteRule
<MultZero
>::apply(Node node
) {
703 BVDebug("bv-rewrite") << "RewriteRule<MultZero>(" << node
<< ")" << std::endl
;
704 return utils::mkConst(utils::getSize(node
), 0);
710 * (a * 2^k) ==> a[n-k-1:0] 0_k
714 bool RewriteRule
<MultPow2
>::applies(Node node
) {
715 if (node
.getKind() != kind::BITVECTOR_MULT
)
718 for(unsigned i
= 0; i
< node
.getNumChildren(); ++i
) {
719 if (utils::isPow2Const(node
[i
])) {
727 Node RewriteRule
<MultPow2
>::apply(Node node
) {
728 BVDebug("bv-rewrite") << "RewriteRule<MultPow2>(" << node
<< ")" << std::endl
;
730 std::vector
<Node
> children
;
731 unsigned exponent
= 0;
732 for(unsigned i
= 0; i
< node
.getNumChildren(); ++i
) {
733 unsigned exp
= utils::isPow2Const(node
[i
]);
738 children
.push_back(node
[i
]);
742 Node a
= utils::mkSortedNode(kind::BITVECTOR_MULT
, children
);
744 Node extract
= utils::mkExtract(a
, utils::getSize(node
) - exponent
- 1, 0);
745 Node zeros
= utils::mkConst(exponent
, 0);
746 return utils::mkConcat(extract
, zeros
);
756 bool RewriteRule
<PlusZero
>::applies(Node node
) {
757 Node zero
= utils::mkConst(utils::getSize(node
), 0);
758 return (node
.getKind() == kind::BITVECTOR_PLUS
&&
764 Node RewriteRule
<PlusZero
>::apply(Node node
) {
765 BVDebug("bv-rewrite") << "RewriteRule<PlusZero>(" << node
<< ")" << std::endl
;
766 Node zero
= utils::mkConst(utils::getSize(node
), 0);
767 if (node
[0] == zero
) {
781 bool RewriteRule
<NegIdemp
>::applies(Node node
) {
782 return (node
.getKind() == kind::BITVECTOR_NEG
&&
783 node
[0].getKind() == kind::BITVECTOR_NEG
);
787 Node RewriteRule
<NegIdemp
>::apply(Node node
) {
788 BVDebug("bv-rewrite") << "RewriteRule<NegIdemp>(" << node
<< ")" << std::endl
;
795 * (a udiv 2^k) ==> 0_k a[n-1: k]
799 bool RewriteRule
<UdivPow2
>::applies(Node node
) {
800 return (node
.getKind() == kind::BITVECTOR_UDIV
&&
801 utils::isPow2Const(node
[1]));
805 Node RewriteRule
<UdivPow2
>::apply(Node node
) {
806 BVDebug("bv-rewrite") << "RewriteRule<UdivPow2>(" << node
<< ")" << std::endl
;
808 unsigned power
= utils::isPow2Const(node
[1]) -1;
810 Node extract
= utils::mkExtract(a
, utils::getSize(node
) - 1, power
);
811 Node zeros
= utils::mkConst(power
, 0);
813 return utils::mkNode(kind::BITVECTOR_CONCAT
, zeros
, extract
);
823 bool RewriteRule
<UdivOne
>::applies(Node node
) {
824 return (node
.getKind() == kind::BITVECTOR_UDIV
&&
825 node
[1] == utils::mkConst(utils::getSize(node
), 1));
829 Node RewriteRule
<UdivOne
>::apply(Node node
) {
830 BVDebug("bv-rewrite") << "RewriteRule<UdivOne>(" << node
<< ")" << std::endl
;
841 bool RewriteRule
<UdivSelf
>::applies(Node node
) {
842 return (node
.getKind() == kind::BITVECTOR_UDIV
&&
847 Node RewriteRule
<UdivSelf
>::apply(Node node
) {
848 BVDebug("bv-rewrite") << "RewriteRule<UdivSelf>(" << node
<< ")" << std::endl
;
849 return utils::mkConst(utils::getSize(node
), 1);
855 * (a urem 2^k) ==> 0_(n-k) a[k-1:0]
859 bool RewriteRule
<UremPow2
>::applies(Node node
) {
860 return (node
.getKind() == kind::BITVECTOR_UREM
&&
861 utils::isPow2Const(node
[1]));
865 Node RewriteRule
<UremPow2
>::apply(Node node
) {
866 BVDebug("bv-rewrite") << "RewriteRule<UremPow2>(" << node
<< ")" << std::endl
;
868 unsigned power
= utils::isPow2Const(node
[1]) - 1;
870 return utils::mkConst(utils::getSize(node
), 0);
872 Node extract
= utils::mkExtract(a
, power
- 1, 0);
873 Node zeros
= utils::mkConst(utils::getSize(node
) - power
, 0);
874 return utils::mkNode(kind::BITVECTOR_CONCAT
, zeros
, extract
);
884 bool RewriteRule
<UremOne
>::applies(Node node
) {
885 return (node
.getKind() == kind::BITVECTOR_UREM
&&
886 node
[1] == utils::mkConst(utils::getSize(node
), 1));
890 Node RewriteRule
<UremOne
>::apply(Node node
) {
891 BVDebug("bv-rewrite") << "RewriteRule<UremOne>(" << node
<< ")" << std::endl
;
892 return utils::mkConst(utils::getSize(node
), 0);
902 bool RewriteRule
<UremSelf
>::applies(Node node
) {
903 return (node
.getKind() == kind::BITVECTOR_UREM
&&
908 Node RewriteRule
<UremSelf
>::apply(Node node
) {
909 BVDebug("bv-rewrite") << "RewriteRule<UremSelf>(" << node
<< ")" << std::endl
;
910 return utils::mkConst(utils::getSize(node
), 0);
920 bool RewriteRule
<ShiftZero
>::applies(Node node
) {
921 return ((node
.getKind() == kind::BITVECTOR_SHL
||
922 node
.getKind() == kind::BITVECTOR_LSHR
||
923 node
.getKind() == kind::BITVECTOR_ASHR
) &&
924 node
[0] == utils::mkConst(utils::getSize(node
), 0));
928 Node RewriteRule
<ShiftZero
>::apply(Node node
) {
929 BVDebug("bv-rewrite") << "RewriteRule<ShiftZero>(" << node
<< ")" << std::endl
;
936 * -a1 - a2 - ... - an + ak + .. ==> - (a1 + a2 + ... + an) + ak
941 bool RewriteRule
<BBPlusNeg
>::applies(Node node
) {
942 if (node
.getKind() != kind::BITVECTOR_PLUS
) {
946 unsigned neg_count
= 0;
947 for(unsigned i
= 0; i
< node
.getNumChildren(); ++i
) {
948 if (node
[i
].getKind()== kind::BITVECTOR_NEG
) {
952 return neg_count
> 1;
956 Node RewriteRule
<BBPlusNeg
>::apply(Node node
) {
957 BVDebug("bv-rewrite") << "RewriteRule<BBPlusNeg>(" << node
<< ")" << std::endl
;
959 std::vector
<Node
> children
;
960 unsigned neg_count
= 0;
961 for(unsigned i
= 0; i
< node
.getNumChildren(); ++i
) {
962 if (node
[i
].getKind() == kind::BITVECTOR_NEG
) {
964 children
.push_back(utils::mkNode(kind::BITVECTOR_NOT
, node
[i
][0]));
966 children
.push_back(node
[i
]);
969 Assert(neg_count
!= 0);
970 children
.push_back(utils::mkConst(utils::getSize(node
), neg_count
));
972 return utils::mkSortedNode(kind::BITVECTOR_PLUS
, children
);
982 // bool RewriteRule<BBFactorOut>::applies(Node node) {
983 // if (node.getKind() != kind::BITVECTOR_PLUS) {
987 // for (unsigned i = 0; i < node.getNumChildren(); ++i) {
988 // if (node[i].getKind() != kind::BITVECTOR_MULT) {
995 // Node RewriteRule<BBFactorOut>::apply(Node node) {
996 // BVDebug("bv-rewrite") << "RewriteRule<BBFactorOut>(" << node << ")" << std::endl;
997 // std::hash_set<TNode, TNodeHashFunction> factors;
999 // for (unsigned i = 0; i < node.getNumChildren(); ++i) {
1000 // Assert (node[i].getKind() == kind::BITVECTOR_MULT);
1001 // for (unsigned j = 0; j < node[i].getNumChildren(); ++j) {
1002 // factors.insert(node[i][j]);
1006 // std::vector<TNode> gcd;
1007 // std::hash_set<TNode, TNodeHashFunction>::const_iterator it;
1008 // for (it = factors.begin(); it != factors.end(); ++it) {
1009 // // for each factor check if it occurs in all children
1011 // for (unsigned i = 0; i < node.getNumChildren
1025 // template<> inline
1026 // bool RewriteRule<>::applies(Node node) {
1027 // return (node.getKind() == );
1030 // template<> inline
1031 // Node RewriteRule<>::apply(Node node) {
1032 // BVDebug("bv-rewrite") << "RewriteRule<>(" << node << ")" << std::endl;