在Z3约束求解器中，我们可能需要寻找同时满足两个条件的模型，也可能需要寻找满足两个条件中一个条件的模型，这个时候，我们可以借助And方法和Or方法来实现

引入

我们先来举一个简单的例子

当我们想要查找满足a+b=2且a、b均为正整数时，a、b可能的值
我们可以通过如下方法查找到满足条件的结果

from z3 import *a = Int('a')
b = Int('b')
s = Solver()
s.add(a+b<2)
s.add(a>=0)
s.add(b>=0)s.check()
print(s.model())

这个时候，符合条件的结果总共有四种（model()方法只会输出一种，所以在控制台上我们只能看到一组a和b的值）

[b = 0, a = 0]
[b = 0, a = 1]
[b = 1, a = 0]
[b = 1, a = 1]

And语句

如果我希望查找到的结果中，把结果中包含a=1的情况和包含b=1情况去掉，只保留[b = 0, a = 0]这一组，这个时候我们可以通过两个add语句实现

s.add(a!=1)
s.add(b!=1)

也可以借助And语句实现

s.add(And(a!=1,b!=1))

下面是借助And语句实现的完整代码

from z3 import *a = Int('a')
b = Int('b')
s = Solver()
s.add(a+b<2)
s.add(a>=0)
s.add(b>=0)
s.add(And(a!=1,b!=1))
s.check()
print(s.model())

此时，符合条件的结果只有[b = 0, a = 0]这一种情况

Or语句

如果我希望符合条件的结果中，把a为1且b为1的情况去掉，也就是去掉[b = 1, a = 1]这一组，这个时候我们不能使用s.add(a!=1)和s.add(b!=1)来实现这一操作，可以借助Or语句来实现

s.add(Or(a!=1,b!=1))

下面是借助Or语句实现的完整代码

from z3 import *a = Int('a')
b = Int('b')
s = Solver()
s.add(a+b<2)
s.add(a>=0)
s.add(b>=0)
s.add(Or(a!=1,b!=1))
s.check()
print(s.model())

这种情况下，符合条件的结果中，不存在a和b同时为1的情况了，只有a、b不同时为1的三种结果。

技巧

关于Or还有一个很实用的例子

a = Int('a')
b = Int('b')
s = Solver()
s.add(1 <= a)
s.add(a <= 20)
s.add(1 <= b)
s.add(b <= 20)
s.add(a >= 2*b)
while s.check() == sat:print (s.model())s.add(Or(a != s.model()[a], b != s.model()[b]))

因为model()方法只能输出最后一个check()方法的模型，导致我们无法直接获取到全部符合条件的模型
因此，借助while循环和Or语句来添加条件，实现全部符合条件的模型结果的获取。

【python环境下Z3约束求解器学习笔记】And和Or的用法相关推荐

Python Z3约束求解器解决数独问题
Z3是由Microsoft Research开发的高性能定理证明器.接下来将使用Python3中的Z3库来实现对数独问题的解决. 关于Python中Z3的使用入门,可以参考这篇博文https://bl ...
【嵌入式环境下linux内核及驱动学习笔记-（16）linux总线、设备、驱动模型之input框架】
目录 1.Linux内核输入子系统概念导入 1.1 输入设备工作机制 1.2 运行框架 1.3 分层思想 2.驱动开发步骤 2.1 在init()或probe()函数中 2.2 在exit()或rem ...
【嵌入式环境下linux内核及驱动学习笔记-（15-1）例程】
目录 1.在APP直接调用标准文件IO操作I2C(针对学习笔记-15的15.3节) 1.1 mail.c 1.2 mpu6050.h 1.3 mpu6050.c 1.4 Makefile 2.以外称i ...
re学习笔记（37）BUUCTF-re-[GUET-CTF2019]re Z3约束求解器
推荐肉丝r0ysue课程(包含安卓逆向与js逆向): 新手一枚,如有错误(不足)请指正,谢谢!! 个人博客:点击进入题目链接:[GUET-CTF2019]re 题目下载:点击下载 IDA64位载入 ...
【嵌入式环境下linux内核及驱动学习笔记-（11-设备树）】
目录 1.设备树体系 1.1 DTS /DTSI / DTC / DTB 2.基础语法 2.1 节点语法 2.1.1 通用名称建议 2.2 属性语法 2.2.1 属性值 2.3 关于label 2.4 ...
python求解立方根,python环境下使用牛顿迭代法求任意实数立方根
https://images1.tqwba.com/20200918/xx0b50i53j4 推导过程如下: 一般牛顿迭代法的图名都叫做Newton-Raphson.也就是牛顿-拉弗森法二.使用牛顿 ...
c++调用cplex求解例子_视频教程 | 用Python玩转运筹优化求解器IBM CPLEX（二）
编者按优化求解器对于做运筹学应用的学生来说,意义重大. 然而直到今天,放眼望去,全网(包括墙外)几乎没有一个系统的Cplex中文求解器教程. 作为华人运筹学的最大的社区,『运筹OR帷幄』责无旁贷, ...
“芯”自主，更安全。国产三维云CAD:CrownCAD完全自主知识产权三维几何建模内核、约束求解器。
CAD软件是产品创新的工具,是研发设计师不可或缺的必备软件,它解放设计师的双手和大脑,将设计师精力更多地集中于设计和创新上.在长期的使用过程中,设计师用户既是CAD技术的受益者,也是CAD技术的历史创 ...
使用 Python 和 OpenCV 构建 SET 求解器
作者 | 小白来源 | 小白学视觉小伙伴们玩过 SET 吗?SET 是一种游戏,玩家在指定的时间竞相识别出十二张独特纸牌中的三张纸牌(或 SET)的模式.每张 SET 卡都有四个属性:形状.阴影/ ...

【python环境下Z3约束求解器学习笔记】And和Or的用法

引入

And语句

Or语句

技巧

【python环境下Z3约束求解器学习笔记】And和Or的用法相关推荐

最新文章

热门文章