CODEWITHSUNDEEP
pythonz3z3py
zell
zell

Reputation: 10204

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.

Upvotes: 1

Views: 428

Answers (2)

Netwave
Netwave

Reputation: 42716

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.

Upvotes: 2

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

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.

Upvotes: 0

Related Questions