(Z3Py) comprobando todas las soluciones para la ecuación

Question

En Z3Py, ¿cómo puedo verificar si la ecuación para las restricciones dadas tiene una sola solución?

Si hay más de una solución, ¿cómo puedo enumerarlas?

Answer 1

Puede hacerlo agregando una nueva restricción que bloquea el modelo devuelto por Z3. Por ejemplo, supongamos que en el modelo devuelto por Z3 tenemos ese x = 0 y y = 1. Entonces, podemos bloquear este modelo agregando la restricción Or(x != 0, y != 1). La siguiente secuencia de comandos funciona. Puede intentarlo en línea en: http://rise4fun.com/Z3Py/4blB

Tenga en cuenta que la siguiente secuencia de comandos tiene un par de limitaciones. La fórmula de entrada no puede incluir funciones no interpretadas, matrices o géneros no interpretados.

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