1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Liana Hadarean, Aina Niemetz, Mathias Preiner |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* [[ Add one-line brief description here ]] |
14 |
|
* |
15 |
|
* [[ Add lengthier description here ]] |
16 |
|
* \todo document this file |
17 |
|
*/ |
18 |
|
|
19 |
|
#include "cvc5_private.h" |
20 |
|
|
21 |
|
#pragma once |
22 |
|
|
23 |
|
#include "options/bv_options.h" |
24 |
|
#include "theory/bv/theory_bv_rewrite_rules.h" |
25 |
|
#include "theory/bv/theory_bv_utils.h" |
26 |
|
#include "util/bitvector.h" |
27 |
|
|
28 |
|
namespace cvc5 { |
29 |
|
namespace theory { |
30 |
|
namespace bv { |
31 |
|
|
32 |
|
/* -------------------------------------------------------------------------- */ |
33 |
|
|
34 |
|
/** |
35 |
|
* BitOfConst |
36 |
|
*/ |
37 |
|
template <> |
38 |
451609 |
inline bool RewriteRule<BitOfConst>::applies(TNode node) |
39 |
|
{ |
40 |
451609 |
return node.getKind() == kind::BITVECTOR_BITOF && node[0].isConst(); |
41 |
|
} |
42 |
|
|
43 |
|
template <> |
44 |
59 |
inline Node RewriteRule<BitOfConst>::apply(TNode node) |
45 |
|
{ |
46 |
59 |
size_t pos = node.getOperator().getConst<BitVectorBitOf>().d_bitIndex; |
47 |
59 |
return utils::getBit(node[0], pos) ? utils::mkTrue() : utils::mkFalse(); |
48 |
|
} |
49 |
|
|
50 |
|
/* -------------------------------------------------------------------------- */ |
51 |
|
|
52 |
|
/** |
53 |
|
* BvIteConstCond |
54 |
|
* |
55 |
|
* BITVECTOR_ITE with constant condition |
56 |
|
*/ |
57 |
|
template <> |
58 |
22026 |
inline bool RewriteRule<BvIteConstCond>::applies(TNode node) |
59 |
|
{ |
60 |
22026 |
return (node.getKind() == kind::BITVECTOR_ITE && node[0].isConst()); |
61 |
|
} |
62 |
|
|
63 |
|
template <> |
64 |
390 |
inline Node RewriteRule<BvIteConstCond>::apply(TNode node) |
65 |
|
{ |
66 |
780 |
Debug("bv-rewrite") << "RewriteRule<BvIteConstCond>(" << node << ")" |
67 |
390 |
<< std::endl; |
68 |
390 |
return utils::isZero(node[0]) ? node[2] : node[1]; |
69 |
|
} |
70 |
|
|
71 |
|
/* -------------------------------------------------------------------------- */ |
72 |
|
|
73 |
|
/** |
74 |
|
* BvIteEqualChildren |
75 |
|
* |
76 |
|
* BITVECTOR_ITE with term_then = term_else |
77 |
|
*/ |
78 |
|
template <> |
79 |
22044 |
inline bool RewriteRule<BvIteEqualChildren>::applies(TNode node) |
80 |
|
{ |
81 |
22044 |
return (node.getKind() == kind::BITVECTOR_ITE && node[1] == node[2]); |
82 |
|
} |
83 |
|
|
84 |
|
template <> |
85 |
408 |
inline Node RewriteRule<BvIteEqualChildren>::apply(TNode node) |
86 |
|
{ |
87 |
816 |
Debug("bv-rewrite") << "RewriteRule<BvIteEqualChildren>(" << node << ")" |
88 |
408 |
<< std::endl; |
89 |
408 |
return node[1]; |
90 |
|
} |
91 |
|
|
92 |
|
/* -------------------------------------------------------------------------- */ |
93 |
|
|
94 |
|
/** |
95 |
|
* BvIteConstChildren |
96 |
|
* |
97 |
|
* BITVECTOR_ITE with constant children of size one |
98 |
|
*/ |
99 |
|
template <> |
100 |
20070 |
inline bool RewriteRule<BvIteConstChildren>::applies(TNode node) |
101 |
|
{ |
102 |
20070 |
return (node.getKind() == kind::BITVECTOR_ITE |
103 |
40140 |
&& utils::getSize(node[1]) == 1 |
104 |
68958 |
&& node[1].isConst() && node[2].isConst()); |
105 |
|
} |
106 |
|
|
107 |
|
template <> |
108 |
206 |
inline Node RewriteRule<BvIteConstChildren>::apply(TNode node) |
109 |
|
{ |
110 |
412 |
Debug("bv-rewrite") << "RewriteRule<BvIteConstChildren>(" << node << ")" |
111 |
206 |
<< std::endl; |
112 |
206 |
if (utils::isOne(node[1]) && utils::isZero(node[2])) |
113 |
|
{ |
114 |
180 |
return node[0]; |
115 |
|
} |
116 |
26 |
Assert(utils::isZero(node[1]) && utils::isOne(node[2])); |
117 |
26 |
return NodeManager::currentNM()->mkNode(kind::BITVECTOR_NOT, node[0]); |
118 |
|
} |
119 |
|
|
120 |
|
/* -------------------------------------------------------------------------- */ |
121 |
|
|
122 |
|
/** |
123 |
|
* BvIteEqualCond |
124 |
|
* |
125 |
|
* Nested BITVECTOR_ITE with cond_outer == cond_inner |
126 |
|
* |
127 |
|
* c0 ? (c0 ? t0 : e0) : e1 -> c0 ? t0 : e1 |
128 |
|
* c0 ? t0 : (c0 ? t1 : e1) -> c0 ? t0 : e1 |
129 |
|
* c0 ? (c0 ? t0 : e0) : (c0 ? t1 : e1) -> c0 ? t0 : e1 |
130 |
|
*/ |
131 |
|
template <> |
132 |
19873 |
inline bool RewriteRule<BvIteEqualCond>::applies(TNode node) |
133 |
|
{ |
134 |
|
return ( |
135 |
19873 |
node.getKind() == kind::BITVECTOR_ITE |
136 |
59637 |
&& ((node[1].getKind() == kind::BITVECTOR_ITE && node[0] == node[1][0]) |
137 |
39530 |
|| (node[2].getKind() == kind::BITVECTOR_ITE |
138 |
48554 |
&& node[0] == node[2][0]))); |
139 |
|
} |
140 |
|
|
141 |
|
template <> |
142 |
9 |
inline Node RewriteRule<BvIteEqualCond>::apply(TNode node) |
143 |
|
{ |
144 |
18 |
Debug("bv-rewrite") << "RewriteRule<BvIteEqualCond>(" << node << ")" |
145 |
9 |
<< std::endl; |
146 |
36 |
Node t0 = node[1].getKind() == kind::BITVECTOR_ITE && node[0] == node[1][0] |
147 |
45 |
? node[1][1] |
148 |
18 |
: node[1]; |
149 |
33 |
Node e1 = node[2].getKind() == kind::BITVECTOR_ITE && node[0] == node[2][0] |
150 |
36 |
? node[2][2] |
151 |
18 |
: node[2]; |
152 |
18 |
return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ITE, node[0], t0, e1); |
153 |
|
} |
154 |
|
|
155 |
|
/* -------------------------------------------------------------------------- */ |
156 |
|
|
157 |
|
/** |
158 |
|
* BvIteMergeThenIf |
159 |
|
* |
160 |
|
* Nested BITVECTOR_ITE of the form |
161 |
|
* c0 ? (c1 ? t1 : e1) : t1 -> c0 AND NOT(c1) ? e1 : t1 |
162 |
|
*/ |
163 |
|
template <> |
164 |
19674 |
inline bool RewriteRule<BvIteMergeThenIf>::applies(TNode node) |
165 |
|
{ |
166 |
19674 |
return (node.getKind() == kind::BITVECTOR_ITE |
167 |
39348 |
&& node[1].getKind() == kind::BITVECTOR_ITE |
168 |
61242 |
&& node[1][1] == node[2]); |
169 |
|
} |
170 |
|
|
171 |
|
template <> |
172 |
25 |
inline Node RewriteRule<BvIteMergeThenIf>::apply(TNode node) |
173 |
|
{ |
174 |
50 |
Debug("bv-rewrite") << "RewriteRule<BvIteMergeThenIf>(" << node << ")" |
175 |
25 |
<< std::endl; |
176 |
25 |
NodeManager* nm = NodeManager::currentNM(); |
177 |
25 |
Assert(node[1].getKind() == kind::BITVECTOR_ITE); |
178 |
|
Node cond = nm->mkNode(kind::BITVECTOR_AND, |
179 |
|
node[0], |
180 |
50 |
nm->mkNode(kind::BITVECTOR_NOT, node[1][0])); |
181 |
50 |
return nm->mkNode(kind::BITVECTOR_ITE, cond, node[1][2], node[2]); |
182 |
|
} |
183 |
|
|
184 |
|
/* -------------------------------------------------------------------------- */ |
185 |
|
|
186 |
|
/** |
187 |
|
* BvIteMergeElseIf |
188 |
|
* |
189 |
|
* Nested BITVECTOR_ITE of the form |
190 |
|
* c0 ? (c1 ? t1 : e1) : e1 -> c0 AND c1 ? t1 : e1 |
191 |
|
*/ |
192 |
|
template <> |
193 |
19668 |
inline bool RewriteRule<BvIteMergeElseIf>::applies(TNode node) |
194 |
|
{ |
195 |
19668 |
return (node.getKind() == kind::BITVECTOR_ITE |
196 |
39336 |
&& node[1].getKind() == kind::BITVECTOR_ITE |
197 |
61205 |
&& node[1][2] == node[2]); |
198 |
|
} |
199 |
|
|
200 |
|
template <> |
201 |
19 |
inline Node RewriteRule<BvIteMergeElseIf>::apply(TNode node) |
202 |
|
{ |
203 |
38 |
Debug("bv-rewrite") << "RewriteRule<BvIteMergeElseIf>(" << node << ")" |
204 |
19 |
<< std::endl; |
205 |
19 |
NodeManager* nm = NodeManager::currentNM(); |
206 |
19 |
Assert(node[1].getKind() == kind::BITVECTOR_ITE); |
207 |
38 |
Node cond = nm->mkNode(kind::BITVECTOR_AND, node[0], node[1][0]); |
208 |
38 |
return nm->mkNode(kind::BITVECTOR_ITE, cond, node[1][1], node[2]); |
209 |
|
} |
210 |
|
|
211 |
|
/* -------------------------------------------------------------------------- */ |
212 |
|
|
213 |
|
/** |
214 |
|
* BvIteMergeThenElse |
215 |
|
* |
216 |
|
* Nested BITVECTOR_ITE of the form |
217 |
|
* c0 ? t0 : (c1 ? t0 : e1) -> NOT(c0) AND NOT(c1) ? e1 : t0 |
218 |
|
*/ |
219 |
|
template <> |
220 |
19724 |
inline bool RewriteRule<BvIteMergeThenElse>::applies(TNode node) |
221 |
|
{ |
222 |
19724 |
return (node.getKind() == kind::BITVECTOR_ITE |
223 |
39448 |
&& node[2].getKind() == kind::BITVECTOR_ITE |
224 |
68055 |
&& node[1] == node[2][1]); |
225 |
|
} |
226 |
|
|
227 |
|
template <> |
228 |
75 |
inline Node RewriteRule<BvIteMergeThenElse>::apply(TNode node) |
229 |
|
{ |
230 |
150 |
Debug("bv-rewrite") << "RewriteRule<BvIteMergeThenElse>(" << node << ")" |
231 |
75 |
<< std::endl; |
232 |
75 |
NodeManager* nm = NodeManager::currentNM(); |
233 |
75 |
Assert(node[2].getKind() == kind::BITVECTOR_ITE); |
234 |
|
Node cond = nm->mkNode(kind::BITVECTOR_AND, |
235 |
150 |
nm->mkNode(kind::BITVECTOR_NOT, node[0]), |
236 |
300 |
nm->mkNode(kind::BITVECTOR_NOT, node[2][0])); |
237 |
150 |
return nm->mkNode(kind::BITVECTOR_ITE, cond, node[2][2], node[1]); |
238 |
|
} |
239 |
|
|
240 |
|
/* -------------------------------------------------------------------------- */ |
241 |
|
|
242 |
|
/** |
243 |
|
* BvIteMergeElseElse |
244 |
|
* |
245 |
|
* Nested BITVECTOR_ITE of the form |
246 |
|
* c0 ? t0 : (c1 ? t1 : t0) -> NOT(c0) AND c1 ? t1 : t0 |
247 |
|
*/ |
248 |
|
template <> |
249 |
19666 |
inline bool RewriteRule<BvIteMergeElseElse>::applies(TNode node) |
250 |
|
{ |
251 |
19666 |
return (node.getKind() == kind::BITVECTOR_ITE |
252 |
39332 |
&& node[2].getKind() == kind::BITVECTOR_ITE |
253 |
67767 |
&& node[1] == node[2][2]); |
254 |
|
} |
255 |
|
|
256 |
|
template <> |
257 |
17 |
inline Node RewriteRule<BvIteMergeElseElse>::apply(TNode node) |
258 |
|
{ |
259 |
34 |
Debug("bv-rewrite") << "RewriteRule<BvIteMergeElseElse>(" << node << ")" |
260 |
17 |
<< std::endl; |
261 |
17 |
NodeManager* nm = NodeManager::currentNM(); |
262 |
17 |
Assert(node[2].getKind() == kind::BITVECTOR_ITE); |
263 |
|
Node cond = nm->mkNode(kind::BITVECTOR_AND, |
264 |
34 |
nm->mkNode(kind::BITVECTOR_NOT, node[0]), |
265 |
68 |
node[2][0]); |
266 |
34 |
return nm->mkNode(kind::BITVECTOR_ITE, cond, node[2][1], node[1]); |
267 |
|
} |
268 |
|
|
269 |
|
/* -------------------------------------------------------------------------- */ |
270 |
|
|
271 |
|
/** |
272 |
|
* BvComp |
273 |
|
* |
274 |
|
* BITVECTOR_COMP of children of size 1 with one constant child |
275 |
|
*/ |
276 |
|
template <> |
277 |
28246 |
inline bool RewriteRule<BvComp>::applies(TNode node) |
278 |
|
{ |
279 |
28246 |
return (node.getKind() == kind::BITVECTOR_COMP |
280 |
56492 |
&& utils::getSize(node[0]) == 1 |
281 |
88351 |
&& (node[0].isConst() || node[1].isConst())); |
282 |
|
} |
283 |
|
|
284 |
|
template <> |
285 |
1137 |
inline Node RewriteRule<BvComp>::apply(TNode node) |
286 |
|
{ |
287 |
1137 |
Debug("bv-rewrite") << "RewriteRule<BvComp>(" << node << ")" << std::endl; |
288 |
1137 |
NodeManager* nm = NodeManager::currentNM(); |
289 |
1137 |
if (node[0].isConst()) |
290 |
|
{ |
291 |
586 |
return utils::isZero(node[0]) ? nm->mkNode(kind::BITVECTOR_NOT, node[1]) |
292 |
293 |
: Node(node[1]); |
293 |
|
} |
294 |
1688 |
return utils::isZero(node[1]) ? nm->mkNode(kind::BITVECTOR_NOT, node[0]) |
295 |
844 |
: Node(node[0]); |
296 |
|
} |
297 |
|
|
298 |
|
/* -------------------------------------------------------------------------- */ |
299 |
|
|
300 |
|
/** |
301 |
|
* ShlByConst |
302 |
|
* |
303 |
|
* Left Shift by constant amount |
304 |
|
*/ |
305 |
|
template<> inline |
306 |
35941 |
bool RewriteRule<ShlByConst>::applies(TNode node) { |
307 |
|
// if the shift amount is constant |
308 |
107823 |
return (node.getKind() == kind::BITVECTOR_SHL && |
309 |
107823 |
node[1].getKind() == kind::CONST_BITVECTOR); |
310 |
|
} |
311 |
|
|
312 |
|
template<> inline |
313 |
14859 |
Node RewriteRule<ShlByConst>::apply(TNode node) { |
314 |
14859 |
Debug("bv-rewrite") << "RewriteRule<ShlByConst>(" << node << ")" << std::endl; |
315 |
29718 |
Integer amount = node[1].getConst<BitVector>().toInteger(); |
316 |
14859 |
if (amount == 0) { |
317 |
2829 |
return node[0]; |
318 |
|
} |
319 |
24060 |
Node a = node[0]; |
320 |
12030 |
uint32_t size = utils::getSize(a); |
321 |
|
|
322 |
|
|
323 |
12030 |
if (amount >= Integer(size)) { |
324 |
|
// if we are shifting more than the length of the bitvector return 0 |
325 |
8962 |
return utils::mkZero(size); |
326 |
|
} |
327 |
|
|
328 |
|
// make sure we do not lose information casting |
329 |
3068 |
Assert(amount < Integer(1).multiplyByPow2(32)); |
330 |
|
|
331 |
3068 |
uint32_t uint32_amount = amount.toUnsignedInt(); |
332 |
|
|
333 |
6136 |
Node left = utils::mkExtract(a, size - 1 - uint32_amount, 0); |
334 |
6136 |
Node right = utils::mkZero(uint32_amount); |
335 |
3068 |
return utils::mkConcat(left, right); |
336 |
|
} |
337 |
|
|
338 |
|
/* -------------------------------------------------------------------------- */ |
339 |
|
|
340 |
|
/** |
341 |
|
* LshrByConst |
342 |
|
* |
343 |
|
* Right Logical Shift by constant amount |
344 |
|
*/ |
345 |
|
|
346 |
|
template<> inline |
347 |
40310 |
bool RewriteRule<LshrByConst>::applies(TNode node) { |
348 |
|
// if the shift amount is constant |
349 |
120930 |
return (node.getKind() == kind::BITVECTOR_LSHR && |
350 |
120930 |
node[1].getKind() == kind::CONST_BITVECTOR); |
351 |
|
} |
352 |
|
|
353 |
|
template<> inline |
354 |
15573 |
Node RewriteRule<LshrByConst>::apply(TNode node) { |
355 |
15573 |
Debug("bv-rewrite") << "RewriteRule<LshrByConst>(" << node << ")" << std::endl; |
356 |
31146 |
Integer amount = node[1].getConst<BitVector>().toInteger(); |
357 |
15573 |
if (amount == 0) { |
358 |
2957 |
return node[0]; |
359 |
|
} |
360 |
|
|
361 |
25232 |
Node a = node[0]; |
362 |
12616 |
uint32_t size = utils::getSize(a); |
363 |
|
|
364 |
|
|
365 |
12616 |
if (amount >= Integer(size)) { |
366 |
|
// if we are shifting more than the length of the bitvector return 0 |
367 |
10205 |
return utils::mkZero(size); |
368 |
|
} |
369 |
|
|
370 |
|
// make sure we do not lose information casting |
371 |
2411 |
Assert(amount < Integer(1).multiplyByPow2(32)); |
372 |
|
|
373 |
2411 |
uint32_t uint32_amount = amount.toUnsignedInt(); |
374 |
4822 |
Node right = utils::mkExtract(a, size - 1, uint32_amount); |
375 |
4822 |
Node left = utils::mkZero(uint32_amount); |
376 |
2411 |
return utils::mkConcat(left, right); |
377 |
|
} |
378 |
|
|
379 |
|
/* -------------------------------------------------------------------------- */ |
380 |
|
|
381 |
|
/** |
382 |
|
* AshrByConst |
383 |
|
* |
384 |
|
* Right Arithmetic Shift by constant amount |
385 |
|
*/ |
386 |
|
|
387 |
|
template<> inline |
388 |
3846 |
bool RewriteRule<AshrByConst>::applies(TNode node) { |
389 |
|
// if the shift amount is constant |
390 |
11538 |
return (node.getKind() == kind::BITVECTOR_ASHR && |
391 |
11538 |
node[1].getKind() == kind::CONST_BITVECTOR); |
392 |
|
} |
393 |
|
|
394 |
|
template<> inline |
395 |
532 |
Node RewriteRule<AshrByConst>::apply(TNode node) { |
396 |
532 |
Debug("bv-rewrite") << "RewriteRule<AshrByConst>(" << node << ")" << std::endl; |
397 |
1064 |
Integer amount = node[1].getConst<BitVector>().toInteger(); |
398 |
532 |
if (amount == 0) { |
399 |
88 |
return node[0]; |
400 |
|
} |
401 |
|
|
402 |
888 |
Node a = node[0]; |
403 |
444 |
uint32_t size = utils::getSize(a); |
404 |
888 |
Node sign_bit = utils::mkExtract(a, size-1, size-1); |
405 |
|
|
406 |
444 |
if (amount >= Integer(size)) { |
407 |
|
// if we are shifting more than the length of the bitvector return n repetitions |
408 |
|
// of the first bit |
409 |
80 |
return utils::mkConcat(sign_bit, size); |
410 |
|
} |
411 |
|
|
412 |
|
// make sure we do not lose information casting |
413 |
364 |
Assert(amount < Integer(1).multiplyByPow2(32)); |
414 |
|
|
415 |
364 |
uint32_t uint32_amount = amount.toUnsignedInt(); |
416 |
364 |
if (uint32_amount == 0) { |
417 |
|
return a; |
418 |
|
} |
419 |
|
|
420 |
728 |
Node left = utils::mkConcat(sign_bit, uint32_amount); |
421 |
728 |
Node right = utils::mkExtract(a, size - 1, uint32_amount); |
422 |
364 |
return utils::mkConcat(left, right); |
423 |
|
} |
424 |
|
|
425 |
|
/* -------------------------------------------------------------------------- */ |
426 |
|
|
427 |
|
/** |
428 |
|
* BitwiseIdemp |
429 |
|
* |
430 |
|
* (a bvand a) ==> a |
431 |
|
* (a bvor a) ==> a |
432 |
|
*/ |
433 |
|
|
434 |
|
template<> inline |
435 |
|
bool RewriteRule<BitwiseIdemp>::applies(TNode node) { |
436 |
|
Unreachable(); |
437 |
|
return ((node.getKind() == kind::BITVECTOR_AND || |
438 |
|
node.getKind() == kind::BITVECTOR_OR) && |
439 |
|
node.getNumChildren() == 2 && |
440 |
|
node[0] == node[1]); |
441 |
|
} |
442 |
|
|
443 |
|
template<> inline |
444 |
|
Node RewriteRule<BitwiseIdemp>::apply(TNode node) { |
445 |
|
Unreachable(); |
446 |
|
Debug("bv-rewrite") << "RewriteRule<BitwiseIdemp>(" << node << ")" << std::endl; |
447 |
|
return node[0]; |
448 |
|
} |
449 |
|
|
450 |
|
/* -------------------------------------------------------------------------- */ |
451 |
|
|
452 |
|
/** |
453 |
|
* AndZero |
454 |
|
* |
455 |
|
* (a bvand 0) ==> 0 |
456 |
|
*/ |
457 |
|
|
458 |
|
template<> inline |
459 |
|
bool RewriteRule<AndZero>::applies(TNode node) { |
460 |
|
Unreachable(); |
461 |
|
unsigned size = utils::getSize(node); |
462 |
|
return (node.getKind() == kind::BITVECTOR_AND && |
463 |
|
node.getNumChildren() == 2 && |
464 |
|
(node[0] == utils::mkConst(size, 0) || |
465 |
|
node[1] == utils::mkConst(size, 0))); |
466 |
|
} |
467 |
|
|
468 |
|
template<> inline |
469 |
|
Node RewriteRule<AndZero>::apply(TNode node) { |
470 |
|
Unreachable(); |
471 |
|
Debug("bv-rewrite") << "RewriteRule<AndZero>(" << node << ")" << std::endl; |
472 |
|
return utils::mkConst(utils::getSize(node), 0); |
473 |
|
} |
474 |
|
|
475 |
|
/* -------------------------------------------------------------------------- */ |
476 |
|
|
477 |
|
/** |
478 |
|
* AndOne |
479 |
|
* |
480 |
|
* (a bvand 1) ==> a |
481 |
|
*/ |
482 |
|
|
483 |
|
template<> inline |
484 |
|
bool RewriteRule<AndOne>::applies(TNode node) { |
485 |
|
Unreachable(); |
486 |
|
unsigned size = utils::getSize(node); |
487 |
|
Node ones = utils::mkOnes(size); |
488 |
|
return (node.getKind() == kind::BITVECTOR_AND && |
489 |
|
node.getNumChildren() == 2 && |
490 |
|
(node[0] == ones || |
491 |
|
node[1] == ones)); |
492 |
|
} |
493 |
|
|
494 |
|
template<> inline |
495 |
|
Node RewriteRule<AndOne>::apply(TNode node) { |
496 |
|
Unreachable(); |
497 |
|
Debug("bv-rewrite") << "RewriteRule<AndOne>(" << node << ")" << std::endl; |
498 |
|
unsigned size = utils::getSize(node); |
499 |
|
|
500 |
|
if (node[0] == utils::mkOnes(size)) { |
501 |
|
return node[1]; |
502 |
|
} else { |
503 |
|
Assert(node[1] == utils::mkOnes(size)); |
504 |
|
return node[0]; |
505 |
|
} |
506 |
|
} |
507 |
|
|
508 |
|
/* -------------------------------------------------------------------------- */ |
509 |
|
|
510 |
|
/** |
511 |
|
* AndOrXorConcatPullUp |
512 |
|
* |
513 |
|
* Match: x_m <op> concat(y_my, <const>_n, z_mz) |
514 |
|
* <const>_n in { 0_n, 1_n, ~0_n } |
515 |
|
* |
516 |
|
* Rewrites to: concat(x[m-1:m-my] <op> y, |
517 |
|
* x[m-my-1:mz] <op> <const>_n, |
518 |
|
* x[mz-1:0] <op> z) |
519 |
|
*/ |
520 |
|
|
521 |
|
template <> |
522 |
248492 |
inline bool RewriteRule<AndOrXorConcatPullUp>::applies(TNode node) |
523 |
|
{ |
524 |
496984 |
if (node.getKind() != kind::BITVECTOR_AND |
525 |
179173 |
&& node.getKind() != kind::BITVECTOR_OR |
526 |
337947 |
&& node.getKind() != kind::BITVECTOR_XOR) |
527 |
|
{ |
528 |
85616 |
return false; |
529 |
|
} |
530 |
|
|
531 |
325752 |
TNode n; |
532 |
|
|
533 |
766197 |
for (const TNode& c : node) |
534 |
|
{ |
535 |
608701 |
if (c.getKind() == kind::BITVECTOR_CONCAT) |
536 |
|
{ |
537 |
32715 |
for (const TNode& cc : c) |
538 |
|
{ |
539 |
31216 |
if (cc.isConst()) |
540 |
|
{ |
541 |
3881 |
n = cc; |
542 |
3881 |
break; |
543 |
|
} |
544 |
|
} |
545 |
5380 |
break; |
546 |
|
} |
547 |
|
} |
548 |
162876 |
if (n.isNull()) return false; |
549 |
3881 |
return utils::isZero(n) || utils::isOne(n) || utils::isOnes(n); |
550 |
|
} |
551 |
|
|
552 |
|
template <> |
553 |
1935 |
inline Node RewriteRule<AndOrXorConcatPullUp>::apply(TNode node) |
554 |
|
{ |
555 |
3870 |
Debug("bv-rewrite") << "RewriteRule<AndOrXorConcatPullUp>(" << node << ")" |
556 |
1935 |
<< std::endl; |
557 |
|
uint32_t m, my, mz; |
558 |
|
size_t nc; |
559 |
1935 |
Kind kind = node.getKind(); |
560 |
3870 |
TNode concat; |
561 |
3870 |
Node x, y, z, c; |
562 |
3870 |
NodeBuilder xb(kind); |
563 |
3870 |
NodeBuilder yb(kind::BITVECTOR_CONCAT); |
564 |
3870 |
NodeBuilder zb(kind::BITVECTOR_CONCAT); |
565 |
3870 |
NodeBuilder res(kind::BITVECTOR_CONCAT); |
566 |
1935 |
NodeManager* nm = NodeManager::currentNM(); |
567 |
|
|
568 |
6203 |
for (const TNode& child : node) |
569 |
|
{ |
570 |
4268 |
if (concat.isNull() && child.getKind() == kind::BITVECTOR_CONCAT) |
571 |
|
{ |
572 |
1935 |
concat = child; |
573 |
|
} |
574 |
|
else |
575 |
|
{ |
576 |
2333 |
xb << child; |
577 |
|
} |
578 |
|
} |
579 |
1935 |
x = xb.getNumChildren() > 1 ? xb.constructNode() : xb[0]; |
580 |
|
|
581 |
7454 |
for (const TNode& child : concat) |
582 |
|
{ |
583 |
5519 |
if (c.isNull()) |
584 |
|
{ |
585 |
4727 |
if (utils::isZero(child) || utils::isOne(child) || utils::isOnes(child)) |
586 |
|
{ |
587 |
1935 |
c = child; |
588 |
|
} |
589 |
|
else |
590 |
|
{ |
591 |
2792 |
yb << child; |
592 |
|
} |
593 |
|
} |
594 |
|
else |
595 |
|
{ |
596 |
792 |
zb << child; |
597 |
|
} |
598 |
|
} |
599 |
1935 |
Assert(!c.isNull()); |
600 |
1935 |
Assert(yb.getNumChildren() || zb.getNumChildren()); |
601 |
|
|
602 |
1935 |
if ((nc = yb.getNumChildren()) > 0) |
603 |
|
{ |
604 |
1310 |
y = nc > 1 ? yb.constructNode() : yb[0]; |
605 |
|
} |
606 |
1935 |
if ((nc = zb.getNumChildren()) > 0) |
607 |
|
{ |
608 |
629 |
z = nc > 1 ? zb.constructNode() : zb[0]; |
609 |
|
} |
610 |
1935 |
m = utils::getSize(x); |
611 |
|
#ifdef CVC5_ASSERTIONS |
612 |
1935 |
uint32_t n = utils::getSize(c); |
613 |
|
#endif |
614 |
1935 |
my = y.isNull() ? 0 : utils::getSize(y); |
615 |
1935 |
mz = z.isNull() ? 0 : utils::getSize(z); |
616 |
1935 |
Assert(mz == m - my - n); |
617 |
1935 |
Assert(my || mz); |
618 |
|
|
619 |
1935 |
if (my) |
620 |
|
{ |
621 |
1310 |
res << nm->mkNode(kind, utils::mkExtract(x, m - 1, m - my), y); |
622 |
|
} |
623 |
|
|
624 |
1935 |
res << nm->mkNode(kind, utils::mkExtract(x, m - my - 1, mz), c); |
625 |
|
|
626 |
1935 |
if (mz) |
627 |
|
{ |
628 |
629 |
res << nm->mkNode(kind, utils::mkExtract(x, mz - 1, 0), z); |
629 |
|
} |
630 |
|
|
631 |
3870 |
return res; |
632 |
|
} |
633 |
|
|
634 |
|
/* -------------------------------------------------------------------------- */ |
635 |
|
|
636 |
|
/** |
637 |
|
* OrZero |
638 |
|
* |
639 |
|
* (a bvor 0) ==> a |
640 |
|
*/ |
641 |
|
|
642 |
|
template<> inline |
643 |
|
bool RewriteRule<OrZero>::applies(TNode node) { |
644 |
|
Unreachable(); |
645 |
|
unsigned size = utils::getSize(node); |
646 |
|
return (node.getKind() == kind::BITVECTOR_OR && |
647 |
|
node.getNumChildren() == 2 && |
648 |
|
(node[0] == utils::mkConst(size, 0) || |
649 |
|
node[1] == utils::mkConst(size, 0))); |
650 |
|
} |
651 |
|
|
652 |
|
template<> inline |
653 |
|
Node RewriteRule<OrZero>::apply(TNode node) { |
654 |
|
Unreachable(); |
655 |
|
Debug("bv-rewrite") << "RewriteRule<OrZero>(" << node << ")" << std::endl; |
656 |
|
|
657 |
|
unsigned size = utils::getSize(node); |
658 |
|
if (node[0] == utils::mkConst(size, 0)) { |
659 |
|
return node[1]; |
660 |
|
} else { |
661 |
|
Assert(node[1] == utils::mkConst(size, 0)); |
662 |
|
return node[0]; |
663 |
|
} |
664 |
|
} |
665 |
|
|
666 |
|
/* -------------------------------------------------------------------------- */ |
667 |
|
|
668 |
|
/** |
669 |
|
* OrOne |
670 |
|
* |
671 |
|
* (a bvor 1) ==> 1 |
672 |
|
*/ |
673 |
|
|
674 |
|
template<> inline |
675 |
|
bool RewriteRule<OrOne>::applies(TNode node) { |
676 |
|
Unreachable(); |
677 |
|
unsigned size = utils::getSize(node); |
678 |
|
Node ones = utils::mkOnes(size); |
679 |
|
return (node.getKind() == kind::BITVECTOR_OR && |
680 |
|
node.getNumChildren() == 2 && |
681 |
|
(node[0] == ones || |
682 |
|
node[1] == ones)); |
683 |
|
} |
684 |
|
|
685 |
|
template<> inline |
686 |
|
Node RewriteRule<OrOne>::apply(TNode node) { |
687 |
|
Unreachable(); |
688 |
|
Debug("bv-rewrite") << "RewriteRule<OrOne>(" << node << ")" << std::endl; |
689 |
|
return utils::mkOnes(utils::getSize(node)); |
690 |
|
} |
691 |
|
|
692 |
|
/* -------------------------------------------------------------------------- */ |
693 |
|
|
694 |
|
/** |
695 |
|
* XorDuplicate |
696 |
|
* |
697 |
|
* (a bvxor a) ==> 0 |
698 |
|
*/ |
699 |
|
|
700 |
|
template<> inline |
701 |
|
bool RewriteRule<XorDuplicate>::applies(TNode node) { |
702 |
|
Unreachable(); |
703 |
|
return (node.getKind() == kind::BITVECTOR_XOR && |
704 |
|
node.getNumChildren() == 2 && |
705 |
|
node[0] == node[1]); |
706 |
|
} |
707 |
|
|
708 |
|
template<> inline |
709 |
|
Node RewriteRule<XorDuplicate>::apply(TNode node) { |
710 |
|
Unreachable(); |
711 |
|
Debug("bv-rewrite") << "RewriteRule<XorDuplicate>(" << node << ")" << std::endl; |
712 |
|
return utils::mkZero(utils::getSize(node)); |
713 |
|
} |
714 |
|
|
715 |
|
/* -------------------------------------------------------------------------- */ |
716 |
|
|
717 |
|
/** |
718 |
|
* XorOne |
719 |
|
* |
720 |
|
* (a bvxor 1) ==> ~a |
721 |
|
*/ |
722 |
|
|
723 |
|
template<> inline |
724 |
2522 |
bool RewriteRule<XorOne>::applies(TNode node) { |
725 |
2522 |
if (node.getKind() != kind::BITVECTOR_XOR) { |
726 |
617 |
return false; |
727 |
|
} |
728 |
3810 |
Node ones = utils::mkOnes(utils::getSize(node)); |
729 |
4857 |
for (unsigned i = 0; i < node.getNumChildren(); ++i) { |
730 |
3424 |
if (node[i] == ones) { |
731 |
472 |
return true; |
732 |
|
} |
733 |
|
} |
734 |
1433 |
return false; |
735 |
|
} |
736 |
|
|
737 |
|
template <> |
738 |
236 |
inline Node RewriteRule<XorOne>::apply(TNode node) |
739 |
|
{ |
740 |
236 |
Debug("bv-rewrite") << "RewriteRule<XorOne>(" << node << ")" << std::endl; |
741 |
236 |
NodeManager *nm = NodeManager::currentNM(); |
742 |
472 |
Node ones = utils::mkOnes(utils::getSize(node)); |
743 |
472 |
std::vector<Node> children; |
744 |
236 |
bool found_ones = false; |
745 |
|
// XorSimplify should have been called before |
746 |
717 |
for (unsigned i = 0; i < node.getNumChildren(); ++i) |
747 |
|
{ |
748 |
481 |
if (node[i] == ones) |
749 |
|
{ |
750 |
|
// make sure only ones occurs only once |
751 |
236 |
found_ones = !found_ones; |
752 |
|
} |
753 |
|
else |
754 |
|
{ |
755 |
245 |
children.push_back(node[i]); |
756 |
|
} |
757 |
|
} |
758 |
|
|
759 |
236 |
Node result = utils::mkNaryNode(kind::BITVECTOR_XOR, children); |
760 |
236 |
if (found_ones) |
761 |
|
{ |
762 |
236 |
result = nm->mkNode(kind::BITVECTOR_NOT, result); |
763 |
|
} |
764 |
472 |
return result; |
765 |
|
} |
766 |
|
|
767 |
|
/* -------------------------------------------------------------------------- */ |
768 |
|
|
769 |
|
/** |
770 |
|
* XorZero |
771 |
|
* |
772 |
|
* (a bvxor 0) ==> a |
773 |
|
*/ |
774 |
|
|
775 |
|
template<> inline |
776 |
5014 |
bool RewriteRule<XorZero>::applies(TNode node) { |
777 |
5014 |
if (node.getKind() != kind::BITVECTOR_XOR) { |
778 |
406 |
return false; |
779 |
|
} |
780 |
9216 |
Node zero = utils::mkConst(utils::getSize(node), 0); |
781 |
12192 |
for (unsigned i = 0; i < node.getNumChildren(); ++i) { |
782 |
8492 |
if (node[i] == zero) { |
783 |
908 |
return true; |
784 |
|
} |
785 |
|
} |
786 |
3700 |
return false; |
787 |
|
} |
788 |
|
|
789 |
|
template <> |
790 |
454 |
inline Node RewriteRule<XorZero>::apply(TNode node) |
791 |
|
{ |
792 |
454 |
Debug("bv-rewrite") << "RewriteRule<XorZero>(" << node << ")" << std::endl; |
793 |
908 |
std::vector<Node> children; |
794 |
908 |
Node zero = utils::mkConst(utils::getSize(node), 0); |
795 |
|
|
796 |
|
// XorSimplify should have been called before |
797 |
1369 |
for (unsigned i = 0; i < node.getNumChildren(); ++i) |
798 |
|
{ |
799 |
915 |
if (node[i] != zero) |
800 |
|
{ |
801 |
461 |
children.push_back(node[i]); |
802 |
|
} |
803 |
|
} |
804 |
454 |
Node res = utils::mkNaryNode(kind::BITVECTOR_XOR, children); |
805 |
908 |
return res; |
806 |
|
} |
807 |
|
|
808 |
|
/* -------------------------------------------------------------------------- */ |
809 |
|
|
810 |
|
/** |
811 |
|
* BitwiseNotAnd |
812 |
|
* |
813 |
|
* (a bvand (~ a)) ==> 0 |
814 |
|
*/ |
815 |
|
|
816 |
|
template<> inline |
817 |
|
bool RewriteRule<BitwiseNotAnd>::applies(TNode node) { |
818 |
|
Unreachable(); |
819 |
|
return (node.getKind() == kind::BITVECTOR_AND && |
820 |
|
node.getNumChildren() == 2 && |
821 |
|
((node[0].getKind() == kind::BITVECTOR_NOT && node[0][0] == node[1]) || |
822 |
|
(node[1].getKind() == kind::BITVECTOR_NOT && node[1][0] == node[0]))); |
823 |
|
} |
824 |
|
|
825 |
|
template<> inline |
826 |
|
Node RewriteRule<BitwiseNotAnd>::apply(TNode node) { |
827 |
|
Unreachable(); |
828 |
|
Debug("bv-rewrite") << "RewriteRule<BitwiseNegAnd>(" << node << ")" << std::endl; |
829 |
|
return utils::mkZero(utils::getSize(node)); |
830 |
|
} |
831 |
|
|
832 |
|
/* -------------------------------------------------------------------------- */ |
833 |
|
|
834 |
|
/** |
835 |
|
* BitwiseNegOr |
836 |
|
* |
837 |
|
* (a bvor (~ a)) ==> 1 |
838 |
|
*/ |
839 |
|
|
840 |
|
template<> inline |
841 |
|
bool RewriteRule<BitwiseNotOr>::applies(TNode node) { |
842 |
|
Unreachable(); |
843 |
|
return (node.getKind() == kind::BITVECTOR_OR && |
844 |
|
node.getNumChildren() == 2 && |
845 |
|
((node[0].getKind() == kind::BITVECTOR_NOT && node[0][0] == node[1]) || |
846 |
|
(node[1].getKind() == kind::BITVECTOR_NOT && node[1][0] == node[0]))); |
847 |
|
} |
848 |
|
|
849 |
|
template<> inline |
850 |
|
Node RewriteRule<BitwiseNotOr>::apply(TNode node) { |
851 |
|
Unreachable(); |
852 |
|
Debug("bv-rewrite") << "RewriteRule<BitwiseNotOr>(" << node << ")" << std::endl; |
853 |
|
uint32_t size = utils::getSize(node); |
854 |
|
return utils::mkOnes(size); |
855 |
|
} |
856 |
|
|
857 |
|
/* -------------------------------------------------------------------------- */ |
858 |
|
|
859 |
|
/** |
860 |
|
* XorNot |
861 |
|
* |
862 |
|
* ((~ a) bvxor (~ b)) ==> (a bvxor b) |
863 |
|
*/ |
864 |
|
|
865 |
|
template<> inline |
866 |
|
bool RewriteRule<XorNot>::applies(TNode node) { |
867 |
|
Unreachable(); |
868 |
|
} |
869 |
|
|
870 |
|
template <> |
871 |
|
inline Node RewriteRule<XorNot>::apply(TNode node) |
872 |
|
{ |
873 |
|
Unreachable(); |
874 |
|
Debug("bv-rewrite") << "RewriteRule<XorNot>(" << node << ")" << std::endl; |
875 |
|
Node a = node[0][0]; |
876 |
|
Node b = node[1][0]; |
877 |
|
return NodeManager::currentNM()->mkNode(kind::BITVECTOR_XOR, a, b); |
878 |
|
} |
879 |
|
|
880 |
|
/* -------------------------------------------------------------------------- */ |
881 |
|
|
882 |
|
/** |
883 |
|
* NotXor |
884 |
|
* |
885 |
|
* ~(a bvxor b) ==> (~ a bvxor b) |
886 |
|
*/ |
887 |
|
|
888 |
|
template<> inline |
889 |
|
bool RewriteRule<NotXor>::applies(TNode node) { |
890 |
|
return (node.getKind() == kind::BITVECTOR_NOT && |
891 |
|
node[0].getKind() == kind::BITVECTOR_XOR); |
892 |
|
} |
893 |
|
|
894 |
|
template <> |
895 |
|
inline Node RewriteRule<NotXor>::apply(TNode node) |
896 |
|
{ |
897 |
|
Debug("bv-rewrite") << "RewriteRule<NotXor>(" << node << ")" << std::endl; |
898 |
|
std::vector<Node> children; |
899 |
|
TNode::iterator child_it = node[0].begin(); |
900 |
|
children.push_back( |
901 |
|
NodeManager::currentNM()->mkNode(kind::BITVECTOR_NOT, *child_it)); |
902 |
|
for (++child_it; child_it != node[0].end(); ++child_it) |
903 |
|
{ |
904 |
|
children.push_back(*child_it); |
905 |
|
} |
906 |
|
return utils::mkSortedNode(kind::BITVECTOR_XOR, children); |
907 |
|
} |
908 |
|
|
909 |
|
/* -------------------------------------------------------------------------- */ |
910 |
|
|
911 |
|
/** |
912 |
|
* NotIdemp |
913 |
|
* |
914 |
|
* ~ (~ a) ==> a |
915 |
|
*/ |
916 |
|
|
917 |
|
template<> inline |
918 |
74548 |
bool RewriteRule<NotIdemp>::applies(TNode node) { |
919 |
186640 |
return (node.getKind() == kind::BITVECTOR_NOT && |
920 |
186640 |
node[0].getKind() == kind::BITVECTOR_NOT); |
921 |
|
} |
922 |
|
|
923 |
|
template<> inline |
924 |
354 |
Node RewriteRule<NotIdemp>::apply(TNode node) { |
925 |
354 |
Debug("bv-rewrite") << "RewriteRule<NotIdemp>(" << node << ")" << std::endl; |
926 |
354 |
return node[0][0]; |
927 |
|
} |
928 |
|
|
929 |
|
/* -------------------------------------------------------------------------- */ |
930 |
|
|
931 |
|
/** |
932 |
|
* LtSelf |
933 |
|
* |
934 |
|
* a < a ==> false |
935 |
|
*/ |
936 |
|
|
937 |
|
template<> inline |
938 |
|
bool RewriteRule<LtSelf>::applies(TNode node) { |
939 |
|
return ((node.getKind() == kind::BITVECTOR_ULT || |
940 |
|
node.getKind() == kind::BITVECTOR_SLT) && |
941 |
|
node[0] == node[1]); |
942 |
|
} |
943 |
|
|
944 |
|
template<> inline |
945 |
|
Node RewriteRule<LtSelf>::apply(TNode node) { |
946 |
|
Debug("bv-rewrite") << "RewriteRule<LtSelf>(" << node << ")" << std::endl; |
947 |
|
return utils::mkFalse(); |
948 |
|
} |
949 |
|
|
950 |
|
/* -------------------------------------------------------------------------- */ |
951 |
|
|
952 |
|
/** |
953 |
|
* LteSelf |
954 |
|
* |
955 |
|
* a <= a ==> true |
956 |
|
*/ |
957 |
|
|
958 |
|
template<> inline |
959 |
|
bool RewriteRule<LteSelf>::applies(TNode node) { |
960 |
|
return ((node.getKind() == kind::BITVECTOR_ULE || |
961 |
|
node.getKind() == kind::BITVECTOR_SLE) && |
962 |
|
node[0] == node[1]); |
963 |
|
} |
964 |
|
|
965 |
|
template<> inline |
966 |
|
Node RewriteRule<LteSelf>::apply(TNode node) { |
967 |
|
Debug("bv-rewrite") << "RewriteRule<LteSelf>(" << node << ")" << std::endl; |
968 |
|
return utils::mkTrue(); |
969 |
|
} |
970 |
|
|
971 |
|
/* -------------------------------------------------------------------------- */ |
972 |
|
|
973 |
|
/** |
974 |
|
* ZeroUlt |
975 |
|
* |
976 |
|
* 0 < a ==> a != 0 |
977 |
|
*/ |
978 |
|
|
979 |
|
template <> |
980 |
|
inline bool RewriteRule<ZeroUlt>::applies(TNode node) |
981 |
|
{ |
982 |
|
return (node.getKind() == kind::BITVECTOR_ULT |
983 |
|
&& node[0] == utils::mkZero(utils::getSize(node[0]))); |
984 |
|
} |
985 |
|
|
986 |
|
template <> |
987 |
|
inline Node RewriteRule<ZeroUlt>::apply(TNode node) |
988 |
|
{ |
989 |
|
Debug("bv-rewrite") << "RewriteRule<ZeroUlt>(" << node << ")" << std::endl; |
990 |
|
NodeManager *nm = NodeManager::currentNM(); |
991 |
|
return nm->mkNode(kind::NOT, nm->mkNode(kind::EQUAL, node[0], node[1])); |
992 |
|
} |
993 |
|
|
994 |
|
/* -------------------------------------------------------------------------- */ |
995 |
|
|
996 |
|
/** |
997 |
|
* UltZero |
998 |
|
* |
999 |
|
* a < 0 ==> false |
1000 |
|
*/ |
1001 |
|
|
1002 |
|
template<> inline |
1003 |
42115 |
bool RewriteRule<UltZero>::applies(TNode node) { |
1004 |
165058 |
return (node.getKind() == kind::BITVECTOR_ULT && |
1005 |
165058 |
node[1] == utils::mkZero(utils::getSize(node[0]))); |
1006 |
|
} |
1007 |
|
|
1008 |
|
template<> inline |
1009 |
163 |
Node RewriteRule<UltZero>::apply(TNode node) { |
1010 |
163 |
Debug("bv-rewrite") << "RewriteRule<UltZero>(" << node << ")" << std::endl; |
1011 |
163 |
return utils::mkFalse(); |
1012 |
|
} |
1013 |
|
|
1014 |
|
|
1015 |
|
/* -------------------------------------------------------------------------- */ |
1016 |
|
|
1017 |
|
/** |
1018 |
|
* |
1019 |
|
*/ |
1020 |
|
template<> inline |
1021 |
|
bool RewriteRule<UltOne>::applies(TNode node) { |
1022 |
|
return (node.getKind() == kind::BITVECTOR_ULT && |
1023 |
|
node[1] == utils::mkOne(utils::getSize(node[0]))); |
1024 |
|
} |
1025 |
|
|
1026 |
|
template <> |
1027 |
|
inline Node RewriteRule<UltOne>::apply(TNode node) |
1028 |
|
{ |
1029 |
|
Debug("bv-rewrite") << "RewriteRule<UltOne>(" << node << ")" << std::endl; |
1030 |
|
return NodeManager::currentNM()->mkNode( |
1031 |
|
kind::EQUAL, node[0], utils::mkZero(utils::getSize(node[0]))); |
1032 |
|
} |
1033 |
|
|
1034 |
|
/* -------------------------------------------------------------------------- */ |
1035 |
|
|
1036 |
|
/** |
1037 |
|
* |
1038 |
|
*/ |
1039 |
|
template<> inline |
1040 |
|
bool RewriteRule<SltZero>::applies(TNode node) { |
1041 |
|
return (node.getKind() == kind::BITVECTOR_SLT && |
1042 |
|
node[1] == utils::mkZero(utils::getSize(node[0]))); |
1043 |
|
} |
1044 |
|
|
1045 |
|
template <> |
1046 |
|
inline Node RewriteRule<SltZero>::apply(TNode node) |
1047 |
|
{ |
1048 |
|
Debug("bv-rewrite") << "RewriteRule<UltZero>(" << node << ")" << std::endl; |
1049 |
|
unsigned size = utils::getSize(node[0]); |
1050 |
|
Node most_significant_bit = utils::mkExtract(node[0], size - 1, size - 1); |
1051 |
|
return NodeManager::currentNM()->mkNode( |
1052 |
|
kind::EQUAL, most_significant_bit, utils::mkOne(1)); |
1053 |
|
} |
1054 |
|
|
1055 |
|
/* -------------------------------------------------------------------------- */ |
1056 |
|
|
1057 |
|
/** |
1058 |
|
* UltSelf |
1059 |
|
* |
1060 |
|
* a < a ==> false |
1061 |
|
*/ |
1062 |
|
|
1063 |
|
template<> inline |
1064 |
|
bool RewriteRule<UltSelf>::applies(TNode node) { |
1065 |
|
return (node.getKind() == kind::BITVECTOR_ULT && |
1066 |
|
node[1] == node[0]); |
1067 |
|
} |
1068 |
|
|
1069 |
|
template<> inline |
1070 |
|
Node RewriteRule<UltSelf>::apply(TNode node) { |
1071 |
|
Debug("bv-rewrite") << "RewriteRule<UltSelf>(" << node << ")" << std::endl; |
1072 |
|
return utils::mkFalse(); |
1073 |
|
} |
1074 |
|
|
1075 |
|
|
1076 |
|
/* -------------------------------------------------------------------------- */ |
1077 |
|
|
1078 |
|
/** |
1079 |
|
* UleZero |
1080 |
|
* |
1081 |
|
* a <= 0 ==> a = 0 |
1082 |
|
*/ |
1083 |
|
|
1084 |
|
template<> inline |
1085 |
2434 |
bool RewriteRule<UleZero>::applies(TNode node) { |
1086 |
9592 |
return (node.getKind() == kind::BITVECTOR_ULE && |
1087 |
9592 |
node[1] == utils::mkZero(utils::getSize(node[0]))); |
1088 |
|
} |
1089 |
|
|
1090 |
|
template <> |
1091 |
24 |
inline Node RewriteRule<UleZero>::apply(TNode node) |
1092 |
|
{ |
1093 |
24 |
Debug("bv-rewrite") << "RewriteRule<UleZero>(" << node << ")" << std::endl; |
1094 |
24 |
return NodeManager::currentNM()->mkNode(kind::EQUAL, node[0], node[1]); |
1095 |
|
} |
1096 |
|
|
1097 |
|
/* -------------------------------------------------------------------------- */ |
1098 |
|
|
1099 |
|
/** |
1100 |
|
* UleSelf |
1101 |
|
* |
1102 |
|
* a <= a ==> true |
1103 |
|
*/ |
1104 |
|
|
1105 |
|
template<> inline |
1106 |
2430 |
bool RewriteRule<UleSelf>::applies(TNode node) { |
1107 |
9504 |
return (node.getKind() == kind::BITVECTOR_ULE && |
1108 |
9504 |
node[1] == node[0]); |
1109 |
|
} |
1110 |
|
|
1111 |
|
template<> inline |
1112 |
20 |
Node RewriteRule<UleSelf>::apply(TNode node) { |
1113 |
20 |
Debug("bv-rewrite") << "RewriteRule<UleSelf>(" << node << ")" << std::endl; |
1114 |
20 |
return utils::mkTrue(); |
1115 |
|
} |
1116 |
|
|
1117 |
|
/* -------------------------------------------------------------------------- */ |
1118 |
|
|
1119 |
|
/** |
1120 |
|
* ZeroUle |
1121 |
|
* |
1122 |
|
* 0 <= a ==> true |
1123 |
|
*/ |
1124 |
|
|
1125 |
|
template<> inline |
1126 |
2426 |
bool RewriteRule<ZeroUle>::applies(TNode node) { |
1127 |
9608 |
return (node.getKind() == kind::BITVECTOR_ULE && |
1128 |
9608 |
node[0] == utils::mkZero(utils::getSize(node[0]))); |
1129 |
|
} |
1130 |
|
|
1131 |
|
template<> inline |
1132 |
16 |
Node RewriteRule<ZeroUle>::apply(TNode node) { |
1133 |
16 |
Debug("bv-rewrite") << "RewriteRule<ZeroUle>(" << node << ")" << std::endl; |
1134 |
16 |
return utils::mkTrue(); |
1135 |
|
} |
1136 |
|
|
1137 |
|
/* -------------------------------------------------------------------------- */ |
1138 |
|
|
1139 |
|
/** |
1140 |
|
* UleMax |
1141 |
|
* |
1142 |
|
* a <= 11..1 ==> true |
1143 |
|
*/ |
1144 |
|
|
1145 |
|
template<> inline |
1146 |
2423 |
bool RewriteRule<UleMax>::applies(TNode node) { |
1147 |
2423 |
if (node.getKind()!= kind::BITVECTOR_ULE) { |
1148 |
19 |
return false; |
1149 |
|
} |
1150 |
2404 |
uint32_t size = utils::getSize(node[0]); |
1151 |
2404 |
return (node.getKind() == kind::BITVECTOR_ULE |
1152 |
4808 |
&& node[1] == utils::mkOnes(size)); |
1153 |
|
} |
1154 |
|
|
1155 |
|
template<> inline |
1156 |
13 |
Node RewriteRule<UleMax>::apply(TNode node) { |
1157 |
13 |
Debug("bv-rewrite") << "RewriteRule<UleMax>(" << node << ")" << std::endl; |
1158 |
13 |
return utils::mkTrue(); |
1159 |
|
} |
1160 |
|
|
1161 |
|
/* -------------------------------------------------------------------------- */ |
1162 |
|
|
1163 |
|
/** |
1164 |
|
* NotUlt |
1165 |
|
* |
1166 |
|
* ~ ( a < b) ==> b <= a |
1167 |
|
*/ |
1168 |
|
|
1169 |
|
template<> inline |
1170 |
|
bool RewriteRule<NotUlt>::applies(TNode node) { |
1171 |
|
return (node.getKind() == kind::NOT && |
1172 |
|
node[0].getKind() == kind::BITVECTOR_ULT); |
1173 |
|
} |
1174 |
|
|
1175 |
|
template <> |
1176 |
|
inline Node RewriteRule<NotUlt>::apply(TNode node) |
1177 |
|
{ |
1178 |
|
Debug("bv-rewrite") << "RewriteRule<NotUlt>(" << node << ")" << std::endl; |
1179 |
|
Node ult = node[0]; |
1180 |
|
Node a = ult[0]; |
1181 |
|
Node b = ult[1]; |
1182 |
|
return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULE, b, a); |
1183 |
|
} |
1184 |
|
|
1185 |
|
/* -------------------------------------------------------------------------- */ |
1186 |
|
|
1187 |
|
/** |
1188 |
|
* NotUle |
1189 |
|
* |
1190 |
|
* ~ ( a <= b) ==> b < a |
1191 |
|
*/ |
1192 |
|
|
1193 |
|
template<> inline |
1194 |
|
bool RewriteRule<NotUle>::applies(TNode node) { |
1195 |
|
return (node.getKind() == kind::NOT && |
1196 |
|
node[0].getKind() == kind::BITVECTOR_ULE); |
1197 |
|
} |
1198 |
|
|
1199 |
|
template <> |
1200 |
|
inline Node RewriteRule<NotUle>::apply(TNode node) |
1201 |
|
{ |
1202 |
|
Debug("bv-rewrite") << "RewriteRule<NotUle>(" << node << ")" << std::endl; |
1203 |
|
Node ult = node[0]; |
1204 |
|
Node a = ult[0]; |
1205 |
|
Node b = ult[1]; |
1206 |
|
return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, b, a); |
1207 |
|
} |
1208 |
|
|
1209 |
|
/* -------------------------------------------------------------------------- */ |
1210 |
|
|
1211 |
|
/** |
1212 |
|
* MultPow2 |
1213 |
|
* |
1214 |
|
* (a * 2^k) ==> a[n-k-1:0] 0_k |
1215 |
|
*/ |
1216 |
|
|
1217 |
|
template <> |
1218 |
236224 |
inline bool RewriteRule<MultPow2>::applies(TNode node) |
1219 |
|
{ |
1220 |
236224 |
if (node.getKind() != kind::BITVECTOR_MULT) |
1221 |
30969 |
return false; |
1222 |
|
|
1223 |
789776 |
for (const Node& cn : node) |
1224 |
|
{ |
1225 |
596751 |
bool cIsNeg = false; |
1226 |
596751 |
if (utils::isPow2Const(cn, cIsNeg)) |
1227 |
|
{ |
1228 |
12230 |
return true; |
1229 |
|
} |
1230 |
|
} |
1231 |
193025 |
return false; |
1232 |
|
} |
1233 |
|
|
1234 |
|
template <> |
1235 |
6115 |
inline Node RewriteRule<MultPow2>::apply(TNode node) |
1236 |
|
{ |
1237 |
6115 |
Debug("bv-rewrite") << "RewriteRule<MultPow2>(" << node << ")" << std::endl; |
1238 |
6115 |
NodeManager *nm = NodeManager::currentNM(); |
1239 |
6115 |
unsigned size = utils::getSize(node); |
1240 |
12230 |
std::vector<Node> children; |
1241 |
6115 |
unsigned exponent = 0; |
1242 |
6115 |
bool isNeg = false; |
1243 |
18403 |
for (const Node& cn : node) |
1244 |
|
{ |
1245 |
12288 |
bool cIsNeg = false; |
1246 |
12288 |
unsigned exp = utils::isPow2Const(cn, cIsNeg); |
1247 |
12288 |
if (exp) { |
1248 |
6117 |
exponent += exp - 1; |
1249 |
6117 |
if (cIsNeg) |
1250 |
|
{ |
1251 |
1408 |
isNeg = !isNeg; |
1252 |
|
} |
1253 |
|
} |
1254 |
|
else { |
1255 |
6171 |
children.push_back(cn); |
1256 |
|
} |
1257 |
|
} |
1258 |
6115 |
if (exponent >= size) |
1259 |
|
{ |
1260 |
|
return utils::mkZero(size); |
1261 |
|
} |
1262 |
|
|
1263 |
12230 |
Node a; |
1264 |
6115 |
if (children.empty()) |
1265 |
|
{ |
1266 |
2 |
a = utils::mkOne(size); |
1267 |
|
} |
1268 |
|
else |
1269 |
|
{ |
1270 |
6113 |
a = utils::mkNaryNode(kind::BITVECTOR_MULT, children); |
1271 |
|
} |
1272 |
|
|
1273 |
6115 |
if (isNeg && size > 1) |
1274 |
|
{ |
1275 |
1404 |
a = nm->mkNode(kind::BITVECTOR_NEG, a); |
1276 |
|
} |
1277 |
6115 |
if (exponent == 0) |
1278 |
|
{ |
1279 |
2 |
return a; |
1280 |
|
} |
1281 |
12226 |
Node extract = utils::mkExtract(a, size - exponent - 1, 0); |
1282 |
12226 |
Node zeros = utils::mkConst(exponent, 0); |
1283 |
6113 |
return utils::mkConcat(extract, zeros); |
1284 |
|
} |
1285 |
|
|
1286 |
|
/* -------------------------------------------------------------------------- */ |
1287 |
|
|
1288 |
|
/** |
1289 |
|
* ExtractMultLeadingBit |
1290 |
|
* |
1291 |
|
* If the bit-vectors multiplied have enough leading zeros, |
1292 |
|
* we can determine that the top bits of the multiplication |
1293 |
|
* are zero and not compute them. Only apply for large bitwidths |
1294 |
|
* as this can interfere with other mult normalization rewrites such |
1295 |
|
* as flattening. |
1296 |
|
*/ |
1297 |
|
|
1298 |
|
template<> inline |
1299 |
79429 |
bool RewriteRule<ExtractMultLeadingBit>::applies(TNode node) { |
1300 |
79429 |
if (node.getKind() != kind::BITVECTOR_EXTRACT) |
1301 |
23746 |
return false; |
1302 |
55683 |
unsigned low = utils::getExtractLow(node); |
1303 |
55683 |
node = node[0]; |
1304 |
|
|
1305 |
112672 |
if (node.getKind() != kind::BITVECTOR_MULT || |
1306 |
113884 |
node.getNumChildren() != 2 || |
1307 |
58201 |
utils::getSize(node) <= 64) |
1308 |
55643 |
return false; |
1309 |
|
|
1310 |
184 |
if (node[0].getKind() != kind::BITVECTOR_CONCAT || |
1311 |
168 |
node[1].getKind() != kind::BITVECTOR_CONCAT || |
1312 |
288 |
!node[0][0].isConst() || |
1313 |
104 |
!node[1][0].isConst()) |
1314 |
8 |
return false; |
1315 |
|
|
1316 |
32 |
unsigned n = utils::getSize(node); |
1317 |
|
// count number of leading zeroes |
1318 |
64 |
const Integer& int1 = node[0][0].getConst<BitVector>().toInteger(); |
1319 |
64 |
const Integer& int2 = node[1][0].getConst<BitVector>().toInteger(); |
1320 |
32 |
size_t int1_size = utils::getSize(node[0][0]); |
1321 |
32 |
size_t int2_size = utils::getSize(node[1][0]); |
1322 |
32 |
unsigned zeroes1 = int1.isZero() ? int1_size : int1_size - int1.length(); |
1323 |
32 |
unsigned zeroes2 = int2.isZero() ? int2_size : int2_size - int2.length(); |
1324 |
|
|
1325 |
|
// first k bits are not zero in the result |
1326 |
32 |
unsigned k = 2 * n - (zeroes1 + zeroes2); |
1327 |
|
|
1328 |
32 |
if (k > low) |
1329 |
32 |
return false; |
1330 |
|
|
1331 |
|
return true; |
1332 |
|
} |
1333 |
|
|
1334 |
|
template<> inline |
1335 |
|
Node RewriteRule<ExtractMultLeadingBit>::apply(TNode node) { |
1336 |
|
Debug("bv-rewrite") << "RewriteRule<MultLeadingBit>(" << node << ")" << std::endl; |
1337 |
|
|
1338 |
|
unsigned bitwidth = utils::getSize(node); |
1339 |
|
|
1340 |
|
// node = node[0]; |
1341 |
|
// const Integer& int1 = node[0][0].getConst<BitVector>().toInteger(); |
1342 |
|
// const Integer& int2 = node[1][0].getConst<BitVector>().toInteger(); |
1343 |
|
// unsigned zeroes1 = int1.isZero()? utils::getSize(node[0][0]) : |
1344 |
|
// int1.length(); |
1345 |
|
|
1346 |
|
// unsigned zeroes2 = int2.isZero()? utils::getSize(node[1][0]) : |
1347 |
|
// int2.length(); |
1348 |
|
// all bits >= k in the multiplier will have to be 0 |
1349 |
|
// unsigned n = utils::getSize(node); |
1350 |
|
// unsigned k = 2 * n - (zeroes1 + zeroes2); |
1351 |
|
// Node extract1 = utils::mkExtract(node[0], k - 1, 0); |
1352 |
|
// Node extract2 = utils::mkExtract(node[1], k - 1, 0); |
1353 |
|
// Node k_zeroes = utils::mkConst(n - k, 0u); |
1354 |
|
|
1355 |
|
// NodeManager *nm = NodeManager::currentNM(); |
1356 |
|
// Node new_mult = nm->mkNode(kind::BITVECTOR_MULT, extract1, extract2); |
1357 |
|
// Node result = utils::mkExtract(nm->mkNode(kind::BITVECTOR_CONCAT, k_zeroes, new_mult), high, low); |
1358 |
|
|
1359 |
|
// since the extract is over multiplier bits that have to be 0, return 0 |
1360 |
|
Node result = utils::mkConst(bitwidth, 0u); |
1361 |
|
// std::cout << "MultLeadingBit " << node <<" => " << result <<"\n"; |
1362 |
|
return result; |
1363 |
|
} |
1364 |
|
|
1365 |
|
/* -------------------------------------------------------------------------- */ |
1366 |
|
|
1367 |
|
/** |
1368 |
|
* NegIdemp |
1369 |
|
* |
1370 |
|
* -(-a) ==> a |
1371 |
|
*/ |
1372 |
|
|
1373 |
|
template<> inline |
1374 |
26889 |
bool RewriteRule<NegIdemp>::applies(TNode node) { |
1375 |
66775 |
return (node.getKind() == kind::BITVECTOR_NEG && |
1376 |
66775 |
node[0].getKind() == kind::BITVECTOR_NEG); |
1377 |
|
} |
1378 |
|
|
1379 |
|
template<> inline |
1380 |
85 |
Node RewriteRule<NegIdemp>::apply(TNode node) { |
1381 |
85 |
Debug("bv-rewrite") << "RewriteRule<NegIdemp>(" << node << ")" << std::endl; |
1382 |
85 |
return node[0][0]; |
1383 |
|
} |
1384 |
|
|
1385 |
|
/* -------------------------------------------------------------------------- */ |
1386 |
|
|
1387 |
|
/** |
1388 |
|
* UdivPow2 |
1389 |
|
* |
1390 |
|
* (a udiv 2^k) ==> 0_k a[n-1: k] |
1391 |
|
*/ |
1392 |
|
|
1393 |
|
template <> |
1394 |
24816 |
inline bool RewriteRule<UdivPow2>::applies(TNode node) |
1395 |
|
{ |
1396 |
24816 |
bool isNeg = false; |
1397 |
49632 |
if (node.getKind() == kind::BITVECTOR_UDIV |
1398 |
49632 |
&& utils::isPow2Const(node[1], isNeg)) |
1399 |
|
{ |
1400 |
4357 |
return !isNeg; |
1401 |
|
} |
1402 |
20459 |
return false; |
1403 |
|
} |
1404 |
|
|
1405 |
|
template <> |
1406 |
1435 |
inline Node RewriteRule<UdivPow2>::apply(TNode node) |
1407 |
|
{ |
1408 |
1435 |
Debug("bv-rewrite") << "RewriteRule<UdivPow2>(" << node << ")" << std::endl; |
1409 |
1435 |
NodeManager *nm = NodeManager::currentNM(); |
1410 |
1435 |
unsigned size = utils::getSize(node); |
1411 |
2870 |
Node a = node[0]; |
1412 |
1435 |
bool isNeg = false; |
1413 |
1435 |
unsigned power = utils::isPow2Const(node[1], isNeg) - 1; |
1414 |
1435 |
Node ret; |
1415 |
1435 |
if (power == 0) |
1416 |
|
{ |
1417 |
873 |
ret = a; |
1418 |
|
} |
1419 |
|
else |
1420 |
|
{ |
1421 |
1124 |
Node extract = utils::mkExtract(a, size - 1, power); |
1422 |
1124 |
Node zeros = utils::mkConst(power, 0); |
1423 |
|
|
1424 |
562 |
ret = nm->mkNode(kind::BITVECTOR_CONCAT, zeros, extract); |
1425 |
|
} |
1426 |
1435 |
if (isNeg && size > 1) |
1427 |
|
{ |
1428 |
|
ret = nm->mkNode(kind::BITVECTOR_NEG, ret); |
1429 |
|
} |
1430 |
2870 |
return ret; |
1431 |
|
} |
1432 |
|
|
1433 |
|
/* -------------------------------------------------------------------------- */ |
1434 |
|
|
1435 |
|
/** |
1436 |
|
* UdivZero |
1437 |
|
* |
1438 |
|
* (a udiv 0) ==> 111...1 |
1439 |
|
*/ |
1440 |
|
|
1441 |
|
template <> |
1442 |
23128 |
inline bool RewriteRule<UdivZero>::applies(TNode node) { |
1443 |
23128 |
return (node.getKind() == kind::BITVECTOR_UDIV |
1444 |
46256 |
&& node[1] == utils::mkConst(utils::getSize(node), 0)); |
1445 |
|
} |
1446 |
|
|
1447 |
|
template <> |
1448 |
66 |
inline Node RewriteRule<UdivZero>::apply(TNode node) { |
1449 |
66 |
Debug("bv-rewrite") << "RewriteRule<UdivZero>(" << node << ")" << std::endl; |
1450 |
66 |
return utils::mkOnes(utils::getSize(node)); |
1451 |
|
} |
1452 |
|
|
1453 |
|
/* -------------------------------------------------------------------------- */ |
1454 |
|
|
1455 |
|
/** |
1456 |
|
* UdivOne |
1457 |
|
* |
1458 |
|
* (a udiv 1) ==> a |
1459 |
|
*/ |
1460 |
|
|
1461 |
|
template <> |
1462 |
21946 |
inline bool RewriteRule<UdivOne>::applies(TNode node) { |
1463 |
21946 |
return (node.getKind() == kind::BITVECTOR_UDIV |
1464 |
43892 |
&& node[1] == utils::mkConst(utils::getSize(node), 1)); |
1465 |
|
} |
1466 |
|
|
1467 |
|
template <> |
1468 |
|
inline Node RewriteRule<UdivOne>::apply(TNode node) { |
1469 |
|
Debug("bv-rewrite") << "RewriteRule<UdivOne>(" << node << ")" << std::endl; |
1470 |
|
return node[0]; |
1471 |
|
} |
1472 |
|
|
1473 |
|
/* -------------------------------------------------------------------------- */ |
1474 |
|
|
1475 |
|
/** |
1476 |
|
* UremPow2 |
1477 |
|
* |
1478 |
|
* (a urem 2^k) ==> 0_(n-k) a[k-1:0] |
1479 |
|
*/ |
1480 |
|
|
1481 |
|
template <> |
1482 |
24402 |
inline bool RewriteRule<UremPow2>::applies(TNode node) |
1483 |
|
{ |
1484 |
|
bool isNeg; |
1485 |
48804 |
if (node.getKind() == kind::BITVECTOR_UREM |
1486 |
48804 |
&& utils::isPow2Const(node[1], isNeg)) |
1487 |
|
{ |
1488 |
3138 |
return !isNeg; |
1489 |
|
} |
1490 |
21264 |
return false; |
1491 |
|
} |
1492 |
|
|
1493 |
|
template <> |
1494 |
1177 |
inline Node RewriteRule<UremPow2>::apply(TNode node) |
1495 |
|
{ |
1496 |
1177 |
Debug("bv-rewrite") << "RewriteRule<UremPow2>(" << node << ")" << std::endl; |
1497 |
2354 |
TNode a = node[0]; |
1498 |
1177 |
bool isNeg = false; |
1499 |
1177 |
unsigned power = utils::isPow2Const(node[1], isNeg) - 1; |
1500 |
1177 |
Node ret; |
1501 |
1177 |
if (power == 0) |
1502 |
|
{ |
1503 |
643 |
ret = utils::mkZero(utils::getSize(node)); |
1504 |
|
} |
1505 |
|
else |
1506 |
|
{ |
1507 |
1068 |
Node extract = utils::mkExtract(a, power - 1, 0); |
1508 |
1068 |
Node zeros = utils::mkZero(utils::getSize(node) - power); |
1509 |
534 |
ret = NodeManager::currentNM()->mkNode( |
1510 |
|
kind::BITVECTOR_CONCAT, zeros, extract); |
1511 |
|
} |
1512 |
2354 |
return ret; |
1513 |
|
} |
1514 |
|
|
1515 |
|
/* -------------------------------------------------------------------------- */ |
1516 |
|
|
1517 |
|
/** |
1518 |
|
* UremOne |
1519 |
|
* |
1520 |
|
* (a urem 1) ==> 0 |
1521 |
|
*/ |
1522 |
|
|
1523 |
|
template<> inline |
1524 |
22048 |
bool RewriteRule<UremOne>::applies(TNode node) { |
1525 |
22048 |
return (node.getKind() == kind::BITVECTOR_UREM |
1526 |
44096 |
&& node[1] == utils::mkConst(utils::getSize(node), 1)); |
1527 |
|
} |
1528 |
|
|
1529 |
|
template<> inline |
1530 |
|
Node RewriteRule<UremOne>::apply(TNode node) { |
1531 |
|
Debug("bv-rewrite") << "RewriteRule<UremOne>(" << node << ")" << std::endl; |
1532 |
|
return utils::mkConst(utils::getSize(node), 0); |
1533 |
|
} |
1534 |
|
|
1535 |
|
/* -------------------------------------------------------------------------- */ |
1536 |
|
|
1537 |
|
/** |
1538 |
|
* UremSelf |
1539 |
|
* |
1540 |
|
* (a urem a) ==> 0 |
1541 |
|
*/ |
1542 |
|
|
1543 |
|
template<> inline |
1544 |
22068 |
bool RewriteRule<UremSelf>::applies(TNode node) { |
1545 |
22068 |
return (node.getKind() == kind::BITVECTOR_UREM && node[0] == node[1]); |
1546 |
|
} |
1547 |
|
|
1548 |
|
template<> inline |
1549 |
20 |
Node RewriteRule<UremSelf>::apply(TNode node) { |
1550 |
20 |
Debug("bv-rewrite") << "RewriteRule<UremSelf>(" << node << ")" << std::endl; |
1551 |
20 |
return utils::mkConst(utils::getSize(node), 0); |
1552 |
|
} |
1553 |
|
|
1554 |
|
/* -------------------------------------------------------------------------- */ |
1555 |
|
|
1556 |
|
/** |
1557 |
|
* ShiftZero |
1558 |
|
* |
1559 |
|
* (0_k >> a) ==> 0_k |
1560 |
|
*/ |
1561 |
|
|
1562 |
|
template<> inline |
1563 |
19151 |
bool RewriteRule<ShiftZero>::applies(TNode node) { |
1564 |
31621 |
return ((node.getKind() == kind::BITVECTOR_SHL || |
1565 |
15259 |
node.getKind() == kind::BITVECTOR_LSHR || |
1566 |
98544 |
node.getKind() == kind::BITVECTOR_ASHR) && |
1567 |
76604 |
node[0] == utils::mkConst(utils::getSize(node), 0)); |
1568 |
|
} |
1569 |
|
|
1570 |
|
template<> inline |
1571 |
982 |
Node RewriteRule<ShiftZero>::apply(TNode node) { |
1572 |
982 |
Debug("bv-rewrite") << "RewriteRule<ShiftZero>(" << node << ")" << std::endl; |
1573 |
982 |
return node[0]; |
1574 |
|
} |
1575 |
|
|
1576 |
|
/* -------------------------------------------------------------------------- */ |
1577 |
|
|
1578 |
|
/** |
1579 |
|
* UgtUrem |
1580 |
|
* |
1581 |
|
* (bvugt (bvurem T x) x) |
1582 |
|
* ==> (ite (= x 0_k) (bvugt T x) false) |
1583 |
|
* ==> (and (=> (= x 0_k) (bvugt T x)) (=> (not (= x 0_k)) false)) |
1584 |
|
* ==> (and (=> (= x 0_k) (bvugt T x)) (= x 0_k)) |
1585 |
|
* ==> (and (bvugt T x) (= x 0_k)) |
1586 |
|
* ==> (and (bvugt T 0_k) (= x 0_k)) |
1587 |
|
*/ |
1588 |
|
|
1589 |
|
template <> |
1590 |
1459 |
inline bool RewriteRule<UgtUrem>::applies(TNode node) |
1591 |
|
{ |
1592 |
1459 |
return (node.getKind() == kind::BITVECTOR_UGT |
1593 |
2918 |
&& node[0].getKind() == kind::BITVECTOR_UREM |
1594 |
4395 |
&& node[0][1] == node[1]); |
1595 |
|
} |
1596 |
|
|
1597 |
|
template <> |
1598 |
3 |
inline Node RewriteRule<UgtUrem>::apply(TNode node) |
1599 |
|
{ |
1600 |
3 |
Debug("bv-rewrite") << "RewriteRule<UgtUrem>(" << node << ")" << std::endl; |
1601 |
6 |
const Node& T = node[0][0]; |
1602 |
6 |
const Node& x = node[1]; |
1603 |
6 |
Node zero = utils::mkConst(utils::getSize(x), 0); |
1604 |
3 |
NodeManager* nm = NodeManager::currentNM(); |
1605 |
|
return nm->mkNode(kind::AND, |
1606 |
6 |
nm->mkNode(kind::EQUAL, x, zero), |
1607 |
12 |
nm->mkNode(kind::BITVECTOR_UGT, T, zero)); |
1608 |
|
} |
1609 |
|
|
1610 |
|
/* -------------------------------------------------------------------------- */ |
1611 |
|
|
1612 |
|
/** |
1613 |
|
* BBAddNeg |
1614 |
|
* |
1615 |
|
* -a1 - a2 - ... - an + ak + .. ==> - (a1 + a2 + ... + an) + ak |
1616 |
|
* |
1617 |
|
*/ |
1618 |
|
|
1619 |
|
template <> |
1620 |
|
inline bool RewriteRule<BBAddNeg>::applies(TNode node) |
1621 |
|
{ |
1622 |
|
if (node.getKind() != kind::BITVECTOR_ADD) |
1623 |
|
{ |
1624 |
|
return false; |
1625 |
|
} |
1626 |
|
|
1627 |
|
unsigned neg_count = 0; |
1628 |
|
for(unsigned i = 0; i < node.getNumChildren(); ++i) { |
1629 |
|
if (node[i].getKind()== kind::BITVECTOR_NEG) { |
1630 |
|
++neg_count; |
1631 |
|
} |
1632 |
|
} |
1633 |
|
return neg_count > 1; |
1634 |
|
} |
1635 |
|
|
1636 |
|
template <> |
1637 |
|
inline Node RewriteRule<BBAddNeg>::apply(TNode node) |
1638 |
|
{ |
1639 |
|
Debug("bv-rewrite") << "RewriteRule<BBAddNeg>(" << node << ")" << std::endl; |
1640 |
|
NodeManager *nm = NodeManager::currentNM(); |
1641 |
|
std::vector<Node> children; |
1642 |
|
unsigned neg_count = 0; |
1643 |
|
for (unsigned i = 0; i < node.getNumChildren(); ++i) |
1644 |
|
{ |
1645 |
|
if (node[i].getKind() == kind::BITVECTOR_NEG) |
1646 |
|
{ |
1647 |
|
++neg_count; |
1648 |
|
children.push_back(nm->mkNode(kind::BITVECTOR_NOT, node[i][0])); |
1649 |
|
} |
1650 |
|
else |
1651 |
|
{ |
1652 |
|
children.push_back(node[i]); |
1653 |
|
} |
1654 |
|
} |
1655 |
|
Assert(neg_count != 0); |
1656 |
|
children.push_back(utils::mkConst(utils::getSize(node), neg_count)); |
1657 |
|
|
1658 |
|
return utils::mkNaryNode(kind::BITVECTOR_ADD, children); |
1659 |
|
} |
1660 |
|
|
1661 |
|
/* -------------------------------------------------------------------------- */ |
1662 |
|
|
1663 |
|
template<> inline |
1664 |
24242 |
bool RewriteRule<MergeSignExtend>::applies(TNode node) { |
1665 |
120950 |
if (node.getKind() != kind::BITVECTOR_SIGN_EXTEND || |
1666 |
120878 |
(node[0].getKind() != kind::BITVECTOR_SIGN_EXTEND && |
1667 |
72394 |
node[0].getKind() != kind::BITVECTOR_ZERO_EXTEND)) |
1668 |
23982 |
return false; |
1669 |
260 |
return true; |
1670 |
|
} |
1671 |
|
|
1672 |
|
template<> inline |
1673 |
130 |
Node RewriteRule<MergeSignExtend>::apply(TNode node) { |
1674 |
130 |
Debug("bv-rewrite") << "RewriteRule<MergeSignExtend>(" << node << ")" << std::endl; |
1675 |
|
unsigned amount1 = |
1676 |
130 |
node.getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount; |
1677 |
|
|
1678 |
130 |
NodeManager* nm = NodeManager::currentNM(); |
1679 |
130 |
if (node[0].getKind() == kind::BITVECTOR_ZERO_EXTEND) { |
1680 |
|
unsigned amount2 = node[0] |
1681 |
94 |
.getOperator() |
1682 |
47 |
.getConst<BitVectorZeroExtend>() |
1683 |
47 |
.d_zeroExtendAmount; |
1684 |
47 |
if (amount2 == 0) |
1685 |
|
{ |
1686 |
38 |
NodeBuilder nb(kind::BITVECTOR_SIGN_EXTEND); |
1687 |
38 |
Node op = nm->mkConst<BitVectorSignExtend>(BitVectorSignExtend(amount1)); |
1688 |
19 |
nb << op << node[0][0]; |
1689 |
38 |
Node res = nb; |
1690 |
19 |
return res; |
1691 |
|
} |
1692 |
56 |
NodeBuilder nb(kind::BITVECTOR_ZERO_EXTEND); |
1693 |
|
Node op = nm->mkConst<BitVectorZeroExtend>( |
1694 |
56 |
BitVectorZeroExtend(amount1 + amount2)); |
1695 |
28 |
nb << op << node[0][0]; |
1696 |
56 |
Node res = nb; |
1697 |
28 |
return res; |
1698 |
|
} |
1699 |
83 |
Assert(node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND); |
1700 |
|
unsigned amount2 = |
1701 |
83 |
node[0].getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount; |
1702 |
83 |
return utils::mkSignExtend(node[0][0], amount1 + amount2); |
1703 |
|
} |
1704 |
|
|
1705 |
|
/* -------------------------------------------------------------------------- */ |
1706 |
|
|
1707 |
|
/** |
1708 |
|
* ZeroExtendEqConst |
1709 |
|
* |
1710 |
|
* Rewrite zero_extend(x^n, m) = c^n+m to |
1711 |
|
* |
1712 |
|
* false if c[n+m-1:n] != 0 |
1713 |
|
* x = c[n-1:0] otherwise. |
1714 |
|
*/ |
1715 |
|
template <> |
1716 |
23 |
inline bool RewriteRule<ZeroExtendEqConst>::applies(TNode node) { |
1717 |
43 |
return node.getKind() == kind::EQUAL && |
1718 |
43 |
((node[0].getKind() == kind::BITVECTOR_ZERO_EXTEND && |
1719 |
43 |
node[1].isConst()) || |
1720 |
43 |
(node[1].getKind() == kind::BITVECTOR_ZERO_EXTEND && |
1721 |
46 |
node[0].isConst())); |
1722 |
|
} |
1723 |
|
|
1724 |
|
template <> |
1725 |
|
inline Node RewriteRule<ZeroExtendEqConst>::apply(TNode node) { |
1726 |
|
TNode t, c; |
1727 |
|
if (node[0].getKind() == kind::BITVECTOR_ZERO_EXTEND) { |
1728 |
|
t = node[0][0]; |
1729 |
|
c = node[1]; |
1730 |
|
} else { |
1731 |
|
t = node[1][0]; |
1732 |
|
c = node[0]; |
1733 |
|
} |
1734 |
|
BitVector c_hi = |
1735 |
|
c.getConst<BitVector>().extract(utils::getSize(c) - 1, utils::getSize(t)); |
1736 |
|
BitVector c_lo = c.getConst<BitVector>().extract(utils::getSize(t) - 1, 0); |
1737 |
|
BitVector zero = BitVector(c_hi.getSize(), Integer(0)); |
1738 |
|
|
1739 |
|
if (c_hi == zero) { |
1740 |
|
return NodeManager::currentNM()->mkNode(kind::EQUAL, t, |
1741 |
|
utils::mkConst(c_lo)); |
1742 |
|
} |
1743 |
|
return utils::mkFalse(); |
1744 |
|
} |
1745 |
|
|
1746 |
|
/* -------------------------------------------------------------------------- */ |
1747 |
|
|
1748 |
|
/** |
1749 |
|
* SignExtendEqConst |
1750 |
|
* |
1751 |
|
* Rewrite sign_extend(x^n, m) = c^n+m to |
1752 |
|
* |
1753 |
|
* x = c[n-1:0] if (c[n-1:n-1] == 0 && c[n+m-1:n] == 0) || |
1754 |
|
* (c[n-1:n-1] == 1 && c[n+m-1:n] == ~0) |
1755 |
|
* false otherwise. |
1756 |
|
*/ |
1757 |
|
template <> |
1758 |
23 |
inline bool RewriteRule<SignExtendEqConst>::applies(TNode node) { |
1759 |
43 |
return node.getKind() == kind::EQUAL && |
1760 |
43 |
((node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND && |
1761 |
43 |
node[1].isConst()) || |
1762 |
43 |
(node[1].getKind() == kind::BITVECTOR_SIGN_EXTEND && |
1763 |
46 |
node[0].isConst())); |
1764 |
|
} |
1765 |
|
|
1766 |
|
template <> |
1767 |
|
inline Node RewriteRule<SignExtendEqConst>::apply(TNode node) { |
1768 |
|
TNode t, c; |
1769 |
|
if (node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND) { |
1770 |
|
t = node[0][0]; |
1771 |
|
c = node[1]; |
1772 |
|
} else { |
1773 |
|
t = node[1][0]; |
1774 |
|
c = node[0]; |
1775 |
|
} |
1776 |
|
unsigned pos_msb_t = utils::getSize(t) - 1; |
1777 |
|
BitVector c_hi = |
1778 |
|
c.getConst<BitVector>().extract(utils::getSize(c) - 1, pos_msb_t); |
1779 |
|
BitVector c_lo = c.getConst<BitVector>().extract(pos_msb_t, 0); |
1780 |
|
BitVector zero = BitVector(c_hi.getSize(), Integer(0)); |
1781 |
|
|
1782 |
|
if (c_hi == zero || c_hi == ~zero) { |
1783 |
|
return NodeManager::currentNM()->mkNode(kind::EQUAL, t, |
1784 |
|
utils::mkConst(c_lo)); |
1785 |
|
} |
1786 |
|
return utils::mkFalse(); |
1787 |
|
} |
1788 |
|
|
1789 |
|
/* -------------------------------------------------------------------------- */ |
1790 |
|
|
1791 |
|
/** |
1792 |
|
* ZeroExtendUltConst |
1793 |
|
* |
1794 |
|
* Rewrite zero_extend(x^n,m) < c^n+m to |
1795 |
|
* |
1796 |
|
* x < c[n-1:0] if c[n+m-1:n] == 0. |
1797 |
|
* |
1798 |
|
* Rewrite c^n+m < Rewrite zero_extend(x^n,m) to |
1799 |
|
* |
1800 |
|
* c[n-1:0] < x if c[n+m-1:n] == 0. |
1801 |
|
*/ |
1802 |
|
template <> |
1803 |
41974 |
inline bool RewriteRule<ZeroExtendUltConst>::applies(TNode node) { |
1804 |
165166 |
if (node.getKind() == kind::BITVECTOR_ULT && |
1805 |
124540 |
((node[0].getKind() == kind::BITVECTOR_ZERO_EXTEND && |
1806 |
124446 |
node[1].isConst()) || |
1807 |
124374 |
(node[1].getKind() == kind::BITVECTOR_ZERO_EXTEND && |
1808 |
43360 |
node[0].isConst()))) { |
1809 |
220 |
TNode t, c; |
1810 |
110 |
bool is_lhs = node[0].getKind() == kind::BITVECTOR_ZERO_EXTEND; |
1811 |
110 |
if (is_lhs) { |
1812 |
47 |
t = node[0][0]; |
1813 |
47 |
c = node[1]; |
1814 |
|
} else { |
1815 |
63 |
t = node[1][0]; |
1816 |
63 |
c = node[0]; |
1817 |
|
} |
1818 |
|
|
1819 |
110 |
if (utils::getSize(t) == utils::getSize(c)) |
1820 |
|
{ |
1821 |
5 |
return false; |
1822 |
|
} |
1823 |
|
|
1824 |
210 |
BitVector bv_c = c.getConst<BitVector>(); |
1825 |
315 |
BitVector c_hi = c.getConst<BitVector>().extract(utils::getSize(c) - 1, |
1826 |
420 |
utils::getSize(t)); |
1827 |
210 |
BitVector zero = BitVector(c_hi.getSize(), Integer(0)); |
1828 |
|
|
1829 |
105 |
return c_hi == zero; |
1830 |
|
} |
1831 |
41864 |
return false; |
1832 |
|
} |
1833 |
|
|
1834 |
|
template <> |
1835 |
22 |
inline Node RewriteRule<ZeroExtendUltConst>::apply(TNode node) { |
1836 |
44 |
TNode t, c; |
1837 |
22 |
bool is_lhs = node[0].getKind() == kind::BITVECTOR_ZERO_EXTEND; |
1838 |
22 |
if (is_lhs) { |
1839 |
9 |
t = node[0][0]; |
1840 |
9 |
c = node[1]; |
1841 |
|
} else { |
1842 |
13 |
t = node[1][0]; |
1843 |
13 |
c = node[0]; |
1844 |
|
} |
1845 |
|
Node c_lo = |
1846 |
44 |
utils::mkConst(c.getConst<BitVector>().extract(utils::getSize(t) - 1, 0)); |
1847 |
|
|
1848 |
22 |
if (is_lhs) { |
1849 |
9 |
return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, t, c_lo); |
1850 |
|
} |
1851 |
13 |
return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, c_lo, t); |
1852 |
|
} |
1853 |
|
|
1854 |
|
/* -------------------------------------------------------------------------- */ |
1855 |
|
|
1856 |
|
/** |
1857 |
|
* SignExtendUltConst |
1858 |
|
* |
1859 |
|
* Rewrite sign_extend(x^n,m) < c^n+m to |
1860 |
|
* |
1861 |
|
* x < c[n-1:0] if (c <= (1 << (n - 1))) || (c >= (~0 << (n - 1))) |
1862 |
|
* x[n-1:n-1] = 0 if (1 << (n - 1)) < c <= (~0 << (n - 1)). |
1863 |
|
* |
1864 |
|
* Rewrite c^n+m < sign_extend(x^n,m) to |
1865 |
|
* |
1866 |
|
* c[n-1:0] < x if (c < (1 << (n - 1))) || (c >= ~(1 << (n-1))) |
1867 |
|
* x[n-1:n-1] = 1 if ~(~0 << (n-1)) <= c <= ~(1 << (n-1)) |
1868 |
|
* |
1869 |
|
* where ~(~0 << (n - 1)) == (1 << (n - 1)) - 1 |
1870 |
|
* |
1871 |
|
*/ |
1872 |
|
template <> |
1873 |
42126 |
inline bool RewriteRule<SignExtendUltConst>::applies(TNode node) |
1874 |
|
{ |
1875 |
84252 |
if (node.getKind() == kind::BITVECTOR_ULT |
1876 |
126726 |
&& ((node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND |
1877 |
46825 |
&& node[1].isConst()) |
1878 |
82779 |
|| (node[1].getKind() == kind::BITVECTOR_SIGN_EXTEND |
1879 |
47026 |
&& node[0].isConst()))) |
1880 |
|
{ |
1881 |
696 |
TNode x, c; |
1882 |
348 |
bool is_lhs = node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND; |
1883 |
348 |
if (is_lhs) |
1884 |
|
{ |
1885 |
176 |
x = node[0][0]; |
1886 |
176 |
c = node[1]; |
1887 |
|
} |
1888 |
|
else |
1889 |
|
{ |
1890 |
172 |
x = node[1][0]; |
1891 |
172 |
c = node[0]; |
1892 |
|
} |
1893 |
696 |
BitVector bv_c = c.getConst<BitVector>(); |
1894 |
348 |
unsigned size_c = utils::getSize(c); |
1895 |
348 |
unsigned msb_x_pos = utils::getSize(x) - 1; |
1896 |
|
// (1 << (n - 1))) |
1897 |
696 |
BitVector bv_msb_x(size_c); |
1898 |
348 |
bv_msb_x.setBit(msb_x_pos, true); |
1899 |
|
// (~0 << (n - 1)) |
1900 |
|
BitVector bv_upper_bits = |
1901 |
696 |
(~BitVector(size_c)).leftShift(BitVector(size_c, msb_x_pos)); |
1902 |
|
|
1903 |
|
return (is_lhs |
1904 |
176 |
&& (bv_c <= bv_msb_x || bv_c >= bv_upper_bits |
1905 |
104 |
|| (bv_msb_x < bv_c && bv_c <= bv_upper_bits))) |
1906 |
868 |
|| (!is_lhs |
1907 |
520 |
&& (bv_c < bv_msb_x || bv_c >= ~bv_msb_x |
1908 |
434 |
|| (~bv_upper_bits <= bv_c && bv_c <= ~bv_msb_x))); |
1909 |
|
} |
1910 |
41778 |
return false; |
1911 |
|
} |
1912 |
|
|
1913 |
|
template <> |
1914 |
174 |
inline Node RewriteRule<SignExtendUltConst>::apply(TNode node) |
1915 |
|
{ |
1916 |
348 |
TNode x, c; |
1917 |
174 |
bool is_lhs = node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND; |
1918 |
174 |
if (is_lhs) |
1919 |
|
{ |
1920 |
88 |
x = node[0][0]; |
1921 |
88 |
c = node[1]; |
1922 |
|
} |
1923 |
|
else |
1924 |
|
{ |
1925 |
86 |
x = node[1][0]; |
1926 |
86 |
c = node[0]; |
1927 |
|
} |
1928 |
348 |
BitVector bv_c = c.getConst<BitVector>(); |
1929 |
|
|
1930 |
174 |
unsigned size_c = utils::getSize(c); |
1931 |
174 |
unsigned msb_x_pos = utils::getSize(x) - 1; |
1932 |
348 |
Node c_lo = utils::mkConst(bv_c.extract(msb_x_pos, 0)); |
1933 |
|
// (1 << (n - 1))) |
1934 |
348 |
BitVector bv_msb_x(size_c); |
1935 |
174 |
bv_msb_x.setBit(msb_x_pos, true); |
1936 |
|
// (~0 << (n - 1)) |
1937 |
|
BitVector bv_upper_bits = |
1938 |
348 |
(~BitVector(size_c)).leftShift(BitVector(size_c, msb_x_pos)); |
1939 |
|
|
1940 |
174 |
NodeManager* nm = NodeManager::currentNM(); |
1941 |
174 |
if (is_lhs) |
1942 |
|
{ |
1943 |
|
// x[n-1:n-1] = 0 |
1944 |
88 |
if (bv_msb_x < bv_c && bv_c <= bv_upper_bits) |
1945 |
|
{ |
1946 |
120 |
Node msb_x = utils::mkExtract(x, msb_x_pos, msb_x_pos); |
1947 |
60 |
return nm->mkNode(kind::EQUAL, msb_x, utils::mkZero(1)); |
1948 |
|
} |
1949 |
|
// x < c[n-1:0] |
1950 |
28 |
Assert(bv_c <= bv_msb_x || bv_c >= bv_upper_bits); |
1951 |
28 |
return nm->mkNode(kind::BITVECTOR_ULT, x, c_lo); |
1952 |
|
} |
1953 |
|
|
1954 |
|
// x[n-1:n-1] = 1 |
1955 |
86 |
if (~bv_upper_bits <= bv_c && bv_c <= ~bv_msb_x) |
1956 |
|
{ |
1957 |
126 |
Node msb_x = utils::mkExtract(x, msb_x_pos, msb_x_pos); |
1958 |
63 |
return nm->mkNode(kind::EQUAL, msb_x, utils::mkOne(1)); |
1959 |
|
} |
1960 |
|
// c[n-1:0] < x |
1961 |
23 |
Assert(bv_c < bv_msb_x || bv_c >= ~bv_msb_x); |
1962 |
23 |
return nm->mkNode(kind::BITVECTOR_ULT, c_lo, x); |
1963 |
|
} |
1964 |
|
|
1965 |
|
/* -------------------------------------------------------------------------- */ |
1966 |
|
|
1967 |
|
template<> inline |
1968 |
4 |
bool RewriteRule<MultSlice>::applies(TNode node) { |
1969 |
4 |
if (node.getKind() != kind::BITVECTOR_MULT || node.getNumChildren() != 2) { |
1970 |
2 |
return false; |
1971 |
|
} |
1972 |
2 |
return utils::getSize(node[0]) % 2 == 0; |
1973 |
|
} |
1974 |
|
|
1975 |
|
/** |
1976 |
|
* Expressses the multiplication in terms of the top and bottom |
1977 |
|
* slices of the terms. Note increases circuit size, but could |
1978 |
|
* lead to simplifications (use wisely!). |
1979 |
|
* |
1980 |
|
* @param node |
1981 |
|
* |
1982 |
|
* @return |
1983 |
|
*/ |
1984 |
|
template <> |
1985 |
2 |
inline Node RewriteRule<MultSlice>::apply(TNode node) |
1986 |
|
{ |
1987 |
2 |
Debug("bv-rewrite") << "RewriteRule<MultSlice>(" << node << ")" << std::endl; |
1988 |
2 |
NodeManager *nm = NodeManager::currentNM(); |
1989 |
2 |
unsigned bitwidth = utils::getSize(node[0]); |
1990 |
4 |
Node zeros = utils::mkConst(bitwidth / 2, 0); |
1991 |
4 |
TNode a = node[0]; |
1992 |
4 |
Node bottom_a = utils::mkExtract(a, bitwidth / 2 - 1, 0); |
1993 |
4 |
Node top_a = utils::mkExtract(a, bitwidth - 1, bitwidth / 2); |
1994 |
4 |
TNode b = node[1]; |
1995 |
4 |
Node bottom_b = utils::mkExtract(b, bitwidth / 2 - 1, 0); |
1996 |
4 |
Node top_b = utils::mkExtract(b, bitwidth - 1, bitwidth / 2); |
1997 |
|
|
1998 |
|
Node term1 = nm->mkNode(kind::BITVECTOR_MULT, |
1999 |
4 |
nm->mkNode(kind::BITVECTOR_CONCAT, zeros, bottom_a), |
2000 |
8 |
nm->mkNode(kind::BITVECTOR_CONCAT, zeros, bottom_b)); |
2001 |
|
|
2002 |
|
Node term2 = nm->mkNode(kind::BITVECTOR_CONCAT, |
2003 |
4 |
nm->mkNode(kind::BITVECTOR_MULT, top_b, bottom_a), |
2004 |
8 |
zeros); |
2005 |
|
Node term3 = nm->mkNode(kind::BITVECTOR_CONCAT, |
2006 |
4 |
nm->mkNode(kind::BITVECTOR_MULT, top_a, bottom_b), |
2007 |
8 |
zeros); |
2008 |
4 |
return nm->mkNode(kind::BITVECTOR_ADD, term1, term2, term3); |
2009 |
|
} |
2010 |
|
|
2011 |
|
/* -------------------------------------------------------------------------- */ |
2012 |
|
|
2013 |
|
/** |
2014 |
|
* x < y + 1 <=> (not y < x) and y != 1...1 |
2015 |
|
* |
2016 |
|
* @param node |
2017 |
|
* |
2018 |
|
* @return |
2019 |
|
*/ |
2020 |
|
template <> |
2021 |
23 |
inline bool RewriteRule<UltAddOne>::applies(TNode node) |
2022 |
|
{ |
2023 |
23 |
if (node.getKind() != kind::BITVECTOR_ULT) return false; |
2024 |
|
TNode x = node[0]; |
2025 |
|
TNode y1 = node[1]; |
2026 |
|
if (y1.getKind() != kind::BITVECTOR_ADD) return false; |
2027 |
|
if (y1[0].getKind() != kind::CONST_BITVECTOR && |
2028 |
|
y1[1].getKind() != kind::CONST_BITVECTOR) |
2029 |
|
return false; |
2030 |
|
|
2031 |
|
if (y1[0].getKind() == kind::CONST_BITVECTOR && |
2032 |
|
y1[1].getKind() == kind::CONST_BITVECTOR) |
2033 |
|
return false; |
2034 |
|
|
2035 |
|
if (y1.getNumChildren() != 2) |
2036 |
|
return false; |
2037 |
|
|
2038 |
|
TNode one = y1[0].getKind() == kind::CONST_BITVECTOR ? y1[0] : y1[1]; |
2039 |
|
if (one != utils::mkConst(utils::getSize(one), 1)) return false; |
2040 |
|
return true; |
2041 |
|
} |
2042 |
|
|
2043 |
|
template <> |
2044 |
|
inline Node RewriteRule<UltAddOne>::apply(TNode node) |
2045 |
|
{ |
2046 |
|
Debug("bv-rewrite") << "RewriteRule<UltAddOne>(" << node << ")" << std::endl; |
2047 |
|
NodeManager *nm = NodeManager::currentNM(); |
2048 |
|
TNode x = node[0]; |
2049 |
|
TNode y1 = node[1]; |
2050 |
|
TNode y = y1[0].getKind() != kind::CONST_BITVECTOR ? y1[0] : y1[1]; |
2051 |
|
unsigned size = utils::getSize(x); |
2052 |
|
Node not_y_eq_1 = |
2053 |
|
nm->mkNode(kind::NOT, nm->mkNode(kind::EQUAL, y, utils::mkOnes(size))); |
2054 |
|
Node not_y_lt_x = |
2055 |
|
nm->mkNode(kind::NOT, nm->mkNode(kind::BITVECTOR_ULT, y, x)); |
2056 |
|
return nm->mkNode(kind::AND, not_y_eq_1, not_y_lt_x); |
2057 |
|
} |
2058 |
|
|
2059 |
|
/* -------------------------------------------------------------------------- */ |
2060 |
|
|
2061 |
|
/** |
2062 |
|
* Rewrite |
2063 |
|
* sign_extend(x+t,n) * sign_extend(a,m) < sign_extend(x,n) * sign_extend(a,m) |
2064 |
|
* to |
2065 |
|
* (and |
2066 |
|
* (not (= t zero)) |
2067 |
|
* (not (= a zero)) |
2068 |
|
* (= (bvslt (bvadd x t) x) (bvsgt a zero)) |
2069 |
|
* ) |
2070 |
|
* |
2071 |
|
* Rewrite |
2072 |
|
* zero_extend(x+t,n) * sign_extend(a,m) < zero_extend(x,n) * sign_extend(a,m) |
2073 |
|
* to |
2074 |
|
* (and |
2075 |
|
* (not (= t zero)) |
2076 |
|
* (not (= a zero)) |
2077 |
|
* (= (bvult (bvadd x t) x) (bvsgt a zero)) |
2078 |
|
* ) |
2079 |
|
* where n and m are sufficiently big to not produce an overflow for |
2080 |
|
* the multiplications. |
2081 |
|
* |
2082 |
|
* These patterns occur in the quantified BV benchmark family 'ranking', |
2083 |
|
* where the BV engine struggles due to the high bit widths of the |
2084 |
|
* multiplication's operands. |
2085 |
|
*/ |
2086 |
|
static std::tuple<Node, Node, bool> |
2087 |
10 |
extract_ext_tuple(TNode node) |
2088 |
|
{ |
2089 |
20 |
TNode a = node[0]; |
2090 |
20 |
TNode b = node[1]; |
2091 |
30 |
for (unsigned i = 0; i < 2; ++i) |
2092 |
|
{ |
2093 |
40 |
if (a.getKind() == kind::BITVECTOR_CONCAT |
2094 |
8 |
&& b.getKind() == kind::BITVECTOR_SIGN_EXTEND |
2095 |
20 |
&& a[0] == utils::mkZero(utils::getSize(a[0])) |
2096 |
20 |
&& utils::getSize(a[1]) <= utils::getSize(a[0]) |
2097 |
40 |
&& utils::getSize(b[0]) <= utils::getSignExtendAmount(b)) |
2098 |
|
{ |
2099 |
|
return std::make_tuple(a[1], b[0], false); |
2100 |
|
} |
2101 |
20 |
else if (i == 0 |
2102 |
10 |
&& a.getKind() == kind::BITVECTOR_SIGN_EXTEND |
2103 |
|
&& b.getKind() == kind::BITVECTOR_SIGN_EXTEND |
2104 |
20 |
&& utils::getSize(a[0]) <= utils::getSignExtendAmount(a) |
2105 |
20 |
&& utils::getSize(b[0]) <= utils::getSignExtendAmount(b)) |
2106 |
|
{ |
2107 |
|
return std::make_tuple(a[0], b[0], true); |
2108 |
|
} |
2109 |
20 |
std::swap(a, b); |
2110 |
|
} |
2111 |
10 |
return std::make_tuple(Node::null(), Node::null(), false); |
2112 |
|
} |
2113 |
|
|
2114 |
|
/* -------------------------------------------------------------------------- */ |
2115 |
|
|
2116 |
|
template<> inline |
2117 |
43944 |
bool RewriteRule<MultSltMult>::applies(TNode node) |
2118 |
|
{ |
2119 |
87888 |
if (node.getKind() != kind::BITVECTOR_SLT |
2120 |
86932 |
|| node[0].getKind() != kind::BITVECTOR_MULT |
2121 |
88936 |
|| node[1].getKind() != kind::BITVECTOR_MULT) |
2122 |
43924 |
return false; |
2123 |
|
|
2124 |
20 |
if (node[0].getNumChildren() > 2 || node[1].getNumChildren() > 2) |
2125 |
10 |
return false; |
2126 |
|
|
2127 |
|
bool is_sext_l, is_sext_r; |
2128 |
20 |
TNode ml[2], mr[2]; |
2129 |
|
|
2130 |
10 |
std::tie(ml[0], ml[1], is_sext_l) = extract_ext_tuple(node[0]); |
2131 |
10 |
if (ml[0].isNull()) |
2132 |
10 |
return false; |
2133 |
|
|
2134 |
|
std::tie(mr[0], mr[1], is_sext_r) = extract_ext_tuple(node[1]); |
2135 |
|
if (mr[0].isNull()) |
2136 |
|
return false; |
2137 |
|
|
2138 |
|
if (is_sext_l != is_sext_r) |
2139 |
|
return false; |
2140 |
|
|
2141 |
|
TNode addxt, x, a; |
2142 |
|
if (ml[0].getKind() == kind::BITVECTOR_ADD) |
2143 |
|
{ |
2144 |
|
addxt = ml[0]; |
2145 |
|
a = ml[1]; |
2146 |
|
} |
2147 |
|
else if (ml[1].getKind() == kind::BITVECTOR_ADD) |
2148 |
|
{ |
2149 |
|
addxt = ml[1]; |
2150 |
|
a = ml[0]; |
2151 |
|
} |
2152 |
|
else |
2153 |
|
return false; |
2154 |
|
|
2155 |
|
if (addxt.getNumChildren() > 2) |
2156 |
|
return false; |
2157 |
|
|
2158 |
|
if (mr[0] == a) |
2159 |
|
{ |
2160 |
|
x = mr[1]; |
2161 |
|
} |
2162 |
|
else if (mr[1] == a) |
2163 |
|
{ |
2164 |
|
x = mr[0]; |
2165 |
|
} |
2166 |
|
else |
2167 |
|
return false; |
2168 |
|
|
2169 |
|
return (addxt[0] == x || addxt[1] == x); |
2170 |
|
} |
2171 |
|
|
2172 |
|
template<> inline |
2173 |
|
Node RewriteRule<MultSltMult>::apply(TNode node) |
2174 |
|
{ |
2175 |
|
bool is_sext; |
2176 |
|
TNode ml[2], mr[2]; |
2177 |
|
|
2178 |
|
std::tie(ml[0], ml[1], is_sext) = extract_ext_tuple(node[0]); |
2179 |
|
std::tie(mr[0], mr[1], std::ignore) = extract_ext_tuple(node[1]); |
2180 |
|
|
2181 |
|
TNode addxt, x, t, a; |
2182 |
|
if (ml[0].getKind() == kind::BITVECTOR_ADD) |
2183 |
|
{ |
2184 |
|
addxt = ml[0]; |
2185 |
|
a = ml[1]; |
2186 |
|
} |
2187 |
|
else |
2188 |
|
{ |
2189 |
|
Assert(ml[1].getKind() == kind::BITVECTOR_ADD); |
2190 |
|
addxt = ml[1]; |
2191 |
|
a = ml[0]; |
2192 |
|
} |
2193 |
|
|
2194 |
|
x = (mr[0] == a) ? mr[1] : mr[0]; |
2195 |
|
t = (addxt[0] == x) ? addxt[1] : addxt[0]; |
2196 |
|
|
2197 |
|
NodeManager *nm = NodeManager::currentNM(); |
2198 |
|
Node zero_t = utils::mkZero(utils::getSize(t)); |
2199 |
|
Node zero_a = utils::mkZero(utils::getSize(a)); |
2200 |
|
|
2201 |
|
NodeBuilder nb(kind::AND); |
2202 |
|
Kind k = is_sext ? kind::BITVECTOR_SLT : kind::BITVECTOR_ULT; |
2203 |
|
nb << t.eqNode(zero_t).notNode(); |
2204 |
|
nb << a.eqNode(zero_a).notNode(); |
2205 |
|
nb << nm->mkNode(k, addxt, x) |
2206 |
|
.eqNode(nm->mkNode(kind::BITVECTOR_SGT, a, zero_a)); |
2207 |
|
return nb.constructNode(); |
2208 |
|
} |
2209 |
|
|
2210 |
|
} // namespace bv |
2211 |
|
} // namespace theory |
2212 |
|
} // namespace cvc5 |