kdrag.trans

kdrag.trans(step: FuncDeclRef) → FuncDeclRef

The transitive closure of a step function. Takes a function of type State -> State and returns a function of type Int, State -> State where the first argument is the number of steps to take.

>>> hr = smt.Int("hr")
>>> clk_step = define("clk_step", [hr], smt.If(hr == 12, 1, hr + 1))
>>> clk_trans = trans(clk_step)
>>> full_simp(clk_trans(4, 1))
5
>>> full_simp(clk_trans(12, 1))
1
>>> full_simp(clk_trans(-3, 42)) # stutters on negative steps
42

Parameters:

step (FuncDeclRef)

Return type:

FuncDeclRef