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

Function Extract

lean_py/z3/core.py:1546–1553  ·  view source on GitHub ↗

Extract bits [hi:lo] from a bit-vector.

(hi: int, lo: int, x: BitVecRef)

Source from the content-addressed store, hash-verified

1544
1545
1546def Extract(hi: int, lo: int, x: BitVecRef) -> BitVecRef:
1547 """Extract bits [hi:lo] from a bit-vector."""
1548 width = hi - lo + 1
1549 return BitVecRef(
1550 ExtractNode(hi, lo, x._ast),
1551 BitVecSort(width),
1552 x._vars,
1553 )
1554
1555
1556def Concat(*args: BitVecRef) -> BitVecRef:

Callers 9

_resolve_indexed_appMethod · 0.90
test_extractMethod · 0.90
test_extract_paramsMethod · 0.90
test_extractMethod · 0.90
BVRedAndFunction · 0.85
BVRedOrFunction · 0.85

Calls 3

ExtractNodeClass · 0.90
BitVecRefClass · 0.85
BitVecSortFunction · 0.85

Tested by 6

test_extractMethod · 0.72
test_extract_paramsMethod · 0.72
test_extractMethod · 0.72