Z3 的这个输出是什么意思？

Question

使用这个简单的代码：

from z3 import *
a, b, c, d =  Ints('a b c d')
s = Solver()
s.add(a>0)
s.add(b>1)
s.add(c>0)
s.add(d>0)
s.add(a*b - c*d< 20)
s.add(d/a+b/d > 2)
s.add((a*c)/(b*d) > 3)
s.check()
s.model()

这给了我：

[d = 8,
 a = 4,
 c = 64,
 b = 8,
 div0 = [(8, 4) -> 2, (256, 64) -> 4, else -> 1],
 mod0 = [else -> 0]]

这是版本 4.8.12。

div0 和 mod0 行是什么意思？

Answer 1

请注意，在您的程序中直接调用 z3 不会为我生成此输出。我得到：

[b = 2, a = 1, c = 9, d = 1]

也许您正在向 z3 传递一些额外的参数来改变行为？

尽管如此，mod0 和 div0 告诉你的是 z3 在构建模型时如何选择定义除以 0。例如：

div0 = [(8, 4) -> 2, (256, 64) -> 4, else -> 1],

意味着 z3 依赖于 8/4=2、256/64=4 和所有其他除法结果 1 的事实；不管参数如何。您可能会觉得这很奇怪，但它绕过了为整数除以 0 赋予意义的古老问题。在 SMTLib 中，此值保持未定义状态，这意味着求解器可以自由选择它想要的任何值，它会告诉您它为此目的选择了 1。当然，对于你的问题，完全没有关系，因为它找到的模型没有利用这个事实。

通常，您可以忽略 div0/mod0 分配，除非 z3 为您提供了一个实际使用 0 除法的模型。（也就是说，对于你的程序，你可以忽略它。）这是一个你不能的例子：

from z3 import *
a = Int('a')
s = Solver()
s.add(a > 2)
s.add(a / 0 == 5)
print(s.check())
print(s.model())

这个程序打印：

sat
[a = 3]

原因是因为规格不足，z3 可以自由选择 3 / 0 成为 5。这在 http://smtlib.cs.uiowa.edu/theories-Reals.shtml:

中有解释

Since in SMT-LIB logic all function symbols are interpreted as total
functions, terms of the form (/ t 0) are meaningful in every
instance of Reals. However, the declaration imposes no constraints
on their value. This means in particular that

for every instance theory T and

for every value v (as defined in the :values attribute) and closed term t of sort Real, there is a model of T that satisfies (= v (/ t 0)).

（此文本大约 Real 秒，但它也适用于 Int 秒。）

长话短说：如果你得到一个模型，它用 division/modulus 做一些时髦的事 0，那么你需要注意 z3 如何选择定义 div0 和 mod0在模型中。否则，您可以忽略这些作业。

Z3 的这个输出是什么意思？

What does this output from Z3 mean?

python

z3