python - 如何按顺序打印 z3 求解器结果 print(s.model())?
问题描述
假设我有一个包含 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 有没有这种功能?谢谢!
解决方案
您可以将模型转换为列表并以您喜欢的任何方式对其进行排序:
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
afterv_1
和 before v_2
。如果你想v_10
在最后,你可以做进一步的处理,因为它适合你的需要。
推荐阅读
- python - 如何将属性列表应用于 Python 中的对象
- facebook - 如何显示来自任何 Facebook 页面的帖子(当我不是此页面的所有者时)
- java - 仅将外部字段用于一种方法
- azure - 天蓝色突触。高效地将数据插入哈希分布式表中
- resx - InvalidOperationException:资源类型“XXXX.Localize.Resource”没有名为“EnterEmailAddress”的可访问静态属性
- python - 建立模型关系时,相关字段查找无效
- javascript - 我无法在我的 html 页面上获得幻灯片放映图像
- wordpress - 使用超过 7 个 meta_queries 时,WP Query 速度极慢
- wpf - WPF Unknown 属性不指向依赖对象
- json - 在本地使用 spark/scala 查询数据框时,如何更改列中值的输出?