Python Z3安装和使用

听说Z3在CTF中很好用，于是决定试一试

安装

尝试使用 pip install z3-resolver结果报错：

  ERROR: Could not find a version that satisfies the requirement z3-solver (from versions: none)
ERROR: No matching distribution found for z3-solver

于是直接下载：whell文件并安装
安装成功（但是很奇怪的一点，我的电脑是64位的，我却需要使用32位的版本）

C:\Users\Administrator\Downloads>pip install z3_solver-4.8.7.0-py2.py3-none-win32.whl
Processing c:\users\administrator\downloads\z3_solver-4.8.7.0-py2.py3-none-win32.whl
Installing collected packages: z3-solver
Successfully installed z3-solver-4.8.7.0

导入pycharm ,ok!

简单使用

from z3 import *

x = Int('x')
y = Int('y')
solve(x > 2, y < 10, x + 2*y == 7)

确实能用。

用来解题

用它来解一下攻防世界中的RE第一题，

结果发现并不能行，貌似是因为他的代码中包含了判断 ，所以会报错。。

from z3 import *


def getEncrypt(input):
    if input>57 or input<48:
        if input>122 or input<97:
            return input-29
        else:
            return input-87
    else:
        return input-48

abc='abcdefghiABCDEFGHIJKLMNjklmn0123456789opqrstuvwxyzOPQRSTUVWXYZ'
crypt='KanXueCTF2019JustForhappy'

input= [ Int('x%s' % i) for i in range(len(crypt)) ]

def getResult(int_list):
    crypted=''
    for ele in int_list:
        crypted+=abc[ele];
    return crypted;

solver= Solver()
for i in range(len(crypt)):
    solver.add(abc[getEncrypt(input[i])]==crypt[i]);
print(solver.model())
m=solver.check()
print(m)

报错如下：

z3.z3types.Z3Exception: Symbolic expressions cannot be cast to concrete Boolean values.

看起来这东西还是更适合有很多数学表达式的那种题目？