Sì, ci sono essenzialmente due modalità incrementali.
In pila: utilizzando push(), pop() si crea un contesto locale, che segue una disciplina di stack. Le asserzioni aggiunte sotto un push() vengono rimosse dopo un pop corrispondente(). Inoltre, tutti i lemmi derivati da una spinta vengono rimossi. Utilizzare push()/pop() per emulare il congelamento di uno stato e aggiungere ulteriori vincoli sullo stato congelato, quindi riprendere lo stato congelato. Ha il vantaggio che qualsiasi overhead di memoria addizionale (come i lemmi appresi) creato nell'ambito di un push() viene rilasciato. L'ipotesi di lavoro è che i lemmi appresi sotto una spinta non sarebbero più utili.
Assunzione base: usando lettere assunzione aggiuntivi passati per verificare()/check_sat() è possibile (1) estratto nuclei insoddisfacibile nel corso degli letterali assunzione, (2) guadagnare incrementalità locale senza lemmi della spazzatura raccolta che vengono derivate indipendentemente dalle ipotesi . In altre parole, se Z3 impara un lemma che non contiene nessuno dei presupposti letterali, si aspetta di non raccoglierli. Per utilizzare efficacemente i letterali di presupposto, dovresti aggiungerli anche alle formule. Quindi il compromesso è che le clausole usate con le assunzioni contengono una certa quantità di bloat. Ad esempio, se si desidera assumere localmente una formula (< = xy), aggiungere una clausola (=> p (< = xy)) e assumere p quando si chiama check_sat(). Si noti che l'ipotesi originale era un'unità. Z3 diffonde le unità in modo efficiente. Con la formulazione che utilizza i letterali di assunzione non è più un'unità al livello di base della ricerca. Ciò comporta un ulteriore sovraccarico. Le unità diventano clausole binarie, le clausole binarie diventano clausole ternarie, ecc.
La differenziazione tra funzionalità push/pop vale per il motore SMT predefinito di Z3. Questo è il motore che la maggior parte delle formule utilizzerà. Z3 contiene alcuni portfolio di motori. Ad esempio, per i problemi con il vettore di bit puro, Z3 può finire per utilizzare il motore basato su sat. L'incrementalità nel motore basato su sat è implementata in modo diverso rispetto al motore predefinito. Qui l'incrementalità è implementata usando i letterali di presupposto. Ogni asserzione che aggiungi nell'ambito di una spinta è asserita come implicazione (=> formula scope_literals). check_sat() all'interno di tale ambito dovrà occuparsi di valori letterali di assunzione. Sul rovescio della medaglia, qualsiasi conseguenza (lemma) che non dipende dall'ambito corrente è non garbage collection su pop().
In modalità di ottimizzazione, quando si asseriscono obiettivi di ottimizzazione o quando si utilizzano gli oggetti di ottimizzazione sull'API, è anche possibile richiamare il push/pop. Allo stesso modo con punti fissi. Per queste due funzionalità, push/pop sono essenzialmente utili per l'utente. Non c'è incrementalità interna. Il motivo è che queste due modalità utilizzano una pre-elaborazione sostanziale super-non incrementale.
fonte
2016-11-04 16:35:20