Z3 Python Check whether pairs are distinct

Question

I have a 2 matrices, each of them are 3 by 3 (call them M1 and M2, each of their entries are of type Int in Z3. I need to add the constraint that says all pairs of the form ([M1[i][j], M2[i][j]) are distinct (i and j are arbitrary indices for the matrix).

In other words,

if   (i1,j1) != (i2,j2) 
then ([M1[i1][j1], M2[i1][j1]) != ([M1[i2][j2], M2[i1][j2])

I tried making an array of all the pairs, called array, then using Distinct(array), but this doesn't seem to work since I get an error saying

"At least one of the arguments must be a Z3 expression"

Is there a way to see if 2 pairs of integers are distinct in Z3 for Python? And if not what's a good way to enable the constraint that the pairs described above are distinct?

Answer 1

Something like this?

from z3 import *

def CreateMatrix(name, rows, cols):
    a=[] 
    for row in range(rows): 
        b=[]
        for col in range(cols): 
            v = Int(name + str(row+1) + str(col+1))
            b.append(v)
        a.append(b)
    return a

def ShowMatrix(model, name, mat, rows, cols):
    print()
    print("Matrix " + name)
    for row in range(rows):
        s = ""
        for col in range(cols):
            s = s + str(model.eval(mat[row][col])).ljust(4)
        print(s)

s = Solver()
rows = 3
cols = 3
M1 = CreateMatrix('M1', rows, cols)
M2 = CreateMatrix('M2', rows, cols)

for row1 in range(rows):
    for col1 in range(cols):
        for row2 in range(rows):
            for col2 in range(cols):
                s.add(M1[row1][col1] != M2[row2][col2])

print(s.check())

ShowMatrix(s.model(), "M1", M1, rows, cols)
ShowMatrix(s.model(), "M2", M2, rows, cols)

The constraints for pairwise inequality are added in a fourfold nested loop. For 3x3 matrices, this results in 81 constraints.