kdrag.reflect.reflect_expr_string

kdrag.reflect.reflect_expr_string(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.

>>> reflect_expr_string("x + 1", globals={"x": smt.Int("x")})
x + 1
>>> x = smt.Int("x")
>>> f = smt.Function("f", smt.IntSort(), smt.IntSort())
>>> reflect_expr_string("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