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

Function IntVector

lean_py/z3/core.py:1727–1729  ·  view source on GitHub ↗

Create a vector of ``sz`` integer variables named prefix__0, ..., prefix__sz-1.

(prefix: str, sz: int)

Source from the content-addressed store, hash-verified

1725
1726
1727def IntVector(prefix: str, sz: int) -> list[ArithRef]:
1728 """Create a vector of ``sz`` integer variables named prefix__0, ..., prefix__sz-1."""
1729 return [Int(f"{prefix}__{i}") for i in range(sz)]
1730
1731
1732def BoolVector(prefix: str, sz: int) -> list[BoolRef]:

Callers 4

test_int_vectorMethod · 0.90
test_vector_namesMethod · 0.90
test_vector_zeroMethod · 0.90
test_vector_sumMethod · 0.90

Calls 1

IntFunction · 0.85

Tested by 4

test_int_vectorMethod · 0.72
test_vector_namesMethod · 0.72
test_vector_zeroMethod · 0.72
test_vector_sumMethod · 0.72