from z3 import *

# Solver 생성
s = Solver()

# 미지수 선언
# 정수형
x = Int('x')
y = Int('y')

# 실수형
x = Real('x')
y = Real('y')

# bool형
x = Bool('x')
y = Bool('y')

# 비트벡터형
x = BitVec('x', 16)    # 16비트 크기의 미지수 x 선언
y = BitVec('y', 50)    # 50비트 크기의 미지수 y 선언

# 여러 개의 미지수를 리스트 형태로 동시에 선언하기
A = list()
for i in range(100):
    A.append(BitVec('a_{}'.format(i), 64))

B = [Int('b_{}'.format(i)) for i in range(64)]

# 생성한 Solver에 수식 추가하기
s.add()
s.append()
s.Insert()
# 괄호 안에 추가할 수식을 넣어 주면 됩니다.

# 그 외에 push pop으로 수식을 넣었다가 뺐다가 할 수 있습니다.
s.push()
s.pop()

# 일반적인 python 코드와 거의 유사하게 수식을 추가하면 됩니다.
x = Int('x')
y = Int('y')
s.add(x + y == 15)
s.add(x ^ y == 0xDEADBEEF)
s.add(Or(x == 15, y == 10))

# 답을 얻기 위해서는 먼저 check()를 이용해 해가 있는지 없는지 알아야 합니다.
s.check()
# 이렇게 Solver에 check() 메소드를 호출하면 sat(해 존재) 혹은 unsat(해 존재 안함)을 반환합니다.
# 아니면 unknown을 반환하기도 합니다.

# check()을 호출했을 때 sat을 반환하면 해를 얻을 수 있습니다.
s.model()

while s.check() == sat:
  print(s.model())
  s.add(Or(x != s.model()[x], y != s.model()[y]))
  
# 미지수가 많아 지면 위에처럼 쓰면 엄청 지저분해지니까, 아래처럼 쓸 수 있음
# 모든 해를 구해서 출력하는 코드
while solver.check() == sat:
    model = solver.model()
    flag = [model[inp[i]].as_long() for i in range(64)]
    for i in flag:
        print(hex(i)[-1], end='')
    print()

    ex = False # Oring을 덮어 씌울 거니까 초기값은 False가 되야 하겠죠
    for idx, i in enumerate(flag):
        ex = Or(ex, inp[idx] != i)
    solver.add(ex)