z3-solver安裝和使用方法

Z3是一個微軟研究院開源的theorem prover(定理證明器)，支持位向量、布爾、數組、浮點數、字符串以及其他數據類型。Z3是一個SMT solver以及支持 SMTLIB的格式。

 

這里簡單介紹幾個概念：

SAT(Boolean Satisfiability Problem/布爾可滿足性問題)

SMT(Satisfiability Modulo Theories/可滿足性模理論)

SAT + Theory Solvers = SMT

 

github項目： https://github.com/Z3Prover/z3

官方文檔： http://z3prover.github.io/api/html/

angr框架的內置Z3:  https://github.com/angr/angr-z3

-------

 

0x01 安裝z3-solver

pip install z3-solver

以下是錯誤安裝方式：

# 別安裝成這個
# Backup ZFS snapshots to S3
pip install z3

 

0x02 使用z3-solver來解方程

例如最簡單的三元一次方程組：

from z3 import *
x,y,z=Ints('x y z')
s=Solver()
s.add(2*x+3*y+z==6)
s.add(x-y+2*z==-1)
s.add(x+2*y-z==5)
print s.check()
print s.model()

模運算：

from z3 import *
x=Int('x')
s=Solver()
a = 65537
b = 64834
c = 41958
s.add(x>0)
s.add(x % a == b)
s.add(x % b == c)
print s.check()
print s.model()

 

0x03 其他用法

等pcat以后再補充