Question(z3py ,Array,SMT): 3 Dimention Array as the other Array's Index

[allen0917-user]

Hi , I'm a z3 beginner from Taiwan.

And I'm trying to implement some constrants (SMT problems )with 2d and 3d arrays，some thing like this:
[
∀k∈[1,2,3]:∀i∈[1,2,3]:∀j∈[1,2,3] #constraint(1)
(w[k][i][j]≥1)∧(w[k][i][j]<5)

∀k∈[1,2,3]:∀i∈[1,2,3]:∀j∈[1,2,3] #constraint(2)
o[k,[w[k],[i],[j]]>2
]

And here is what I'm trying to do:

from z3 import *

# Create solver
s = Solver()

# Create Z3 variables
#w(3d)
w = [ [ [Int("w_%s_%s_%s" % (k+1,i+1, j+1)) 
       for k in range(3) ] 
      for i in range(3) ]for j in range(3)]
#O(2d)
O = [ [ Int("O_%s_%s" % (k+1,w+1)) 
      for w in range(5) ]for k in range(3)]

#constrant1
smt  = [ And(1 <= w[k][i][j], w[k][i][j] <= 5) 
            for k in range(3) for i in range(3) for j in range(3) ]
#constrant2
smt1  = [1 <= O[k,[w[k][i][j]]]
            for k in range(3) for i in range(3) for j in range(3) ]

s.add(smt)
s.add(smt1)

if s.check():                                                               # 检查是否有解
    m=s.model()
    r = [ [ m.evaluate(w[k][i][j])for k in range(3) for i in range(3)] for j in range(3) ] 
print(r)

TypeError: list indices must be integers or slices, not ArithRef

And It seems that i need to declare two of the array with z3 variable, so that i can use them as variables of my constraint.

Array('A', IntSort(), ArraySort(IntSort(), IntSort()))

but i don't know how to implement 3 dimention array with "z3 variable"

I want to know how can i implement "3 dimention array" with z3 variable?and as index of the other array?

Any help , I'll be very appreciate!

[aytey]

How about this:

from z3 import *

s = Solver()

one_dimension_sort = ArraySort(IntSort(), IntSort())
two_dimension_sort = ArraySort(IntSort(), one_dimension_sort)
three_dimension_sort = ArraySort(IntSort(), two_dimension_sort)

one_dimension_array = Const("one", one_dimension_sort)
two_dimension_array = Const("two", two_dimension_sort)
three_dimension_array = Const("three", three_dimension_sort)

s.add(one_dimension_array[1] == 1)
s.add(two_dimension_array[1][1] == 2)
s.add(three_dimension_array[1][1][1] == 3)

assert s.check() == sat
print(s.model())

# EOF

which gives:

[three = K(Int, K(Int, K(Int, 3))),
 two = K(Int, K(Int, 2)),
 one = K(Int, 1)]

(K is for "constant array")

[aytey]

I want to know how can i implement "3 dimention array" with z3 variable?and as index of the other array?

Do you mean you want to index into a second array, giving a second array as the index sort?

If so:

from z3 import *

s = Solver()

one_dimension_sort = ArraySort(IntSort(), IntSort())
two_dimension_sort = ArraySort(one_dimension_sort, IntSort())

array_1 = Const("array_1", one_dimension_sort)
array_2 = Const("array_2", one_dimension_sort)
two_dimension_array = Const("two", two_dimension_sort)

s.add(array_1[1] == 1)
s.add(array_2[2] == 2)
s.add(array_1 != array_2)
s.add(two_dimension_array[array_1] == 1)
s.add(two_dimension_array[array_2] == 2)

assert s.check() == sat
print(s.model())

# EOF

[allen0917-user]

Thanks for your reply ，

i want to restrict 3darray[k][i][j] in 1~2
for i,j,k in range(2)
, so the satisfy value of 3darray is 1 or 2
.
.
.
and i want to give a constraint for 2darray[ k , 3darray[i][j][k] ]
，for i,j,k in range(2) .
which 3d array is the 2d arrays's second index
.
.
.
because 3darray is 1 or 2 ，so 2darray only run 2darray[ k , 1 ] and 2darray[ k , 2 ] two constraint for i,j,k in range(2)

[allen0917-user]

I tried this:

from z3 import *

s = Solver()

one_dimension_sort = ArraySort(IntSort(), IntSort())
two_dimension_sort = ArraySort(IntSort(), one_dimension_sort)
three_dimension_sort = ArraySort(IntSort(), two_dimension_sort)

one_dimension_array = Const("one", one_dimension_sort)
two_dimension_array = Const("two", two_dimension_sort)
three_dimension_array = Const("three", three_dimension_sort)

#3d_constraint
m=[ three_dimension_array[k][i][j]<=2
for k in range(2) for i in range(2) for j in range(2) ]
m1=[ three_dimension_array[k][i][j]>=1
for k in range(2) for i in range(2) for j in range(2) ]

#2d_constraint
m2=[ two_dimension_array[k][three_dimension_array[k][i][j]]==10
for k in range(2) for i in range(2) for j in range(2) ]

s.add(m)
s.add(m1)
s.add(m2)

if s.check():
m=s.model()
r = [ [[ m.evaluate(three_dimension_array[k][i][j])for k in range(2) ]for i in range(2)] for j in range(2) ]
print("three:",r)
t = [ [ [ m.evaluate(two_dimension_array[k][three_dimension_array[k][i][j]])for k in range(2) ]for i in range(2)] for j in range(2) ]
print("two:",t)

but the output is not what i want:

three: [[[1, 2], [1, 2]],
           [[2, 2], [2, 2]]]
two: [[[10, 10], [10, 10]],
        [[10, 10], [10, 10]]]
​

i expect it would be like:(only for [ k , 1 ] and [ k , 2 ])

three: [[[1, 2], [1, 2]],
         [[2, 2], [2, 2]]]
two: [[10, 10], [10, 10]]

[aytey]

Sorry, are you asking for bounded arrays? In SMT, arrays are bounded by the "size" of the input domain (as you're using Int, which is unbounded, this means that your arrays are of unbounded size).

If you're after something that is "limited" to a maximum of 3, then you could use a BitVec of size 2:

from z3 import *

s = Solver()

elem_sort = BitVecSort(2)

one_dimension_sort = ArraySort(elem_sort, elem_sort)
two_dimension_sort = ArraySort(elem_sort, one_dimension_sort)
three_dimension_sort = ArraySort(elem_sort, two_dimension_sort)

one_dimension_array = Const("one", one_dimension_sort)
two_dimension_array = Const("two", two_dimension_sort)
three_dimension_array = Const("three", three_dimension_sort)

s.add(one_dimension_array[1] == 1)
s.add(two_dimension_array[1][1] == 2)
s.add(three_dimension_array[1][1][1] == 3)

assert s.check() == sat
print(s.model())

# EOF

If you're after more precision than this (e.g., you only want 1, 2 and 3, but not 0), then you'll probably need to put some s.add(And([1 >= idx, idx <= 3])) in your code to restrict the input domain.

[aytey]

This line:

one_dimension_sort = ArraySort(elem_sort, elem_sort)

doesn't have to map elem_sort to elem_sort; you could map BitVecSort(2) to IntSort, but I think because you want to do stuff like this:

two_dimension_array[k][three_dimension_array[k][i][j]]==10

you have to make sure that the codomain of three_dimension_array matches the domain of (the second level of) two_dimension_array.

[allen0917-user]

Oh okay i got it ,
Thanks for your reply, thank you so much !