1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Yoni Zohar, Liana Hadarean, Aina Niemetz |
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 |
|
|
27 |
|
namespace cvc5 { |
28 |
|
namespace theory { |
29 |
|
namespace bv { |
30 |
|
|
31 |
|
/* |
32 |
|
* This rewrite is not meant to be used by the BV rewriter. |
33 |
|
* It is specifically designed for the bv-to-int preprocessing pass. |
34 |
|
* Based on Hacker's Delight section 2-2 equation a: |
35 |
|
* -x = ~x+1 |
36 |
|
*/ |
37 |
|
template <> |
38 |
2077 |
inline bool RewriteRule<NegEliminate>::applies(TNode node) |
39 |
|
{ |
40 |
2077 |
return (node.getKind() == kind::BITVECTOR_NEG); |
41 |
|
} |
42 |
|
|
43 |
|
template <> |
44 |
34 |
inline Node RewriteRule<NegEliminate>::apply(TNode node) |
45 |
|
{ |
46 |
68 |
Debug("bv-rewrite") << "RewriteRule<NegEliminate>(" << node << ")" |
47 |
34 |
<< std::endl; |
48 |
34 |
NodeManager* nm = NodeManager::currentNM(); |
49 |
68 |
TNode a = node[0]; |
50 |
34 |
unsigned size = utils::getSize(a); |
51 |
68 |
Node one = utils::mkOne(size); |
52 |
68 |
Node nota = nm->mkNode(kind::BITVECTOR_NOT, a); |
53 |
34 |
Node bvadd = nm->mkNode(kind::BITVECTOR_ADD, nota, one); |
54 |
68 |
return bvadd; |
55 |
|
} |
56 |
|
|
57 |
|
/* |
58 |
|
* This rewrite is not meant to be used by the BV rewriter. |
59 |
|
* It is specifically designed for the bv-to-int preprocessing pass. |
60 |
|
* Based on Hacker's Delight section 2-2 equation h: |
61 |
|
* x+y = x|y + x&y |
62 |
|
*/ |
63 |
|
template <> |
64 |
2075 |
inline bool RewriteRule<OrEliminate>::applies(TNode node) |
65 |
|
{ |
66 |
2075 |
return (node.getKind() == kind::BITVECTOR_OR); |
67 |
|
} |
68 |
|
|
69 |
|
template <> |
70 |
32 |
inline Node RewriteRule<OrEliminate>::apply(TNode node) |
71 |
|
{ |
72 |
64 |
Debug("bv-rewrite") << "RewriteRule<OrEliminate>(" << node << ")" |
73 |
32 |
<< std::endl; |
74 |
32 |
NodeManager* nm = NodeManager::currentNM(); |
75 |
64 |
TNode a = node[0]; |
76 |
64 |
TNode b = node[1]; |
77 |
64 |
Node bvadd = nm->mkNode(kind::BITVECTOR_ADD, a, b); |
78 |
64 |
Node bvand = nm->mkNode(kind::BITVECTOR_AND, a, b); |
79 |
|
Node result = |
80 |
32 |
nm->mkNode(kind::BITVECTOR_SUB, bvadd, bvand); |
81 |
64 |
return result; |
82 |
|
} |
83 |
|
|
84 |
|
/* |
85 |
|
* This rewrite is not meant to be used by the BV rewriter. |
86 |
|
* It is specifically designed for the bv-to-int preprocessing pass. |
87 |
|
* Based on Hacker's Delight section 2-2 equation n: |
88 |
|
* x xor y = x|y - x&y |
89 |
|
*/ |
90 |
|
template <> |
91 |
2043 |
inline bool RewriteRule<XorEliminate>::applies(TNode node) |
92 |
|
{ |
93 |
2043 |
return (node.getKind() == kind::BITVECTOR_XOR); |
94 |
|
} |
95 |
|
|
96 |
|
template <> |
97 |
|
inline Node RewriteRule<XorEliminate>::apply(TNode node) |
98 |
|
{ |
99 |
|
Debug("bv-rewrite") << "RewriteRule<XorEliminate>(" << node << ")" |
100 |
|
<< std::endl; |
101 |
|
NodeManager* nm = NodeManager::currentNM(); |
102 |
|
TNode a = node[0]; |
103 |
|
TNode b = node[1]; |
104 |
|
Node bvor = nm->mkNode(kind::BITVECTOR_OR, a, b); |
105 |
|
Node bvand = nm->mkNode(kind::BITVECTOR_AND, a, b); |
106 |
|
Node result = nm->mkNode(kind::BITVECTOR_SUB, bvor, bvand); |
107 |
|
return result; |
108 |
|
} |
109 |
|
|
110 |
|
template <> |
111 |
7610 |
inline bool RewriteRule<UgtEliminate>::applies(TNode node) |
112 |
|
{ |
113 |
7610 |
return (node.getKind() == kind::BITVECTOR_UGT); |
114 |
|
} |
115 |
|
|
116 |
|
template <> |
117 |
3799 |
inline Node RewriteRule<UgtEliminate>::apply(TNode node) |
118 |
|
{ |
119 |
7598 |
Debug("bv-rewrite") << "RewriteRule<UgtEliminate>(" << node << ")" |
120 |
3799 |
<< std::endl; |
121 |
7598 |
TNode a = node[0]; |
122 |
7598 |
TNode b = node[1]; |
123 |
3799 |
Node result = NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, b, a); |
124 |
7598 |
return result; |
125 |
|
} |
126 |
|
|
127 |
|
template <> |
128 |
7100 |
inline bool RewriteRule<UgeEliminate>::applies(TNode node) |
129 |
|
{ |
130 |
7100 |
return (node.getKind() == kind::BITVECTOR_UGE); |
131 |
|
} |
132 |
|
|
133 |
|
template <> |
134 |
3550 |
inline Node RewriteRule<UgeEliminate>::apply(TNode node) |
135 |
|
{ |
136 |
7100 |
Debug("bv-rewrite") << "RewriteRule<UgeEliminate>(" << node << ")" |
137 |
3550 |
<< std::endl; |
138 |
7100 |
TNode a = node[0]; |
139 |
7100 |
TNode b = node[1]; |
140 |
3550 |
Node result = NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULE, b, a); |
141 |
7100 |
return result; |
142 |
|
} |
143 |
|
|
144 |
|
template <> |
145 |
9785 |
inline bool RewriteRule<SgtEliminate>::applies(TNode node) |
146 |
|
{ |
147 |
9785 |
return (node.getKind() == kind::BITVECTOR_SGT); |
148 |
|
} |
149 |
|
|
150 |
|
template <> |
151 |
3871 |
inline Node RewriteRule<SgtEliminate>::apply(TNode node) |
152 |
|
{ |
153 |
7742 |
Debug("bv-rewrite") << "RewriteRule<SgtEliminate>(" << node << ")" |
154 |
3871 |
<< std::endl; |
155 |
7742 |
TNode a = node[0]; |
156 |
7742 |
TNode b = node[1]; |
157 |
3871 |
Node result = NodeManager::currentNM()->mkNode(kind::BITVECTOR_SLT, b, a); |
158 |
7742 |
return result; |
159 |
|
} |
160 |
|
|
161 |
|
template <> |
162 |
9301 |
inline bool RewriteRule<SgeEliminate>::applies(TNode node) |
163 |
|
{ |
164 |
9301 |
return (node.getKind() == kind::BITVECTOR_SGE); |
165 |
|
} |
166 |
|
|
167 |
|
template <> |
168 |
3629 |
inline Node RewriteRule<SgeEliminate>::apply(TNode node) |
169 |
|
{ |
170 |
7258 |
Debug("bv-rewrite") << "RewriteRule<SgeEliminate>(" << node << ")" |
171 |
3629 |
<< std::endl; |
172 |
7258 |
TNode a = node[0]; |
173 |
7258 |
TNode b = node[1]; |
174 |
3629 |
Node result = NodeManager::currentNM()->mkNode(kind::BITVECTOR_SLE, b, a); |
175 |
7258 |
return result; |
176 |
|
} |
177 |
|
|
178 |
|
template <> |
179 |
2058 |
inline bool RewriteRule<SltEliminate>::applies(TNode node) |
180 |
|
{ |
181 |
2058 |
return (node.getKind() == kind::BITVECTOR_SLT); |
182 |
|
} |
183 |
|
|
184 |
|
template <> |
185 |
15 |
inline Node RewriteRule<SltEliminate>::apply(TNode node) |
186 |
|
{ |
187 |
30 |
Debug("bv-rewrite") << "RewriteRule<SltEliminate>(" << node << ")" |
188 |
15 |
<< std::endl; |
189 |
15 |
NodeManager *nm = NodeManager::currentNM(); |
190 |
15 |
unsigned size = utils::getSize(node[0]); |
191 |
30 |
Integer val = Integer(1).multiplyByPow2(size - 1); |
192 |
30 |
Node pow_two = utils::mkConst(size, val); |
193 |
30 |
Node a = nm->mkNode(kind::BITVECTOR_ADD, node[0], pow_two); |
194 |
30 |
Node b = nm->mkNode(kind::BITVECTOR_ADD, node[1], pow_two); |
195 |
|
|
196 |
30 |
return nm->mkNode(kind::BITVECTOR_ULT, a, b); |
197 |
|
} |
198 |
|
|
199 |
|
template <> |
200 |
16730 |
inline bool RewriteRule<SleEliminate>::applies(TNode node) |
201 |
|
{ |
202 |
16730 |
return (node.getKind() == kind::BITVECTOR_SLE); |
203 |
|
} |
204 |
|
|
205 |
|
template <> |
206 |
7330 |
inline Node RewriteRule<SleEliminate>::apply(TNode node) |
207 |
|
{ |
208 |
14660 |
Debug("bv-rewrite") << "RewriteRule<SleEliminate>(" << node << ")" |
209 |
7330 |
<< std::endl; |
210 |
7330 |
NodeManager *nm = NodeManager::currentNM(); |
211 |
14660 |
TNode a = node[0]; |
212 |
14660 |
TNode b = node[1]; |
213 |
14660 |
Node b_slt_a = nm->mkNode(kind::BITVECTOR_SLT, b, a); |
214 |
14660 |
return nm->mkNode(kind::NOT, b_slt_a); |
215 |
|
} |
216 |
|
|
217 |
|
template <> |
218 |
14089 |
inline bool RewriteRule<UleEliminate>::applies(TNode node) |
219 |
|
{ |
220 |
14089 |
return (node.getKind() == kind::BITVECTOR_ULE); |
221 |
|
} |
222 |
|
|
223 |
|
template <> |
224 |
6967 |
inline Node RewriteRule<UleEliminate>::apply(TNode node) |
225 |
|
{ |
226 |
13934 |
Debug("bv-rewrite") << "RewriteRule<UleEliminate>(" << node << ")" |
227 |
6967 |
<< std::endl; |
228 |
6967 |
NodeManager *nm = NodeManager::currentNM(); |
229 |
13934 |
TNode a = node[0]; |
230 |
13934 |
TNode b = node[1]; |
231 |
13934 |
Node b_ult_a = nm->mkNode(kind::BITVECTOR_ULT, b, a); |
232 |
13934 |
return nm->mkNode(kind::NOT, b_ult_a); |
233 |
|
} |
234 |
|
|
235 |
|
template <> |
236 |
2043 |
inline bool RewriteRule<CompEliminate>::applies(TNode node) |
237 |
|
{ |
238 |
2043 |
return (node.getKind() == kind::BITVECTOR_COMP); |
239 |
|
} |
240 |
|
|
241 |
|
template <> |
242 |
|
inline Node RewriteRule<CompEliminate>::apply(TNode node) |
243 |
|
{ |
244 |
|
Debug("bv-rewrite") << "RewriteRule<CompEliminate>(" << node << ")" |
245 |
|
<< std::endl; |
246 |
|
NodeManager *nm = NodeManager::currentNM(); |
247 |
|
Node comp = nm->mkNode(kind::EQUAL, node[0], node[1]); |
248 |
|
Node one = utils::mkConst(1, 1); |
249 |
|
Node zero = utils::mkConst(1, 0); |
250 |
|
|
251 |
|
return nm->mkNode(kind::ITE, comp, one, zero); |
252 |
|
} |
253 |
|
|
254 |
|
template <> |
255 |
7113 |
inline bool RewriteRule<SubEliminate>::applies(TNode node) |
256 |
|
{ |
257 |
7113 |
return (node.getKind() == kind::BITVECTOR_SUB); |
258 |
|
} |
259 |
|
|
260 |
|
template <> |
261 |
2551 |
inline Node RewriteRule<SubEliminate>::apply(TNode node) |
262 |
|
{ |
263 |
5102 |
Debug("bv-rewrite") << "RewriteRule<SubEliminate>(" << node << ")" |
264 |
2551 |
<< std::endl; |
265 |
2551 |
NodeManager *nm = NodeManager::currentNM(); |
266 |
5102 |
Node negb = nm->mkNode(kind::BITVECTOR_NEG, node[1]); |
267 |
5102 |
Node a = node[0]; |
268 |
|
|
269 |
5102 |
return nm->mkNode(kind::BITVECTOR_ADD, a, negb); |
270 |
|
} |
271 |
|
|
272 |
|
template <> |
273 |
3811 |
inline bool RewriteRule<RepeatEliminate>::applies(TNode node) |
274 |
|
{ |
275 |
3811 |
return (node.getKind() == kind::BITVECTOR_REPEAT); |
276 |
|
} |
277 |
|
|
278 |
|
template <> |
279 |
884 |
inline Node RewriteRule<RepeatEliminate>::apply(TNode node) |
280 |
|
{ |
281 |
884 |
Debug("bv-rewrite") << "RewriteRule<RepeatEliminate>(" << node << ")" << std::endl; |
282 |
1768 |
TNode a = node[0]; |
283 |
|
unsigned amount = |
284 |
884 |
node.getOperator().getConst<BitVectorRepeat>().d_repeatAmount; |
285 |
884 |
Assert(amount >= 1); |
286 |
884 |
if(amount == 1) { |
287 |
562 |
return a; |
288 |
|
} |
289 |
644 |
NodeBuilder result(kind::BITVECTOR_CONCAT); |
290 |
1708 |
for(unsigned i = 0; i < amount; ++i) { |
291 |
1386 |
result << node[0]; |
292 |
|
} |
293 |
644 |
Node resultNode = result; |
294 |
322 |
return resultNode; |
295 |
|
} |
296 |
|
|
297 |
|
template <> |
298 |
3569 |
inline bool RewriteRule<RotateLeftEliminate>::applies(TNode node) |
299 |
|
{ |
300 |
3569 |
return (node.getKind() == kind::BITVECTOR_ROTATE_LEFT); |
301 |
|
} |
302 |
|
|
303 |
|
template <> |
304 |
763 |
inline Node RewriteRule<RotateLeftEliminate>::apply(TNode node) |
305 |
|
{ |
306 |
763 |
Debug("bv-rewrite") << "RewriteRule<RotateLeftEliminate>(" << node << ")" << std::endl; |
307 |
1526 |
TNode a = node[0]; |
308 |
|
unsigned amount = |
309 |
763 |
node.getOperator().getConst<BitVectorRotateLeft>().d_rotateLeftAmount; |
310 |
763 |
amount = amount % utils::getSize(a); |
311 |
763 |
if (amount == 0) { |
312 |
441 |
return a; |
313 |
|
} |
314 |
|
|
315 |
644 |
Node left = utils::mkExtract(a, utils::getSize(a)-1 - amount, 0); |
316 |
644 |
Node right = utils::mkExtract(a, utils::getSize(a) -1, utils::getSize(a) - amount); |
317 |
644 |
Node result = utils::mkConcat(left, right); |
318 |
|
|
319 |
322 |
return result; |
320 |
|
} |
321 |
|
|
322 |
|
template <> |
323 |
3757 |
inline bool RewriteRule<RotateRightEliminate>::applies(TNode node) |
324 |
|
{ |
325 |
3757 |
return (node.getKind() == kind::BITVECTOR_ROTATE_RIGHT); |
326 |
|
} |
327 |
|
|
328 |
|
template <> |
329 |
857 |
inline Node RewriteRule<RotateRightEliminate>::apply(TNode node) |
330 |
|
{ |
331 |
857 |
Debug("bv-rewrite") << "RewriteRule<RotateRightEliminate>(" << node << ")" << std::endl; |
332 |
1714 |
TNode a = node[0]; |
333 |
|
unsigned amount = |
334 |
857 |
node.getOperator().getConst<BitVectorRotateRight>().d_rotateRightAmount; |
335 |
857 |
amount = amount % utils::getSize(a); |
336 |
857 |
if (amount == 0) { |
337 |
375 |
return a; |
338 |
|
} |
339 |
|
|
340 |
964 |
Node left = utils::mkExtract(a, amount - 1, 0); |
341 |
964 |
Node right = utils::mkExtract(a, utils::getSize(a)-1, amount); |
342 |
964 |
Node result = utils::mkConcat(left, right); |
343 |
|
|
344 |
482 |
return result; |
345 |
|
} |
346 |
|
|
347 |
|
template <> |
348 |
394 |
inline bool RewriteRule<BVToNatEliminate>::applies(TNode node) |
349 |
|
{ |
350 |
394 |
return (node.getKind() == kind::BITVECTOR_TO_NAT); |
351 |
|
} |
352 |
|
|
353 |
|
template <> |
354 |
197 |
inline Node RewriteRule<BVToNatEliminate>::apply(TNode node) |
355 |
|
{ |
356 |
197 |
Debug("bv-rewrite") << "RewriteRule<BVToNatEliminate>(" << node << ")" << std::endl; |
357 |
|
|
358 |
|
//if( node[0].isConst() ){ |
359 |
|
//TODO? direct computation instead of term construction+rewriting |
360 |
|
//} |
361 |
197 |
return utils::eliminateBv2Nat(node); |
362 |
|
} |
363 |
|
|
364 |
|
template <> |
365 |
550 |
inline bool RewriteRule<IntToBVEliminate>::applies(TNode node) |
366 |
|
{ |
367 |
550 |
return (node.getKind() == kind::INT_TO_BITVECTOR); |
368 |
|
} |
369 |
|
|
370 |
|
template <> |
371 |
275 |
inline Node RewriteRule<IntToBVEliminate>::apply(TNode node) |
372 |
|
{ |
373 |
275 |
Debug("bv-rewrite") << "RewriteRule<IntToBVEliminate>(" << node << ")" << std::endl; |
374 |
|
|
375 |
|
//if( node[0].isConst() ){ |
376 |
|
//TODO? direct computation instead of term construction+rewriting |
377 |
|
//} |
378 |
275 |
return utils::eliminateInt2Bv(node); |
379 |
|
} |
380 |
|
|
381 |
|
template <> |
382 |
3473 |
inline bool RewriteRule<NandEliminate>::applies(TNode node) |
383 |
|
{ |
384 |
4903 |
return (node.getKind() == kind::BITVECTOR_NAND && |
385 |
4903 |
node.getNumChildren() == 2); |
386 |
|
} |
387 |
|
|
388 |
|
template <> |
389 |
715 |
inline Node RewriteRule<NandEliminate>::apply(TNode node) |
390 |
|
{ |
391 |
1430 |
Debug("bv-rewrite") << "RewriteRule<NandEliminate>(" << node << ")" |
392 |
715 |
<< std::endl; |
393 |
715 |
NodeManager *nm = NodeManager::currentNM(); |
394 |
1430 |
TNode a = node[0]; |
395 |
1430 |
TNode b = node[1]; |
396 |
1430 |
Node andNode = nm->mkNode(kind::BITVECTOR_AND, a, b); |
397 |
715 |
Node result = nm->mkNode(kind::BITVECTOR_NOT, andNode); |
398 |
1430 |
return result; |
399 |
|
} |
400 |
|
|
401 |
|
template <> |
402 |
3877 |
inline bool RewriteRule<NorEliminate>::applies(TNode node) |
403 |
|
{ |
404 |
3877 |
return (node.getKind() == kind::BITVECTOR_NOR && node.getNumChildren() == 2); |
405 |
|
} |
406 |
|
|
407 |
|
template <> |
408 |
917 |
inline Node RewriteRule<NorEliminate>::apply(TNode node) |
409 |
|
{ |
410 |
1834 |
Debug("bv-rewrite") << "RewriteRule<NorEliminate>(" << node << ")" |
411 |
917 |
<< std::endl; |
412 |
917 |
NodeManager *nm = NodeManager::currentNM(); |
413 |
1834 |
TNode a = node[0]; |
414 |
1834 |
TNode b = node[1]; |
415 |
1834 |
Node orNode = nm->mkNode(kind::BITVECTOR_OR, a, b); |
416 |
917 |
Node result = nm->mkNode(kind::BITVECTOR_NOT, orNode); |
417 |
1834 |
return result; |
418 |
|
} |
419 |
|
|
420 |
|
template <> |
421 |
4067 |
inline bool RewriteRule<XnorEliminate>::applies(TNode node) |
422 |
|
{ |
423 |
6091 |
return (node.getKind() == kind::BITVECTOR_XNOR && |
424 |
6091 |
node.getNumChildren() == 2); |
425 |
|
} |
426 |
|
|
427 |
|
template <> |
428 |
1012 |
inline Node RewriteRule<XnorEliminate>::apply(TNode node) |
429 |
|
{ |
430 |
2024 |
Debug("bv-rewrite") << "RewriteRule<XnorEliminate>(" << node << ")" |
431 |
1012 |
<< std::endl; |
432 |
1012 |
NodeManager *nm = NodeManager::currentNM(); |
433 |
2024 |
TNode a = node[0]; |
434 |
2024 |
TNode b = node[1]; |
435 |
2024 |
Node xorNode = nm->mkNode(kind::BITVECTOR_XOR, a, b); |
436 |
1012 |
Node result = nm->mkNode(kind::BITVECTOR_NOT, xorNode); |
437 |
2024 |
return result; |
438 |
|
} |
439 |
|
|
440 |
|
template <> |
441 |
311 |
inline bool RewriteRule<SdivEliminate>::applies(TNode node) |
442 |
|
{ |
443 |
311 |
return (node.getKind() == kind::BITVECTOR_SDIV); |
444 |
|
} |
445 |
|
|
446 |
|
template <> |
447 |
154 |
inline Node RewriteRule<SdivEliminate>::apply(TNode node) |
448 |
|
{ |
449 |
308 |
Debug("bv-rewrite") << "RewriteRule<SdivEliminate>(" << node << ")" |
450 |
154 |
<< std::endl; |
451 |
|
|
452 |
154 |
NodeManager *nm = NodeManager::currentNM(); |
453 |
308 |
TNode a = node[0]; |
454 |
308 |
TNode b = node[1]; |
455 |
154 |
unsigned size = utils::getSize(a); |
456 |
|
|
457 |
308 |
Node one = utils::mkConst(1, 1); |
458 |
|
Node a_lt_0 = |
459 |
308 |
nm->mkNode(kind::EQUAL, utils::mkExtract(a, size - 1, size - 1), one); |
460 |
|
Node b_lt_0 = |
461 |
308 |
nm->mkNode(kind::EQUAL, utils::mkExtract(b, size - 1, size - 1), one); |
462 |
|
Node abs_a = |
463 |
308 |
nm->mkNode(kind::ITE, a_lt_0, nm->mkNode(kind::BITVECTOR_NEG, a), a); |
464 |
|
Node abs_b = |
465 |
308 |
nm->mkNode(kind::ITE, b_lt_0, nm->mkNode(kind::BITVECTOR_NEG, b), b); |
466 |
|
|
467 |
308 |
Node a_udiv_b = nm->mkNode(kind::BITVECTOR_UDIV, abs_a, abs_b); |
468 |
308 |
Node neg_result = nm->mkNode(kind::BITVECTOR_NEG, a_udiv_b); |
469 |
|
|
470 |
308 |
Node condition = nm->mkNode(kind::XOR, a_lt_0, b_lt_0); |
471 |
154 |
Node result = nm->mkNode(kind::ITE, condition, neg_result, a_udiv_b); |
472 |
|
|
473 |
308 |
return result; |
474 |
|
} |
475 |
|
|
476 |
|
/* |
477 |
|
* This rewrite is not meant to be used by the BV rewriter |
478 |
|
* It is specifically designed for the bv-to-int preprocessing pass. |
479 |
|
* Similar to ordinary sdiv elimination. |
480 |
|
* The sign-check is done with bvult instead of bit-extraction. |
481 |
|
*/ |
482 |
|
template <> |
483 |
2043 |
inline bool RewriteRule<SdivEliminateFewerBitwiseOps>::applies(TNode node) |
484 |
|
{ |
485 |
2043 |
return (node.getKind() == kind::BITVECTOR_SDIV); |
486 |
|
} |
487 |
|
|
488 |
|
template <> |
489 |
|
inline Node RewriteRule<SdivEliminateFewerBitwiseOps>::apply(TNode node) |
490 |
|
{ |
491 |
|
Debug("bv-rewrite") << "RewriteRule<SdivEliminateFewerBitwiseOps>(" << node |
492 |
|
<< ")" << std::endl; |
493 |
|
|
494 |
|
NodeManager* nm = NodeManager::currentNM(); |
495 |
|
TNode a = node[0]; |
496 |
|
TNode b = node[1]; |
497 |
|
unsigned size = utils::getSize(a); |
498 |
|
Node a_lt_0 = nm->mkNode(kind::BITVECTOR_UGE, a, utils::mkMinSigned(size)); |
499 |
|
Node b_lt_0 = nm->mkNode(kind::BITVECTOR_UGE, b, utils::mkMinSigned(size)); |
500 |
|
Node abs_a = |
501 |
|
nm->mkNode(kind::ITE, a_lt_0, nm->mkNode(kind::BITVECTOR_NEG, a), a); |
502 |
|
Node abs_b = |
503 |
|
nm->mkNode(kind::ITE, b_lt_0, nm->mkNode(kind::BITVECTOR_NEG, b), b); |
504 |
|
|
505 |
|
Node a_udiv_b = nm->mkNode(kind::BITVECTOR_UDIV, abs_a, abs_b); |
506 |
|
Node neg_result = nm->mkNode(kind::BITVECTOR_NEG, a_udiv_b); |
507 |
|
|
508 |
|
Node result = nm->mkNode(kind::ITE, a_lt_0.xorNode(b_lt_0), neg_result, a_udiv_b); |
509 |
|
|
510 |
|
return result; |
511 |
|
} |
512 |
|
|
513 |
|
template <> |
514 |
153 |
inline bool RewriteRule<SremEliminate>::applies(TNode node) |
515 |
|
{ |
516 |
153 |
return (node.getKind() == kind::BITVECTOR_SREM); |
517 |
|
} |
518 |
|
|
519 |
|
template <> |
520 |
74 |
inline Node RewriteRule<SremEliminate>::apply(TNode node) |
521 |
|
{ |
522 |
148 |
Debug("bv-rewrite") << "RewriteRule<SremEliminate>(" << node << ")" |
523 |
74 |
<< std::endl; |
524 |
74 |
NodeManager *nm = NodeManager::currentNM(); |
525 |
148 |
TNode a = node[0]; |
526 |
148 |
TNode b = node[1]; |
527 |
74 |
unsigned size = utils::getSize(a); |
528 |
|
|
529 |
148 |
Node one = utils::mkConst(1, 1); |
530 |
|
Node a_lt_0 = |
531 |
148 |
nm->mkNode(kind::EQUAL, utils::mkExtract(a, size - 1, size - 1), one); |
532 |
|
Node b_lt_0 = |
533 |
148 |
nm->mkNode(kind::EQUAL, utils::mkExtract(b, size - 1, size - 1), one); |
534 |
|
Node abs_a = |
535 |
148 |
nm->mkNode(kind::ITE, a_lt_0, nm->mkNode(kind::BITVECTOR_NEG, a), a); |
536 |
|
Node abs_b = |
537 |
148 |
nm->mkNode(kind::ITE, b_lt_0, nm->mkNode(kind::BITVECTOR_NEG, b), b); |
538 |
|
|
539 |
148 |
Node a_urem_b = nm->mkNode(kind::BITVECTOR_UREM, abs_a, abs_b); |
540 |
148 |
Node neg_result = nm->mkNode(kind::BITVECTOR_NEG, a_urem_b); |
541 |
|
|
542 |
74 |
Node result = nm->mkNode(kind::ITE, a_lt_0, neg_result, a_urem_b); |
543 |
|
|
544 |
148 |
return result; |
545 |
|
} |
546 |
|
|
547 |
|
/* |
548 |
|
* This rewrite is not meant to be used by the BV rewriter |
549 |
|
* It is specifically designed for the bv-to-int preprocessing pass. |
550 |
|
* Similar to ordinary srem elimination. |
551 |
|
* The sign-check is done with bvult instead of bit-extraction. |
552 |
|
*/ |
553 |
|
template <> |
554 |
2043 |
inline bool RewriteRule<SremEliminateFewerBitwiseOps>::applies(TNode node) |
555 |
|
{ |
556 |
2043 |
return (node.getKind() == kind::BITVECTOR_SREM); |
557 |
|
} |
558 |
|
|
559 |
|
template <> |
560 |
|
inline Node RewriteRule<SremEliminateFewerBitwiseOps>::apply(TNode node) |
561 |
|
{ |
562 |
|
Debug("bv-rewrite") << "RewriteRule<SremEliminateFewerBitwiseOps>(" << node |
563 |
|
<< ")" << std::endl; |
564 |
|
NodeManager* nm = NodeManager::currentNM(); |
565 |
|
TNode a = node[0]; |
566 |
|
TNode b = node[1]; |
567 |
|
unsigned size = utils::getSize(a); |
568 |
|
Node a_lt_0 = nm->mkNode(kind::BITVECTOR_UGE, a, utils::mkMinSigned(size)); |
569 |
|
Node b_lt_0 = nm->mkNode(kind::BITVECTOR_UGE, b, utils::mkMinSigned(size)); |
570 |
|
Node abs_a = |
571 |
|
nm->mkNode(kind::ITE, a_lt_0, nm->mkNode(kind::BITVECTOR_NEG, a), a); |
572 |
|
Node abs_b = |
573 |
|
nm->mkNode(kind::ITE, b_lt_0, nm->mkNode(kind::BITVECTOR_NEG, b), b); |
574 |
|
Node a_urem_b = nm->mkNode(kind::BITVECTOR_UREM, abs_a, abs_b); |
575 |
|
Node neg_result = nm->mkNode(kind::BITVECTOR_NEG, a_urem_b); |
576 |
|
|
577 |
|
Node result = nm->mkNode(kind::ITE, a_lt_0, neg_result, a_urem_b); |
578 |
|
|
579 |
|
return result; |
580 |
|
} |
581 |
|
|
582 |
|
template <> |
583 |
236 |
inline bool RewriteRule<SmodEliminate>::applies(TNode node) |
584 |
|
{ |
585 |
236 |
return (node.getKind() == kind::BITVECTOR_SMOD); |
586 |
|
} |
587 |
|
|
588 |
|
template <> |
589 |
114 |
inline Node RewriteRule<SmodEliminate>::apply(TNode node) |
590 |
|
{ |
591 |
228 |
Debug("bv-rewrite") << "RewriteRule<SmodEliminate>(" << node << ")" |
592 |
114 |
<< std::endl; |
593 |
114 |
NodeManager *nm = NodeManager::currentNM(); |
594 |
228 |
TNode s = node[0]; |
595 |
228 |
TNode t = node[1]; |
596 |
114 |
unsigned size = utils::getSize(s); |
597 |
|
|
598 |
|
// (bvsmod s t) abbreviates |
599 |
|
// (let ((?msb_s ((_ extract |m-1| |m-1|) s)) |
600 |
|
// (?msb_t ((_ extract |m-1| |m-1|) t))) |
601 |
|
// (let ((abs_s (ite (= ?msb_s #b0) s (bvneg s))) |
602 |
|
// (abs_t (ite (= ?msb_t #b0) t (bvneg t)))) |
603 |
|
// (let ((u (bvurem abs_s abs_t))) |
604 |
|
// (ite (= u (_ bv0 m)) |
605 |
|
// u |
606 |
|
// (ite (and (= ?msb_s #b0) (= ?msb_t #b0)) |
607 |
|
// u |
608 |
|
// (ite (and (= ?msb_s #b1) (= ?msb_t #b0)) |
609 |
|
// (bvadd (bvneg u) t) |
610 |
|
// (ite (and (= ?msb_s #b0) (= ?msb_t #b1)) |
611 |
|
// (bvadd u t) |
612 |
|
// (bvneg u)))))))) |
613 |
|
|
614 |
228 |
Node msb_s = utils::mkExtract(s, size - 1, size - 1); |
615 |
228 |
Node msb_t = utils::mkExtract(t, size - 1, size - 1); |
616 |
|
|
617 |
228 |
Node bit1 = utils::mkConst(1, 1); |
618 |
228 |
Node bit0 = utils::mkConst(1, 0); |
619 |
|
|
620 |
|
Node abs_s = |
621 |
228 |
msb_s.eqNode(bit0).iteNode(s, nm->mkNode(kind::BITVECTOR_NEG, s)); |
622 |
|
Node abs_t = |
623 |
228 |
msb_t.eqNode(bit0).iteNode(t, nm->mkNode(kind::BITVECTOR_NEG, t)); |
624 |
|
|
625 |
228 |
Node u = nm->mkNode(kind::BITVECTOR_UREM, abs_s, abs_t); |
626 |
228 |
Node neg_u = nm->mkNode(kind::BITVECTOR_NEG, u); |
627 |
|
|
628 |
228 |
Node cond0 = u.eqNode(utils::mkConst(size, 0)); |
629 |
228 |
Node cond1 = msb_s.eqNode(bit0).andNode(msb_t.eqNode(bit0)); |
630 |
228 |
Node cond2 = msb_s.eqNode(bit1).andNode(msb_t.eqNode(bit0)); |
631 |
228 |
Node cond3 = msb_s.eqNode(bit0).andNode(msb_t.eqNode(bit1)); |
632 |
|
|
633 |
|
Node result = cond0.iteNode( |
634 |
|
u, |
635 |
228 |
cond1.iteNode( |
636 |
|
u, |
637 |
228 |
cond2.iteNode( |
638 |
228 |
nm->mkNode(kind::BITVECTOR_ADD, neg_u, t), |
639 |
342 |
cond3.iteNode(nm->mkNode(kind::BITVECTOR_ADD, u, t), neg_u)))); |
640 |
|
|
641 |
228 |
return result; |
642 |
|
} |
643 |
|
|
644 |
|
/* |
645 |
|
* This rewrite is not meant to be used by the BV rewriter |
646 |
|
* It is specifically designed for the bv-to-int preprocessing pass. |
647 |
|
* Similar to ordinary smod elimination. |
648 |
|
* The sign-check is done with bvult instead of bit-extraction. |
649 |
|
*/ |
650 |
|
template <> |
651 |
2043 |
inline bool RewriteRule<SmodEliminateFewerBitwiseOps>::applies(TNode node) |
652 |
|
{ |
653 |
2043 |
return (node.getKind() == kind::BITVECTOR_SMOD); |
654 |
|
} |
655 |
|
|
656 |
|
template <> |
657 |
|
inline Node RewriteRule<SmodEliminateFewerBitwiseOps>::apply(TNode node) |
658 |
|
{ |
659 |
|
Debug("bv-rewrite") << "RewriteRule<SmodEliminate>(" << node << ")" |
660 |
|
<< std::endl; |
661 |
|
NodeManager* nm = NodeManager::currentNM(); |
662 |
|
TNode s = node[0]; |
663 |
|
TNode t = node[1]; |
664 |
|
unsigned size = utils::getSize(s); |
665 |
|
|
666 |
|
/* |
667 |
|
* (bvsmod s t) abbreviates |
668 |
|
* (let ((?msb_s ((_ extract |m-1| |m-1|) s)) |
669 |
|
* (?msb_t ((_ extract |m-1| |m-1|) t))) |
670 |
|
* (let ((abs_s (ite (= ?msb_s #b0) s (bvneg s))) |
671 |
|
* (abs_t (ite (= ?msb_t #b0) t (bvneg t)))) |
672 |
|
* (let ((u (bvurem abs_s abs_t))) |
673 |
|
* (ite (= u (_ bv0 m)) |
674 |
|
* u |
675 |
|
* (ite (and (= ?msb_s #b0) (= ?msb_t #b0)) |
676 |
|
* u |
677 |
|
* (ite (and (= ?msb_s #b1) (= ?msb_t #b0)) |
678 |
|
* (bvadd (bvneg u) t) |
679 |
|
* (ite (and (= ?msb_s #b0) (= ?msb_t #b1)) |
680 |
|
* (bvadd u t) |
681 |
|
* (bvneg u)))))))) |
682 |
|
*/ |
683 |
|
|
684 |
|
Node s_lt_0 = nm->mkNode(kind::BITVECTOR_UGE, s, utils::mkMinSigned(size)); |
685 |
|
Node t_lt_0 = nm->mkNode(kind::BITVECTOR_UGE, t, utils::mkMinSigned(size)); |
686 |
|
Node abs_s = |
687 |
|
nm->mkNode(kind::ITE, s_lt_0, nm->mkNode(kind::BITVECTOR_NEG, s), s); |
688 |
|
Node abs_t = |
689 |
|
nm->mkNode(kind::ITE, t_lt_0, nm->mkNode(kind::BITVECTOR_NEG, t), t); |
690 |
|
|
691 |
|
Node u = nm->mkNode(kind::BITVECTOR_UREM, abs_s, abs_t); |
692 |
|
Node neg_u = nm->mkNode(kind::BITVECTOR_NEG, u); |
693 |
|
|
694 |
|
Node cond0 = u.eqNode(utils::mkConst(size, 0)); |
695 |
|
Node cond1 = |
696 |
|
nm->mkNode(kind::NOT, s_lt_0).andNode(nm->mkNode(kind::NOT, t_lt_0)); |
697 |
|
Node cond2 = s_lt_0.andNode(nm->mkNode(kind::NOT, t_lt_0)); |
698 |
|
Node cond3 = nm->mkNode(kind::NOT, s_lt_0).andNode(t_lt_0); |
699 |
|
|
700 |
|
Node result = cond0.iteNode( |
701 |
|
u, |
702 |
|
cond1.iteNode( |
703 |
|
u, |
704 |
|
cond2.iteNode( |
705 |
|
nm->mkNode(kind::BITVECTOR_ADD, neg_u, t), |
706 |
|
cond3.iteNode(nm->mkNode(kind::BITVECTOR_ADD, u, t), neg_u)))); |
707 |
|
|
708 |
|
return result; |
709 |
|
} |
710 |
|
|
711 |
|
template <> |
712 |
23392 |
inline bool RewriteRule<ZeroExtendEliminate>::applies(TNode node) |
713 |
|
{ |
714 |
23392 |
return (node.getKind() == kind::BITVECTOR_ZERO_EXTEND); |
715 |
|
} |
716 |
|
|
717 |
|
template <> |
718 |
11696 |
inline Node RewriteRule<ZeroExtendEliminate>::apply(TNode node) |
719 |
|
{ |
720 |
11696 |
Debug("bv-rewrite") << "RewriteRule<ZeroExtendEliminate>(" << node << ")" << std::endl; |
721 |
|
|
722 |
23392 |
TNode bv = node[0]; |
723 |
|
unsigned amount = |
724 |
11696 |
node.getOperator().getConst<BitVectorZeroExtend>().d_zeroExtendAmount; |
725 |
11696 |
if (amount == 0) { |
726 |
466 |
return node[0]; |
727 |
|
} |
728 |
22460 |
Node zero = utils::mkConst(amount, 0); |
729 |
22460 |
Node result = utils::mkConcat(zero, node[0]); |
730 |
|
|
731 |
11230 |
return result; |
732 |
|
} |
733 |
|
|
734 |
|
template <> |
735 |
|
inline bool RewriteRule<SignExtendEliminate>::applies(TNode node) |
736 |
|
{ |
737 |
|
return (node.getKind() == kind::BITVECTOR_SIGN_EXTEND); |
738 |
|
} |
739 |
|
|
740 |
|
template <> |
741 |
|
inline Node RewriteRule<SignExtendEliminate>::apply(TNode node) |
742 |
|
{ |
743 |
|
Debug("bv-rewrite") << "RewriteRule<SignExtendEliminate>(" << node << ")" << std::endl; |
744 |
|
|
745 |
|
unsigned amount = |
746 |
|
node.getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount; |
747 |
|
if(amount == 0) { |
748 |
|
return node[0]; |
749 |
|
} |
750 |
|
unsigned size = utils::getSize(node[0]); |
751 |
|
Node sign_bit = utils::mkExtract(node[0], size-1, size-1); |
752 |
|
Node extension = utils::mkConcat(sign_bit, amount); |
753 |
|
|
754 |
|
return utils::mkConcat(extension, node[0]); |
755 |
|
} |
756 |
|
|
757 |
|
template <> |
758 |
|
inline bool RewriteRule<RedorEliminate>::applies(TNode node) |
759 |
|
{ |
760 |
|
return (node.getKind() == kind::BITVECTOR_REDOR); |
761 |
|
} |
762 |
|
|
763 |
|
template <> |
764 |
|
inline Node RewriteRule<RedorEliminate>::apply(TNode node) |
765 |
|
{ |
766 |
|
Debug("bv-rewrite") << "RewriteRule<RedorEliminate>(" << node << ")" << std::endl; |
767 |
|
TNode a = node[0]; |
768 |
|
unsigned size = utils::getSize(node[0]); |
769 |
|
Node result = NodeManager::currentNM()->mkNode(kind::EQUAL, a, utils::mkConst( size, 0 ) ); |
770 |
|
return result.negate(); |
771 |
|
} |
772 |
|
|
773 |
|
template <> |
774 |
|
inline bool RewriteRule<RedandEliminate>::applies(TNode node) |
775 |
|
{ |
776 |
|
return (node.getKind() == kind::BITVECTOR_REDAND); |
777 |
|
} |
778 |
|
|
779 |
|
template <> |
780 |
|
inline Node RewriteRule<RedandEliminate>::apply(TNode node) |
781 |
|
{ |
782 |
|
Debug("bv-rewrite") << "RewriteRule<RedandEliminate>(" << node << ")" << std::endl; |
783 |
|
TNode a = node[0]; |
784 |
|
unsigned size = utils::getSize(node[0]); |
785 |
|
Node result = NodeManager::currentNM()->mkNode(kind::EQUAL, a, utils::mkOnes( size ) ); |
786 |
|
return result; |
787 |
|
} |
788 |
|
|
789 |
|
} |
790 |
|
} |
791 |
|
} // namespace cvc5 |