Z3 SMT Solver for windows using visual studio

SMT(Satisfiability modulo theories) Solver란 수학의 방정식을 풀어주는 해석기이다.

z3는 SMT Solver의 한 종류로 마이크로 소프트에서 개발했다고 한다. 

나는 파이썬으로 비쥬얼 스튜디오에서 작업하였다.

https://z3.codeplex.com/releases 에서 다운을 받는다.

비쥬얼 스튜디오를 통해 파이썬 프로젝트를 생성한다.

search Path-add forder to search path 클릭한다.

z3홈페이지에서 다운받은 파일에 있는 bin 폴더로 경로를 지정해준다.

from z3 import * # z3모듈을 import
 
x=Int('x')         
y=Int('y')         # 방정식에 사용할 변수 x,y를 선언
 
s=Solver()       # solver를 생성
 
s.add(x+y>5, x>1, y>1) # add함수를 통해 방정식을 추가
 
print(s.check())     # 방정식에 만족하는 값을 구한다.
                     # 올바르게 식이 풀렸다면 z3.sat를 반환한다 
 
print(s.model())     # 방정식을 통해 구한 값을 출력한다.

참고 : https://github.com/Z3Prover/z3