z3库的安装

pip install z3_solver

注意要安装z3_solver库而不是z3

z3的作用

用于约束求解。

如果你已经知道了变量需要满足的若干条件，但是不想写for循环的暴力，那么就可以用这个库，你只需要告诉他变量需要满足的条件，它就可以告诉你满足条件的若干变量。

z3的基本使用模板

from z3 import *
a=Int('a')  #定义单个int型变量
b,c,d=Ints('b c d') #定义多个int型变量
s=Solver() #定义一个约束器
s.add(a+b==10,b-c==7)#添加约束条件,可以添加多个，也可以添加一个
s.add(a+c!=5)#s.add可以多次使用
print(s.check())#check就是求解，有解的话返回sat，无解返回unsat
print(s.model())#输出解，注意输出的时候不按照定义的顺序来，可以认为输出是无序的
'''
sat
[c = 0, a = 3, b = 7]
'''

这些模板中一些特殊的地方

定义变量

  1. 上面的模板中展示了int型变量的定义方法，但是要注意，int型变量无法使用位运算，如^ & |。

  2. 如果想用位运算怎么办？那就定义位向量

    a, b, c=BitVecs('a b c',32)

    a=BitVecs('a',32)

    以上就是定义位向量的方式，其中后面的参数指的是位向量的位数。

    另外需要注意的一点是，位向量好像是不能使用乘法的，如果一定要使用的话，要先转化成int型再去使用

    比如

    s.add(5*BV2Int(a)%3==4)

  3. 在逆向中不常使用的变量定义方式还有一种，定义实数变量（小数）

    y = Real('y')

  4. 如果想定义很多个变量怎么办？使用列表！

    x = [Int('x%s' % i) for i in range(0x22) ]

    如何使用？




    ## 添加约束条件

    模板中添加的约束调价都是和的关系，也就是都要满足，但是有时候我们希望添加或的关系，那我们应该怎么办？

    ``` s.add(Or(x + y > 3, x - y < 2))```

    这样就可以了

    ## 输出

    在逆向中，我们计算出来的变量往往是一个ASCLL码，我们希望将它们转化成可视字符，那应该如何操作？

    ```python
    for i in range(0,32):      #添加可视化字符的约束条件
        s.add(BV2Int(a1[i])<127)
        s.add(BV2Int(a1[i])>31)
    s.check()
    m=s.model()
    #print(m)
    res=''
    for i in range(0,32):
        res+=(chr(m[a1[i]].as_long()))
        
    print(res)

    后言

    值得注意的一点是，即使约束器求出来是多解，最终也只能输出一解，但是在逆向中往往只需要知道一个解就可以了（或者说题目条件的约束只能出来一个解），因此在本篇中本没有记录多解的输出方法。