kdrag.reflect.eval_

kdrag.reflect.eval_(e: ~z3.z3.ExprRef, globals={}, locals={}, default=<function __default_error>)

Evaluate a z3 expression in a given environment. The analog of python’s eval.

>>> eval_(smt.IntVal(42))
42
>>> eval_(smt.IntVal(1) + smt.IntVal(2))
3
>>> x = smt.Int("x")
>>> eval_(smt.Lambda([x], x + 1)[3])
4
>>> R = kd.Struct("R", ("x", kd.Z), ("y", smt.BoolSort()))
>>> eval_(R(42, True).x)
42
>>> eval_(R(42,True).is_R)
True

Parameters:

e (ExprRef)