i have this list which is a z3 model:

list = [x_2 = 0, x_1 = 1, x_3 = 27, x_11 = 1, x_18 = 4, x_17 = 6, x_26 = 4, x_12 = 4, x_7 = 2, x_22 = 8, x_23 = 27, x_21 = 1, x_28 = 4,x_6 = 1, x_16 = 4, x_27 = 9, x_13 = 27, x_8 = 27, x_29 = 1, x_24 = 19, x_19 = 2, x_14 = 13, x_9 = 20, x_4 = 23, x_25 = 5, x_20 = 4, x_15 = 3, x_10 = 2,x_5 = 1, x_0 = 0]

i have tried to use:

solved = solver.model()

list = sorted ([(i, solved[i]) for i in solved], key = lambda x: str(x[0]))

to sort the list so x_0 is first, x_1 is second, x_2 is next .....etc, but i get the result:

[(x_0, 0), (x_1, 1), (x_10, 2), (x_11, 1), (x_12, 4), (x_13, 27), (x_14, 13), (x_15, 3), (x_16, 4), (x_17, 6), (x_18, 4), (x_19, 2), (x_2, 0), (x_20, 4), (x_21, 1), (x_22, 8), (x_23, 27), (x_24, 19), (x_25, 5), (x_26, 4), (x_27, 9), (x_28, 4), (x_29, 1), (x_3, 27), (x_4, 23), (x_5, 1), (x_6, 1), (x_7, 2), (x_8, 27), (x_9, 20)]

where it has all the ones with 1's at the start first but its still quite out of order but i feel like this is close

CodePudding user response：

just wanted to ask.. is this working in your code.? Please let me know.

list = sorted ([(i, solved[i]) for i in solved], key = lambda x: int(str(x[0])[2:]))

My approach:- as all contains (x_) slicing this part (x_)-> [2:] and than sorting on the basis of integer. Just don't know is it working or not.