kdrag.reflect.nbe

kdrag.reflect.nbe(x: ExprRef) → ExprRef

Normalization by evaluation.

>>> nbe(smt.IntVal(41) + smt.IntVal(1))
42
>>> x,y = smt.Ints("x y")
>>> nbe(smt.Lambda([x], x + 1)[3])
4
>>> nbe(smt.Lambda([x], x + 1))
Lambda(x, x + 1)
>>> nbe(smt.Lambda([x], smt.IntVal(3) + 1))
Lambda(x, 3 + 1)

Parameters:

x (ExprRef)

Return type:

ExprRef