Компиляция и сборка с MinGW

по-моему, неплохая статья http://www.crossplatform.ru/node/58

И вновь про двойную диспетчеризацию на Java

Пусть надо реализовать функцию от двух переменных f(X, Y), где типы X и Y - суть корни деревьев наследования, причем так, чтобы при появлении нового типа X или Y компилятор нам сам подсказывал, что надо дописать. Обычная стандартная задача двойной диспетчеризации :) Не претендуя на всеобщий ее охват, напишу примененный мною метод реализации такого механизма. Добавлю только, что типы X и Y абстрактные.

Итак, в типе

Определяю новый тип (interface) YVisitor:
public interface YVisitor
{
void visitY1( Y1 y );
void visitY2( Y1 y );
}
помещаю туда методы про те потомки типа Y, которые вспоминаются.

В тип Y помещаю абстрактный метод:
public abstract void visit( X x );

Тип X делаю implements YVisitor и добавляю метод

public void f( Y y )
{
y.visit( this );
}

В каждом потомке типа Y нужно теперь реализовать метод visit. Делаем это по такой схеме, для примера на классе Y1:
class Y1 extends Y
{
...
public void visit(X x)
{
x.visitY1(this);
}
}
Очень важный момент, что суффикс имени вызываемого метода должен содержать имя класса (потомка Y)! Если такого метода нет в классе X (а это означает, что еще нет соотв.visit-метода в интерфейсе), то идем в интерфейс YVisitor и добавляем метод void visitY1(Y1 y1); Таким образом, при добавлении нового потомка типа Y такая схема работы позволит отследить весь необходимый новый код.

Кроме того, компилятор будет требовать реализации методов visitYi в каждом потомке типа X. Если появится новый потомок типа X, компилятор сообщит, что в нем нужно реализовать все visitYi.

Вызвать это дело следует так: x.f(y), где x типа X, y типа Y.

Как использовать Yices из Java под Windows

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