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

Function PbGe

lean_py/z3/core.py:2135–2141  ·  view source on GitHub ↗

Pseudo-boolean >=: sum of (coeff * bool) >= k.

(args: Sequence[tuple[BoolRef, int]], k: int)

Source from the content-addressed store, hash-verified

2133
2134
2135def PbGe(args: Sequence[tuple[BoolRef, int]], k: int) -> BoolRef:
2136 """Pseudo-boolean >=: sum of (coeff * bool) >= k."""
2137 if not args:
2138 return BoolVal(0 >= k)
2139 int_args = [_bool_to_int(b, c) for b, c in args]
2140 total = Sum(*int_args)
2141 return total >= k
2142
2143
2144# ---------------------------------------------------------------------------

Callers 1

test_pbgeMethod · 0.90

Calls 3

BoolValFunction · 0.85
_bool_to_intFunction · 0.85
SumFunction · 0.85

Tested by 1

test_pbgeMethod · 0.72