如何按顺序打印 z3 求解器结果 print(s.model())? [英] How to print z3 solver results print(s.model()) in order?
问题描述
假设我有一个包含 10 个变量的列表
Suppose I have a list of 10 variables
v = [Real('v_%s' % (i+1)) for i in range(10)]
我想添加一个像这样的简单约束
and I want to add a simple constraint like this
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 有没有这种功能?谢谢!
So a satisfying model is v_1 = 0, v_2 = 1 .... v_10 = 9
. However the output of print(s.model())
is totoally unordered which makes me confused when I have lots of variables in a bigger model. For this example, the output of my computer is v_5, v_7, v_4, v_2, v_1, v_3, v_6, v_8, v_9, v_10
, but I want to ouput the variables of this model in order like v_1, v_2, ..., v_10
. Can anyone tell me does z3Py have this kind of function or not? Thanks!
推荐答案
您可以将模型转换为列表并按您喜欢的任何方式对其进行排序:
You can turn the model into a list and sort it in any way you like:
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
在 v_1
之后,v_2
之前.如果您希望 v_10
出现在最后,您可以根据需要进行进一步处理.
Note that the names are sorted lexicographically, hence v_10
comes after v_1
and before v_2
. If you want v_10
to come at the end, you can do further processing as it fits your needs.
这篇关于如何按顺序打印 z3 求解器结果 print(s.model())?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!