| 1109 | } |
| 1110 | |
| 1111 | expr expr::ctpop() const { |
| 1112 | C(); |
| 1113 | auto nbits = bits(); |
| 1114 | |
| 1115 | auto res = mkUInt(0, sort()); |
| 1116 | for (unsigned i = 0; i < nbits; ++i) { |
| 1117 | res = res + extract(i, i).zext(nbits - 1); |
| 1118 | } |
| 1119 | |
| 1120 | return res; |
| 1121 | } |
| 1122 | |
| 1123 | expr expr::umin(const expr &rhs) const { |
| 1124 | return mkIf(ule(rhs), *this, rhs); |