kdrag.termination.search_wf

kdrag.termination.search_wf(head: list[~z3.z3.ExprRef], calls: list[tuple[~z3.z3.BoolRef, list[~z3.z3.ExprRef]]], measure=<function default_measure>) → tuple[int, ...]

Find a permutation that makes every head greater than every call.

>>> x, y = smt.Consts("x y", kd.Nat)
>>> search_wf([x, y], [(x.is_S, [x.pred, y])])
(0, 1)
>>> search_wf([x, y], [(y.is_S, [x, y.pred])])
(0, 1)
>>> search_wf([x, y], [(y.is_S, [kd.Nat.S(x), y.pred])])
(1, 0)

Parameters:

head (list[ExprRef])
calls (list[tuple[BoolRef, list[ExprRef]]])

Return type:

tuple[int, …]