QF_FPA? Z3 supporta l'aritmetica IEEE-754?

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?

fonte

2013-03-03 Levent Erkok

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)

fonte

2013-03-04 11:11:45

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

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)

fonte

2015-10-30 15:46:57

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. –

QF_FPA? Z3 supporta l'aritmetica IEEE-754?

risposta

Problemi correlati