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…...
基于算法竞赛的c++编程(28)结构体的进阶应用
结构体的嵌套与复杂数据组织 在C中,结构体可以嵌套使用,形成更复杂的数据结构。例如,可以通过嵌套结构体描述多层级数据关系: struct Address {string city;string street;int zipCode; };struct Employee {string name;int id;…...

业务系统对接大模型的基础方案:架构设计与关键步骤
业务系统对接大模型:架构设计与关键步骤 在当今数字化转型的浪潮中,大语言模型(LLM)已成为企业提升业务效率和创新能力的关键技术之一。将大模型集成到业务系统中,不仅可以优化用户体验,还能为业务决策提供…...
解锁数据库简洁之道:FastAPI与SQLModel实战指南
在构建现代Web应用程序时,与数据库的交互无疑是核心环节。虽然传统的数据库操作方式(如直接编写SQL语句与psycopg2交互)赋予了我们精细的控制权,但在面对日益复杂的业务逻辑和快速迭代的需求时,这种方式的开发效率和可…...
oracle与MySQL数据库之间数据同步的技术要点
Oracle与MySQL数据库之间的数据同步是一个涉及多个技术要点的复杂任务。由于Oracle和MySQL的架构差异,它们的数据同步要求既要保持数据的准确性和一致性,又要处理好性能问题。以下是一些主要的技术要点: 数据结构差异 数据类型差异ÿ…...

如何将联系人从 iPhone 转移到 Android
从 iPhone 换到 Android 手机时,你可能需要保留重要的数据,例如通讯录。好在,将通讯录从 iPhone 转移到 Android 手机非常简单,你可以从本文中学习 6 种可靠的方法,确保随时保持连接,不错过任何信息。 第 1…...

【单片机期末】单片机系统设计
主要内容:系统状态机,系统时基,系统需求分析,系统构建,系统状态流图 一、题目要求 二、绘制系统状态流图 题目:根据上述描述绘制系统状态流图,注明状态转移条件及方向。 三、利用定时器产生时…...

九天毕昇深度学习平台 | 如何安装库?
pip install 库名 -i https://pypi.tuna.tsinghua.edu.cn/simple --user 举个例子: 报错 ModuleNotFoundError: No module named torch 那么我需要安装 torch pip install torch -i https://pypi.tuna.tsinghua.edu.cn/simple --user pip install 库名&#x…...

2025年渗透测试面试题总结-腾讯[实习]科恩实验室-安全工程师(题目+回答)
安全领域各种资源,学习文档,以及工具分享、前沿信息分享、POC、EXP分享。不定期分享各种好玩的项目及好用的工具,欢迎关注。 目录 腾讯[实习]科恩实验室-安全工程师 一、网络与协议 1. TCP三次握手 2. SYN扫描原理 3. HTTPS证书机制 二…...
作为测试我们应该关注redis哪些方面
1、功能测试 数据结构操作:验证字符串、列表、哈希、集合和有序的基本操作是否正确 持久化:测试aof和aof持久化机制,确保数据在开启后正确恢复。 事务:检查事务的原子性和回滚机制。 发布订阅:确保消息正确传递。 2、性…...

水泥厂自动化升级利器:Devicenet转Modbus rtu协议转换网关
在水泥厂的生产流程中,工业自动化网关起着至关重要的作用,尤其是JH-DVN-RTU疆鸿智能Devicenet转Modbus rtu协议转换网关,为水泥厂实现高效生产与精准控制提供了有力支持。 水泥厂设备众多,其中不少设备采用Devicenet协议。Devicen…...