python - Z3 Python : ordering models and accessing their elements

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' 需要一个 'str' 对象但收到了'FuncDeclRef'。这意味着我应该将每个元素转换为 str，这是我不想要的。

我更喜欢 Z3 的“ native ”方法，它不会对变量类型进行任何修改。

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]

现在您已经有了一个配对列表，您可以随心所欲地用它做任意事情。

旁注:我理解在您的问题中放入“最小”数量的代码背后的动机；这很诱人，我自己也做过!但最好提供一个最小完整的示例，即本论坛的读者可以按原样运行的示例。这可以确保他们不必猜测您可能正在做的其他事情，或导致误解。请尽可能发布一个最小完整的示例来演示您所面临的问题。另外，如果你每篇文章只问一个问题，堆栈溢出效果最好；否则细节会变得模糊。最好的办法是用一个最小完整的例子来提出一个具体问题，尽管我知道这并不总是可能的。谢谢!