Get The Corresponding Python Variable Name Of A Z3 Model Name

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 r

Solution 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 inrange(10)]

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

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

   ifnot m:
       breakprint 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.)