z3-solver

就记录个z3顺序输出

1
2
3
4
5
6
7
8
9
10
from z3 import *

s = Solver()
flag = [BitVec("{}".format(i), 8) for i in range(23)]

if s.check() == sat:
    m = s.model()
    result = [int(str(m[each]), 10) for each in flag]
    print(bytes(result))

BitVec类型不能直接转int，但是可以通过转str再转int。。。。。

真sb

另一种输出

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
from z3 import *

v10 = [0x0000007E, 0x000000E1, 0x0000003E, 0x00000028, 0x000000D8,
       0x000000FD, 0x00000014, 0x0000007C, 0x000000E8, 0x0000007A,
       0x0000003E, 0x00000017, 0x00000064, 0x000000A1, 0x00000024,
       0x00000076, 0x00000015, 0x000000B8, 0x0000001A, 0x0000008E,
       0x0000003B, 0x0000001F, 0x000000BA, 0x00000052, 0x0000004F]
v12 = [0x0000F9FE, 0x00008157, 0x000108B2, 0x0000D605, 0x0000F21B,
       0x00010FF3, 0x00009146, 0x00011212, 0x0000CF76, 0x00010C46,
       0x0000F76B, 0x000077DF, 0x000103BE, 0x0000C6F8, 0x0000ED8A,
       0x0000BE90, 0x000075EC, 0x0000EAC8, 0x0000AE37, 0x0000CC29,
       0x0000A828, 0x00005C6C, 0x0000AB4A, 0x0000836E, 0x0000ACEE]

s = Solver()

x = [Int('x[%d]' % i) for i in range(25)]
for i in range(5):
    for j in range(5):
        s.add(v12[i * 5 + j] == (
                    x[i * 5] * v10[j] + x[i * 5 + 1] * v10[1 * 5 + j] + x[i * 5 + 2] * v10[2 * 5 + j] + x[i * 5 + 3] *
                    v10[3 * 5 + j] + x[i * 5 + 4] * v10[4 * 5 + j]))

if (s.check()):
    k = 0
    while (s.check() == sat):
        condition = []
        m = s.model()
        print("[%d]" % k)
        print(m)
        k += 1
        for i in range(25):
            condition.append(x[i] != int("%s" % (m[x[i]])))

        s.add(Or(condition))
else:
    print("No")