kdrag.utils.ite_to_cases

kdrag.utils.ite_to_cases(e: ExprRef) tuple[list[tuple[BoolRef, ExprRef]], ExprRef]

Convert nested if then elses into a list of cases and a default.

>>> x = smt.Int("x")
>>> ite_to_cases(smt.If(x > 0, x, smt.If(x == 0, smt.IntVal(0), -x)))
([(x > 0, x), (x == 0, 0)], -x)
Parameters:

e (ExprRef)

Return type:

tuple[list[tuple[BoolRef, ExprRef]], ExprRef]