Problemi di trigger in Z3

Question

Ho osservato di recente diversi comportamenti in Z3 rispetto al trigger, che non capisco. Sfortunatamente, gli esempi provengono da grandi file Boogie, quindi ho pensato di descriverli in astratto per ora, solo per vedere se ci sono risposte ovvie. Tuttavia, se i file concreti fossero migliori, posso allegarli.

Ci sono fondamentalmente tre problemi, anche se il terzo potrebbe essere un caso speciale del secondo. Per quanto riguarda la mia comprensione, nessuno dei comportamenti è previsto, ma forse mi manca qualcosa. Qualsiasi aiuto sarebbe molto apprezzato!

In primo luogo: uguaglianze Trivial nel mio programma sembrano avere ignorato per quanto scatenante è interessato. Ad esempio, se t1 è un termine che dovrebbe corrispondere al modello per un assioma quantificata, se posso aggiungere una riga nel mio programma Boogie della forma

assert t1 == t1; 

poi t1 fa non sembrano abituarsi come trigger per assiomi quantificati. Ho aggiunto esplicitamente la riga per fornire t1 come trigger al prover, cosa che faccio spesso/faccio nei programmi Boogie.

Se invece vi presento una funzione extra, dicono

function f(x : same_type_as_t1) : bool 
{ true } 

e ora invece aggiungere una riga

assert f(t1); 

al mio programma, quindi t1fa sembrano essere usato come un trigger Z3. Ho controllato la traduzione Z3 del programma precedente e l'uguaglianza (banale) su t1 è sopravvissuta alla traduzione di Boogie (ad esempio, non è Boogie che cerca di fare qualcosa di intelligente).

In secondo luogo: schemi secondari non sembrano funzionare correttamente per me. Ad esempio, ho un programma in cui uno assioma ha la forma

axiom (forall ... :: {t1,t2} {t3,t4,t5} .....); 

e una situazione in cui tutti sono verificati t3, t4 e t5. Il programma non riesce a verificare, apparentemente perché l'assioma non è istanziato. Tuttavia, se riscrivo l'assioma come

axiom (forall ... :: {t3,t4,t5} {t1,t2} .....); 

quindi il programma verifica. In entrambi i casi, il tempo di eseguire Boogie è di circa 3 secondi e i pattern sopravvivono all'output Z3.

In terzo luogo: questo potrebbe essere un sintomo del secondo problema, ma sono rimasto sorpreso dal seguente comportamento:

ho scritto assiomi della forma

axiom (forall .. :: {t1,t2} ....); 

axiom (forall ... :: {t2,t4} {t2,t3} ...some expression involving t1...); 

e in un situazione in cui si era verificato t2 e t3, il primo assioma non è stato istanziato (mi aspettavo che fosse, poiché dopo l'istanziazione del secondo assioma, si verifica t1).Tuttavia, se ho riscritto come

axiom (forall .. :: {t2,t3} {t1,t2} ....); 

axiom (forall ... :: {t2,t4} {t2,t3} ...some expression involving t1...); 

quindi il primo assioma è stato istanziato. Tuttavia, se per qualche motivo gli schemi secondari non vengono utilizzati in generale, ciò spiegherebbe anche questo comportamento.

Se esempi espliciti sarebbero utili, posso certamente attaccare quelli lunghi e provare a ridurli un po '(ma ovviamente i problemi di avvio sono un po' delicati, quindi potrei perdere il comportamento se faccio l'esempio troppo piccolo).

Grazie mille in anticipo per qualsiasi consiglio!

Alex Summers

Edit: qui è un esempio che illustra parzialmente il secondo e terzo comportamenti sopra descritti. Ho allegato il codice Boogie per renderlo più facile da leggere qui, ma posso anche copiare o inviare tramite e-mail l'input Z3 se fosse più utile. Ho tagliato quasi tutto il codice originale di Boogie, ma sembra difficile renderlo più semplice senza perdere completamente il comportamento.

Già il codice qui sotto si comporta in modo leggermente diverso dal mio esempio originale, ma penso che sia abbastanza vicino. Fondamentalmente l'assioma etichettato (1) di seguito non riesce a far corrispondere il suo secondo set di schemi. Se commentassi axiom (1), e invece lo sostituissi con gli assiomi (attualmente commentati) (2) e (3), che sono solo copie dell'originale con ciascuno dei due insiemi di modelli, allora il programma verifica. In realtà, è sufficiente avere assioma (2) in questo caso particolare. Nel mio codice originale (prima che lo riducessi) era anche sufficiente capovolgere l'ordine dei due insiemi di modelli nell'assioma (1), ma ciò non sembra più il caso nella mia versione più piccola.

type ref; 
type HeapType; 

function vals1(HeapType, ref) returns (ref); 
function vals2(HeapType, ref) returns (ref); 
function vals3(HeapType, ref) returns (ref); 

function heap_trigger(HeapType) returns (bool); 

function trigger1(ref) returns (bool); 
function trigger2(ref) returns (bool); 

axiom (forall Heap: HeapType, this: ref :: {vals1(Heap, this)} (vals1(Heap, this) == vals3(Heap,this))); 

axiom (forall Heap: HeapType, this: ref :: {vals2(Heap, this)} trigger2(this)); 

// (1) 
axiom (forall Heap: HeapType, this: ref :: {vals1(Heap, this)} {trigger1(this), heap_trigger(Heap), trigger2(this)} (vals1(Heap, this) == vals2(Heap, this))); 

// (2) 
// axiom (forall Heap: HeapType, this: ref :: {trigger1(this), heap_trigger(Heap), trigger2(this)} (vals1(Heap, this) == vals2(Heap, this))); 
// (3)  
// axiom (forall Heap: HeapType, this: ref :: {vals1(Heap, this)} (vals1(Heap, this) == vals2(Heap, this))); 

procedure test(Heap:HeapType, this:ref) 
{ 
    assume trigger1(this); assume heap_trigger(Heap); 

    assert (vals2(Heap, this) == vals3(Heap,this)); 
} 

Answer 1

Prima domanda:

affermazioni banali sono semplificati Z3 durante una fase di pre-elaborazione. L'affermazione assert t1 == t1 è semplificata in assert true. Pertanto, il termine t1 non viene considerato dal motore di corrispondenza elettronica. Il trucco assert f(t1) è quello standard di rendere disponibile un termine t1 per E-matching per Z3. Gli attuali pre-processori in Z3 non sono "abbastanza intelligenti" per rimuovere l'asserzione irrilevante assert f(t1). Naturalmente, una versione futura di Z3 potrebbe avere un pre-processore migliore e il trucco non funzionerà più.

Per la seconda e la terza domanda, sarebbe bello avere (piccoli) script Z3 che producono il comportamento descritto.

Modifica. Ho analizzato l'esempio nella tua domanda. Si scopre che si tratta di un bug in Z3. Ho corretto il bug e la correzione sarà disponibile in Z3 4.1. Grazie per il tempo dedicato a ridurre le dimensioni dell'esempio. Lo apprezzo molto. Ci vorrebbe "per sempre" per trovare questo bug in un'istanza più grande. Il motore di corrispondenza elettronica mancava alcune istanze. Il problema interessa gli script Z3 che contengono pattern multipli che utilizzano un simbolo di funzione f che non si verifica in uno schema unario. Il modello multiplo dovrebbe verificarsi anche prima delle applicazioni di terra. Inoltre, il motore MBQI deve essere disabilitato. Per impostazione predefinita, Boogie disabilita il motore MBQI. In questo scenario, le istanze del modello multiplo potrebbero essere perse. Questo errore era nel motore di corrispondenza elettronica per un tempo molto lungo.Penso che sia stato mai rilevato per due motivi:

1- Non influisce solidità (Z3 non produrrà una risposta sbagliata, ma la risposta “sconosciuto”)

2- Il motore MBQI “compensa” per ogni istanza mancante.

Per quanto riguarda i comandi aggiuntivi per fornire termini aggiuntivi per l'e-matching, possiamo simularlo nel modo seguente. Il comando add_term(t) è solo zucchero di sintassi per (assert (add_term t)). Anche se implementiamo un preprocessore che elimina i simboli di predicato che si verificano solo positivamente (o negativamente), non eliminerà il simbolo del predicato prenotato add_term. Quindi, il trucco continuerà a funzionare anche se aggiungiamo questo pre-processore.