Python - Pass variable handle to evaluate

Question

I am writing some program using python and the z3py module.
What I am trying to do is the following: I extract a constraint of an if or a while statement from a function which is located in some other file. Additionally I extract the used variables in the statement as well as their types.
As I do not want to parse the constraint by hand into a z3py friendly form, I tried to use evaluate to do this for me. Therefore I used the tip of the following page: Z3 with string expressions
Now the problem is: I do not know how the variables in the constraint are called. But it seems as I have to name the handle of each variable like the actual variable. Otherwise evaluate won't find it. My code looks like this:

solver = Solver()
# Look up the constraint:
branch = bd.getBranchNum(0)
constr = branch.code
# Create handle for each variable, depending on its type:
for k in mapper.getVariables():
    var = mapper.getVariables()[k]
    if k in constr:
        if var.type == "intNum":
            Int(k)
        else:
            Real(k)
# Evaluate constraint, insert the result and solve it:
f = eval(constr)
solver.insert(f)
solve(f)

As you can see I saved the variables and constraints in classes. When executing this code I get the following error:

NameError: name 'real_x' is not defined

If I do not use the looping over the variables, but instead the following code, everything works fine:

solver = Solver()
branch = bd.getBranchNum(0)
constr = branch.code
print(constr)
real_x = Real('real_x')
int_y = Int('int_y')
f = eval(constr)
print(f)
solver.insert(f)
solve(f)

The problem is: I do not know, that the variables are called "real_x" or "int_y". Furthermore I do not know how many variables there are used, which means I have to use some dynamic thing like a loop.

Now my question is: Is there a way around this? What can I do to tell python that the handles already exist, but have a different name? Or is my approach completely wrong and I have to do something totally different?

Answer 1

This kind of thing is almost always a bad idea (see Why eval/exec is bad for more details), but "almost always" isn't "always", and it looks like you're using a library that was specifically designed to be used this way, in which case you've found one of the exceptions.

And at first glance, it seems like you've also hit one of the rare exceptions to the Keep data out of your variable names guideline (also see Why you don't want to dynamically create variables). But you haven't.

The only reason you need these variables like real_x to exist is so that eval can see them, right? But the eval function already knows how to look for variables in a dictionary instead of in your global namespace. And it looks like what you're getting back from mapper.getVariables() is a dictionary.

So, skip that whole messy loop, and just do this:

variables = mapper.getVariables()
f = eval(constr, globals=variables)

(In earlier versions of Python, globals is a positional-only argument, so just drop the globals= if you get an error about that.)

As the documentation explains, this gives the eval function access to your actual variables, plus the ones the mapper wants to generate, and it can do all kinds of unsafe things. If you want to prevent unsafe things, do this:

variables = dict(mapper.getVariables())
variables['__builtins__'] = {}
f = eval(constr, globals=variables)