Class ModelRef

lean_py/z3/solver.py:510–541

Placeholder — Lean is a proof checker, not an SMT solver.

class ModelRef:
    """Placeholder — Lean is a proof checker, not an SMT solver."""

    def __getitem__(self, key: Any) -> Any:
        raise NotImplementedError(
            "Model extraction not supported: Lean cannot produce counter-models"
        )

    def eval(self, t: Any, model_completion: bool = False) -> Any:
        raise NotImplementedError(
            "Model extraction not supported: Lean cannot produce counter-models"
        )

    evaluate = eval

    def decls(self) -> list:
        return []

    def __len__(self) -> int:
        return 0

    def __contains__(self, key: Any) -> bool:
        return False

    def __iter__(self):
        return iter([])

    def sexpr(self) -> str:
        return "(model)"

    def __repr__(self) -> str:
        return "ModelRef(unsupported)"


class Solver: