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…...

Chapter03-Authentication vulnerabilities
文章目录 1. 身份验证简介1.1 What is authentication1.2 difference between authentication and authorization1.3 身份验证机制失效的原因1.4 身份验证机制失效的影响 2. 基于登录功能的漏洞2.1 密码爆破2.2 用户名枚举2.3 有缺陷的暴力破解防护2.3.1 如果用户登录尝试失败次…...
反向工程与模型迁移:打造未来商品详情API的可持续创新体系
在电商行业蓬勃发展的当下,商品详情API作为连接电商平台与开发者、商家及用户的关键纽带,其重要性日益凸显。传统商品详情API主要聚焦于商品基本信息(如名称、价格、库存等)的获取与展示,已难以满足市场对个性化、智能…...

UDP(Echoserver)
网络命令 Ping 命令 检测网络是否连通 使用方法: ping -c 次数 网址ping -c 3 www.baidu.comnetstat 命令 netstat 是一个用来查看网络状态的重要工具. 语法:netstat [选项] 功能:查看网络状态 常用选项: n 拒绝显示别名&#…...

SAP学习笔记 - 开发26 - 前端Fiori开发 OData V2 和 V4 的差异 (Deepseek整理)
上一章用到了V2 的概念,其实 Fiori当中还有 V4,咱们这一章来总结一下 V2 和 V4。 SAP学习笔记 - 开发25 - 前端Fiori开发 Remote OData Service(使用远端Odata服务),代理中间件(ui5-middleware-simpleproxy)-CSDN博客…...

LINUX 69 FTP 客服管理系统 man 5 /etc/vsftpd/vsftpd.conf
FTP 客服管理系统 实现kefu123登录,不允许匿名访问,kefu只能访问/data/kefu目录,不能查看其他目录 创建账号密码 useradd kefu echo 123|passwd -stdin kefu [rootcode caozx26420]# echo 123|passwd --stdin kefu 更改用户 kefu 的密码…...

人工智能(大型语言模型 LLMs)对不同学科的影响以及由此产生的新学习方式
今天是关于AI如何在教学中增强学生的学习体验,我把重要信息标红了。人文学科的价值被低估了 ⬇️ 转型与必要性 人工智能正在深刻地改变教育,这并非炒作,而是已经发生的巨大变革。教育机构和教育者不能忽视它,试图简单地禁止学生使…...

【JVM】Java虚拟机(二)——垃圾回收
目录 一、如何判断对象可以回收 (一)引用计数法 (二)可达性分析算法 二、垃圾回收算法 (一)标记清除 (二)标记整理 (三)复制 (四ÿ…...

【MATLAB代码】基于最大相关熵准则(MCC)的三维鲁棒卡尔曼滤波算法(MCC-KF),附源代码|订阅专栏后可直接查看
文章所述的代码实现了基于最大相关熵准则(MCC)的三维鲁棒卡尔曼滤波算法(MCC-KF),针对传感器观测数据中存在的脉冲型异常噪声问题,通过非线性加权机制提升滤波器的抗干扰能力。代码通过对比传统KF与MCC-KF在含异常值场景下的表现,验证了后者在状态估计鲁棒性方面的显著优…...
MySQL 主从同步异常处理
阅读原文:https://www.xiaozaoshu.top/articles/mysql-m-s-update-pk MySQL 做双主,遇到的这个错误: Could not execute Update_rows event on table ... Error_code: 1032是 MySQL 主从复制时的经典错误之一,通常表示ÿ…...

数据结构:递归的种类(Types of Recursion)
目录 尾递归(Tail Recursion) 什么是 Loop(循环)? 复杂度分析 头递归(Head Recursion) 树形递归(Tree Recursion) 线性递归(Linear Recursion)…...