From other questions, I know how to convert a 1-d list to an array. The function “Store” inside can finish this. However, I would like to get a general method to do this job.

Here’s an example to explain my question:

i, j = Ints('i j')
VG = [[0, 0, 0], [0, 0, 0], [0, 0, 0], [0, 0, 0], [0, 0, 0], [0, 0, 0], [0, 0, 0], [0, 0, 0], [0, 0, 0]]
A = Array('A',IntSort(),ArraySort(IntSort(), IntSort()))

I need to make the array A equal the list VG, because I will add some constraints like this:

s = Solver()
s.add(FORALL([i,j],Implies(And(i>=0, i<9, j>=0, j<3), A[i][j]>=0)))

If I use the list L to do this:
s.add(FORALL([i,j],Implies(And(i>=0, i<9, j>=0, j<3), VG[i][j]>=0)))
z3 reported below error messages:

s.add(ForAll([i,j],Implies(And(i>=0, i<9, j>=0, j<3), VG[i][j]>=0)))
                                                          ~~^^^
TypeError: list indices must be integers or slices, not ArithRef

I searched for information about this error message on Stack Overflow, like this Error with quantifier in Z3Py, so I want to use this method to solve my question. But when the list have more dimensions, this method doesn’t seems to work.

I don’t know how many dimensions the list has, and I don’t know the size of each dimension in the array. All I have is just a list, like the ‘VG’ above, I need to get a result for some constraints like ‘VG[i][j]>0’, so how to solve it? Any better methods?