Z3 Python：订购模型并访问它们的元素

Question

在 Z3 (Python) 中，假设我得到一个具有以下形状的模型：

[c_0 = True, c_3 = False, c_1 = False, c_2 = False]

1. 如何对变量进行排序，以便赋值按字母顺序排列？ [c_0 = True, c_1 = False, c_2 = False, c_3 = False]

2. 如何访问模型的任何元素？我的意思是，如果我这样做：

m = s.model() #equivalent to [c_0 = True, c_3 = False, c_1 = False, c_2 = False]
a = m[0]
print(a)

我得到了c_0，而不是预期的c_0 = True。

为了让这篇文章尽可能简单，我不再添加代码，c 变量只是示例。

我的最终目标是一个方法，给定[c_0 = True, c_3 = False, c_1 = False, c_2 = False]返回一个数组a=[True, False, False, False]，其中a[0]对应c_0的值，a[1]对应c_1的值等

编辑

对于 (1)，我尝试了 sorted(m, key=str.lower)，但出现以下错误：descriptor 'lower' requires a 'str' object but received a 'FuncDeclRef'。这意味着我应该将每个元素转换为 str，这是我不想要的。

我更喜欢 Z3 的“原生”方法，它不会修改变量的类型。

Answer 1

如果您想通过键对模型进行排序，则必须将其转换为不同的数据结构。 （这实际上与 z3 没有太大关系，而是字典在内部是如何完成的。）您尝试的几乎就在那里，您只需要确保同时保留变量和值。这是一个例子：

from z3 import *

a, b = Bools('a b')
s = Solver()
s.add(And(a, Not(b)))
print(s.check())

m = s.model()
nicer = sorted ([(d, m[d]) for d in m], key = lambda x: str(x[0]))
print(nicer)

打印出来：

sat
[(a, True), (b, False)]

请注意，它会保持一切原样，即不会丢失对象属性：

print(type(nicer[0][0]))
print(type(nicer[0][1]))

打印：

<class 'z3.z3.FuncDeclRef'>
<class 'z3.z3.BoolRef'>

对于第二个问题，您可以通过变量本身访问：请注意，模型是字典，因此可以通过变量查找它们。对于上面的程序，你可以说：

print(m[a])
print(m[b])

打印出来：

True
False

获得对列表后，您可以简单地获取值：

print([v for (d, v) in nicer])

打印出来：

[True, False]

现在你有了一个配对列表，你可以随意用它做任何事情。

旁注：我理解在您的问题中使用“最少”代码量的动机；这很诱人，我已经在自己之前做到了！但最好提供一个最低限度完整的示例，即本论坛的读者可以按原样运行的示例。这样可以确保他们不必猜测您可能在做什么其他事情，或导致误解。请尽可能发布一个最完整的示例来展示您所面临的问题。此外，如果您每篇文章只问一个问题，stack-overflow 效果最好；否则细节会变得模糊不清。最好的办法是用一个最完整的例子提出一个具体的问题，尽管我知道这可能并不总是可能的。谢谢！