z3 정리

from z3 import *

x = Int('x')

y = Int('y')

s = Solve()

s.add() # 조건식 1

s.add() # 조건식 2

print(s) # 리스트 된 조건식들

print(s.check()) # sat이면 계산된거 unsat이면 계산 ㄴ

print(s.model()) # 나온 x, y 값을 보여줌