(Z3Py) Denklem için tüm çözümleri gözden geçirme

Question

Z3Py'de, belirli kısıtlamalar için denklemin yalnızca bir çözümü olup olmadığını nasıl kontrol edebilirim?

Birden fazla çözüm varsa, bunları nasıl numaralandırabilirim?

Answer 1

Bunu, Z3 tarafından döndürülen modeli engelleyen yeni bir kısıtlama ekleyerek yapabilirsiniz. Örneğin, Z3 tarafından döndürülen modelde bunu x = 0 ve y = 1 var. Daha sonra, bu modeli kısıtlama Or(x != 0, y != 1) ekleyerek engelleyebiliriz. Aşağıdaki betik hile yapar. Çevrimiçi olarak deneyebilirsiniz: http://rise4fun.com/Z3Py/4blB

Aşağıdaki komut dosyasının birkaç sınırlaması olduğunu unutmayın. Giriş formülü, yorumlanmamış işlevler, diziler veya yorumlanmamış türler içeremez.

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