3

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)ina的“else”是指数组的第 0 个参数，是什么a意思a[i] = k!5!7[k!6[i]]？是否有可能从 Z3 中获得具体令人满意的任务a，例如a = [1 -> 1, else -> 0]？

4

1 回答 1

3

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

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

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

您可以在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()
于 2012-12-07T22:13:39.943 回答