Java - Windows Intellij: Configure Microsoft z3

When I start configuring Microsoft Z3 solver for Java and for Intellij, I have a lot of difficulties. Here is some important points you must take care of to make it work.

• Download Microsoft Z3 and save it to your folder. e.g: C:\z3-4.8.8-x64-win. Remember the fitness of Z3 must be the same as Java virtual machine. I used the 64-bit version.
• Copy com.microsoft.z3.jar to your libs folder inside the project and add it as a library.
• I get the sample from this link: https://github.com/Z3Prover/z3/blob/master/examples/java/JavaExample.java

package solver;

import com.microsoft.z3.*;

public class z3solver {
    public z3solver() {

    }

    public static void main(String[] args) throws Exception {

//        System.loadLibrary("E:\\Vie" +"t" + "Data\\Th" + "ay Hung\\DSE\\libs\\z3-4.8.8-x64-win\\bin\\lib" + "z3java.dll");
        z3solver solver = new z3solver();
        solver.quantifierExample1();
    }

    public void simpleExample() {
        System.out.println("SimpleExample");
        Log.append("SimpleExample");

        {
            Context ctx = new Context();
            /* do something with the context */

            /* be kind to dispose manually and not wait for the GC. */
            ctx.close();
        }
    }

    void quantifierExample1() {
        try
        {
            Context ctx = new Context();

            System.out.println("QuantifierExample");
//            Log.append("QuantifierExample");

            Sort[] types = new Sort[3];
            IntExpr[] xs = new IntExpr[3];
            Symbol[] names = new Symbol[3];
            IntExpr[] vars = new IntExpr[3];

            for (int j = 0; j < 3; j++) {
                types[j] = ctx.getIntSort();
                names[j] = ctx.mkSymbol("x_" + Integer.toString(j));
                xs[j] = (IntExpr) ctx.mkConst(names[j], types[j]);
                vars[j] = (IntExpr) ctx.mkBound(2 - j, types[j]); // <-- vars
                // reversed!
            }

            Expr body_vars = ctx.mkAnd(
                    ctx.mkEq(ctx.mkAdd(vars[0], ctx.mkInt(1)), ctx.mkInt(2)),
                    ctx.mkEq(ctx.mkAdd(vars[1], ctx.mkInt(2)),
                            ctx.mkAdd(vars[2], ctx.mkInt(3))));

            Expr body_const = ctx.mkAnd(
                    ctx.mkEq(ctx.mkAdd(xs[0], ctx.mkInt(1)), ctx.mkInt(2)),
                    ctx.mkEq(ctx.mkAdd(xs[1], ctx.mkInt(2)),
                            ctx.mkAdd(xs[2], ctx.mkInt(3))));

            Expr x = ctx.mkForall(types, names, body_vars, 1, null, null,
                    ctx.mkSymbol("Q1"), ctx.mkSymbol("skid1"));
            System.out.println("Quantifier X: " + x.toString());

            Expr y = ctx.mkForall(xs, body_const, 1, null, null,
                    ctx.mkSymbol("Q2"), ctx.mkSymbol("skid2"));
            System.out.println("Quantifier Y: " + y.toString());

        }
        catch (Exception ex)
        {

        }
    }

    Model check(Context ctx, BoolExpr f, Status sat) throws Exception {
        Solver s = ctx.mkSolver();
        s.add(f);
        if (s.check() != sat)
            throw new Exception();
        if (sat == Status.SATISFIABLE)
            return s.getModel();
        else
            return null;
    }
}

• Build the project successfully, but then I get the error.

Connected to the target VM, address: '127.0.0.1:54691', transport: 'socket'

Exception in thread "main" java.lang.UnsatisfiedLinkError: no libz3java in java.library.path

at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1860)

at java.lang.Runtime.loadLibrary0(Runtime.java:870)

at java.lang.System.loadLibrary(System.java:1122)

at com.microsoft.z3.Native.<clinit>(Native.java:14)

at com.microsoft.z3.Context.<init>(Context.java:41)

at solver.z3solver.quantifierExample1(z3solver.java:33)

at solver.z3solver.main(z3solver.java:14)

Disconnected from the target VM, address: '127.0.0.1:54691', transport: 'socket'

• You must understand that Java takes care of the build so using the import com.microsoft.z3.*; command is enough, but when running, you must provide java.library.path to the library of Z3 so it knows where the library is. You can do this by go to Run --> Edit Configurations --> VM options: Add this command: -Djava.library.path="C:\z3-4.8.8-x64-win\bin\". If your path have the last "\", VM still complains as follows:

Exception in thread "main" java.lang.UnsatisfiedLinkError: no libz3java in java.library.path

at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1860)

at java.lang.Runtime.loadLibrary0(Runtime.java:870)

at java.lang.System.loadLibrary(System.java:1122)

at com.microsoft.z3.Native.<clinit>(Native.java:14)

at com.microsoft.z3.Context.<init>(Context.java:41)

at solver.z3solver.quantifierExample1(z3solver.java:33)

at solver.z3solver.main(z3solver.java:14)

Disconnected from the target VM, address: '127.0.0.1:53632', transport: 'socket'

• You must remove the last "\" from the path, VM will understand it. So the last and successful will be: -Djava.library.path="C:\z3-4.8.8-x64-win\bin". However, now you will have the following error.

Exception in thread "main" java.lang.UnsatisfiedLinkError: C:\z3-4.8.8-x64-win\bin\libz3java.dll: Can't find dependent libraries

at java.lang.ClassLoader$NativeLibrary.load(Native Method)

at java.lang.ClassLoader.loadLibrary0(ClassLoader.java:1934)

at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1850)

at java.lang.Runtime.loadLibrary0(Runtime.java:870)

at java.lang.System.loadLibrary(System.java:1122)

at com.microsoft.z3.Native.<clinit>(Native.java:14)

at com.microsoft.z3.Context.<init>(Context.java:41)

at solver.z3solver.quantifierExample1(z3solver.java:33)

at solver.z3solver.main(z3solver.java:14)

Disconnected from the target VM, address: '127.0.0.1:56441', transport: 'socket'

• Now I copy all the folder of Z3 to my libs folder. remove the previous com.microsoft.z3.jar from the libs folder. Add the new one com.microsoft.z3.jar as a library. Now I must edit the Run configurations. so it is: -Djava.library.path="My path\libs\z3-4.8.8-x64-win\bin"

• Now you can run the sample code without problem.

Connected to the target VM, address: '127.0.0.1:58074', transport: 'socket'

QuantifierExample

Quantifier X: (forall ((x_0 Int) (x_1 Int) (x_2 Int))

  (! (and (= (+ x_0 1) 2) (= (+ x_1 2) (+ x_2 3))) :skolemid skid1 :qid Q1))

Quantifier Y: (forall ((x_0 Int) (x_1 Int) (x_2 Int))

  (! (and (= (+ x_0 1) 2) (= (+ x_1 2) (+ x_2 3))) :skolemid skid1 :qid Q1))