z3 모든 경우의 수

from z3 import *


# find hidden menu route with z3 solver.
input = [BitVec("input[%d]" % i, 32) for i in range(4)]

s = Solver()


for i in range(4):
	s.add(input[i] >= 0, input[i] <= 11)


money = [199, 299, 499, 399]
payload = 0
for i in range(4):
	payload += (money[i] * input[i])

s.add( payload == 0x1C06)


try:
	while s.check() == sat:
		print "[!] z3 result: sat"

		m = s.model()
		applestore = [0, 0, 0, 0]
		for i in range(4):
			applestore[i] = int(str(m[input[i]]))

		print applestore
		# prevent next model from using the same assignment as a previous model
		s.add(Or(input[0] != m[input[0]], input[1] != m[input[1]], input[2] != m[input[2]], input[3] != m[input[3]],))	
		
	else:
		print "[!] z3 result: unsat"
		sys.exit(-1)


except Exception as e:
	print "[!] z3 error : %s" % (e)
	sys.exit(-1)

finally:
	print ""

s.add(Or(input[0] != m[input[0]], input[1] != m[input[1]], input[2] != m[input[2]], input[3] != m[input[3]],))