1
Z3専用のシステムをセットアップしたいと思う。 4つのコアがあり、マシンのすべてのパワーを使いたいとしましょう。マルチコアサーバーでZ3を使用する
約1000個のインクリメンタルアサートを持つ大きな数式を解くことになります。
私は数式を並列に解きたいと思っています。私はthis questionを読んでおり、数式を解くすべてのインスタンスに対してユニークなContextを作成する必要があることがわかります。
私の質問は、完全なシステムリソース（4コア）を使用し、インクリメンタルアサートで数式を解決する最適な方法は何ですか？コアごとにコンテキストを作成し、何らかの形でプッシュとポップを同期させて式を段階的に解決する必要がありますか？
ありがとうございました
"最適な"方法はないと思いますが、実際には解決しようとしている問題によって異なります。 APIを使用している場合は、スレッド/プロセスごとに別々のコンテキストを使用する必要があります。私はスレッド/プロセスごとに複数のコンテキストを持つ良い理由はないと思います。 –
コアあたりのコンテキストを作成しますか？各コンテキストは別のコアを使用しますか？ 4つのコンテキストが重複した情報を4回（1つのコアにつき1つ）持つことを意味するために、段階的に解決される1000個のアサートが存在するので、私はそう？すべてのコンテキストですべての主張をするよりも、より良い方法がありますか？ありがとう@ChristophWintersteiger – user1618465