列表理解项，在z3模型中部分评估

Question

请考虑以下示例：

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()

产生以下结果：

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]

结果似乎正确，但我不明白为什么x_17出现在列表中。

另一个结果：

1
[var = 0]

是否将空列表视为Sum(data1) == 10的有效解决方案？如何明确指定列表必须包含10或20个项目？但是我的主要问题是：为什么提出部分清单作为解决方案？

在此示例中：

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()

程序不会退出循环，没有提出带有部分列表的解决方案。也许And运算符的设计具有类似短路的行为？

Answer 1

第一程序

您的约束是：

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

通过De Morgan's laws，这等效于：

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

请考虑如果求解器将var设置为0会发生什么：两个析取均为真，因此系统可满足要求。因此，x都设置为什么，总和是什么都没有关系。

总而言之，其中var不是100且200是您的问题的模型的任何分配。请注意，z3只会分配“足够”的变量以使您的问题进入sat状态，因此您看不到其他变量。 （但是，如果确实需要它们，可以获取它们的值； z3只是通过不将它们放入模型中来告诉您它们无关紧要。）

第二程序

在您的第二个问题中（将data1重命名为data之后），您的Python程序陷入了无限循环。 Z3实际上几乎立即回答了您的查询，但是您的if条件是：

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

并且z3找到的模型中恰好有10个东西。因此，您一直在z3之外循环播放。也许您打算让if行读取== 10？