3

Z3の並列バージョンを再アクティブ化するための現在の計画は何ですか？

4

1 に答える 1

7

Z3は、並列処理を広範囲にサポートしていませんでした。バージョン2.xには、ユーザーがさまざまな構成オプションを使用して複数のコピーを並行して実行できるようにする実験的な機能が含まれていました。異なるコピーは、情報を共有し、お互いの検索スペースを整理することもできます。この機能にはいくつかの制限がありました。たとえば、プログラムAPIでは使用できませんでした。また、長期的な研究の目標や方向性とも矛盾していました。したがって、この機能は最近のバージョンから削除されました。

そうは言っても、Z3 4.x APIでは、複数のコンテキスト（Z3_Context）を作成し、それらに異なるスレッドから同時にアクセスするのが安全です。以前のバージョンはスレッドセーフではありませんでした。Z3 4.xでは、並列コンビネータを使用してカスタム戦略を定義できます。たとえば、コンビネータ(par-or t1 t2)は戦略t1をt2並行して実行します。これらのコンビネータは、プログラマティックAPIおよびSMT2.0フロントエンドで使用できます。次のオンラインチュートリアルには、追加情報が含まれています：http: //rise4fun.com/Z3/tutorial/strategies

smt次のコマンド（SMT 2.0フロントエンドの場合）は、異なるランダムシードを持つ戦術の2つのコピーを使用して、アサートされた式をチェックします。

(check-sat-using (par-or (! smt :random-seed 10) (! smt :random-seed 20)))
于 2012-09-17T14:24:23.463 に答える