오늘

Windows에서 Python부터 개별 구해기에 필요한 z3를 사용합니다.

할 수 없는 일

pip 배치

import는 가능하지만 모듈의 클래스에 접근하면 실행 오류가 됩니다.

> pip install z3

conda install ... 갈 수 있어요?

찾고 있는데... https://anaconda.org/asmeurer/z3
상기 사이트의 주문에 따라 실험을 해도 Package Not Found Error에 격분한다.

> conda install -c asmeurer z3 

Mac과 동일

> conda install z3-solver

시도해도 구축에 실패했습니다. Windows는 안 되잖아요.

해결 방법

위커 보기

https://github.com/Z3Prover/z3/wiki/Using-Z3Py-on-Windows
이동한 페이지는 설치 Z3Py with pre-compiled Windows binaries 마법사를 따릅니다. 최신 pre-compile binaries 발표 페이지를 다운로드하십시오.
https://github.com/Z3Prover/bin/tree/master/releases
예를 들어 z3-4.5.0-x64-win입니다.압축 해제
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의β판이 완성되었다 참조하십시오.

윈도우즈 환경도 잘 갔네요. 다행이네요.