Using native solvers from a dependent Maven package

[jasper-vb]

I have two Maven packages: In project1 I use java-smt with native solvers (specifically Z3). I then install project1 to my local Maven repository, and use it in project2 (where I set up the solver context etc.).

When I run project1 directly, I can successfully create the solver context by following the method outlined in the Example-Maven-Project, i.e. copying the org.sosy_lab.common JAR and the native libraries to the same directory and setting the classpath there.

However, this fails when I create an uber-JAR (JAR with dependencies) using maven-shade-plugin and try to run that, or when I try to run project2. As far as I can tell, this happens because org.sosy_lab.common.NativeLibraries.loadLibrary() tries to find the native libraries in the directory of the org.sosy_lab.common JAR, or in java.library.path, and project2 doesn't have the native libraries copied to a dependency directory with the org.sosy_lab.common JAR.

Is there a way to get native solvers working with either uber-JARs or dependent packages?

---

Alternatively, is there some way to load the libraries from a custom path? Usually when I depend on a native library, I package it as a resource, extract that to a temporary file and then load it using System.loadLibrary() with the absolute path. I've tried doing that, but it seems that java-smt tries to load the native libraries again anyways (and fails). I've also tried extracting the libraries to a temporary directory and adding that to java.library.path, but adding library directories at runtime doesn't seem to work.

[ThomasHaas]

Towards the second solution: SolverContextFactory. I haven't tried it myself, but it seems you can pass a path (pLoader argument) to look for native libraries in custom locations.

[jasper-vb]

Thank you, that seems to work. For reference, this is my solution now:

Creating the SolverContext

```java public class Util { private static void loadLibrary(String library) { if (library.equals("z3") || library.equals("z3java")) { System.out.println("Loading library: " + library); String filename = System.mapLibraryName(library); int pos = filename.lastIndexOf('.'); Path file; try { file = Files.createTempFile(filename.substring(0, pos), filename.substring(pos)); file.toFile().deleteOnExit(); try (var in = Util.class.getClassLoader().getResourceAsStream(filename); var out = Files.newOutputStream(file)) { in.transferTo(out); } System.load(file.toAbsolutePath().toString()); } catch (IOException e) { throw new UnsatisfiedLinkError(e.getMessage()); } } else { System.out.println("Loading other library: " + library); System.loadLibrary(library); } } public static SolverContext createSolverContext(Solvers solvers) throws InvalidConfigurationException { return SolverContextFactory.createSolverContext(Configuration.defaultConfiguration(), org.sosy_lab.common.log.LogManager.createNullLogManager(), ShutdownNotifier.createDummy(), solvers, Util::loadLibrary); } } ```

pom.xml

```xml org.apache.maven.plugins maven-dependency-plugin 3.1.1 copy initialize copy ${project.dependency.path} true org.sosy-lab javasmt-solver-z3 so libz3java libz3java.so org.sosy-lab javasmt-solver-z3 so libz3 libz3.so ${project.dependency.path} ```

This seems rather convoluted, though. Is there a better/intended way to do this?

[baierd]

When i created the Maven example i also tried to build an example with FAT-Jars and found it to be rather hard with the way we load libs. (In some cases is was even impossible) Since we have a use-case and an example now, we should take a look at how we can improve this in my opinion. @kfriedberger do you agree?

[kfriedberger]

I also thought about providing a fat JAR via Maven, depending on architecture (x64 vs arm64), operating system (Linux vs Windows vs MacOS) and licence (GPL-included vs non-GPL). This would make at least 6 fat JARs. Technically, this is no big issue, as long as a users does not include multiple fat JARs at once.

We would need to provide:

• a small wrapper class for the loading mechanism that extracts the native library from JAR and loads them.
• a Maven package and upload task as configuration for Ant.
• testing.