2019-04-02

自动化解题神器————z3

Z3

解方程组

from z3 import *
#定义变量
x = Real('x')
y = Real('y')

s = Solver()
#添加约束条件
s.add(x+y==6)
s.add(2*x==(3*y)+6)

#s.check() #若结果为sat则为有解
#解题
m = s.model()

print m

模板

from z3 import *
#char input[32] 输入32个char
input = [BitVec('input_%d' % i, 8) for i in range(32)]

s = Solver()
    
s.add(state == 0xde11c105) #约束

if s.check() != sat:
    print 'unsat'
else:
	m = s.model()
    print m
    print repr("".join([chr(m[input[i]].as_long()) for i in range(32)])) #输出比特向量

例子

from z3 import *
state = 42
def dish(d):
    global state
    state = ((state + d) * 3294782) ^ 3159238819
input = [BitVec('input_%d' % i, 32) for i in range(32)] #int[32]  输入32个int

s = Solver()

for idx in range(32):
	desh(input[idx])
    
s.add(state == 0xde11c105) #约束
#确保输入是可打印字符串
for i in range(32):
    s.add(input[i]>=0, input[i]<=0xff)
    
    
if s.check() != sat:
    print 'unsat'
else:
	m = s.model()
    print m
    print repr("".join([chr(m[input[i]].as_long()) for i in range(32)])) #输出比特向量