Optimization solver. Lean is a proof checker, not an optimization solver, so optimization queries return ``unknown``. Programs that build Optimize expressions will work; solving requires an SMT backend.
| 799 | |
| 800 | |
| 801 | class Optimize: |
| 802 | """Optimization solver. |
| 803 | |
| 804 | Lean is a proof checker, not an optimization solver, so optimization |
| 805 | queries return ``unknown``. Programs that build Optimize expressions |
| 806 | will work; solving requires an SMT backend. |
| 807 | """ |
| 808 | |
| 809 | def __init__(self) -> None: |
| 810 | self._assertions: list[BoolRef] = [] |
| 811 | self._objectives: list[tuple[str, ExprRef]] = [] |
| 812 | |
| 813 | def add(self, *args: BoolRef) -> None: |
| 814 | for a in args: |
| 815 | self._assertions.append(a) |
| 816 | |
| 817 | def maximize(self, expr: ExprRef) -> int: |
| 818 | """Add maximization objective (returns handle index).""" |
| 819 | self._objectives.append(("max", expr)) |
| 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).""" |
| 829 | return unknown |
| 830 | |
| 831 | def model(self) -> ModelRef: |
| 832 | raise NotImplementedError( |
| 833 | "Model extraction not supported: Lean is a proof checker, not an optimization solver" |
| 834 | ) |
| 835 | |
| 836 | def push(self) -> None: |
| 837 | pass |
| 838 | |
| 839 | def pop(self) -> None: |
| 840 | pass |
| 841 | |
| 842 | def assertions(self) -> list[BoolRef]: |
| 843 | return list(self._assertions) |
| 844 | |
| 845 | def objectives(self) -> list[tuple[str, ExprRef]]: |
| 846 | return list(self._objectives) |
| 847 | |
| 848 | def assert_soft(self, expr: BoolRef, weight: Any = None, id: Any = None) -> int: |
| 849 | """Add a soft constraint with optional weight and group id.""" |
| 850 | self._assertions.append(expr) |
| 851 | return len(self._assertions) - 1 |
| 852 | |
| 853 | def set(self, *args: Any, **keys: Any) -> None: |
| 854 | pass |
| 855 | |
| 856 | def __repr__(self) -> str: |
| 857 | return f"Optimize({len(self._assertions)} assertions, {len(self._objectives)} objectives)" |
| 858 |
no outgoing calls