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#