如何在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

很难理解您在这里想要实现的目标。如果您发布人们可以运行的代码并查看您遇到的问题，则 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}]

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