Блог

Главная - Вопросы по программированию - vz (z3opt): невозможно создать объект оптимизации с помощью Java API

vz (z3opt): невозможно создать объект оптимизации с помощью Java API

#z3

#z3

Вопрос:

Я пытаюсь использовать Max-SMT с использованием Java API. Ниже приведена моя попытка:

 Optimize opt = ctx.mkOptimize();
opt.Add(hardConstraints);
for(BoolExpr c : C){
  opt.AssertSoft(c, 1, "group");
}

Однако в первой строке, где создается ошибка времени выполнения opt .

Вызвано: java.lang.Ошибка неудовлетворительной ссылки:
com.microsoft.z3.Native.INTERNALmkOptimize(J)J в
com.microsoft.z3.Native.Внутренняя оптимизация (собственный метод) в
com.microsoft.z3.Native.mkOptimize(Native.java: 5237) в
com.microsoft.z3.Optimize.(Optimize.java: 265) в
com.microsoft.z3.Context.mkOptimize(Context.java:3036)

Я использую последнюю версию Z3 с Github, загруженную 30 сентября.

Комментарии:

1. Вы скомпилировали Z3 из исходных текстов или использовали загрузку двоичного файла?

2. @ChristophWintersteiger Я скомпилировал Z3 из исходных текстов. Я использую Mac OS X

Ответ №1:

В OSX убедитесь, что защита целостности системы не мешает вашей работе. В этом параметре он может удалить параметр DYLD_LIBRARY_PATH среды из вашей среды при запуске JVM, что приводит *.dylib к невозможности найти эффект.

Для получения информации о Z3 см. Z3 Java API не удается обнаружить libz3.dylib . Общие сведения о SIP см. в разделе О защите целостности системы на вашем Mac. Я еще не нашел хорошего способа сообщить OSX, что Z3 «безопасен», не отключая SIP полностью.