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

Function Int2BV

lean_py/z3/core.py:1615–1621  ·  view source on GitHub ↗

Convert an integer to a bit-vector of width n.

(x: ArithRef, n: int)

Source from the content-addressed store, hash-verified

1613
1614
1615def Int2BV(x: ArithRef, n: int) -> BitVecRef:
1616 """Convert an integer to a bit-vector of width n."""
1617 return BitVecRef(
1618 Int2BvNode(n, x._ast),
1619 BitVecSort(n),
1620 x._vars,
1621 )
1622
1623
1624def RotateLeft(a: BitVecRef, b: BitVecRef | int) -> BitVecRef:

Callers 4

_resolve_indexed_appMethod · 0.90
test_int2bvMethod · 0.90
test_int2bvMethod · 0.90

Calls 3

Int2BvNodeClass · 0.90
BitVecRefClass · 0.85
BitVecSortFunction · 0.85

Tested by 3

test_int2bvMethod · 0.72
test_int2bvMethod · 0.72