Method params

lean_py/z3/core.py:361–374

Return parameters of this expression (e.g. bit-width for Extract).

(self)

        return _ast_repr(self._ast)

    def params(self) -> list:
        """Return parameters of this expression (e.g. bit-width for Extract)."""
        ast = self._ast
        if isinstance(ast, ExtractNode):
            return [ast.hi, ast.lo]
        if isinstance(ast, (ZeroExtNode, SignExtNode)):
            return [ast.bits]
        if isinstance(ast, Int2BvNode):
            return [ast.width]
        if isinstance(ast, BvLit):
            return [ast.width]
        if isinstance(ast, ReLoopNode):
            return [ast.lo, ast.hi]
        return []

    def translate(self, ctx: object) -> ExprRef:
        """Translate expression to another context (no-op — single context)."""