mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity
z3/examples/java
History
Alexander Kreuzer dc5fa89de3
Mixing Integers and Rational in the new Java API #5085 (#5098) 
* Added covariance to arithmetic operations

* Added distillSort

* Update JavaGenericExample.java

Co-authored-by: Alexander Kreuzer <alexander.kreuzer@sap.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-03-16 05:24:23 -07:00
..
JavaExample.java Java type generics (#4832) 2020-11-30 10:04:54 -08:00
JavaGenericExample.java Mixing Integers and Rational in the new Java API #5085 (#5098) 2021-03-16 05:24:23 -07:00
README Refer to macOS rather than Mac OS / OSX. 2018-10-02 17:38:09 +07:00

README 

A small example using the Z3 Java bindings.   

To build the example, configure Z3 with the --java option to scripts/mk_make.py, build via  
   make examples
in the build directory.

It will create JavaExample.class in the build directory,
which can be run on Windows via 
   java -cp com.microsoft.z3.jar;. JavaExample

On Linux and FreeBSD, we must use
   LD_LIBRARY_PATH=. java -cp com.microsoft.z3.jar:. JavaExample
On macOS, the corresponding option is DYLD_LIBRARY_PATH:
   DYLD_LIBRARY_PATH=. java -cp com.microsoft.z3.jar:. JavaExample