MCPcopy Create free account
hub / github.com/BasisResearch/lean.py / ZeroExt

Function ZeroExt

lean_py/z3/core.py:1575–1585  ·  view source on GitHub ↗

Zero-extend a bit-vector by n bits.

(n: int, x: BitVecRef)

Source from the content-addressed store, hash-verified

1573
1574
1575def ZeroExt(n: int, x: BitVecRef) -> BitVecRef:
1576 """Zero-extend a bit-vector by n bits."""
1577 sort = x._sort
1578 if not isinstance(sort, BitVecSortRef):
1579 raise TypeError("ZeroExt requires BitVecRef")
1580 new_width = sort._width + n
1581 return BitVecRef(
1582 ZeroExtNode(new_width, x._ast),
1583 BitVecSort(new_width),
1584 x._vars,
1585 )
1586
1587
1588def SignExt(n: int, x: BitVecRef) -> BitVecRef:

Callers 9

_resolve_indexed_appMethod · 0.90
test_bv_zero_extendMethod · 0.90
test_zeroextMethod · 0.90
test_zeroext_paramsMethod · 0.90
test_zeroextMethod · 0.90
test_zeroext_valueMethod · 0.90
BVAddNoOverflowFunction · 0.85
BVMulNoOverflowFunction · 0.85

Calls 3

ZeroExtNodeClass · 0.90
BitVecRefClass · 0.85
BitVecSortFunction · 0.85

Tested by 6

test_bv_zero_extendMethod · 0.72
test_zeroextMethod · 0.72
test_zeroext_paramsMethod · 0.72
test_zeroextMethod · 0.72
test_zeroext_valueMethod · 0.72