java-smt
java-smt copied to clipboard
sosy-lab
Installation of CVC4
The explanations for installation do not mention all solvers.
E.g. CVC4 is missing. The website seems to have only an .exe for windows. Which files are needed and where to get them?
For Linux users:
We provide all necessary files in our Ivy repository. When using Ant/Ivy as build tool, those dependencies are automatically installed. For manual installation, please check the dependencies in the ivy-xml file to get the correct version. CVC4 is build from source using the steps written in the build script.
For Windows users:
We are currently working on supporting more solvers on more operating systems. CVC4 can be build from source for Windows using Mingw-w64. I will test this and report back here. My plan is to also provide those binaries in our Ivy repository.
A quick initial test showed several problems when compiling the Java bindings for Windows. If really needed, I will investigate further. However, for myself and our group, running other solvers than CVC4 on Windows has higher priority.
I would greatly appreciate your efforts. In fact, I am currently using Z3 with its API but I would like to add support to my tool (with windows and linux users) for CVC4 because it is able to simplify some expressions for which Z3 does not succeed.
Current status: CVC4 dropped support for Java and will re-implement it in the future. Until then we stay with the existing version, which is the revision shortly before they dropped Java support. The existing release does not allow to build a Windows binary with Java bindings. This might be an option conflict in the build script, further documentation and information is currently missing.
CVC4 is superseeded by CVC5. JavaSMT will provide both solvers for some time and then drop support for CVC4.