Function _fp_pred

lean_py/z3/core.py:3353–3359

(name: str, *args: ExprRef)

def _fp_pred(name: str, *args: ExprRef) -> BoolRef:
    real_args = [a for a in args if not isinstance(a, FPRMRef)]
    merged: frozenset[tuple[str, ASTSort]] = frozenset()
    for a in real_args:
        if isinstance(a, ExprRef):
            merged = merged | a._vars
    return BoolRef(FpOpNode(name, tuple(a._ast for a in real_args)), merged)


# FP arithmetic