MozhuCY's blog.

z3求解器的一些简单使用

字数统计: 131阅读时长: 1 min
1970/01/01 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()
  • 之后有用到的例题在下面总结下

原文作者:MozhuCY

原文链接:http://mozhucy.com/1970/01/01/z3/

发表日期:January 1st 1970, 12:00:00 am

更新日期:July 29th 2019, 11:32:03 am

版权声明:本文采用知识共享署名-非商业性使用 4.0 国际许可协议进行许可

CATALOG
  1. 1. pip install z3-solver