Z3コンテキストのシリアライズ/デシリアライズ？

Question

Z3コンテキスト（C＃から）をシリアライズ/デシリアライズすることはできますか？ そうでない場合、この機能は計画されていますか？

この機能は実際のアプリケーションでは重要だと思います。

Answer 1

これは現在のAPIでは直接サポートされていません。次のリリースでは複数のソルバーをサポートし、あるソルバーから別のソルバーにアサーションをコピーしてアサーションを取得するコマンドを提供します。これらのコマンドを使用すると、式をファイル（SMT 2.0形式）にダンプすることによってシリアル化を実装できます。デシリアライズするには、ファイルを読み戻すだけです。 論理的なコンテキストにアサーションしたアサーションを追跡している場合は、この解決策はすでに現在のAPIを使用して実装できます。

私は、Z3を使用する多くのプロジェクトで以下のアプローチが使用されていることを知りました。彼らは式のための独自の表現を持っています。彼らはZ3を呼び出すと、その表現をZ3の表現に変換します。ほとんどの場合、パフォーマンスのオーバーヘッドは最小限に抑えられます。このアプローチにより、多くの柔軟性が得られます。シリアライゼーションは良い例です。いくつかのプログラミング環境（例えば、Python）は、シリアライズのための組み込みサポートを既に提供している。