如何从Eclipse插件链接Z3 build，编译为Java？

Question

我有一个完美的适用于Java的Z3构建系统。我想从Eclipse插件中调用它。我尝试了几种方法，但其中没有一种为我工作。这些方法是：

1. 添加Z3建立作为外部类文件夹 How to Use External Class Files in an Eclipse Project

Exception in thread "main" java.lang.UnsatisfiedLinkError: no libz3java in java.library.path at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1867) at java.lang.Runtime.loadLibrary0(Runtime.java:870) at java.lang.System.loadLibrary(System.java:1122) at com.microsoft.z3.Native.(Native.java:14) at com.microsoft.z3.Global.ToggleWarningMessages(Global.java:87) at TestZ3.main(TestZ3.java:9)

复制Z3建立到Eclipse插件，在根目录下。然后在库下添加com.microsoft.z3.jar（右键单击项目 - > Build Path-> Configure Build Path-> Libraries-> Add Jars）。错误是：

java.lang.UnsatisfiedLinkError: no libz3java in java.library.path at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1867) at java.lang.Runtime.loadLibrary0(Runtime.java:870) at java.lang.System.loadLibrary(System.java:1122) at com.microsoft.z3.Native.(Native.java:14) at com.microsoft.z3.Global.ToggleWarningMessages(Global.java:87) at plugintest.handlers.SampleHandler.execute(SampleHandler.java:37) at org.eclipse.ui.internal.handlers.HandlerProxy.execute(HandlerProxy.java:295) at org.eclipse.ui.internal.handlers.E4HandlerProxy.execute(E4HandlerProxy.java:90) at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method) at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62) at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43) at java.lang.reflect.Method.invoke(Method.java:498) at org.eclipse.e4.core.internal.di.MethodRequestor.execute(MethodRequestor.java:56) at org.eclipse.e4.core.internal.di.InjectorImpl.invokeUsingClass(InjectorImpl.java:252) at org.eclipse.e4.core.internal.di.InjectorImpl.invoke(InjectorImpl.java:234) at org.eclipse.e4.core.contexts.ContextInjectionFactory.invoke(ContextInjectionFactory.java:132) at org.eclipse.e4.core.commands.internal.HandlerServiceHandler.execute(HandlerServiceHandler.java:152) at org.eclipse.core.commands.Command.executeWithChecks(Command.java:493) at org.eclipse.core.commands.ParameterizedCommand.executeWithChecks(ParameterizedCommand.java:486) at org.eclipse.e4.core.commands.internal.HandlerServiceImpl.executeHandler(HandlerServiceImpl.java:210) at org.eclipse.e4.ui.workbench.renderers.swt.HandledContributionItem.executeItem(HandledContributionItem.java:799) at org.eclipse.e4.ui.workbench.renderers.swt.HandledContributionItem.handleWidgetSelection(HandledContributionItem.java:675) at org.eclipse.e4.ui.workbench.renderers.swt.HandledContributionItem.access$7(HandledContributionItem.java:659) at org.eclipse.e4.ui.workbench.renderers.swt.HandledContributionItem$4.handleEvent(HandledContributionItem.java:592) at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:84) at org.eclipse.swt.widgets.Display.sendEvent(Display.java:4362) at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1113) at org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:4180) at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3769) at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine$4.run(PartRenderingEngine.java:1127) at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:337) at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine.run(PartRenderingEngine.java:1018) at org.eclipse.e4.ui.internal.workbench.E4Workbench.createAndRunUI(E4Workbench.java:156) at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:694) at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:337) at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:606) at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:150) at org.eclipse.ui.internal.ide.application.IDEApplication.start(IDEApplication.java:139) at org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:196) at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:134) at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:104) at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:380) at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:235) at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method) at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62) at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43) at java.lang.reflect.Method.invoke(Method.java:498) at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:669) at org.eclipse.equinox.launcher.Main.basicRun(Main.java:608) at org.eclipse.equinox.launcher.Main.run(Main.java:1515) at org.eclipse.equinox.launcher.Main.main(Main.java:1488)

有或没​​有前面的步骤，我添加com.microsoft.z3.jar到类路径，位于所述的plugin.xml Runtime选项卡。在这种情况下，插件找不到按钮按下命令后调用的处理程序。

!MESSAGE plugintest.handlers.SampleHandler cannot be found by PluginTest_1.0.0.qualifier !STACK 0 java.lang.ClassNotFoundException: plugintest.handlers.SampleHandler cannot be found by ....more

事实上，这种做法为我以前的一个安装（戴尔，英特尔，X64 Eclipse的火星（64），爪哇1.8 X64）！

1. 在https://github.com/Z3Prover/z3/issues/1093的讨论之后，我将com.microsoft.z3.jar的Native Library Location配置为Z3 Build目录。调用Z3从Eclipse插件生成，所报告的误差是相同方法2，但在Java应用程序调用它，误差更具体：

Exception in thread "main" java.lang.UnsatisfiedLinkError: C:\Users...TestZ33\build\libz3java.dll: Can't find dependent libraries at java.lang.ClassLoader$NativeLibrary.load(Native Method) at java.lang.ClassLoader.loadLibrary0(ClassLoader.java:1941) at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1857) at java.lang.Runtime.loadLibrary0(Runtime.java:870) at java.lang.System.loadLibrary(System.java:1122) at com.microsoft.z3.Native.(Native.java:14) at com.microsoft.z3.Global.ToggleWarningMessages(Global.java:87) at TestZ3.main(TestZ3.java:9)

其他https://www.chilkatsoft.com/java-loadlibrary-windows.asp

当Z3构建目录下有一个Java应用程序时，什么是工作。任何人都可以帮助如何从Java应用程序或Eclipse插件中使用Z3构建目录。顺便说一下，我遵循方法＃2，工作正常，直到我试图复制它（因为我的笔记本电脑崩溃），并被迫使用另一台笔记本电脑，然后同样的过程不适合我（我有运气，之前）。眼下，新的笔记本电脑具有以下设置：

HP Laptop (AMD, x64) 

C:\Users\nmd02\git\resa_mars_workspace>java -version 
java version "1.8.0_144" 
Java(TM) SE Runtime Environment (build 1.8.0_144-b01) 
Java HotSpot(TM) 64-Bit Server VM (build 25.144-b01, mixed mode) 

PATH：

%SystemRoot%\system32;%SystemRoot%;%SystemRoot%\System32\Wbem;%SYSTEMROOT%\System32\WindowsPowerShell\v1.0\;C:\Program Files (x86)\QuickTime\QTSystem\;C:\Program Files\MATLAB\2017a\runtime\win64;C:\Program Files\Java\jdk1.8.0_144\bin;C:\Program Files\Git\cmd;C:\Program Files\CMake\bin;C:\MinGW\bin;C:\python36;C:\Users...git\ninja;C:\Program Files (x86)\Windows Kits\8.1\Windows Performance Toolkit\;C:\gnuwin32\bin

我真的很感激为您的帮助提前。

干杯， /NAS

Answer 1

在运行时代码需要找到com.microsoft.z3.jar，libz3.dll/.so/.dylib和libz3java.dll/.so/.dylib。 Java需要处理第一个操作系统，但操作系统必须找到其他库，也就是说，无论您的代码运行在哪个环境中，都必须设置为使得PATH（Windows），LD_LIBRARY_PATH（Linux）或DYLD_LIBRARY_PATH（OSX）点到图书馆。另外，请确保您的Z3版本和您的Java版本都是32位或64位，否则您得到的错误消息可能不会很有用。

对于某些Java版本，将java.library.path设置提供给JVM可能也是必要的或有帮助的。