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

Function RepeatBitVec

lean_py/z3/core.py:1919–1926  ·  view source on GitHub ↗

Repeat a bit-vector n times by concatenation.

(n: int, a: BitVecRef)

Source from the content-addressed store, hash-verified

1917
1918
1919def RepeatBitVec(n: int, a: BitVecRef) -> BitVecRef:
1920 """Repeat a bit-vector n times by concatenation."""
1921 if n < 1:
1922 raise TypeError("RepeatBitVec requires n >= 1")
1923 result = a
1924 for _ in range(n - 1):
1925 result = Concat(result, a)
1926 return result
1927
1928
1929def BVRedAnd(a: BitVecRef) -> BitVecRef:

Callers 4

_resolve_indexed_appMethod · 0.90
test_repeat_bitvecMethod · 0.90

Calls 1

ConcatFunction · 0.85

Tested by 3

test_repeat_bitvecMethod · 0.72