z3 - Z3 Context serialization/deserialization?

Question

Is it possible to serialize/deserialize a Z3 context (from C#)? If not, is this feature planned ?

I think this feature is important for real world applications.

Answer 1

これは、現在の API では直接サポートされていません。次のリリースでは複数のソルバーがサポートされ、あるソルバーから別のソルバーにアサーションをコピーし、アサーションを取得するためのコマンドが提供されます。これらのコマンドを使用すると、式をファイル (SMT 2.0 形式) にダンプすることでシリアル化を実装できます。逆シリアル化するには、ファイルを読み戻すだけです。論理コンテキストにアサートしたアサーションを追跡している場合、このソリューションは現在の API を使用して既に実装できることに注意してください。

そうは言っても、Z3 を使用する多くのプロジェクトで次のアプローチが使用されているのを見てきました。式の独自の表現があります。Z3 を呼び出すと、その表現が Z3 の表現に変換されます。ほとんどの場合、パフォーマンスのオーバーヘッドは最小限です。このアプローチにより、多くの柔軟性が得られます。シリアル化はその良い例です。一部のプログラミング環境 (Python など) では、シリアライゼーションの組み込みサポートが既に提供されています。