基本数据类型

在python使用Z3模块，一半使用以下几种数据类型：

Int相对应int

Real 有理数

Bool 布尔类型

Array 数组

BitVec('a',8)向量

其中BitVec可以制定大小的数据类型，不一定是八位，例如在C语言中的int可以用BitVec('a',32)表示

基础用法

• Solver()创建一个通用求解器，以进行下一步求解
• add()添加约束条件，通常在sovler（）之后，添加约束条件通常是一个逻辑等死
• check()添加所有约束条件后，来检测是否有解，有解返回set，无解返回unsat
• model()存在解的时候，该函数会奖每个限制条件所对应的解集的交集，从而得出正解
• 分别对应设未知数，列方程，判断方程是否有解，解方程组

简单使用

案例1：

假设有方程组

30x+15y=675
12+5y=265

from z3 import *
s=Solver()
x,y=Ints("x y")
s.add(30*x+15*y==675)
s.add(12*x+5*y==265)
if s.check() == sat:
    print(s.model())

如果要取某一个x或者y

from z3 import *
s=Solver()
x,y=Ints("x y")
s.add(30*x+15*y==675)
s.add(12*x+5*y==265)
if s.check() == sat:
    _solve=s.model()
    print(_solve[x])

案例2

from z3 import *
dog,cat,mouse =Ints("dog cat mouse")
s=Solver()
s.add(dog>=1,cat>=1,mouse>=1)
s.add(dog*10+cat*3+mouse*0.5==100)
s.add(dog+cat+mouse==100)
if s.check()==sat:
    print(s.model())

案例3

小李的弟弟比小李小2岁，小王的哥哥比小王大2岁，比小李大5岁。1994年，小李和弟弟和小王的年龄之和为15，问2024年小李与小王的年龄分别为多少岁

设2014年小李年龄为a;小李弟弟年龄为b,小王年龄为c，小王哥哥年龄为d

from z3 import *
a,b,c,d=Ints("a b c d")
s=Solver()
s.add(b==a-2)
s.add(d==c+2)
s.add(d==a+5)
s.add(b-20+c-20==15)

if s.check() == sat:
    print(s.model())

存在多解的情况把所有解打印出来

from z3 import *
a,b,c,d=Ints("a b c d")
s=Solver()
s.add(b==a-2)
s.add(d==c+2)
s.add(d==a+5)

while s.check() == sat:
    m=s.model()
    print(m)
    s.add(a!=m[a])
    s.add(b != m[b])
    s.add(c != m[c])
    s.add(d != m[d])

例题分析 [ACTF新生赛2020]Universe_final_answer

进入main函数发现有个check函数

进区看，里面有一串方程

一共10个未知数

把方程提出来，整理一遍

from z3 import *
a1=[BitVec(str(i),8)  for i in range(10)]#初始z3的10个向量,长度为8 长度改长一点也是没问题的
v1 = a1[1]
v2 = a1[0]
v3 = a1[2]
v4 = a1[3]
v5 = a1[4]
v6 = a1[6]
v7 = a1[5]
v8 = a1[7]
v9 = a1[8]
v11 = a1[9]
s=Solver()


for x in a1:
    s.add(x >= 32, x <= 126)##添加约数条件约束到可打印字符
    
s.add(-85 * v9 + 58 * v8 + 97 * v6 + v7 + -45 * v5 + 84 * v4 + 95 * v2 - 20 * v1 + 12 * v3 == 12613)
s.add(30 * v11 + -70 * v9 + -122 * v6 + -81 * v7 + -66 * v5 + -115 * v4 + -41 * v3 + -86 * v1 - 15 * v2 - 30 * v8 == -54400)
s.add(-103 * v11 + 120 * v8 + 108 * v7 + 48 * v4 + -89 * v3 + 78 * v1 - 41 * v2 + 31 * v5 - (v6 << 6) - 120 * v9 == -10283)
s.add(71 * v6 + (v7 << 7) + 99 * v5 + -111 * v3 + 85 * v1 + 79 * v2 - 30 * v4 - 119 * v8 + 48 * v9 - 16 * v11 == 22855)
s.add(5 * v11 + 23 * v9 + 122 * v8 + -19 * v6 + 99 * v7 + -117 * v5 + -69 * v3 + 22 * v1 - 98 * v2 + 10 * v4 == -2944)
s.add(-54 * v11 + -23 * v8 + -82 * v3 + -85 * v2 + 124 * v1 - 11 * v4 - 8 * v5 - 60 * v7 + 95 * v6 + 100 * v9 == -2222)
s.add(-83 * v11 + -111 * v7 + -57 * v2 + 41 * v1 + 73 * v3 - 18 * v4 + 26 * v5 + 16 * v6 + 77 * v8 - 63 * v9 == -13258)
s.add(81 * v11 + -48 * v9 + 66 * v8 + -104 * v6 + -121 * v7 + 95 * v5 + 85 * v4 + 60 * v3 + -85 * v2 + 80 * v1 == -1559)
s.add(101 * v11 + -85 * v9 + 7 * v6 + 117 * v7 + -83 * v5 + -101 * v4 + 90 * v3 + -28 * v1 + 18 * v2 - v8 == 6308)


if s.check() == sat:
    m=s.model()
    flag = "".join([chr(m[unk].as_long()) for unk in a1])
    print(flag)

把结果F0uRTy_7w@给回程序就可以得到flag

actf{F0uRTy_7w@_42}