获取Z3模型名称的相应python变量名

Question

有没有办法获得z3模型名对应的python变量名？

假设我有以下代码：

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])

在这里，m中的d是a_0, a_1, a_2,..., a_9，它们的所有值都是11。我正在尝试设置一些约束，使变量与之前的检查结果不相等，如下所示：

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

因此，我的问题是，Z3是否有方法来获取z3模型名称的相应python变量名？如果是这样的话，我就不需要枚举所有的变量名。因为如果我们有很多变量，这将是一项巨大的工作。我想要实现的目标可以是：

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

Z3有corresponding_python_variable_name()功能吗？提前感谢！

Answer 1

看起来你正在尝试生成所有可能的模型？

如果是这种情况，请使用以下模板：

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])))

请注意，这将循环尽可能多的不同模型；因此，如果您有许多模型(使用Real可能是无限的，就像您的问题一样)，那么这将永远持续下去。(或直到内存/CPU耗尽等)