SMT solver 모듈인데 배우는 게 좋겠지! 리버싱을 공부해보겠슨, 참고한 블로그는 https://tistory.d1n0.me/18

설치

Z3 solver 설치는 다음과 같이 한다.

pip install z3-solver

basic

그리고 문법은 아래에 정리했다.

from z3 import *

# 정수형 미지수 선언 
x = Int('x')

# 실수형 미지수 선언 
y = Real('y')

# bool 
z = Bool('z')

# Bit vector 
a = BicVec('a',16)

모듈러 역수 구할 때 비트벡터 사용한다. 미지수 뒤의 숫자는 몇 비트인지 설정하는 숫자이다. 위 예시는 16비트이다.

답은 solve()로 구한다.

from z3 import *
x=Int('x')
y=Int('y')
solve(x+y==12, x-y==6)

Solver Class

Solver라는 객체가 뭐에 쓰는 건지 알아보자.

s= Solver()
s.add(x+y==12)
s.add(x-y==6)

아까 예제를 솔버 객체로 표현하면 위와 같다.

s.check()
s.reason_unknown()
s.reset()

# 상태를 기억하기 위해 사용한다고 함 
# 약간 디버거의 중단점 같은 느낌인듯
s.push()
s.pop()

답이 여러개라면?

while s.check() == sat:
    print(s.model())
    s.add(OR(x != s.model()[x], y !=model()[y]))
    # s.model의 x,y가 기존에 있는 x,y와 겹치지 않도록(중복 방지) 수식 추가 
    # 이러면 중복 답 사라지고 다른 답 print 
    # 위 두 단계가 unsat이 될 때까지 반복 출력