如何在 python 中声明具有唯一名称的变量？

Question

一个程序收到一个映射 vars，它映射了 pathCons 中变量的名称和类型。现在，我要解决这个path_cons，我设计了下面的parse()函数来尝试实现它。但是，要使 solver 识别 path_cons 中的所有变量，我必须先声明它们。但是他们的名字被记录到一个变量中，那么我该如何实现我的目标呢？

def parse(vars, pathCons):
    for var in list(vars.keys()):
       if vars[var] == "uint":
           ???(should be name of var) = BitVec(var, 256)
       elif vars[x] == "bool":
           ??? = Bool(var)
   solver.add(eval(path_cons))

我想到了一个想法，我为每个变量随机生成一个唯一的名称，然后用path_cons中的新名称替换它们。但同样，生成的名字也是一个值，不能作为变量的名字。

例如，

vars = {"length":"int", "balance":"uint", "day":"uint", "flag":"bool"}
pathcons = "length>9, ULT(day, 10), UGE(balance + day, 100), flag == true"

现在我收到这两个变量，我想求解pathcons。

Answer 1

很难理解您要在此处实现的目标。如果您 post 编码人们可以运行并看到您正在运行遇到的问题，那么 Stack-overflow 的效果最好。

但在我看来，您想创建一堆与您拥有的某些变量概念相对应的 z3 名称。为此，只需创建一个数组并相应地使用它。我会这样做：

from z3 import *

progVars = {"length":"int", "balance":"uint", "day":"uint", "flag":"bool"}

def mkVar(var):
    if progVars[var] == "uint":
        return BitVec(var, 256)
    elif progVars[var] == "bool":
        return Bool(var)
    elif progVars[var] == "int":
        return Int(var)
    else:
        raise Exception("Don't know how to handle %s" % progVars[var])

z3Vars = [{"progVar": v, "z3Var": mkVar(v)} for v in progVars.keys()]

print(z3Vars)

这会打印：

[{'progVar': 'length', 'z3Var': length}, {'progVar': 'balance', 'z3Var': balance}, {'progVar': 'flag', 'z3Var': flag}, {'progVar': 'day', 'z3Var': day}]

注意我们的字典现在如何通过您的“程序键”进行索引，并且对于每个我们在 z3Var 字段中存储创建的 z3 变量。这些将是真正的符号值，您稍后可以使用 z3 进行操作，添加到带有约束的求解器等。

如何在 python 中声明具有唯一名称的变量？

How to declare variables with unique name in python?

python-3.x

z3

solver