Ich möchte ein System einrichten, das vollständig für Z3 gewidmet ist. Nehmen wir an es hat 4 Kerne und ich möchte die ganze Kraft der Maschine nutzen.Verwenden Sie Z3 in Multicore-Server
Ich werde große Formeln lösen, die ungefähr 1000 inkrementelle Behauptungen haben.
Ich möchte die Formeln in einer parallelen Weise lösen. Ich habe this question gelesen und ich sehe, dass eine eindeutige Context für jede Instanz erstellt werden sollte, die eine Formel löst.
Meine Frage ist dann, was ist der optimale Weg, um die vollen Systemressourcen (4 Kerne) zu nutzen und Formeln mit inkrementellen Behauptungen zu lösen? Sollte ich einen Kontext pro Kern erstellen und irgendwie den Push synchronisieren und mit ihnen zusammenkommen, um die Formeln inkrementell zu lösen?
Dank
Ich glaube nicht, dass es einen "optimalen" Weg gibt, es hängt wirklich von den Problemen ab, die Sie versuchen zu lösen. Wenn Sie die API verwenden, müssen Sie für jeden Thread/Prozess separate Kontexte verwenden. Ich glaube nicht, dass es einen guten Grund dafür gibt, mehr als einen Kontext pro Thread/Prozess zu haben. –
Also würden Sie einen Kontext pro Kern erstellen? Wird jeder Kontext einen anderen Kern verwenden? Da es 1000 Behauptungen geben wird, die inkrementell gelöst werden, wenn 4 Kontexte bedeutet, haben Sie Informationen viermal dupliziert (1 pro Kern). Ich richtig? Gibt es einen besseren Weg, es zu tun als nur jede Behauptung in jedem Kontext zu haben? Danke @ChristophWintersteiger – user1618465