Я видел, что Z3 можно построить из источников с помощью --noomp, чтобы он не связывался с OpenMP.Преимущества использования OpenMP в версии Z3 nix
В чем преимущество использования OpenMP. Если я использую флаг --noomp, процесс решения будет медленнее?
Спасибо
Используйте OpenMP, если вы используете Z3 из нескольких потоков в рамках одного процесса. В противном случае Z3 быстрее без OpenMP. Когда вы включаете OpenMP, он использует блокировки для защиты потенциально разделяемой памяти, но если вы никогда не используете разные потоки (все операции в одном контексте должны выполняться в одном потоке или, по меньшей мере, сериализованном), то эти блокировки являются чистыми служебными данными.