Z3のパラレルバージョンはBVロジックに対応していますか？

Question

Windows7上で並列Z3 3.2（bin_mtまたはx64_mtディレクトリ）のプロセッサコアとPAR_NUM_THREADS=2の両方を使用できませんでした。シングルスレッド版と同じ50％で、時間差はありません。

これらのロジックではパラレルバージョンがサポートされていますか、それともQF_IDLのみで動作しますか？

Answer 1

誤って、パラレル実行はZ3 3.2に含まれていません。だから、あなたがPAR_NUM_THREADS=2に設定したとき、Z3は依然として連続して動いています。 Z3チームが間違いを修正したので、次のリリースで並列機能が利用可能になります。

EDIT：@Leoコメントで述べたように

、パラレル機能は今Z3 4.1のために計画されています。