获取一个Z3型号名称对应的python变量名

Get the corresponding python variable name of a Z3 model name

有没有办法获取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中的da_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()功能吗?提前致谢!

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

如果是这种情况,请使用以下模板:

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 可能是无限的),那么这将永远持续下去。 (或者直到 memory/CPU 等 运行)