Supponiamo che a sia un numero intero di 8 bit del valore 254. Se a è un numero intero con segno, viene in realtà considerato -2. Al contrario, se a non è firmato, rimane 254.Come modellare il numero intero con segno con BitVector?
Sto provando a modellare questo problema con segno/senza segno con la teoria di BitVector con Z3, ma sembra che BitVector non lo consenta. È vero? Quindi qualche idea su come modellare questo in Z3py?
Grazie mille.
Z3 ha API per le interpretazioni firmati e non firmati. Ad esempio, nell'API C, Z3_mk_bvslt crea il carattere firmato meno di, e Z3_mk_bvult quello senza segno. In Z3Py, abbiamo sovraccaricato <, <=, ... utilizzando quelli firmati. Per creare, il unsigned a < b, dobbiamo usare ULT(a,b). Ecco l'elenco degli operatori non firmati: ULE (<=), ULT (<), UGE (>=), UGT (>), UDiv (divisione senza segno), URem (resto senza segno). E 'possibile trovare maggiori informazioni qui:
http://research.microsoft.com/en-us/um/redmond/projects/z3/namespacez3py.html
È corretto osservare che i valori del vettore di bit non portano un segno. D'altra parte, ci sono versioni firmate di operazioni e relazioni bit-vettore. Quindi è possibile trattare la stessa entità bit vettoriale di un numero firmato o senza segno passandoli a un confronto firmato o senza segno (firmato meno/senza segno) o con segno o senza segno (divisione firmata/divisione senza segno). Altre operazioni aritmetiche funzionano allo stesso modo su entità firmate e non firmate. Ad esempio, l'aggiunta sposta i bit nello stesso modo, sia che li si desideri interpretarli come firmati o non firmati.
Z3 segue le convenzioni delle teorie SMT-LIB2, e si può trovare un'ampia documentazione su questi su: http://smtlib.cs.uiowa.edu/theories/FixedSizeBitVectors.smt2
risposta Eccellente come sempre! Grazie Leo! – user311703