Problems with installation

[cloerkes]

Hi, I am facing problems during the installation of JavaSMT. Could anyone please help me with appropriate build.xml and ivy.xml? You can find my current attempts attached, but they do not work as intended. Furthermore, I am not sure if I am to use ivysettings.xml (as given under /build) and where to put it. If you need any more information, please let me know.

Thank you in advance!

[daniel-raffler]

Hello,
We have an example project for Maven here. Maybe this would work as a starting point? Setting up Ivy is a little more complicated as it requires you to write your own Ant script for the project.

[daniel-raffler]

If you'd prefer to use Ant/Ivy I've now written an example project here:
Example-Ivy-Project.zip

[cloerkes]

Thank you, this helped a lot! However, I am still struggling with the available solvers. The example project outputs that only Princess and SMTInterpol are available (I work on a Windows x64 machine). How can I install Bitwuzla, Z3 and CVC5?

Edit: I managed to install at least CVC5 to Java-SMT (via WSL). Its version is 1.0.5, the latest version is 1.2.1. Is there a possibility to access a newer (or even the newest) version of a solver, e.g. CVC5?

[daniel-raffler]

Thank you, this helped a lot!

That's great to hear!

However, I am still struggling with the available solvers. The example project outputs that only Princess and SMTInterpol are available (I work on a Windows x64 machine). How can I install Bitwuzla, Z3 and CVC5?

Did you use the Maven project or the zip file I uploaded? If you used the project from the zip file the solver binaries should already have been downloaded. However, on Windows they still have to be copied/linked to a different location before they can be used. You can either do this manually by following these instructions, or as part of the Ant build script.

Here is an updated version of the project that copies the binaries automatically:
Example-Ivy-Project.zip

Edit: I managed to install at least CVC5 to Java-SMT (via WSL). Its version is 1.0.5, the latest version is 1.2.1. Is there a possibility to access a newer (or even the newest) version of a solver, e.g. CVC5?

We're working on an upgrade for CVC5 and it should be available soon.

Currently Z3, Mathsat, Bitwuzla, SMTInterpol and Princess are supported on Windows. With the update CVC5 it will also become available.

[kfriedberger]

There should be no need to copy dependencies (or create symlink) in a user-sided application. The copy- or symlink-approach is only required for internal development in JavaSMT itself. Other projects should use a proper environment variable like PATH or CLASSPATH or LD_LIBRARY_PATH to load native libraries.

An example project using JavaSMT with Ant/Ivy is CPAchecker: https://gitlab.com/sosy-lab/software/cpachecker , e.g., with CLASSPATH settings from here: https://gitlab.com/sosy-lab/software/cpachecker/-/blob/main/bin/cpachecker?ref_type=heads#L69

[kfriedberger]

The availability of CVC5 on Windows is currently waiting on PR #454 . We still try to minimize the number of dependencies and libraries required by CVC5, e.g., by static linking.

[cloerkes]

Hi, I understand that you updgraded CVC5 in the meantime (from looking at the linked PR). Ant/Ivy did not automatically synchronize this upgrade locally. What is the easiest way to do so? Thank you in advance!

[kfriedberger]

We updated CVC5 as dependency in our development (master) branch. This is not synchronized with any already released version. There are several ways that your installation receives the newest version of CVC5:

1. we provide a (intermediate) release of JavaSMT in Ivy and Maven --> simplest way for you, just update the version numbers in your dependency file (ivy.lmx or pom.xml). We do this regularly, if we think that the current version is stable and we have some spare time ⏲.
2. you install CVC5 on your own, e.g., by updating only the version number of CVC5 in your dependency file (only for developers, could work, or maybe not, because their API changed and JavaSMT needs to be updated) ⚙
3. you compile JavaSMT on your own and include the latest versions of CVC5.

For point 1: I will provide a release version on weekend.

Additionally, you need to check that your dependency management updates any dependent copied files of binary libraries. This is under your own control, as only you know about your project, i.e., where Ivy or Maven copy any files.

[kfriedberger]

Update:
Intermediate version java-smt-5.0.1-523-g9001c0ea4 was released to ivy and Maven. It contains references to the latest solver integration.

[cloerkes]

I am sorry to bother you again, but unfortunately I am still not able to access the latest solver versions. I currently use the WSL (Windows Subsystem for Linux) to execute ant. When I run the example project (with adapted revision number for java-smt), none of the solvers shows an updated version (compared to the status before the intermediate version). Even worse, CVC5 switches from 1.0.5 to "not available". I am afraid the posts from March 24th confused me quite a bit regarding copying of solver binaries.
In case you need more information about my setup, please let me know. Every little help is appreciated. Thank you!

[kfriedberger]

Windows does not support proper symlinks. Thus, I assume that your depentent native libraries in the directory 'lib/native' are outdated. Please cleanup that directory, e.g. remove all so-files, and then copy over the newer files from the directory where Ivy downloaded the latest version, e.g. 'lib/java/runtime-z3/'.

[daniel-raffler]

Hello Daniel,
the example project was missing a symlink, and that's probably why CVC5 didn't work. I've updated it once more and all the binaries now get copied to avoid issues like this in the future:
Example-Ivy-Project.zip

Could you give it another try?