Z3约束器使用流程
- 创建变量
例：
x = Int('x')
y = Int('y')
2.创建solver求解器
例：s = Solver()
3.添加约束条件
例：s.add(x+y==10)
4.检查solver中的约束是否满足
例：s.check()
5.利用model()输出运算结果
例：s.model()
Z3-example
from z3 import *
v2=[18564, 37316, 32053, 33278, 23993, 33151,
15248, 13719, 34137, 27391, 28639, 18453, 28465,
12384, 20780, 45085, 35827, 37243, 26037, 39409,
17583, 20825, 44474, 35138, 36914, 25918, 38915,
17672, 21219, 43935, 37072, 39359, 27793, 41447,
18098, 21335, 46164, 38698, 39084, 29205, 40913,
19117, 21786, 46573, 38322, 41017, 29298, 43409,
19655]
s = Solver()#设置一个解方程的类Solver(必须要设置）
a1 = [0]*49 #设置的列表长度为49，从0到48，因为下面这个如果是空列表的话不能用索引
for i in range(49):
a1[i] = Int('a1['+str(i)+']')
#这里的3行 是设置未知量，都要设置，Int是设置int型的
s.add(v2[0] == 34 * a1[3] + 12 * a1[0] + 53 * a1[1] + 6 * a1[2] + 58 * a1[4] + 36 * a1[5] + a1[6])
s.add(v2[1] == 27 * a1[4] + 73 * a1[3] + 12 * a1[2] + 83 * a1[0] + 85 * a1[1] + 96 * a1[5] + 52 * a1[6])
s.add(v2[2] == 24 * a1[2] + 78 * a1[0] + 53 * a1[1] + 36 * a1[3] + 86 * a1[4] + 25 * a1[5] + 46 * a1[6])
s.add(v2[3] == 78 * a1[1] + 39 * a1[0] + 52 * a1[2] + 9 * a1[3] + 62 * a1[4] + 37 * a1[5] + 84 * a1[6])
s.add(v2[4] == 48 * a1[4] + 6 * a1[1] + 23 * a1[0] + 14 * a1[2] + 74 * a1[3] + 12 * a1[5] + 83 * a1[6])
s.add(v2[5] == 15 * a1[5] + 48 * a1[4] + 92 * a1[2] + 85 * a1[1] + 27 * a1[0] + 42 * a1[3] + 72 * a1[6])
s.add(v2[6] == 26 * a1[5] + 67 * a1[3] + 6 * a1[1] + 4 * a1[0] + 3 * a1[2] + 68 * a1[6])
s.add(v2[7] == 34 * a1[10] + 12 * a1[7] + 53 * a1[8] + 6 * a1[9] + 58 * a1[11] + 36 * a1[12] + a1[13])
s.add(v2[8] == 27 * a1[11] + 73 * a1[10] + 12 * a1[9] + 83 * a1[7] + 85 * a1[8] + 96 * a1[12] + 52 * a1[13])
s.add(v2[9] == 24 * a1[9] + 78 * a1[7] + 53 * a1[8] + 36 * a1[10] + 86 * a1[11] + 25 * a1[12] + 46 * a1[13])
s.add(v2[10] == 78 * a1[8] + 39 * a1[7] + 52 * a1[9] + 9 * a1[10] + 62 * a1[11] + 37 * a1[12] + 84 * a1[13])
s.add(v2[11] == 48 * a1[11] + 6 * a1[8] + 23 * a1[7] + 14 * a1[9] + 74 * a1[10] + 12 * a1[12] + 83 * a1[13])
s.add(v2[12] == 15 * a1[12] + 48 * a1[11] + 92 * a1[9] + 85 * a1[8] + 27 * a1[7] + 42 * a1[10] + 72 * a1[13])
s.add(v2[13] == 26 * a1[12] + 67 * a1[10] + 6 * a1[8] + 4 * a1[7] + 3 * a1[9] + 68 * a1[13])
s.add(v2[14] == 34 * a1[17] + 12 * a1[14] + 53 * a1[15] + 6 * a1[16] + 58 * a1[18] + 36 * a1[19] + a1[20])
s.add(v2[15] == 27 * a1[18] + 73 * a1[17] + 12 * a1[16] + 83 * a1[14] + 85 * a1[15] + 96 * a1[19] + 52 * a1[20])
s.add(v2[16] == 24 * a1[16] + 78 * a1[14] + 53 * a1[15] + 36 * a1[17] + 86 * a1[18] + 25 * a1[19] + 46 * a1[20])
s.add(v2[17] == 78 * a1[15] + 39 * a1[14] + 52 * a1[16] + 9 * a1[17] + 62 * a1[18] + 37 * a1[19] + 84 * a1[20])
s.add(v2[18] == 48 * a1[18] + 6 * a1[15] + 23 * a1[14] + 14 * a1[16] + 74 * a1[17] + 12 * a1[19] + 83 * a1[20])
s.add(v2[19] == 15 * a1[19] + 48 * a1[18] + 92 * a1[16] + 85 * a1[15] + 27 * a1[14] + 42 * a1[17] + 72 * a1[20])
s.add(v2[20] == 26 * a1[19] + 67 * a1[17] + 6 * a1[15] + 4 * a1[14] + 3 * a1[16] + 68 * a1[20])
s.add(v2[21] == 34 * a1[24] + 12 * a1[21] + 53 * a1[22] + 6 * a1[23] + 58 * a1[25] + 36 * a1[26] + a1[27])
s.add(v2[22] == 27 * a1[25] + 73 * a1[24] + 12 * a1[23] + 83 * a1[21] + 85 * a1[22] + 96 * a1[26] + 52 * a1[27])
s.add(v2[23] == 24 * a1[23] + 78 * a1[21] + 53 * a1[22] + 36 * a1[24] + 86 * a1[25] + 25 * a1[26] + 46 * a1[27])
s.add(v2[24] == 78 * a1[22] + 39 * a1[21] + 52 * a1[23] + 9 * a1[24] + 62 * a1[25] + 37 * a1[26] + 84 * a1[27])
s.add(v2[25] == 48 * a1[25] + 6 * a1[22] + 23 * a1[21] + 14 * a1[23] + 74 * a1[24] + 12 * a1[26] + 83 * a1[27])
s.add(v2[26] == 15 * a1[26] + 48 * a1[25] + 92 * a1[23] + 85 * a1[22] + 27 * a1[21] + 42 * a1[24] + 72 * a1[27])
s.add(v2[27] == 26 * a1[26] + 67 * a1[24] + 6 * a1[22] + 4 * a1[21] + 3 * a1[23] + 68 * a1[27])
s.add(v2[28] == 34 * a1[31] + 12 * a1[28] + 53 * a1[29] + 6 * a1[30] + 58 * a1[32] + 36 * a1[33] + a1[34])
s.add(v2[29] == 27 * a1[32] + 73 * a1[31] + 12 * a1[30] + 83 * a1[28] + 85 * a1[29] + 96 * a1[33] + 52 * a1[34])
s.add(v2[30] == 24 * a1[30] + 78 * a1[28] + 53 * a1[29] + 36 * a1[31] + 86 * a1[32] + 25 * a1[33] + 46 * a1[34])
s.add(v2[31] == 78 * a1[29] + 39 * a1[28] + 52 * a1[30] + 9 * a1[31] + 62 * a1[32] + 37 * a1[33] + 84 * a1[34])
s.add(v2[32] == 48 * a1[32] + 6 * a1[29] + 23 * a1[28] + 14 * a1[30] + 74 * a1[31] + 12 * a1[33] + 83 * a1[34])
s.add(v2[33] == 15 * a1[33] + 48 * a1[32] + 92 * a1[30] + 85 * a1[29] + 27 * a1[28] + 42 * a1[31] + 72 * a1[34])
s.add(v2[34] == 26 * a1[33] + 67 * a1[31] + 6 * a1[29] + 4 * a1[28] + 3 * a1[30] + 68 * a1[34])
s.add(v2[35] == 34 * a1[38] + 12 * a1[35] + 53 * a1[36] + 6 * a1[37] + 58 * a1[39] + 36 * a1[40] + a1[41])
s.add(v2[36] == 27 * a1[39] + 73 * a1[38] + 12 * a1[37] + 83 * a1[35] + 85 * a1[36] + 96 * a1[40] + 52 * a1[41])
s.add(v2[37] == 24 * a1[37] + 78 * a1[35] + 53 * a1[36] + 36 * a1[38] + 86 * a1[39] + 25 * a1[40] + 46 * a1[41])
s.add(v2[38] == 78 * a1[36] + 39 * a1[35] + 52 * a1[37] + 9 * a1[38] + 62 * a1[39] + 37 * a1[40] + 84 * a1[41])
s.add(v2[39] == 48 * a1[39] + 6 * a1[36] + 23 * a1[35] + 14 * a1[37] + 74 * a1[38] + 12 * a1[40] + 83 * a1[41])
s.add(v2[40] == 15 * a1[40] + 48 * a1[39] + 92 * a1[37] + 85 * a1[36] + 27 * a1[35] + 42 * a1[38] + 72 * a1[41])
s.add(v2[41] == 26 * a1[40] + 67 * a1[38] + 6 * a1[36] + 4 * a1[35] + 3 * a1[37] + 68 * a1[41])
s.add(v2[42] == 34 * a1[45] + 12 * a1[42] + 53 * a1[43] + 6 * a1[44] + 58 * a1[46] + 36 * a1[47] + a1[48])
s.add(v2[43] == 27 * a1[46] + 73 * a1[45] + 12 * a1[44] + 83 * a1[42] + 85 * a1[43] + 96 * a1[47] + 52 * a1[48])
s.add(v2[44] == 24 * a1[44] + 78 * a1[42] + 53 * a1[43] + 36 * a1[45] + 86 * a1[46] + 25 * a1[47] + 46 * a1[48])
s.add(v2[45] == 78 * a1[43] + 39 * a1[42] + 52 * a1[44] + 9 * a1[45] + 62 * a1[46] + 37 * a1[47] + 84 * a1[48])
s.add(v2[46] == 48 * a1[46] + 6 * a1[43] + 23 * a1[42] + 14 * a1[44] + 74 * a1[45] + 12 * a1[47] + 83 * a1[48])
s.add(v2[47] == 15 * a1[47] + 48 * a1[46] + 92 * a1[44] + 85 * a1[43] + 27 * a1[42] + 42 * a1[45] + 72 * a1[48])
s.add(v2[48] == 26 * a1[47] + 67 * a1[45] + 6 * a1[43] + 4 * a1[42] + 3 * a1[44] + 68 * a1[48])
#add是添加约束条件
print(s.check())#check是保证有解
answer=s.model()#model是输出运算结果
print(answer)