Python z3 모듈

Python z3 Module

더 추가할 예정!

z3에 대해 공부할겸 올려봅니다.. ㅎ 틀린부분이나 팁?그런거 있으면 알려주세요

모듈 링크 : https://github.com/Z3Prover/z3

유용한 외국 문서 : https://ericpony.github.io/z3py-tutorial/guide-examples.htm

일반적으로 그냥 근의 공식을 사용해서 프로그래밍을 해서 방정식의 근을 구하는 것은 imperative programming 방식이다.

파이썬의 z3 SMT solver 모듈을 사용해서 방정식의 근을 구하는 것은 decalarative programming이다.

나는 SMT solver 모듈을 사용하는 법에 대해 간단하게 공부하면서 포스팅하겠돠..

SMT solver?

Satisfiability Modulo Theories의 약자이다.

수식을 만족하는 값이 존재하는지 찾아준다. 수식을 만족하는 값이 존재할 경우 그 값을 구해준다.

True or False + 방정식, 부등식 해 구하기

Function

from z3 import *

z3 모듈 사용하기 위해 임포트

x = Int('x')
y = Int('y')

Int()는 미지수(정수)를 선언

x = Real('x')
y = Real('y')

Real()은 미지수(실수)를 선언

x = BitVec('x',8)
y = BitVec('y',8)

BitVec() 미지수(비트 벡터)를 선언

비트 연산을 할 때 사용되는데 BitVec('미지수',n)으로 n비트 미지수를 선언 해준다.

set_option(precision=3)

Real()을 사용했을 때 3자리 까지만 출력하고 싶다면 set_option 함수 사용

s = Solver()

Solver 객체 생성하는 함수

https://z3prover.github.io/api/html/classz3py_1_1_solver.html

위에 Solver()에 대해 많은 예제와 함수들이 있습니다.

s.add()

s.append() 

s.assert_exprs()

s.Insert()

수식을 추가하는 함수

s.assertions()

추가된 수식을 반환하는 함수

s.push()

s.pop()

수식을 넣고 빼는 함수

s.check()

값이 존재하면 sat 값이 존재하지 않으면 unsat을 반환

s.model()

값이 존재할 경우 값을 구해주는 함수

unsat , unknown이면 에러를 반환

s.reason_unknown()

check() 함수의 반환 값이 unknown인 이유를 알려줌

s.reset()

추가한 수식을 초기화 시키는 함수

Example

from z3 import *
x = Int('x')
s = Solver()
s.insert(x*x-4*x+3==0)
print s.check()
print s.model()

x^2 - 4x +3 =0을 풀어주는 예시다.