1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Liana Hadarean, Clark Barrett, 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 "theory/bv/theory_bv_rewrite_rules.h" |
24 |
|
#include "theory/bv/theory_bv_utils.h" |
25 |
|
#include "util/bitvector.h" |
26 |
|
|
27 |
|
namespace cvc5 { |
28 |
|
namespace theory { |
29 |
|
namespace bv { |
30 |
|
|
31 |
|
template<> inline |
32 |
|
bool RewriteRule<EvalAnd>::applies(TNode node) { |
33 |
|
Unreachable(); |
34 |
|
return (node.getKind() == kind::BITVECTOR_AND && |
35 |
|
node.getNumChildren() == 2 && |
36 |
|
utils::isBvConstTerm(node)); |
37 |
|
} |
38 |
|
|
39 |
|
template<> inline |
40 |
|
Node RewriteRule<EvalAnd>::apply(TNode node) { |
41 |
|
Unreachable(); |
42 |
|
Debug("bv-rewrite") << "RewriteRule<EvalAnd>(" << node << ")" << std::endl; |
43 |
|
BitVector a = node[0].getConst<BitVector>(); |
44 |
|
BitVector b = node[1].getConst<BitVector>(); |
45 |
|
BitVector res = a & b; |
46 |
|
|
47 |
|
return utils::mkConst(res); |
48 |
|
} |
49 |
|
|
50 |
|
template<> inline |
51 |
|
bool RewriteRule<EvalOr>::applies(TNode node) { |
52 |
|
Unreachable(); |
53 |
|
return (node.getKind() == kind::BITVECTOR_OR && |
54 |
|
node.getNumChildren() == 2 && |
55 |
|
utils::isBvConstTerm(node)); |
56 |
|
} |
57 |
|
|
58 |
|
template<> inline |
59 |
|
Node RewriteRule<EvalOr>::apply(TNode node) { |
60 |
|
Unreachable(); |
61 |
|
Debug("bv-rewrite") << "RewriteRule<EvalOr>(" << node << ")" << std::endl; |
62 |
|
BitVector a = node[0].getConst<BitVector>(); |
63 |
|
BitVector b = node[1].getConst<BitVector>(); |
64 |
|
BitVector res = a | b; |
65 |
|
|
66 |
|
return utils::mkConst(res); |
67 |
|
} |
68 |
|
|
69 |
|
template<> inline |
70 |
|
bool RewriteRule<EvalXor>::applies(TNode node) { |
71 |
|
Unreachable(); |
72 |
|
return (node.getKind() == kind::BITVECTOR_XOR && |
73 |
|
node.getNumChildren() == 2 && |
74 |
|
utils::isBvConstTerm(node)); |
75 |
|
} |
76 |
|
|
77 |
|
template<> inline |
78 |
|
Node RewriteRule<EvalXor>::apply(TNode node) { |
79 |
|
Unreachable(); |
80 |
|
Debug("bv-rewrite") << "RewriteRule<EvalXor>(" << node << ")" << std::endl; |
81 |
|
BitVector a = node[0].getConst<BitVector>(); |
82 |
|
BitVector b = node[1].getConst<BitVector>(); |
83 |
|
BitVector res = a ^ b; |
84 |
|
|
85 |
|
return utils::mkConst(res); |
86 |
|
} |
87 |
|
|
88 |
|
// template<> inline |
89 |
|
// bool RewriteRule<EvalXnor>::applies(TNode node) { |
90 |
|
// return (node.getKind() == kind::BITVECTOR_XNOR && |
91 |
|
// utils::isBvConstTerm(node)); |
92 |
|
// } |
93 |
|
|
94 |
|
// template<> inline |
95 |
|
// Node RewriteRule<EvalXnor>::apply(TNode node) { |
96 |
|
// Debug("bv-rewrite") << "RewriteRule<EvalXnor>(" << node << ")" << std::endl; |
97 |
|
// BitVector a = node[0].getConst<BitVector>(); |
98 |
|
// BitVector b = node[1].getConst<BitVector>(); |
99 |
|
// BitVector res = ~ (a ^ b); |
100 |
|
|
101 |
|
// return utils::mkConst(res); |
102 |
|
// } |
103 |
|
template<> inline |
104 |
110389 |
bool RewriteRule<EvalNot>::applies(TNode node) { |
105 |
331167 |
return (node.getKind() == kind::BITVECTOR_NOT && |
106 |
331167 |
utils::isBvConstTerm(node)); |
107 |
|
} |
108 |
|
|
109 |
|
template<> inline |
110 |
18874 |
Node RewriteRule<EvalNot>::apply(TNode node) { |
111 |
18874 |
Debug("bv-rewrite") << "RewriteRule<EvalNot>(" << node << ")" << std::endl; |
112 |
37748 |
BitVector a = node[0].getConst<BitVector>(); |
113 |
37748 |
BitVector res = ~ a; |
114 |
37748 |
return utils::mkConst(res); |
115 |
|
} |
116 |
|
|
117 |
|
// template<> inline |
118 |
|
// bool RewriteRule<EvalComp>::applies(TNode node) { |
119 |
|
// return (node.getKind() == kind::BITVECTOR_COMP && |
120 |
|
// utils::isBvConstTerm(node)); |
121 |
|
// } |
122 |
|
|
123 |
|
// template<> inline |
124 |
|
// Node RewriteRule<EvalComp>::apply(TNode node) { |
125 |
|
// Debug("bv-rewrite") << "RewriteRule<EvalComp>(" << node << ")" << std::endl; |
126 |
|
// BitVector a = node[0].getConst<BitVector>(); |
127 |
|
// BitVector b = node[1].getConst<BitVector>(); |
128 |
|
// BitVector res; |
129 |
|
// if (a == b) { |
130 |
|
// res = BitVector(1, Integer(1)); |
131 |
|
// } else { |
132 |
|
// res = BitVector(1, Integer(0)); |
133 |
|
// } |
134 |
|
|
135 |
|
// return utils::mkConst(res); |
136 |
|
// } |
137 |
|
|
138 |
|
template<> inline |
139 |
|
bool RewriteRule<EvalMult>::applies(TNode node) { |
140 |
|
return (node.getKind() == kind::BITVECTOR_MULT && |
141 |
|
utils::isBvConstTerm(node)); |
142 |
|
} |
143 |
|
|
144 |
|
template<> inline |
145 |
|
Node RewriteRule<EvalMult>::apply(TNode node) { |
146 |
|
Debug("bv-rewrite") << "RewriteRule<EvalMult>(" << node << ")" << std::endl; |
147 |
|
TNode::iterator child_it = node.begin(); |
148 |
|
BitVector res = (*child_it).getConst<BitVector>(); |
149 |
|
for(++child_it; child_it != node.end(); ++child_it) { |
150 |
|
res = res * (*child_it).getConst<BitVector>(); |
151 |
|
} |
152 |
|
return utils::mkConst(res); |
153 |
|
} |
154 |
|
|
155 |
|
template <> |
156 |
|
inline bool RewriteRule<EvalAdd>::applies(TNode node) |
157 |
|
{ |
158 |
|
return (node.getKind() == kind::BITVECTOR_ADD && utils::isBvConstTerm(node)); |
159 |
|
} |
160 |
|
|
161 |
|
template <> |
162 |
|
inline Node RewriteRule<EvalAdd>::apply(TNode node) |
163 |
|
{ |
164 |
|
Debug("bv-rewrite") << "RewriteRule<EvalAdd>(" << node << ")" << std::endl; |
165 |
|
TNode::iterator child_it = node.begin(); |
166 |
|
BitVector res = (*child_it).getConst<BitVector>(); |
167 |
|
for(++child_it; child_it != node.end(); ++child_it) { |
168 |
|
res = res + (*child_it).getConst<BitVector>(); |
169 |
|
} |
170 |
|
return utils::mkConst(res); |
171 |
|
} |
172 |
|
|
173 |
|
// template<> inline |
174 |
|
// bool RewriteRule<EvalSub>::applies(TNode node) { |
175 |
|
// return (node.getKind() == kind::BITVECTOR_SUB && |
176 |
|
// utils::isBvConstTerm(node)); |
177 |
|
// } |
178 |
|
|
179 |
|
// template<> inline |
180 |
|
// Node RewriteRule<EvalSub>::apply(TNode node) { |
181 |
|
// Debug("bv-rewrite") << "RewriteRule<EvalSub>(" << node << ")" << std::endl; |
182 |
|
// BitVector a = node[0].getConst<BitVector>(); |
183 |
|
// BitVector b = node[1].getConst<BitVector>(); |
184 |
|
// BitVector res = a - b; |
185 |
|
|
186 |
|
// return utils::mkConst(res); |
187 |
|
// } |
188 |
|
template<> inline |
189 |
39823 |
bool RewriteRule<EvalNeg>::applies(TNode node) { |
190 |
119469 |
return (node.getKind() == kind::BITVECTOR_NEG && |
191 |
119469 |
utils::isBvConstTerm(node)); |
192 |
|
} |
193 |
|
|
194 |
|
template<> inline |
195 |
7253 |
Node RewriteRule<EvalNeg>::apply(TNode node) { |
196 |
7253 |
Debug("bv-rewrite") << "RewriteRule<EvalNeg>(" << node << ")" << std::endl; |
197 |
14506 |
BitVector a = node[0].getConst<BitVector>(); |
198 |
14506 |
BitVector res = - a; |
199 |
|
|
200 |
14506 |
return utils::mkConst(res); |
201 |
|
} |
202 |
|
template<> inline |
203 |
28340 |
bool RewriteRule<EvalUdiv>::applies(TNode node) { |
204 |
28340 |
return utils::isBvConstTerm(node) && node.getKind() == kind::BITVECTOR_UDIV; |
205 |
|
} |
206 |
|
|
207 |
|
template<> inline |
208 |
5887 |
Node RewriteRule<EvalUdiv>::apply(TNode node) { |
209 |
5887 |
Debug("bv-rewrite") << "RewriteRule<EvalUdiv>(" << node << ")" << std::endl; |
210 |
11774 |
BitVector a = node[0].getConst<BitVector>(); |
211 |
11774 |
BitVector b = node[1].getConst<BitVector>(); |
212 |
11774 |
BitVector res = a.unsignedDivTotal(b); |
213 |
|
|
214 |
11774 |
return utils::mkConst(res); |
215 |
|
} |
216 |
|
template<> inline |
217 |
28871 |
bool RewriteRule<EvalUrem>::applies(TNode node) { |
218 |
28871 |
return utils::isBvConstTerm(node) && node.getKind() == kind::BITVECTOR_UREM; |
219 |
|
} |
220 |
|
|
221 |
|
template<> inline |
222 |
6333 |
Node RewriteRule<EvalUrem>::apply(TNode node) { |
223 |
6333 |
Debug("bv-rewrite") << "RewriteRule<EvalUrem>(" << node << ")" << std::endl; |
224 |
12666 |
BitVector a = node[0].getConst<BitVector>(); |
225 |
12666 |
BitVector b = node[1].getConst<BitVector>(); |
226 |
12666 |
BitVector res = a.unsignedRemTotal(b); |
227 |
12666 |
return utils::mkConst(res); |
228 |
|
} |
229 |
|
|
230 |
|
template<> inline |
231 |
8532 |
bool RewriteRule<EvalShl>::applies(TNode node) { |
232 |
25596 |
return (node.getKind() == kind::BITVECTOR_SHL && |
233 |
25596 |
utils::isBvConstTerm(node)); |
234 |
|
} |
235 |
|
|
236 |
|
template<> inline |
237 |
|
Node RewriteRule<EvalShl>::apply(TNode node) { |
238 |
|
Debug("bv-rewrite") << "RewriteRule<EvalShl>(" << node << ")" << std::endl; |
239 |
|
BitVector a = node[0].getConst<BitVector>(); |
240 |
|
BitVector b = node[1].getConst<BitVector>(); |
241 |
|
|
242 |
|
BitVector res = a.leftShift(b); |
243 |
|
return utils::mkConst(res); |
244 |
|
} |
245 |
|
|
246 |
|
template<> inline |
247 |
11539 |
bool RewriteRule<EvalLshr>::applies(TNode node) { |
248 |
34617 |
return (node.getKind() == kind::BITVECTOR_LSHR && |
249 |
34617 |
utils::isBvConstTerm(node)); |
250 |
|
} |
251 |
|
|
252 |
|
template<> inline |
253 |
|
Node RewriteRule<EvalLshr>::apply(TNode node) { |
254 |
|
Debug("bv-rewrite") << "RewriteRule<EvalLshr>(" << node << ")" << std::endl; |
255 |
|
BitVector a = node[0].getConst<BitVector>(); |
256 |
|
BitVector b = node[1].getConst<BitVector>(); |
257 |
|
|
258 |
|
BitVector res = a.logicalRightShift(b); |
259 |
|
return utils::mkConst(res); |
260 |
|
} |
261 |
|
|
262 |
|
template<> inline |
263 |
5434 |
bool RewriteRule<EvalAshr>::applies(TNode node) { |
264 |
16302 |
return (node.getKind() == kind::BITVECTOR_ASHR && |
265 |
16302 |
utils::isBvConstTerm(node)); |
266 |
|
} |
267 |
|
|
268 |
|
template<> inline |
269 |
|
Node RewriteRule<EvalAshr>::apply(TNode node) { |
270 |
|
Debug("bv-rewrite") << "RewriteRule<EvalAshr>(" << node << ")" << std::endl; |
271 |
|
BitVector a = node[0].getConst<BitVector>(); |
272 |
|
BitVector b = node[1].getConst<BitVector>(); |
273 |
|
|
274 |
|
BitVector res = a.arithRightShift(b); |
275 |
|
return utils::mkConst(res); |
276 |
|
} |
277 |
|
|
278 |
|
template<> inline |
279 |
96865 |
bool RewriteRule<EvalUlt>::applies(TNode node) { |
280 |
290595 |
return (node.getKind() == kind::BITVECTOR_ULT && |
281 |
290595 |
utils::isBvConstTerm(node)); |
282 |
|
} |
283 |
|
|
284 |
|
template<> inline |
285 |
1304 |
Node RewriteRule<EvalUlt>::apply(TNode node) { |
286 |
1304 |
Debug("bv-rewrite") << "RewriteRule<EvalUlt>(" << node << ")" << std::endl; |
287 |
2608 |
BitVector a = node[0].getConst<BitVector>(); |
288 |
2608 |
BitVector b = node[1].getConst<BitVector>(); |
289 |
|
|
290 |
1304 |
if (a.unsignedLessThan(b)) { |
291 |
586 |
return utils::mkTrue(); |
292 |
|
} |
293 |
718 |
return utils::mkFalse(); |
294 |
|
} |
295 |
|
|
296 |
|
template<> inline |
297 |
3626 |
bool RewriteRule<EvalUltBv>::applies(TNode node) { |
298 |
10878 |
return (node.getKind() == kind::BITVECTOR_ULTBV && |
299 |
10878 |
utils::isBvConstTerm(node)); |
300 |
|
} |
301 |
|
|
302 |
|
template<> inline |
303 |
76 |
Node RewriteRule<EvalUltBv>::apply(TNode node) { |
304 |
76 |
Debug("bv-rewrite") << "RewriteRule<EvalUltBv>(" << node << ")" << std::endl; |
305 |
152 |
BitVector a = node[0].getConst<BitVector>(); |
306 |
152 |
BitVector b = node[1].getConst<BitVector>(); |
307 |
|
|
308 |
76 |
if (a.unsignedLessThan(b)) { |
309 |
20 |
return utils::mkConst(1,1); |
310 |
|
} |
311 |
56 |
return utils::mkConst(1, 0); |
312 |
|
} |
313 |
|
|
314 |
|
template<> inline |
315 |
104296 |
bool RewriteRule<EvalSlt>::applies(TNode node) { |
316 |
312888 |
return (node.getKind() == kind::BITVECTOR_SLT && |
317 |
312888 |
utils::isBvConstTerm(node)); |
318 |
|
} |
319 |
|
|
320 |
|
template<> inline |
321 |
1256 |
Node RewriteRule<EvalSlt>::apply(TNode node) { |
322 |
1256 |
Debug("bv-rewrite") << "RewriteRule<EvalSlt>(" << node << ")" << std::endl; |
323 |
2512 |
BitVector a = node[0].getConst<BitVector>(); |
324 |
2512 |
BitVector b = node[1].getConst<BitVector>(); |
325 |
|
|
326 |
1256 |
if (a.signedLessThan(b)) { |
327 |
512 |
return utils::mkTrue(); |
328 |
|
} |
329 |
744 |
return utils::mkFalse(); |
330 |
|
|
331 |
|
} |
332 |
|
|
333 |
|
template<> inline |
334 |
7198 |
bool RewriteRule<EvalSltBv>::applies(TNode node) { |
335 |
21594 |
return (node.getKind() == kind::BITVECTOR_SLTBV && |
336 |
21594 |
utils::isBvConstTerm(node)); |
337 |
|
} |
338 |
|
|
339 |
|
template<> inline |
340 |
354 |
Node RewriteRule<EvalSltBv>::apply(TNode node) { |
341 |
354 |
Debug("bv-rewrite") << "RewriteRule<EvalSltBv>(" << node << ")" << std::endl; |
342 |
708 |
BitVector a = node[0].getConst<BitVector>(); |
343 |
708 |
BitVector b = node[1].getConst<BitVector>(); |
344 |
|
|
345 |
354 |
if (a.signedLessThan(b)) { |
346 |
176 |
return utils::mkConst(1, 1); |
347 |
|
} |
348 |
178 |
return utils::mkConst(1, 0); |
349 |
|
|
350 |
|
} |
351 |
|
|
352 |
|
template<> inline |
353 |
27300 |
bool RewriteRule<EvalITEBv>::applies(TNode node) { |
354 |
27300 |
Debug("bv-rewrite") << "RewriteRule<EvalITEBv>::applies(" << node << ")" << std::endl; |
355 |
81900 |
return (node.getKind() == kind::BITVECTOR_ITE && |
356 |
81900 |
utils::isBvConstTerm(node)); |
357 |
|
} |
358 |
|
|
359 |
|
template<> inline |
360 |
1113 |
Node RewriteRule<EvalITEBv>::apply(TNode node) { |
361 |
1113 |
Debug("bv-rewrite") << "RewriteRule<EvalITEBv>(" << node << ")" << std::endl; |
362 |
2226 |
BitVector cond = node[0].getConst<BitVector>(); |
363 |
|
|
364 |
1113 |
if (node[0] == utils::mkConst(1, 1)) { |
365 |
476 |
return node[1]; |
366 |
|
} else { |
367 |
637 |
Assert(node[0] == utils::mkConst(1, 0)); |
368 |
637 |
return node[2]; |
369 |
|
} |
370 |
|
} |
371 |
|
|
372 |
|
template<> inline |
373 |
6454 |
bool RewriteRule<EvalUle>::applies(TNode node) { |
374 |
19362 |
return (node.getKind() == kind::BITVECTOR_ULE && |
375 |
19362 |
utils::isBvConstTerm(node)); |
376 |
|
} |
377 |
|
|
378 |
|
template<> inline |
379 |
26 |
Node RewriteRule<EvalUle>::apply(TNode node) { |
380 |
26 |
Debug("bv-rewrite") << "RewriteRule<EvalUle>(" << node << ")" << std::endl; |
381 |
52 |
BitVector a = node[0].getConst<BitVector>(); |
382 |
52 |
BitVector b = node[1].getConst<BitVector>(); |
383 |
|
|
384 |
26 |
if (a.unsignedLessThanEq(b)) { |
385 |
20 |
return utils::mkTrue(); |
386 |
|
} |
387 |
6 |
return utils::mkFalse(); |
388 |
|
} |
389 |
|
|
390 |
|
template<> inline |
391 |
6825 |
bool RewriteRule<EvalSle>::applies(TNode node) { |
392 |
20475 |
return (node.getKind() == kind::BITVECTOR_SLE && |
393 |
20475 |
utils::isBvConstTerm(node)); |
394 |
|
} |
395 |
|
|
396 |
|
template<> inline |
397 |
25 |
Node RewriteRule<EvalSle>::apply(TNode node) { |
398 |
25 |
Debug("bv-rewrite") << "RewriteRule<EvalSle>(" << node << ")" << std::endl; |
399 |
50 |
BitVector a = node[0].getConst<BitVector>(); |
400 |
50 |
BitVector b = node[1].getConst<BitVector>(); |
401 |
|
|
402 |
25 |
if (a.signedLessThanEq(b)) { |
403 |
25 |
return utils::mkTrue(); |
404 |
|
} |
405 |
|
return utils::mkFalse(); |
406 |
|
} |
407 |
|
|
408 |
|
template<> inline |
409 |
|
bool RewriteRule<EvalExtract>::applies(TNode node) { |
410 |
|
return (node.getKind() == kind::BITVECTOR_EXTRACT && |
411 |
|
utils::isBvConstTerm(node)); |
412 |
|
} |
413 |
|
|
414 |
|
template<> inline |
415 |
|
Node RewriteRule<EvalExtract>::apply(TNode node) { |
416 |
|
Debug("bv-rewrite") << "RewriteRule<EvalExtract>(" << node << ")" << std::endl; |
417 |
|
BitVector a = node[0].getConst<BitVector>(); |
418 |
|
unsigned lo = utils::getExtractLow(node); |
419 |
|
unsigned hi = utils::getExtractHigh(node); |
420 |
|
|
421 |
|
BitVector res = a.extract(hi, lo); |
422 |
|
return utils::mkConst(res); |
423 |
|
} |
424 |
|
|
425 |
|
|
426 |
|
template<> inline |
427 |
|
bool RewriteRule<EvalConcat>::applies(TNode node) { |
428 |
|
return (node.getKind() == kind::BITVECTOR_CONCAT && |
429 |
|
utils::isBvConstTerm(node)); |
430 |
|
} |
431 |
|
|
432 |
|
template<> inline |
433 |
|
Node RewriteRule<EvalConcat>::apply(TNode node) { |
434 |
|
Debug("bv-rewrite") << "RewriteRule<EvalConcat>(" << node << ")" << std::endl; |
435 |
|
unsigned num = node.getNumChildren(); |
436 |
|
BitVector res = node[0].getConst<BitVector>(); |
437 |
|
for(unsigned i = 1; i < num; ++i ) { |
438 |
|
BitVector a = node[i].getConst<BitVector>(); |
439 |
|
res = res.concat(a); |
440 |
|
} |
441 |
|
return utils::mkConst(res); |
442 |
|
} |
443 |
|
|
444 |
|
template<> inline |
445 |
56502 |
bool RewriteRule<EvalSignExtend>::applies(TNode node) { |
446 |
169274 |
return (node.getKind() == kind::BITVECTOR_SIGN_EXTEND && |
447 |
169274 |
utils::isBvConstTerm(node)); |
448 |
|
} |
449 |
|
|
450 |
|
template<> inline |
451 |
1650 |
Node RewriteRule<EvalSignExtend>::apply(TNode node) { |
452 |
1650 |
Debug("bv-rewrite") << "RewriteRule<EvalSignExtend>(" << node << ")" << std::endl; |
453 |
3300 |
BitVector a = node[0].getConst<BitVector>(); |
454 |
|
unsigned amount = |
455 |
1650 |
node.getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount; |
456 |
3300 |
BitVector res = a.signExtend(amount); |
457 |
|
|
458 |
3300 |
return utils::mkConst(res); |
459 |
|
} |
460 |
|
|
461 |
|
template<> inline |
462 |
|
bool RewriteRule<EvalEquals>::applies(TNode node) { |
463 |
|
return (node.getKind() == kind::EQUAL && |
464 |
|
utils::isBvConstTerm(node)); |
465 |
|
} |
466 |
|
|
467 |
|
template<> inline |
468 |
|
Node RewriteRule<EvalEquals>::apply(TNode node) { |
469 |
|
Debug("bv-rewrite") << "RewriteRule<EvalEquals>(" << node << ")" << std::endl; |
470 |
|
BitVector a = node[0].getConst<BitVector>(); |
471 |
|
BitVector b = node[1].getConst<BitVector>(); |
472 |
|
if (a == b) { |
473 |
|
return utils::mkTrue(); |
474 |
|
} |
475 |
|
return utils::mkFalse(); |
476 |
|
|
477 |
|
} |
478 |
|
|
479 |
|
template<> inline |
480 |
304870 |
bool RewriteRule<EvalComp>::applies(TNode node) { |
481 |
914610 |
return (node.getKind() == kind::BITVECTOR_COMP && |
482 |
914610 |
utils::isBvConstTerm(node)); |
483 |
|
} |
484 |
|
|
485 |
|
template<> inline |
486 |
131342 |
Node RewriteRule<EvalComp>::apply(TNode node) { |
487 |
131342 |
Debug("bv-rewrite") << "RewriteRule<EvalComp>(" << node << ")" << std::endl; |
488 |
262684 |
BitVector a = node[0].getConst<BitVector>(); |
489 |
262684 |
BitVector b = node[1].getConst<BitVector>(); |
490 |
131342 |
if (a == b) { |
491 |
319 |
return utils::mkConst(1, 1); |
492 |
|
} |
493 |
131023 |
return utils::mkConst(1, 0); |
494 |
|
} |
495 |
|
|
496 |
|
template <> |
497 |
503 |
inline bool RewriteRule<EvalEagerAtom>::applies(TNode node) |
498 |
|
{ |
499 |
503 |
return (node.getKind() == kind::BITVECTOR_EAGER_ATOM && node[0].isConst()); |
500 |
|
} |
501 |
|
|
502 |
|
template <> |
503 |
7 |
inline Node RewriteRule<EvalEagerAtom>::apply(TNode node) |
504 |
|
{ |
505 |
7 |
Debug("bv-rewrite") << "RewriteRule<EvalComp>(" << node << ")" << std::endl; |
506 |
7 |
return node[0]; |
507 |
|
} |
508 |
|
} |
509 |
|
} |
510 |
|
} // namespace cvc5 |