from
z3
import
*
s
=
Solver()
X
[''
for
i
in
range
(
8
)]
r
Int
'r'
)
):
t
'X'
+
str
(i)
X[i]
(t)
print
s.add(And(X[i]>
0
,X[i]<
9
))
v1
X[
3
]
1000
100
1
10
2
v2
5
4
v3
7
6
r1
(v1
v2)
s.add(r1
4040
r2
/
s.add(r2
115
s.add(v1
-
110
1900
num
''
if
s.check()
sat:
m
s.model()
#print m
chr
int
(m[X[i]]))
0x30
else
:
"No Solution!"
[培训]内核驱动高级班,冲击BAT一流互联网大厂工作,每周日13:00-18:00直播授课