就题论题吧罢了, 后续做题如果遇到新的错误,我会更新文章

我写错了,就告诉我,我的QQ 935797872

安装有问题可以问我

我写错了,就告诉我,

我很愿意与志同道合的人结为朋友

一.准备工作

---

---

你要去下载z3呀!

首先去百度一下命令行下载z3,你就知道怎么安装z3了,好像好像是pip install z3-solver...还是去百度吧

好吧,直接在cmd窗口就可以安装,如果下载慢就退出,换手机热点试一下

pip install z3-solver

然后你就可以直接直接直接在vscode那里使用,我不喜欢用pycharm,vscode挺好,另外你要记住,z3的使用必须是python3.8及一下,你的python3.9什么的无法用

另外,你下载z3完的时候,它可能会报错,它叫你更新一些东西,你就跟着上面的东西照做就行了,如果你用的vscode,z3安装成功后,它会自动代码高亮一些关键字,比如check,modei...

二.基本语法

1.引入头文件

from z3 import*

2.生成一个解题器,名字叫做 flag,注意那里面有个大写'S'

from z3 import*
flag=Solver()

3.声明单个未知参数的类型

x = Int('x')
x,y=Ints('x y') #这里有个Ints

s= BitVec('s',8)
s1,s2 = BitVec('s1 s2',8)
'''这里的8是参数是8bit的,也就是参数大小是1字节byte,写16,就是2字节,到底用8还是用16,看题目对未知数的要求怎么样'''

我们常常会用到BitVec型变量,通常只有这种类型可以进行位运算的操作,也就是那些

>> <<  | & ~ ^ 运算就要用BitVec的变量类型

4.一个数组作为参数,很重要,节约时间

s= [BitVec('%d'%i,8) for i in range(18)]
s= [BitVec('s[%d]'%i,8) for i in range(18)]

那个%d应该类似于c语言

,那个16与8是bit位1

这里就是定义了一个长度18的数组s,于是我们就直接用s[1],s[2]....

对于第2种写法,其实就是你在答案的输出时会多一个s[i]罢了,比如下面就是第2种写法

[s[1] = 90,
 s[3] = 123,
....
 s[13] = 77,
 s[16] = 78]

对于第一种写法,输出样子如下

[70, 90, 81, 123, 90, 97, 95, 74, 105, 97, 110, 103, 95, 77, 105, 65, 78, 125]

5.x.add( )添加解题的约束条件

 s.add(cmp[j]==table[(s[i]>>2)^0x34])

值得我们注意的是add()里面只能放判断型语句,不能放赋值语句

6.检查是否有解并且输出

if x.check() == sat: 
    flag_result = solver.model() 
    print(flag_result)
else:
    print("no flag_result!")

这里的sat就是satisface满足的意思

7.check()

来检测解的情况，

8.model()

在存在解的时候，求解的交集,除非只有解只有一个

二.谈一下注意事项(很重要)

1.忽略C代码转化为python的byte,bit,word的约束范围

"在c语言中"
v3 = (unsigned __int8)(flag >> 7) >> 4;

z3就是这样(对__int8做处理)取&0xff,0xff=255,就是一个字节的范围大小

"在python中"
v3 =(((s[i] >> 7)&0xff) >> 4)&0xff

2未知数字节范围设置

        比如16bit与8bit

3.未考虑输出ascill可见字符范围

for i in range(18):
    ....
    x.add(s[i]>=20)
    x.add(s[i]<=127)

4.谈一下输出的技巧

我们常常会遇到输出的解是乱序的,好比下面

[s[1] = 90,
 s[3] = 123,
 s[8] = 105,
 .....
 s[13] = 77,
 s[16] = 78]

我们要让它按照顺序输出

声明另外一个数组,他就按顺序写入到flag数组

头部
s= [BitVec('%d'%i,8) for i in range(18)]
尾部
先声明一个数组
flag=[]
if x.check() == sat: 
    ans = x.model()
    for i in s:      
        flag.append(ans[i])

5.我遇到的sb问题

1.好像z3不能对下标设置位置变量

2.因为我没有学过python,下面这样写是错的

 if(chr('97')=='a'):
     print("yes")
  else:
     print("no")