以可读格式输出z3模型输出

问题描述

我问了this问题，关于如何将变量分配给集合，但是我一直在努力理解如何以可读的格式输出s.model()结果。

虽然我可能能够解释以下内容

[A = Lambda(k!0,Or(k!0 == 1,k!0 == 4)),b = 5,a = 1,d = 4,sizeB = 2,c = 3,sizeA = 2,B = Lambda(k!0,Or(k!0 == 3,k!0 == 5)),Ext = [else -> 5]]

用户对此进行解释是不合理的。我想以易于读取/使用的格式（例如{A: [a,d],B: [b,c]}）获取输出。我该怎么办？

解决方法

当然可以。您可以通过编程方式提取模型并以任意方式显示它。对于您提到的程序，只需在r = s.check()行之后的末尾添加以下内容：

if r != sat:
    print("Solver said: %s" % r)
else:
    m = s.model()
    print("A = %s" % [e for e in allElems if m.evaluate(m[A][e])])
    print("B = %s" % [e for e in allElems if m.evaluate(m[B][e])])

有了这个添加，当我运行该程序时，它会打印：

A = [a,d]
B = [b,c]

我相信这就是您要寻找的东西。

很显然，您可以提取这些值，对其进行操作，甚至可以根据找到的模型声明新的约束，并进行更多查询。该API非常灵活，如果您想进一步编程，我建议您通读https://ericpony.github.io/z3py-tutorial/guide-examples.htm

output output python z3 z3py