kdrag.modal.PIf

kdrag.modal.PIf(c, t: ExprRef, e: ExprRef) → ExprRef

Pointwise if-then-else rather than on the nose if-then-else.

>>> x = smt.Int("x")
>>> PointIf(smt.Lambda([x], x > 0), 1, -1)
Lambda(x0!..., If(x0!... > 0, 1, -1))
>>> PointIf(smt.Lambda([x], x > 0), smt.Lambda([x], x+1), -1)
Lambda(x0!..., If(x0!... > 0, x0!... + 1, -1))

Parameters:

• t (ExprRef)

• e (ExprRef)

Return type:

ExprRef