Method sexpr

lean_py/z3/solver.py:622–627

Return S-expression representation of assertions.

(self)

        return {}

    def sexpr(self) -> str:
        """Return S-expression representation of assertions."""
        if not self._assertions:
            return "()"
        parts = [_ast_repr(a._ast) for a in self._assertions]
        return "(" + " ".join(parts) + ")"

    def to_smt2(self) -> str:
        """Return SMT-LIB2 representation (approximate)."""