访问 z3 中空序列的元素时出现奇怪的行为

Question

我在使用 z3py 解决一些约束时发现了奇怪的效果。这是代码：

from z3 import *

# Custom tuple
IntPair, mkIntPair, (first, second) = TupleSort("IntPair", [IntSort(), IntSort()])

s = Solver()

iseq = Const('iseq', SeqSort(IntPair))
p = mkIntPair(Int('a'), Int('b'))

# Some constraints
s.add(And(first(p) > 0, second(p) > 0))
s.add(Length(iseq) == 0)
s.add(first(iseq[0]) >= first(p))

if s.check() == sat:
    print(s.model())

输出为：

[b = 1,
 iseq = Empty(Seq(IntPair)),
 a = 1,
 seq.nth_u = [else -> IntPair(1, 2)]]

如您所见，由于 Length(iseq) == 0 约束，iseq 在 z3 模型中为空。但是这里如何满足约束 first(iseq[0]) >= first(p) 呢？我们如何访问空序列中的第 0 个元素？以及如何修改此代码以使其由于诸如序列超出范围之类的原因而无法满足？

谢谢！

Answer 1

这是设计使然。

请注意，序列逻辑尚未由 SMTLib 形式化，z3 中的实现基于 https://smt2012.loria.fr/paper11.pdf

在那篇论文的第 2.2.1 节中，它指出：

Observe that the value of (seq-head seq-empty) is undetermined. Similarly for seq-tail, seq-first and seq-last. Their meaning is under-specified. Thus, the theory Seq admits all interpretations that satisfy the free monoid properties and the axioms above.

也就是说，当你取一个空序列的头部，或者长度最多为i的序列的第i个元素时，z3可以自由地赋值，对于任何 i.

你可能会问为什么会这样。简短的回答是 SMTLib 本质上是一个总函数的逻辑，即所有项要么是值，要么可以简化为一个值。它不支持所谓的“部分函数”，即 not 根据类型在其整个域上定义的函数。序列访问恰好是这些功能之一。另一个典型的例子是除以 0：在实数上，除以 0 是未指定的，即求解器可以自由分配它想要的任何值。（请参阅“注释”部分下的 https://smtlib.cs.uiowa.edu/theories-Reals.shtml。）

如果您检查 z3 给您的模型，您可以看到以下证据：

seq.nth_u = [else -> IntPair(1, 2)]]

上面的意思是当你访问任何超出范围的元素时，z3 将分配对 (1,2)。对于不同的问题，z3 当然可以选择不同的解释，以确保满足所有其他约束。

如果您希望您的查询是 unsat，那么您在建模时必须小心。也就是说，如果您正在访问任何序列的第 i 个元素，您还必须断言该序列至少有 i+1 个元素。那是，如果添加约束：

s.add(first(iseq[0]) >= first(p))

那么你在道德上还需要添加：

s.add(Length(iseq) > 0)

您可以手动执行此操作，或者您的编程环境可以在幕后为您执行此操作。 Python 绑定将这部分留给程序员：虽然这是设计 API 的合理选择，但它不一定是唯一的选择。长话短说，如果你在上面添加第二个约束，z3 会出于明显的原因告诉你 unsat，并且如你所愿。

请注意，添加您自己的自动为您执行此操作的索引运算符并不是一件非常困难的练习。您可以定义：

def access(solver, seq, idx):
    solver.add(Length(seq) > idx)
    return seq[idx]

然后：

s.add(first(access(s, iseq, 0)) >= first(p))

这也会产生 unsat，在幕后为您处理基数要求，您不必每次都担心。

访问 z3 中空序列的元素时出现奇怪的行为

Strange behavior while accessing elements of empty sequences in z3

z3

z3py