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
6
A
Respuesta
6
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).
Cuestiones relacionadas
- 1. conversión de cadena estrecha a cadena ancha
- 2. Conversión de expresión <T, bool> en la cadena
- 3. conversión de cadena a numérico
- 4. Conversión de cadena a entero
- 5. Conversión de la cadena de entrada del usuario a la expresión regular
- 6. Conversión de archivo binario a cadena Base64
- 7. Conversión de cadena binaria a ASCII correspondiente
- 8. conversión de cadena a largo en pitón
- 9. C#: Conversión de cadena a Sbyte *
- 10. Cadena de conversión Sqlite a la fecha
- 11. Conversión de la cadena Haml a html
- 12. Ruby - Conversión de entero a cadena
- 13. Conversión de Unicode a cadena en Java
- 14. Conversión de PDF a la cadena
- 15. Hex a cadena de conversión ascii
- 16. Conversión de cadena a puntero para JNA
- 17. conversión de bytes a una cadena C#
- 18. conversión de XML a cadena usando C#
- 19. Java: inetaddress a la conversión de cadena
- 20. cacao - conversión de un doble a cadena
- 21. cadena de conversión a long long
- 22. Ruby - cadena de conversión a la fecha
- 23. C# cadena de conversión explícita a ENUM
- 24. Conversión de doble a cadena en C++
- 25. Conversión de una cadena a DateTime
- 26. Conversión de un vector a cadena
- 27. Cadena de C++ a doble conversión
- 28. conversión de expresión lambda en un árbol de expresión
- 29. expresión de cadena C# convert a una expresión booleana
- 30. cadena a cadena de matriz de conversión en Java
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 –