我想在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’,IntSort(),IntSort
如何缩短这段代码?我想用If缩短循环中的代码。我试着做类似于这个Me.Controls("x" & t) = 0的事情,但是它返回了一个语法错误。我不知道我能做什么。请帮帮忙。Dim x1 As Byte = 0Dim x30 As Byte = 0
If x = t And x1 = 0 ThenEnd If.........