본문 바로가기

Programming

Install z3 for python from source

z3 공홈에서 받으려고하면 뭔가 git 에서 오류나거나 python 버전등등의 문제로 소스좀 수정해줘야하고 무튼 귀찮다. 인터넷에서 리눅스용 z3py.tgz 를 받았으면.

다운로드하고 압축푼다음 일단 ./configure 부터 해주자.



그리고 그냥 시키는대로 설치하면 끝~


아래처럼 Int 형 변수 x, y 선언하고 아주 간단한 수식으로 solve 를 돌려보면 해를 잘 찾는것을 볼 수 있다 :)



64bit 리눅스 설치 참고 -> http://smleenull.tistory.com/591




z3py 간단 사용예.

root@ubuntu:/tmp/1832# cat z.py
from z3 import *
x = Int('var1')
y = Int('var2')
s = Solver()
s.add(x+y==1)
s.check()
m = s.model()
print m.evaluate(x)
print m.evaluate(y)

root@ubuntu:/tmp/1832# python z.py
1
0
root@ubuntu:/tmp/1832#