z3笔记

Last updated on January 30, 2024 am

记录一些z3食用方式

1. 变量定义

1
2
3
4
5
6
7
8
9
10
# 定义一个整型变量
x = Int('x')
# 定义两个实数型变量，
a, b = Reals('a b')
# 定义一个32位向量
eax = BitVec('eax', 32)
# 定义两个32位向量
ebx, ecx = BitVecs('ebx ecx', 32)
# 定义一组变量列表
X = [Int('x_%s' % i) for i in range(8)]

2.逻辑相关

And与Or

1
2
3
4
5
6
7
8
9
10
11
12
x = Int('x')
y = Int('y')

# 或逻辑，两者满足其一
constrains1 = Or(x < 0, x > 5)
# 与逻辑，两者均要满足
constrains2 = And(1 < y, y < 10)
# 取反
constrains3 = Not(x < -1)

s = Solver()
s.add(constrains1, constrains2)

IF

1
2
3
4
5
x = Int('x')
y = Int('y')
s = Solver()
# 添加If约束
s.add(If(y > 10, x == 115, x == 1))

3.输出相关

式子

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
x = Int('x')
y = Int('y')
z = Int('z')

n = x + y + z == 3

# 输出子式数目
print(n.num_args())
>>> 2

# 输出表达式的子式
print(n.children())
>>> [x + y + z, 3]

# 输出具体子式
print(n.arg(0))
>>> x+y+Z
print(n.arg(1))
>>> 3

# 输出具体操作
print(n.decl())
>>> ==

输出具体值设置

1
2
3
4
5
6
7
8
9
10
11
12
13
14
x = Real('x')
# 输出分数
solve(3*x == 1)
>>> [1/3]

# 输出十进制数
set_option(rational_to_decimal=True)
solve(3*x == 1)
>>> [x = 0.3333333333?]

# 设定小数位数
set_option(precision=30)
solve(3*x == 1)
>>> [x = 0.333333333333333333333333333333?]

输出约束

1
2
3
4
5
6
7
8
9
10
x = Real('x')
y = Real('y')
s = Solver()
s.add(x > 1, y > 1, Or(x + y > 3, x - y < 2))
# 输出约束条件 可以用来验证约束设定的对不对
for c in s.assertions():
    print(c)
>>> x > 1
>>> y > 1
>>> Or(x + y > 3, x - y < 2)

取解、解的转化

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
x, y, z = Reals('x y z')
s = Solver()
s.add(x > 1, y > 1, x + y > 3, z - x < 10)

s.check()
m = s.model()
# 取特定的值
print("x = %s" % m[x])

# 取出所有的值
for d in m.decls():
    print("%s = %s" % (d.name(), m[d]))
    
# 对于Int，BitVec型可以这样将值转化为python int
x_int = x.as_long()

# 对于Real型可以这样将值转化为python float
x_float = x.as_decimal(10) #括号中是保留小数位数

4.列表

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
# 创建一个包含五个变量的列表
X = [ Int('x%s' % i) for i in range(5) ]
Y = [ Int('y%s' % i) for i in range(5) ]
print (X)

# 创建一个包含五个运算的列表
X_plus_Y = [ X[i] + Y[i] for i in range(5) ]
print (X_plus_Y)

# 创建一个包含五个约束的列表
X_gt_Y = [ X[i] > Y[i] for i in range(5) ]
print (X_gt_Y)

print (And(X_gt_Y))

# 创建多维的变量
X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(3) ] 
      for i in range(3) ]
pp(X)

5.例子

（1）数独

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
from z3 import *

# 创建9*9的列表存储变量
x = [[Int("x_%s_%s" % (i + 1, j + 1)) for j in range(9)] for i in range(9)]

# 对一个变量限定在取值范围
bounds = [And(1 <= x[i][j], x[i][j] <= 9) for i in range(9) for j in range(9)]

# 每一行不能有相同元素，Distinct即为添加约束两两不同
rows = [Distinct(x[i]) for i in range(9)]

# 每一列不能有相同元素
cols = [Distinct([x[i][j] for i in range(9)]) for j in range(9)]

# 每一个九宫格不能有相同元素
sq = [Distinct([x[3 * ii + i][3 * jj + j]
                for i in range(3) for j in range(3)])
      for ii in range(3) for jj in range(3)]

base_rules = bounds + rows + cols + sq

# 数独矩阵，为0的即为没有填的
instance = ((0, 0, 0, 0, 9, 4, 0, 3, 0),
            (0, 0, 0, 5, 1, 0, 0, 0, 7),
            (0, 8, 9, 0, 0, 0, 0, 4, 0),
            (0, 0, 0, 0, 0, 0, 2, 0, 8),
            (0, 6, 0, 2, 0, 1, 0, 5, 0),
            (1, 0, 2, 0, 0, 0, 0, 0, 0),
            (0, 7, 0, 0, 0, 0, 5, 2, 0),
            (9, 0, 0, 0, 6, 5, 0, 0, 0),
            (0, 4, 0, 9, 7, 0, 0, 0, 0))

# 利用If语句将棋盘元素映射为z3类型
instance_c = [If(instance[i][j] == 0,
                 True,
                 x[i][j] == instance[i][j])
              for i in range(9) for j in range(9)]

s = Solver()

s.add(base_rules + instance_c)

if s.check() == sat:
    m = s.model()
    r = [[m.evaluate(x[i][j]) for j in range(9)]
         for i in range(9)]
    print_matrix(r)

else:
    print("failed to solve")

（2）hackgame2023 小z的谜题

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
from z3 import *
import itertools

bound = 5
constraints = ((1, 1, 3), (1, 2, 2), (1, 2, 4), (1, 4, 4), (2, 2, 2), (2, 2, 3))
count = [3, 4, 2, 2, 2, 3]
num_constraints = sum(count)
num_dims = len(constraints[0])

# 创建16*3*3的列表存储变量
arrange = [[[Int('x_%s_%s_%s' % (k + 1, j + 1, i + 1)) for i in range(3)] for j in range(3)] for k in range(16)]

solver = Solver()

# Stage 0
# 添加约束一
for i in range(16):
    for j in range(3):
        for k in range(3):
            if k == 2:
                solver.add(arrange[i][j][k] == -1)
            else:
                solver.add(0 <= arrange[i][j][k])
                solver.add(arrange[i][j][k] <= bound)

# Stage 2
# 添加约束二，因为满足其一即可，所以是Or的关系
for i in range(16):
    for j in range(16):
        if i == j:
            continue
        solver.add(
            Or([(Or(arrange[i][k][1] <= arrange[j][k][0], arrange[j][k][1] <= arrange[i][k][0])) for k in range(3)]))

# Stage 3
# 添加约束三，这里的核心思想是，只要每一行能够满足其中一个
# ((1, 1, 3), (1, 2, 2), (1, 2, 4), (1, 4, 4), (2, 2, 2), (2, 2, 3))
# 即可，同时也有数量约束，利用count[t]实现对这此约束
for i in range(16):
    for t in range(6):
        if count[t]:
            g = []
            for p in set(itertools.permutations(constraints[t])):
                o = []
                for j in range(3):
                    o.append(arrange[i][j][1] - arrange[i][j][0] == p[j])
                g.append(And(o))

            solver.add(Or(g))
            count[t] -= 1
            break


 
# 计算分数
# 这里计算分数方式是每一行能产生多少种笛卡尔积，16行再做累计
# 因此只需要每一行的每一种笛卡尔积能够对应所有笛卡尔积中的一种即可
# 耗时操作主要就在这一步
g = []
for x0, y0, z0 in itertools.product(*([list(range(-1, bound + 1))] * 3)):
    t = []
    for i in range(16):
        for x1, y1, z1 in itertools.product(*arrange[i]):
            o = [x0 == x1, y0 == y1, z0 == z1]
            t.append(And(o))
    g.append(Or(t))


# 统计有多少种笛卡尔积
s = Sum([If(i, 1, 0) for i in g])

# 控制分数
solver.add(s >= 157)

if solver.check() == z3.sat:
    ans = solver.model()
    for i in range(16):
        for j in range(3):
            for k in range(3):
                arrange[i][j][k] = ans[arrange[i][j][k]].as_long()

    arrange.sort()
    print(''.join([str(arrange[i][j][k]) for i in range(num_constraints) for j in range(num_dims) for k in range(2)]))

print(arrange)

(3) FlipGame 脚本

题源强网杯 HappyChess

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
from z3 import *

puzzle = """●○○○○○○○●
●●○●○○○○●
○○●○●○●○●
●●●○○○○●○
●●●○○●○●●
○●○○●○○●●
○●○○○○○○●
●●●●●○●●●
●○○○●●○○●"""
puzzle = puzzle.split('\n')
state = [[0 for i in range(9)] for j in range(9)]

for i in range(9):
    for j in range(9):
        if puzzle[i][j] == '○':
            state[i][j] = 1
        else:
            state[i][j] = 0

switches = [[BitVec("s_%d_%d" % (i, j), 1) for i in range(1, 10)] for j in range(1, 10)]
s = Solver()
for row in range(9):
    for col in range(9):
        t = 0
        for p in switches[row][:]:
            t ^= p
        for p in switches[:][col]:
            t ^= p
        t ^= switches[row][col]
        s.add(t == state[row][col])

s_list = list()

final = 0
temp = 9999999

while s.check() == sat:
    m = s.model()
    s.add(Or([switches[i][j] != m[switches[i][j]] for i in range(9) for j in range(9)]))

    summ = 0
    for pp in m:
        summ += m[pp].as_long()
    if summ < temp and summ != 0:
        temp = summ
        final = m
    if 24 > summ > 0:
        final = m
        print(summ)
        break

index = 0
for i in range(9):
    for j in range(9):
        if final[switches[i][j]].as_long() == 1:
            index += 1
            print("({},{})".format(i + 1, j + 1))

print(index)
# icq2f196f4f5398cc97a74d8b1032027

CTF > Reverse > notes
#z3
z3笔记
http://example.com/2023/11/07/z3_study/
Author
yring
Posted on
November 7, 2023
Licensed under