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

理解 MCP 工作流:使用 Ollama 和 LangChain 构建本地 MCP 客户端
🌟 什么是 MCP? 模型控制协议 (MCP) 是一种创新的协议,旨在无缝连接 AI 模型与应用程序。 MCP 是一个开源协议,它标准化了我们的 LLM 应用程序连接所需工具和数据源并与之协作的方式。 可以把它想象成你的 AI 模型 和想要使用它…...

渗透实战PortSwigger靶场-XSS Lab 14:大多数标签和属性被阻止
<script>标签被拦截 我们需要把全部可用的 tag 和 event 进行暴力破解 XSS cheat sheet: https://portswigger.net/web-security/cross-site-scripting/cheat-sheet 通过爆破发现body可以用 再把全部 events 放进去爆破 这些 event 全部可用 <body onres…...

高频面试之3Zookeeper
高频面试之3Zookeeper 文章目录 高频面试之3Zookeeper3.1 常用命令3.2 选举机制3.3 Zookeeper符合法则中哪两个?3.4 Zookeeper脑裂3.5 Zookeeper用来干嘛了 3.1 常用命令 ls、get、create、delete、deleteall3.2 选举机制 半数机制(过半机制࿰…...
vue3 定时器-定义全局方法 vue+ts
1.创建ts文件 路径:src/utils/timer.ts 完整代码: import { onUnmounted } from vuetype TimerCallback (...args: any[]) > voidexport function useGlobalTimer() {const timers: Map<number, NodeJS.Timeout> new Map()// 创建定时器con…...

RNN避坑指南:从数学推导到LSTM/GRU工业级部署实战流程
本文较长,建议点赞收藏,以免遗失。更多AI大模型应用开发学习视频及资料,尽在聚客AI学院。 本文全面剖析RNN核心原理,深入讲解梯度消失/爆炸问题,并通过LSTM/GRU结构实现解决方案,提供时间序列预测和文本生成…...
【Go语言基础【12】】指针:声明、取地址、解引用
文章目录 零、概述:指针 vs. 引用(类比其他语言)一、指针基础概念二、指针声明与初始化三、指针操作符1. &:取地址(拿到内存地址)2. *:解引用(拿到值) 四、空指针&am…...

【QT控件】显示类控件
目录 一、Label 二、LCD Number 三、ProgressBar 四、Calendar Widget QT专栏:QT_uyeonashi的博客-CSDN博客 一、Label QLabel 可以用来显示文本和图片. 核心属性如下 代码示例: 显示不同格式的文本 1) 在界面上创建三个 QLabel 尺寸放大一些. objectName 分别…...

【threejs】每天一个小案例讲解:创建基本的3D场景
代码仓 GitHub - TiffanyHoo/three_practices: Learning three.js together! 可自行clone,无需安装依赖,直接liver-server运行/直接打开chapter01中的html文件 运行效果图 知识要点 核心三要素 场景(Scene) 使用 THREE.Scene(…...

Spring是如何实现无代理对象的循环依赖
无代理对象的循环依赖 什么是循环依赖解决方案实现方式测试验证 引入代理对象的影响创建代理对象问题分析 源码见:mini-spring 什么是循环依赖 循环依赖是指在对象创建过程中,两个或多个对象相互依赖,导致创建过程陷入死循环。以下通过一个简…...

vue3 手动封装城市三级联动
要做的功能 示意图是这样的,因为后端给的数据结构 不足以使用ant-design组件 的联动查询组件 所以只能自己分装 组件 当然 这个数据后端给的不一样的情况下 可能组件内对应的 逻辑方式就不一样 毕竟是 三个 数组 省份 城市 区域 我直接粘贴组件代码了 <temp…...