In Z3 (Python), imagine I get a model with the following shape:

[c_0 = True, c_3 = False, c_1 = False, c_2 = False]

1. How can I order the variables, so that the assignment is alphabetically ordered? [c_0 = True, c_1 = False, c_2 = False, c_3 = False]

2. How can I access any element of the model? I mean, if I do:

m = s.model() #equivalent to [c_0 = True, c_3 = False, c_1 = False, c_2 = False]
a = m[0]
print(a)

I get c_0, and not the expected c_0 = True.

I put no more code in order to keep this post as simple as possible, the c variables are just examples.

My final objective is a method that, given [c_0 = True, c_3 = False, c_1 = False, c_2 = False] returns an array a=[True, False, False, False], where a[0] corresponds to the value of c_0, a[1] corresponds to the value of c_1, etc.

EDIT

For (1), I tried sorted(m, key=str.lower), but I get the following error: descriptor 'lower' requires a 'str' object but received a 'FuncDeclRef'. This means I should convert each element to str, which I do not want.

I prefer a 'native' method of Z3 that yields no modification in the type of the variables.

CodePudding user response：

If you want to sort the model by its keys, you have to convert it to a different data-structure. (This really doesn't have much to do with z3, but rather how dictionaries are internally done.) What you tried is almost there, you just need to make sure to keep both the variable and the value. Here's an example:

from z3 import *

a, b = Bools('a b')
s = Solver()
s.add(And(a, Not(b)))
print(s.check())

m = s.model()
nicer = sorted ([(d, m[d]) for d in m], key = lambda x: str(x[0]))
print(nicer)

This prints:

sat
[(a, True), (b, False)]

Note that it keeps everything as is, i.e., you don't lose the object properties:

print(type(nicer[0][0]))
print(type(nicer[0][1]))

prints:

<class 'z3.z3.FuncDeclRef'>
<class 'z3.z3.BoolRef'>

For your second question, you can access by the variable itself: Notice that models are dictionaries, so they can be looked up by the variables. For the program above, you can say:

print(m[a])
print(m[b])

This prints:

True
False

Once you have the list of pairs, you can simply get the values:

print([v for (d, v) in nicer])

This prints:

[True, False]

Now that you have a list of pairs, you can do arbitrary things with it as you please.

Side note: I understand the motivation behind putting "minimum" amount of code in your questions; it's tempting and I've done it before myself! But it's always best to present a minimum-complete example, i.e., something the readers of this forum can run as is. This makes sure that they don't have to guess what other things you might be doing, or lead to misunderstandings. As much as possible, please post a minimal-complete example demonstrating the problem you're facing. Also, stack-overflow works the best if you ask just one question per post; otherwise details get murky. The best is to have one specific question with a minimal-complete example, though I understand this may not always be possible. Thanks!