Navigando sul codice sorgente Z3, mi sono imbattuto in un mucchio di file che si riferiscono a QF_FPA, che sembra rappresentare un'aritmetica a virgola mobile, senza quantificatori. Tuttavia, non riesco a trovare alcuna documentazione relativa al suo stato, né come possa essere utilizzato attraverso vari front-end (in particolare SMT-Lib2). È una codifica di IEEE-754 FP? In tal caso, quali precisioni/operazioni sono supportate? Tutta la documentazione sarebbe molto utile ..QF_FPA? Z3 supporta l'aritmetica IEEE-754?
risposta
Sì, Z3 supporta l'aritmetica in virgola mobile proposta da Ruemmer e Wahl in una recente officina SMT paper. Allo stato attuale, non esiste una teoria ufficiale FPA, e il supporto di Z3 è molto semplice (solo un po 'blaster). Non lo pubblichiamo ancora attivamente, ma può essere utilizzato esattamente come proposto nel documento di Ruemmer/Wahl (impostazione logiche QF_FPA e QF_FPABV). Al momento stiamo lavorando a una nuova procedura decisionale per l'FPA, ma ci vorrà del tempo prima che sia disponibile.
Ecco un breve esempio di ciò che una formula FPA SMT2 potrebbe apparire come:
(set-logic QF_FPA)
(declare-const x (_ FP 11 53))
(declare-const y (_ FP 11 53))
(declare-const r (_ FP 11 53))
(assert (and
(= x ((_ asFloat 11 53) roundTowardZero 0.5 0))
(= y ((_ asFloat 11 53) roundTowardZero 0.5 0))
(= r (+ roundTowardZero x y))
))
(check-sat)
Le logiche in virgola mobile sono chiamati QF_FP e QF_FPBV in v4.4.2. Il collegamento alla descrizione della teoria in RELEASE_NOTES è rotto. La pagina corretta è http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml. L'esempio proposto sopra deve essere
(set-logic QF_FP)
(declare-const x (_ FloatingPoint 11 53))
(declare-const y (_ FloatingPoint 11 53))
(declare-const r (_ FloatingPoint 11 53))
(assert (and
(= x (fp #b0 #b00000000010 #b0000000000000000000000000000000000000000000000000010))
(= y (fp #b0 #b00000000010 #b0000000000000000000000000000000000000000000000000010))
(= r (fp.add roundTowardZero x y))
))
(check-sat)
Grazie Daniel per aver aggiornato l'esempio! Lo standard SMT FP è stato aggiornato da allora e questa è davvero la nuova sintassi. Abbiamo rimosso tutti i vecchi simboli da Z3 e supportiamo solo lo standard finale. –
- 1. Lettura interp di un array z3 dal modello z3
- 2. Quantificatore in Z3
- 3. z3 C++ API & ite
- 4. Interpretazione delle statistiche Z3
- 5. Controlla overflow con Z3
- 6. Supporto quantificatore Z3
- 7. Problemi di trigger in Z3
- 8. Come nascondere variabile con Z3
- 9. Output di controesempio di Z3
- 10. Serializzazione portatile dei valori a virgola mobile IEEE754
- 11. Lua - imballaggio numeri a virgola mobile in singola precisione IEEE754
- 12. Z3: trovare tutti i modelli soddisfacenti
- 13. Come ottenere risultati casuali da Microsoft Z3?
- 14. Come funziona la risoluzione incrementale in Z3?
- 15. Comprensione dell'indicizzazione delle variabili associate in Z3
- 16. (get-unsat-core) restituisce vuoto in Z3
- 17. Z3 Performance con aritmetica non lineare
- 18. formule di risolutore interno in z3
- 19. Alla ricerca di esempi pratici di applicazioni SMT Z3 (come DbC) e alternative open source a Z3?
- 20. Il riferimento di conteggio riferimenti Z3_ast fa riferimento a Z3?
- 21. Teoria della matrice degli array SMTLIB in Z3
- 22. È possibile utilizzare Z3 per ragionare su sottostringhe?
- 23. È possibile utilizzare Z3 per eseguire il preprocesso dei problemi?
- 24. un tipo di dati contiene un set in Z3
- 25. Z3/Python che ottiene i valori di python dal modello
- 26. Definizione di una teoria di insiemi con Z3/SMT-LIB2
- 27. È consigliabile utilizzare il NaN in virgola mobile IEEE754 per i valori non impostati?
- 28. C'è un modo di vedere un numero nella sua float rappresentazione IEEE754 a 64 bit
- 29. SQL Azure supporta o non supporta gli assembly CLR?
- 30. JSONKit supporta ARC oppure esiste un fork che supporta ARC?
Questo supporto per l'aritmetica in virgola mobile è stato incorporato nell'ultima versione stabile 4.3.2 di z3? Inoltre, il supporto della teoria in virgola mobile è stato combinato con altre teorie, ad es. Con aritmetica lineare intera, in versione stabile o instabile? – user1779685
4.3.2 aveva solo un supporto parziale, la versione corrente è 4.4.0, che ha pieno supporto, inclusa la combinazione di teoria. Si noti che la conversione da numero in virgola mobile a numero reale/razionale introduce vincoli non lineari, quindi anche la combinazione con l'aritmetica lineare diventa non lineare. –
Grazie per la conoscenza sulla combinazione di conversione e teoria. Ho controllato su github: la versione z3 di aprile con un supporto più ampio è una grande notizia. Proverò presto. – user1779685