z3 - Solver.model() 返回的无用 Var()

Solver.model() 有时会返回一个看似不必要的 Var() 赋值，而我(可能是天真地)期望 Solver.model() 总是为每个变量返回一个具体的值。例如:

#!/usr/bin/python
import z3

x, y = z3.Ints('x y')
a = z3.Array('a', z3.IntSort(), z3.IntSort())
e = z3.Not(z3.Exists([x], z3.And(x != y, a[x] == a[y])))

solver = z3.Solver()
solver.add(e)
print solver.check()
print solver.model()

产生

sat
[k!1 = 0,
 a = [else -> k!5!7(k!6(Var(0)))],
 y = 1,
 k!5 = [else -> k!5!7(k!6(Var(0)))],
 k!5!7 = [1 -> 3, else -> 2],
 k!6 = [1 -> 1, else -> 0]]

这里发生了什么？ Var(0) 的“else”中的 a 是指 a 数组的第 0 个参数，即 a[i] = k!5!7[k!6[i]] 吗？是否有可能从 Z3 中获得 a 的具体令人满意的分配，例如 a = [1 -> 1, else -> 0] ？

最佳答案

这是预期的输出。函数和数组的解释应该被视为函数定义。请记住，断言

z3.Not(z3.Exists([x], z3.And(x != y, a[x] == a[y])))

本质上是一个全称量词。对于无量词问题，Z3 确实会生成您帖子中建议的“具体分配”。然而，这种表现形式不够表达。在消息的末尾，我附上了一个无法使用“具体分配”进行编码的示例。
以下帖子提供了有关如何在 Z3 中对模型进行编码的其他信息。

understanding the z3 model

您可以在 http://rise4fun.com/Z3/tutorial/guide 找到有关 Z3 使用的编码的更多详细信息

这是一个生成无法使用“具体”分配(可在 http://rise4fun.com/Z3Py/eggh 在线获得)进行编码的模型的示例:

a = Array('a', IntSort(), IntSort())
i, j = Ints('i j')
solver = Solver()
x, y = Ints('x y')
solver.add(ForAll([x, y], Implies(x <= y, a[x] <= a[y])))
solver.add(a[i] != a[j])
print solver.check()
print solver.model()

关于z3 - Solver.model() 返回的无用 Var()，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/13771206/