Get the corresponding python variable name of a Z3

问题:

Is there a way to get the corresponding python variable name of a z3 model name?

Suppose I have the following code:

from z3 import *

s = Solver()

a = [Real('a_%s' % k) for k in range(10)]

for i in range(10):
    s.add(a[i] > 10)

s.check()

m = s.model()
for d in m:
    print(d, m[d])

Here the d in m are a_0, a_1, a_2,..., a_9, and all of their values are 11. I'm trying to set up some constraints which make the variables don't equal to the previous checking result, like the following:

s.add(a[0] != m['a_0']
...
s.add(a[9] != m['a_9']

Therefore my question is that does Z3 has a method to get the corresponding python variable name of a z3 model name? If so, then I don't need to enumerate all the variables names. Because this will be a huge work if we have many variables. What I want to achieve can be the following:

m = s.model()
for d in m:
    s.add(corresponding_python_variabl_name(d) != m[d])

Does Z3 have that corresponding_python_variable_name() function? Thanks in advance!

回答1:

Looks like you're trying to generate all possible models?

If that's the case, use the following template:

from z3 import *

s = Solver()

a = [Real('a_%s' % k) for k in range(10)]

for i in range(10):
    s.add(a[i] > 10)

while s.check() == sat:
   m = s.model()

   if not m:
       break

   print m

   s.add(Not(And([v() == m[v] for v in m])))

Note that this will loop as many different models as there are; so if you have many models (potentially infinite with Reals as in your problem), then this'll go on forever. (Or till you run out of memory/CPU etc.)