z3基础学习
z3基础学习
z3是一个微软出品的开源约束求解器,能够解决很多种情况下的给定部分约束条件寻求一组满足条件的解的问题。
安装:pip install z3-solver
1. 简单使用
from z3 import *
x = Int('x') #创建名为x的int类型变量
y = Int('y')
solve(x + y==10,2*x+4*y==32) #求解并输出结果
#[y = 6, x = 4]
添加约束条件
from z3 import *
a,b=Ints('a b')
s=Solver() #创建一个约束求解器
s.add(a+b==10) #添加约束条件
s.add(a+3*b==12)if s.check()==sat: #有解r=s.model() #求解
print(r) #[b = 1, a = 9]
print(r[a]) #9
print(r[b]) #1
精度设置,简化表达式
from z3 import *
x=Real('x')
y=simplify(3*x+1==2) #化简表达式
print(y) #x == 1/3
solve(y) #[x = 1/3]
set_option(rational_to_decimal=True) #实数结果以小数呈现,默认10位小数
solve(y) #[x = 0.3333333333?]
set_option(precision=30) #精度设为30位
solve(y) #[x = 0.333333333333333333333333333333?]
#有问号说明输出有精度限制x, y = Reals('x y')
# 简化为单项式之和
t = simplify((x + y)**3, som=True)
print (t) #x*x*x + 3*x*x*y + 3*x*y*y + y*y*y
# 幂运算符简化
t = simplify(t, mul_to_power=True)
print (t) #x**3 + 3*x**2*y + 3*x*y**2 + y**3
快速添加变量
s=[Real('s%d' % i) for i in range(50)] #添加50个Real变量
s.add(s[18]*s[8]==5)
可见字符
s.add(x<127)
s.add(x>=32)
注意:
- 当问题有多个解时,z3求解器只会输出一个解
- z3不允许列表与列表间添加
==约束
2. 数据类型
| 数据类型 | 格式 | 解释 |
|---|---|---|
| 整数 | x=Int('x') | |
| 实数 | y=Real('y') | |
RealVal(1) | 实数1 | |
| 布尔 | b=Bool('b') | |
| 有理数 | Q(1,3) | 表示1/3 |
| 位向量 | x=BitVec('x',16) | 长度16位的变量x |
BitVecVal(10,32) | 大小为32的位向量,其值为10 | |
| 数组 | a=Array('a',IntSort(),IntSort()) | 索引为整数,值为整数 |
3. 布尔逻辑与常见运算符
>> <<
== >= > !=
And() Or() Not()
Implies(P,Q) #蕴含式 p->Q,若P则Q
z=If(b,x,y) #b为真,则z=x,否则z=y
4. 尝试一下
useZ3.bin
main函数

跟踪一下

a1,a2是Dword数组的地址,按Y改一波类型


from z3 import *
dword_602120=[0x0000007A, 0x000000CF, 0x0000008C, 0x00000095, 0x0000008E, 0x000000A8, 0x0000005F, 0x000000C9, 0x0000007A, 0x00000091, 0x00000088, 0x000000A7, 0x00000070, 0x000000C0, 0x0000007F, 0x00000089, 0x00000086, 0x00000093, 0x0000005F, 0x000000CF, 0x0000006E, 0x00000086, 0x00000085, 0x000000AD, 0x00000088, 0x000000D4, 0x000000A0, 0x000000A2, 0x00000098, 0x000000B3, 0x00000079, 0x000000C1, 0x0000007E, 0x0000007E, 0x00000077, 0x00000093]
dword_6021C0=[0x00000010, 0x00000008, 0x00000008, 0x0000000E, 0x00000006, 0x0000000B, 0x00000005, 0x00000017, 0x00000005, 0x0000000A, 0x0000000C, 0x00000017, 0x0000000E, 0x00000017, 0x00000013, 0x00000007, 0x00000008, 0x0000000A, 0x00000004, 0x0000000D, 0x00000016, 0x00000011, 0x0000000B, 0x00000016, 0x00000006, 0x0000000E, 0x00000002, 0x0000000B, 0x00000012, 0x00000009, 0x00000005, 0x00000008, 0x00000008, 0x0000000A, 0x00000010, 0x0000000D]
unk_602080=[0x00000008, 0x00000001, 0x00000007, 0x00000001, 0x00000001, 0x00000000, 0x00000004, 0x00000008, 0x00000001, 0x00000002, 0x00000003, 0x00000009, 0x00000003, 0x00000008, 0x00000006, 0x00000006, 0x00000004, 0x00000008, 0x00000003, 0x00000005, 0x00000007, 0x00000008, 0x00000008, 0x00000007, 0x00000000, 0x00000009, 0x00000000, 0x00000002, 0x00000003, 0x00000004, 0x00000002, 0x00000003, 0x00000002, 0x00000005, 0x00000004, 0x00000000]
s=Solver()
a1=[BitVec('%d' % i, 8) for i in range(36)] #8位位向量
ptr=[0]*36
v7=[0]*36
v8=[0]*36
v9=[0]*36for i in range(36):s.add(a1[i] <127) #添加约束条件①s.add(a1[i] >=32)for i in range(36):ptr[i] = a1[i] >> 4v7[i] = a1[i] & 15for i in range(6):for j in range(6):for k in range(6):v8[6*i+j] += ptr[6*i + k] * unk_602080[6*k+j]for i in range(6):for j in range(6):v9[6*i+j]=v7[6*i+j]+unk_602080[6*i+j] #原函数识别一下数组for i in range(36):s.add(v8[i] == dword_602120[i])s.add(v9[i] == dword_6021C0[i])flag=[]
if s.check()==sat:r=s.model()for i in a1:flag.append(r[i].as_long())#BitVecNumRef转长整型print("".join(chr(x) for x in flag))
else:print("无解")
#hgame{1_think_Matr1x_is_very_usef5l}
参考
- z3学习 lancer0rz
相关文章:
z3基础学习
z3基础学习 z3是一个微软出品的开源约束求解器,能够解决很多种情况下的给定部分约束条件寻求一组满足条件的解的问题。 安装:pip install z3-solver 1. 简单使用 from z3 import * x Int(x) #创建名为x的int类型变量 y Int(y) solve(x y10,2*x…...
开发助手专业版,有反编译等多种功能
软件介绍 开发助手能够用来快速调试应用以及查看手机软硬件相关信息,包括:快速打开或关闭开发者选项中的选项。 将原来几十秒的操作缩短为一次点击。包括显示布局边界,显示 GPU 过度绘制。显示布局更新。强制 GPU 渲染 显示 GPU 视图更新&a…...
嵌入式初学-C语言-十一
#接嵌入式初学-C语言-十,以及部分例题# 循环结构 break和continue break 功能: 1. 用在switch中,用来跳出switch的case语句;如果case没有break,可能会产生case穿透。 2. 用在循环中(while、do..while、for..&#…...
浅谈几个常用OJ的注册方式
众所周知,好的OJ是成功的一半,但是有些英文OJ的注册很让人伤脑筋。 CodeForces 点进官网 戳这里 然后就会进入这个页面 在这一页里面里填写好信息即可 最后,一个邮件就会发到你的邮箱上,点击其中的链接即可激活账号 AtCoder …...
Html实现全国省市区三级联动
目录 前言 1.全国省市区的Json数据 2.找到Json数据文件(在此博文绑定资源)之后,放到resource目录下。 3.通过类加载器加载资源文件,读取Json文件 3.1 创建JsonLoader类 3.2 注入JsonLoader实体,解析Json文件 4.构建前端Html页面 5.通过…...
前端构建工具Webpack 与 Vite 大对比
在现代前端开发领域,构建工具扮演着至关重要的角色。它们不仅可以帮助我们管理项目依赖关系,还可以优化我们的代码,使其在生产环境中运行得更快更高效。其中两个最受欢迎的构建工具就是 Webpack 和 Vite。在这篇文章中,我们将深入…...
Ubuntu-22.04环境搭建
安装wget(一般ubuntu会自带) sudo apt-get install wget 更换国内软件源 先备份原来的/etc/apt/source.list⽂件 sudo cp /etc/apt/sources.list /etc/apt/sources.list.bak 防止修改错误 导致无可挽回 将下列国内镜像源 写入原来的/etc/apt/source.list⽂件(注…...
嵌入式学习---DAY17:共用体与位运算
链表剩余的一些内容 一、共用体 union 共用体名 名称首字母大写 { 成员表列; }; union Demo {int i;short s;char c; }; int main(void) {union Demo d;d.i 10;d.s 100;d.c 200;printf("%d\n", sizeof(d)); /…...
蓝牙网关和蓝牙MESH总结
可参考: https://zhuanlan.zhihu.com/p/695144946 蓝牙网关 参考: https://www.bilibili.com/read/cv28872282/ 蓝牙网关是一种特殊的网络设备,它能够实现蓝牙设备与互联网或其他类型网络之间的数据传输和通信。通过蓝牙网关,用户…...
了解关于标准化的知识
1.标准化组织 1.1国家标准化管理委员会(Standardization Administration of the Peoples Republic of China,简称SAC) TC--(Technical Committee) 技术委员会. SAC/TC,就是“国家标准化管理委员会”下属的一个专项或一个行业的“技术委员会或技术小组”&a…...
【云原生】数据库忘记密码怎么办?
相信很多人都会遇到在虚拟机中忘记数据库密码的情况,想必大家都很苦恼,所以今天给大家来讲讲数据库忘记密码了如何修改密码再登录数据库!!! 1、关闭数据库服务 systemctl stop mariadb 2、执行MySQL 服务器在启动时跳…...
Postman 接口测试详解
Postman 接口测试详解 Postman 接口测试详解1. Postman 基础知识1.1 什么是 Postman?1.2 Postman 的主要功能 2. 安装与设置2.1 安装 Postman2.2 创建 Postman 账户 3. Postman 的基本操作3.1 创建和发送请求3.2 解析响应数据3.3 使用环境和变量 4. 进阶功能4.1 编写…...
【JavaEE】线程状态
目录 前言 一.线程状态图 二.线程状态 1.初始状态(NEW) 2.运行状态(RUNNING) 3.等待状态(WAITING) 4.超时等待(TIMED_WAITING) 5.阻塞状态(BLOCKED) 6.终止状态(TERMINATED) 三.线程状态间的转换 四.总结 前言 线程状态及其状态转换…...
C++笔记之编译过程和面向对象
回顾: “abcd”//数据类型 字符串常量 const char *p"abc"; new STU const char *//8 指针的内存空间 int float 指针的内存空间 p 指针指向的内存空间 "abc" 取决于字符串长度 指针变量的内容一级指针 指针变量的地址二级指针 …...
ModuleNotFoundError: No module named ‘tqdm‘
报错信息: tqdm是一个快速、可扩展的Python进度条库,用于展示迭代器的长循环执行进度。 解决:通过以下命令安装 使用conda命令安装 conda install tqdm使用pip安装: pip install tqdm...
东京电影节公布2024年竞赛片评审团成员并对其业绩分别进行评介 没什么含金量
第37届东京国际电影节竞赛单元评审团名单正式公布。 周五,电影节组织者宣布,香港电影制片人杜琪峰、匈牙利电影制片人伊尔迪科恩耶迪、日本女演员桥本爱和法国女演员基娅拉马斯楚安尼将与之前宣布的评审团主席梁朝伟一起担任 2024 年主竞赛评审团成员。 …...
智能景区垃圾识别系统:基于YOLO的深度学习实现
基于深度学习的景区垃圾识别系统(UI界面YOLOv8/v7/v6/v5代码训练数据集) 1. 引言 景区垃圾识别是环保管理的重要任务之一。传统的人工清理方式效率低、成本高,而借助深度学习技术可以实现自动化的垃圾检测与识别,提高景区的清洁…...
ventoy和微pe可以共存吗?ventoy和pe共存使用教程
Ventoy新一代多系统启动U盘解决方案。国产开源U盘启动制作工具,支持Legacy BIOS和UEFI模式,理论上几乎支持任何ISO镜像文件,支持加载多个不同类型的ISO文件启动,无需反复地格式化U盘,插入U盘安装写入就能制作成可引导的…...
如何获取和安装SSL证书
SSL(Secure Sockets Layer)证书是用于加密网站服务器和客户端之间通信的一种数字证书。它通过HTTPS协议保护数据传输的安全性,防止数据被窃听或篡改。本文将指导您如何为您的网站获取并安装SSL证书。 步骤1:选择SSL证书提供商 首…...
makefile在IC设计中的使用笔记
1 makefile在IC设计中的地位 关于makefile的详细介绍可以参考第一个连接,里面的内容很多也很详细。但在数字IC设计中,并不会把所有的用法都用到,下面记录一下主要用到的规则。 2 IC设计涉及到的主要用法 2.1 变量的定义和使用 在makefile…...
连锁超市冷库节能解决方案:如何实现超市降本增效
在连锁超市冷库运营中,高能耗、设备损耗快、人工管理低效等问题长期困扰企业。御控冷库节能解决方案通过智能控制化霜、按需化霜、实时监控、故障诊断、自动预警、远程控制开关六大核心技术,实现年省电费15%-60%,且不改动原有装备、安装快捷、…...
【磁盘】每天掌握一个Linux命令 - iostat
目录 【磁盘】每天掌握一个Linux命令 - iostat工具概述安装方式核心功能基础用法进阶操作实战案例面试题场景生产场景 注意事项 【磁盘】每天掌握一个Linux命令 - iostat 工具概述 iostat(I/O Statistics)是Linux系统下用于监视系统输入输出设备和CPU使…...
Java多线程实现之Callable接口深度解析
Java多线程实现之Callable接口深度解析 一、Callable接口概述1.1 接口定义1.2 与Runnable接口的对比1.3 Future接口与FutureTask类 二、Callable接口的基本使用方法2.1 传统方式实现Callable接口2.2 使用Lambda表达式简化Callable实现2.3 使用FutureTask类执行Callable任务 三、…...
Java入门学习详细版(一)
大家好,Java 学习是一个系统学习的过程,核心原则就是“理论 实践 坚持”,并且需循序渐进,不可过于着急,本篇文章推出的这份详细入门学习资料将带大家从零基础开始,逐步掌握 Java 的核心概念和编程技能。 …...
【HarmonyOS 5 开发速记】如何获取用户信息(头像/昵称/手机号)
1.获取 authorizationCode: 2.利用 authorizationCode 获取 accessToken:文档中心 3.获取手机:文档中心 4.获取昵称头像:文档中心 首先创建 request 若要获取手机号,scope必填 phone,permissions 必填 …...
代理篇12|深入理解 Vite中的Proxy接口代理配置
在前端开发中,常常会遇到 跨域请求接口 的情况。为了解决这个问题,Vite 和 Webpack 都提供了 proxy 代理功能,用于将本地开发请求转发到后端服务器。 什么是代理(proxy)? 代理是在开发过程中,前端项目通过开发服务器,将指定的请求“转发”到真实的后端服务器,从而绕…...
Mobile ALOHA全身模仿学习
一、题目 Mobile ALOHA:通过低成本全身远程操作学习双手移动操作 传统模仿学习(Imitation Learning)缺点:聚焦与桌面操作,缺乏通用任务所需的移动性和灵活性 本论文优点:(1)在ALOHA…...
使用Matplotlib创建炫酷的3D散点图:数据可视化的新维度
文章目录 基础实现代码代码解析进阶技巧1. 自定义点的大小和颜色2. 添加图例和样式美化3. 真实数据应用示例实用技巧与注意事项完整示例(带样式)应用场景在数据科学和可视化领域,三维图形能为我们提供更丰富的数据洞察。本文将手把手教你如何使用Python的Matplotlib库创建引…...
RabbitMQ入门4.1.0版本(基于java、SpringBoot操作)
RabbitMQ 一、RabbitMQ概述 RabbitMQ RabbitMQ最初由LShift和CohesiveFT于2007年开发,后来由Pivotal Software Inc.(现为VMware子公司)接管。RabbitMQ 是一个开源的消息代理和队列服务器,用 Erlang 语言编写。广泛应用于各种分布…...
从面试角度回答Android中ContentProvider启动原理
Android中ContentProvider原理的面试角度解析,分为已启动和未启动两种场景: 一、ContentProvider已启动的情况 1. 核心流程 触发条件:当其他组件(如Activity、Service)通过ContentR…...
