我有这个问题,就是访问数组索引的错误。索引应该是一个整数,但它不能工作。我最初尝试使用一个变量,但在本例中,我将其更改为整数,0,只是为了显示它不存在这个问题所在的变量。Cannot subscript a value of type '[LocationStore]' with an index of type '(Int, () -> ())'
那么,有人能解释为什么数组不想要一个int作为索引
我想在Z3py中定义一个二维布尔数组。实际上,我希望使用其他整数变量来访问数组索引,例如,Ax,其中x是一个整数变量,其值由运行时的SMT-solver决定。如果我按如下方式定义二维数组:a=[ Bool("a_%s_%s“% (i,j)) for j in range(5) for i in range(5) ],则在添加约束(如(Ax==True) )时会得到我检查了一下,对于定义为A= z3 (‘A’