mozhucy's blog.

z3求解器的一些简单使用

字数统计: 131阅读时长: 1 min
2018/08/16 Share

pip install z3-solver

  • 安装这东西,一行就够了,记住不要直接pip install z3就好
  • from z3 import *
  • 然后创建一个通用求解器,s = Solver()
  • 一些函数:s.add()添加条件,s.model()列出求解结果,s.check()查看约束条件是否合格
  • 一般循环设立值是这样的:X=[Int(“x%d”%i) for i in range(5)]
  • add的条件可以用逗号隔开,然后从s.model()中提取数据s.model()[x].as_long()
  • 之后有用到的例题在下面总结下
CATALOG
  1. 1. pip install z3-solver