다중 모델 시간을 단축하십시오.

Question

여러 모델을 얻지 만 몇 시간이 걸립니다. 그래서 모든 모델을 가져 오는 시간을 줄이는 것이 좋습니다. 적은 시간에 Satisfy 방정식에 대한 모든 가능한 솔루션을 얻으시겠습니까? 가능한 모든 솔루션을 얻기위한 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 초가 걸렸습니다. 그리고 나는 정말로 매우 빠른 기계도 가지고 있지 않습니다. 그래서, 런타임의 시간을보기 위해 어떤 종류의 기계를 실행하고 있는지 궁금합니다.