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])))
This prints:
[(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)]
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.
与恶龙缠斗过久,自身亦成为恶龙;凝视深渊过久,深渊将回以凝视…