1 /********************* */
2 /*! \file theory_bv_rewrite_rules_simplification.h
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
12 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
18 #include "cvc4_private.h"
22 #include "theory/bv/theory_bv_rewrite_rules.h"
23 #include "theory/bv/theory_bv_utils.h"
29 // FIXME: this rules subsume the constant evaluation ones
35 * Left Shift by constant amount
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
);
45 Node RewriteRule
<ShlByConst
>::apply(TNode node
) {
46 Debug("bv-rewrite") << "RewriteRule<ShlByConst>(" << node
<< ")" << std::endl
;
47 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();
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
);
73 * Right Logical Shift by constant amount
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
);
84 Node RewriteRule
<LshrByConst
>::apply(TNode node
) {
85 Debug("bv-rewrite") << "RewriteRule<LshrByConst>(" << node
<< ")" << std::endl
;
86 Integer amount
= node
[1].getConst
<BitVector
>().toInteger();
92 uint32_t size
= utils::getSize(a
);
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)));
100 // make sure we do not lose information casting
101 Assert(amount
< Integer(1).multiplyByPow2(32));
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
);
112 * Right Arithmetic Shift by constant amount
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
);
123 Node RewriteRule
<AshrByConst
>::apply(TNode node
) {
124 Debug("bv-rewrite") << "RewriteRule<AshrByConst>(" << node
<< ")" << std::endl
;
125 Integer amount
= node
[1].getConst
<BitVector
>().toInteger();
131 uint32_t size
= utils::getSize(a
);
132 Node sign_bit
= utils::mkExtract(a
, size
-1, size
-1);
134 if (amount
>= Integer(size
)) {
135 // if we are shifting more than the length of the bitvector return n repetitions
137 return utils::mkConcat(sign_bit
, size
);
140 // make sure we do not lose information casting
141 Assert(amount
< Integer(1).multiplyByPow2(32));
143 uint32_t uint32_amount
= amount
.toUnsignedInt();
144 if (uint32_amount
== 0) {
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
);
161 bool RewriteRule
<BitwiseIdemp
>::applies(TNode node
) {
163 return ((node
.getKind() == kind::BITVECTOR_AND
||
164 node
.getKind() == kind::BITVECTOR_OR
) &&
165 node
.getNumChildren() == 2 &&
170 Node RewriteRule
<BitwiseIdemp
>::apply(TNode node
) {
172 Debug("bv-rewrite") << "RewriteRule<BitwiseIdemp>(" << node
<< ")" << std::endl
;
183 bool RewriteRule
<AndZero
>::applies(TNode node
) {
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)));
193 Node RewriteRule
<AndZero
>::apply(TNode node
) {
195 Debug("bv-rewrite") << "RewriteRule<AndZero>(" << node
<< ")" << std::endl
;
196 return utils::mkConst(utils::getSize(node
), 0);
206 bool RewriteRule
<AndOne
>::applies(TNode node
) {
208 unsigned size
= utils::getSize(node
);
209 Node ones
= utils::mkOnes(size
);
210 return (node
.getKind() == kind::BITVECTOR_AND
&&
211 node
.getNumChildren() == 2 &&
217 Node RewriteRule
<AndOne
>::apply(TNode node
) {
219 Debug("bv-rewrite") << "RewriteRule<AndOne>(" << node
<< ")" << std::endl
;
220 unsigned size
= utils::getSize(node
);
222 if (node
[0] == utils::mkOnes(size
)) {
225 Assert (node
[1] == utils::mkOnes(size
));
237 bool RewriteRule
<OrZero
>::applies(TNode node
) {
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)));
247 Node RewriteRule
<OrZero
>::apply(TNode node
) {
249 Debug("bv-rewrite") << "RewriteRule<OrZero>(" << node
<< ")" << std::endl
;
251 unsigned size
= utils::getSize(node
);
252 if (node
[0] == utils::mkConst(size
, 0)) {
255 Assert(node
[1] == utils::mkConst(size
, 0));
267 bool RewriteRule
<OrOne
>::applies(TNode node
) {
269 unsigned size
= utils::getSize(node
);
270 Node ones
= utils::mkOnes(size
);
271 return (node
.getKind() == kind::BITVECTOR_OR
&&
272 node
.getNumChildren() == 2 &&
278 Node RewriteRule
<OrOne
>::apply(TNode node
) {
280 Debug("bv-rewrite") << "RewriteRule<OrOne>(" << node
<< ")" << std::endl
;
281 return utils::mkOnes(utils::getSize(node
));
292 bool RewriteRule
<XorDuplicate
>::applies(TNode node
) {
294 return (node
.getKind() == kind::BITVECTOR_XOR
&&
295 node
.getNumChildren() == 2 &&
300 Node RewriteRule
<XorDuplicate
>::apply(TNode node
) {
302 Debug("bv-rewrite") << "RewriteRule<XorDuplicate>(" << node
<< ")" << std::endl
;
303 return utils::mkConst(BitVector(utils::getSize(node
), Integer(0)));
313 bool RewriteRule
<XorOne
>::applies(TNode node
) {
314 if (node
.getKind() != kind::BITVECTOR_XOR
) {
317 Node ones
= utils::mkOnes(utils::getSize(node
));
318 for (unsigned i
= 0; i
< node
.getNumChildren(); ++i
) {
319 if (node
[i
] == ones
) {
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
;
338 children
.push_back(node
[i
]);
342 Node result
= utils::mkNode(kind::BITVECTOR_XOR
, children
);
344 result
= utils::mkNode(kind::BITVECTOR_NOT
, result
);
357 bool RewriteRule
<XorZero
>::applies(TNode node
) {
358 if (node
.getKind() != kind::BITVECTOR_XOR
) {
361 Node zero
= utils::mkConst(utils::getSize(node
), 0);
362 for (unsigned i
= 0; i
< node
.getNumChildren(); ++i
) {
363 if (node
[i
] == zero
) {
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);
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
]);
382 Node res
= utils::mkNode(kind::BITVECTOR_XOR
, children
);
390 * (a bvand (~ a)) ==> 0
394 bool RewriteRule
<BitwiseNotAnd
>::applies(TNode node
) {
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])));
403 Node RewriteRule
<BitwiseNotAnd
>::apply(TNode node
) {
405 Debug("bv-rewrite") << "RewriteRule<BitwiseNegAnd>(" << node
<< ")" << std::endl
;
406 return utils::mkConst(BitVector(utils::getSize(node
), Integer(0)));
412 * (a bvor (~ a)) ==> 1
416 bool RewriteRule
<BitwiseNotOr
>::applies(TNode node
) {
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])));
425 Node RewriteRule
<BitwiseNotOr
>::apply(TNode node
) {
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
));
436 * ((~ a) bvxor (~ b)) ==> (a bvxor b)
440 bool RewriteRule
<XorNot
>::applies(TNode node
) {
445 Node RewriteRule
<XorNot
>::apply(TNode node
) {
447 Debug("bv-rewrite") << "RewriteRule<XorNot>(" << node
<< ")" << std::endl
;
450 return utils::mkNode(kind::BITVECTOR_XOR
, a
, b
);
456 * ~(a bvxor b) ==> (~ a bvxor b)
460 bool RewriteRule
<NotXor
>::applies(TNode node
) {
461 return (node
.getKind() == kind::BITVECTOR_NOT
&&
462 node
[0].getKind() == kind::BITVECTOR_XOR
);
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
);
474 return utils::mkSortedNode(kind::BITVECTOR_XOR
, children
);
484 bool RewriteRule
<NotIdemp
>::applies(TNode node
) {
485 return (node
.getKind() == kind::BITVECTOR_NOT
&&
486 node
[0].getKind() == kind::BITVECTOR_NOT
);
490 Node RewriteRule
<NotIdemp
>::apply(TNode node
) {
491 Debug("bv-rewrite") << "RewriteRule<NotIdemp>(" << node
<< ")" << std::endl
;
504 bool RewriteRule
<LtSelf
>::applies(TNode node
) {
505 return ((node
.getKind() == kind::BITVECTOR_ULT
||
506 node
.getKind() == kind::BITVECTOR_SLT
) &&
511 Node RewriteRule
<LtSelf
>::apply(TNode node
) {
512 Debug("bv-rewrite") << "RewriteRule<LtSelf>(" << node
<< ")" << std::endl
;
513 return utils::mkFalse();
523 bool RewriteRule
<LteSelf
>::applies(TNode node
) {
524 return ((node
.getKind() == kind::BITVECTOR_ULE
||
525 node
.getKind() == kind::BITVECTOR_SLE
) &&
530 Node RewriteRule
<LteSelf
>::apply(TNode node
) {
531 Debug("bv-rewrite") << "RewriteRule<LteSelf>(" << node
<< ")" << std::endl
;
532 return utils::mkTrue();
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))));
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]));
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))));
567 Node RewriteRule
<UltZero
>::apply(TNode node
) {
568 Debug("bv-rewrite") << "RewriteRule<UltZero>(" << node
<< ")" << std::endl
;
569 return utils::mkFalse();
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))));
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)));
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))));
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));
604 return utils::mkNode(kind::EQUAL
, most_significant_bit
, one
);
615 bool RewriteRule
<UltSelf
>::applies(TNode node
) {
616 return (node
.getKind() == kind::BITVECTOR_ULT
&&
621 Node RewriteRule
<UltSelf
>::apply(TNode node
) {
622 Debug("bv-rewrite") << "RewriteRule<UltSelf>(" << node
<< ")" << std::endl
;
623 return utils::mkFalse();
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))));
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]);
652 bool RewriteRule
<UleSelf
>::applies(TNode node
) {
653 return (node
.getKind() == kind::BITVECTOR_ULE
&&
658 Node RewriteRule
<UleSelf
>::apply(TNode node
) {
659 Debug("bv-rewrite") << "RewriteRule<UleSelf>(" << node
<< ")" << std::endl
;
660 return utils::mkTrue();
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))));
677 Node RewriteRule
<ZeroUle
>::apply(TNode node
) {
678 Debug("bv-rewrite") << "RewriteRule<ZeroUle>(" << node
<< ")" << std::endl
;
679 return utils::mkTrue();
685 * a <= 11..1 ==> true
689 bool RewriteRule
<UleMax
>::applies(TNode node
) {
690 if (node
.getKind()!= kind::BITVECTOR_ULE
) {
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
)));
700 Node RewriteRule
<UleMax
>::apply(TNode node
) {
701 Debug("bv-rewrite") << "RewriteRule<UleMax>(" << node
<< ")" << std::endl
;
702 return utils::mkTrue();
708 * ~ ( a < b) ==> b <= a
712 bool RewriteRule
<NotUlt
>::applies(TNode node
) {
713 return (node
.getKind() == kind::NOT
&&
714 node
[0].getKind() == kind::BITVECTOR_ULT
);
718 Node RewriteRule
<NotUlt
>::apply(TNode node
) {
719 Debug("bv-rewrite") << "RewriteRule<NotUlt>(" << node
<< ")" << std::endl
;
723 return utils::mkNode(kind::BITVECTOR_ULE
, b
, a
);
729 * ~ ( a <= b) ==> b < a
733 bool RewriteRule
<NotUle
>::applies(TNode node
) {
734 return (node
.getKind() == kind::NOT
&&
735 node
[0].getKind() == kind::BITVECTOR_ULE
);
739 Node RewriteRule
<NotUle
>::apply(TNode node
) {
740 Debug("bv-rewrite") << "RewriteRule<NotUle>(" << node
<< ")" << std::endl
;
744 return utils::mkNode(kind::BITVECTOR_ULT
, b
, a
);
750 * (a * 2^k) ==> a[n-k-1:0] 0_k
754 bool RewriteRule
<MultPow2
>::applies(TNode node
) {
755 if (node
.getKind() != kind::BITVECTOR_MULT
)
758 for(unsigned i
= 0; i
< node
.getNumChildren(); ++i
) {
759 if (utils::isPow2Const(node
[i
])) {
767 Node RewriteRule
<MultPow2
>::apply(TNode node
) {
768 Debug("bv-rewrite") << "RewriteRule<MultPow2>(" << node
<< ")" << std::endl
;
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
]);
778 children
.push_back(node
[i
]);
782 Node a
= utils::mkNode(kind::BITVECTOR_MULT
, children
);
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
);
790 * ExtractMultLeadingBit
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
800 bool RewriteRule
<ExtractMultLeadingBit
>::applies(TNode node
) {
801 if (node
.getKind() != kind::BITVECTOR_EXTRACT
)
803 unsigned low
= utils::getExtractLow(node
);
806 if (node
.getKind() != kind::BITVECTOR_MULT
||
807 node
.getNumChildren() != 2 ||
808 utils::getSize(node
) <= 64)
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())
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]) :
824 unsigned zeroes2
= int2
.isZero()? utils::getSize(node
[1][0]) :
827 // first k bits are not zero in the result
828 unsigned k
= 2 * n
- (zeroes1
+ zeroes2
);
837 Node RewriteRule
<ExtractMultLeadingBit
>::apply(TNode node
) {
838 Debug("bv-rewrite") << "RewriteRule<MultLeadingBit>(" << node
<< ")" << std::endl
;
840 unsigned bitwidth
= utils::getSize(node
);
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]) :
848 // unsigned zeroes2 = int2.isZero()? utils::getSize(node[1][0]) :
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);
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),
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";
874 bool RewriteRule
<NegIdemp
>::applies(TNode node
) {
875 return (node
.getKind() == kind::BITVECTOR_NEG
&&
876 node
[0].getKind() == kind::BITVECTOR_NEG
);
880 Node RewriteRule
<NegIdemp
>::apply(TNode node
) {
881 Debug("bv-rewrite") << "RewriteRule<NegIdemp>(" << node
<< ")" << std::endl
;
888 * (a udiv 2^k) ==> 0_k a[n-1: k]
892 bool RewriteRule
<UdivPow2
>::applies(TNode node
) {
893 return (node
.getKind() == kind::BITVECTOR_UDIV_TOTAL
&&
894 utils::isPow2Const(node
[1]));
898 Node RewriteRule
<UdivPow2
>::apply(TNode node
) {
899 Debug("bv-rewrite") << "RewriteRule<UdivPow2>(" << node
<< ")" << std::endl
;
901 unsigned power
= utils::isPow2Const(node
[1]) -1;
905 Node extract
= utils::mkExtract(a
, utils::getSize(node
) - 1, power
);
906 Node zeros
= utils::mkConst(power
, 0);
908 return utils::mkNode(kind::BITVECTOR_CONCAT
, zeros
, extract
);
918 bool RewriteRule
<UdivOne
>::applies(TNode node
) {
919 return (node
.getKind() == kind::BITVECTOR_UDIV_TOTAL
&&
920 node
[1] == utils::mkConst(utils::getSize(node
), 1));
924 Node RewriteRule
<UdivOne
>::apply(TNode node
) {
925 Debug("bv-rewrite") << "RewriteRule<UdivOne>(" << node
<< ")" << std::endl
;
936 bool RewriteRule
<UdivSelf
>::applies(TNode node
) {
937 return (node
.getKind() == kind::BITVECTOR_UDIV_TOTAL
&&
942 Node RewriteRule
<UdivSelf
>::apply(TNode node
) {
943 Debug("bv-rewrite") << "RewriteRule<UdivSelf>(" << node
<< ")" << std::endl
;
944 return utils::mkConst(utils::getSize(node
), 1);
950 * (a urem 2^k) ==> 0_(n-k) a[k-1:0]
954 bool RewriteRule
<UremPow2
>::applies(TNode node
) {
955 return (node
.getKind() == kind::BITVECTOR_UREM_TOTAL
&&
956 utils::isPow2Const(node
[1]));
960 Node RewriteRule
<UremPow2
>::apply(TNode node
) {
961 Debug("bv-rewrite") << "RewriteRule<UremPow2>(" << node
<< ")" << std::endl
;
963 unsigned power
= utils::isPow2Const(node
[1]) - 1;
965 return utils::mkConst(utils::getSize(node
), 0);
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
);
979 bool RewriteRule
<UremOne
>::applies(TNode node
) {
980 return (node
.getKind() == kind::BITVECTOR_UREM_TOTAL
&&
981 node
[1] == utils::mkConst(utils::getSize(node
), 1));
985 Node RewriteRule
<UremOne
>::apply(TNode node
) {
986 Debug("bv-rewrite") << "RewriteRule<UremOne>(" << node
<< ")" << std::endl
;
987 return utils::mkConst(utils::getSize(node
), 0);
997 bool RewriteRule
<UremSelf
>::applies(TNode node
) {
998 return (node
.getKind() == kind::BITVECTOR_UREM_TOTAL
&&
1003 Node RewriteRule
<UremSelf
>::apply(TNode node
) {
1004 Debug("bv-rewrite") << "RewriteRule<UremSelf>(" << node
<< ")" << std::endl
;
1005 return utils::mkConst(utils::getSize(node
), 0);
1011 * (0_k >> a) ==> 0_k
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));
1023 Node RewriteRule
<ShiftZero
>::apply(TNode node
) {
1024 Debug("bv-rewrite") << "RewriteRule<ShiftZero>(" << node
<< ")" << std::endl
;
1031 * -a1 - a2 - ... - an + ak + .. ==> - (a1 + a2 + ... + an) + ak
1036 bool RewriteRule
<BBPlusNeg
>::applies(TNode node
) {
1037 if (node
.getKind() != kind::BITVECTOR_PLUS
) {
1041 unsigned neg_count
= 0;
1042 for(unsigned i
= 0; i
< node
.getNumChildren(); ++i
) {
1043 if (node
[i
].getKind()== kind::BITVECTOR_NEG
) {
1047 return neg_count
> 1;
1051 Node RewriteRule
<BBPlusNeg
>::apply(TNode node
) {
1052 Debug("bv-rewrite") << "RewriteRule<BBPlusNeg>(" << node
<< ")" << std::endl
;
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
) {
1059 children
.push_back(utils::mkNode(kind::BITVECTOR_NOT
, node
[i
][0]));
1061 children
.push_back(node
[i
]);
1064 Assert(neg_count
!= 0);
1065 children
.push_back(utils::mkConst(utils::getSize(node
), neg_count
));
1067 return utils::mkNode(kind::BITVECTOR_PLUS
, children
);
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
))
1080 Node RewriteRule
<MergeSignExtend
>::apply(TNode node
) {
1081 Debug("bv-rewrite") << "RewriteRule<MergeSignExtend>(" << node
<< ")" << std::endl
;
1082 unsigned ammount1
= node
.getOperator().getConst
<BitVectorSignExtend
>().signExtendAmount
;
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];
1094 NodeBuilder
<> nb(kind::BITVECTOR_ZERO_EXTEND
);
1095 Node op
= nm
->mkConst
<BitVectorZeroExtend
>(BitVectorZeroExtend(ammount1
+ ammount2
));
1096 nb
<< op
<< node
[0][0];
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];
1111 bool RewriteRule
<MultSlice
>::applies(TNode node
) {
1112 if (node
.getKind() != kind::BITVECTOR_MULT
) {
1115 if (utils::getSize(node
[0]) % 2 != 0) {
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!).
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);
1136 Node bottom_a
= utils::mkExtract(a
, bitwidth
/2 - 1, 0);
1137 Node top_a
= utils::mkExtract(a
, bitwidth
-1, bitwidth
/2);
1139 Node bottom_b
= utils::mkExtract(b
, bitwidth
/2 - 1, 0);
1140 Node top_b
= utils::mkExtract(b
, bitwidth
-1, bitwidth
/2);
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
));
1146 Node term2
= utils::mkNode(kind::BITVECTOR_CONCAT
,
1147 utils::mkNode(kind::BITVECTOR_MULT
, top_b
, bottom_a
),
1149 Node term3
= utils::mkNode(kind::BITVECTOR_CONCAT
,
1150 utils::mkNode(kind::BITVECTOR_MULT
, top_a
, bottom_b
),
1152 return utils::mkNode(kind::BITVECTOR_PLUS
, term1
, term2
, term3
);
1156 * x < y + 1 <=> (not y < x) and y != 1...1
1163 bool RewriteRule
<UltPlusOne
>::applies(TNode node
) {
1164 if (node
.getKind() != kind::BITVECTOR_ULT
) return false;
1167 if (y1
.getKind() != kind::BITVECTOR_PLUS
) return false;
1168 if (y1
[0].getKind() != kind::CONST_BITVECTOR
&&
1169 y1
[1].getKind() != kind::CONST_BITVECTOR
)
1172 if (y1
[0].getKind() == kind::CONST_BITVECTOR
&&
1173 y1
[1].getKind() == kind::CONST_BITVECTOR
)
1176 if (y1
.getNumChildren() != 2)
1179 TNode one
= y1
[0].getKind() == kind::CONST_BITVECTOR
? y1
[0] : y1
[1];
1180 if (one
!= utils::mkConst(utils::getSize(one
), 1)) return false;
1185 Node RewriteRule
<UltPlusOne
>::apply(TNode node
) {
1186 Debug("bv-rewrite") << "RewriteRule<UltPlusOne>(" << node
<< ")" << std::endl
;
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
);
1197 * x ^(x-1) = 0 => 1 << sk
1198 * WARNING: this is an **EQUISATISFIABLE** transformation!
1199 * Only to be called on top level assertions.
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
)
1211 if (!utils::isZero(node
[0]) &&
1212 !utils::isZero(node
[1]))
1215 TNode t
= !utils::isZero(node
[0])? node
[0]: node
[1];
1216 if (t
.getNumChildren() != 2) return false;
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
)));
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];
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
);