Max of a list of vectors of Boolean using z3 for resolution of SAT problem

I am working on a Sat project, one of my subtasks is to compute the max of a list of a vectors of boolean, each of them is a number. An example of the vector is [False,True,True,False], it represents the number 2^2 + 2^1 = 6. In this resolution I cannot use the Int data of z3, but I must use only the Bool data of z3. To solve this problem I tried to use the following code, but it doesn't work.

from z3 import *
def greater(vec1, vec2, name):
   
    constraints = []
    gt = [Bool(f"gt_{name}{i}") for i in range(len(vec1))]
    
    constraints.append(
                And(
                    [
                    Implies(Not(vec1[0]), Not(vec2[0])),
                    Implies(And(vec1[0], Not(vec2[0])), gt[0]),
                    Implies(Not(Xor(vec1[0], vec2[0])), Not(gt[0]))]
                )
            )
    

    for i in range(1, len(vec1)):
        constraints.append(
            And(
            Or(gt[i-1], 
                And(
                [
                Implies(Not(vec1[i]), Not(vec2[i])),
                Implies(And(vec1[i], Not(vec2[i])), gt[i]),
                Implies(Not(Xor(vec1[i], vec2[i])), Not(gt[i]))]
                )    
            ),
            Implies(gt[i-1], gt[i])
        )
    )     
    return And(constraints)



def max_of_bin_int(values, max_values):

    constraints = []
    len_bits = len(values[0])
    constraints.append(
        And([max_values[0][j] == values[0][j] for j in range(len_bits)]),
    )

    for i in range(0, len(values)-1):
        constraints.append(
            If(greater(max_values[i], values[i+1], f"max{i}"), 
                And([max_values[i+1][j] == max_values[i][j] for j in range(len_bits)]),
                And([max_values[i+1][j] == values[i+1][j] for j in range(len_bits)])
        )
       )
    return And(constraints)


# Testing 
values = [ [True,True,True,False],
       [True,True,False,False],
        [True,True,False,False]
]

s = Solver()
max_values = [[Bool(f"x_{i}_{j}") for j in range(len(values[0]))] for i in range(len(values)) ]
s.add(max_of_bin_int(values, max_values))
print(s.check())
m = s.model()

print([m.evaluate(max_values[-1][j]) for j in range(len(values[0]))] )

The result that returns the function is [True, True, False, False] but it should be [True,True,True,False]. Can someone helps me?
Important:
I cannot use Int data of z3 only Bool data.

I am expecting a function that returns the constraints to find the maximum value of list of Boolean vectors to be used in a solver.

The following variant of your code works for me:

from z3 import *

def greater(vec1, vec2):
    """
    cf. https://en.wikipedia.org/wiki/Digital_comparator
    """
    bits = len(vec1)
    msb = bits-1
    gt = And(vec1[msb], Not(vec2[msb]))    
    x = (vec1[msb] == vec2[msb])

    for i in reversed(range(msb)):
        gt = Or(gt, And(x, vec1[i], Not(vec2[i])))
        x = And(x, (vec1[i] == vec2[i]))

    return gt


def max_of_bin_int(values, max_values):
    rBits = range(len(values[0]))
    constraints = [max_values[0][j] == values[0][j] for j in rBits]

    for i in range(1, len(values)):
        gt = greater(max_values[i-1], values[i])
        constraints.append(
           And([max_values[i][j] == If(gt, max_values[i-1][j], values[i][j]) for j in rBits])
        )
 
    return And(constraints)


# Testing 
values = [[True,True,True,False],
          [True,True,False,False],
          [True,True,True,True],
          [True,True,False,False]
]

s = Solver()
rColumns = range(len(values[0]))
rRows = range(len(values))
max_values = [[Bool(f"x_{row}_{col}") for col in rColumns] for row in rRows]
s.add(max_of_bin_int(values, max_values))
print(s.check())
m = s.model()

print([m.evaluate(max_values[-1][col]) for col in rColumns] )

I've changed the vector comparator logic inspired by Wikipedia. Your greater function does not return a proper condition to control the If() function. It performs the comparison in the wrong bit-order. A digital comparator starts at the most-significant-bit (msb) and descends to the least-significant-bit. I am using reversed(range()) to get the order right.