Z3 Java API for v4.3.2

Mar 4, 2015 at 1:46 AM
Edited Mar 4, 2015 at 1:51 AM
Hi,

I am unable to compile Z3 with Java binding.

I am using z3 source from commit cee7dd39444c9060186df79c2a2c7f8845de415b
Author: Christoph M. Wintersteiger
Date: Fri Oct 24 23:52:40 2014

The discussion here: http://stackoverflow.com/questions/26530162/z3-solver-stable-version-for-java-api?rq=1 suggests that Java API is available in main branch for the above commit.

For compiling, I pass --java flag to mk_make.py

followed by make which reports error in src/api/java/Native.cpp

The top few lines of the error are
../src/api/java/Native.cpp: In function ‘void Java_com_microsoft_z3_Native_INTERNALglobalParamSet(JNIEnv_methods**, jclass, jstring, jstring)’:
../src/api/java/Native.cpp:74:37: error: request for member ‘GetStringUTFChars’ in ‘* jenv’, which is of pointer type ‘JNIEnv’ (maybe you meant to use ‘->’ ?)
   Z3_string _a0 = (Z3_string) jenv->GetStringUTFChars(a0, NULL);
                                     ^
../src/api/java/Native.cpp:75:37: error: request for member ‘GetStringUTFChars’ in ‘* jenv’, which is of pointer type ‘JNIEnv’ (maybe you meant to use ‘->’ ?)
   Z3_string _a1 = (Z3_string) jenv->GetStringUTFChars(a1, NULL);
                                     ^
../src/api/java/Native.cpp: In function ‘jboolean Java_com_microsoft_z3_Native_INTERNALglobalParamGet(JNIEnv_methods**, jclass, jstring, jobject)’:
../src/api/java/Native.cpp:82:37: error: request for member ‘GetStringUTFChars’ in ‘* jenv’, which is of pointer type ‘JNIEnv’ (maybe you meant to use ‘->’ ?)
   Z3_string _a0 = (Z3_string) jenv->GetStringUTFChars(a0, NULL);
                                     ^
../src/api/java/Native.cpp:86:27: error: request for member ‘GetObjectClass’ in ‘* jenv’, which is of pointer type ‘JNIEnv’ (maybe you meant to use ‘->’ ?)
      jclass mc    = jenv->GetObjectClass(a1);
                           ^
../src/api/java/Native.cpp:87:27: error: request for member ‘GetFieldID’ in ‘* jenv’, which is of pointer type ‘JNIEnv’ (maybe you meant to use ‘->’ ?)
      jfieldID fid = jenv->GetFieldID(mc, "value", "J");
                           ^
../src/api/java/Native.cpp:88:12: error: request for member ‘SetLongField’ in ‘* jenv’, which is of pointer type ‘JNIEnv’ (maybe you meant to use ‘->’ ?)
      jenv->SetLongField(a1, fid, (jlong) _a1);
So, essentially it appears to be having problems with jenv .

Java and cpp compiler versions in my environment are:
jhask@berkeley:~/tools/z3-zip/build$ java -version
java version "1.7.0_76"
Java(TM) SE Runtime Environment (build 1.7.0_76-b13)
Java HotSpot(TM) 64-Bit Server VM (build 24.76-b04, mixed mode)

jhask@berkeley:~/tools/z3-zip/build$ javac -version
javac 1.7.0_76

jhask@berkeley:~/tools/z3-zip/build$ g++ --version
g++ (Ubuntu 4.8.2-19ubuntu1) 4.8.2
Could someone point me to what could be wrong in my setup or have I run into some bug with the Java API binding ?

Thanks,
Susmit
Mar 4, 2015 at 2:40 AM
Switching from IKVM to JVM for jni fixed the above problem.

But now, it complains about missing z3java :
jhask@berkeley:~/tools/z3-contrib/examples/java$ java -cp ../../build/com.microsoft.z3.jar:. -Djava.library.path=~/tools/z3-contrib/build/ JavaExample
Exception in thread "main" java.lang.UnsatisfiedLinkError: no z3java in java.library.path
    at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1886)
    at java.lang.Runtime.loadLibrary0(Runtime.java:849)
    at java.lang.System.loadLibrary(System.java:1088)
    at com.microsoft.z3.Native.<clinit>(Native.java:12)
    at com.microsoft.z3.Context.ToggleWarningMessages(Context.java:2910)
    at JavaExample.main(JavaExample.java:2165)
I can see the so files in the given path
jhask@berkeley:~/tools/z3-contrib/examples/java$ ls ~/tools/z3-contrib/build/
api                   libz3java.so  qe      z3            z3poly.pyc     z3test.pyc
ast                   libz3.so      sat     z3consts.py   z3printer.py   z3types.py
cmd_context           Makefile      shell   z3consts.pyc  z3printer.pyc  z3types.pyc
com.microsoft.z3.jar  math          smt     z3core.py     z3.py          z3util.py
config.mk             model         solver  z3core.pyc    z3.pyc         z3util.pyc
duality               muz           tactic  z3num.py      z3rcf.py
example.py            nlsat         test    z3num.pyc     z3rcf.pyc
interp                parsers       util    z3poly.py     z3test.py
My LD_LIBRARY_PATH also includes path to the build directory
jhask@berkeley:~/tools/z3-contrib/examples/java$ echo $LD_LIBRARY_PATH
/home/jhask/tools/z3-contrib/build:/home/jhask/tools/z3-contrib/build/:/home/jhask/tools/z3/lib/
I have also tried switching the name z3java to libz3java in Native.cpp of src/api/java and recompiling - it does not help.

Any suggestion on how to resolve this problem ?
Coordinator
Mar 4, 2015 at 12:23 PM
Thanks for reporting this issue. Regarding the first problem, it seems that IKVM.NET doesn't support all parts of JNI yet. Was IKVM.NET the default choice for Java on your system? If so, could you let us know what kind of system you're using?
Coordinator
Mar 4, 2015 at 12:30 PM
Regarding the second problem, it seems that for some reason the JVM can't find libz3java.so. There are lots of reasons for why this could be the case. Before going further, try to see whether both, your Java distributions is 64-bit and libz3java.so and libz3.so are also compiled for 64-bit. Any mismatch between those will produce problems now or later, and the error messages are not always helpful. Another common issue that LD_LIBRARY_PATH is called DYLD_LIBRARY_PATH on OSX.
Coordinator
Mar 4, 2015 at 1:58 PM
I'm now able to reproduce this problem, but only when using version 7 of the JDK. Everything works fine using version 8, so updating the JDK could be a quick fix for users. I wasn't able to figure out why exactly version 7 refuses to load the .so yet though.
Coordinator
Mar 4, 2015 at 3:32 PM
This now resolved (as of this fix). The reason for this problem was that the default linkage of symbols in shared libraries had changed in GCC 4.x, requiring a change in the default linkage declarations within JNI. Consequently, on systems with new GCC and old Java, the linkage declarations didn't match up.
Mar 4, 2015 at 6:24 PM
Thanks a lot, Wintersteiger !

I was able to run the Java example in the distribution with the fixed version albeit with the following 2 errors:
  1. fpa error (I commented out call to both floatingpoint examples)
    java: symbol lookup error: /home/jhask/tools/java-z3/z3/build/libz3java.so: undefined symbol: Z3_mk_fpa_sort
  2. log error ( I commented out all log.append calls)
    Z3 error: com.microsoft.z3.Z3Exception: parser error
    ITEExample
    Z3 Managed Exception: Log cannot be closed.
    Stack trace:
    com.microsoft.z3.Z3Exception: Log cannot be closed.
    at com.microsoft.z3.Log.append(Log.java:59)
    at JavaExample.iteExample(JavaExample.java:1585)
    at JavaExample.main(JavaExample.java:2318)
After commenting both of these out, the example went through smoothly.

Yes, I was using old java and new gcc (confirming for anyone that runs into this issue again)
jhask@berkeley:~/tools/java-z3/z3/examples/java$ javac -version
javac 1.7.0_75
jhask@berkeley:~/tools/java-z3/z3/examples/java$ java -version
java version "1.7.0_75"
OpenJDK Runtime Environment (IcedTea 2.5.4) (7u75-2.5.4-1~trusty1)
OpenJDK 64-Bit Server VM (build 24.75-b04, mixed mode)
jhask@berkeley:~/tools/java-z3/z3/examples/java$ gcc --version
gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
Copyright (C) 2013 Free Software Foundation, Inc.
This is free software; see the source for copying conditions.  There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
jhask@berkeley:~/tools/java-z3/z3/examples/java$ g++ --version
g++ (Ubuntu 4.8.2-19ubuntu1) 4.8.2
Copyright (C) 2013 Free Software Foundation, Inc.
This is free software; see the source for copying conditions.  There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
Once again thanks, Winstersteiger. I will update my Java to 1.8.
Coordinator
Mar 5, 2015 at 12:41 PM
This is very strange; I haven't seen any such errors on any system yet. The problem with Z3_mk_fpa_sort might be that it was added fairly recently and that you didn't re-run scripts/mk_make.py after it was added (that script generates large parts of the APIs too). Could you try getting a fresh copy of the unstable branch and then compile it from scratch, so we can see whether there is some problem with your system or with the code?
Mar 6, 2015 at 12:51 AM
Thanks, Wintersteiger.


================== STABLE BRANCH ==================================================================
The above is from the stable branch - your commit ec4a07318e700b2ee434e4aa118919830879ec8a

This is the one which was showing issues with log and mk_fpa_sort .

I reran mk_make.py with --java flag and then did a make in build directory.

With the example Java file, I get
jhask@berkeley:~/tools/java-z3/z3/examples/java$ java -cp ../../build/com.microsoft.z3.jar:. -Djava.library.path=../../build/ JavaExample
Z3 Major Version: 4
Z3 Full Version: 4.3.2.0
SimpleExample
Z3 Managed Exception: Log cannot be closed.
Stack trace: 
com.microsoft.z3.Z3Exception: Log cannot be closed.
    at com.microsoft.z3.Log.append(Log.java:59)
    at JavaExample.simpleExample(JavaExample.java:185)
    at JavaExample.main(JavaExample.java:2294)
jhask@berkeley:~/tools/java-z3/z3/examples/java$ 
Removing all the logs from the file, exposes error for mk_fpa_sort
FloatingPointExample1
java: symbol lookup error: /home/jhask/tools/java-z3/z3/build/libz3java.so: undefined symbol: Z3_mk_fpa_sort
Since I am the only one running into the problem, it is highly likely its an environment issue. I am dumping as much information as possible below in case someone else runs into it.
jhask@berkeley:~/tools/java-z3/z3/examples/java$ java -version
java version "1.8.0_31"
Java(TM) SE Runtime Environment (build 1.8.0_31-b13)
Java HotSpot(TM) 64-Bit Server VM (build 25.31-b07, mixed mode)
jhask@berkeley:~/tools/java-z3/z3/examples/java$ javac -version
javac 1.8.0_31
jhask@berkeley:~/tools/java-z3/z3/examples/java$ gcc --version
gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
Copyright (C) 2013 Free Software Foundation, Inc.
This is free software; see the source for copying conditions.  There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

jhask@berkeley:~/tools/java-z3/z3/examples/java$ g++ --version
g++ (Ubuntu 4.8.2-19ubuntu1) 4.8.2
Copyright (C) 2013 Free Software Foundation, Inc.
This is free software; see the source for copying conditions.  There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

jhask@berkeley:~/tools/java-z3/z3/examples/java$ echo $JNI_HOME
/usr/lib/jvm/java-8-oracle/include/
jhask@berkeley:~/tools/java-z3/z3/examples/java$ echo $JDK_HOME
/usr/lib/jvm/java-8-oracle
jhask@berkeley:~/tools/java-z3/z3/examples/java$ 
======================UNSTABLE BRANCH ====================================================

I checked out the unstable branch - your commit 55ca6ce44b2f6963831209528a8b49728c7c58bf
This worked out perfectly.


Once again, I really appreciate your quick response and taking time to help us !