[smt solver]z3py 튜토리얼

z3는 smt solver의 일종인데 간단하게 각종 수식들의 해답을 구해주는 일종의 공학계산기 역할이다. ㅋㅋ
소프트웨어 테스팅이나 생물학쪽, 역학 등등 여러분야에서 많이 쓰이는것 같다.

잘 정리된 문서는 다음과 같다: 튜토리얼 

일단 z3 설치는 https://github.com/Z3Prover/z3 여기 그대로 따라하면 됨
일단 간단한 연립방정식은 다음과 같이 풀린다

>>> from z3 import *

>>> x = Int('x')

>>> y = Int('y')

>>> solve(x+y>10,x>20)

[x = 21, y = -10]

변수를 실수범위 내에서 구하려면 다음과 같이 하면 됨.

>>> solve(x*y == 12,y==13)

[y = 13, x = 12/13]

또 그냥 solve메서드로 풀지 말고 Solver라는 객체를 생성해서 수식을 풀 수도 있다. 다음과 같이.

>>> x = Int('x')

>>> y = Int('y')

>>> s = Solver()

>>> s.add(x+y==3)

>>> s.add(y==2)

>>> s

[x + y == 3, y == 2]

>>> s.check()

sat

>>> s.model()

[y = 2, x = 1]

그리고 add 메서드로 로 수식 조건(constraints)를 추가하는데 잘못된 add를 막기 위해 약간의 스냅샷(?)기능이 존재한다 push() 와 pop()이다. 이를 이용하면 이전 상태로 돌아갈 수 있다.

>>> s

[x + y == 3, y == 2] >>> s.push()

>>> s.add(x<2)

>>> s.add(y**2>10)

>>> s

[x + y == 3, y == 2, x < 2, y**2 > 10]

>>> s.pop()

>>> s

[x + y == 3, y == 2]

마지막으로 함수기능을 설명하자면, 일단 간략한 정의는 다음과 같다.

Function('함수명', 입력값, 출력값)

>>> x = Int('x')

>>> y = Int('y')

>>> f = Function('f',IntSort(),IntSort())

>>> solve(f(f(x))==x,x+y==2)

[y = 0, x = 2, f = [2 -> 1, 1 -> 2, else -> 1]]

결과 값은 다음과 같이 해석하면 된다. 만약 y =0 이고 x =2 이고, f(x)의 상태는 다음과 같아야 한다. f(2) = 1, f(1) = 2, f(아무값) = 1 따라서, f(f(x))는 x가 2이므로 0이 성립( 합성함수 이므로) 하고 x+y ==2또한 성립한다.