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
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
| from z3 import *
a = Int('a')
b = Int('b')
solver = Solver()
solver.add(a * b == 342772773)
solver.add(a + b == 39526)
if solver.check() == sat:
m = solver.model()
o = ""
o += chr(int(m[a].as_long() & 0xff))
o += chr(int(m[a].as_long() >> 8))
o += chr(int(m[b].as_long() & 0xff))
o += chr(int(m[b].as_long() >> 8))
print(o)
else:
print("No solution")
a, b, c, d, e, f, g, h = Ints('a b c d e f g h')
solver = Solver()
solver.add((d * (1 << 24)) + (c * (1 << 16)) + (b * (1 << 8)) + a - (
(h * (1 << 24)) + (g * (1 << 16)) + (f * (1 << 8)) + e) == 1005712381)
solver.add((b * (1 << 8)) + a + (d * (1 << 8)) + c == 56269)
solver.add((f * (1 << 8)) + e - (h * (1 << 8)) - g == 15092)
solver.add(a * e == 10710)
solver.add(c * g == 12051)
solver.add(d + h == 172)
if solver.check() == sat:
m = solver.model()
print("a =", chr(m[a].as_long()))
print("b =", chr(m[b].as_long()))
print("c =", chr(m[c].as_long()))
print("d =", chr(m[d].as_long()))
print("e =", chr(m[e].as_long()))
print("f =", chr(m[f].as_long()))
print("g =", chr(m[g].as_long()))
print("h =", chr(m[h].as_long()))
else:
print("No solution")
a, b=Ints('a b')
solver = Solver()
solver.add(a * b == 171593250)
solver.add(a + b == 26219)
if solver.check() == sat:
m = solver.model()
o = ""
o += chr(int(m[a].as_long() & 0xff))
o += chr(int(m[a].as_long() >> 8))
o += chr(int(m[b].as_long() & 0xff))
o += chr(int(m[b].as_long() >> 8))
print(o)
a, b=Ints('a b')
solver = Solver()
solver.add(a * b == 376306868)
solver.add(a + b == 40341)
if solver.check() == sat:
m = solver.model()
o = ""
o += chr(int(m[a].as_long() & 0xff))
o += chr(int(m[a].as_long() >> 8))
o += chr(int(m[b].as_long() & 0xff))
o += chr(int(m[b].as_long() >> 8))
print(o)
|
不能直接反编译成python
