Je souhaite configurer un système entièrement dédié à Z3. Disons qu'il a 4 cœurs et je voudrais utiliser toute la puissance de la machine.Utiliser Z3 dans un serveur multicœur
Je vais résoudre de grandes formules qui ont environ 1000 affirmations incrémentales.
Je voudrais résoudre les formules de manière parallèle. J'ai lu this question et je vois qu'un Context unique devrait être créé pour chaque instance résolvant une formule.
Ma question est alors, quelle est la manière la plus optimale d'utiliser les ressources du système complet (4 cœurs) et de résoudre des formules avec des affirmations incrémentales? Dois-je créer un contexte par cœur et synchroniser d'une manière ou d'une autre la poussée et les pops le long d'eux pour résoudre progressivement les formules?
Merci
Je ne pense pas qu'il existe un moyen "optimal", cela dépend vraiment des problèmes que vous essayez de résoudre. Si vous utilisez l'API, vous devez utiliser des contextes distincts pour chaque thread/processus. Je ne pense pas qu'il y ait une bonne raison d'avoir plus d'un contexte par fil/processus. –
Donc, vous créez un Context par core? Est-ce que chaque contexte utilisera un noyau différent? Puisqu'il y aura 1000 affirmations qui seront résolues par incrémentation ayant 4 Contextes signifie avoir dupliqué l'information 4 fois (1 par noyau). J'ai raison? Y a-t-il une meilleure façon de le faire que de simplement avoir chaque assertion dans chaque contexte? Merci @ChristophWintersteiger – user1618465