Reduzieren Sie die Zeit für mehrere modles

Question

Es Mehrere Modelle bekommen, aber es dauert Stunden time.So schlagen mir bitte die Zeit zu reduzieren, um alle alle möglichen Lösung in kürzerer Zeit models.how für Satisfy Gleichung zu bekommen? Gibt es eine Funktion in z3python, um alle möglichen Lösungen in Zahlen zu erhalten?

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

Ich lief Ihr Programm unverändert und es dauerte nur 0,5 Sekunden zu vervollständigen. Und ich habe auch keine wirklich schnelle Maschine. Also, ich bin neugierig, was für eine Maschine Sie laufen, um Stunden der Laufzeit zu sehen?