[Tips] z3 unsigned 미지수 사용

[*] 이슈

z3에서 미지수를 만들때 사용하는 BitVec()은 기본적으로 모든 미지수를 signed 값으로 취급한다.

때문에 이런 이슈가 발생하게 된다.

from z3 import *

# 미지수 a0, a1을 1bit 크기의 미지수로 설정
a0 = BitVecs('a0', 1)
a1 = BitVecs('a1', 1)

s = Solver()
s.add(a0 > a1) 

print(s.check())
print(s.model())

$ python3 z3test.py 
sat
[a0 = 0, a1 = 1] # ??????????????????

위와 같이 a1의 값이 1로 더 크게 나와버린다.

- signed는 최상위 bit를 부호 비트로 사용하여 1이면 음수라고 인식하는데, a0과 a1은 1 bit 크기의 미지수이므로 값이 1이면 결과적으로 1bit 크기의 변수이기 때문에 음수 값이라고 판단을 하게 되어 이런 현상이 일어나는 듯하다. 

 

[*] 해결

이러한 문제를 해결하기 위해 z3에서는 unsigned 값 전용의 비교 연산 함수를 제공한다.

Signed	Unsigned
a0 < a1	ULT(a0, a1)
a0 <= a1	ULE(a0, a1)
a0 > a1	UGT(a0, a1)
a0 >= a1	UGE(a0, a1)
a0 / a1	UDiv(a0, a1)
a0 % a1	URem(a0, a1)
a0 >>a1	LShR(a0, a1)

 

사용 예시는 아래와 같다.

from z3 import *

# 미지수 a0, a1을 1bit 크기의 미지수로 설정
a0, a1 = BitVecs('a0 a1', 1) # [참고] BitVec()이 아닌 BitVecs로 한번에 미지수 두개 설정

s = Solver()
# s.add(a0 > a1)      # Signed
s.add(UGT(a0, a1))    # Unsigned

print(s.check())
print(s.model())

# [참고] 위처럼 안하고 그냥 아래와 같이 해도 바로 결과가 나온다. (코드 길이를 줄일 수 있음)
# solve(UGT(a0, a1))

$ python3 z3test.py 
sat
[a0 = 1, a1 = 0]

결과가 잘 나오는 것을 확인 할 수 있다.

 

[*] 참고

- https://stackoverflow.com/questions/17838424/how-to-model-signed-integer-with-bitvector

- z3 Guide 문서: https://ericpony.github.io/z3py-tutorial/guide-examples.htm : Machine Arithmetic 부분 참고