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

Function SignExt

lean_py/z3/core.py:1588–1598  ·  view source on GitHub ↗

Sign-extend a bit-vector by n bits.

(n: int, x: BitVecRef)

Source from the content-addressed store, hash-verified

1586
1587
1588def SignExt(n: int, x: BitVecRef) -> BitVecRef:
1589 """Sign-extend a bit-vector by n bits."""
1590 sort = x._sort
1591 if not isinstance(sort, BitVecSortRef):
1592 raise TypeError("SignExt requires BitVecRef")
1593 new_width = sort._width + n
1594 return BitVecRef(
1595 SignExtNode(new_width, x._ast),
1596 BitVecSort(new_width),
1597 x._vars,
1598 )
1599
1600
1601def BV2Int(x: BitVecRef, is_signed: bool = False) -> ArithRef:

Callers 11

_resolve_indexed_appMethod · 0.90
test_signextMethod · 0.90
test_signextMethod · 0.90
test_signext_positiveMethod · 0.90
test_signext_negativeMethod · 0.90
BVAddNoOverflowFunction · 0.85
BVAddNoUnderflowFunction · 0.85
BVSubNoOverflowFunction · 0.85
BVSubNoUnderflowFunction · 0.85
BVMulNoOverflowFunction · 0.85
BVMulNoUnderflowFunction · 0.85

Calls 3

SignExtNodeClass · 0.90
BitVecRefClass · 0.85
BitVecSortFunction · 0.85

Tested by 4

test_signextMethod · 0.72
test_signextMethod · 0.72
test_signext_positiveMethod · 0.72
test_signext_negativeMethod · 0.72