νz (z3opt)：无法使用 Java API 创建优化对象

Question

我正在尝试通过 Java API 使用 Max-SMT。以下是我的尝试：

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

但是，第一行存在运行时错误，其中创建了 opt。

Caused by: java.lang.UnsatisfiedLinkError:
com.microsoft.z3.Native.INTERNALmkOptimize(J)J at
com.microsoft.z3.Native.INTERNALmkOptimize(Native Method) at
com.microsoft.z3.Native.mkOptimize(Native.java:5237) at
com.microsoft.z3.Optimize.(Optimize.java:265) at
com.microsoft.z3.Context.mkOptimize(Context.java:3036)

我使用的是 Github 的最新版 Z3，于 9 月 30 日下载。

Answer 1

在 OSX，确保系统完整性保护不会干扰您的工作。在此设置中，它可能会在启动 JVM 时从您的环境中删除 DYLD_LIBRARY_PATH 环境设置，这会导致无法找到 *.dylib。

有关 Z3 的特定信息，请参阅 Z3 Java API fails to detect libz3.dylib. For general info about SIP see About System Integrity Protection on your Mac。我还没有找到一个好方法来告诉 OSX Z3 是 "safe" 但又不完全禁用 SIP。

νz (z3opt)：无法使用 Java API 创建优化对象

νz (z3opt): Unable to make an Optimize object using Java API

z3