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以后再补充