如何解决以可读格式输出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
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。