Тот же ввод, Z3 работает в Windows, но дает ошибки сегментации в Linux.

Я использую Z3 в качестве внутреннего решателя для проверки ограниченной программы. Я подаю одни и те же формулы на Z3 в разных операционных системах, Windows 7 X64 и SuSe 10.3 X64, оба Z3 версии 3.2.

Их ввод: run.z3, он содержит вложенные квантификаторы.

Без каких-либо явных включенных опций (режим по умолчанию) Z3 очень хорошо работает в Windows, однако в Linux он дает мне «ошибку сегментации»:

../solvers/z3/bin/z3: строка 11: 27951 Ошибка сегментации

Затем я добавляю единственный вариант

(параметр установки: PULL_NESTED_QUANTIFIERS true)

к формулам, и перезапустите его, на этот раз он работает в Linux, а в Windows все еще работает и решает быстрее. Этот вариант решает мою проблему в Linux.

Предоставляет ли Z3 версии 3.2 для Windows и Linux разные функции? Это правда, какие еще отличия? Заранее спасибо!


windows linux segmentation-fault z3
person Tianhai Liu    schedule 25.01.2012    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Версии для Linux и Windows не идентичны, но предоставляют практически одинаковые функции. Основное отличие заключается в используемом пакете чисел произвольной точности (примечание: в следующей версии мы будем использовать свой собственный пакет, и этой разницы больше не будет). Нам также пришлось внести несколько корректировок, чтобы справиться с различиями между этими двумя платформами. Сбой произошел из-за повреждения памяти. Эта ошибка была исправлена, и в следующем выпуске будет исправление.

Различия в производительности возможны по следующим причинам: версии для Linux и Windows были скомпилированы с использованием разных единиц измерения с плавающей запятой. Вычисления с плавающей запятой используются в некоторых эвристиках, реализованных в Z3. Таким образом, эти колебания в вычислениях с плавающей запятой могут привести к другому пространству поиска. Некоторые стандартные функции C++, которые мы используем (например, std::sort), имеют различную реализацию в gcc и Visual Studio. Мы также наблюдали другие колебания производительности из-за различий в реализации стандартной библиотеки C++ в Visual Studio и GCC.

person Leonardo de Moura    schedule 29.01.2012