9

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.

Leonardo de Moura
  • 21,065
  • 2
  • 47
  • 53
Vu Nguyen
  • 987
  • 1
  • 9
  • 20

1 Answers1

10

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).

Leonardo de Moura
  • 21,065
  • 2
  • 47
  • 53
  • 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`. – Vu Nguyen Sep 22 '12 at 05:32
  • 1
    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 – Vu Nguyen Sep 22 '12 at 05:44
  • 1
    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: http://www.python.org/workshops/1998-11/proceedings/papers/aycock-little/aycock-little.ps – Leonardo de Moura Sep 22 '12 at 14:56