z3约束器学习笔记

1	pip install z3-solver

或者也可以去github

1	https://github.com/Z3Prover/z3

一，申请 Int对象语法 “ Int(name) ” name即对象名字

1	x = Int('x')

　　似乎只能进行加减乘除的约束

二，申请位向量语法“ Bitvex(name,size) ” name为对象名字，size为大小 2^size （这里似乎可以看作是一个约束）

1	x = BitVec('x',16)

　　位向量还可以一次性申请多个，类似这样

1	x,y,z = BitVecs('x y z',16)

　　等价于

1
2
3

x = BitVec('x',16)
y = BitVec('y',16)
z = BitVec('z',16)

BitVec在python3上说为定义。。。疑惑

BitVec最好用在位运算复杂又多多时候，能用Int就用Int 运行更快

1	sol = Solver()

1	sol.add(约束式子)

1	sol.check() # 如果返回 sat 则存在解

1	print sol.model()

　　sol.model() 其实是一个list，可以用我们变量名称作为下标取出里面的值，比如

x = Int('x')
y = Int('y')
s = Solver()
s.add(x+y == 4)
s.add(x > 0)
s.add(y > 0)
if s.check() == sat:
    m = s.model()
    print m[x]

　　很清晰的思路，直接吧每一次计算出来的解add进入条件，使其不成立

while s.check() == sat:
    m = s.model()
    print m
    s.add(Or(x!=m[x],y!=m[y],z!=m[z]))

　　注意这里的Or()，可以理解为不能让里面的式子同时不成立。少了它就相当于

1	x!=m[x] and y!=m[y] and z!=m[z]

　　明显就会漏解

Papaya