複数のモデムの時間を短縮

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秒かかりました。私は本当に非常に高速なマシンを持っていません。だから、私はあなたがランタイムの時間を見るためにこれを実行しているマシンのどのような種類が好奇心ですか？