Yices - SMT-solver от Computer Science Laboratory SRI International ( http://yices.csl.sri.com/ ). Иными словами, этот инструмент предназначен для решения задачи SAT, но с оптимизациями в некоторых теориях (например, битовые вектора, целые числа). Инструмент не является (пока) open-source. К дистрибутиву поставляется библиотека (dll и so) для вызова Yices из программ на Си. Мне же нужно было вызвать ее из Java, для чего пришлось воспользоваться механизмом JNI. Но для этого нужен архив объектных модулей (".a"), который отсутствовал в дистрибутиве. Коллеги из PACE University сделали уже готовую JNI-оболочку для вызова Yices из Java ( http://atlantis.seidenberg.pace.edu/wiki/lep/Yices%20Java%20API%20Lite ), однако на их сайте были представлены только jar под Linux, а, поскольку, потенциальные пользователи моей программы работают под Windows, то надо было ее пересобрать для Windows. К счастью, PACE University предоставляет исходники JNI-оболочки бесплатно, чем я и воспользовался.
Итак, качаем http://atlantis.seidenberg.pace.edu/~lep/yices/codes/source.tar.gz , распаковываем.
я собирал под MinGW 5.1.4 (под cygwin не получилось).
Если у вас не установлен JDK, сделайте это - его header'ы потребуются при компиляции оболочки. я для простоты поместил в директорию include из sources.tar.gz содержимое директории include (c win32) из JDK (в моем случае 1.6.0_13).
подготавливаем libyices.a - коллеги его уже подготовили для нас и поместили в директорию lib архива sources.tar.gz. (иначе пришлось бы возиться с reimp и dlltool)
компилируем оболочку (прилагаемый Makefile, как выяснилось, не подходит для компиляции под Windows):
gcc -o libYicesLite.dll -shared YicesLite.c -Iinclude -Iinclude/win32 -Llib -lyices -Wl,--add-stdcall-alias
(последний параметр очень важен - без него не получится вызвать функции оболочки из Java!)
эта команда может выдать набор предупреждений, но никаких ошибок не должно быть (иначе не появится dll)
теперь компилируем java-исходники:
javac yices\YicesLite.java
обратите внимание, что YicesLite.java именован именно так и в этом пакете. Менять имя пакета и имя класса НЕЛЬЗЯ - под эти имена сгенерирована оболочка на Си, под эти имена мы только же компилировали dll.
Теперь можно написать тестовый пример и запустить его :) Только не забудьте сделать очень важную вещь: поместить скомпилированный libYicesLite.dll в директорию из переменной среды java.library.path и libyices.dll (ее можно скачать с сайта Yices) в директорию из переменной среды PATH (чтобы она могла подгрузиться, как зависимость). И еще проверьте, как вызывается метод System.loadLibrary! Для данных имен правильным будет вызов
System.loadLibrary("libYicesLite")
(с префиксом lib!!!)
Теперь, кажется, всё :)
скачать libYicesLite.dll и соответствующий jar под Windows можно тут: http://tesla-project.googlecode.com/files/libYicesLite.dll
http://tesla-project.googlecode.com/files/YicesLite.jar
Комментариев нет:
Отправить комментарий