| 913 | } |
| 914 | |
| 915 | expr expr::operator<<(const expr &rhs) const { |
| 916 | C(); |
| 917 | if (isZero() || rhs.isZero()) |
| 918 | return *this; |
| 919 | |
| 920 | uint64_t shift; |
| 921 | if (rhs.isUInt(shift)) { |
| 922 | auto bw = bits(); |
| 923 | if (shift >= bw) |
| 924 | return mkUInt(0, sort()); |
| 925 | return extract(bw-shift-1, 0).concat(mkUInt(0, shift)); |
| 926 | } |
| 927 | |
| 928 | return binop_fold(rhs, Z3_mk_bvshl); |
| 929 | } |
| 930 | |
| 931 | expr expr::ashr(const expr &rhs) const { |
| 932 | if (isZero() || rhs.isZero()) |