1
我想建立一個完全專用於Z3的系統。假設它有4個內核，我想使用機器的所有功能。在多核服務器中使用Z3
我將解決大約1000個增量斷言的大公式。
我想以平行的方式解決公式。我讀過this question，我發現應該爲解決公式的每個實例創建一個獨特的Context。
我的問題是，使用完整系統資源（4個核心）和解決增量斷言的公式的最佳方式是什麼？我應該爲每個核心創建一個上下文，並以某種方式同步推送和彈出來逐步解決公式？經由一個上下文中創建
由於
我不認爲有一個「最優化」的方式，它取決於你想解決的問題。如果您使用API，則必須爲每個線程/進程使用不同的上下文。我不認爲每個線程/進程擁有多個上下文都有很好的理由。 –
所以你會創建一個上下文每核心？每個環境會使用不同的核心嗎？由於將有1000個斷言將逐步解決，有4個上下文意味着重複信息4次（每個核心1個）。我說得對嗎？有沒有更好的方法來做到這一點，而不僅僅是在每個環境中都有每個斷言？謝謝@ChristophWintersteiger – user1618465