z3 - z3pyでコア数を設定するにはどうすればよいですか

Question

http://research.microsoft.com/en-us/um/people/leonardo/z3_doc/parallel.htmlによると、.smt ファイルを使用している場合、z3 コマンド ラインから CC_NUM_THREADS=4 を設定できます。

z3py API を使用している場合、これを行うにはどうすればよいですか?

Answer 1

補題共有をサポートするポートフォリオ ソルバーは、Z3 の最新バージョンには含まれていません。したがって、これらのパラメーターはサポートされておらず、各パラメーターに複数の値を許可するパラメーター形式も (コマンドラインまたは Python 経由で) サポートされていません。

とはいえ、複数のコアを利用する方法はまだあります。これはパーオア戦術です。たとえば、Z3 Strategy Tutorial (par-or を検索) を参照してください。この例は、SMT2 入力言語を介して複数の戦術を並行して実行する方法を示しています (この例では、異なるランダム シードを使用)。z3py では、ParOr 関数を使用して、このような並列戦術を作成します。