| 536 | } |
| 537 | |
| 538 | bool expr::isBasePlusOffset(expr &base, uint64_t &offset) const { |
| 539 | expr a, b; |
| 540 | if (isAdd(a, b)) { |
| 541 | if (a.isUInt(offset)) { |
| 542 | base = b; |
| 543 | return true; |
| 544 | } |
| 545 | if (b.isUInt(offset)) { |
| 546 | base = a; |
| 547 | return true; |
| 548 | } |
| 549 | } |
| 550 | base = *this; |
| 551 | offset = 0; |
| 552 | return true; |
| 553 | } |
| 554 | |
| 555 | bool expr::isConstArray(expr &val) const { |
| 556 | return isUnOp(val, Z3_OP_CONST_ARRAY); |