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

Function AtMost

lean_py/z3/core.py:2097–2104  ·  view source on GitHub ↗

At most k of the boolean args are true.

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

Source from the content-addressed store, hash-verified

2095
2096
2097def AtMost(args: Sequence[BoolRef], k: int) -> BoolRef:
2098 """At most k of the boolean args are true."""
2099 exprs = list(args)
2100 if not exprs:
2101 return BoolVal(True)
2102 int_args = [_bool_to_int(b) for b in exprs]
2103 total = Sum(*int_args)
2104 return total <= k
2105
2106
2107def AtLeast(args: Sequence[BoolRef], k: int) -> BoolRef:

Callers 3

test_atmostMethod · 0.90
test_atmost_emptyMethod · 0.90
test_atmost_unsatMethod · 0.90

Calls 3

BoolValFunction · 0.85
_bool_to_intFunction · 0.85
SumFunction · 0.85

Tested by 3

test_atmostMethod · 0.72
test_atmost_emptyMethod · 0.72
test_atmost_unsatMethod · 0.72