Z3python: convert string to expression

Question

Given that x,y,z = Ints('xy z') and a string like s='x + y + 2*z = 5' , is there a quick way to convert s to expression z3? If this is not possible, it seems to me that I have to do many string operations for conversion.

Answer 1

You can use the Python function eval . Here is an example:

 from z3 import * x,y,z = Ints('xy z') s = 'x + y + 2*z == 5' F = eval(s) solve(F) 

This script displays [y = 0, z = 0, x = 5] on my machine.

Unfortunately, we cannot execute this script at http://rise4fun.com/z3py . The rise4fun site rejects Python scripts containing eval (for security reasons).