Работает ли параллельная версия Z3 для логики BV?

Question

Я не смог использовать оба ядра процессора с параллельным Z3 3.2 (из каталога bin_mt или x64_mt) с PAR_NUM_THREADS=2 в Windows7.Те же 50% и отсутствие разницы во времени с однопоточной версией.

Поддерживается ли параллельная версия для этих логик или она работает только с QF_IDL?

Answer 1

По ошибке параллельное выполнение не было включено в Z3 3.2. Вот почему Z3 все еще работает последовательно, когда вы устанавливаете PAR_NUM_THREADS=2. Команда Z3 исправила ошибку, поэтому параллельная функция будет доступна в следующем выпуске.

EDIT:

Как упоминалось в комментарии @Leo, параллельная функция теперь запланирована для Z3 4.1.