jConstraints-z3 is a plugin for jConstraints, adding support for Z3 as a constraint solver.
Z3 is not distributed along with jConstraints-z3, but is available at The Z3 Theorem Prover's GitHub repository.
Note: Installing Z3 requires git, python, maven, and a C++
compiler to be installed and to reside in your PATH environment
variable.
The following instructions are taken from the README from The Z3 Theorem Prover's GitHub repository.
First, clone Z3:
git clone https://github.com/Z3Prover/z3.gitMake sure that you use the 4.4.1 release:
git checkout z3-4.4.1Next, we generate a Z3 Makefile with the --java option to get the Z3 Java bindings.
python scripts/mk_make.py --javaNow, we build Z3
cd build
make allMake sure to install libz3.so and libz3java.so (extension .dylib
in OSX) to a global library folder or to one that is contained in your
java.library.path property (the LD_LIBRARY_PATH for Linux and DYLD_LIBRARY_PATH for OS X).
Install the com.microsoft.z3.jar file from the build directory of
your Z3 working copy into the local Maven directory:
mvn install:install-file -Dfile=com.microsoft.z3.jar -DgroupId=com.microsoft -DartifactId=z3 -Dversion=4.4.1 -Dpackaging=jar- In the jConstraints-z3 folder, run
mvn install - If the compilation was successful, the jConstraints-z3
library can be found in the JAR file
target/jconstraints-z3-[VERSION].jar - jConstraints loads extensions automatically from the
~/.jconstraints/extensionsfolder in the user's home directory. Create this directory and copycom.microsoft.z3.jar(from Z3, see above) andjConstraints-z3-[version].jarinto this folder.
jconstraints-z3 supports setting some of the options in z3 via constructor parameters or configuration options:
z3.timeout=[timeout in millis]
z3.options=[option1]=[value1];[option2]=[value2];...
Example:
z3.timeout=2
z3.options=smt.mbqi=true;smt.macro-finder=true