Function _fp_op

lean_py/z3/core.py:3341–3350

(name: str, *args: ExprRef)

def _fp_op(name: str, *args: ExprRef) -> FPRef:
    # Filter out rounding mode args — we only support RNE
    real_args = [a for a in args if not isinstance(a, FPRMRef)]
    fp_args = [a for a in real_args if isinstance(a, FPRef)]
    sort = fp_args[0]._sort if fp_args else FPSort(11, 53)
    merged: frozenset[tuple[str, ASTSort]] = frozenset()
    for a in real_args:
        if isinstance(a, ExprRef):
            merged = merged | a._vars
    return FPRef(FpOpNode(name, tuple(a._ast for a in real_args)), sort, merged)


def _fp_pred(name: str, *args: ExprRef) -> BoolRef: