Class Solver

lean_py/z3/solver.py:544–722

z3py-compatible solver interface. ``check()`` builds the conjunction of all assertions, negates it, and tries to prove the negation via grind. If proved, returns ``unsat`` (the constraints are contradictory). Otherwise ``unknown``.

class Solver:
    """z3py-compatible solver interface.

    ``check()`` builds the conjunction of all assertions, negates it,
    and tries to prove the negation via grind.  If proved, returns
    ``unsat`` (the constraints are contradictory).  Otherwise ``unknown``.
    """

    def __init__(self) -> None:
        self._assertions: list[BoolRef] = []
        self._stack: list[int] = []

    def add(self, *args: BoolRef) -> None:
        for a in args:
            self._assertions.append(a)

    # Aliases for add
    append = add
    insert = add

    def set(self, *args: Any, **keys: Any) -> None:
        """Set solver options (no-op — Lean solver has no tunable parameters)."""
        pass

    def push(self) -> None:
        self._stack.append(len(self._assertions))

    def pop(self, n: int = 1) -> None:
        for _ in range(n):
            if not self._stack:
                raise IndexError("pop from empty solver stack")
            self._assertions = self._assertions[: self._stack.pop()]

    def num_scopes(self) -> int:
        """Return number of push scopes."""
        return len(self._stack)

    def check(self, *assumptions: BoolRef) -> CheckSatResult:
        asserts = list(self._assertions)
        asserts.extend(assumptions)
        if not asserts:
            return sat
        conj = And(*asserts)
        # Try proving negation → unsat
        negated = Not(conj)
        if _try_prove(negated):
            return unsat
        # Try proving conjunction directly → sat (tautologically true)
        if _try_prove(conj):
            return sat
        return unknown

    def model(self) -> ModelRef:
        raise NotImplementedError(
            "Model extraction not supported: Lean is a proof checker, not an SMT solver"
        )

    def assertions(self) -> list[BoolRef]: