Z3 约束器 使用

#!/usr/bin/env python
# -*- coding: utf-8 -*-
fro<a href="https://www.gaodaima.com/tag/m" title="查看更多关于m的文章" target="_blank">m</a> z3 <span>import</span> *
# 创建约束解析器
<a href="https://www.gaodaima.com/tag/solver" title="查看更多关于solver的文章" target="_blank">solver</a> = Solver()
# 定义变量
m1 = Int("m1")
m2 = Int("m2")
m3 = Int("m3")
m4 = Int("m4")
m5 = Int("m5")
m6 = Int("m6")
m7 = Int("m7")
# 添加约束条件
# 参数前7个ascii等于0x321
solver.<span>add</span>(m1+m2+m3+m4+m5+m6+m7==0x321)
# 约束每个解的范围都是在可见字符串
solver.<span>add</span>(32<=m1)
solver.<span>add</span>(m1<127)
solver.<span>add</span>(32<=m2)
solver.<span>add</span>(m2<127)
solver.<span>add</span>(32<=m3)
solver.<span>add</span>(m3<127)
solver.<span>add</span>(32<=m4)
solver.<span>add</span>(m4<127)
solver.<span>add</span>(32<=m5)
solver.<span>add</span>(m5<127)
solver.<span>add</span>(32<=m6)
solver.<span>add</span>(m6<127)
solver.<span>add</span>(32<=m7)
solver.<span>add</span>(m7<127)
<span>if</span> solver.check() == sat:
    flag = solver.model()
    <span>pr<a href="https://www.gaodaima.com/tag/int" title="查看更多关于int的文章" target="_blank">int</a></span>(flag)
<span>else</span>:
    <span>print</span>("<span>no answer</span>")

www#gaodaima.com来源gao!%daima.com搞$代*!码$网搞代码