#!/usr/bin/env python3

from z3 import And, Int, Solver, sat

# 矩阵
m = [
    [1, 2, 3, 4, 5],
    [2, 3, 4, 5, 6],
    [3, 4, 5, 6, 7],
    [4, 5, 6, 7, 8],
    [5, 6, 7, 8, 9],
]

# 每一行的系数
vars = [Int(f'v{i}') for i in range(5)]

# 将系数乘上去并计算每列的和
final = []
for i in range(5):
    final.append(sum([a * b for a, b in zip([l[i] for l in m], vars)]))

s = Solver()

# 添加约束条件
s.add(final[0] > 5)
s.add(final[1] < 600)
s.add(final[2] > 7)
s.add(final[3] < 800)
s.add(final[4] > 9)

while s.check() == sat:
    m = s.model()
    print(m)
    # 排除掉这个解
    s.add(And(*[i != m[i] for i in vars]))

print('finish')