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