Z3 for Java in Eclipse

Jul 26, 2013 at 6:51 PM
Edited Jul 27, 2013 at 11:48 AM
Hi,

I'm trying to use z3 for my project. What I has done is:
The program was compiled OK, but when running it, I was given an error:
Exception in thread "main" java.lang.UnsatisfiedLinkError: no z3java in java.library.path
    at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1860)
    at java.lang.Runtime.loadLibrary0(Runtime.java:845)
    at java.lang.System.loadLibrary(System.java:1084)
    at com.microsoft.z3.Native.<clinit>(Native.java:10)
    at com.microsoft.z3.Context.ToggleWarningMessages(Context.java:2907)
Could you give me an advice how I should fix this error?
Thank you.
Coordinator
Jul 29, 2013 at 12:43 PM
What you did is correct, however the .so files must be visible at runtime. This means, the path in which they reside must be in LD_LIBRARY_PATH on Linux, or simply in PATH on Windows. The easiest way is to either set the Working Directory to your lib directory in Eclipse (in the run/debug configuration, Arguments), or to copy the .so files over to where your binary is produced.
Jul 29, 2013 at 4:28 PM
Thank you for your reply.

Actually, I already set the LD_LIBRARY_PATH in .bashrc, but Eclipse doesn't recognize it. Following your advice, I set environment variable in the run configuration, and it works for me.
Name: LD_LIBRARY_PATH
Value: ${project_loc}/lib:$LD_LIBRARY_PATH
Thanks again.
Jan 10, 2014 at 6:52 AM
Hey,

I tried the above steps in eclipse still m getting this error
Exception in thread "main" java.lang.UnsatisfiedLinkError: no z3java in java.library.path

Please help me.
thanks in advance.
Coordinator
Jan 10, 2014 at 11:39 AM
Hi vadave,

could you give us a little bit more information about your system and setup? E.g., on OSX LD_LIBRARY_PATH is called DYLD_LIBRARY_PATH, so that could be the problem.

Cheers,
Christoph
Jan 15, 2014 at 6:31 AM
Hi Christoph,

I am using Windows.
above error is for eclipse.
from command prompt I am getting error regarding Expr class not found thuogh I have set the classpaths.
Can you please mention all the steps from the first to run that JavaExample.java file .
Thanks for your help.

Regards,
vadave
Coordinator
Jan 15, 2014 at 4:54 PM
This is a different error, most probably because com.microsoft.z3.jar hasn't been added to the classpath.

The README in the java example directory gives instructions for running the example, but they are very simple:
java -cp com.microsoft.z3.jar;. JavaExample
This assumes that java is executed in the build directory, otherwise the paths have do be adapted accordingly. Note that, on Windows, the current directory is included in the search path for .dll files, so if libz3.dll is in the current directory it will find it. If this is not the case, that directory needs to be added to the PATH variable.

The steps for building the example, com.microsoft.z3.jar, and libz3java.dll can be seen in the Makefile in the build directory, but the crucial bit of information is again that all the paths have to be set up correctly. Note that both, libz3.dll and libz3java.dll are required at runtime.

In your specific case you say "in eclipse" but then "from the command line".... This can be very confusing, because eclipse sets up a fresh environment for run/debug runs and all the respective environment variables have to be set inside the run/debug configuration that you're trying to run. From your description I guess that everything compiles inside of eclipse but at runtime throws an unsatisfied link exception (you just need to add the path to where libz3.dll and libz3java.dll reside to the PATH in your run configuration). To compile on the command line, the classpath has to be given to the compiler as well, e.g., the instructions for building JavaExample.class in my Makefile are as follows:
"C:\Program Files (x86)\Java\jdk1.7.0_40\bin\javac.exe" -cp com.microsoft.z3.jar  ..\examples\java\JavaExample.java -d .
Jan 16, 2014 at 9:52 AM
Thanks. Its working now. I was trying with .so file in windows. Due to that error was there.

If you are working on z3 for java can you pls help a little bit more.? If you have any small codes to understand it then can you pls mail me?
Coordinator
Jan 16, 2014 at 2:57 PM
Great, good to hear it's working now!

All the examples we have are collected in JavaExample.java (its a collection of many functions, each of which shows some basic usecase). The best place to start is probably the SimpleExample and BasicTests functions.
Jan 17, 2014 at 8:53 AM
okay.
I am actually trying to understand the same program.
and thanks for the reply.
Jan 21, 2014 at 10:24 AM
hello,

Can you please elaborate arguments of MkForAll() function. I want to implement "for all x, if librarian(x) then employee(x)".

This is my code:
            FiniteDomainSort fdse = ctx.MkFiniteDomainSort("Employees", 10);
    FiniteDomainSort fdsl = ctx.MkFiniteDomainSort("Librarian", 2);
    FiniteDomainSort fdsi = fdse;

    FuncDecl employee = ctx.MkFuncDecl("employee", fdse, ctx.MkBoolSort());
    FuncDecl librarian = ctx.MkFuncDecl("librarian", fdsl, ctx.MkBoolSort());

    BoolExpr lib_y = (BoolExpr) ctx.MkApp(librarian, ctx.MkConst("y", fdsl));
    BoolExpr emp_z = (BoolExpr) ctx.MkApp(employee, ctx.MkConst("y", fdse));

            Expr[] bound1 = new Expr[] {lib_y};
    Expr body1 = ctx.MkImplies(lib_y, emp_z);
// Expr body1 = ctx.MkImplies((BoolExpr)ctx.MkApp(librarian, ctx.MkConst("y", fdsl)),(BoolExpr) ctx.MkApp(employee,ctx.MkConst("y", fdse)));
// Expr body1 =emp_z;
    BoolExpr q1 = ctx.MkForall(bound1, body1, 1, null, null, null,null);
What is the problem with this code?

And also I want to know can we concatenate 2 sorts to create a new sort?
Coordinator
Jan 21, 2014 at 5:54 PM
Z3 provides two different ways of creating quantifiers, either by using de Bruijn indexed variables (see e.g., Understanding the indexing of bound variables in Z3), or by giving a list of constants (which are then internally replaced by de Bruijn variables).

You are using the version of MkForall which takes an array of expressions as the first argument. This is meant to be an array of constants, but
Expr[] bound1 = new Expr[] {lib_y};
puts an application of a function to a constant (librarian(y)) into the array. We can change this line to
Expr[] bound1 = new Expr[] { ctx.MkConst("y", fdsl) };
to quantify over y. Z3 will then not complain about an invalid argument anymore.

Here are some more links to questions and answers about quantifier topics that might be of relevance:
C API for Quantifiers
Strange results with quantified formula
Forall quantifier in Z3
Feb 11, 2014 at 7:17 PM
Hello,

I would like to ask you for your help. When I try to make the java api under cygwin, I get the error __int64 not a valid type.

Can you please help me with this? Is there another way to compile?

Thank you in advance for your time and effort.

Best regards,
JAsen
Coordinator
Feb 13, 2014 at 7:41 PM
Hi jasenmarkovski, could you provide me with a little bit more detail about how you build Z3? Does the z3 library (libz3.so/.dll) build correctly and only when building libz3java.so an error is encountered?

Thanks,
Christoph
Feb 20, 2014 at 11:52 AM
Dear Christoph,

Thank you for taking time to review this issue.

I apologize for the delayed reply.

Here is the source of the error:

In file included from /cygdrive/c/Program Files/Java/jdk1.7.0//include/jni.h:43:0,
             from ../src/api/java/Native.cpp:2:
/cygdrive/c/Program Files/Java/jdk1.7.0//include/win32/jni_md.h:35:9: error: ‘__int64’ does not name a
typedef __int64 jlong;


and this is the list of all files in /z3/build after the make stopped (it contains libz3.dll):
$ ls
api config.mk Makefile muz_qe sat solver util z3consts.pyc z3poly.pyc z3types
ast example.py math nlsat shell tactic z3.exe z3core.pyc z3printer.pyc
cmd_context libz3.dll model parsers smt test z3.pyc z3num.pyc z3test.pyc

I also attempted a build using Visual studio, but I got an error that the library System.core.dll is missing. Finally, I attempted to use several nightly builds from the Z3 website, but I could not run JavaExample due to missing classes in com.microsoft.z3.jar.

Again, thank you for the time and effort you take in resolving this issue.

Best regards,
Jasen
Coordinator
Feb 21, 2014 at 1:54 PM
Hi Jasen,

I've committed a couple fixes for compilation of the java API in cygwin (see here). This particular issue (__int64 not being defined) should be gone now.

Note that using java from cygwin can be very confusing because it is a normal Windows binary and needs Windows-style paths in the classpath, etc. See, e.g., here.

System.core.dll is an core part of the .NET library, so if that is missing, then something is wrong with your Visual Studio setup. Note that you should build Z3 from the "Visual Studio Command Prompt", of which there are multiple, most notably x86 and x64. I would advise to use whichever one matches your python and java version (they need to be either 32 or 64 bit, but all need to be the same).

Thanks,
Christoph
Feb 21, 2014 at 7:46 PM
Dear Christoph,

Thank you for your time and effort. I have managed to build the Java API and produce a class from the JavaExample. However, when I attempt to run it, I get the follwing error:

Exception in thread "main" java.lang.UnsatisfiedLinkError: no z3java in java.lib
rary.path
    at java.lang.ClassLoader.loadLibrary(Unknown Source)
    at java.lang.Runtime.loadLibrary0(Unknown Source)
    at java.lang.System.loadLibrary(Unknown Source)
    at com.microsoft.z3.Native.<clinit>(Native.java:10)
    at com.microsoft.z3.Context.ToggleWarningMessages(Context.java:2899)
    at JavaExample.main(JavaExample.java:2165)
I have checked that the libraries are in the path and I have copied them to c:\windows\systems32 folder, but nothing works. I do not seem to be able to locate the problem.

Could you maybe suggest something?

Best regards,
Jasen
Coordinator
Feb 22, 2014 at 5:56 PM
Hi Jasen,

the fixes i submitted require that you re-run python scripts/mk_make.py and one of them fixes exactly that problem when used through cygwin. Could you re-run that and then recompile? Thanks!

Christoph
Feb 23, 2014 at 1:30 PM
Dear Christoph,

I did not run Java under Cygwin, but I employed it only to build the Java api. I ran Java under Windows command prompt with PATH to the build libraries. Maybe the Java API I built is not compatible. I will attempt one more time a Visual Studio build after I reinstall it properly.

Again, thank you for your time and effort.

Best regards,
Jasen
Feb 23, 2014 at 7:38 PM
Dear Christoph,

I am sorry for bothering you again, but I have managed finally to make a Visual Studio build and run the JavaExample and I got this error message:

Z3 Major Version: 4
Z3 Full Version: 4.3.2.0
SimpleExample

A fatal error has been detected by the Java Runtime Environment:

EXCEPTION_ACCESS_VIOLATION (0xc0000005) at pc=0x0000000076efd256, pid=395444,

tid=395460

JRE version: Java(TM) SE Runtime Environment (7.0_51-b13) (build 1.7.0_51-b13)

Java VM: Java HotSpot(TM) 64-Bit Server VM (24.51-b03 mixed mode windows-amd64

compressed oops)

Problematic frame:

C [ntdll.dll+0x4d256]

Failed to write core dump. Minidumps are not enabled by default on client vers

ions of Windows

An error report file with more information is saved as:

D:\Temp\z3\build\hs_err_pid395444.log

If you would like to submit a bug report, please visit:

http://bugreport.sun.com/bugreport/crash.jsp

The crash happened outside the Java Virtual Machine in native code.

See problematic frame for where to report the bug.

Is this a known problem or again I did something wrong?

Again, thank you for your time and effort.

Best regards,
Jasen
Coordinator
Feb 24, 2014 at 2:17 PM
Hi Jasen,

This kind of crash means that something in the native layer went wrong, but I need more information to be able to reproduce this error. Can you give me all the version numbers of your toolchain (python, visual studio, java) and the output and parameters of python scripts/mk_make.py?

Thanks,
Christoph
Coordinator
Feb 24, 2014 at 2:35 PM
Jasen: Also, what is your version of Windows? This kind of error would be expected on Windows XP, which is not supported. (See also here.)
Feb 26, 2014 at 12:18 PM
Dear Christoph,

Indeed I was using Windows XP. I upgraded now to Win 7 x64 and I managed to get it right.

Thank you again for your time and patience.

Best regards,
Jasen