Z3 Java why do I need a tactic for this?

Question

I have the following Java program that solves (not (and (= b false) (= d false))). It does not work with an out-of-the-box context/solver. It looks like the D const gets dropped from the model when I try model.getConstInterp(d).

If I run this with andThen(mkTactic("simplify"), mkTactic("sat")) it works OK. If I try running this in an SMT script from the z3 binary, it works fine without any special tactics.

What am I missing? I assume it's a context option.

Yes, I realize that the predicate (not (and (= b false) (= d false))) could be written much more simply, but this is auto-generated by some other code that is not so easy to track down and change. This statement is actually part of a much larger generated program.

  @Test
  void testQuestion() {
    var ctx = new Context();
    var b = ctx.mkBoolConst("B");
    var d = ctx.mkBoolConst("D");
    var solver = ctx.mkSolver();

    var p4 = ctx.mkNot(
        ctx.mkAnd(
            ctx.mkEq(b, ctx.mkFalse()),
            ctx.mkEq(d, ctx.mkFalse())));
    solver.assertAndTrack(p4, ctx.mkBoolConst("P4"));

    var result = solver.check();
    assertEquals(Status.SATISFIABLE, result);
    var model = solver.getModel();
    assertEquals("true", model.getConstInterp(b).toString());

    // this throws NPE as the cgid_enable declaration is missing
    assertEquals("false", model.getConstInterp(d).toString());
  }

Answer 1

By default z3 will only assign values to variables in the model if they are needed. Unfortunately, what "needed" means is up-to z3; if the underlying engine already showed a problem to be sat without assigning to some of the variables, then they'll remain unassigned. And which variables will go unassigned can change from run-to-run/version-to-version.

In your case, as soon as the solver assigns b to be true it notices that its work is done; since the assignment to d no longer matters. (By symmetry, it could've done it the other way around as well, of course.) So, it's left unassigned, causing your NPE later on.

The solution is to always ask for completion, using the eval function. Here's your code, coded without using the test-framework, but using eval instead, to illustrate the issue:

import com.microsoft.z3.*;

class JavaZ3Example {
   public static void main(String [] args) {
         var ctx = new Context();
         var b = ctx.mkBoolConst("B");
         var d = ctx.mkBoolConst("D");
         var solver = ctx.mkSolver();

         var p4 = ctx.mkNot(
             ctx.mkAnd(
                 ctx.mkEq(b, ctx.mkFalse()),
                 ctx.mkEq(d, ctx.mkFalse())));
         solver.assertAndTrack(p4, ctx.mkBoolConst("P4"));

         var result = solver.check();
         System.out.println(result);
         var model = solver.getModel();
         System.out.println(model.eval(b, false).toString());
         System.out.println(model.eval(d, false).toString());
   };
};

If you run the above, you'll get:

SATISFIABLE
true
D

And that's the tell-tale sign there in the last line where the solver decided not to assign a value to the variable D. i.e., it left it unassigned; which, in this context, prints simply as the name of the variable.

You can simply pass true to the second argument of eval to change this behavior. Passing true as the second argument tells z3 to make sure all variables are assigned a value, regardless whether that assignment is needed or not. That is, change the last two lines to:

         System.out.println(model.eval(b, true).toString());
         System.out.println(model.eval(d, true).toString());

and when you run the new program, you'll get:

SATISFIABLE
true
false

The last line could've come out as true as well, of course, but that information is lost when you force eval to assign a value to every variable.

Long story short, for these sorts of problems where you need every model value to have an assignment, do not use getConstInterp. Instead, use eval, passing true for the second parameter.