您可以通过添加新的约束来阻止Z3返回的模型来做到这一点。例如，假设在Z3返回的模型中，我们有
x = 0和
y =1。然后，我们可以通过添加约束来阻止此模型
Or(x != 0, y !=1)。以下脚本可以解决问题。您可以在以下位置在线尝试：http :
//rise4fun.com/Z3Py/4blB
请注意，以下脚本有两个限制。输入公式不能包含未解释的函数，数组或未解释的排序。
from z3 import *# Return the first "M" models of formula list of formulas F def get_models(F, M): result = [] s = Solver() s.add(F) while len(result) < M 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# Return True if F has exactly one model.def exactly_one_model(F): return len(get_models(F, 2)) == 1x, y = Ints('x y')s = Solver()F = [x >= 0, x <= 1, y >= 0, y <= 2, y == 2*x]print get_models(F, 10)print exactly_one_model(F)print exactly_one_model([x >= 0, x <= 1, y >= 0, y <= 2, 2*y == x])# Demonstrate unsupported featurestry: a = Array('a', IntSort(), IntSort()) b = Array('b', IntSort(), IntSort()) print get_models(a==b, 10)except Z3Exception as ex: print "Error: ", extry: f = Function('f', IntSort(), IntSort()) print get_models(f(x) == x, 10)except Z3Exception as ex: print "Error: ", ex
