문제를 조건에 맞게 해결할 때 사용하는 라이브러리
from z3 import *
s = Solver()
일단 Solver()로 인스턴스 생성
x = Int('x')
s.add(x > 0)
s.add(x < 10)
add()로 제약 조건 추가
result = s.check()
check()로 해당 조건으로 문제가 해결되는지 판단
sat(가능) unsat(불가능) unknown(몰라)
if s.check() == sat:
m = s.model()
print(m[x])
sat일 시(가능하다면) model()로 해 반환
추가 기능은 코드로 한 번에 정리
# push()와 pop(), 스택 관리
s.push() # 현재 상태 저장
s.add(x == 5)
s.pop() # 이전 상태로 복원
# reset() 초기화
s.reset()
# assertions(), 제약 조건 반환
for assertion in s.assertions():
print(assertion)
# statistics() 성능 통계
print(s.statistics())
# unsat_core() 불만족하는 제약 조건 반환(항상 최소한으로)
# proof() 불만족의 증명 생성