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]]