Как настроить Java среду разработки для Z3 - PullRequest
Новая
       44

Как настроить Java среду разработки для Z3

2 голосов
/ 26 февраля 2020

Как настроить Java среду разработки для SMT-решателя Z3?

Примечание: Письмо и ответ автора, см. Могу ли я ответить на мой свой вопрос? .

1 Ответ

2 голосов
/ 26 февраля 2020

  • Z3 - это приложение на C ++ с привязками Java. Начните с загрузки собственного дистрибутива, в нашем случае Ubuntu (аналогичный подход должен работать для macOS), с https://github.com/Z3Prover/z3/releases, например: z3-4.8.7-x64-ubuntu-16.04.zip.

  • Разархивируйте сборку в Z3_DIR. Чтобы упростить задачу, выполните следующие операции экспорта: 

 export Z3_DIR=<some_path>/z3-4.8.7-x64-ubuntu-16.04
 export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:$Z3_DIR/bin
  • Загрузите пример Java, соответствующий вашей версии Z3, скомпилируйте и запустите его: 
$ curl https://raw.githubusercontent.com/Z3Prover/z3/z3-4.8.7/examples/java/JavaExample.java > JavaExample.java
$ javac -cp $Z3_DIR/bin/com.microsoft.z3.jar JavaExample.java
$ java -cp $Z3_DIR/bin/com.microsoft.z3.jar:. JavaExample

Если все хорошо, вы должны увидеть пример выполнения без ошибок.

  • Чтобы использовать банку Z3 с Maven, установите ее в локальный репозиторий maven: 
$ mvn install:install-file \
   -Dfile=$Z3_DIR/bin/com.microsoft.z3.jar \
   -DgroupId=com.microsoft \
   -DartifactId=z3 \
   -Dversion=4.8.7 \
   -Dpackaging=jar \
   -DgeneratePom=true

В <mavenrepo>/repository/com/microsoft/z3/4.8.7/ будет создан сосуд с именем z3-4.8.7.jar. Его можно добавить в проект maven как зависимость: 

     <dependency>
         <groupId>com.microsoft</groupId>
         <artifactId>z3</artifactId>
         <version>4.8.7</version>
     </dependency>
  • Приятно иметь под рукой исходники Z3 API Java, они доступны на Github: https://github.com/Z3Prover/z3/tree/z3-4.8.7/src/api/java. Обратите внимание, что структура папок не соответствует имени пакета, поэтому вы можете скопировать файлы в com/microsoft/z3 перед их регистрацией в IDE.

EDIT - macOS К сожалению установка пути к библиотеке (DYLD_LIBRARY_PATH) в macOS не работает, некоторые подробности и решение см. здесь: https://github.com/Z3Prover/z3/issues/294

...