Class Tactic

lean_py/z3/tactic.py:77–107

A named tactic that dispatches to Pantograph.

class Tactic:
    """A named tactic that dispatches to Pantograph."""

    __slots__ = ("_name",)

    def __init__(self, name: str) -> None:
        self._name = name

    def apply(self, goal: Goal) -> ApplyResult:
        """Apply this tactic to a goal via Pantograph."""
        expr = goal.as_expr()
        k = _get_kernel()
        lib = k._lib

        ast = _wrap_free_vars(expr)
        z3_expr = _marshal_expr(lib, ast)
        lean_expr = lib.z3_compile(z3_expr)
        gs = k.goal_create_expr(lean_expr)

        result = gs.try_tactic(self._name)
        if result.ok and result.state is not None and result.state.is_solved():
            return ApplyResult([])  # proved
        # Tactic produced subgoals or failed
        return ApplyResult([goal])  # unchanged

    def solver(self):
        """Create a Solver that uses this tactic."""
        return Solver()

    def __repr__(self) -> str:
        return f"Tactic({self._name})"


# ---------------------------------------------------------------------------