z3python: convirtiendo cadena a expresión

Dado que x,y,z = Ints('xy z') y una cadena como s='x + y + 2*z = 5' , ¿hay una forma rápida de convertir s en una expresión z3? Si no es posible, parece que tengo que hacer muchas operaciones de cadena para hacer la conversión.

Puedes usar la función eval Python. Aquí hay un ejemplo:

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

Este script muestra [y = 0, z = 0, x = 5] en mi máquina.

Desafortunadamente, no podemos ejecutar este script en http://rise4fun.com/z3py . El sitio web rise4fun rechaza los scripts de Python que contienen eval (por razones de seguridad).