1

The installation problems pointed out in an earlier question are still present. I have tried to install Z3 4.3.0 and 4.1 under Windows XP SP3 32-bit and under Windows 7 64-bit. None of the combinations work! I am able to do the "from z3 import *", but the init() of the Z3 dll fails. My Python version is 2.7.3. Z3 stand-alone and Python stand-alone do work, but they don't work together without lots of complaints.

It would help to get an up-to-date installation recipe which answers the following questions:

Which Z3 download (source version, precompiled version) should be used?

Which Python version should be used?

Which or the various Z3 DLLs should be referenced in the init() call? An example would help (including raw string usage for paths with blanks).

Which Z3 Python source files should be used (some downloads of Z3 have *.py files, others have *.pyc files)? Are the compiled Python files compatible with more than one Python version?

How to set PATH and PYTHONPATH?

How to call the IDLE shell of Python in such a way that Z3 initialization is provided automatically?

Sorry, if this should sound like a newbie question, but ...

Community
  • 1
  • 1
Axel Kemper
  • 10,544
  • 2
  • 31
  • 54

2 Answers2

6

Christoph's answer is correct. Thank you!

Here are some more details which could help others. (make sure to adjust the path accordingly)

The modified idle.bat script of Python 2.7.3 (64-bit):

@echo off
rem Start IDLE using the appropriate Python interpreter
setlocal
set PATH=%PATH%;X:\my\Programme\z3-4.3.0-x64\bin
set PYTHONPATH=X:\my\Programme\z3-4.3.0-x64\bin
set CURRDIR=%~dp0
start "IDLE" "%CURRDIR%..\..\pythonw.exe" "%CURRDIR%idle.pyw" %1 %2 %3 %4 %5 %6 %7 %8 %9
endlocal

The z3 path has to be in PATH and in PYTHONPATH.

The first two statements in the Python/Idle shell:

from z3 import *
init(r"X:\my\Programme\z3-4.3.0-x64\bin\libz3.dll")

(note the 'r' which indicates a raw string with backslashes treated as normal characters)

Axel Kemper
  • 10,544
  • 2
  • 31
  • 54
1

Windows XP does not support thread-local storage in DLLs, which Z3 requires. We're currently working on a fix for that, but in any case it will mean that you would have to compile your own DLL even when it's fixed.

On Windows 7, it should work out of the box. However, you need to make sure that either everything or nothing is compiled for 64-bit. If you're using a 32-bit python version, it will not be able to load a 64-bit DLL and vice versa. At Python.org there are two downloads, one of them labeled X86-64, which is the 64-bit version.

Finally, the directory where libz3.dll and *.pyc/py are located needs to be added to PYTHONPATH. You can set this system-wide (Control Panel, System, Advanced System Settings, Advanced, Environment Variables), then IDLE should see it too.

Christoph Wintersteiger
  • 8,234
  • 1
  • 16
  • 30