如何按顺序打印 z3 求解器结果 print(s.model())？

Question

假设我有一个包含 10 个变量的列表

v = [Real('v_%s' % (i+1)) for i in range(10)]

我想添加一个像这样的简单约束

s = Solver()
for i in range(10):
    s.add(v[i] == i)
if s.check() == sat:
    print(s.model())

所以一个令人满意的模型是 v_1 = 0, v_2 = 1 .... v_10 = 9。然而 print(s.model()) 的输出是完全无序的，这让我在更大的模型中有很多变量时感到困惑。对于这个例子，我的电脑输出是v_5, v_7, v_4, v_2, v_1, v_3, v_6, v_8, v_9, v_10，但是我想输出这个模型的变量，像v_1, v_2, ..., v_10这样的顺序。谁能告诉我 z3Py 有没有这种功能？谢谢！

Answer 1

您可以将模型变成一个列表，并按照您喜欢的方式对其进行排序：

from z3 import *

v = [Real('v_%s' % (i+1)) for i in range(10)]

s = Solver()
for i in range(10):
    s.add(v[i] == i)
if s.check() == sat:
    m = s.model()
    print (sorted ([(d, m[d]) for d in m], key = lambda x: str(x[0])))

这会打印：

[(v_1, 0), (v_10, 9), (v_2, 1), (v_3, 2), (v_4, 3), (v_5, 4), (v_6, 5), (v_7, 6), (v_8, 7), (v_9, 8)]

请注意，名称按字典顺序排序，因此 v_10 在 v_1 之后和 v_2 之前。如果你希望v_10在最后，你可以根据需要做进一步的处理。

Answer 2

当您使用像 IntVector 这样的向量时，您可以使用 m[v[i]] 调用 i 位置上的元素，其中 m 是模型，v 是向量和 i 是期望的位置：

v = IntVector('v', 10)

for i in range(10):
    s.add(v[i] == i)

s = Solver()
if (s.check()):
    m = s.model()

    for i in range(10):
        print(m[v[i]])

它不会在模型上打印i-元素，而是在原始位置打印正确的元素。

对于你的情况，你可以做同样的事情：

v = [Real('v_%s' % (i+1)) for i in range(10)]

for i in range(10):
    s.add(v[i] == i)

s = Solver()
if (s.check()):
    m = s.model()

    for i in range(10):
        print(m[v[i]])

如何按顺序打印 z3 求解器结果 print(s.model())？

How to print z3 solver results print(s.model()) in order?

python

python-3.x

z3

z3py