z3求解器使用

CTF逆向碰到几次用到z3求解器的题，如果算法便于表达式描述的话，可以直接使用z3求解，另外一般这种题都是很多位运算与循环的结合算法。例如des等。

github文档：Z3Prover/doc: Documentation (github.com)

z3库名为z3_solver，安装使用：

1
pip install z3_solver

或者下载whl包(包含中文简单使用文档)：

z3_whl.zip下载

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
# coding : utf-8

from z3 import *


x = Int('x')  #声明未知数，类型是整数类型Int
y = Int('y')
solve(x > 2, y < 10, x + 2 * y == 7)
# 输出 [y = 0, x = 7]

# =================================================================================================

# 声明整数
x = Int('x')
# 声明实数
x = Real('x')
# 声明布尔类型
x = Bool('x')
# ...
x = BitVec('x', 8)
# 批量声明未知数加s

# =================================================================================================

# 更改类型
# IntVal() # 返回Z3整数
# RealVal() # 返回Z3实数
# RatVal() # 返回Z3有理数值

# =================================================================================================

# 函数化简
simplify(x + y + 2 * x + 3)
# 3 + 3*x + y

simplify(x < y + x + 2)
# Not(y <= -2)

simplify(And(x + 1 >= 3, x**2 + x**2 + y**2 + 2 >= 5))
# And(x >= 2, 2*x**2 + y**2 >= 3)


simplify((x + 1)*(y + 1), som=True) # sum-of-monomials： 单项式的和
# 1 + x + y + 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


'''
simplify( <表达式> )  #对表达式进行化简
simplify( <表达式>, som=True)   #sum-of-monomials： 单项式的和 将表达式转成单项式的和
simplify( <表达式>, mul_to_power=True)   # mul_to_power 将乘法转换为乘方
'''


Q(1, 3) # 返回有理数 a/b
# 1/3


set_param() # 函数配置全局变量

# >>> solve(x**2 + y**2 == 3, x**3 == 2)
# [x = 1.2599210498?, y = -1.1885280594?]

set_param(precision=30)   #保留30位的小数

# >>> solve(x**2 + y**2 == 3, x**3 == 2)
# [x = 1.259921049894873164767210607278?, y = -1.188528059421316533710369365015?]

set_param(rational_to_decimal=True) # 以十进制形式表示有理数


'''
>>> from z3 import *
>>> x = Int('x')
>>> y = Int('y')
>>> s = Solver()
#创造一个通用solver
>>> type(s)
# Solver 类
<class ' Z3. z3. Solver'>

>>> s.add(x>10,y==x+2)  #添加约束到solver 中
>>> s
[x>10,y==x+2]
>>> s.check()   #检查solver中的约束 是否满足
sat   # satisfiable/满足

>>> s. push( )   #创建一个回溯点，即将当前栈的大小保存下来

>>> s.add(y < 11)
>>> s
[x>10,y==x+2，y<11]

>>> s.check()
unsat   # unsatisfiable/不满足

>>> s. pop(num=1)   #回溯num个点
>>> s
[x>10，y==X+2]
>>> s. check()
sat

>>> for C in s.assertions():
# assertions() 返回一个包含所有约束的AstVector

>>> s. statistics( )
# statistics() 返回最后一个check() 的统计信息
(   :max- memory     6.26
    :memory          4.37
    :mk -bool -var   1
    :num- al locs   331960806
    :rlimit-count 7016)
>>> m = s.model( )   # model() 返回最后一个check() 的model
>>> type(m)   # ModelRef 类
<class ' Z3. z3. ModelRef '>
>>> m
[x=11,y=13]
>>> for d in m.dec1s():   # decls()返回model包含了所有符号的列表
print("%S = %S" % (d.name()，m[d]))
x=11
y=13
'''
'''
Z3约束器使用流程

创建变量
例:
x = Int('x')
y = Int('y')

创建solver求解器
例：s = Solver()

添加约束条件
例：s.add(x+y==10)

检查solver中的约束是否满足
例：s.check()

利用model()输出运算结果
例：s.model()
'''



Page View
2021-11-22
Contents
⬆︎TOP