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

Method minimize

lean_py/z3/solver.py:822–825  ·  view source on GitHub ↗

Add minimization objective (returns handle index).

(self, expr: ExprRef)

Source from the content-addressed store, hash-verified

820 return len(self._objectives) - 1
821
822 def minimize(self, expr: ExprRef) -> int:
823 """Add minimization objective (returns handle index)."""
824 self._objectives.append(("min", expr))
825 return len(self._objectives) - 1
826
827 def check(self) -> CheckSatResult:
828 """Check satisfiability (always returns unknown for optimization)."""

Callers 1

test_minimizeMethod · 0.95

Calls

no outgoing calls

Tested by 1

test_minimizeMethod · 0.76