z3py examples do not to work on macOS

3
votes

I can not get any of the z3py examples to work. I was able to install it successful using the instructions from the README on github. I successfully updated my python path to point to the appropriate directory. Furthermore, I was able to successfully import z3, but I get an error every time I declare a variable. The compiler does not recognize Int, Ints, Real , RealVal.

I have included an example to illustrate.

Code:

from z3 import *
x = Int('x')
y = Int('y')
solve(x > 2, y < 10, x + 2*y == 7)

Error: Traceback (most recent call last): File "test.py", line 3, in x = Int('x') NameError: name 'Int' is not defined

I would really appreciate any help. Thank you so much.

1
pythonz3z3py
What does dir() show you after from z3 import * ? Have you instead tried import z3; x = z3.Int('x') ? - nekomatic
@nekomantic: Thanks for your response. Here are the answers: from z3 import * dir() >>>['__builtins__', '__doc__', '__name__', '__package__'] >>> x = Int('x') Traceback (most recent call last): File "<stdin>", line 1, in <module> NameError: name 'Int' is not defined >>> import z3 >>> x = Int('x') Traceback (most recent call last): File "<stdin>", line 1, in <module> NameError: name 'Int' is not defined - Akanksha Vyas
After you import a module it should appear in the result of dir(), so I would check whether you've installed z3 properly. - nekomatic
Please read my suggestion carefully: if you have done import z3 then try x = z3.Int('x'), and so on. - nekomatic
Do you have z3.py in your working dir? It shadows installed package. - Łukasz Rogalski

1 Answers

0
votes

There is something wrong with your local installation, either of Python or Z3.

I just compiled Z3 on my Mac and ran the example test.py you provided with no problems. I'm using OS X 10.9.5 with Python 2.7.11 and the current master version of Z3 (commit 41edf5f). The exact instructions I used were:

git clone https://github.com/Z3Prover/z3.git
cd z3
./configure
cd build
make -j4
emacs test.py
# Write in the example you gave.
python ./test.py

The output I got was [y = 0, x = 7], which is the same output that I got from your script on my Linux box. So the problem is specific to your OS X machine or build procedure.