2012-03-07 7 views
1

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

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

+0

関連性があります。http://stackoverflow.com/questions/7726607/is-it-possible-to-clone-z3-context – AKX

答えて

1

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

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