Z3 オブジェクトのピクル (またはシリアル化) のサポートは、将来のリリースで検討されていますか? 現在、Z3 Python API によって生成されたモデルをファイルにピクルしようとしていますが、エラー メッセージが表示されますctypes objects containing pointers cannot be pickled。これは、Python API が Z3 DLL の単なるラッパーであることを意味します。
または、Z3 Python API によって生成されたオブジェクトを将来の使用のためにファイルに保存するより良い方法はありますか?
ありがとう！
はい、Z3 Python API は Z3 共有ライブラリ (つまり、Windows 上の DLL) のラッパーです。メソッドを追加し、式やモデルなどをラップする Z3 Python オブジェクトに追加することは可能__getstate__()です__setstate(state)__。これらのメソッドが利用可能な場合、Python pickler はそれらを使用します。したがって、原則として、この機能を追加できます。つまり、Z3 式/式およびモジュールをバイト ストリームにエンコード/デコードするための Z3 API (C API) プロシージャを追加できます。これらの API は、__getstate__()およびを実装するために使用され__setstate(state)__ます。詳細は次のとおりです。
共有: Z3 式の Python リストがあり、これらの式が多くの部分式を共有しているとします。Python pickler は__getstate__()リストの各要素に対して呼び出し、Z3 は共有部分式を複数回エンコードします。問題は、Python の場合、各 Z3 式は「ブロブ」であり、Z3 エンコーダー/シリアライザーは、これらの異なる式がより大きな Python データ構造の一部であることを認識していないことです。そのため、多くの異なる Z3 オブジェクトへの参照を含む Python オブジェクトをピクルするときは注意が必要です。場合によっては、この問題を簡単に修正できることに注意してください。たとえば、ASTVectorZ3 式の Python リストの代わりに Z3 を使用できます。次に、Z3 はASTVector、各共有サブ式が 1 回だけエンコードされる 1 つの大きな「ブロブ」としてエンコードできます。
式やモデルなどの Z3 オブジェクトは、コンテキストに関連付けられています。Python API のほとんどのプロシージャには、追加のctxパラメータがあることに注意してください。たとえば、デフォルトのコンテキストで指定されInt('x')た整数変数を作成し、それを context で作成します。複数のコンテキストは、異なる実行スレッドから同時にアクセスできるため便利です。Z3 オブジェクトを unpickle するとき、それを保存するコンテキストを決定する必要があります。可能性としては、使用するコンテキストを指定するグローバル パラメータを設定することです。設定されていない場合は、デフォルトのコンテキストが使用されます。これは完璧な解決策ではありませんxInt('x', ctx)ctx. さまざまなコンテキストからの Z3 式への参照を含む Python データ構造があり、それをピクルするとします。次に、データを unpickle すると、すべての式が同じ Z3 コンテキストに追加されます。ほとんどのユーザーは 1 つの Z3 コンテキストしか使用せず、複数のコンテキストを使用するユーザーは通常、同じ Python オブジェクト内の異なるコンテキストからの式への参照を格納しないため、おそらくこれは大きな問題ではありません。
代替ソリューションを提案してください。Z3 チームの誰も Python の専門家ではありません。