Skip to content
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

Problems with installation #463

Open
cloerkes opened this issue Mar 21, 2025 · 9 comments · May be fixed by #467
Open

Problems with installation #463

cloerkes opened this issue Mar 21, 2025 · 9 comments · May be fixed by #467

Comments

@cloerkes
Copy link

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
Copy link
Contributor

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
Copy link
Contributor

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

@cloerkes
Copy link
Author

cloerkes commented Mar 24, 2025

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
Copy link
Contributor

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
Copy link
Member

kfriedberger commented Mar 24, 2025

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
Copy link
Member

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
Copy link
Author

cloerkes commented Apr 9, 2025

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
Copy link
Member

kfriedberger commented Apr 10, 2025

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
Copy link
Member

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Development

Successfully merging a pull request may close this issue.

3 participants