Convert a bit-vector to an integer. If is_signed is False (default, matching z3), uses unsigned (toNat). If is_signed is True, uses signed (toInt).
(x: BitVecRef, is_signed: bool = False)
| 1599 | |
| 1600 | |
| 1601 | def BV2Int(x: BitVecRef, is_signed: bool = False) -> ArithRef: |
| 1602 | """Convert a bit-vector to an integer. |
| 1603 | |
| 1604 | If is_signed is False (default, matching z3), uses unsigned (toNat). |
| 1605 | If is_signed is True, uses signed (toInt). |
| 1606 | """ |
| 1607 | op = UnOp.BV2INT if is_signed else UnOp.BV2NAT |
| 1608 | return ArithRef( |
| 1609 | UnOpNode(op, x._ast), |
| 1610 | IntSort(), |
| 1611 | x._vars, |
| 1612 | ) |
| 1613 | |
| 1614 | |
| 1615 | def Int2BV(x: ArithRef, n: int) -> BitVecRef: |