Rendimiento Z3 con aritmética no lineal

Question

Estamos teniendo problemas de rendimiento con lo que creo que es la parte de Z3 que trata la aritmética no lineal. Aquí hay un ejemplo concreto de Boogie, que cuando se verifica con Z3 (versión 4.1) tarda mucho tiempo (del orden de 3 minutos) en completarse.

const D: int; 
function f(n: int) returns (int) { n * D } 

procedure test() returns() 
{ 
    var a, b, c: int; 
    var M: [int]int; 
    var t: int; 

    assume 0 < a && 1000 * a < f(1); 
    assume 0 < c && 1000 * c < f(1); 
    assume f(100) * b == a * c; 

    assert M[t] > 0; 
} 

Parece que el problema está causado por una interacción de las funciones, la asunción gama de variables enteras así como multiplicaciones de valores (desconocido) enteros. La afirmación al final no debe ser comprobable. En lugar de fallar rápidamente, parece que Z3 tiene formas de instanciar muchos términos de alguna manera, ya que sus consumos de memoria crecen bastante rápido a unos 300 MB, momento en el que se da por vencido.

Me pregunto si esto es un error, o si es posible mejorar la heurística en cuando Z3 debería detener la búsqueda en la dirección particular en la que actualmente está tratando de resolver el problema.

Una cosa interesante es que la función inline utilizando

function {:inline} f(n: int) returns (int) { n * D } 

realiza la verificación terminar muy rápidamente.

Antecedentes: Este es un caso de prueba mínimo para un problema que vemos en nuestro verificador Chalice. Allí, los programas de Boogie son mucho más largos, potencialmente con múltiples suposiciones de un tipo similar. A menudo, la verificación no parece terminar en absoluto.

¿Alguna idea?

Answer 1

Sí, la no terminación se debe a la aritmética de enteros no lineales. Z3 tiene un nuevo solucionador no lineal, pero es para "aritmética real no lineal", y solo se puede usar en problemas sin cuantificadores que solo usan aritmética (es decir, funciones no interpretadas como en su ejemplo). Por lo tanto, el viejo solucionador de aritmética se usa en su ejemplo. Este solucionador tiene un soporte muy limitado para la aritmética de enteros. Tu análisis del problema es correcto. Z3 tiene problemas para encontrar una solución para el bloque de restricciones enteras no lineales. Tenga en cuenta que si reemplazamos f(100) * b == a * c con f(100) * b <= a * c, entonces Z3 regresa inmediatamente con una respuesta "desconocida".

Podemos evitar la no terminación al limitar el número de razonamiento aritmético no lineal en Z3. La opción NL_ARITH_ROUNDS=100 usará el módulo no lineal como máximo 100 veces para cada consulta Z3. Esta no es una solución ideal, pero al menos evitamos la no terminación.