Comment lier la compilation Z3, compilée pour Java, à partir du plugin Eclipse?

Question

J'ai un système Z3 Build parfaitement fonctionnel pour Java. Je veux l'appeler à partir d'un plugin Eclipse. J'ai essayé plusieurs approches, mais aucune d'entre elles ne fonctionne pour moi. Ces approches sont:

1. Ajout Z3 construit comme un dossier de classe externe 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)

2. Copié Z3 construire au plug-in Eclipse, à la racine. Puis ajouté com.microsoft.z3.jar sous les bibliothèques (clic droit sur le projet-> Build Path-> Configurer le chemin de construction-> Bibliothèques-> Ajouter des bocaux). L'erreur est:

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)

3. Avec ou sans l'étape précédente, j'ai ajouté com.microsoft.z3.jar à Classpath, situé dans l'onglet plugin.xml Runtime. Dans ce cas, le plug-in ne trouve pas le gestionnaire invoqué après la commande de touche.

!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

En fait, cette approche a fonctionné pour moi une une installation précédente (Dell, Intel, x64, Eclipse Mars (x64), Java 1.8 x64)!

4. Suite à la discussion dans https://github.com/Z3Prover/z3/issues/1093, j'ai configuré l'emplacement de la bibliothèque native de com.microsoft.z3.jar avec le répertoire Z3 Build. L'appel de la Z3 Construire à partir de plug-in Eclipse, l'erreur signalée est le même que dans l'approche 2, mais l'appeler à partir d'une application Java, l'erreur est plus spécifique:

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)

5. Autre https://www.chilkatsoft.com/java-loadlibrary-windows.asp

Ce qui fonctionne est lorsque vous avez une application Java dans le répertoire de construction Z3. Quelqu'un peut-il aider à utiliser le répertoire de construction Z3 à partir d'une application Java ou du plugin Eclipse. En passant, j'ai suivi l'approche # 2, fonctionnait bien jusqu'à ce que j'essaie de le répliquer (parce que mon ordinateur portable s'est écrasé) et forcé d'utiliser un autre ordinateur portable, alors la même procédure ne fonctionne pas pour moi. En ce moment, le nouvel ordinateur portable a les paramètres suivants:

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) 

CHEMIN:

%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

Je vous remercie vraiment pour votre aide à l'avance.

Cheers, /Nas

Answer 1

Lors de l'exécution de votre code doit trouver com.microsoft.z3.jar, libz3.dll/.so/.dylib et libz3java.dll/.so/.dylib. Java prend en charge le premier, mais le système d'exploitation devra trouver les autres bibliothèques, c'est-à-dire que l'environnement dans lequel votre code s'exécute doit être configuré de telle sorte que PATH (Windows), LD_LIBRARY_PATH (Linux) ou DYLD_LIBRARY_PATH (OSX) aux bibliothèques. Assurez-vous également que votre version de Z3 et votre version de Java sont à la fois 32 bits ou 64 bits, sinon les messages d'erreur que vous obtenez peuvent ne pas être très informatifs.

Pour certaines versions de Java, il peut également être nécessaire ou utile de fournir le paramètre java.library.path à la machine virtuelle Java.