Z3PY converting Ints to Python int

Question

Is there a way to convert the Z3PY datatypes to native Python datatypes?

When my formula is solved by Z3, I can print it out by calling the model()-function. But how do I save the model output as ordinary ints in variables? So I can use them.

Can I convert them to ordinary ints so I can use them in the rest of my Python code in my program?

My whole purpose of using the solver is to take the result as an input to another Python program. So I need it to be able to process it.

Answer 1

Suppose your variable declared was x:

x = z3.Int("x")

You would get it as a Python int like this:

model[x].as_long()

z3 models are also iterable. Retrieving all parameters in a list comprehension:

[model[v] for v in model]