Dado que x,y,z = Ints('x y 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, entonces parece que tengo que hacer muchas operaciones de cadena para hacer la conversión.z3python: conversión de cadena a expresión
Puede usar la función Python eval. Aquí está un ejemplo:
from z3 import *
x,y,z = Ints('x y 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 las secuencias de comandos de Python que contienen eval (por razones de seguridad).
geat - gracias por la respuesta rápida Leonardo –
Dando un paso más, si no tengo 'x, y, z' declarado antes de tiempo, ¿cómo declararía automáticamente' x, y, z'? Supongo que sé que todas las variables en ''x + y + 2 * z == 5'' son de tipo' Int'. –
Pude lograr la declaración de variables usando 'exec', por ejemplo,' exec ("x, y, z = Ints ('x y z')") '. Me pregunto si hay mejor manera de hacerlo. 'exec/eval' son operaciones peligrosas en Python –