Function PiecewiseLinearOrder

lean_py/z3/core.py:4382–4385

Declare a piecewise linear order relation.

(name: str, ctx: Context | None = None)

def PiecewiseLinearOrder(name: str, ctx: Context | None = None) -> FuncDeclRef:
    """Declare a piecewise linear order relation."""
    s = DeclareSort(name)
    return FuncDeclRef(f"{name}_le", (s, s), BoolSort())


def TransitiveClosure(f: FuncDeclRef) -> FuncDeclRef: