z3 정리~

문제를 조건에 맞게 해결할 때 사용하는 라이브러리 

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() 불만족의 증명 생성