So kopieren Sie pyz3 Solver schnell

Question

Ich bin in eine Situation geraten, in der ich wirklich eine Kopierfunktion für den Z3 Solver lieben würde. Damit meine ich, dass ich einen Solver mit einigen Einschränkungen instanziiert habe. Ich möchte es jetzt kopieren, so dass ich zwei unabhängige Löser habe. Im Moment mache ich das, indem ich einen neuen Solver erstelle und einfach über ASertionen iteriere und sie wieder hinzufüge. Für kleine Solver ist das in Ordnung. Bei größeren Solvern kann sich dies erheblich auf die Zeit auswirken, in der eine Kopie erstellt wird, da Z3 die bereits erstellte Arbeit neu erstellt.

Dies ist zwar kein Show-Stopper, aber es wäre sehr vorteilhaft, den Solver direkt kopieren zu können. Die normale decopy-Methode gibt einen Fehler aus, weil es nicht möglich ist, ctypes zu decopyen (was sinnvoll ist), also würde ich annehmen, dass irgendeine bessere Lösung von z3 oder z3py korrekt implementiert werden müsste.

Wer weiß von einem effizienteren Weg, den Solver zu kopieren, wie angegeben, und nicht den Overhead von Z3 auflösen, was er bereits weiß?

Answer 1

Wenn Sie die neueste Z3-Quelle erstellen, haben Solver-Objekte eine translate-Methode, die einen neuen Kontext als Parameter verwendet (es kann derselbe Kontext sein) und eine Kopie des Solver in diesem Kontext erstellt.

s = Solver() 
...add some assertions... 
solver2 = s.translate(main_ctx()) # create a copy in the same context 
solver3 = s.translate(ctx) # create a copy in some other context