Z3 Performance con aritmetica non lineare

Question

Stiamo riscontrando problemi di prestazioni con quello che ritengo sia la parte di Z3 che tratta l'aritmetica non lineare. Ecco un semplice esempio concreto di Boogie, che quando verificato con Z3 (versione 4.1) richiede molto tempo (dell'ordine di 3 minuti) per essere completato.

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; 
} 

Sembra che il problema è causato da un'interazione di funzioni, gamma assunto su variabili intere nonché moltiplicazioni di valori (Sconosciuto) interi. L'affermazione alla fine non dovrebbe essere dimostrabile. Invece di fallire rapidamente, sembra che Z3 abbia modi per istanziare un sacco di termini in qualche modo, poiché i suoi consumi di memoria crescono abbastanza velocemente a circa 300 MB, a quel punto si arrende.

Mi chiedo se questo sia un bug o se sia possibile migliorare l'euristica quando Z3 deve interrompere la ricerca nella direzione specifica in cui sta attualmente cercando di risolvere il problema.

Una cosa interessante è che inlining la funzione utilizzando

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

rende la verifica terminare molto rapidamente.

Background: questo è un caso di prova minimo per un problema che vediamo nel nostro verificatore Chalice. Lì, i programmi Boogie diventano molto più lunghi, potenzialmente con più ipotesi di un tipo simile. Spesso, la verifica non sembra affatto terminare.

Qualche idea?

Answer 1

Sì, la non terminazione è dovuta all'aritmetica dei numeri interi non lineari. Z3 ha un nuovo solutore non lineare, ma è per "aritmetica reale non lineare" e può essere utilizzato solo in problemi quantificatori che utilizzano solo l'aritmetica (cioè, nessuna funzione non interpretata come nell'esempio). Quindi, il vecchio risolutore aritmetico è usato nel tuo esempio. Questo risolutore ha un supporto molto limitato per l'aritmetica dei numeri interi. La tua analisi del problema è corretta. Z3 ha difficoltà a trovare una soluzione per il blocco dei vincoli di interi non lineari. Notare che se sostituiamo f(100) * b == a * c con f(100) * b <= a * c, Z3 restituisce immediatamente una risposta "sconosciuta".

Possiamo evitare la mancata limitazione limitando il numero di ragionamento aritmetico non lineare in Z3. L'opzione NL_ARITH_ROUNDS=100 utilizzerà il modulo non lineare al massimo 100 volte per ogni query Z3. Questa non è una soluzione ideale, ma almeno evitiamo la non-terminazione.