0

我正在使用 python 和 z3py 模块编写一些程序。
我要做的是以下内容：我从位于其他文件中的函数中提取 if 或 while 语句的约束。此外，我提取语句中使用的变量及其类型。
由于我不想手动将约束解析为 z3py 友好的形式，因此我尝试使用评估来为我执行此操作。因此我使用了以下页面的提示：Z3 with string expressions
现在问题是：我不知道约束中的变量是如何调用的。但似乎我必须将每个变量的句柄命名为实际变量。否则评估不会找到它。我的代码如下所示： 

solver = Solver()
# Look up the constraint:
branch = bd.getBranchNum(0)
constr = branch.code
# Create handle for each variable, depending on its type:
for k in mapper.getVariables():
    var = mapper.getVariables()[k]
    if k in constr:
        if var.type == "intNum":
            Int(k)
        else:
            Real(k)
# Evaluate constraint, insert the result and solve it:
f = eval(constr)
solver.insert(f)
solve(f)

如您所见，我将变量和约束保存在类中。执行此代码时，我收到以下错误：

NameError: name 'real_x' is not defined

如果我不使用对变量的循环，而是使用以下代码，则一切正常：

solver = Solver()
branch = bd.getBranchNum(0)
constr = branch.code
print(constr)
real_x = Real('real_x')
int_y = Int('int_y')
f = eval(constr)
print(f)
solver.insert(f)
solve(f)

问题是：我不知道这些变量被称为“real_x”还是“int_y”。此外，我不知道使用了多少变量，这意味着我必须使用一些动态的东西，比如循环。

现在我的问题是：有没有办法解决这个问题？我该怎么做才能告诉 python 句柄已经存在，但名称不同？还是我的方法完全错误，我必须做一些完全不同的事情？

4

1 回答 1

1

这种事情几乎总是一个坏主意（有关更多详细信息，请参阅为什么 eval/exec 不好），但“几乎总是”不是“总是”，而且看起来您正在使用专门设计的库以这种方式使用，在这种情况下，您会发现其中一个例外。

乍一看，您似乎还遇到了将数据排除在变量名称之外的罕见例外情况之一（另请参阅为什么您不想动态创建变量）。但你没有。

您需要这些变量real_x存在的唯一原因是eval可以看到它们，对吗？但是该eval函数已经知道如何在字典中而不是在全局命名空间中查找变量。看起来你得到的mapper.getVariables()是一本字典。

所以，跳过整个凌乱的循环，然后这样做：

variables = mapper.getVariables()
f = eval(constr, globals=variables)

（在早期版本的 Python 中，globals是一个仅位置参数，所以globals=如果你得到一个错误，就删除它。）

正如文档所解释的，这使eval函数可以访问您的实际变量以及mapper想要生成的变量，并且它可以做各种不安全的事情。如果您想防止不安全的事情发生，请执行以下操作：

variables = dict(mapper.getVariables())
variables['__builtins__'] = {}
f = eval(constr, globals=variables)
于 2014-07-23T19:26:37.127 回答