(Z3Py) Überprüfung aller Lösungen für die Gleichung

Question

Wie kann ich in Z3Py überprüfen, ob die Gleichung für gegebene Einschränkungen nur eine Lösung hat?

Wenn mehr als eine Lösung, wie kann ich sie aufzählen?

Answer 1

Sie können das tun, indem Sie eine neue Einschränkung hinzufügen, die das von Z3 zurückgegebene Modell blockiert. Angenommen, in dem von Z3 zurückgegebenen Modell haben wir x = 0 und y = 1. Dann können wir dieses Modell blockieren, indem wir die Bedingung Or(x != 0, y != 1) hinzufügen. Das folgende Skript macht den Trick. Sie können es online ausprobieren unter: http://rise4fun.com/Z3Py/4blB

Beachten Sie, dass das folgende Skript ein paar Einschränkungen hat. Die Eingabeformel darf keine nicht interpretierten Funktionen, Arrays oder nicht interpretierten Sortierungen enthalten.

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)) == 1 

x, 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 features 
try: 
    a = Array('a', IntSort(), IntSort()) 
    b = Array('b', IntSort(), IntSort()) 
    print get_models(a==b, 10) 
except Z3Exception as ex: 
    print "Error: ", ex 

try: 
    f = Function('f', IntSort(), IntSort()) 
    print get_models(f(x) == x, 10) 
except Z3Exception as ex: 
    print "Error: ", ex