D1N0's hacking blog

Z3 solver z3 solver는 특정 값들을 찾아주는 SMT solver 모듈이라고 한다 쉽게 말하면 여러 수식을 풀어주는 모듈이라고 생각하면 된다 리버싱 할 때도 많이 필요하고 그게 아니더라도 유용히 쓸 수 있을 거 같아서 정리하기로 했다 설치 일단 Z3 solver 모듈의 링크는 이곳이다 github.com/Z3Prover/z3 들어가면 다양한 언어에서의 설치 과정이 자세히 나와있지만 나는 파이썬을 쓸 거라서 pip로 간단히 설치가 가능하다 pip install z3-solver or pip3 install z3-solver 기본 문법 사용 전 모듈 불러오기 from z3 import * 정수형 미지수 선언 x = Int('x') y = Int('y') 실수형 미지수 선언 x = Real('x'..