Items of a list-comprehension, partially evaluated in z3 model

Question

Consider the following example :

from z3 import *

data1 = [BitVec("x_{}".format(i), 8) for i in range(10)]
data2 = [BitVec("x_{}".format(i), 8) for i in range(20)]
var = BitVec("var", 16)

s = Solver()
s.add(Not(Or(
    And(var == 100, Sum(data1) == 10),
    And(var == 200, Sum(data2) == 10))))

while True:
    s.push()
    if s.check() == sat:
        if len(s.model()) != 11 and len(s.model()) != 21:
            print(len(s.model()))
            print(s.model())
            break
    s.pop()

produce the following result :

12
[x_2 = 252,
 x_9 = 248,
 x_1 = 255,
 x_3 = 96,
 x_5 = 192,
 x_4 = 223,
 x_17 = 0,
 var = 0,
 x_0 = 0,
 x_6 = 252,
 x_7 = 254,
 x_8 = 248]

The result seems correct but I don't understand why x_17 appears in the list.

Another result :

1
[var = 0]

Is an empty list considered to be a valid solution of Sum(data1) == 10 ? How does it explicitly specify that the list must have 10 or 20 items? But my main question is: why is a partial list being proposed as a solution?

With this example :

from z3 import *
data = [BitVec("x_{}".format(i), 8) for i in range(10)]
s = Solver()
s.add(Sum(data1) == 10)
while True:
    s.push()
    if s.check() == sat:
        if len(s.model()) != 10:
            print(len(s.model()))
            print(s.model())
            break
    s.pop()

The program does not come out of the loop, no solution proposed with a partial list. Perhaps the And operator is designed with short-circuit-like behaviour?

Answer 1

First Program

Your constraint is:

s.add(Not(Or(
    And(var == 100, Sum(data1) == 10),
    And(var == 200, Sum(data2) == 10))))

By De Morgan's laws, this is equivalent to:

s.add(Or(var != 100, Sum(data1) != 10))
s.add(Or(var != 200, Sum(data2) != 10))

Consider what happens if the solver sets var to be 0: Both disjunctions are true and thus the system is satisfiable. So, it doesn't matter what all the x's are set to, nor what the sums are.

To sum up, any assignment where var is something other than 100 and 200 is a model for your problem. Note that z3 will only assign "enough" of the variables to get your problem to a sat state, so you don't see the other variables. (But it is possible to get their values if you do need them; z3 is just telling you that they do not matter by not putting them into the model.)

Second program

In your second problem (after renaming data1 to data) it is your Python program that goes into an infinite loop. Z3 actually answers your query almost instantly, but your if condition is:

if len(s.model()) != 10:

and the model found by z3 has exactly 10 things in it. So you keep looping outside of z3. Perhaps you intended that if line to read == 10?