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?

alias · Accepted Answer · 2020-06-04T15:57:54.523

2

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?

edited Jun 04 '20 at 15:57

answered Jun 04 '20 at 15:32

alias

28,120
2
23
40

Thank you for your response. My question is stupid. I thought I was doing a sum of unsigned, so if the sum of the first n elements was greater than 10, the following values were not necessary. It was without thinking about the integer overflow. In fact, signed or unsigned, it is mandatory that the model must contain all 10 values. I'm sorry about that. – no_name Jun 04 '20 at 19:24
But, if z3 will only assign "enough" of the variables to get my problem to a sat state, why do I get the first answer? "var = 0" seems sufficient in this case but the model provides many more values. "But it is possible to get their values if you do need them" : I need it. ;) How do you do it? Precisely in this case where I use a list-comprehension? – no_name Jun 04 '20 at 19:25
1

Model generation is "opportunistic." As the solver explores the state space, you will get *enough* assignments to satisfy the constraints. But there's no guarantee that this assignment will be minimal. (In general, the notion of "minimal" such assignment isn't even well defined. There's no "order" in the assignment sets.) So, you'll get the minimum required, and plus perhaps a few others as the solver explored the solution space. – alias Jun 04 '20 at 19:56
1

To get "all" values, see this answer: https://stackoverflow.com/questions/53162290/why-z3py-does-not-provide-all-possible-solutions/53163796#53163796 Essentially, it boils down to calling `model.eval(var, model_completion=True)` for each `var` you're interested in. – alias Jun 04 '20 at 19:58
Thank you very much! that's exactly the answer I was looking for. – no_name Jun 04 '20 at 22:31

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

1 Answers1

First Program

Second program