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