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

Question

我正在尝试使用使用Java的Max。以下是我的尝试：

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

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

原因: java.lang.UnsatisfiedLinkError： com.microsoft.z3.Native.INTERNALmkOptimize(J)J地址为 com.microsoft.z3.Native.INTERNALmkOptimize(Native方法) at com.microsoft.z3.Native.mkOptimize(Native.java:5237)地址为 优化.(Optimize.java:265) com.microsoft.z3.Context.mkOptimize(Context.java:3036)

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

Answer 1

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

有关Z3的特定信息，请参见Z3 Java未能检测到libz3.dylib。有关SIP的一般信息，请参见关于Mac上的系统完整性保护。我还没有找到一种很好的方法来告诉OSX Z3是“安全的”，但是没有完全禁用它。