Windows環境でPythonのz3pyを導入する

本日は

数独のソルバーで必要だったz3をWindows上でPythonから使うようにします．

できなかったこと

pipで導入

importはできるのにそこからモジュールのクラスにアクセスすると実行エラーになります．

> pip install z3

conda install ... で行けるかな？

探してると一応ある．．．https://anaconda.org/asmeurer/z3
上記のサイトの呪文通り試すもPackageNotFoundErrorで怒られる．

> conda install -c asmeurer z3 

Macと同様に

> conda install z3-solver

を試してもビルドで失敗．Windows ダメなんじゃないかな．

解決策

Wikiを見る

https://github.com/Z3Prover/z3/wiki/Using-Z3Py-on-Windows
のページにジャンプしてInstalling Z3Py with pre-compiled Windows binariesの案内にに従います．Download the latest pre-compile binariesのリリースのページまで行きましょう：
https://github.com/Z3Prover/bin/tree/master/releases

例えば z3-4.5.0-x64-win.zip をダウンロードします．解凍して
bin/python の中身にあるexapmle.pyの中身を見てみましょう：

example.py

# Copyright (c) Microsoft Corporation 2015, 2016

# The Z3 Python API requires libz3.dll/.so/.dylib in the 
# PATH/LD_LIBRARY_PATH/DYLD_LIBRARY_PATH
# environment variable and the PYTHON_PATH environment variable
# needs to point to the `python' directory that contains `z3/z3.py'
# (which is at bin/python in our binary releases).

# If you obtained example.py as part of our binary release zip files,
# which you unzipped into a directory called `MYZ3', then follow these
# instructions to run the example:

# Running this example on Windows:
# set PATH=%PATH%;MYZ3\bin
# set PYTHONPATH=MYZ3\bin\python
# python example.py

# Running this example on Linux:
# export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:MYZ3/bin
# export PYTHONPATH=MYZ3/bin/python
# python example.py

# Running this example on OSX:
# export DYLD_LIBRARY_PATH=$DYLD_LIBRARY_PATH:MYZ3/bin
# export PYTHONPATH=MYZ3/bin/python
# python example.py


from z3 import *

x = Real('x')
y = Real('y')
s = Solver()
s.add(x + y > 5, x > 1, y > 1)
print(s.check())
print(s.model())

環境整備

通常

上のexample.pyのコメントに従えば，とりあえず bin に入っている
libz3.dll をPathが通っているところに配置すること，bin/python/z3 を各自のPython環境のsite-package内に配置することでいけそうです．

超手抜き

もしくは一番手抜きな整備方法は libz3.dll とz3フォルダをimport するPythonのファイル（すなわち import z3を記述しているファイル）と同じ階層に配置することです．
たとえば私が z3solver.py, sudoku.py でimport z3 を宣言している場合は下の写真のようになります．

z3solver.py, sudoku.py のソースは Kivyを用いた数独ソルバーのGUIのβ版ができましたを参照ください．

windows 環境でもちゃんと行けましたね．よかった・・・．