Search code examples
pythonz3z3py

How do I arrange the values in the model generated by Z3 in an ascending order?

I am using Z3 to generate an optimized schedule. After checking for satisfiability, I generate the model and store it into a text file. But, I observed that Z3 doesn't really arrange the values in the model in any order. Is there a way to make Z3 arrange them in an ascending order?

This is one of the variable values that it has generated.

enter image description here

Is there a way to make this ascending?

Solution

  • (Essentially repeating the answer from: How to print z3 solver results print(s.model()) in order?)

    You can turn the model into a list and sort it in any way you like. Here's an example:

    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.

    In your case, looks like car is either an array-value, or an uninterpreted function. For that specific case, you'll have to query the indices you're interested in separately and collect them in a data-structure of your own to display them in the order you like. Long story short, z3 will give you the values, but how you "present" them is up to you. (If you get stuck, please post what you've tried with an example that others can replicate to help you further.)