减少多modles

Question

时它得到多个模型，但它需要time.So小时请给我建议，以减少时间让所有models.how得到了满足公式所有可能的解决方案在更短的时间？ z3python中是否有任何函数用于获取所有可能的解决方案。

from z3 import * 
x0,x1,x2,x3,x4,x5=BitVecs('x0 x1 x2 x3 x4 x5',32) 
y0,y1,y2,y3,y4,y5=BitVecs('y0 y1 y2 y3 y4 y5',32) 
k0,k1,k2,k3,k4=BitVecs('k0 k1 k2 k3 k4',32) 
c0,c1,c2=BitVecs('c0 c1 c2',32) 
s = Solver() 
s.add(x0==0x656b696c) 
s.add(y0==0x20646e75) 
s.add(x5==0xcf9919c3) 
s.add(y5==0xf776ba96) 
s.add(x1==simplify((RotateLeft(x0,1)&RotateLeft(x0,8))^(RotateLeft(x0,2))^y0^k0)) 
s.add(y1==x0) 

s.add(x2==simplify((RotateLeft(x1,1)&RotateLeft(x1,8))^(RotateLeft(x1,2))^y1^k1)) 
s.add(y2==x1) 

s.add(x3==simplify((RotateLeft(x2,1)&RotateLeft(x2,8))^(RotateLeft(x2,2))^y2^k2)) 
s.add(y3==x2) 

s.add(x4==simplify((RotateLeft(x3,1)&RotateLeft(x3,8))^(RotateLeft(x3,2))^y3^k3)) 
s.add(y4==x3) 

s.add(x5==simplify((RotateLeft(x4,1)&RotateLeft(x4,8))^(RotateLeft(x4,2))^y4^k4)) 
s.add(y5==x4) 

s.add(c1==0) 
s.add(c2==1) 
s.add(k3==(RotateRight(RotateRight(k2,3),1)^(RotateRight(k2,3)^k0))^c0^c1) 
s.add(k4==(RotateRight(RotateRight(k3,3),1)^(RotateRight(k3,3)^k1))^c0^c1) 

count = 1 
while s.check() == sat: 
    if (count > 10): 
     break 
    print 'The count is:', count 
    count=count + 1 
    print 'x1=',hex(s.model()[x1].as_long()),'y1=',hex(s.model()[y1].as_long()),'k0=',hex(s.model()[k0].as_long()),"\n " 
    print 'x2=',hex(s.model()[x2].as_long()),'y2=',hex(s.model()[y2].as_long()),'k1=',hex(s.model()[k1].as_long()),"\n " 
    print 'x3=',hex(s.model()[x3].as_long()),'y3=',hex(s.model()[y3].as_long()),'k2=',hex(s.model()[k2].as_long()),"\n " 
    print 'x4=',hex(s.model()[x4].as_long()),'y4=',hex(s.model()[y4].as_long()),'k3=',hex(s.model()[k3].as_long()),"\n " 
    print 'x5=',hex(s.model()[x5].as_long()),'y5=',hex(s.model()[y5].as_long()),'k4=',hex(s.model()[k4].as_long()),"\n " 
    m = s.model() 
    block = [] 
    for d in m: 
     c = d() 
     block.append(c != m[d]) 
    s.add(Or(block)) 

Answer 1

我没有修改你的程序，只花了0.5秒就完成了。而且我也没有一台非常快的机器。所以，我很好奇你用什么样的机器来运行这个小时的运行时间？