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

Function BitVec

lean_py/z3/core.py:1084–1086  ·  view source on GitHub ↗
(name: str, width: int)

Source from the content-addressed store, hash-verified

1082
1083
1084def BitVec(name: str, width: int) -> BitVecRef:
1085 s = BitVecSort(width)
1086 return BitVecRef(_AstVar(name), s, frozenset([(name, s._ast_sort)]))
1087
1088
1089def BitVecs(names: str, width: int) -> tuple[BitVecRef, ...]:

Callers 15

test_bv_arithmeticMethod · 0.90
test_bv_xor_self_is_zeroMethod · 0.90
test_bv_and_selfMethod · 0.90
test_bv_or_selfMethod · 0.90
test_bv_not_notMethod · 0.90
test_bv_add_zeroMethod · 0.90
test_bv_sub_selfMethod · 0.90
test_shift_left_rightMethod · 0.90
test_rotate_left_right_inverseMethod · 0.90
test_sdiv_by_oneMethod · 0.90
test_concat_extract_roundtripMethod · 0.90
test_bv_negate_is_complement_plus_oneMethod · 0.90

Calls 2

BitVecSortFunction · 0.85
BitVecRefClass · 0.85

Tested by 15

test_bv_arithmeticMethod · 0.72
test_bv_xor_self_is_zeroMethod · 0.72
test_bv_and_selfMethod · 0.72
test_bv_or_selfMethod · 0.72
test_bv_not_notMethod · 0.72
test_bv_add_zeroMethod · 0.72
test_bv_sub_selfMethod · 0.72
test_shift_left_rightMethod · 0.72
test_rotate_left_right_inverseMethod · 0.72
test_sdiv_by_oneMethod · 0.72
test_concat_extract_roundtripMethod · 0.72
test_bv_negate_is_complement_plus_oneMethod · 0.72