1 /********************************************************************
2 * AUTHORS: Vijay Ganesh, Trevor Hansen
3 *
4 * BEGIN DATE: November, 2005
5 *
6 Permission is hereby granted, free of charge, to any person obtaining a copy
7 of this software and associated documentation files (the "Software"), to deal
8 in the Software without restriction, including without limitation the rights
9 to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
10 copies of the Software, and to permit persons to whom the Software is
11 furnished to do so, subject to the following conditions:
12
13 The above copyright notice and this permission notice shall be included in
14 all copies or substantial portions of the Software.
15
16 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
17 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
18 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
19 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
20 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
21 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
22 THE SOFTWARE.
23 ********************************************************************/
24
25 #include "stp/Simplifier/Simplifier.h"
26 #include <cassert>
27
28 namespace stp
29 {
30
31 // error printing
BVConstEvaluatorError(CONSTANTBV::ErrCode e)32 static void BVConstEvaluatorError(CONSTANTBV::ErrCode e)
33 {
34 std::string ss("BVConstEvaluator:");
35 ss += (const char*)BitVector_Error(e);
36 FatalError(ss.c_str());
37 }
38
39 // Const evaluator logical and arithmetic operations.
NonMemberBVConstEvaluator(STPMgr * _bm,const Kind k,const ASTVec & input_children,unsigned int inputwidth)40 ASTNode NonMemberBVConstEvaluator(STPMgr* _bm, const Kind k,
41 const ASTVec& input_children,
42 unsigned int inputwidth)
43 {
44 ASTNode OutputNode;
45
46 ASTNode& ASTTrue = _bm->ASTTrue;
47 ASTNode& ASTFalse = _bm->ASTFalse;
48
49 unsigned int outputwidth = inputwidth;
50 CBV output = NULL;
51
52 CBV tmp0 = NULL;
53 CBV tmp1 = NULL;
54
55 const size_t number_of_children = input_children.size();
56 assert(number_of_children >= 1);
57 assert(k != BVCONST);
58
59 ASTVec children;
60 children.reserve(number_of_children);
61 for (size_t i = 0; i < number_of_children; i++)
62 {
63 if (input_children[i].isConstant())
64 children.push_back(input_children[i]);
65 else
66 children.push_back(NonMemberBVConstEvaluator(_bm, input_children[i]));
67 }
68
69 if ((number_of_children == 2 || number_of_children == 1) &&
70 input_children[0].GetType() == BITVECTOR_TYPE)
71 {
72 // saving some typing. BVPLUS does not use these variables. if the
73 // input BVPLUS has two nodes, then we want to avoid setting these
74 // variables.
75 if (1 == number_of_children)
76 {
77 tmp0 = children[0].GetBVConst();
78 }
79 else if (2 == number_of_children && k != BVPLUS)
80 {
81 tmp0 = children[0].GetBVConst();
82 tmp1 = children[1].GetBVConst();
83 }
84 }
85
86 switch (k)
87 {
88 case UNDEFINED:
89 case READ:
90 case WRITE:
91 case SYMBOL:
92 FatalError("BVConstEvaluator: term is not a constant-term");
93 break;
94 // case BVCONST:
95 // OutputNode = t;
96 // break;
97 case BOOLEXTRACT:
98 {
99 unsigned int bit = children[1].GetUnsignedConst();
100 if (CONSTANTBV::BitVector_bit_test(tmp0, bit))
101 {
102 OutputNode = ASTTrue;
103 }
104 else
105 {
106 OutputNode = ASTFalse;
107 }
108 break;
109 }
110 case BVNOT:
111 {
112 output = CONSTANTBV::BitVector_Create(inputwidth, true);
113 CONSTANTBV::Set_Complement(output, tmp0);
114 OutputNode = _bm->CreateBVConst(output, outputwidth);
115 break;
116 }
117 case BVSX:
118 case BVZX:
119 {
120 output = CONSTANTBV::BitVector_Create(inputwidth, true);
121 unsigned t0_width = input_children[0].GetValueWidth();
122 if (inputwidth == t0_width)
123 {
124 CONSTANTBV::BitVector_Copy(output, tmp0);
125 OutputNode = _bm->CreateBVConst(output, outputwidth);
126 }
127 else
128 {
129 bool topbit_sign =
130 (k == BVSX) ? (CONSTANTBV::BitVector_Sign(tmp0) < 0) : false;
131
132 if (topbit_sign)
133 {
134 CONSTANTBV::BitVector_Fill(output);
135 }
136 CONSTANTBV::BitVector_Interval_Copy(output, tmp0, 0, 0, t0_width);
137 OutputNode = _bm->CreateBVConst(output, outputwidth);
138 }
139 break;
140 }
141
142 case BVLEFTSHIFT:
143 case BVRIGHTSHIFT:
144 case BVSRSHIFT:
145 {
146 // load in the bitWidth.
147 CBV width = CONSTANTBV::BitVector_Create(inputwidth, true);
148 for (unsigned i = 0; i < sizeof(inputwidth) * 8; i++)
149 if ((inputwidth & (0x1 << i)) != 0)
150 CONSTANTBV::BitVector_Bit_On(width, i);
151
152 output = CONSTANTBV::BitVector_Create(inputwidth, true);
153
154 // Number of bits to shift it.
155 ASTNode shiftNode = children[1];
156
157 bool msb = CONSTANTBV::BitVector_msb_(tmp0);
158
159 // If this shift is greater than the bitWidth, make it zero.
160 if (CONSTANTBV::BitVector_Lexicompare(width, shiftNode.GetBVConst()) < 0)
161 {
162 if (k == BVSRSHIFT && msb)
163 CONSTANTBV::Set_Complement(output, output);
164 }
165 else
166 {
167 // the shift is destructive, get a copy.
168 CONSTANTBV::BitVector_Interval_Copy(output, tmp0, 0, 0, inputwidth);
169
170 unsigned int shift = shiftNode.GetUnsignedConst();
171
172 if (k == BVLEFTSHIFT)
173 CONSTANTBV::BitVector_Move_Left(output, shift);
174 else
175 CONSTANTBV::BitVector_Move_Right(output, shift);
176
177 if (k == BVSRSHIFT && msb)
178 {
179 // signed shift, and the number was originally negative.
180 // Shift may be larger than the inputwidth.
181 for (unsigned int i = 0; i < std::min(shift, inputwidth); i++)
182 {
183 CONSTANTBV::BitVector_Bit_On(output, (inputwidth - 1 - i));
184 }
185 assert(CONSTANTBV::BitVector_Sign(output) == -1); // must be negative.
186 }
187 }
188
189 OutputNode = _bm->CreateBVConst(output, outputwidth);
190
191 CONSTANTBV::BitVector_Destroy(width);
192 break;
193 }
194
195 case BVAND:
196 {
197 assert(1 <= number_of_children);
198
199 output = CONSTANTBV::BitVector_Create(inputwidth, true);
200 CONSTANTBV::BitVector_Fill(output);
201
202 for (ASTVec::iterator it = children.begin(), itend = children.end();
203 it != itend; it++)
204 {
205 CBV kk = (*it).GetBVConst();
206 CONSTANTBV::Set_Intersection(output, output, kk);
207 }
208
209 OutputNode = _bm->CreateBVConst(output, outputwidth);
210 break;
211 }
212 case BVOR:
213 {
214 assert(1 <= number_of_children);
215
216 output = CONSTANTBV::BitVector_Create(inputwidth, true);
217
218 for (ASTVec::iterator it = children.begin(), itend = children.end();
219 it != itend; it++)
220 {
221 CBV kk = (*it).GetBVConst();
222 CONSTANTBV::Set_Union(output, output, kk);
223 }
224
225 OutputNode = _bm->CreateBVConst(output, outputwidth);
226 break;
227 }
228 case BVXOR:
229 {
230 assert(2 == number_of_children);
231 output = CONSTANTBV::BitVector_Create(inputwidth, true);
232 CONSTANTBV::Set_ExclusiveOr(output, tmp0, tmp1);
233 OutputNode = _bm->CreateBVConst(output, outputwidth);
234 break;
235 }
236 case BVSUB:
237 {
238 assert(2 == number_of_children);
239 output = CONSTANTBV::BitVector_Create(inputwidth, true);
240 bool carry = false;
241 CONSTANTBV::BitVector_sub(output, tmp0, tmp1, &carry);
242 OutputNode = _bm->CreateBVConst(output, outputwidth);
243 break;
244 }
245 case BVUMINUS:
246 {
247 output = CONSTANTBV::BitVector_Create(inputwidth, true);
248 CONSTANTBV::BitVector_Negate(output, tmp0);
249 OutputNode = _bm->CreateBVConst(output, outputwidth);
250 break;
251 }
252 case BVEXTRACT:
253 {
254 output = CONSTANTBV::BitVector_Create(inputwidth, true);
255 tmp0 = children[0].GetBVConst();
256 unsigned int hi = children[1].GetUnsignedConst();
257 unsigned int low = children[2].GetUnsignedConst();
258 unsigned int len = hi - low + 1;
259
260 CONSTANTBV::BitVector_Destroy(output);
261 output = CONSTANTBV::BitVector_Create(len, false);
262 CONSTANTBV::BitVector_Interval_Copy(output, tmp0, 0, low, len);
263 outputwidth = len;
264 OutputNode = _bm->CreateBVConst(output, outputwidth);
265 break;
266 }
267
268 case BVCONCAT:
269 {
270 assert(2 == number_of_children);
271 output = CONSTANTBV::BitVector_Create(inputwidth, true);
272 unsigned t0_width = children[0].GetValueWidth();
273 unsigned t1_width = children[1].GetValueWidth();
274 CONSTANTBV::BitVector_Destroy(output);
275
276 output = CONSTANTBV::BitVector_Concat(tmp0, tmp1);
277 outputwidth = t0_width + t1_width;
278 OutputNode = _bm->CreateBVConst(output, outputwidth);
279
280 break;
281 }
282 case BVMULT:
283 {
284 output = CONSTANTBV::BitVector_Create(inputwidth, true);
285 CONSTANTBV::BitVector_increment(output);
286
287 CBV tmp = CONSTANTBV::BitVector_Create(2 * inputwidth, true);
288
289 for (ASTVec::iterator it = children.begin(), itend = children.end();
290 it != itend; it++)
291 {
292 CBV kk = (*it).GetBVConst();
293 CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Multiply(tmp, output, kk);
294
295 if (0 != e)
296 {
297 BVConstEvaluatorError(e);
298 }
299 CONSTANTBV::BitVector_Interval_Copy(output, tmp, 0, 0, inputwidth);
300 }
301
302 OutputNode = _bm->CreateBVConst(output, outputwidth);
303 CONSTANTBV::BitVector_Destroy(tmp);
304 break;
305 }
306 case BVPLUS:
307 {
308 output = CONSTANTBV::BitVector_Create(inputwidth, true);
309 bool carry = false;
310 for (ASTVec::iterator it = children.begin(), itend = children.end();
311 it != itend; it++)
312 {
313 CBV kk = (*it).GetBVConst();
314 CONSTANTBV::BitVector_add(output, output, kk, &carry);
315 carry = false;
316 }
317 OutputNode = _bm->CreateBVConst(output, outputwidth);
318 break;
319 }
320
321 // SBVREM : Result of rounding the quotient towards
322 // zero. i.e. (-10)/3, has a remainder of -1
323 //
324 // SBVMOD : Result of rounding the quotient towards
325 // -infinity. i.e. (-10)/3, has a modulus of 2. EXCEPT THAT
326 // if it divides exactly and the signs are different, then
327 // it's equal to the dividend.
328 case SBVDIV:
329 case SBVREM:
330 {
331 assert(2 == number_of_children);
332 CBV quotient = CONSTANTBV::BitVector_Create(inputwidth, true);
333 CBV remainder = CONSTANTBV::BitVector_Create(inputwidth, true);
334
335 if (CONSTANTBV::BitVector_is_empty(tmp1))
336 {
337 // Expecting a division by zero. Just return one.
338 if (k == SBVREM)
339 OutputNode = children[0];
340 else
341 {
342 if (CONSTANTBV::BitVector_bit_test(tmp0, inputwidth - 1))
343 OutputNode = _bm->CreateOneConst(inputwidth);
344 else
345 OutputNode = _bm->CreateMaxConst(inputwidth);
346 }
347
348 CONSTANTBV::BitVector_Destroy(remainder);
349 CONSTANTBV::BitVector_Destroy(quotient);
350 }
351 else
352 {
353 CONSTANTBV::ErrCode e =
354 CONSTANTBV::BitVector_Divide(quotient, tmp0, tmp1, remainder);
355
356 if (e != 0)
357 {
358 std::cerr << "WARNING" << std::endl;
359 FatalError((const char*)CONSTANTBV::BitVector_Error(e));
360 }
361
362 if (SBVDIV == k)
363 {
364 OutputNode = _bm->CreateBVConst(quotient, outputwidth);
365 CONSTANTBV::BitVector_Destroy(remainder);
366 }
367 else
368 {
369 OutputNode = _bm->CreateBVConst(remainder, outputwidth);
370 CONSTANTBV::BitVector_Destroy(quotient);
371 }
372 }
373 break;
374 }
375
376 case SBVMOD:
377 {
378 assert(2 == number_of_children);
379 /*
380 (bvsmod s t) abbreviates
381 (let ((?msb_s ((_ extract |m-1| |m-1|) s))
382 (?msb_t ((_ extract |m-1| |m-1|) t)))
383 (let ((abs_s (ite (= ?msb_s #b0) s (bvneg s)))
384 (abs_t (ite (= ?msb_t #b0) t (bvneg t))))
385 (let ((u (bvurem abs_s abs_t)))
386 (ite (= u (_ bv0 m))
387 u
388 (ite (and (= ?msb_s #b0) (= ?msb_t #b0))
389 u
390 (ite (and (= ?msb_s #b1) (= ?msb_t #b0))
391 (bvadd (bvneg u) t)
392 (ite (and (= ?msb_s #b0) (= ?msb_t #b1))
393 (bvadd u t)
394 (bvneg u))))))))
395 */
396
397 assert(input_children[0].GetValueWidth() ==
398 input_children[1].GetValueWidth());
399
400 bool isNegativeS = CONSTANTBV::BitVector_msb_(tmp0);
401 bool isNegativeT = CONSTANTBV::BitVector_msb_(tmp1);
402
403 CBV quotient = CONSTANTBV::BitVector_Create(inputwidth, true);
404 CBV remainder = CONSTANTBV::BitVector_Create(inputwidth, true);
405 tmp0 = CONSTANTBV::BitVector_Clone(tmp0);
406 tmp1 = CONSTANTBV::BitVector_Clone(tmp1);
407
408 if (CONSTANTBV::BitVector_is_empty(tmp1))
409 {
410 OutputNode = children[0];
411 CONSTANTBV::BitVector_Destroy(remainder);
412 }
413 else
414 {
415 if (!isNegativeS && !isNegativeT)
416 {
417 // Signs are both positive
418 CONSTANTBV::ErrCode e =
419 CONSTANTBV::BitVector_Div_Pos(quotient, tmp0, tmp1, remainder);
420 if (e != CONSTANTBV::ErrCode_Ok)
421 {
422 std::cerr << "Error code was:" << e << std::endl;
423 assert(e == CONSTANTBV::ErrCode_Ok);
424 }
425 OutputNode = _bm->CreateBVConst(remainder, outputwidth);
426 }
427 else if (isNegativeS && !isNegativeT)
428 {
429 // S negative, T positive.
430 CBV tmp0b = CONSTANTBV::BitVector_Create(inputwidth, true);
431 CONSTANTBV::BitVector_Negate(tmp0b, tmp0);
432
433 CONSTANTBV::ErrCode e =
434 CONSTANTBV::BitVector_Div_Pos(quotient, tmp0b, tmp1, remainder);
435 assert(e == CONSTANTBV::ErrCode_Ok);
436
437 CBV remb = CONSTANTBV::BitVector_Create(inputwidth, true);
438 CONSTANTBV::BitVector_Negate(remb, remainder);
439
440 if (CONSTANTBV::BitVector_is_empty(remb))
441 {
442 OutputNode = _bm->CreateZeroConst(outputwidth);
443 }
444 else
445 {
446 CBV res = CONSTANTBV::BitVector_Create(inputwidth, true);
447 bool carry = false;
448 CONSTANTBV::BitVector_add(res, remb, tmp1, &carry);
449 OutputNode = _bm->CreateBVConst(res, outputwidth);
450 }
451
452 CONSTANTBV::BitVector_Destroy(remb);
453 CONSTANTBV::BitVector_Destroy(tmp0b);
454 CONSTANTBV::BitVector_Destroy(remainder);
455 }
456 else if (!isNegativeS && isNegativeT)
457 {
458 // If s is positive and t is negative
459 CBV tmp1b = CONSTANTBV::BitVector_Create(inputwidth, true);
460 CONSTANTBV::BitVector_Negate(tmp1b, tmp1);
461
462 CONSTANTBV::ErrCode e =
463 CONSTANTBV::BitVector_Div_Pos(quotient, tmp0, tmp1b, remainder);
464
465 assert(e == CONSTANTBV::ErrCode_Ok);
466
467 if (CONSTANTBV::BitVector_is_empty(remainder))
468 {
469 OutputNode = _bm->CreateZeroConst(outputwidth);
470 }
471 else
472 {
473 CBV res = CONSTANTBV::BitVector_Create(inputwidth, true);
474 bool carry = false;
475 CONSTANTBV::BitVector_add(res, remainder, tmp1, &carry);
476 OutputNode = _bm->CreateBVConst(res, outputwidth);
477 }
478
479 CONSTANTBV::BitVector_Destroy(tmp1b);
480 CONSTANTBV::BitVector_Destroy(remainder);
481 }
482 else if (isNegativeS && isNegativeT)
483 {
484 // Signs are both negative
485 CBV tmp0b = CONSTANTBV::BitVector_Create(inputwidth, true);
486 CBV tmp1b = CONSTANTBV::BitVector_Create(inputwidth, true);
487 CONSTANTBV::BitVector_Negate(tmp0b, tmp0);
488 CONSTANTBV::BitVector_Negate(tmp1b, tmp1);
489
490 CONSTANTBV::ErrCode e =
491 CONSTANTBV::BitVector_Div_Pos(quotient, tmp0b, tmp1b, remainder);
492 assert(e == CONSTANTBV::ErrCode_Ok);
493
494 CBV remb = CONSTANTBV::BitVector_Create(inputwidth, true);
495 CONSTANTBV::BitVector_Negate(remb, remainder);
496
497 OutputNode = _bm->CreateBVConst(remb, outputwidth);
498 CONSTANTBV::BitVector_Destroy(tmp0b);
499 CONSTANTBV::BitVector_Destroy(tmp1b);
500 CONSTANTBV::BitVector_Destroy(remainder);
501 }
502 else
503 {
504 FatalError("never get called");
505 }
506 }
507
508 CONSTANTBV::BitVector_Destroy(tmp0);
509 CONSTANTBV::BitVector_Destroy(tmp1);
510 CONSTANTBV::BitVector_Destroy(quotient);
511 }
512 break;
513
514 case BVDIV:
515 case BVMOD:
516 {
517 assert(2 == number_of_children);
518
519 if (CONSTANTBV::BitVector_is_empty(tmp1))
520 {
521 // a = bq + r, where b!=0 implies r < b. q is quotient, r remainder.
522 // i.e. a/b = q.
523 // It doesn't matter what q is when b=0, but r needs to be a.
524 if (k == BVMOD)
525 OutputNode = children[0];
526 else
527 OutputNode = _bm->CreateMaxConst(outputwidth);
528 // Expecting a division by zero. Just return one.
529 }
530 else
531 {
532 CBV quotient = CONSTANTBV::BitVector_Create(inputwidth, true);
533 CBV remainder = CONSTANTBV::BitVector_Create(inputwidth, true);
534
535 // tmp0 is dividend, tmp1 is the divisor All parameters
536 // to BitVector_Div_Pos must be distinct unlike
537 // BitVector_Divide FIXME the contents of the second
538 // parameter to Div_Pos is destroyed As tmp0 is currently
539 // the same as the copy belonging to an ASTNode input_children[0] this
540 // must be copied.
541 tmp0 = CONSTANTBV::BitVector_Clone(tmp0);
542 CONSTANTBV::ErrCode e =
543 CONSTANTBV::BitVector_Div_Pos(quotient, tmp0, tmp1, remainder);
544 CONSTANTBV::BitVector_Destroy(tmp0);
545
546 if (0 != e)
547 {
548 CONSTANTBV::BitVector_Destroy(quotient);
549 CONSTANTBV::BitVector_Destroy(remainder);
550 // error printing
551 if (_bm->counterexample_checking_during_refinement)
552 {
553 output = CONSTANTBV::BitVector_Create(inputwidth, true);
554 OutputNode = _bm->CreateBVConst(output, outputwidth);
555 // CONSTANTBV::BitVector_Destroy(output);
556 break;
557 }
558 else
559 {
560 BVConstEvaluatorError(e);
561 }
562 }
563
564 // FIXME Not very standard in the current scheme
565 if (BVDIV == k)
566 {
567 OutputNode = _bm->CreateBVConst(quotient, outputwidth);
568 CONSTANTBV::BitVector_Destroy(remainder);
569 }
570 else
571 {
572 OutputNode = _bm->CreateBVConst(remainder, outputwidth);
573 CONSTANTBV::BitVector_Destroy(quotient);
574 }
575 }
576 break;
577 }
578 case ITE:
579 {
580 if (ASTTrue == input_children[0])
581 OutputNode = children[1];
582 else if (ASTFalse == input_children[0])
583 OutputNode = children[2];
584 else
585 {
586 std::cerr << tmp0;
587 FatalError(
588 "BVConstEvaluator: ITE condiional must be either TRUE or FALSE:");
589 }
590 }
591 break;
592 case EQ:
593 assert(2 == number_of_children);
594 if (CONSTANTBV::BitVector_equal(tmp0, tmp1))
595 OutputNode = ASTTrue;
596 else
597 OutputNode = ASTFalse;
598 break;
599
600 case BVLT:
601 assert(2 == number_of_children);
602 if (-1 == CONSTANTBV::BitVector_Lexicompare(tmp0, tmp1))
603 OutputNode = ASTTrue;
604 else
605 OutputNode = ASTFalse;
606 break;
607
608 case BVLE:
609 {
610 assert(2 == number_of_children);
611 int comp = CONSTANTBV::BitVector_Lexicompare(tmp0, tmp1);
612 if (comp <= 0)
613 OutputNode = ASTTrue;
614 else
615 OutputNode = ASTFalse;
616 break;
617 }
618
619 case BVGT:
620 assert(2 == number_of_children);
621 if (1 == CONSTANTBV::BitVector_Lexicompare(tmp0, tmp1))
622 OutputNode = ASTTrue;
623 else
624 OutputNode = ASTFalse;
625 break;
626
627 case BVGE:
628 {
629 assert(2 == number_of_children);
630 const int comp = CONSTANTBV::BitVector_Lexicompare(tmp0, tmp1);
631 if (comp >= 0)
632 OutputNode = ASTTrue;
633 else
634 OutputNode = ASTFalse;
635 break;
636 }
637
638 case BVSLT:
639 assert(2 == number_of_children);
640 if (-1 == CONSTANTBV::BitVector_Compare(tmp0, tmp1))
641 OutputNode = ASTTrue;
642 else
643 OutputNode = ASTFalse;
644 break;
645 case BVSLE:
646 {
647 assert(2 == number_of_children);
648 signed int comp = CONSTANTBV::BitVector_Compare(tmp0, tmp1);
649 if (comp <= 0)
650 OutputNode = ASTTrue;
651 else
652 OutputNode = ASTFalse;
653 break;
654 }
655 case BVSGT:
656 assert(2 == number_of_children);
657 if (1 == CONSTANTBV::BitVector_Compare(tmp0, tmp1))
658 OutputNode = ASTTrue;
659 else
660 OutputNode = ASTFalse;
661 break;
662 case BVSGE:
663 {
664 assert(2 == number_of_children);
665 int comp = CONSTANTBV::BitVector_Compare(tmp0, tmp1);
666 if (comp >= 0)
667 OutputNode = ASTTrue;
668 else
669 OutputNode = ASTFalse;
670 break;
671 }
672
673 case TRUE:
674 OutputNode = ASTTrue;
675 break;
676 case FALSE:
677 OutputNode = ASTFalse;
678 break;
679 case NOT:
680 if (ASTTrue == input_children[0])
681 return ASTFalse;
682 else if (ASTFalse == input_children[0])
683 return ASTTrue;
684 else
685 {
686 std::cerr << ASTFalse;
687 std::cerr << input_children[0];
688 FatalError("BVConstEvaluator: unexpected not input");
689 }
690
691 case OR:
692 OutputNode = ASTFalse;
693 for (ASTVec::const_iterator it = children.begin(), itend = children.end();
694 it != itend; it++)
695 if (ASTTrue == *it)
696 OutputNode = ASTTrue;
697
698 break;
699
700 case NOR:
701 {
702 ASTNode o = ASTFalse;
703 for (ASTVec::const_iterator it = children.begin(), itend = children.end();
704 it != itend; it++)
705 {
706 if (ASTTrue == (*it))
707 {
708 o = ASTTrue;
709 break;
710 }
711 }
712
713 if (o == ASTTrue)
714 OutputNode = ASTFalse;
715 else
716 OutputNode = ASTTrue;
717
718 break;
719 }
720
721 case XOR:
722 {
723 bool output = false;
724 for (ASTVec::const_iterator it = children.begin(), itend = children.end();
725 it != itend; it++)
726 {
727 if (ASTTrue == *it)
728 output = !output; // parity.
729 }
730
731 if (output)
732 OutputNode = ASTTrue;
733 else
734 OutputNode = ASTFalse;
735
736 break;
737 }
738
739 case AND:
740 {
741 OutputNode = ASTTrue;
742 for (ASTVec::const_iterator it = children.begin(), itend = children.end();
743 it != itend; it++)
744 {
745 if (ASTFalse == (*it))
746 {
747 OutputNode = ASTFalse;
748 break;
749 }
750 }
751 break;
752 }
753
754 case NAND:
755 {
756 OutputNode = ASTFalse;
757 for (ASTVec::const_iterator it = children.begin(), itend = children.end();
758 it != itend; it++)
759 {
760 if (ASTFalse == (*it))
761 {
762 OutputNode = ASTTrue;
763 break;
764 }
765 }
766 break;
767 }
768
769 case IFF:
770 {
771 assert(2 == number_of_children);
772 const ASTNode& t0 = children[0];
773 const ASTNode& t1 = children[1];
774 if ((ASTTrue == t0 && ASTTrue == t1) ||
775 (ASTFalse == t0 && ASTFalse == t1))
776 OutputNode = ASTTrue;
777 else
778 OutputNode = ASTFalse;
779 break;
780 }
781
782 case IMPLIES:
783 {
784 assert(2 == number_of_children);
785 const ASTNode& t0 = children[0];
786 const ASTNode& t1 = children[1];
787 if ((ASTFalse == t0) || (ASTTrue == t0 && ASTTrue == t1))
788 OutputNode = ASTTrue;
789 else
790 OutputNode = ASTFalse;
791 break;
792 }
793
794 default:
795 FatalError("BVConstEvaluator: The input kind is not supported yet:");
796 break;
797 }
798 /*
799 if(BVCONST != k){
800 cerr<<inputwidth<<endl;
801 cerr<<"------------------------"<<endl;
802 t.LispPrint(cerr);
803 cerr<<endl;
804 OutputNode.LispPrint(cerr);
805 cerr<<endl<<"------------------------"<<endl;
806 }
807 */
808 assert(OutputNode.isConstant());
809 // UpdateSimplifyMap(t,OutputNode,false);
810 return OutputNode;
811 }
812
813 // Const evaluator logical and arithmetic operations.
NonMemberBVConstEvaluator(STPMgr * mgr,const ASTNode & t)814 ASTNode NonMemberBVConstEvaluator(STPMgr* mgr, const ASTNode& t)
815 {
816 if (t.isConstant())
817 return t;
818
819 return NonMemberBVConstEvaluator(mgr, t.GetKind(), t.GetChildren(),
820 t.GetValueWidth());
821 }
822
BVConstEvaluator(const ASTNode & t)823 ASTNode Simplifier::BVConstEvaluator(const ASTNode& t)
824 {
825 if (t.isConstant())
826 return t;
827
828 ASTNode OutputNode;
829
830 if (InsideSubstitutionMap(t, OutputNode))
831 return OutputNode;
832
833 OutputNode = NonMemberBVConstEvaluator(_bm, t);
834 UpdateSolverMap(t, OutputNode);
835 return OutputNode;
836 }
837 } // end of namespace stp
838