列表理解的项目，在 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 只会分配 "enough" 个变量以使您的问题进入 sat 状态，因此您看不到其他变量。（但如果您确实需要它们，则可以获得它们的值；z3 只是告诉您它们并不重要，因为不将它们放入模型中。）

第二个节目

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

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

而 z3 找到的模型正好有 10 个东西。所以你一直在 z3 之外循环。也许您打算将 if 行读作 == 10?

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

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

python

list-comprehension

z3

z3py

第一个节目

第二个节目