Cannot import z3 in Python

[wenting-zhao]

Hi,

(This is an error on macOS Sierra, and I'm running Python 2.7.10)

When I tried importing the z3 package, I got this error:

Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "z3.py", line 46, in <module>
    from . import z3core
ValueError: Attempted relative import in non-package

A quick search on Google tells me that relative imports don't work in this case, and so I fixed this issue by adding the absolute path to where z3.py is stored:

import sys
sys.path.append(path.dirname(path.dirname(path.abspath(__file__))))

However, it seems like all files are doing relative imports, and adding the above piece of code in every file doesn't sound like a solution. Does anyone run into this as well? Might there be a fix?

Thanks!

[NikolajBjorner]

@delcypher there's got to be something basic?

[johscheuer]

@wenting-zhao I thing the easiest way to import the z3 package is by installing z3 via pip install z3-solver then you can import the module with from z3 import z3core. If you compile your own version of Z3 read this part of the Readme.

[delcypher]

@wenting-zhao @NikolajBjorner Thanks to the work of @rhelmot z3.py does live in a package so I find this error message confusing.

The directory z3 (which containsz3.py) should be a package because it contains an __init__.py file. @wenting-zhao you haven't said anything about how you built Z3 (e.g. which build system) and whether you're trying to use the Z3 python bindings from the build directory or from an installed location. Where ever you are consuming the bindings from you should check that __init__.py exists in the z3 directory. If it doesn't you're likely doing something wrong. Without more detail I can't tell you what.

[wenting-zhao]

This is very much appreciated. It's been a while, so I don't remember what happened there exactly. I think I didn't build it properly, but somehow z3 did get installed under the python-2.7/site-packages directory.
This is fixed by installing the package by running pip install z3-solver. For python3, I ran python3.5 -m pip install z3-solver. So I thought it may be worth adding this instruction in README, as building through pip largely reduces potential installing errors.
Again, thanks very much!

[hectorpla]

Hi Everyone,

I simply ran python3.4 -m pip install z3-solver to install z3 and tried to import z3, the following error prompted:

>>> import z3 Traceback (most recent call last): File "<stdin>", line 1, in <module> File "/Library/Frameworks/Python.framework/Versions/3.4/lib/python3.4/site-packages/z3/z3.py", line 44, in <module> from . import z3core SystemError: Parent module '' not loaded, cannot perform relative import

If I import z3 in python 2.7, ValueError: Attempted relative import in non-package error will come up.

Best

[rhelmot]

It strikes me as incredibly likely that there are some macOS specific packaging bugs in the Python distribution. I have never been able to test the setup on macOS, nor do I have the ability to.

[johscheuer]

@hectorpla you have to do from z3 import z3core not from . import z3core.

[rhelmot]

That's not the problem. The from . import z3core line is in the z3 bindings.

[wintersteiger]

Yes, those relative imports are in the API. I have a sneaking suspicion that this is also the root cause of some of our doctests not working on some platforms, under some configurations, and some versions of python (I haven't seen a pattern yet). @rhelmot: git blames you for these lines of code; do you remember what made this change necessary?

[wenting-zhao]

@rhelmot I wouldn't be surprised if there are some macOS specific packaging bugs in the Python distribution. This happens quite often every time I upgrade my system (macOS Sierra is new). I'd be happy to look at it more and test the setup on macOS if I can steadily produce the bug. However, everything seems to be very well-fixed after I cleaned and rebuilt it.

@hectorpla which version of Mac OS are you running? How did you build z3 for python2, exactly? Did you run pip install z3-solver or python2.7 -m pip install z3-solver? There seems to be a slight difference between the two in my case.

[hectorpla]

@wenting-zhao I am running on Yosmite 10.10.5 and I installed z3 by the command python3 -m pip3 install z3-solver, which is not much different from command pip3 install z3 with --prefix, --pypkgdir and ---python specified.

[hectorpla]

Finally I successfully import z3. It failed because I accidentally added the z3 directory to python's system path. Thanks.