# How to transform a arithmetic expression to a Python arithmetic function?

Suppose I have a arithmetic comparison in Z3. Following the syntax of Z3py, this is:

e=z3.Int('x') <=3

Is there an easy way (rather than a tedious, case-by-case parsing process) to transform the Z3 expression (expressed in Z3py) to a Python function, say:

def e(x): return x<=3

? Thanks.

## Answers

I do not really know about z3 specifically but you can try something like this example:

import operator from functools import partial f_dict = {"e"+str(i):f for i,f in enumerate([partial(op, n) for n in range(10) for op in [operator.lt ,operator.le , operator.eq]])} locals().update(f_dict)

Here I'm automating the creation of functions, and combinations to numbers from 0 to 9 and compare another number if is less than, less equal or equal. Lets split it in concepts:

List of operators to use

[operator.lt ,operator.le , operator.eq]

Generic function binded to a name, which takes a number and uses the operators and the numbers of the comprehension:

lambda x: op(x, n)

Then we just have to bind them to a name in a dictionary (dict comprehension) and make the local dict be updated with it.

locals().update(f_dict)

Working on console:

>>> import operator f_dict = {"e"+str(i):f for i,f in enumerate([lambda x: op(x, n) for n in range(10) for op in [operator.lt ,operator.le , operator.eq]])} locals().update(f_dict) >>> e1(3) False

This functions should work even with the z3 objects if they are properly lifted to be used with the operators.

We don't expose any reflection facilities (either from python to Z3 or the other way) so you would have to walk expressions and determine how to reflect them of you want to produce native python.

Alternatively, you could use the simplifier exposed by Z3 to evaluate expressions. So if you have values for the free variables in a formula, then you use the substitute function (also exposed over Python) to replace them by the values, then call the simplify() method and then retrieve the python values.