Too many possible configurations in z3 using scala^z3

Question

This is mainly a logic problem I guess...

I use this smtlib formula:

(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(declare-fun d () Bool)
(assert (xor (and a (xor b c)) d))

Which is a term of this structure(in my opinion, at least):

    XOR
    | |
  AND d
  | |
  a XOR
    | |
    b c

My guess: The resultSet would look like this:

{ab, ac, d}

But its this using scala^z3 ctx.checkAndGetAllModels():

{ab, d, ac, ad, abcd}

Why is ad and abcd in there? Is it possible to get only the results I would expect?

Answer 1

Using Scala (without Z3) to show that there are, in fact, more solutions to the constraint:

val tf = Seq(true, false)
val allValid =
  for(a <- tf; b <- tf; c <- tf; d <- tf; 
      if((a && (b ^ c)) ^ d)) yield (
    (if(a) "a" else "") + (if(b) "b" else "") +
    (if(c) "c" else "") + (if(d) "d" else ""))

allValid.mkString("{ ", ", ", " }")

Prints:

{ abcd, ab, ac, ad, bcd, bd, cd, d }

So unless I'm missing something, the question is, why does it not find all solutions? Now here is the answer to that one. (Spoiler alert: "getAllModels" doesn't really get all models.) First, let's reproduce what you observed:

import z3.scala._
val ctx = new Z3Context("MODEL" -> true)
val a = ctx.mkFreshConst("a", ctx.mkBoolSort)
val b = ctx.mkFreshConst("b", ctx.mkBoolSort)
val c = ctx.mkFreshConst("c", ctx.mkBoolSort)
val d = ctx.mkFreshConst("d", ctx.mkBoolSort)
val cstr0 = ctx.mkXor(b, c)
val cstr1 = ctx.mkAnd(a, cstr0)
val cstr2 = ctx.mkXor(cstr1, d)
ctx.assertCnstr(cstr2)

Now, if I run: ctx.checkAndGetAllModels.foreach(println(_)), I get:

d!3 -> false
a!0 -> true
c!2 -> false
b!1 -> true

d!3 -> true    // this model is problematic
a!0 -> false

d!3 -> false
a!0 -> true
c!2 -> true
b!1 -> false

d!3 -> true
a!0 -> true
c!2 -> false
b!1 -> false

d!3 -> true
a!0 -> true
c!2 -> true
b!1 -> true

Now, the problem is that the second model is an incomplete model. Z3 can return it, because whatever the values for b and c are, the constraint is satisfied (b and c are don't-care variables). The current implementation of checkAndGetAllModels simply negates the model to prevent repetition; in this case, it will ask for another model such that (not (and d (not a))) holds. This will prevent all other models with this two values from being returned. In a sense, the incomplete model actually represents four valid, completed, models.

By the way, what happens if you use the DSL of ScalaZ3 with the findAll function is that all models will be completed with default values when they are incomplete (and before they are used to compute the next one). In the context of the DSL we can do this, because we know the set of variables that appear in the formula. In this case, it's harder to guess how the model should be completed. One option would be for ScalaZ3 to remember which variables were used. A better solution would be for Z3 to have an option to always return values for don't-care variables, or perhaps simply to list all don't-care variables in a model.