获取一个Z3模型名对应的python变量名 [英] Get the corresponding python variable name of a Z3 model name

问题描述

有没有办法得到一个z3模型名对应的python变量名?

Is there a way to get the corresponding python variable name of a z3 model 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)

s.check()

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

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

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

所以我的问题是Z3有没有获取z3模型名对应的python变量名的方法?如果是这样，那么我不需要枚举所有变量名称.因为如果我们有很多变量，这将是一项巨大的工作.我想实现的目标如下:

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

Z3 有那个 corresponding_python_variable_name() 函数吗?提前致谢！

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

推荐答案

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

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

请注意，这将循环尽可能多的不同模型；因此，如果您有许多模型(在您的问题中使用 Real 可能是无限的)，那么这将永远持续下去.(或者直到内存/CPU 等用完为止)

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

这篇关于获取一个Z3模型名对应的python变量名的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！