Почему в моем инструменте Alloy * / Alloy не отображаются параметры решателя, такие как MiniSat, MiniSat с Unsat Core, Lingeling, Glucose?

Question

В инструменте, который я скачал с: http://alloy.mit.edu/alloy/hola/

единственные варианты решателей, которые появляются - это SAT4J и PLingeling. Почему другие параметры также не отображаются? Я использую Windows и запускаю инструмент, дважды щелкнув файл hola-0.2.jar...

Та же ошибка возникает при использовании инструмента Alloy, загруженного с сайта: http://alloy.mit.edu/alloy/download.html

Однако, когда я запускаю его в Windows 7, появляются такие варианты решения, как miniSAT, miniSAT с Unsat Core, ZChaff! Доступные варианты решателя зависят от операционной системы?

Answer 1

Решатели типа minisat не основаны на Java. Следовательно, Alloy Analyzer поставляется с собственной версией этих решателей для каждой обычно используемой операционной системы. Если вы откроете.jar с помощью архиватора, вы сможете увидеть четыре папки: x86-windows, x86-mac, x86-linux и x86-freebsd, каждая из которых содержит специфичные для ОС исполняемые файлы, связанные с этими решателями.

В своем вопросе вы говорите, что у вас проблемы с использованием этих решателей в Windows, но, тем не менее, говорите, что в Windows 7 все работает нормально. Можно ли предположить, что под Windows вы подразумеваете последнюю версию ОС Windows, то есть Windows 10?

Я не знаком с этим, но это может быть тот случай, когда те.dll, которые присутствуют в папке x86_windows, просто не работают должным образом в Windows 10.

Answer 2

Какую версию Java (32 или 64 бита) вы используете?

Страница загрузки сплава содержит файл jar с собственными библиотеками / решателями для x86_windows, то есть библиотеками, которые работают в 32-битной Java, но не в 64-битной Java. Учитывая, что Alloy использует JNI и эти библиотеки для запуска решателей, вы должны использовать правильную версию Java для использования решателей.

Файл jar Alloy содержит 32-битные собственные библиотеки для Windows, Mac и FreeBSD, а также 32- и 64-битные библиотеки для Linux.