Z3，打 CTF 好用工具
這是我前陣子學到的好用工具 - Z3
解 CTF 某些題目真的爆快XD
那麼深入的解題我還沒學會
但基礎的解國中數學二元一次方程式之類也超快，可以拿來做簡單小練習，增加爽快感
故事起因於我的母親傳給我一張那種長輩們都會流傳的奇怪數學圖
通常這種圖片都是耍人的腦筋急轉彎型
但我非常認真的當作一般數學題目將代數代入
看到題目長這樣
a + b = 12
c - d = 9
a + c = 22
b + d = 12
嗯?
這好像可以拿來用 Z3 玩玩看欸!!
於是開始拿之前的範例數學題做修改
卡在該怎麼宣告未知數
之前練習題的未知數是用Int宣告
已知這題的四個變數都是有小數點的(已手動算完XD)
其實這邊有用Int硬試試看
會跳出 error 表示解不開
用Float試試看，結果跳出沒有這種宣告的 error 訊息
查了一些簡單範例
發現有一種宣告方式是Real
應該是 “實數” 的意思，可以試試看
補充一下數學中所謂的 “實數”
實數，是有理數和無理數的總稱，前者如0、-4、81/7；後者如√2、π等。
以上取自維基百科第一行
z3-demo.py
#!/usr/bin/env python
from z3 import *
a = Real('a')
b = Real('b')
c = Real('c')
d = Real('d')
s = Solver()
s.add(a + b == 12)
s.add(c - d == 9)
s.add(a + c == 22)
s.add(b + d == 12)
print(s.check())
print(s.model())
$ python z3-demo.py
sat
[b = 11/2, a = 13/2, c = 31/2, d = 13/2]
收工