ν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的第一行有一个运行时错误。

原因:java.lang.UnsatisfiedLinkError:
在
com.microsoft.z3.Native.INTERNALmkOptimize (J)com.microsoft.z3.Native。INTERNALmkOptimize(Native Method) at
在
com.microsoft.z3.Native.mkOptimize (Native.java: 5237)com.microsoft.z3.Optimize。(Optimize.java: 265)
com.microsoft.z3.Context.mkOptimize (Context.java: 3036)

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

Answer 1

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

有关Z3特定的信息，请参阅Z3 Java API无法检测libz3.dylib。关于SIP的一般信息，请参阅关于Mac上的系统完整性保护。我还没有找到一个好的方法来告诉OSX Z3是"安全的"，但又不禁用SIP。