νz（z3opt）：Java APIを使用してOptimizeオブジェクトを作成できません

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)

私は9月30日にダウンロードしたGithubのZ3の最新バージョンを使用しています。

Answer 1

OSXでは、システムインテグリティ保護が作業に干渉しないことを確認してください。この設定では、*.dylibが見つからないという、JVMを起動するときに環境からDYLD_LIBRARY_PATH環境設定を削除することがあります。

Z3固有の情報については、Z3 Java API fails to detect libz3.dylibを参照してください。 SIPに関する一般的な情報は、About System Integrity Protection on your Macを参照してください。 OSXに、Z3がSIPを完全に無効にすることなく「安全」であることを伝える良い方法は見つけられませんでした。