z3python: converting string to expression

Question

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

Halima

Answer 1

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

from z3 import *
x,y,z = Ints('x y 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 can't execute this script at http://rise4fun.com/z3py. The rise4fun website rejects Python scripts containing eval (for security reasons).

Swarey

Taking this one step further, if I don't have x,y,z declared ahead of time -- how would I automatically declare x,y,z ? assume I know all variables in 'x+y+2*z==5' are of type Int. – Halima

I was able to achieve variable declaration using exec, e.g., exec("x,y,z = Ints('x y z')"). I am wondering if there's better way to do so. exec/eval are dangerous operations in Python – Halima

Yes, eval is quite dangerous. The Z3 API only has parsers for SMT 2.0, SMT 1.0 and Z3 internal format. However, none of these formats are user friendly. For example, the SMT formats use s-expressions instead of the more natural infix notation. You can try one of the many parser generators available in Python. They will give you maximum flexibility. See this article: python.org/workshops/1998-11/proceedings/papers/aycock-little/… – Swarey