Z3 Solver Java API: Unexpected behaviour

user_13209041 0
Viewed 109

By adding conditions to the solver, I want to check with "solver.check()", whether there exists a solution or not. Therefore, I created a simple example to find a solution for t1. I know that there is a solution for t1, namely t1 = 0. Nevertheless, the solver has not the status "SATISFIABLE". 

public static void main(String[] args) {
        int h_max = 7;
        HashMap<String, String> cfg = new HashMap<String, String>();
        cfg.put("model", "true");
        Context ctx = new Context(cfg);
        FPSort s = ctx.mkFPSort(5, 20);
        Solver solver = ctx.mkSolver();
        Model model = null;

        // Initialize constants
        RealExpr half = ctx.mkFPToReal(ctx.mkFP(0.5, s));
        RealExpr g = ctx.mkFPToReal(ctx.mkFP(9.81, s));
        RealExpr hmax = ctx.mkInt2Real(ctx.mkInt(h_max));
        RealExpr v = ctx.mkFPToReal(ctx.mkFP((Math.sqrt(2*h_max*9.81)), s));

        // Create query Information
        RealExpr q2 = ctx.mkReal(1);
        RealExpr q2Min = (RealExpr) ctx.mkSub(q2, half);
        RealExpr q2Max = (RealExpr) ctx.mkAdd(q2, half);

        // Initialize constraints 
        RealExpr tmax = ctx.mkFPToReal(ctx.mkFP((Math.sqrt(2*h_max/9.81)), s));
        RealExpr t0 = ctx.mkReal(0);

        // Initialize sampling interval
        RealExpr ts = ctx.mkFPToReal(ctx.mkFP(Math.sqrt(2*h_max/9.81)+0.1, s));

        // Variable t1
        RealExpr t1 = ctx.mkRealConst("t1");

        // 0 <= t1 <= tmax
        BoolExpr c1 = ctx.mkGe(t1, t0);
        BoolExpr c2 = ctx.mkLe(t1,tmax);

        // Elapsed Times
        RealExpr tE = (RealExpr) ctx.mkAdd(ts, t1);

        // Add conditions to solver
        solver.add(c1);
        solver.add(c2);

        // Calculating tE2 % tmax, since tE2 > tmax
        RealExpr quotient = (RealExpr) ctx.mkDiv(tE, tmax);
        IntExpr factor = ctx.mkReal2Int(quotient);
        RealExpr t2 = (RealExpr) ctx.mkSub(tE, ctx.mkMul(factor, tmax));

        // Calculating the observation h2 with t2.
        RealExpr h2 = (RealExpr) ctx.mkSub(ctx.mkMul(v,t2), ctx.mkMul(half, t2, t2, g));

        // Defining constraint q2Min <= h2 < q2Max
        BoolExpr c3 = ctx.mkAnd(ctx.mkGe(h2, q2Min),ctx.mkLt(h2, q2Max));

        solver.add(c3);

        //System.out.println("solver c1: " + solver.check(c1));
        //System.out.println("solver c2: " + solver.check(c2));
        //System.out.println("solver c3: " + solver.check(c3));

        if (solver.check() == Status.SATISFIABLE) {
            model = solver.getModel();
            System.out.println("System is Satisfiable");
        }
        else {
            System.out.println("Unsatisfiable");
        }

    ctx.close();
    }

I discovered some unexpected behaviour. If I try to check conditions before I do "solver.check()", for example

System.out.println("solver c2: " + solver.check(c2));
System.out.println("solver c3: " + solver.check(c3));

it outputs: 

solver c2: UNKNOWN
solver c3: UNKNOWN

and suddenly, the solver's status is "SATISFIABLE". But if I only check one condition beforehand, the status is still "UNSATISFIABLE".

Other than that, if I change from

t1 = ctx.mkRealConst("t1");

to 

t1 = ctx.mkReal(0);

the solver also finds a solution and the solver status is "SATISFIABLE".

Why does the solver have this behaviour and how could I possibly make the solver find a solution? Are there any alternative ways that I could try?

smt z3 solver java
1 Answers

In general, when you write:

solver.check(c1)

you are not asking z3 to check that c1 is satisfiable. What you are asking z3 to do is to check that all the assertions you put in are satisfiable assuming c1 is true. This is called "check under assumptions" and is documented here: https://z3prover.github.io/api/html/classcom_1_1microsoft_1_1z3_1_1_solver.html#a71882930969215081ef020ec8fec45f3

This can be rather confusing at first, but it allows checking satisfiability under assumptions without having to assert those assumptions globally.

Regarding why you get UNKNOWN. You are using floating-point arithmetic, and mixing and matching it with real's. That will create a lot of non-linear constraints, something that z3 doesn't really deal with all that well. Try to keep the logics separated: Don't mix reals with floats if you can. (Ask a separate question if you have questions regarding how to model things.)

Finally, writing t1 = ctx.mkReal(0) is very different than writing t1 = ctx.mkRealConst("t1"). The first one is much simpler to deal with: t1 is just 0. In the second case it's a variable. So, it isn't surprising at all that the former leads to much easier problems to handle for z3. Again, there's no silver bullet but start with not-mixing the logics this way: If you want to work on floating-point, keep everything in that land. If you want to work with real values, keep everything real valued. You'll get much more mileage that way. If you have to mix the two, then you'll most likely see UNKNOWN results.

user_9363100
Related