1 /********************************************************************
2 * AUTHORS: Trevor Hansen
3 *
4 * BEGIN DATE: Februrary, 2010
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/AST/NodeFactory/SimplifyingNodeFactory.h"
26 #include "stp/AST/AST.h"
27 #include "stp/AST/ASTKind.h"
28 #include "stp/AbsRefineCounterExample/ArrayTransformer.h"
29 #include "stp/Simplifier/Simplifier.h"
30 #include <cassert>
31 #include <cmath>
32
33 using stp::Kind;
34
35 using stp::SYMBOL;
36 using stp::BVNOT;
37 using stp::BVMOD;
38 using stp::BVUMINUS;
39 using stp::BVMULT;
40 using stp::ITE;
41 using stp::EQ;
42 using stp::BVSRSHIFT;
43 using stp::SBVREM;
44 using stp::SBVMOD;
45 using stp::SBVDIV;
46 using stp::BVCONCAT;
47 using stp::BVEXTRACT;
48 using stp::BVRIGHTSHIFT;
49 using stp::BVPLUS;
50 using stp::BVXOR;
51 using stp::BVDIV;
52
53 using std::cout;
54 using std::endl;
55
56 static bool debug_simplifyingNodeFactory = false;
57
children_all_constants(const ASTVec & children) const58 bool SimplifyingNodeFactory::children_all_constants(
59 const ASTVec& children) const
60 {
61 for (unsigned i = 0; i < children.size(); i++)
62 {
63 if (!children[i].isConstant())
64 {
65 return false;
66 }
67 }
68
69 return true;
70 }
71
get_smallest_number(const unsigned width)72 ASTNode SimplifyingNodeFactory::get_smallest_number(const unsigned width)
73 {
74 // 1000000000 (most negative number.)
75 stp::CBV max = CONSTANTBV::BitVector_Create(width, true);
76 CONSTANTBV::BitVector_Bit_On(max, width - 1);
77 return bm.CreateBVConst(max, width);
78 }
79
get_largest_number(const unsigned width)80 ASTNode SimplifyingNodeFactory::get_largest_number(const unsigned width)
81 {
82 // 011111111 (most positive number.)
83 stp::CBV max = CONSTANTBV::BitVector_Create(width, false);
84 CONSTANTBV::BitVector_Fill(max);
85 CONSTANTBV::BitVector_Bit_Off(max, width - 1);
86 return bm.CreateBVConst(max, width);
87 }
88
create_gt_node(const ASTVec & children)89 ASTNode SimplifyingNodeFactory::create_gt_node(const ASTVec& children)
90 {
91 if (children[0] == children[1])
92 {
93 return ASTFalse;
94 }
95
96 if (children[0].isConstant() &&
97 CONSTANTBV::BitVector_is_empty(children[0].GetBVConst()))
98 {
99 return ASTFalse;
100 }
101
102 if (children[1].isConstant() &&
103 CONSTANTBV::BitVector_is_full(children[1].GetBVConst()))
104 {
105 return ASTFalse;
106 }
107
108 if (children[0].GetKind() == BVRIGHTSHIFT && children[0][0] == children[1])
109 {
110 return ASTFalse;
111 }
112
113 ASTNode result;
114
115 //2nd part is the same ->only care about 1st part
116 if (children[0].GetKind() == BVCONCAT && children[1].GetKind() == BVCONCAT &&
117 children[0][1] == children[1][1])
118 {
119 result = NodeFactory::CreateNode(stp::BVGT, children[0][0], children[1][0]);
120 }
121
122 //1st part is the same ->only care about 2nd part
123 if (children[0].GetKind() == BVCONCAT && children[1].GetKind() == BVCONCAT &&
124 children[0][0] == children[1][0])
125 {
126 result = NodeFactory::CreateNode(stp::BVGT, children[0][1], children[1][1]);
127 }
128
129 //If child 1 is constant, GT == NOT EQ
130 if (children[1].isConstant() &&
131 CONSTANTBV::BitVector_is_empty(children[1].GetBVConst()))
132 {
133 result = NodeFactory::CreateNode(
134 stp::NOT, NodeFactory::CreateNode(EQ, children[0], children[1]));
135 }
136
137 //If child 0 is constant, GT == NOT EQ
138 if (children[0].isConstant() &&
139 CONSTANTBV::BitVector_is_full(children[0].GetBVConst()))
140 {
141 result = NodeFactory::CreateNode(
142 stp::NOT, NodeFactory::CreateNode(EQ, children[0], children[1]));
143 }
144
145 if (children[0].GetKind() == stp::BVAND && children[0].Degree() > 1 &&
146 ((children[0][0] == children[1]) || children[0][1] == children[1]))
147 {
148 return ASTFalse;
149 }
150
151 return result;
152 }
153
CreateNode(Kind kind,const ASTVec & children)154 ASTNode SimplifyingNodeFactory::CreateNode(Kind kind, const ASTVec& children)
155 {
156 assert(kind != SYMBOL);
157 // These are created specially.
158
159 // If all the parameters are constant, return the constant value.
160 // The bitblaster calls CreateNode with a boolean vector. We don't try to
161 // simplify those.
162 if (kind != stp::UNDEFINED && kind != stp::BOOLEAN &&
163 kind != stp::BITVECTOR && kind != stp::ARRAY &&
164 children_all_constants(children))
165 {
166 const ASTNode& hash = hashing.CreateNode(kind, children);
167 const ASTNode& c = NonMemberBVConstEvaluator(&bm, hash);
168 assert(c.isConstant());
169 return c;
170 }
171
172 ASTNode result;
173 switch (kind)
174 {
175 // convert the Less thans to greater thans.
176 case stp::BVLT:
177 assert(children.size() == 2);
178 result = NodeFactory::CreateNode(stp::BVGT, children[1], children[0]);
179 break;
180
181 case stp::BVLE:
182 assert(children.size() == 2);
183 result = NodeFactory::CreateNode(stp::BVGE, children[1], children[0]);
184 break;
185
186 case stp::BVSLT:
187 assert(children.size() == 2);
188 result = NodeFactory::CreateNode(stp::BVSGT, children[1], children[0]);
189 break;
190
191 case stp::BVSLE:
192 assert(children.size() == 2);
193 result = NodeFactory::CreateNode(stp::BVSGE, children[1], children[0]);
194 break;
195
196 case stp::BVSGT:
197 assert(children.size() == 2);
198 if (children[0] == children[1])
199 result = ASTFalse;
200
201 if (children[1].GetKind() == stp::BVCONST)
202 {
203 const unsigned width = children[0].GetValueWidth();
204 if (children[1] == get_largest_number(width))
205 result = ASTFalse;
206 }
207
208 if (children[0].GetKind() == stp::BVCONST)
209 {
210 const unsigned width = children[0].GetValueWidth();
211 if (children[0] == get_smallest_number(width))
212 result = ASTFalse;
213 }
214
215 //2nd part is the same -> only care about 1st part
216 if (children[0].GetKind() == BVCONCAT &&
217 children[1].GetKind() == BVCONCAT && children[0][1] == children[1][1])
218 {
219 result =
220 NodeFactory::CreateNode(stp::BVSGT, children[0][0], children[1][0]);
221 }
222
223 break;
224
225 case stp::BVGT:
226 assert(children.size() == 2);
227 result = create_gt_node(children);
228 break;
229
230 case stp::BVGE:
231 {
232 assert(children.size() == 2);
233 ASTNode a = NodeFactory::CreateNode(stp::BVGT, children[1], children[0]);
234 result = NodeFactory::CreateNode(stp::NOT, a);
235 }
236 break;
237
238 case stp::BVSGE:
239 {
240 assert(children.size() == 2);
241 ASTNode a = NodeFactory::CreateNode(stp::BVSGT, children[1], children[0]);
242 result = NodeFactory::CreateNode(stp::NOT, a);
243 }
244 break;
245
246 case stp::NOT:
247 result = CreateSimpleNot(children);
248 break;
249 case stp::AND:
250 result = CreateSimpleAndOr(1, children);
251 break;
252 case stp::OR:
253 result = CreateSimpleAndOr(0, children);
254 break;
255 case stp::NAND:
256 result = CreateSimpleNot(CreateSimpleAndOr(1, children));
257 break;
258 case stp::NOR:
259 result = CreateSimpleNot(CreateSimpleAndOr(0, children));
260 break;
261 case stp::XOR:
262 result = CreateSimpleXor(children);
263 break;
264 case ITE:
265 result = CreateSimpleFormITE(children);
266 break;
267 case EQ:
268 result = CreateSimpleEQ(children);
269 break;
270 case stp::IFF:
271 {
272 assert(children.size() == 2);
273 ASTVec newCh;
274 newCh.reserve(2);
275 result = CreateSimpleXor(children);
276 result = CreateSimpleNot(result);
277 break;
278 }
279 case stp::IMPLIES:
280 {
281 assert(children.size() == 2);
282 if (children[0] == children[1])
283 {
284 result = bm.ASTTrue;
285 }
286 else
287 {
288 ASTVec newCh;
289 newCh.reserve(2);
290 newCh.push_back(CreateSimpleNot(children[0]));
291 newCh.push_back(children[1]);
292 result = CreateSimpleAndOr(0, newCh);
293 }
294 break;
295 }
296
297 default:
298 result = hashing.CreateNode(kind, children);
299 }
300
301 if (result.IsNull())
302 result = hashing.CreateNode(kind, children);
303
304 return result;
305 }
306
CreateSimpleNot(const ASTNode & form)307 ASTNode SimplifyingNodeFactory::CreateSimpleNot(const ASTNode& form)
308 {
309 const Kind k = form.GetKind();
310 switch (k)
311 {
312 case stp::FALSE:
313 {
314 return ASTTrue;
315 }
316 case stp::TRUE:
317 {
318 return ASTFalse;
319 }
320 case stp::NOT:
321 {
322 // NOT NOT cancellation
323 return form[0];
324 }
325 default:
326 {
327 ASTVec children;
328 children.push_back(form);
329 return hashing.CreateNode(stp::NOT, children);
330 }
331 }
332 }
333
CreateSimpleNot(const ASTVec & children)334 ASTNode SimplifyingNodeFactory::CreateSimpleNot(const ASTVec& children)
335 {
336 assert(children.size() == 1);
337 const Kind k = children[0].GetKind();
338 switch (k)
339 {
340 case stp::FALSE:
341 {
342 return ASTTrue;
343 }
344 case stp::TRUE:
345 {
346 return ASTFalse;
347 }
348 case stp::NOT:
349 {
350 // NOT NOT cancellation
351 return children[0][0];
352 }
353 default:
354 {
355 return hashing.CreateNode(stp::NOT, children);
356 }
357 }
358 }
359
CreateSimpleAndOr(bool IsAnd,const ASTNode & form1,const ASTNode & form2)360 ASTNode SimplifyingNodeFactory::CreateSimpleAndOr(bool IsAnd,
361 const ASTNode& form1,
362 const ASTNode& form2)
363 {
364 ASTVec children;
365 children.push_back(form1);
366 children.push_back(form2);
367 return CreateSimpleAndOr(IsAnd, children);
368 }
369
handle_2_children(bool IsAnd,const ASTVec & children)370 ASTNode SimplifyingNodeFactory::handle_2_children(bool IsAnd,
371 const ASTVec& children)
372 {
373 if (children.size() == 2)
374 {
375 const Kind k = IsAnd ? stp::AND : stp::OR;
376 const ASTNode& c0 = children[0];
377 const ASTNode& c1 = children[1];
378
379 if (k == stp::OR)
380 {
381 //case of a || ~a which is constant TRUE
382
383 if (c0.GetKind() == stp::NOT && c0[0] == c1)
384 return ASTTrue;
385 if (c1.GetKind() == stp::NOT && c1[0] == c0)
386 return ASTTrue;
387 }
388 else
389 {
390 assert(k == stp::AND);
391 //case of a && ~a which is constant FALSE
392
393 if (c0.GetKind() == stp::NOT && c0[0] == c1)
394 return ASTFalse;
395 if (c1.GetKind() == stp::NOT && c1[0] == c0)
396 return ASTFalse;
397 }
398 }
399 return ASTUndefined;
400 }
401
CreateSimpleAndOr(bool IsAnd,const ASTVec & children)402 ASTNode SimplifyingNodeFactory::CreateSimpleAndOr(bool IsAnd,
403 const ASTVec& children)
404 {
405 ASTNode retval = handle_2_children(IsAnd, children);
406 if (retval != ASTUndefined)
407 return retval;
408
409 const ASTNode& annihilator = (IsAnd ? ASTFalse : ASTTrue);
410 const ASTNode& identity = (IsAnd ? ASTTrue : ASTFalse);
411
412 ASTVec new_children;
413 new_children.reserve(children.size());
414
415 for (ASTVec::const_iterator it = children.begin(), it_end = children.end();
416 it != it_end; it++)
417 {
418 ASTVec::const_iterator next_it;
419
420 const bool nextexists = (it + 1 < it_end);
421 if (nextexists)
422 next_it = it + 1;
423 else
424 next_it = it_end;
425
426 if (nextexists)
427 if (next_it->GetKind() == stp::NOT && (*next_it)[0] == *it)
428 return annihilator;
429
430 if (*it == annihilator)
431 {
432 return annihilator;
433 }
434 else if (*it == identity || (nextexists && (*next_it == *it)))
435 {
436 // just drop it
437 }
438 else
439 {
440 new_children.push_back(*it);
441 }
442 }
443
444 // If we get here, we saw no annihilators, and children should
445 // be only the non-True nodes.
446 switch (new_children.size())
447 {
448 case 0:
449 return identity;
450 break;
451
452 case 1:
453 return new_children[0];
454 break;
455
456 default:
457 // 2 or more children. Create a new node.
458 return hashing.CreateNode(IsAnd ? stp::AND : stp::OR, new_children);
459 break;
460 }
461 assert(false);
462 exit(-1);
463 }
464
465 // Tries to simplify the input to TRUE/FALSE. if it fails, then
466 // return the constructed equality
CreateSimpleEQ(const ASTVec & children)467 ASTNode SimplifyingNodeFactory::CreateSimpleEQ(const ASTVec& children)
468 {
469 assert(children.size() == 2);
470
471 // SYMBOL = something, if not that, then CONSTANT =
472 const bool swap = (children[1].GetKind() == stp::SYMBOL ||
473 ((children[0].GetKind() != stp::SYMBOL) &&
474 children[1].GetKind() == stp::BVCONST));
475 const ASTNode& in1 = swap ? children[1] : children[0];
476 const ASTNode& in2 = swap ? children[0] : children[1];
477 const Kind k1 = in1.GetKind();
478 const Kind k2 = in2.GetKind();
479 const int width = in1.GetValueWidth();
480
481 if (in1 == in2)
482 // terms are syntactically the same
483 return ASTTrue;
484
485 // here the terms are definitely not syntactically equal but may be
486 // semantically equal.
487 if (stp::BVCONST == k1 && stp::BVCONST == k2)
488 return ASTFalse;
489
490 if ((k1 == BVNOT && k2 == BVNOT) || (k1 == BVUMINUS && k2 == BVUMINUS))
491 return NodeFactory::CreateNode(EQ, in1[0], in2[0]);
492
493 if ((k1 == BVUMINUS && k2 == stp::BVCONST) ||
494 (k1 == BVNOT && k2 == stp::BVCONST))
495 return NodeFactory::CreateNode(EQ, in1[0],
496 NodeFactory::CreateTerm(k1, width, in2));
497
498 if ((k2 == BVUMINUS && k1 == stp::BVCONST) ||
499 (k2 == BVNOT && k1 == stp::BVCONST))
500 return NodeFactory::CreateNode(EQ, in2[0],
501 NodeFactory::CreateTerm(k2, width, in1));
502
503 if ((k1 == BVNOT && in1[0] == in2) || (k2 == BVNOT && in2[0] == in1))
504 return ASTFalse;
505
506 if (k2 == stp::BVDIV && k1 == stp::BVCONST &&
507 (in1 == bm.CreateZeroConst(width)))
508 return NodeFactory::CreateNode(stp::BVGT, in2[1], in2[0]);
509
510 if (k1 == stp::BVDIV && k2 == stp::BVCONST &&
511 (in2 == bm.CreateZeroConst(width)))
512 return NodeFactory::CreateNode(stp::BVGT, in1[1], in1[0]);
513
514 // split the constant to equal each part of the concat.
515 if (BVCONCAT == k2 && stp::BVCONST == k1)
516 {
517 int low_b = 0;
518 int high_b = (int)in2[1].GetValueWidth() - 1;
519 int low_t = in2[1].GetValueWidth();
520 int high_t = width - 1;
521
522 ASTNode c0 = NodeFactory::CreateTerm(BVEXTRACT, in2[1].GetValueWidth(), in1,
523 bm.CreateBVConst(32, high_b),
524 bm.CreateBVConst(32, low_b));
525 ASTNode c1 = NodeFactory::CreateTerm(BVEXTRACT, in2[0].GetValueWidth(), in1,
526 bm.CreateBVConst(32, high_t),
527 bm.CreateBVConst(32, low_t));
528
529 ASTNode a = NodeFactory::CreateNode(EQ, in2[1], c0);
530 ASTNode b = NodeFactory::CreateNode(EQ, in2[0], c1);
531 return NodeFactory::CreateNode(stp::AND, a, b);
532 }
533
534 // This increases the number of nodes. So disable for now.
535 if (false && BVCONCAT == k1 && BVCONCAT == k2 &&
536 in1[0].GetValueWidth() == in2[0].GetValueWidth())
537 {
538 ASTNode a = NodeFactory::CreateNode(EQ, in1[0], in2[0]);
539 ASTNode b = NodeFactory::CreateNode(EQ, in1[1], in2[1]);
540 return NodeFactory::CreateNode(stp::AND, a, b);
541 }
542
543 if (k1 == stp::BVCONST && k2 == ITE && in2[1].GetKind() == stp::BVCONST &&
544 in2[2].GetKind() == stp::BVCONST)
545 {
546
547 ASTNode result = NodeFactory::CreateNode(
548 ITE, in2[0], NodeFactory::CreateNode(EQ, in1, in2[1]),
549 NodeFactory::CreateNode(EQ, in1, in2[2]));
550
551 return result;
552 }
553
554 // Don't create a PLUS with the same operand on both sides.
555 // We don't do big pluses, because 1) this algorithm isn't good enough
556 // 2) it might split nodes (a lot).
557 if ((k1 == BVPLUS && in1.Degree() <= 2) ||
558 (k2 == BVPLUS && in2.Degree() <= 2))
559 {
560 const ASTVec& c1 = (k1 == BVPLUS) ? in1.GetChildren() : ASTVec(1, in1);
561 const ASTVec& c2 = (k2 == BVPLUS) ? in2.GetChildren() : ASTVec(1, in2);
562
563 if (c1.size() <= 2 && c2.size() <= 2)
564 {
565 int match1 = -1, match2 = -1;
566
567 for (size_t i = 0, c1Size = c1.size(); i < c1Size; ++i)
568 {
569 for (size_t j = 0, c2Size = c2.size(); j < c2Size; ++j)
570 {
571 if (c1[i] == c2[j])
572 {
573 match1 = i;
574 match2 = j;
575 }
576 }
577 }
578
579 if (match1 != -1)
580 {
581 assert(match2 != -1);
582 assert(match1 == 0 || match1 == 1);
583 assert(match2 == 0 || match2 == 1);
584 // If it was 1 element before, it's zero now.
585 ASTNode n1 = c1.size() == 1 ? bm.CreateZeroConst(width)
586 : c1[match1 == 0 ? 1 : 0];
587 ASTNode n2 = c2.size() == 1 ? bm.CreateZeroConst(width)
588 : c2[match2 == 0 ? 1 : 0];
589 return NodeFactory::CreateNode(EQ, n1, n2);
590 }
591 }
592 }
593
594 if (k2 == BVPLUS && in2.Degree() == 2 && (in2[1] == in1 || in2[0] == in1))
595 {
596 return NodeFactory::CreateNode(EQ, bm.CreateZeroConst(width),
597 in2[1] == in1 ? in2[0] : in2[1]);
598 }
599
600 if (k1 == BVPLUS && in1.Degree() == 2 && (in1[1] == in2 || in1[0] == in2))
601 {
602 return NodeFactory::CreateNode(EQ, bm.CreateZeroConst(width),
603 in1[1] == in2 ? in1[0] : in1[1]);
604 }
605
606 if (k1 == stp::BVCONST && k2 == stp::BVXOR && in2.Degree() == 2 &&
607 in2[0].GetKind() == stp::BVCONST)
608 {
609 return NodeFactory::CreateNode(
610 EQ, NodeFactory::CreateTerm(stp::BVXOR, width, in1, in2[0]), in2[1]);
611 }
612
613 if (k2 == stp::BVCONST && k1 == stp::BVXOR && in1.Degree() == 2 &&
614 in1[0].GetKind() == stp::BVCONST)
615 {
616 return NodeFactory::CreateNode(
617 EQ, NodeFactory::CreateTerm(stp::BVXOR, width, in2, in1[0]), in1[1]);
618 }
619
620 if (k2 == stp::BVXOR && in2.Degree() == 2 && in1 == in2[0])
621 {
622 return NodeFactory::CreateNode(EQ, bm.CreateZeroConst(width), in2[1]);
623 }
624
625 if (k1 == stp::BVXOR && in1.Degree() == 2 && in2 == in1[0])
626 {
627 return NodeFactory::CreateNode(EQ, bm.CreateZeroConst(width), in1[1]);
628 }
629
630 if (k1 == stp::BVCONST && k2 == stp::BVSX &&
631 (in2[0].GetValueWidth() != (unsigned)width))
632 {
633 // Each of the bits in the extended part, and one into the un-extended part
634 // must be the same.
635 bool foundZero = false, foundOne = false;
636 const int original_width = in2[0].GetValueWidth();
637 const int new_width = in2.GetValueWidth();
638
639 for (int i = original_width - 1; i < new_width; i++)
640 {
641 if (CONSTANTBV::BitVector_bit_test(in1.GetBVConst(), i))
642 foundOne = true;
643 else
644 foundZero = true;
645 }
646
647 if (foundZero && foundOne)
648 return ASTFalse;
649
650 ASTNode lhs = NodeFactory::CreateTerm(
651 BVEXTRACT, original_width, in1,
652 bm.CreateBVConst(32, original_width - 1), bm.CreateZeroConst(32));
653 ASTNode rhs = NodeFactory::CreateTerm(
654 BVEXTRACT, original_width, in2,
655 bm.CreateBVConst(32, original_width - 1), bm.CreateZeroConst(32));
656
657 return NodeFactory::CreateNode(EQ, lhs, rhs);
658 }
659
660 // Simplifiy (5 = 4/x) to FALSE.
661 if (k1 == stp::BVCONST && k2 == stp::BVDIV &&
662 in2[0].GetKind() == stp::BVCONST)
663 {
664 ASTNode maxV = bm.CreateMaxConst(width);
665 if (CONSTANTBV::BitVector_Lexicompare(in1.GetBVConst(),
666 maxV.GetBVConst()) != 0 &&
667 CONSTANTBV::BitVector_Lexicompare(in1.GetBVConst(),
668 in2[0].GetBVConst()) > 0)
669 {
670 return ASTFalse;
671 }
672 }
673
674 if (k1 == BVNOT && k2 == BVUMINUS && in1[0] == in2[0])
675 return ASTFalse;
676
677 if (k1 == BVUMINUS && k2 == BVNOT && in1[0] == in2[0])
678 return ASTFalse;
679
680 // last resort is to CreateNode
681 return hashing.CreateNode(EQ, children);
682 }
683
684 // Constant children are accumulated in "accumconst".
CreateSimpleXor(const ASTVec & children)685 ASTNode SimplifyingNodeFactory::CreateSimpleXor(const ASTVec& children)
686 {
687 if (debug_simplifyingNodeFactory)
688 {
689 cout << "========" << endl << "CreateSimpXor ";
690
691 lpvec(children);
692 cout << endl;
693 }
694
695 ASTVec flat_children; // empty vector
696 flat_children = children;
697
698 // sort so that identical nodes occur in sequential runs, followed by
699 // their negations.
700 SortByExprNum(flat_children);
701
702 // This is the C Boolean value of all constant args seen. It is initially
703 // 0. TRUE children cause it to change value.
704 bool accumconst = 0;
705
706 ASTVec new_children;
707 new_children.reserve(children.size());
708
709 const ASTVec::const_iterator it_end = flat_children.end();
710 ASTVec::iterator next_it;
711 for (ASTVec::iterator it = flat_children.begin(); it != it_end; it++)
712 {
713 next_it = it + 1;
714 bool nextexists = (next_it < it_end);
715
716 if (ASTTrue == *it)
717 {
718 accumconst = !accumconst;
719 }
720 else if (ASTFalse == *it)
721 {
722 // Ignore it
723 }
724 else if (nextexists && (*next_it == *it))
725 {
726 // x XOR x = FALSE. Skip current, write "false" into next_it
727 // so that it gets tossed, too.
728 *next_it = ASTFalse;
729 }
730 else if (nextexists && (next_it->GetKind() == stp::NOT) &&
731 ((*next_it)[0] == *it))
732 {
733 // x XOR NOT x = TRUE. Skip current, write "true" into next_it
734 // so that it gets tossed, too.
735 *next_it = ASTTrue;
736 }
737 else if (stp::NOT == it->GetKind())
738 {
739 // If child is (NOT alpha), we can flip accumconst and use alpha.
740 // This is ok because (NOT alpha) == TRUE XOR alpha
741 accumconst = !accumconst;
742 // CreateSimpNot just takes child of not.
743 new_children.push_back(CreateSimpleNot(*it));
744 }
745 else
746 {
747 new_children.push_back(*it);
748 }
749 }
750
751 ASTNode retval;
752
753 // Children should be non-constant.
754 if (new_children.size() < 2)
755 {
756 if (0 == new_children.size())
757 {
758 // XOR(TRUE, FALSE) -- accumconst will be 1.
759 if (accumconst)
760 {
761 retval = ASTTrue;
762 }
763 else
764 {
765 retval = ASTFalse;
766 }
767 }
768 else
769 {
770 // there is just one child
771 // XOR(x, TRUE) -- accumconst will be 1.
772 if (accumconst)
773 {
774 retval = CreateSimpleNot(new_children[0]);
775 }
776 else
777 {
778 retval = new_children[0];
779 }
780 }
781 }
782 else
783 {
784 retval = hashing.CreateNode(stp::XOR, new_children);
785
786 // negate the result if accumulated negation
787 if (accumconst)
788 {
789 retval = CreateSimpleNot(retval);
790 }
791 }
792
793 if (debug_simplifyingNodeFactory)
794 {
795 cout << "returns " << retval << endl;
796 }
797 return retval;
798 }
799
CreateSimpleFormITE(const ASTVec & children)800 ASTNode SimplifyingNodeFactory::CreateSimpleFormITE(const ASTVec& children)
801 {
802 const ASTNode& child0 = children[0];
803 const ASTNode& child1 = children[1];
804 const ASTNode& child2 = children[2];
805
806 ASTNode retval;
807
808 if (debug_simplifyingNodeFactory)
809 {
810 cout << "========" << endl
811 << "CreateSimpleFormITE " << child0 << child1 << child2 << endl;
812 }
813
814 if (ASTTrue == child0)
815 {
816 retval = child1;
817 }
818 else if (ASTFalse == child0)
819 {
820 retval = child2;
821 }
822 else if (child1 == child2)
823 {
824 retval = child1;
825 }
826 // ITE(x, TRUE, y ) == x OR y
827 else if (ASTTrue == child1)
828 {
829 retval = CreateSimpleAndOr(0, child0, child2);
830 }
831 // ITE(x, FALSE, y ) == (!x AND y)
832 else if (ASTFalse == child1)
833 {
834 retval = CreateSimpleAndOr(1, CreateSimpleNot(child0), child2);
835 }
836 // ITE(x, y, TRUE ) == (!x OR y)
837 else if (ASTTrue == child2)
838 {
839 retval = CreateSimpleAndOr(0, CreateSimpleNot(child0), child1);
840 }
841 // ITE(x, y, FALSE ) == (x AND y)
842 else if (ASTFalse == child2)
843 {
844 retval = CreateSimpleAndOr(1, child0, child1);
845 }
846 else if (child0 == child1)
847 {
848 retval = CreateSimpleAndOr(0, child0, child2);
849 }
850 else if (child0 == child2)
851 {
852 retval = CreateSimpleAndOr(1, child0, child1);
853 }
854 else
855 {
856 retval = hashing.CreateNode(ITE, children);
857 }
858
859 if (debug_simplifyingNodeFactory)
860 {
861 cout << "returns " << retval << endl;
862 }
863
864 return retval;
865 }
866
867 // Move reads down through writes until, either we hit a write to an identical
868 // (syntactically) index,
869 // or we hit a write to an index that might be the same. This is intended to
870 // simplify things like:
871 // read(write(write(A,1,2),2,3),4) cheaply.
872 // The "children" that are passed should be the children of a READ.
chaseRead(const ASTVec & children,unsigned int width)873 ASTNode SimplifyingNodeFactory::chaseRead(const ASTVec& children,
874 unsigned int width)
875 {
876 assert(children[0].GetKind() == stp::WRITE);
877 const ASTNode& readIndex = children[1];
878 ASTNode write = children[0];
879
880 const bool read_is_const = (stp::BVCONST == readIndex.GetKind());
881 ASTVec c(2);
882
883 while (write.GetKind() == stp::WRITE)
884 {
885 const ASTNode& write_index = write[1];
886
887 if (readIndex == write_index)
888 {
889 // The are definately the same.
890 // cerr << "-";
891 return write[2];
892 }
893 else if (read_is_const && stp::BVCONST == write_index.GetKind())
894 {
895 // They are definately different. Ignore this.
896 // cerr << "+";
897 }
898 else
899 {
900 // They may be the same. Exit.
901 // We've finished the cheap tests, now do the expensive one.
902 // I don't know if the cost of this justifies the benefit.
903 // cerr << "#";
904 c[0] = write_index;
905 c[1] = readIndex;
906 ASTNode n = CreateSimpleEQ(c);
907 if (n == ASTTrue)
908 {
909 // cerr << "#";
910 return write[2];
911 }
912 else if (n == ASTFalse)
913 {
914 // cerr << "!";
915 }
916 else
917 {
918 // cerr << "."
919 // Perhaps they are the same, perhaps not.
920 break;
921 }
922 }
923 write = write[0];
924 }
925 return hashing.CreateTerm(stp::READ, width, write, readIndex);
926 }
927
928 // This gets called with the arguments swapped as well. So the rules don't need
929 // to know about commutivity.
plusRules(const ASTNode & n0,const ASTNode & n1)930 ASTNode SimplifyingNodeFactory::plusRules(const ASTNode& n0, const ASTNode& n1)
931 {
932 ASTNode result;
933 const int width = n0.GetValueWidth();
934
935 if (n0.isConstant() && CONSTANTBV::BitVector_is_empty(n0.GetBVConst()))
936 result = n1;
937 else if (width == 1 && n0 == n1)
938 result = bm.CreateZeroConst(1);
939 else if (n0 == n1)
940 result = NodeFactory::CreateTerm(
941 stp::BVMULT, width, bm.CreateBVConst(std::string("2"), 10, width), n0);
942 else if (n0.GetKind() == BVUMINUS && n1 == n0[0])
943 result = bm.CreateZeroConst(width);
944 else if (n1.GetKind() == BVPLUS && n1[1].GetKind() == BVUMINUS &&
945 n0 == n1[1][0] && n1.Degree() == 2)
946 result = n1[0];
947 else if (n1.GetKind() == BVPLUS && n1[0].GetKind() == BVUMINUS &&
948 n0 == n1[0][0] && n1.Degree() == 2)
949 result = n1[1];
950 else if (n1.GetKind() == BVUMINUS && n0.GetKind() == BVPLUS &&
951 n0.Degree() == 2 && n1[0] == n0[1])
952 result = n0[0];
953 else if (n1.GetKind() == BVUMINUS && n0.GetKind() == BVPLUS &&
954 n0.Degree() == 2 && n1[0] == n0[0])
955 result = n0[1];
956 else if (n1.GetKind() == BVNOT && n1[0] == n0)
957 result = bm.CreateMaxConst(width);
958 else if (n0.GetKind() == stp::BVCONST && n1.GetKind() == BVPLUS &&
959 n1.Degree() == 2 && n1[0].GetKind() == stp::BVCONST)
960 {
961 ASTVec ch;
962 ch.push_back(n0);
963 ch.push_back(n1[0]);
964 ASTNode constant = NonMemberBVConstEvaluator(&bm, BVPLUS, ch, width);
965 result = NodeFactory::CreateTerm(BVPLUS, width, constant, n1[1]);
966 }
967 else if (n1.GetKind() == BVUMINUS &&
968 (n0.isConstant() && CONSTANTBV::BitVector_is_full(n0.GetBVConst())))
969 {
970 result = NodeFactory::CreateTerm(BVNOT, width, n1[0]);
971 }
972 else if (n1.GetKind() == BVUMINUS && n0.GetKind() == BVUMINUS)
973 {
974 ASTNode r = NodeFactory::CreateTerm(BVPLUS, width, n0[0], n1[0]);
975 result = NodeFactory::CreateTerm(BVUMINUS, width, r);
976 }
977
978 return result;
979 }
980
handle_bvand(Kind kind,unsigned int width,const ASTVec & children,ASTNode & result)981 void SimplifyingNodeFactory::handle_bvand(Kind kind, unsigned int width,
982 const ASTVec& children,
983 ASTNode& result)
984 {
985 bool all_one_found = false;
986 bool all_zero_found = false;
987
988 for (size_t i = 0, size = children.size(); i < size; ++i)
989 {
990 if (children[i].GetKind() == stp::BVCONST)
991 {
992 if (CONSTANTBV::BitVector_is_full(children[i].GetBVConst()))
993 all_one_found = true;
994 else if (CONSTANTBV::BitVector_is_empty(children[i].GetBVConst()))
995 all_zero_found = true;
996 }
997 }
998
999 if (all_zero_found)
1000 {
1001 //ZERO out the result
1002 result = bm.CreateZeroConst(width);
1003 return;
1004 }
1005 else if (all_one_found)
1006 {
1007 //Add everything except the ALL-ONE
1008 ASTVec new_children;
1009 for (size_t i = 0, size = children.size(); i < size; ++i)
1010 {
1011 if (children[i].GetKind() != stp::BVCONST ||
1012 !CONSTANTBV::BitVector_is_full(children[i].GetBVConst()))
1013 {
1014 new_children.push_back(children[i]);
1015 }
1016 }
1017
1018 assert(new_children.size() != 0);
1019 // constant. Should have been handled earlier.
1020 if (new_children.size() == 1)
1021 {
1022 result = new_children[0];
1023 }
1024 else
1025 result = hashing.CreateTerm(kind, width, new_children);
1026 }
1027
1028 //Both are equal, return one
1029 if (children.size() == 2 && children[0] == children[1])
1030 {
1031 result = children[0];
1032 }
1033
1034 // If there is just one run of 1 bits, replace by an extract and a concat.
1035 // i.e. 00011111111000000 & x , will be replaced by an extract of x just
1036 // where
1037 // there are one bits.
1038 if (children.size() == 2 &&
1039 (children[0].isConstant() || children[1].isConstant()))
1040 {
1041 ASTNode c0 = children[0];
1042 ASTNode c1 = children[1];
1043 if (c1.isConstant())
1044 {
1045 ASTNode t = c0;
1046 c0 = c1;
1047 c1 = t;
1048 }
1049
1050 int start = -1;
1051 int end = -1;
1052 stp::CBV c = c0.GetBVConst();
1053 bool bad = false;
1054 for (int i = 0; i < (int)width; i++)
1055 {
1056 if (CONSTANTBV::BitVector_bit_test(c, i))
1057 {
1058 if (start == -1)
1059 start = i; // first one bit.
1060 else if (end != -1)
1061 bad = true;
1062 }
1063
1064 if (!CONSTANTBV::BitVector_bit_test(c, i))
1065 {
1066 if (start != -1 && end == -1)
1067 end = i - 1; // end of run.
1068 }
1069 }
1070 if (start != -1 && end == -1)
1071 end = (int)width - 1;
1072
1073 if (!bad && start != -1)
1074 {
1075 assert(end != -1);
1076
1077 result = NodeFactory::CreateTerm(BVEXTRACT, end - start + 1, c1,
1078 bm.CreateBVConst(32, end),
1079 bm.CreateBVConst(32, start));
1080
1081 if (start > 0)
1082 {
1083 ASTNode z = bm.CreateZeroConst(start);
1084 result = NodeFactory::CreateTerm(BVCONCAT, end + 1, result, z);
1085 }
1086 if (end < (int)width - 1)
1087 {
1088 ASTNode z = bm.CreateZeroConst((int)width - end - 1);
1089 result = NodeFactory::CreateTerm(BVCONCAT, width, z, result);
1090 }
1091 }
1092 }
1093
1094 if (children.size() == 2)
1095 {
1096 if (children[1].GetKind() == BVNOT && children[1][0] == children[0])
1097 result = bm.CreateZeroConst(width);
1098 if (children[0].GetKind() == BVNOT && children[0][0] == children[1])
1099 result = bm.CreateZeroConst(width);
1100 }
1101 }
1102
CreateTerm(Kind kind,unsigned int width,const ASTVec & children)1103 ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width,
1104 const ASTVec& children)
1105 {
1106 if (!is_Term_kind(kind))
1107 FatalError("CreateTerm: Illegal kind to CreateTerm:", ASTUndefined, kind);
1108
1109 assert(kind != stp::BVCONST);
1110 // These are created specially.
1111 assert(kind != stp::SYMBOL);
1112 // so are these.
1113
1114 assert(bm.hashingNodeFactory == &hashing);
1115
1116 // If all the parameters are constant, return the constant value.
1117 if (children_all_constants(children))
1118 {
1119 const ASTNode& hash = hashing.CreateTerm(kind, width, children);
1120 const ASTNode& c = NonMemberBVConstEvaluator(&bm, hash);
1121 assert(c.isConstant());
1122 return c;
1123 }
1124
1125 ASTNode result;
1126 switch (kind)
1127 {
1128 case stp::BVZX:
1129 {
1130 if (width - children[0].GetValueWidth() > 0)
1131 {
1132 ASTNode zero = bm.CreateZeroConst(width - children[0].GetValueWidth());
1133 result = NodeFactory::CreateTerm(BVCONCAT, width, zero, children[0]);
1134 }
1135 else if (width == children[0].GetValueWidth())
1136 {
1137 result = children[0];
1138 }
1139 else
1140 {
1141 FatalError("Negative zero extend", children[0]);
1142 }
1143 break;
1144 }
1145
1146 case ITE:
1147 {
1148 if (children[0] == ASTTrue)
1149 result = children[1];
1150 else if (children[0] == ASTFalse)
1151 result = children[2];
1152 else if (children[1] == children[2])
1153 result = children[1];
1154 else if (children[2].GetKind() == ITE && (children[2][0] == children[0]))
1155 {
1156 if (stp::ARRAY_TYPE == children[2].GetType())
1157 result = NodeFactory::CreateArrayTerm(
1158 ITE, children[2].GetIndexWidth(), children[2].GetValueWidth(),
1159 children[0], children[1], children[2][2]);
1160 else
1161 result = NodeFactory::CreateTerm(ITE, width, children[0], children[1],
1162 children[2][2]);
1163 }
1164 else if (children[1].GetKind() == ITE && (children[1][0] == children[0]))
1165 {
1166 if (stp::ARRAY_TYPE == children[1].GetType())
1167 result = NodeFactory::CreateArrayTerm(
1168 ITE, children[1].GetIndexWidth(), children[1].GetValueWidth(),
1169 children[0], children[1][1], children[2]);
1170 else
1171 result = NodeFactory::CreateTerm(ITE, width, children[0],
1172 children[1][1], children[2]);
1173 }
1174 else if (children[0].GetKind() == stp::NOT)
1175 {
1176 if (stp::ARRAY_TYPE == children[1].GetType())
1177 result = NodeFactory::CreateArrayTerm(
1178 ITE, children[1].GetIndexWidth(), children[1].GetValueWidth(),
1179 children[0][0], children[2], children[1]);
1180 else
1181 result = NodeFactory::CreateTerm(ITE, width, children[0][0],
1182 children[2], children[1]);
1183 }
1184 else if (children[0].GetKind() == EQ && children[0][1] == children[1] &&
1185 children[0][0].GetKind() == stp::BVCONST &&
1186 children[0][1].GetKind() != stp::BVCONST)
1187 result = NodeFactory::CreateTerm(ITE, width, children[0],
1188 children[0][0], children[2]);
1189 else if (children[0].GetKind() == EQ && children[0][0] == children[1] &&
1190 children[0][1].GetKind() == stp::BVCONST &&
1191 children[0][0].GetKind() != stp::BVCONST)
1192 result = NodeFactory::CreateTerm(ITE, width, children[0],
1193 children[0][1], children[2]);
1194 break;
1195 }
1196
1197 case stp::BVMULT:
1198 {
1199 if (children.size() == 2)
1200 {
1201 if (children[0].isConstant() &&
1202 CONSTANTBV::BitVector_is_empty(children[0].GetBVConst()))
1203 result = bm.CreateZeroConst(width);
1204
1205 else if (children[1].isConstant() &&
1206 CONSTANTBV::BitVector_is_empty(children[1].GetBVConst()))
1207 result = bm.CreateZeroConst(width);
1208
1209 else if (children[1].isConstant() &&
1210 children[1] == bm.CreateOneConst(width))
1211 result = children[0];
1212
1213 else if (children[0].isConstant() &&
1214 children[0] == bm.CreateOneConst(width))
1215 result = children[1];
1216
1217 else if (width == 1 && children[0] == children[1])
1218 result = children[0];
1219
1220 else if (children[0].GetKind() == BVUMINUS &&
1221 children[1].GetKind() == BVUMINUS)
1222 result = NodeFactory::CreateTerm(stp::BVMULT, width, children[0][0],
1223 children[1][0]);
1224 else if (children[0].GetKind() == BVUMINUS)
1225 {
1226 result = NodeFactory::CreateTerm(stp::BVMULT, width, children[0][0],
1227 children[1]);
1228 result = NodeFactory::CreateTerm(BVUMINUS, width, result);
1229 }
1230 else if (children[1].GetKind() == BVUMINUS)
1231 {
1232 result = NodeFactory::CreateTerm(stp::BVMULT, width, children[1][0],
1233 children[0]);
1234 result = NodeFactory::CreateTerm(BVUMINUS, width, result);
1235 }
1236 }
1237 else if (children.size() > 2)
1238 {
1239 // Never create multiplications with arity > 2.
1240
1241 std::deque<ASTNode> names;
1242
1243 for (unsigned i = 0; i < children.size(); i++)
1244 names.push_back(children[i]);
1245
1246 while (names.size() > 1)
1247 {
1248 ASTNode a = names.front();
1249 names.pop_front();
1250
1251 ASTNode b = names.front();
1252 names.pop_front();
1253
1254 ASTNode n = NodeFactory::CreateTerm(BVMULT, a.GetValueWidth(), a, b);
1255 names.push_back(n);
1256 }
1257 result = names.front();
1258 }
1259 }
1260 break;
1261
1262 case stp::BVLEFTSHIFT:
1263 {
1264 if (children[0].isConstant() &&
1265 CONSTANTBV::BitVector_is_empty(children[0].GetBVConst()))
1266 result = bm.CreateZeroConst(width);
1267 else if (children[1].isConstant())
1268 result = stp::Simplifier::convertKnownShiftAmount(kind, children, bm,
1269 &hashing);
1270 else if (width == 1 && children[0] == children[1])
1271 result = bm.CreateZeroConst(1);
1272 else if (children[0].GetKind() == BVUMINUS)
1273 result = NodeFactory::CreateTerm(
1274 BVUMINUS, width,
1275 NodeFactory::CreateTerm(stp::BVLEFTSHIFT, width, children[0][0],
1276 children[1]));
1277 }
1278 break;
1279
1280 case BVRIGHTSHIFT:
1281 {
1282 if (children[0] == children[1])
1283 result = bm.CreateZeroConst(width);
1284 if (children[0].isConstant() &&
1285 CONSTANTBV::BitVector_is_empty(children[0].GetBVConst()))
1286 result = bm.CreateZeroConst(width);
1287 else if (children[1].isConstant())
1288 result = stp::Simplifier::convertKnownShiftAmount(kind, children, bm,
1289 &hashing);
1290 else if (children[0].isConstant() &&
1291 children[0] == bm.CreateOneConst(width))
1292 result = NodeFactory::CreateTerm(
1293 ITE, width,
1294 NodeFactory::CreateNode(EQ, children[1], bm.CreateZeroConst(width)),
1295 children[0], bm.CreateZeroConst(width));
1296 else if (width >= 3 && children[0].GetKind() == BVNOT &&
1297 children[1] == children[0][0])
1298 result = NodeFactory::CreateTerm(BVRIGHTSHIFT, width,
1299 bm.CreateMaxConst(width),
1300 children[0][0]); // 320 -> 170
1301 else if (width >= 3 && children[1].GetKind() == BVNOT &&
1302 children[1][0] == children[0])
1303 result = NodeFactory::CreateTerm(BVRIGHTSHIFT, width,
1304 bm.CreateMaxConst(width),
1305 children[1]); // 320 -> 170
1306 else if (width >= 3 && children[0].GetKind() == BVNOT &&
1307 children[1].GetKind() == BVUMINUS &&
1308 children[1][0] == children[0][0])
1309 result = NodeFactory::CreateTerm(
1310 BVUMINUS, width,
1311 NodeFactory::CreateTerm(
1312 ITE, width, NodeFactory::CreateNode(
1313 EQ, bm.CreateZeroConst(width), children[0][0]),
1314 bm.CreateOneConst(width),
1315 bm.CreateZeroConst(width))); // 391 -> 70
1316 }
1317 break;
1318
1319 case stp::BVSRSHIFT:
1320 {
1321 if (children[0].isConstant() &&
1322 CONSTANTBV::BitVector_is_empty(children[0].GetBVConst()))
1323 result = bm.CreateZeroConst(width);
1324 else if (width > 1 && children[0].isConstant() &&
1325 children[0] == bm.CreateOneConst(width))
1326 result = NodeFactory::CreateTerm(
1327 ITE, width,
1328 NodeFactory::CreateNode(EQ, children[1], bm.CreateZeroConst(width)),
1329 children[0], bm.CreateZeroConst(width));
1330 else if (children[0].isConstant() &&
1331 CONSTANTBV::BitVector_is_full(children[0].GetBVConst()))
1332 result = bm.CreateMaxConst(width);
1333 else if (children[1].isConstant() &&
1334 CONSTANTBV::BitVector_is_empty(children[1].GetBVConst()))
1335 result = children[0];
1336 else if (width == 1 && children[0] == children[1])
1337 result = children[0];
1338 else if ((children[0] == children[1]) ||
1339 (children[0].GetKind() == BVUMINUS &&
1340 children[0][0] == children[1]))
1341 {
1342 assert(width > 1);
1343 ASTNode extract = NodeFactory::CreateTerm(
1344 BVEXTRACT, 1, children[0], bm.CreateBVConst(32, width - 1),
1345 bm.CreateBVConst(32, width - 1));
1346 result = NodeFactory::CreateTerm(stp::BVSX, width, extract,
1347 bm.CreateBVConst(32, width));
1348 }
1349 else if (width == 1 && children[1].isConstant() &&
1350 children[1] == bm.CreateOneConst(1))
1351 result = children[0];
1352 else if (children[1].isConstant())
1353 result = stp::Simplifier::convertArithmeticKnownShiftAmount(
1354 kind, children, bm, &hashing);
1355 else if (children[1].GetKind() == BVUMINUS &&
1356 children[0] == children[1][0])
1357 result = NodeFactory::CreateTerm(stp::BVSRSHIFT, width, children[0],
1358 children[1][0]);
1359 else if (children[0].isConstant() &&
1360 !CONSTANTBV::BitVector_bit_test(children[0].GetBVConst(),
1361 width - 1))
1362 result = NodeFactory::CreateTerm(BVRIGHTSHIFT, width, children[0],
1363 children[1]);
1364 else if (width >= 3 && children[0].GetKind() == BVNOT &&
1365 children[1].GetKind() == BVUMINUS &&
1366 children[1][0] == children[0][0])
1367 result = NodeFactory::CreateTerm(BVSRSHIFT, width, children[0],
1368 children[0][0]); // 414 -> 361
1369 else if (children[0].GetKind() == BVNOT)
1370 result = NodeFactory::CreateTerm(
1371 BVNOT, width, NodeFactory::CreateTerm(BVSRSHIFT, width,
1372 children[0][0], children[1]));
1373 }
1374 break;
1375
1376 case stp::BVSUB:
1377 if (children.size() == 2)
1378 {
1379 if (children.size() == 2 && children[0] == children[1])
1380 {
1381 result = bm.CreateZeroConst(width);
1382 }
1383 else if (children.size() == 2 &&
1384 children[1] == bm.CreateZeroConst(width))
1385 {
1386 result = children[0];
1387 }
1388 else
1389 {
1390 result = NodeFactory::CreateTerm(
1391 BVPLUS, width, children[0],
1392 NodeFactory::CreateTerm(BVUMINUS, width, children[1]));
1393 }
1394 }
1395 break;
1396
1397 case stp::BVOR:
1398 {
1399 if (children.size() == 2)
1400 {
1401 if (children[0] == children[1])
1402 result = children[0];
1403
1404 if (children[0].isConstant() &&
1405 CONSTANTBV::BitVector_is_full(children[0].GetBVConst()))
1406 result = bm.CreateMaxConst(width);
1407
1408 if (children[1].isConstant() &&
1409 CONSTANTBV::BitVector_is_full(children[1].GetBVConst()))
1410 result = bm.CreateMaxConst(width);
1411
1412 if (children[1].isConstant() &&
1413 CONSTANTBV::BitVector_is_empty(children[1].GetBVConst()))
1414 result = children[0];
1415
1416 if (children[0].isConstant() &&
1417 CONSTANTBV::BitVector_is_empty(children[0].GetBVConst()))
1418 result = children[1];
1419
1420 if (children[1].GetKind() == BVNOT && children[0] == children[1][0])
1421 result = bm.CreateMaxConst(width);
1422 if (children[0].GetKind() == BVNOT && children[1] == children[0][0])
1423 result = bm.CreateMaxConst(width);
1424 }
1425 }
1426 break;
1427
1428 case stp::BVXOR:
1429 if (children.size() == 2)
1430 {
1431 if (children[0] == children[1])
1432 result = bm.CreateZeroConst(width);
1433 if (children[1].isConstant() &&
1434 CONSTANTBV::BitVector_is_empty(children[1].GetBVConst()))
1435 result = children[0];
1436
1437 if (children[0].isConstant() &&
1438 CONSTANTBV::BitVector_is_empty(children[0].GetBVConst()))
1439 result = children[1];
1440
1441 if (children[1].isConstant() &&
1442 CONSTANTBV::BitVector_is_full(children[1].GetBVConst()))
1443 result = NodeFactory::CreateTerm(BVNOT, width, children[0]);
1444
1445 if (children[0].isConstant() &&
1446 CONSTANTBV::BitVector_is_full(children[0].GetBVConst()))
1447 result = NodeFactory::CreateTerm(BVNOT, width, children[1]);
1448
1449 if (children[1].GetKind() == BVNOT)
1450 {
1451 result = NodeFactory::CreateTerm(
1452 BVNOT, width, NodeFactory::CreateTerm(BVXOR, width, children[0],
1453 children[1][0]));
1454 }
1455 else if (children[0].GetKind() == BVNOT)
1456 {
1457 result = NodeFactory::CreateTerm(
1458 BVNOT, width, NodeFactory::CreateTerm(BVXOR, width, children[1],
1459 children[0][0]));
1460 }
1461 }
1462 break;
1463
1464 case stp::BVAND:
1465 {
1466 handle_bvand(kind, width, children, result);
1467 break;
1468 }
1469
1470 case stp::BVSX:
1471 {
1472 if (width == children[0].GetValueWidth())
1473 {
1474 result = children[0];
1475 }
1476 break;
1477 }
1478
1479 case BVNOT:
1480 if (children[0].GetKind() == BVNOT)
1481 result = children[0][0];
1482 if (children[0].GetKind() == BVPLUS && children[0].Degree() == 2 &&
1483 children[0][0].GetKind() == stp::BVCONST &&
1484 children[0][0] == bm.CreateMaxConst(width))
1485 result = NodeFactory::CreateTerm(BVUMINUS, width, children[0][1]);
1486 if (children[0].GetKind() == BVUMINUS)
1487 result = NodeFactory::CreateTerm(BVPLUS, width, children[0][0],
1488 bm.CreateMaxConst(width));
1489 if (children[0].GetKind() == BVMOD && children[0][0].GetKind() == BVNOT &&
1490 children[0][1].GetKind() == BVUMINUS &&
1491 children[0][1][0] == children[0][0][0])
1492 result = children[0][0][0];
1493
1494 break;
1495
1496 case BVUMINUS:
1497 if (children[0].GetKind() == BVUMINUS)
1498 result = children[0][0];
1499 else if (width == 1)
1500 result = children[0];
1501 else if (children[0].GetKind() == BVPLUS && children[0].Degree() == 2 &&
1502 children[0][0].GetKind() == stp::BVCONST &&
1503 children[0][0] == bm.CreateOneConst(width))
1504 result = NodeFactory::CreateTerm(BVNOT, width, children[0][1]);
1505 else if (children[0].GetKind() == BVNOT)
1506 result = NodeFactory::CreateTerm(BVPLUS, width, children[0][0],
1507 bm.CreateOneConst(width));
1508 else if (children[0].GetKind() == stp::BVSX &&
1509 children[0][0].GetValueWidth() == 1)
1510 result = NodeFactory::CreateTerm(
1511 BVCONCAT, width, bm.CreateZeroConst(width - 1), children[0][0]);
1512 else if (children[0].GetKind() == BVMULT && children[0].Degree() == 2 &&
1513 children[0][0] == bm.CreateMaxConst(width))
1514 result = children[0][1];
1515 break;
1516
1517 case BVEXTRACT:
1518 if (width == children[0].GetValueWidth())
1519 result = children[0];
1520 else if (BVEXTRACT ==
1521 children[0].GetKind()) // reduce an extract over an extract.
1522 {
1523 const unsigned outerLow = children[2].GetUnsignedConst();
1524 const unsigned outerHigh = children[1].GetUnsignedConst();
1525
1526 const unsigned innerLow = children[0][2].GetUnsignedConst();
1527 // const unsigned innerHigh = children[0][1].GetUnsignedConst();
1528 result =
1529 NodeFactory::CreateTerm(BVEXTRACT, width, children[0][0],
1530 bm.CreateBVConst(32, outerHigh + innerLow),
1531 bm.CreateBVConst(32, outerLow + innerLow));
1532 }
1533 else if (BVCONCAT == children[0].GetKind())
1534 {
1535 // If the extract doesn't cross the concat, then remove the concat.
1536 const ASTNode& a = children[0][0];
1537 const ASTNode& b = children[0][1];
1538
1539 const unsigned low = children[2].GetUnsignedConst();
1540 const unsigned high = children[1].GetUnsignedConst();
1541
1542 if (high <
1543 b.GetValueWidth()) // Extract entirely from the lower value (b).
1544 {
1545 result = NodeFactory::CreateTerm(BVEXTRACT, width, b, children[1],
1546 children[2]);
1547 }
1548 if (low >=
1549 b.GetValueWidth()) // Extract entirely from the upper value (a).
1550 {
1551 ASTNode i = bm.CreateBVConst(32, high - b.GetValueWidth());
1552 ASTNode j = bm.CreateBVConst(32, low - b.GetValueWidth());
1553 result = NodeFactory::CreateTerm(BVEXTRACT, width, a, i, j);
1554 }
1555 }
1556 else if (BVUMINUS == children[0].GetKind() &&
1557 children[1] == bm.CreateZeroConst(children[1].GetValueWidth()) &&
1558 children[2] == bm.CreateZeroConst(children[2].GetValueWidth()))
1559 {
1560 result = NodeFactory::CreateTerm(BVEXTRACT, width, children[0][0],
1561 children[1], children[2]);
1562 }
1563 break;
1564
1565 case BVPLUS:
1566 if (children.size() == 2)
1567 {
1568 result = plusRules(children[0], children[1]);
1569 if (result.IsNull())
1570 result = plusRules(children[1], children[0]);
1571 }
1572 break;
1573
1574 case SBVMOD:
1575 {
1576 const ASTNode max = bm.CreateMaxConst(width);
1577
1578 if (children[1].isConstant() &&
1579 CONSTANTBV::BitVector_is_empty(children[1].GetBVConst()))
1580 result = children[0];
1581 else if (children[0] == children[1])
1582 result = bm.CreateZeroConst(width);
1583 else if (children[1].isConstant() &&
1584 children[1] == bm.CreateOneConst(width))
1585 result = bm.CreateZeroConst(width);
1586 else if (children[1].isConstant() &&
1587 children[1] == bm.CreateMaxConst(width))
1588 result = bm.CreateZeroConst(width);
1589 else if (children[0].isConstant() &&
1590 children[0] == bm.CreateZeroConst(width))
1591 result = bm.CreateZeroConst(width);
1592 else if (children[0].GetKind() == BVUMINUS &&
1593 children[0][0] == children[1])
1594 result = bm.CreateZeroConst(width);
1595 else if (children[1].GetKind() == BVUMINUS &&
1596 children[1][0] == children[0])
1597 result = bm.CreateZeroConst(width);
1598 #if 0
1599 else if ( width >= 4 && children[0].GetKind() == BVNOT && children[1] == children[0][0] )
1600 result = bm.CreateTerm(SBVMOD,width,max,children[0][0]);//9759 -> 542 | 4842 ms
1601 else if ( width >= 4 && children[1].GetKind() == BVNOT && children[1][0] == children[0] )
1602 result = bm.CreateTerm(SBVMOD,width,max,children[1]);//9759 -> 542 | 4005 ms
1603 else if ( width >= 4 && children[0].GetKind() == BVNOT && children[1].GetKind() == BVUMINUS && children[1][0] == children[0][0] )
1604 result = bm.CreateTerm(SBVMOD,width,max,children[1]);//9807 -> 674 | 2962 ms
1605 #endif
1606 }
1607
1608 break;
1609
1610 case stp::BVDIV:
1611 if (children[1].isConstant() && children[1] == bm.CreateOneConst(width))
1612 result = children[0];
1613 if (children[1].isConstant() &&
1614 CONSTANTBV::BitVector_bit_test(children[1].GetBVConst(), width - 1))
1615 {
1616 // We are dividing by something that has a one in the MSB. It's either 1
1617 // or zero.
1618 result = NodeFactory::CreateTerm(
1619 ITE, width,
1620 NodeFactory::CreateNode(stp::BVGE, children[0], children[1]),
1621 bm.CreateOneConst(width), bm.CreateZeroConst(width));
1622 }
1623 else if (children[1].isConstant() &&
1624 children[1] == bm.CreateZeroConst(width))
1625 result = bm.CreateMaxConst(width);
1626 else if (children[0].isConstant() &&
1627 CONSTANTBV::BitVector_is_empty(children[0].GetBVConst()))
1628 result = NodeFactory::CreateTerm(
1629 ITE, width,
1630 NodeFactory::CreateNode(EQ, children[1], bm.CreateZeroConst(width)),
1631 bm.CreateMaxConst(width), bm.CreateZeroConst(width));
1632
1633 break;
1634
1635 case SBVDIV:
1636 if (children[1].isConstant() && children[1] == bm.CreateOneConst(width))
1637 result = children[0];
1638 if (children[1].isConstant() &&
1639 CONSTANTBV::BitVector_is_full(children[1].GetBVConst()))
1640 result = NodeFactory::CreateTerm(BVUMINUS, width, children[0]);
1641 break;
1642
1643 case SBVREM:
1644 {
1645 const ASTNode one = bm.CreateOneConst(width);
1646 const ASTNode zero = bm.CreateZeroConst(width);
1647 const ASTNode max = bm.CreateMaxConst(width);
1648
1649 if (children[0] == children[1])
1650 result = bm.CreateZeroConst(width);
1651 else if (children[0].isConstant() &&
1652 CONSTANTBV::BitVector_is_empty(children[0].GetBVConst()))
1653 result = bm.CreateZeroConst(width);
1654 else if (children[1].isConstant() &&
1655 CONSTANTBV::BitVector_is_full(children[1].GetBVConst()))
1656 result = bm.CreateZeroConst(width);
1657 else if (children[1].isConstant() &&
1658 CONSTANTBV::BitVector_is_empty(children[1].GetBVConst()))
1659 result = children[0];
1660 else if (children[1].isConstant() &&
1661 bm.CreateOneConst(width) == children[1])
1662 result = bm.CreateZeroConst(width);
1663 else if (children[1].GetKind() == BVUMINUS)
1664 result =
1665 NodeFactory::CreateTerm(SBVREM, width, children[0], children[1][0]);
1666 else if (children[0].GetKind() == BVUMINUS &&
1667 children[0][0] == children[1])
1668 result = bm.CreateZeroConst(width);
1669 #if 0
1670 else if ( width >= 4 && children[0].GetKind() == BVNOT && children[1] == children[0][0] )
1671 result = bm.CreateTerm(BVUMINUS,width,bm.CreateTerm(SBVMOD,width,one,children[0][0]));//9350 -> 624 | 3072 ms
1672 else if ( width >= 4 && children[1].GetKind() == BVNOT && children[1][0] == children[0] )
1673 result = bm.CreateTerm(BVUMINUS,width,bm.CreateTerm(SBVMOD,width,one,children[1]));//9350 -> 624 | 2402 ms
1674 else if ( width >= 4 && children[0].GetKind() == BVUMINUS && children[1] == max)
1675 result = bm.CreateTerm(BVUMINUS,width,bm.CreateTerm(SBVREM,width,children[0][0],children[1]));//123 -> 83 | 1600 ms
1676 #endif
1677 }
1678
1679 break;
1680
1681 case BVMOD:
1682 {
1683 if (children[0] == children[1])
1684 result = bm.CreateZeroConst(width);
1685
1686 if (children[0].isConstant() &&
1687 CONSTANTBV::BitVector_is_empty(children[0].GetBVConst()))
1688 result = bm.CreateZeroConst(width);
1689
1690 if (children[1].isConstant() &&
1691 CONSTANTBV::BitVector_is_empty(children[1].GetBVConst()))
1692 result = children[0];
1693
1694 if (children[0].GetKind() == BVPLUS && children[0].Degree() == 2 &&
1695 children[0][0] == bm.CreateMaxConst(width) &&
1696 children[1] == children[0][1])
1697 result = children[0];
1698
1699 const ASTNode one = bm.CreateOneConst(width);
1700
1701 if (children[0].GetKind() == BVNOT && children[1].GetKind() == BVUMINUS &&
1702 children[1][0] == children[0][0])
1703 result = children[0];
1704
1705 if (children[1].isConstant() && children[1] == one)
1706 result = bm.CreateZeroConst(width);
1707
1708 if (children[0].isConstant() && children[0] == one)
1709 result = NodeFactory::CreateTerm(
1710 ITE, width, NodeFactory::CreateNode(EQ, children[1], one),
1711 bm.CreateZeroConst(width), one);
1712 #if 0
1713 if ( width >= 3 && children[0].GetKind() == BVNOT && children[1] == children[0][0] )
1714 result = NodeFactory::CreateTerm(BVMOD,width,bm.CreateMaxConst(width),children[0][0]);//3285 -> 3113
1715
1716 if ( width >= 3 && children[1].GetKind() == BVNOT && children[1][0] == children[0] )
1717 result = NodeFactory::CreateTerm(BVMOD,width,bm.CreateMaxConst(width),children[1]);//3285 -> 3113
1718
1719 if ( width >= 4 && children[0].GetKind() == BVUMINUS && children[1].GetKind() == BVNOT && children[1][0] == children[0][0] )
1720 result = NodeFactory::CreateTerm(SBVREM,width,one,children[1]); //8883 -> 206 | 1566 ms
1721 #endif
1722 }
1723
1724 break;
1725
1726 case stp::WRITE:
1727 if (children[0].GetKind() == stp::WRITE && children[1] == children[0][1])
1728 {
1729 // If the indexes of two writes are the same, then discard the inner
1730 // write.
1731 result = NodeFactory::CreateArrayTerm(
1732 stp::WRITE, children[0].GetIndexWidth(),
1733 children[0].GetValueWidth(), children[0][0], children[1],
1734 children[2]);
1735 }
1736 else if (children[2].GetKind() == stp::READ &&
1737 children[0] == children[2][0] && children[1] == children[2][1])
1738 {
1739 // Its writing into the array what's already there. i.e. a[i] = a[i]
1740 result = children[0];
1741 }
1742 break;
1743
1744 case stp::READ:
1745 if (children[0].GetKind() == stp::WRITE)
1746 {
1747 result = chaseRead(children, width);
1748 }
1749 break;
1750
1751 default: // quieten compiler.
1752 break;
1753 }
1754
1755 if (result.IsNull())
1756 result = hashing.CreateTerm(kind, width, children);
1757
1758 return result;
1759 }
1760