-
Notifications
You must be signed in to change notification settings - Fork 44
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Using native solvers from a dependent Maven package #393
Labels
Comments
Towards the second solution: SolverContextFactory. |
Thank you, that seems to work. For reference, this is my solution now: Creating the SolverContext
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
<build>
<plugins>
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-dependency-plugin</artifactId>
<version>3.1.1</version>
<executions>
<!-- "copy" renames the native dependencies from their internal Maven name to the normal
library name -->
<execution>
<id>copy</id>
<phase>initialize</phase>
<goals>
<goal>copy</goal>
</goals>
</execution>
</executions>
<configuration>
<outputDirectory>${project.dependency.path}</outputDirectory>
<overWriteReleases>true</overWriteReleases>
<artifactItems>
<artifactItem>
<groupId>org.sosy-lab</groupId>
<artifactId>javasmt-solver-z3</artifactId>
<type>so</type>
<classifier>libz3java</classifier>
<destFileName>libz3java.so</destFileName>
</artifactItem>
<artifactItem>
<groupId>org.sosy-lab</groupId>
<artifactId>javasmt-solver-z3</artifactId>
<type>so</type>
<classifier>libz3</classifier>
<destFileName>libz3.so</destFileName>
</artifactItem>
</artifactItems>
</configuration>
</plugin>
</plugins>
<resources>
<resource>
<directory>${project.dependency.path}</directory>
</resource>
</resources>
</build> This seems rather convoluted, though. Is there a better/intended way to do this? |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
I have two Maven packages: In
project1
I usejava-smt
with native solvers (specifically Z3). I then installproject1
to my local Maven repository, and use it inproject2
(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 theorg.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 runproject2
. As far as I can tell, this happens becauseorg.sosy_lab.common.NativeLibraries.loadLibrary()
tries to find the native libraries in the directory of theorg.sosy_lab.common
JAR, or injava.library.path
, andproject2
doesn't have the native libraries copied to adependency
directory with theorg.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 thatjava-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 tojava.library.path
, but adding library directories at runtime doesn't seem to work.The text was updated successfully, but these errors were encountered: