pyz3ソルバーを素早くコピーする

Question

私はZ3ソルバーのコピー機能が大好きな状況に遭遇しています。これは私がソルバをいくつかの制約でインスタンス化したことを意味します。私は今それをコピーして、の2つのソルバーを持っています。現時点では、私は新しいソルバーを作成し、s.assertionsを繰り返して追加することでこれをやっています。小さなソルバーに対してはこれは問題ありません。より大きなソルバの場合、これはZ3がすでに行った作業を再作成するときのコピー作成に重大な影響を与えます。

これはショーストッパーではありませんが、ソルバーを直接コピーできることは非常に有益です。通常のdeepcopyメソッドは、ctypes（それは理にかなっています）をdeepcopyできないというエラーを投げるので、z3やz3pyによって適切なソリューションを実装する必要があります。

ソルバーをコピーしてZ3のオーバーヘッドが発生していないことを知っている人は誰でも知っているでしょうか？

Answer 1

最新のZ3ソースをビルドする場合、Solverオブジェクトには新しいコンテキストをパラメータとして使用するtranslateメソッドがあり（同じコンテキストでも可）、そのコンテキストでソルバのコピーが作成されます。

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