获取一个Z3模型名对应的python变量名答案

【问题标题】：Get the corresponding python variable name of a Z3 model name获取一个Z3模型名对应的python变量名
【发布时间】：2019-01-09 17:58:47
【问题描述】：

有没有办法获取一个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()这个功能吗？提前致谢！

【问题讨论】：

标签： python z3 smt z3py

【解决方案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])))

请注意，这将循环尽可能多的不同模型；所以如果你有很多模型（Reals 在你的问题中可能是无限的），那么这将永远持续下去。（或者直到你用完内存/CPU等）

【讨论】：