kdrag.reflect.expr

kdrag.reflect.expr(expr: str, globals=None, locals=None) → ExprRef

Turn a string of a python expression into a z3 expressions. Globals are inferred to be current scope if not given.

>>> expr("x + 1", globals={"x": smt.Int("x")})
x + 1
>>> x = smt.Int("x")
>>> f = smt.Function("f", smt.IntSort(), smt.IntSort())
>>> expr("f(x) + 1 if 0 < x < 5 < 7 else x * x")
If(And(0 < x, 5 > x, 5 < 7), f(x) + 1, x*x)

Parameters:

expr (str)

Return type:

ExprRef