Cuál es la razón detrás del mensaje de advertencia en Z3: "no se pudo encontrar un patrón para el cuantificador (identificación del cuantificador: k! 18)"

Question

Encontré un problema como se muestra en el siguiente programa simple SMT-LIB.

El código SMT-LIB:

(declare-fun isDigit (Int) Bool) 
(assert (forall ((x Int)) 
    (=>  (isDigit x) 
     (and (>= x 0) (< x 10)) 
    ) 
) 
) 

(assert (forall ((x Int)) 
    (=>  (and (>= x 12) (< x 15)) 
     (exists ((y Int)) 
      (and (>= y 1) (< y 6) 
       (isHost (- x y)) 
      ) 
     ) 
    ) 
) 
) 

(check-sat) 
(get-model) 

Esto da la siguiente advertencia:

WARNING: failed to find a pattern for quantifier (quantifier id: k!18) 
sat 
........ 
........ 

Me gustaría saber el mensaje de advertencia. Sé que me estoy perdiendo algo, pero no puedo entender. ¿Alguien puede ayudarme en este tema?

Answer 1

Z3 utiliza diferentes motores para el manejo de cuantificadores (ver Z3 guide). Uno de estos motores se basa en la coincidencia de patrones (E-Matching). Z3 intenta inferir patrones para cada fórmula cuantificada. Si no puede encontrar uno, emite el mensaje de advertencia. El usuario también puede proporcionar patrones para cada cuantificador. La guía muestra cómo hacerlo. El ID k!18 es el ID predeterminado creado por Z3. Se basa en el número de línea (línea 18 en su caso). También puede proporcionar sus propios identificadores para cuantificadores. La advertencia solo les dice a los usuarios que el motor de correspondencia electrónica no podrá manejar el cuantificador especificado.