z3 获取所有解

from z3 import *

def get_models(s, count = 1):
    result = []
    while len(result) < count and s.check() == sat:
        m = s.model()
        result.append(m)
        # Create a new constraint the blocks the current model
        block = []
        for d in m:
            # d is a declaration
            if d.arity() > 0:
                raise Z3Exception("uninterpreted functions are not supported")
            # create a constant from declaration
            c = d()
            if is_array(c) or c.sort().kind() == Z3_UNINTERPRETED_SORT:
                raise Z3Exception("arrays and uninterpreted sorts are not supported")
            block.append(c != m[d])
        s.add(Or(block))
    return result

x, y = Ints('x y')
s = Solver()
s.add(And(And(x > 0, y > 0), x * y < 10))
m = get_models(s, 1000) # 获取最多1000个解
print(m)
# [[x = 8, y = 1], [x = 1, y = 2], [x = 2, y = 1], [x = 9, y = 1], [x = 4, y = 2], [x = 3, y = 2], [x = 2, y = 2], [x = 1, y = 3], [x = 1, y = 4], [x = 1, y = 5], [x = 1, y = 6], [x = 1, y = 7], [x = 1, y = 8], [x = 1, y = 9], [x = 2, y = 4], [x = 3, y = 3], [x = 5, y = 1], [x = 6, y = 1], [x = 7, y = 1], [x = 4, y = 1], [x = 3, y = 1], [x = 2, y = 3], [x = 1, y = 1]]